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

Fix infer dotted cases when there are constraints on the dbound.

Browse Source 
Closes PR 14593.

original commit: 2f7cb68aeac2de4a463ea58945e2826848ef9f54
This commit is contained in:
Eric Dobson 2014-06-22 23:26:36 -07:00
parent fe296a8c4d
commit 0a46a27893
2 changed files with 48 additions and 14 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -82,13 +82,15 @@
(define (mover cset dbound vars f)
(map/cset
(lambda (cmap dmap)
(when (hash-has-key? (dmap-map dmap) dbound)
(int-err "Tried to move vars to dbound that already exists"))
(% cons
(hash-remove* cmap (cons dbound vars))
(dmap-meet
(singleton-dmap
dbound
(f cmap))
(make-dmap (hash-remove (dmap-map dmap) dbound)))))
dmap)))
cset))
;; dbound : index variable
@ -237,7 +239,10 @@
#:return-unless (<= (length ss) (length ts))
#f
(define-values (vars new-tys) (generate-dbound-prefix dbound dty (- (length ts) (length ss)) #f))
(% move-vars-to-dmap (cgen/list V (append vars X) Y (append ss new-tys) ts) dbound vars)]
(define-values (ts-front ts-back) (split-at ts (length ss)))
(% cset-meet
(cgen/list V X Y ss ts-front)
(% move-vars-to-dmap (cgen/list V (append vars X) Y new-tys ts-back) dbound vars))]
;; dotted above, nothing below
[((seq ss (null-end))
(seq ts (dotted-end dty dbound)))
@ -246,7 +251,10 @@
#:return-unless (<= (length ts) (length ss))
#f
(define-values (vars new-tys) (generate-dbound-prefix dbound dty (- (length ss) (length ts)) #f))
(% move-vars-to-dmap (cgen/list V (append vars X) Y ss (append ts new-tys)) dbound vars)]
(define-values (ss-front ss-back) (split-at ss (length ts)))
(% cset-meet
(cgen/list V X Y ss-front ts)
(% move-vars-to-dmap (cgen/list V (append vars X) Y ss-back new-tys) dbound vars))]
;; same dotted bound
[((seq ss (dotted-end s-dty dbound))
@ -287,24 +295,33 @@
(define new-bound (gensym dbound))
(define-values (vars new-tys) (generate-dbound-prefix dbound t-dty (- (length ss) (length ts))
new-bound))
(% move-vars+rest-to-dmap
(% cset-meet
(cgen/list (cons new-bound V) (append vars X) (cons new-bound Y) ss (append ts new-tys))
(cgen V (cons dbound X) Y s-rest t-dty))
vars dbound #:exact #t)]
(define-values (ss-front ss-back) (split-at ss (length ts)))
(% cset-meet
(cgen/list V X Y ss-front ts)
(% move-vars+rest-to-dmap
(% cset-meet
(cgen/list (cons new-bound V) (append vars X) (cons new-bound Y) ss-back new-tys)
(cgen V (cons dbound X) Y s-rest t-dty))
vars dbound #:exact #t))]
[((seq ss (dotted-end s-dty dbound))
(seq ts (uniform-end t-rest)))
(cond
[(memq dbound Y)
(define new-bound (gensym dbound))
(define length-delta (- (length ts) (length ss)))
(define-values (vars new-tys)
(generate-dbound-prefix dbound s-dty (max 0 (- (length ts) (length ss))) new-bound))
(% move-vars+rest-to-dmap
(% cset-meet
(cgen/list (cons new-bound V) (append vars X) (cons new-bound Y) (append ss new-tys) (extend ss ts t-rest))
(cgen V (cons dbound X) Y s-dty t-rest))
vars dbound)]
(generate-dbound-prefix dbound s-dty (max 0 length-delta) new-bound))
(% cset-meet
(cgen/list V X Y ss (if (positive? length-delta)
(drop-right ts length-delta)
(extend ss ts t-rest)))
(% move-vars+rest-to-dmap
(% cset-meet
(cgen/list (cons new-bound V) (append vars X) (cons new-bound Y)
new-tys (take-right ts (max 0 length-delta)))
(cgen V (cons dbound X) Y s-dty t-rest))
vars dbound))]
[else
(extend-tvars (list dbound)
(cgen/seq (cons dbound V) X Y (seq ss (uniform-end s-dty)) t-seq))])]))

17
pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/unit-tests/infer-tests.rkt
View File

@ -228,6 +228,23 @@
[infer-t (-> (-values (list -Bottom))) (-> (-values (list (-v b) (-v b)))) #:vars '(a)]
[infer-t (-> (-values (list (-v a)))) (-> (-values (list (-v b) (-v b)))) #:vars '(a)]
[infer-t
(-pair (->... (list) ((-v b) b) Univ) (make-ListDots (-lst (-v b)) 'b))
(-lst* (-> Univ Univ))
#:indices '(b) #:fail]
[infer-t
(-lst* (-> Univ Univ))
(-pair (->... (list) ((-v b) b) Univ) (make-ListDots (-lst (-v b)) 'b))
#:indices '(b) #:fail]
[infer-t
(-pair (->... (list) ((-v b) b) Univ) (make-ListDots (-v b) 'b))
(-pair (-> -Symbol Univ) (-lst -String))
#:indices '(b) #:fail]
[infer-t
(-pair (-> -Symbol Univ) (-lst -String))
(-pair (->... (list) ((-v b) b) Univ) (make-ListDots (-v b) 'b))
#:indices '(b) #:fail]
;; Currently Broken
;(infer-t (make-ListDots -Symbol 'b) (-pair -Symbol (-lst -Symbol)) #:indices '(b))
[i2-t (-v a) N ('a N)]