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

Make cset-meet take more than two arguments.

Browse Source
This commit is contained in:
Eric Dobson 2014-04-29 22:57:43 -07:00
parent bf9cdfb3f1
commit c7645170e3
3 changed files with 42 additions and 45 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

19
pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/infer/constraints.rkt
View File

@ -63,7 +63,11 @@
;; compute the meet of two constraint sets ;; compute the meet of two constraint sets
;; returns #f for failure ;; returns #f for failure
(define (cset-meet x y) (define cset-meet
(case-lambda
[() (empty-cset null null)]
[(x) x]
[(x y)
(match* (x y) (match* (x y)
[((struct cset (maps1)) (struct cset (maps2))) [((struct cset (maps1)) (struct cset (maps2)))
(define maps (for*/list ([(map1 dmap1) (in-pairs (remove-duplicates maps1))] (define maps (for*/list ([(map1 dmap1) (in-pairs (remove-duplicates maps1))]
@ -75,18 +79,15 @@
v)) v))
(cond [(null? maps) (cond [(null? maps)
#f] #f]
[else (make-cset maps)])] [else (make-cset maps)])])]
[(_ _) (int-err "Got non-cset: ~a ~a" x y)])) [(x . ys)
(for/fold ([x x]) ([y (in-list ys)])
(% cset-meet x y))]))
;; combines a list of csets using cset-meet individually ;; combines a list of csets using cset-meet individually
;; returns #f for failure ;; returns #f for failure
(define (cset-meet* args) (define (cset-meet* args)
(for/fold ([c (make-cset (list (cons (apply cset-meet args))
(make-immutable-hash null)
(make-dmap (make-immutable-hash null)))))])
([a (in-list args)]
#:break (not c))
(cset-meet a c)))
;; produces a cset of all of the maps in all of the given csets ;; produces a cset of all of the maps in all of the given csets
;; FIXME: should this call `remove-duplicates`? ;; FIXME: should this call `remove-duplicates`?

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

@ -206,11 +206,11 @@
;; the simplest case - no rests, drests, keywords ;; the simplest case - no rests, drests, keywords
[((arr: ss s #f #f '()) [((arr: ss s #f #f '())
(arr: ts t #f #f '())) (arr: ts t #f #f '()))
(% cset-meet* (% list (% cset-meet
;; contravariant ;; contravariant
(cgen/list V X Y ts ss) (cgen/list V X Y ts ss)
;; covariant ;; covariant
(cg s t)))] (cg s t))]
;; just a rest arg, no drest, no keywords ;; just a rest arg, no drest, no keywords
[((arr: ss s s-rest #f '()) [((arr: ss s s-rest #f '())
(arr: ts t t-rest #f '())) (arr: ts t t-rest #f '()))
@ -227,7 +227,7 @@
;; no rest arg on the left, or wrong number = fail ;; no rest arg on the left, or wrong number = fail
[else #f])] [else #f])]
[ret-mapping (cg s t)]) [ret-mapping (cg s t)])
(% cset-meet* (% list arg-mapping ret-mapping)))] (% cset-meet arg-mapping ret-mapping))]
;; dotted on the left, nothing on the right ;; dotted on the left, nothing on the right
[((arr: ss s #f (cons dty dbound) '()) [((arr: ss s #f (cons dty dbound) '())
(arr: ts t #f #f '())) (arr: ts t #f #f '()))
@ -265,8 +265,7 @@
(let* ([arg-mapping (cgen/list V X Y ts ss)] (let* ([arg-mapping (cgen/list V X Y ts ss)]
[darg-mapping (cgen V X Y t-dty s-dty)] [darg-mapping (cgen V X Y t-dty s-dty)]
[ret-mapping (cg s t)]) [ret-mapping (cg s t)])
(% cset-meet* (% cset-meet arg-mapping darg-mapping ret-mapping))]
(% list arg-mapping darg-mapping ret-mapping)))]
;; bounds are different ;; bounds are different
[((arr: ss s #f (cons s-dty (? (λ (db) (memq db Y)) dbound)) '()) [((arr: ss s #f (cons s-dty (? (λ (db) (memq db Y)) dbound)) '())
(arr: ts t #f (cons t-dty dbound*) '())) (arr: ts t #f (cons t-dty dbound*) '()))
@ -276,8 +275,7 @@
;; just add dbound as something that can be constrained ;; 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)] [darg-mapping (% move-dotted-rest-to-dmap (cgen V (cons dbound X) Y t-dty s-dty) dbound)]
[ret-mapping (cg s t)]) [ret-mapping (cg s t)])
(% cset-meet* (% cset-meet arg-mapping darg-mapping ret-mapping))]
(% list arg-mapping darg-mapping ret-mapping)))]
[((arr: ss s #f (cons s-dty dbound) '()) [((arr: ss s #f (cons s-dty dbound) '())
(arr: ts t #f (cons t-dty (? (λ (db) (memq db Y)) dbound*)) '())) (arr: ts t #f (cons t-dty (? (λ (db) (memq db Y)) dbound*)) '()))
#:return-unless (= (length ss) (length ts)) #f #:return-unless (= (length ss) (length ts)) #f
@ -286,8 +284,7 @@
[darg-mapping (% move-dotted-rest-to-dmap [darg-mapping (% move-dotted-rest-to-dmap
(cgen V (cons dbound* X) Y t-dty s-dty) dbound*)] (cgen V (cons dbound* X) Y t-dty s-dty) dbound*)]
[ret-mapping (cg s t)]) [ret-mapping (cg s t)])
(% cset-meet* (% cset-meet arg-mapping darg-mapping ret-mapping))]
(% list arg-mapping darg-mapping ret-mapping)))]
;; * <: ... ;; * <: ...
[((arr: ss s s-rest #f '()) [((arr: ss s s-rest #f '())
(arr: ts t #f (cons t-dty dbound) '())) (arr: ts t #f (cons t-dty dbound) '()))
@ -299,7 +296,7 @@
[darg-mapping (% move-rest-to-dmap [darg-mapping (% move-rest-to-dmap
(cgen V (cons dbound X) Y t-dty s-rest) dbound)] (cgen V (cons dbound X) Y t-dty s-rest) dbound)]
[ret-mapping (cg s t)]) [ret-mapping (cg s t)])
(% cset-meet* (% list arg-mapping darg-mapping ret-mapping))) (% cset-meet arg-mapping darg-mapping ret-mapping))
;; the hard case ;; the hard case
(let* ([vars (var-store-take dbound t-dty (- (length ss) (length ts)))] (let* ([vars (var-store-take dbound t-dty (- (length ss) (length ts)))]
[new-tys (for/list ([var (in-list vars)]) [new-tys (for/list ([var (in-list vars)])
@ -329,7 +326,7 @@
(move-rest-to-dmap (move-rest-to-dmap
rest-mapping dbound #:exact #t))] rest-mapping dbound #:exact #t))]
[ret-mapping (cg s t)]) [ret-mapping (cg s t)])
(% cset-meet* (% list arg-mapping darg-mapping ret-mapping)))] (% cset-meet arg-mapping darg-mapping ret-mapping))]
[else #f])] [else #f])]
[(_ _) #f])) [(_ _) #f]))
@ -387,10 +384,9 @@
;; check each element ;; check each element
[((Result: s f-s o-s) [((Result: s f-s o-s)
(Result: t f-t o-t)) (Result: t f-t o-t))
(% cset-meet* (% list (% cset-meet (cg s t)
(cg s t)
(cgen/filter-set V X Y f-s f-t) (cgen/filter-set V X Y f-s f-t)
(cgen/object V X Y o-s o-t)))] (cgen/object V X Y o-s o-t))]
;; values are covariant ;; values are covariant
[((Values: ss) (Values: ts)) [((Values: ss) (Values: ts))
@ -531,7 +527,7 @@
;; To check that mutable pair is a sequence we check that the cdr is ;; To check that mutable pair is a sequence we check that the cdr is
;; both an mutable list and a sequence ;; both an mutable list and a sequence
[((MPair: t1 t2) (Sequence: (list t*))) [((MPair: t1 t2) (Sequence: (list t*)))
(% cset-meet* (% list (cg t1 t*) (cg t2 T) (cg t2 (Un (-val null) (make-MPairTop)))))] (% cset-meet (cg t1 t*) (cg t2 T) (cg t2 (Un (-val null) (make-MPairTop))))]
[((List: ts) (Sequence: (list t*))) [((List: ts) (Sequence: (list t*)))
(% cset-meet* (for/list/fail ([t (in-list ts)]) (% cset-meet* (for/list/fail ([t (in-list ts)])
(cg t t*)))] (cg t t*)))]
@ -651,7 +647,7 @@
[((Box: e) (Box: e*)) [((Box: e) (Box: e*))
(% cset-meet (cg e e*) (cg e* e))] (% cset-meet (cg e e*) (cg e* e))]
[((MPair: s t) (MPair: s* t*)) [((MPair: s t) (MPair: s* t*))
(% cset-meet* (% list (cg s s*) (cg s* s) (cg t t*) (cg t* t)))] (% cset-meet (cg s s*) (cg s* s) (cg t t*) (cg t* t))]
[((Channel: e) (Channel: e*)) [((Channel: e) (Channel: e*))
(% cset-meet (cg e e*) (cg e* e))] (% cset-meet (cg e e*) (cg e* e))]
[((ThreadCell: e) (ThreadCell: e*)) [((ThreadCell: e) (ThreadCell: e*))
@ -659,7 +655,7 @@
[((Continuation-Mark-Keyof: e) (Continuation-Mark-Keyof: e*)) [((Continuation-Mark-Keyof: e) (Continuation-Mark-Keyof: e*))
(% cset-meet (cg e e*) (cg e* e))] (% cset-meet (cg e e*) (cg e* e))]
[((Prompt-Tagof: s t) (Prompt-Tagof: s* t*)) [((Prompt-Tagof: s t) (Prompt-Tagof: s* t*))
(% cset-meet* (% list (cg s s*) (cg s* s) (cg t t*) (cg t* t)))] (% cset-meet (cg s s*) (cg s* s) (cg t t*) (cg t* t))]
[((Promise: e) (Promise: e*)) [((Promise: e) (Promise: e*))
(cg e e*)] (cg e e*)]
[((Ephemeron: e) (Ephemeron: e*)) [((Ephemeron: e) (Ephemeron: e*))
@ -694,7 +690,7 @@
;; we assume all HTs are mutable at the moment ;; we assume all HTs are mutable at the moment
[((Hashtable: s1 s2) (Hashtable: t1 t2)) [((Hashtable: s1 s2) (Hashtable: t1 t2))
;; for mutable hash tables, both are invariant ;; for mutable hash tables, both are invariant
(% cset-meet* (% list (cg t1 s1) (cg s1 t1) (cg t2 s2) (cg s2 t2)))] (% cset-meet (cg t1 s1) (cg s1 t1) (cg t2 s2) (cg s2 t2))]
;; syntax is covariant ;; syntax is covariant
[((Syntax: s1) (Syntax: s2)) [((Syntax: s1) (Syntax: s2))
(cg s1 s2)] (cg s1 s2)]

2
pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/infer/signatures.rkt
View File

@ -14,7 +14,7 @@
[cond-contracted var-demote (Type/c (listof symbol?) . -> . Type/c)])) [cond-contracted var-demote (Type/c (listof symbol?) . -> . Type/c)]))
(define-signature constraints^ (define-signature constraints^
([cond-contracted cset-meet (cset? cset? . -> . (or/c #f cset?))] ([cond-contracted cset-meet ((cset? cset?) #:rest (listof cset?) . ->* . (or/c #f cset?))]
[cond-contracted cset-meet* ((listof cset?) . -> . (or/c #f cset?))] [cond-contracted cset-meet* ((listof cset?) . -> . (or/c #f cset?))]
no-constraint no-constraint
[cond-contracted empty-cset ((listof symbol?) (listof symbol?) . -> . cset?)] [cond-contracted empty-cset ((listof symbol?) (listof symbol?) . -> . cset?)]