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

Handle top-arr in infer. Add convenience binding for function top.

Browse Source 
svn: r12745
This commit is contained in:
Sam Tobin-Hochstadt 2008-12-08 18:24:33 +00:00
parent 8c4789a627
commit ea0873adb2
4 changed files with 158 additions and 153 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

301
collects/typed-scheme/infer/infer-unit.ss
View File

@ -251,154 +251,157 @@
(parameterize ([match-equality-test type-equal?] (parameterize ([match-equality-test type-equal?]
[current-seen (remember S T (current-seen))]) [current-seen (remember S T (current-seen))])
(match* (match*
(S T) (S T)
[(a a) empty] [(a a) empty]
[(_ (Univ:)) empty] [(_ (Univ:)) empty]
[((F: (? (lambda (e) (memq e X)) v)) S) [((F: (? (lambda (e) (memq e X)) v)) S)
(when (match S (when (match S
[(F: v*) [(F: v*)
(just-Dotted? (lookup (current-tvars) v* (lambda _ #f)))] (just-Dotted? (lookup (current-tvars) v* (lambda _ #f)))]
[_ #f]) [_ #f])
(fail! S T)) (fail! S T))
(singleton (Un) v (var-demote S V))] (singleton (Un) v (var-demote S V))]
[(S (F: (? (lambda (e) (memq e X)) v))) [(S (F: (? (lambda (e) (memq e X)) v)))
(when (match S (when (match S
[(F: v*) [(F: v*)
(just-Dotted? (lookup (current-tvars) v* (lambda _ #f)))] (just-Dotted? (lookup (current-tvars) v* (lambda _ #f)))]
[_ #f]) [_ #f])
(fail! S T)) (fail! S T))
(singleton (var-promote S V) v Univ)] (singleton (var-promote S V) v Univ)]
;; two unions with the same number of elements, so we just try to unify them pairwise ;; two unions with the same number of elements, so we just try to unify them pairwise
#;[((Union: l1) (Union: l2)) #;[((Union: l1) (Union: l2))
(=> unmatch) (=> unmatch)
(unless (= (length l1) (length l2)) (unless (= (length l1) (length l2))
(unmatch)) (unmatch))
(cgen-union V X l1 l2)] (cgen-union V X l1 l2)]
#;[((Poly: v1 b1) (Poly: v2 b2)) #;[((Poly: v1 b1) (Poly: v2 b2))
(unless (= (length v1) (length v2)) (unless (= (length v1) (length v2))
(fail! S T)) (fail! S T))
(let ([b2* (subst-all (map list v2 v1) b2)]) (let ([b2* (subst-all (map list v2 v1) b2)])
(cg b1 b2*))] (cg b1 b2*))]
#;[((PolyDots: (list v1 ... r1) b1) (PolyDots: (list v2 ... r2) b2)) #;[((PolyDots: (list v1 ... r1) b1) (PolyDots: (list v2 ... r2) b2))
(unless (= (length v1) (length v2)) (unless (= (length v1) (length v2))
(fail! S T)) (fail! S T))
(let ([b2* (substitute-dotted v1 v1 v2 (subst-all (map list v2 v1) b2))]) (let ([b2* (substitute-dotted v1 v1 v2 (subst-all (map list v2 v1) b2))])
(cg b1 b2*))] (cg b1 b2*))]
[((Poly: v1 b1) T) [((Poly: v1 b1) T)
(cgen (append v1 V) X b1 T)] (cgen (append v1 V) X b1 T)]
#;[((PolyDots: (list v1 ... r1) b1) T) #;[((PolyDots: (list v1 ... r1) b1) T)
(let ([b1* (var-demote b1 (cons r1 v1))]) (let ([b1* (var-demote b1 (cons r1 v1))])
(cg b1* T))] (cg b1* T))]
#; #;
[((Poly-unsafe: n b) (Poly-unsafe: n* b*)) [((Poly-unsafe: n b) (Poly-unsafe: n* b*))
(unless (= n n*) (unless (= n n*)
(fail! S T)) (fail! S T))
(cg b b*)] (cg b b*)]
[((Union: es) S) (cset-meet* (cons empty (for/list ([e es]) (cg e S))))] [((Union: es) S) (cset-meet* (cons empty (for/list ([e es]) (cg e S))))]
;; we might want to use multiple csets here, but I don't think it makes a difference ;; we might want to use multiple csets here, but I don't think it makes a difference
[(S (Union: es)) (or [(S (Union: es)) (or
(for/or (for/or
([e es]) ([e es])
(with-handlers (with-handlers
([exn:infer? (lambda _ #f)]) ([exn:infer? (lambda _ #f)])
(cg S e))) (cg S e)))
(fail! S T))] (fail! S T))]
[((Struct: nm p flds proc _ _ _) (Struct: nm p flds* proc* _ _ _)) [((Struct: nm p flds proc _ _ _) (Struct: nm p flds* proc* _ _ _))
(let-values ([(flds flds*) (let-values ([(flds flds*)
(cond [(and proc proc*) (cond [(and proc proc*)
(values (cons proc flds) (cons proc* flds*))] (values (cons proc flds) (cons proc* flds*))]
[(or proc proc*) [(or proc proc*)
(fail! S T)] (fail! S T)]
[else (values flds flds*)])]) [else (values flds flds*)])])
(cgen/list V X flds flds*))] (cgen/list V X flds flds*))]
[((Name: n) (Name: n*)) [((Name: n) (Name: n*))
(if (free-identifier=? n n*) (if (free-identifier=? n n*)
null null
(fail! S T))] (fail! S T))]
[((Pair: a b) (Pair: a* b*)) [((Pair: a b) (Pair: a* b*))
(cset-meet (cg a a*) (cg b b*))] (cset-meet (cg a a*) (cg b b*))]
;; if we have two mu's, we rename them to have the same variable ;; if we have two mu's, we rename them to have the same variable
;; and then compare the bodies ;; and then compare the bodies
[((Mu-unsafe: s) (Mu-unsafe: t)) [((Mu-unsafe: s) (Mu-unsafe: t))
(cg s t)] (cg s t)]
;; other mu's just get unfolded ;; other mu's just get unfolded
[(s (? Mu? t)) (cg s (unfold t))] [(s (? Mu? t)) (cg s (unfold t))]
[((? Mu? s) t) (cg (unfold s) t)] [((? Mu? s) t) (cg (unfold s) t)]
;; type application ;; type application
[((App: (Name: n) args _) [((App: (Name: n) args _)
(App: (Name: n*) args* _)) (App: (Name: n*) args* _))
(unless (free-identifier=? n n*) (unless (free-identifier=? n n*)
(fail! S T)) (fail! S T))
(let ([x (instantiate-poly (lookup-type-name n) args)] (let ([x (instantiate-poly (lookup-type-name n) args)]
[y (instantiate-poly (lookup-type-name n) args*)]) [y (instantiate-poly (lookup-type-name n) args*)])
(cg x y))] (cg x y))]
[((Values: ss) (Values: ts)) [((Values: ss) (Values: ts))
(unless (= (length ss) (length ts)) (unless (= (length ss) (length ts))
(fail! ss ts)) (fail! ss ts))
(cgen/list V X ss ts)] (cgen/list V X ss ts)]
[((Values: ss) (ValuesDots: ts t-dty dbound)) [((Values: ss) (ValuesDots: ts t-dty dbound))
(unless (>= (length ss) (length ts)) (unless (>= (length ss) (length ts))
(fail! ss ts)) (fail! ss ts))
(unless (memq dbound X) (unless (memq dbound X)
(fail! S T)) (fail! S T))
(let* ([num-vars (- (length ss) (length ts))] (let* ([num-vars (- (length ss) (length ts))]
[vars (for/list ([n (in-range num-vars)]) [vars (for/list ([n (in-range num-vars)])
(gensym dbound))] (gensym dbound))]
[new-tys (for/list ([var vars]) [new-tys (for/list ([var vars])
(substitute (make-F var) dbound t-dty))] (substitute (make-F var) dbound t-dty))]
[new-cset (cgen/list V (append vars X) ss (append ts new-tys))]) [new-cset (cgen/list V (append vars X) ss (append ts new-tys))])
(move-vars-to-dmap new-cset dbound vars))] (move-vars-to-dmap new-cset dbound vars))]
[((ValuesDots: ss s-dty dbound) (Values: ts)) [((ValuesDots: ss s-dty dbound) (Values: ts))
(unless (>= (length ts) (length ss)) (unless (>= (length ts) (length ss))
(fail! ss ts)) (fail! ss ts))
(unless (memq dbound X) (unless (memq dbound X)
(fail! S T)) (fail! S T))
(let* ([num-vars (- (length ts) (length ss))] (let* ([num-vars (- (length ts) (length ss))]
[vars (for/list ([n (in-range num-vars)]) [vars (for/list ([n (in-range num-vars)])
(gensym dbound))] (gensym dbound))]
[new-tys (for/list ([var vars]) [new-tys (for/list ([var vars])
(substitute (make-F var) dbound s-dty))] (substitute (make-F var) dbound s-dty))]
[new-cset (cgen/list V (append vars X) (append ss new-tys) ts)]) [new-cset (cgen/list V (append vars X) (append ss new-tys) ts)])
(move-vars-to-dmap new-cset dbound vars))] (move-vars-to-dmap new-cset dbound vars))]
[((ValuesDots: ss s-dty dbound) (ValuesDots: ts t-dty dbound)) [((ValuesDots: ss s-dty dbound) (ValuesDots: ts t-dty dbound))
(when (memq dbound X) (fail! ss ts)) (when (memq dbound X) (fail! ss ts))
(cgen/list V X (cons s-dty ss) (cons t-dty ts))] (cgen/list V X (cons s-dty ss) (cons t-dty ts))]
[((Vector: e) (Vector: e*)) [((Vector: e) (Vector: e*))
(cset-meet (cg e e*) (cg e* e))] (cset-meet (cg e e*) (cg e* e))]
[((Box: e) (Box: e*)) [((Box: e) (Box: e*))
(cset-meet (cg e e*) (cg e* e))] (cset-meet (cg e e*) (cg e* e))]
[((Hashtable: s1 s2) (Hashtable: t1 t2)) [((Hashtable: s1 s2) (Hashtable: t1 t2))
;; the key is covariant, the value is invariant ;; the key is covariant, the value is invariant
(cset-meet* (list (cg s1 t1) (cg t2 s2) (cg s2 t2)))] (cset-meet* (list (cg s1 t1) (cg t2 s2) (cg s2 t2)))]
[((Syntax: s1) (Syntax: s2)) [((Syntax: s1) (Syntax: s2))
(cg s1 s2)] (cg s1 s2)]
;; parameters are just like one-arg functions ;; parameters are just like one-arg functions
[((Param: in1 out1) (Param: in2 out2)) [((Param: in1 out1) (Param: in2 out2))
(cset-meet (cg in2 in1) (cg out1 out2))] (cset-meet (cg in2 in1) (cg out1 out2))]
[((Function: (list t-arr ...)) [((Function: _)
(Function: (list s-arr ...))) (Function: (list (top-arr:))))
(=> unmatch) empty]
(cset-combine [((Function: (list t-arr ...))
(filter (Function: (list s-arr ...)))
values ;; only generate the successful csets (=> unmatch)
(for*/list (cset-combine
([t-arr t-arr] [s-arr s-arr]) (filter
(with-handlers ([exn:infer? (lambda (_) #f)]) values ;; only generate the successful csets
(cgen/arr V X t-arr s-arr)))))] (for*/list
[(_ _) ([t-arr t-arr] [s-arr s-arr])
(cond [(subtype S T) empty] (with-handlers ([exn:infer? (lambda (_) #f)])
;; or, nothing worked, and we fail (cgen/arr V X t-arr s-arr)))))]
[else (fail! S T)])])))) [(_ _)
(cond [(subtype S T) empty]
;; or, nothing worked, and we fail
[else (fail! S T)])]))))
(define (check-vars must-vars subst) (define (check-vars must-vars subst)
(and (for/and ([v must-vars]) (and (for/and ([v must-vars])
@ -488,4 +491,4 @@
(define (i s t r) (define (i s t r)
(infer/simple (list s) (list t) r)) (infer/simple (list s) (list t) r))
;(trace cgen/arr #;cgen #;cgen/list) ;(trace cgen)

4
collects/typed-scheme/private/base-env.ss
View File

@ -90,7 +90,7 @@
[symbol? (make-pred-ty Sym)] [symbol? (make-pred-ty Sym)]
[list? (make-pred-ty (-lst Univ))] [list? (make-pred-ty (-lst Univ))]
[list (-poly (a) (->* '() a (-lst a)))] [list (-poly (a) (->* '() a (-lst a)))]
[procedure? (make-pred-ty (make-Function (list (make-top-arr))))] [procedure? (make-pred-ty top-func)]
[map (-polydots (c a b) ((list ((list a) (b b) . ->... . c) (-lst a)) [map (-polydots (c a b) ((list ((list a) (b b) . ->... . c) (-lst a))
((-lst b) b) . ->... .(-lst c)))] ((-lst b) b) . ->... .(-lst c)))]
[for-each (-polydots (c a b) ((list ((list a) (b b) . ->... . Univ) (-lst a)) [for-each (-polydots (c a b) ((list ((list a) (b b) . ->... . Univ) (-lst a))
@ -561,4 +561,4 @@
;; string.ss ;; string.ss
[real->decimal-string (N [-Nat] . ->opt . -String)] [real->decimal-string (N [-Nat] . ->opt . -String)]
[current-continuation-marks (-> -Cont-Mark-Set)] [current-continuation-marks (-> -Cont-Mark-Set)]

2
collects/typed-scheme/private/base-types.ss
View File

@ -27,5 +27,5 @@
[Boxof (-poly (a) (make-Box a))] [Boxof (-poly (a) (make-Box a))]
[Syntax Any-Syntax] [Syntax Any-Syntax]
[Identifier Ident] [Identifier Ident]
[Procedure (make-Function (list (make-top-arr)))] [Procedure top-func]

4
collects/typed-scheme/private/type-effect-convenience.ss
View File

@ -17,11 +17,13 @@
(provide (all-defined-out) (provide (all-defined-out)
;; these should all eventually go away ;; these should all eventually go away
make-Name make-ValuesDots make-Function make-top-arr make-Latent-Restrict-Effect make-Latent-Remove-Effect) make-Name make-ValuesDots make-Function make-Latent-Restrict-Effect make-Latent-Remove-Effect)
(define (one-of/c . args) (define (one-of/c . args)
(apply Un (map -val args))) (apply Un (map -val args)))
(define top-func (make-Function (list (make-top-arr))))
(define (-vet id) (make-Var-True-Effect id)) (define (-vet id) (make-Var-True-Effect id))
(define (-vef id) (make-Var-False-Effect id)) (define (-vef id) (make-Var-False-Effect id))