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

Add cgen/inv and use it.

Browse Source 
original commit: 03373d11891800aad6bae04f8ccc3fdcb6703b88
This commit is contained in:
Eric Dobson 2014-04-29 23:30:43 -07:00
parent 5609e972b2
commit 9a392d8c09
1 changed files with 19 additions and 14 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -176,10 +176,8 @@
[(e e) (empty-cset X Y)]
[(e (Top:)) (empty-cset X Y)]
;; FIXME - is there something to be said about the logical ones?
[((TypeFilter: s p i) (TypeFilter: t p i))
(% cset-meet (cgen V X Y s t) (cgen V X Y t s))]
[((NotTypeFilter: s p i) (NotTypeFilter: t p i))
(% cset-meet (cgen V X Y s t) (cgen V X Y t s))]
[((TypeFilter: s p i) (TypeFilter: t p i)) (cgen/inv V X Y s t)]
[((NotTypeFilter: s p i) (NotTypeFilter: t p i)) (cgen/inv V X Y s t)]
[(_ _) #f]))
;; s and t must be *latent* filter sets
@ -337,10 +335,14 @@
(for/list/fail ([s (in-list flds-s)] [t (in-list flds-t)])
(match* (s t)
;; mutable - invariant
[((fld: s _ #t) (fld: t _ #t)) (cset-meet (cgen V X Y s t) (cgen V X Y t s))]
[((fld: s _ #t) (fld: t _ #t)) (cgen/inv V X Y s t)]
;; immutable - covariant
[((fld: s _ #f) (fld: t _ #f)) (cgen V X Y s t)]))))
(define (cgen/inv V X Y s t)
(% cset-meet (cgen V X Y s t) (cgen V X Y t s)))
;; V : a set of variables not to mention in the constraints
;; X : the set of type variables to be constrained
;; Y : the set of index variables to be constrained
@ -357,6 +359,9 @@
(define/cond-contract (cg S T)
(Type/c Type/c . -> . (or/c #f cset?))
(cgen V X Y S T))
(define/cond-contract (cg/inv S T)
(Type/c Type/c . -> . cset?)
(cgen/inv V X Y S T))
;; this places no constraints on any variables in X
(define empty (empty-cset X Y))
;; this constrains just x (which is a single var)
@ -638,24 +643,24 @@
;; Invariant here because struct types aren't subtypes just because the
;; structs are (since you can make a constructor from the type).
[((StructType: s) (StructType: t))
(% cset-meet (cg s t) (cg t s))]
(cg/inv s t)]
;; vectors are invariant - generate constraints *both* ways
[((Vector: e) (Vector: e*))
(% cset-meet (cg e e*) (cg e* e))]
(cg/inv e e*)]
;; boxes are invariant - generate constraints *both* ways
[((Box: e) (Box: e*))
(% cset-meet (cg e e*) (cg e* e))]
(cg/inv e e*)]
[((MPair: s t) (MPair: s* t*))
(% cset-meet (cg s s*) (cg s* s) (cg t t*) (cg t* t))]
(% cset-meet (cg/inv s s*) (cg/inv t t*))]
[((Channel: e) (Channel: e*))
(% cset-meet (cg e e*) (cg e* e))]
(cg/inv e e*)]
[((ThreadCell: e) (ThreadCell: e*))
(% cset-meet (cg e e*) (cg e* e))]
(cg/inv e e*)]
[((Continuation-Mark-Keyof: e) (Continuation-Mark-Keyof: e*))
(% cset-meet (cg e e*) (cg e* e))]
(cg/inv e e*)]
[((Prompt-Tagof: s t) (Prompt-Tagof: s* t*))
(% cset-meet (cg s s*) (cg s* s) (cg t t*) (cg t* t))]
(% cset-meet (cg/inv s s*) (cg/inv t t*))]
[((Promise: e) (Promise: e*))
(cg e e*)]
[((Ephemeron: e) (Ephemeron: e*))
@ -690,7 +695,7 @@
;; we assume all HTs are mutable at the moment
[((Hashtable: s1 s2) (Hashtable: t1 t2))
;; for mutable hash tables, both are invariant
(% cset-meet (cg t1 s1) (cg s1 t1) (cg t2 s2) (cg s2 t2))]
(% cset-meet (cg/inv s1 t1) (cg/inv s2 t2))]
;; syntax is covariant
[((Syntax: s1) (Syntax: s2))
(cg s1 s2)]