suzanne.soy/racket
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

Make cgen/seq take its args in the correct order.

Browse Source
This commit is contained in:
Eric Dobson 2014-05-11 12:40:11 -07:00
parent 5b02971615
commit 7e0872d282
1 changed files with 44 additions and 42 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

86
pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/infer/infer-unit.rkt
View File

@ -207,30 +207,29 @@
;; FIXME - do something here ;; FIXME - do something here
[(_ _) #f])) [(_ _) #f]))
;; Currently checks is t-seq <: s-seq.
(define/cond-contract (cgen/seq V X Y s-seq t-seq) (define/cond-contract (cgen/seq V X Y s-seq t-seq)
((listof symbol?) (listof symbol?) (listof symbol?) seq? seq? . -> . (or/c #f cset?)) ((listof symbol?) (listof symbol?) (listof symbol?) seq? seq? . -> . (or/c #f cset?))
(match*/early (s-seq t-seq) (match*/early (s-seq t-seq)
;; The simplest case - both are null-end ;; The simplest case - both are null-end
[((seq ss (null-end)) [((seq ss (null-end))
(seq ts (null-end))) (seq ts (null-end)))
(cgen/list V X Y ts ss)] (cgen/list V X Y ss ts)]
;; One is null-end the other is uniform-end ;; One is null-end the other is uniform-end
[((seq ss (null-end)) [((seq ss (null-end))
(seq ts (uniform-end t-rest))) (seq ts (uniform-end t-rest)))
#f] (and
(<= (length ts) (length ss)))
(cgen/list V X Y ss (extend ss ts t-rest))]
[((seq ss (uniform-end s-rest)) [((seq ss (uniform-end s-rest))
(seq ts (null-end))) (seq ts (null-end)))
(and #f]
(<= (length ss) (length ts)))
(cgen/list V X Y ts (extend ts ss s-rest))]
;; Both are uniform-end ;; Both are uniform-end
[((seq ss (uniform-end s-rest)) [((seq ss (uniform-end s-rest))
(seq ts (uniform-end t-rest))) (seq ts (uniform-end t-rest)))
(cgen/list V X Y (cgen/list V X Y
(cons t-rest (extend ss ts t-rest)) (cons s-rest (extend ts ss s-rest))
(cons s-rest (extend ts ss s-rest)))] (cons t-rest (extend ss ts t-rest)))]
;; dotted on the left, nothing on the right ;; dotted below, nothing above
[((seq ss (dotted-end dty dbound)) [((seq ss (dotted-end dty dbound))
(seq ts (null-end))) (seq ts (null-end)))
#:return-unless (memq dbound Y) #:return-unless (memq dbound Y)
@ -243,18 +242,18 @@
[new-s-seq (seq (append ss new-tys) (null-end))] [new-s-seq (seq (append ss new-tys) (null-end))]
[new-cset (cgen/seq V (append vars X) Y new-s-seq t-seq)]) [new-cset (cgen/seq V (append vars X) Y new-s-seq t-seq)])
(% move-vars-to-dmap new-cset dbound vars))] (% move-vars-to-dmap new-cset dbound vars))]
;; dotted on the right, nothing on the left ;; dotted above, nothing below
[((seq ss (null-end)) [((seq ss (null-end))
(seq ts (dotted-end dty dbound))) (seq ts (dotted-end dty dbound)))
#:return-unless (memq dbound Y) #:return-unless (memq dbound Y)
#f #f
#:return-unless (<= (length ts) (length ss)) #:return-unless (<= (length ts) (length ss))
#f #f
(let* ([vars (var-store-take dbound dty (- (length ss) (length ts)))] (let* ([vars (var-store-take dbound dty (- (length ss) (length ts)))]
[new-tys (for/list ([var (in-list vars)]) [new-tys (for/list ([var (in-list vars)])
(substitute (make-F var) dbound dty))] (substitute (make-F var) dbound dty))]
[new-t-seq (seq (append ts new-tys) (null-end))] [new-t-seq (seq (append ts new-tys) (null-end))]
[new-cset (cgen/seq V (append vars X) Y s-seq new-t-seq)]) [new-cset (cgen/seq V (append vars X) Y s-seq new-t-seq)])
(% move-vars-to-dmap new-cset dbound vars))] (% move-vars-to-dmap new-cset dbound vars))]
;; this case is just for constrainting other variables, not dbound ;; this case is just for constrainting other variables, not dbound
[((seq ss (dotted-end s-dty dbound)) [((seq ss (dotted-end s-dty dbound))
@ -264,47 +263,51 @@
;; If we want to infer the dotted bound, then why is it in both types? ;; If we want to infer the dotted bound, then why is it in both types?
#:return-when (memq dbound Y) #:return-when (memq dbound Y)
#f #f
(let* ([arg-mapping (cgen/list V X Y ts ss)] (let* ([arg-mapping (cgen/list V X Y ss ts)]
[darg-mapping (cgen V X Y t-dty s-dty)]) [darg-mapping (cgen V X Y s-dty t-dty)])
(% cset-meet arg-mapping darg-mapping))] (% cset-meet arg-mapping darg-mapping))]
;; bounds are different ;; bounds are different
[((seq ss (dotted-end s-dty (? (λ (db) (memq db Y)) dbound))) [((seq ss (dotted-end s-dty (? (λ (db) (memq db Y)) dbound)))
(seq ts (dotted-end t-dty dbound*))) (seq ts (dotted-end t-dty dbound*)))
#:return-unless (= (length ss) (length ts)) #f #:return-unless (= (length ss) (length ts)) #f
#:return-when (memq dbound* Y) #f #:return-when (memq dbound* Y) #f
(let* ([arg-mapping (cgen/list V X Y ts ss)] (let* ([arg-mapping (cgen/list V X Y ss ts)]
;; just add dbound as something that can be constrained ;; just add dbound as something that can be constrained
[darg-mapping [darg-mapping
(extend-tvars (list dbound*) (extend-tvars (list dbound*)
(% move-dotted-rest-to-dmap (cgen V (cons dbound X) Y t-dty s-dty) dbound dbound*))]) (% move-dotted-rest-to-dmap (cgen V (cons dbound X) Y s-dty t-dty) dbound dbound*))])
(% cset-meet arg-mapping darg-mapping))] (% cset-meet arg-mapping darg-mapping))]
[((seq ss (dotted-end s-dty dbound)) [((seq ss (dotted-end s-dty dbound))
(seq ts (dotted-end t-dty (? (λ (db) (memq db Y)) dbound*)))) (seq ts (dotted-end t-dty (? (λ (db) (memq db Y)) dbound*))))
#:return-unless (= (length ss) (length ts)) #f #:return-unless (= (length ss) (length ts)) #f
(let* ([arg-mapping (cgen/list V X Y ts ss)] (let* ([arg-mapping (cgen/list V X Y ss ts)]
;; just add dbound as something that can be constrained ;; just add dbound* as something that can be constrained
[darg-mapping [darg-mapping
(extend-tvars (list dbound) (extend-tvars (list dbound)
(% move-dotted-rest-to-dmap (cgen V (cons dbound* X) Y t-dty s-dty) dbound* dbound))]) (% move-dotted-rest-to-dmap (cgen V (cons dbound* X) Y s-dty t-dty) dbound* dbound))])
(% cset-meet arg-mapping darg-mapping))] (% cset-meet arg-mapping darg-mapping))]
;; * <: ... ;; * <: ...
[((seq ss (uniform-end s-rest)) [((seq ss (uniform-end s-rest))
(seq ts (dotted-end t-dty dbound))) (seq ts (dotted-end t-dty dbound)))
#:return-unless (memq dbound Y) #:return-unless (memq dbound Y)
#f #f
(if (<= (length ss) (length ts)) (cond
;; the simple case [(= (length ts) (length ss))
(let* ([arg-mapping (cgen/list V X Y ts (extend ts ss s-rest))] ;; the simple case
[darg-mapping (% move-rest-to-dmap (let* ([arg-mapping (cgen/list V X Y ss ts)]
(cgen V (cons dbound X) Y t-dty s-rest) dbound)]) [darg-mapping (% move-rest-to-dmap
(% cset-meet arg-mapping darg-mapping)) (cgen V (cons dbound X) Y s-rest t-dty) dbound #:exact #t)])
;; the hard case (% cset-meet arg-mapping darg-mapping))]
(let* ([vars (var-store-take dbound t-dty (- (length ss) (length ts)))] [(< (length ts) (length ss))
[new-tys (for/list ([var (in-list vars)]) ;; the hard case
(substitute (make-F var) dbound t-dty))] (let* ([vars (var-store-take dbound t-dty (- (length ss) (length ts)))]
[new-t-seq (seq (append ts new-tys) (dotted-end t-dty dbound))] [new-tys (for/list ([var (in-list vars)])
[new-cset (cgen/seq V (append vars X) Y s-seq new-t-seq)]) (substitute (make-F var) dbound t-dty))]
(% move-vars+rest-to-dmap new-cset dbound vars)))] [new-t-seq (seq (append ts new-tys) (dotted-end t-dty dbound))]
[new-cset (cgen/seq V (append vars X) Y s-seq new-t-seq)])
(% move-vars+rest-to-dmap new-cset dbound vars #:exact #t))]
[else #f])]
;; If dotted <: starred is correct, add it below. Not sure it is. ;; If dotted <: starred is correct, add it below. Not sure it is.
[((seq ss (dotted-end s-dty dbound)) [((seq ss (dotted-end s-dty dbound))
(seq ts (uniform-end t-rest))) (seq ts (uniform-end t-rest)))
@ -317,14 +320,13 @@
(substitute (make-F var) dbound s-dty))] (substitute (make-F var) dbound s-dty))]
[new-s-seq (make-arr (append ss new-tys) (dotted-end s-dty dbound))] [new-s-seq (make-arr (append ss new-tys) (dotted-end s-dty dbound))]
[new-cset (cgen/seq V (append vars X) Y new-s-seq t-seq)]) [new-cset (cgen/seq V (append vars X) Y new-s-seq t-seq)])
(% move-vars+rest-to-dmap new-cset dbound vars #:exact #t))] (% move-vars+rest-to-dmap new-cset dbound vars))]
[(= (length ss) (length ts)) [else
;; the simple case ;; the simple case
(let* ([arg-mapping (cgen/list V X Y (extend ss ts t-rest) ss)] (let* ([arg-mapping (cgen/list V X Y ss (extend ss ts t-rest))]
[rest-mapping (cgen V (cons dbound X) Y t-rest s-dty)] [darg-mapping (% move-rest-to-dmap
[darg-mapping (% move-rest-to-dmap rest-mapping dbound #:exact #t)]) (cgen V (cons dbound X) Y t-rest s-dty) dbound)])
(% cset-meet arg-mapping darg-mapping))] (% cset-meet arg-mapping darg-mapping))])]))
[else #f])]))
(define/cond-contract (cgen/arr V X Y s-arr t-arr) (define/cond-contract (cgen/arr V X Y s-arr t-arr)
@ -344,7 +346,7 @@
(null? t-kws) (null? t-kws)
(% cset-meet (% cset-meet
(cgen V X Y s t) (cgen V X Y s t)
(cgen/seq V X Y s-seq t-seq)))])) (cgen/seq V X Y t-seq s-seq)))]))
(define/cond-contract (cgen/flds V X Y flds-s flds-t) (define/cond-contract (cgen/flds V X Y flds-s flds-t)
((listof symbol?) (listof symbol?) (listof symbol?) (listof fld?) (listof fld?) ((listof symbol?) (listof symbol?) (listof symbol?) (listof fld?) (listof fld?)