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

Correctly extend tvars in the right place during inference.

Browse Source 
Removes wrong extension of tvars in apply as well.

original commit: 1d43b583fb04140f55c290fee98db28467d96c98
This commit is contained in:
Eric Dobson 2014-05-09 22:03:35 -07:00
parent d3ea8b43e2
commit 0b626757bb
2 changed files with 18 additions and 20 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -272,7 +272,9 @@
#:return-when (memq dbound* Y) #f
(let* ([arg-mapping (cgen/list V X Y ts ss)]
;; just add dbound as something that can be constrained
[darg-mapping (% move-dotted-rest-to-dmap (cgen V (cons dbound X) Y t-dty s-dty) dbound dbound*)]
[darg-mapping
(extend-tvars (list dbound*)
(% move-dotted-rest-to-dmap (cgen V (cons dbound X) Y t-dty s-dty) dbound dbound*))]
[ret-mapping (cg s t)])
(% cset-meet arg-mapping darg-mapping ret-mapping))]
[((arr: ss s #f (cons s-dty dbound) '())
@ -280,7 +282,9 @@
#:return-unless (= (length ss) (length ts)) #f
(let* ([arg-mapping (cgen/list V X Y ts ss)]
;; just add dbound as something that can be constrained
[darg-mapping (% move-dotted-rest-to-dmap (cgen V (cons dbound* X) Y t-dty s-dty) dbound* dbound)]
[darg-mapping
(extend-tvars (list dbound)
(% move-dotted-rest-to-dmap (cgen V (cons dbound* X) Y t-dty s-dty) dbound* dbound))]
[ret-mapping (cg s t)])
(% cset-meet arg-mapping darg-mapping ret-mapping))]
;; * <: ...
@ -438,13 +442,15 @@
#:return-when (memq t-dbound Y) #f
(% cset-meet
(cgen/list V X Y ss ts)
(% move-dotted-rest-to-dmap (cgen V (cons s-dbound X) Y s-dty t-dty) s-dbound t-dbound))]
(extend-tvars (list t-dbound)
(% move-dotted-rest-to-dmap (cgen V (cons s-dbound X) Y s-dty t-dty) s-dbound t-dbound)))]
[((ValuesDots: ss s-dty s-dbound)
(ValuesDots: ts t-dty (? (λ (db) (memq db Y)) t-dbound)))
;; s-dbound can't be in Y, due to previous rule
(% cset-meet
(cgen/list V X Y ss ts)
(% move-dotted-rest-to-dmap (cgen V (cons t-dbound X) Y s-dty t-dty) t-dbound s-dbound))]
(extend-tvars (list s-dbound)
(% move-dotted-rest-to-dmap (cgen V (cons t-dbound X) Y s-dty t-dty) t-dbound s-dbound)))]
;; they're subtypes. easy.
[(a b)
@ -585,10 +591,12 @@
[((ListDots: s-dty (? (λ (db) (memq db Y)) s-dbound)) (ListDots: t-dty t-dbound))
;; What should we do if both are in Y?
#:return-when (memq t-dbound Y) #f
(% move-dotted-rest-to-dmap (cgen V (cons s-dbound X) Y s-dty t-dty) s-dbound t-dbound)]
(extend-tvars (list t-dbound)
(% move-dotted-rest-to-dmap (cgen V (cons s-dbound X) Y s-dty t-dty) s-dbound t-dbound))]
[((ListDots: s-dty s-dbound) (ListDots: t-dty (? (λ (db) (memq db Y)) t-dbound)))
;; s-dbound can't be in Y, due to previous rule
(% move-dotted-rest-to-dmap (cgen V (cons t-dbound X) Y s-dty t-dty) t-dbound s-dbound)]
(extend-tvars (list s-dbound)
(% move-dotted-rest-to-dmap (cgen V (cons t-dbound X) Y s-dty t-dty) t-dbound s-dbound))]
;; this constrains `dbound' to be |ts| - |ss|
[((ListDots: s-dty dbound) (List: ts))

18
pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-apply.rkt
View File

@ -98,20 +98,10 @@
;; ... function, ... arg
[(and drest tail-bound
(= (length domain) (length arg-tys))
(if (eq? tail-bound (cdr drest))
;; same bound on the ...s
(infer fixed-vars (list dotted-var)
(cons (make-ListDots tail-ty tail-bound) arg-tys)
(cons (make-ListDots (car drest) (cdr drest)) domain)
range)
;; different bounds on the ...s
(extend-tvars (list tail-bound (cdr drest))
(extend-indexes (cdr drest)
;; don't need to add tail-bound - it must already be an index
(infer fixed-vars (list dotted-var)
(cons (make-ListDots tail-ty tail-bound) arg-tys)
(cons (make-ListDots (car drest) (cdr drest)) domain)
range)))))
(infer fixed-vars (list dotted-var)
(cons (make-ListDots tail-ty tail-bound) arg-tys)
(cons (make-ListDots (car drest) (cdr drest)) domain)
range))
=> finish]
;; ... function, (Listof A) or (List A B C etc) arg
[(and drest (not tail-bound)