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

Inference for passing ListDots as Listof.

Browse Source 
original commit: a2af89bafd3d79587c87425488833e07465f5fc5
This commit is contained in:
Sam Tobin-Hochstadt 2010-05-28 12:08:44 -04:00
parent 92c48f6521
commit db8c693481
2 changed files with 11 additions and 4 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

3
collects/tests/typed-scheme/succeed/list-dots.rkt
View File

@ -16,3 +16,6 @@
(: h3 (All (a ...) ((Pair String a) ... -> (Listof Any))))
(define (h3 . x) x)
(: h4 (All (a ...) (a ... -> Number)))
(define (h4 . x) (length x))

12
collects/typed-scheme/infer/infer-unit.rkt
View File

@ -250,7 +250,7 @@
(cset-meet* (list arg-mapping darg-mapping ret-mapping)))])]
[(_ _) (fail! S T)]))
;; determine constraints on the variables in X that would make T a supertype of S
;; determine constraints on the variables in X that would make S a subtype of T
;; the resulting constraints will not mention V
(define (cgen V X S T)
(define (cg S T) (cgen V X S T))
@ -364,6 +364,13 @@
(cg t t*)]
[((Hashtable: k v) (Sequence: (list k* v*)))
(cgen/list V X (list k v) (list k* v*))]
;; must be above mu unfolding
[((ListDots: s-dty dbound) (Listof: t-elem))
(when (memq dbound X) (fail! S T))
(cgen V X (substitute Univ dbound s-dty) t-elem)]
[((ListDots: s-dty dbound) (ListDots: t-dty dbound))
(when (memq dbound X) (fail! S T))
(cgen V X s-dty t-dty)]
;; if we have two mu's, we rename them to have the same variable
;; and then compare the bodies
[((Mu-unsafe: s) (Mu-unsafe: t))
@ -410,9 +417,6 @@
[((ValuesDots: ss s-dty dbound) (ValuesDots: ts t-dty dbound))
(when (memq dbound X) (fail! ss ts))
(cgen/list V X (cons s-dty ss) (cons t-dty ts))]
[((ListDots: s-dty dbound) (ListDots: t-dty dbound))
(when (memq dbound X) (fail! S T))
(cgen V X s-dty t-dty)]
[((Vector: e) (Vector: e*))
(cset-meet (cg e e*) (cg e* e))]
[((Box: e) (Box: e*))