dont let-alias type vars, better overlap & restrict

This commit is contained in:
Andrew Kent 2015-01-06 13:51:40 -05:00
parent dc2ce38aef
commit 16db5ecc78
4 changed files with 53 additions and 60 deletions

View File

@ -51,9 +51,9 @@
;; resolve resolvable types if we haven't already done so
[((? needs-resolving?) _) #:when (not (set-member? resolved (cons t1 t2)))
(restrict* (resolve-once t1) t2 pref (set-add resolved (cons t1 t2)))]
(restrict* (resolve t1) t2 pref (set-add resolved (cons t1 t2)))]
[(_ (? needs-resolving?)) #:when (not (set-member? resolved (cons t1 t2)))
(restrict* t1 (resolve-once t2) pref (set-add resolved (cons t1 t2)))]
(restrict* t1 (resolve t2) pref (set-add resolved (cons t1 t2)))]
;; we don't actually want this - want something that's a part of t1
[(_ _) #:when (subtype t2 t1)

View File

@ -6,7 +6,7 @@
(private type-annotation parse-type syntax-properties)
(env lexical-env type-alias-helper mvar-env
global-env scoped-tvar-env)
(rep filter-rep object-rep)
(rep filter-rep object-rep type-rep)
syntax/free-vars
(typecheck signatures tc-metafunctions tc-subst internal-forms tc-envops)
(utils tarjan)
@ -52,7 +52,7 @@
(match e-r
[(list (tc-result: e-ts (FilterSet: fs+ fs-) os) ...)
(values e-ts
(map (λ (o n) (if (is-var-mutated? n) -empty-obj o)) os names)
(map (λ (o n t) (if (or (is-var-mutated? n) (F? t)) -empty-obj o)) os names e-ts)
(apply append
(for/list ([n (in-list names)]
[t (in-list e-ts)]
@ -64,12 +64,12 @@
(list f+)]
[(is-var-mutated? n)
(list)]
;; n is being bound to an expression w/ object o
;; we don't need any new info, aliasing and the
;; lexical environment will have the needed info
[(Path? o) (list)]
;; n is being bound to an expression w/o an object
;; so remember n in our propositions
;; n is being bound to an expression w/ object o, no new info
;; is required due to aliasing (note: we currently do not
;; alias objects typed as type variables)
[(and (Path? o) (not (F? t))) (list)]
;; n is being bound to an expression w/o an object (or whose
;; type is a type variable) so create props about n
[else (list (-or (-and (-not-filter (-val #f) n) f+)
(-and (-filter (-val #f) n) f-)))]))))]
[(list (tc-result: e-ts (NoFilter:) _) ...)

View File

@ -32,69 +32,49 @@
#f]
[else
(match (list t1 t2)
[(list (Univ:) _) #t]
[(list _ (Univ:)) #t]
[(list (F: _) _) #t]
[(list _ (F: _)) #t]
[(list-no-order (Univ:) _) #t]
[(list-no-order (F: _) _) #t]
[(list (Opaque: _) _) #t]
[(list _ (Opaque: _)) #t]
[(list-no-order _ (Opaque: _)) #t]
[(list (Name/simple: n) (Name/simple: n*))
(or (free-identifier=? n n*)
(overlap (resolve-once t1) (resolve-once t2)))]
[(list _ (? Name?))
(overlap t1 (resolve-once t2))]
[(list (? Name?) _)
(overlap (resolve-once t1) t2)]
[(list (? Mu?) _) (overlap (unfold t1) t2)]
[(list _ (? Mu?)) (overlap t1 (unfold t2))]
[(list (Refinement: t _) t2) (overlap t t2)]
[(list t1 (Refinement: t _)) (overlap t1 t)]
[(list (Union: e) t)
(ormap (lambda (t*) (overlap t* t)) e)]
[(list t (Union: e))
(ormap (lambda (t*) (overlap t t*)) e)]
[(or (list _ (? Poly?)) (list (? Poly?) _))
#t] ;; these can have overlap, conservatively
[(list-no-order t (? Name? s))
(overlap t (resolve-once s))]
[(list-no-order (? Mu? t) s) (overlap (unfold t) s)]
[(list-no-order (Refinement: t _) s) (overlap t s)]
[(list-no-order (Union: ts) s)
(ormap (lambda (t*) (overlap t* s)) ts)]
[(list-no-order (? Poly?) _) #t] ;; conservative
[(list (Base: s1 _ _ _) (Base: s2 _ _ _)) (or (subtype t1 t2) (subtype t2 t1))]
[(list (Base: _ _ _ _) (Value: _)) (subtype t2 t1)] ;; conservative
[(list (Value: _) (Base: _ _ _ _)) (subtype t1 t2)] ;; conservative
[(list (Syntax: t) (Syntax: t*))
(overlap t t*)]
[(or (list (Syntax: _) _)
(list _ (Syntax: _)))
#f]
[(list (Base: _ _ _ _) _) #f]
[(list _ (Base: _ _ _ _)) #f]
[(list (Value: (? pair? v)) (Pair: _ _)) #t]
[(list (Pair: _ _) (Value: (? pair? v))) #t]
[(list (Pair: a b) (Pair: a* b*))
(and (overlap a a*)
(overlap b b*))]
;; lots of things are sequences
[(list (Sequence: _) _) #t]
[(list _ (Sequence: _)) #t]
[(or (list (Pair: _ _) _)
(list _ (Pair: _ _)))
#f]
[(list-no-order (? Base? t) (? Value? s)) (subtype t s)] ;; conservative
[(list (Syntax: t) (Syntax: t*)) (overlap t t*)]
[(list-no-order (Syntax: _) _) #f]
[(list-no-order (Base: _ _ _ _) _) #f]
[(list-no-order (Value: (? pair?)) (Pair: _ _)) #t]
[(list (Pair: a b) (Pair: a* b*)) (and (overlap a a*)
(overlap b b*))]
;; lots of things are sequences, but not values where sequence? produces #f
[(list-no-order (Sequence: _) (Value: v)) (sequence? v)]
[(list-no-order (Sequence: _) _) #t]
;; Values where evt? produces #f cannot be Evt
[(list-no-order (Evt: _) (Value: v)) (evt? v)]
[(list-no-order (Pair: _ _) _) #f]
[(list (Value: (? simple-datum? v1))
(Value: (? simple-datum? v2)))
(equal? v1 v2)]
[(or (list (Value: (? simple-datum?))
(or (? Struct?) (? StructTop?) (? Function?)))
(list (or (? Struct?) (? StructTop?) (? Function?))
(Value: (? simple-datum?))))
[(list-no-order (Value: (? simple-datum?))
(or (? Struct?) (? StructTop?) (? Function?)))
#f]
[(list (Struct: n _ flds _ _ _)
(Struct: n* _ flds* _ _ _)) (=> nevermind)
(unless (free-identifier=? n n*) (nevermind))
(Struct: n* _ flds* _ _ _))
#:when (free-identifier=? n n*)
(for/and ([f (in-list flds)] [f* (in-list flds*)])
(match* (f f*)
[((fld: t _ _) (fld: t* _ _)) (overlap t t*)]))]
[(list (Struct: n #f _ _ _ _)
(StructTop: (Struct: n* #f _ _ _ _))) (=> nevermind)
(unless (free-identifier=? n n*) (nevermind))
(StructTop: (Struct: n* #f _ _ _ _)))
#:when (free-identifier=? n n*)
#t]
;; n and n* must be different, so there's no overlap
[(list (Struct: n #f flds _ _ _)

View File

@ -1957,7 +1957,7 @@
(Boolean -> #t))
(t:-> -Boolean (-val #t))]
[tc-e (sequence? 'foo)
[tc-e (sequence? (ann 'foo Any))
-Boolean]
[tc-err (stop-before (inst empty-sequence Symbol) zero?)]
[tc-e (stop-before (inst empty-sequence Integer) zero?)
@ -3402,6 +3402,19 @@
x*
42))))))]
;; ensure let-aliasing doesn't cause problems w/ type variable types
[tc-e (let ()
(: foo (All (A) (-> A (Tuple Number A))))
(define foo
(λ (x)
(let ([x* x])
(cond
[(number? x*) (list x* x)]
[(number? x) (list x x*)]
[else (list 42 x*)]))))
(void))
-Void]
;; tests looking up path-types into unions
[tc-e (let ()
(: foo ((U (Pairof Number Number) (Pairof Number String)) -> Number))