fix resolve usage in overlap, allocate less (#555)
check calls to resolve-once to see if they return #f (i.e. if a type is not yet defined), and have overlap only extend its seen list when it is resolving/unfolding a potentially infinite type
This commit is contained in:
Andrew Kent
GitHub
parent
2785e6f950
commit
dda8b1da20
|
|
@ -7,7 +7,7 @@
|
|||
|
||||
|
||||
;;************************************************************
|
||||
;; Current Seen Continuation Mark
|
||||
;; Current Seen Continuation Mark for Subtyping
|
||||
;;************************************************************
|
||||
;;
|
||||
;; Prevents infinite loops when subtyping calls outside
|
||||
|
|
|
|||
|
|
@ -24,11 +24,13 @@
|
|||
;; let's not loop forever while checking overlap
|
||||
(define current-seen (make-parameter '()))
|
||||
(define (seen? t1 t2)
|
||||
(let ([a (cons t1 t2)]
|
||||
[b (cons t2 t1)])
|
||||
(for/or ([p (in-list (current-seen))])
|
||||
(or (equal? p a)
|
||||
(equal? p b)))))
|
||||
(for*/or ([p (in-list (current-seen))]
|
||||
[a (in-value (car p))]
|
||||
[d (in-value (cdr p))])
|
||||
(or (and (equal? t1 a)
|
||||
(equal? t2 d))
|
||||
(and (equal? t1 d)
|
||||
(equal? t2 a)))))
|
||||
(define-syntax-rule (with-updated-seen t1 t2 body ...)
|
||||
(parameterize ([current-seen (cons (cons t1 t2) (current-seen))])
|
||||
body ...))
|
||||
|
|
@ -39,123 +41,122 @@
|
|||
;; have a non-empty intersection
|
||||
(define/cond-contract (overlap? t1 t2)
|
||||
(c:-> Type? Type? boolean?)
|
||||
(cond
|
||||
[(equal? t1 t2) #t]
|
||||
[(disjoint-masks? (mask t1) (mask t2)) #f]
|
||||
[(seen? t1 t2) #t]
|
||||
[else
|
||||
(with-updated-seen
|
||||
t1 t2
|
||||
(match*/no-order
|
||||
(t1 t2)
|
||||
[((Univ:) _) #:no-order #t]
|
||||
[((or (B: _) (F: _)) _) #:no-order #t]
|
||||
[((Opaque: _) _) #:no-order #t]
|
||||
[((Name/simple: n) (Name/simple: n*))
|
||||
(or (free-identifier=? n n*)
|
||||
(overlap? (resolve-once t1) (resolve-once t2)))]
|
||||
[(t (or (? Name? s)
|
||||
(? App? s)))
|
||||
#:no-order
|
||||
(overlap? t (resolve-once s))]
|
||||
[((? Mu? t1) t2) #:no-order (overlap? (unfold t1) t2)]
|
||||
[((Refinement: t1 _) t2) #:no-order (overlap? t1 t2)]
|
||||
[((BaseUnion: bbits1 nbits1)
|
||||
(BaseUnion: bbits2 nbits2))
|
||||
(or (bbits-overlap? bbits1 bbits2)
|
||||
(nbits-overlap? nbits1 nbits2))]
|
||||
[((BaseUnion: bbits nbits) (Base-bits: num? bits))
|
||||
#:no-order
|
||||
(if num?
|
||||
(nbits-overlap? nbits bits)
|
||||
(bbits-overlap? bbits bits))]
|
||||
[((BaseUnion-bases: bases1) t2)
|
||||
#:no-order
|
||||
(for/or ([b1 (in-list bases1)]) (overlap? b1 t2))]
|
||||
[((Union: (BaseUnion: bbits1 nbits1) _)
|
||||
(Union: (BaseUnion: bbits2 nbits2) _))
|
||||
#:when (or (bbits-overlap? bbits1 bbits2)
|
||||
(nbits-overlap? nbits1 nbits2))
|
||||
#t]
|
||||
[((Union/set: base1 ts1 elems1) t2)
|
||||
#:no-order
|
||||
(or (hash-ref elems1 t2 #f)
|
||||
(overlap? base1 t2)
|
||||
(for/or ([t1 (in-list ts1)]) (overlap? t1 t2)))]
|
||||
;; we ignore the possible refining prop for simplicities sake
|
||||
[((Intersection: ts _) s)
|
||||
#:no-order
|
||||
(for/and ([t (in-list ts)]) (overlap? t s))]
|
||||
[((or (Poly-unsafe: _ t1)
|
||||
(PolyDots-unsafe: _ t1))
|
||||
t2)
|
||||
#:no-order
|
||||
(overlap? t1 t2)] ;; conservative
|
||||
[((? Base?) (? Base?)) (or (subtype t1 t2) (subtype t2 t1))]
|
||||
[((? Base? t) (? Value? s)) #:no-order (subtype s t)] ;; conservative
|
||||
[((Syntax: t) (Syntax: t*)) (overlap? t t*)]
|
||||
[((Syntax: _) _) #:no-order #f]
|
||||
[((? Base?) _) #:no-order #f]
|
||||
[((Value: (? pair?)) (Pair: _ _)) #:no-order #t]
|
||||
[((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
|
||||
[((Sequence: _) (Val-able: v)) #:no-order (sequence? v)]
|
||||
;; hash tables are two-valued sequences
|
||||
[((Sequence: (or (list _) (list _ _ _ ...)))
|
||||
(or (? Hashtable?) (? HashtableTop?)))
|
||||
#:no-order
|
||||
#f]
|
||||
;; these are single-valued sequences
|
||||
[((Sequence: (list _ _ _ ...))
|
||||
(or (? Pair?) (? Vector?) (? VectorTop?)))
|
||||
#:no-order
|
||||
#f]
|
||||
;; be conservative about other kinds of sequences
|
||||
[((Sequence: _) _) #:no-order #t]
|
||||
;; Values where evt? produces #f cannot be Evt
|
||||
[((Evt: _) (Val-able: v)) #:no-order (evt? v)]
|
||||
[((Pair: _ _) _) #:no-order #f]
|
||||
[((Val-able: (? simple-datum? v1))
|
||||
(Val-able: (? simple-datum? v2)))
|
||||
(equal? v1 v2)]
|
||||
[((Val-able: (? simple-datum?))
|
||||
(or (? Struct?) (? StructTop?) (? Function?)))
|
||||
#:no-order
|
||||
#f]
|
||||
[((Val-able: (not (? hash?)))
|
||||
(or (? Hashtable?) (? HashtableTop?)))
|
||||
#:no-order
|
||||
#f]
|
||||
[((Struct: n _ flds _ _ _)
|
||||
(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*)]))]
|
||||
[((Struct: n #f _ _ _ _)
|
||||
(StructTop: (Struct: n* #f _ _ _ _)))
|
||||
#:when (free-identifier=? n n*)
|
||||
#t]
|
||||
[((StructTop: (Struct: n* #f _ _ _ _))
|
||||
(Struct: n #f _ _ _ _))
|
||||
#:when (free-identifier=? n n*)
|
||||
#t]
|
||||
;; n and n* must be different, so there's no overlap
|
||||
[((Struct: n #f flds _ _ _)
|
||||
(Struct: n* #f flds* _ _ _))
|
||||
#f]
|
||||
[((Struct: n #f flds _ _ _)
|
||||
(StructTop: (Struct: n* #f flds* _ _ _)))
|
||||
#f]
|
||||
[((StructTop: (Struct: n* #f flds* _ _ _))
|
||||
(Struct: n #f flds _ _ _))
|
||||
#f]
|
||||
[((and t1 (Struct: _ _ _ _ _ _))
|
||||
(and t2 (Struct: _ _ _ _ _ _)))
|
||||
(or (subtype t1 t2) (subtype t2 t1)
|
||||
(parent-of? t1 t2) (parent-of? t2 t1))]
|
||||
[(_ _) #t]))]))
|
||||
(match*/no-order
|
||||
(t1 t2)
|
||||
[(_ _) #:when (equal? t1 t2) #t]
|
||||
[(_ _) #:when (disjoint-masks? (mask t1) (mask t2)) #f]
|
||||
[(_ _) #:when (seen? t1 t2) #t]
|
||||
[((Univ:) _) #:no-order #t]
|
||||
[((or (B: _) (F: _)) _) #:no-order #t]
|
||||
[((Opaque: _) _) #:no-order #t]
|
||||
[((Name/simple: n) (Name/simple: n*)) #:when (free-identifier=? n n*) #t]
|
||||
[(t1 (or (? Name? t2)
|
||||
(? App? t2)))
|
||||
#:no-order
|
||||
(with-updated-seen t1 t2
|
||||
(let ([t2 (resolve-once t2)])
|
||||
(or (not t2) (overlap? t1 t2))))]
|
||||
[((? Mu? t1) t2)
|
||||
#:no-order
|
||||
(with-updated-seen t1 t2
|
||||
(overlap? (unfold t1) t2))]
|
||||
[((Refinement: t1 _) t2) #:no-order (overlap? t1 t2)]
|
||||
[((BaseUnion: bbits1 nbits1)
|
||||
(BaseUnion: bbits2 nbits2))
|
||||
(or (bbits-overlap? bbits1 bbits2)
|
||||
(nbits-overlap? nbits1 nbits2))]
|
||||
[((BaseUnion: bbits nbits) (Base-bits: num? bits))
|
||||
#:no-order
|
||||
(if num?
|
||||
(nbits-overlap? nbits bits)
|
||||
(bbits-overlap? bbits bits))]
|
||||
[((BaseUnion-bases: bases1) t2)
|
||||
#:no-order
|
||||
(for/or ([b1 (in-list bases1)]) (overlap? b1 t2))]
|
||||
[((Union: (BaseUnion: bbits1 nbits1) _)
|
||||
(Union: (BaseUnion: bbits2 nbits2) _))
|
||||
#:when (or (bbits-overlap? bbits1 bbits2)
|
||||
(nbits-overlap? nbits1 nbits2))
|
||||
#t]
|
||||
[((Union/set: base1 ts1 elems1) t2)
|
||||
#:no-order
|
||||
(or (hash-ref elems1 t2 #f)
|
||||
(overlap? base1 t2)
|
||||
(for/or ([t1 (in-list ts1)]) (overlap? t1 t2)))]
|
||||
;; we ignore the possible refining prop for simplicities sake
|
||||
[((Intersection: ts _) s)
|
||||
#:no-order
|
||||
(for/and ([t (in-list ts)]) (overlap? t s))]
|
||||
[((or (Poly-unsafe: _ t1)
|
||||
(PolyDots-unsafe: _ t1))
|
||||
t2)
|
||||
#:no-order
|
||||
(overlap? t1 t2)] ;; conservative
|
||||
[((? Base?) (? Base?)) (or (subtype t1 t2) (subtype t2 t1))]
|
||||
[((? Base? t) (? Value? s)) #:no-order (subtype s t)] ;; conservative
|
||||
[((Syntax: t) (Syntax: t*)) (overlap? t t*)]
|
||||
[((Syntax: _) _) #:no-order #f]
|
||||
[((? Base?) _) #:no-order #f]
|
||||
[((Value: (? pair?)) (Pair: _ _)) #:no-order #t]
|
||||
[((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
|
||||
[((Sequence: _) (Val-able: v)) #:no-order (sequence? v)]
|
||||
;; hash tables are two-valued sequences
|
||||
[((Sequence: (or (list _) (list _ _ _ ...)))
|
||||
(or (? Hashtable?) (? HashtableTop?)))
|
||||
#:no-order
|
||||
#f]
|
||||
;; these are single-valued sequences
|
||||
[((Sequence: (list _ _ _ ...))
|
||||
(or (? Pair?) (? Vector?) (? VectorTop?)))
|
||||
#:no-order
|
||||
#f]
|
||||
;; be conservative about other kinds of sequences
|
||||
[((Sequence: _) _) #:no-order #t]
|
||||
;; Values where evt? produces #f cannot be Evt
|
||||
[((Evt: _) (Val-able: v)) #:no-order (evt? v)]
|
||||
[((Pair: _ _) _) #:no-order #f]
|
||||
[((Val-able: (? simple-datum? v1))
|
||||
(Val-able: (? simple-datum? v2)))
|
||||
(equal? v1 v2)]
|
||||
[((Val-able: (? simple-datum?))
|
||||
(or (? Struct?) (? StructTop?) (? Function?)))
|
||||
#:no-order
|
||||
#f]
|
||||
[((Val-able: (not (? hash?)))
|
||||
(or (? Hashtable?) (? HashtableTop?)))
|
||||
#:no-order
|
||||
#f]
|
||||
[((Struct: n _ flds _ _ _)
|
||||
(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*)]))]
|
||||
[((Struct: n #f _ _ _ _)
|
||||
(StructTop: (Struct: n* #f _ _ _ _)))
|
||||
#:when (free-identifier=? n n*)
|
||||
#t]
|
||||
[((StructTop: (Struct: n* #f _ _ _ _))
|
||||
(Struct: n #f _ _ _ _))
|
||||
#:when (free-identifier=? n n*)
|
||||
#t]
|
||||
;; n and n* must be different, so there's no overlap
|
||||
[((Struct: n #f flds _ _ _)
|
||||
(Struct: n* #f flds* _ _ _))
|
||||
#f]
|
||||
[((Struct: n #f flds _ _ _)
|
||||
(StructTop: (Struct: n* #f flds* _ _ _)))
|
||||
#f]
|
||||
[((StructTop: (Struct: n* #f flds* _ _ _))
|
||||
(Struct: n #f flds _ _ _))
|
||||
#f]
|
||||
[((and t1 (Struct: _ _ _ _ _ _))
|
||||
(and t2 (Struct: _ _ _ _ _ _)))
|
||||
(or (subtype t1 t2) (subtype t2 t1)
|
||||
(parent-of? t1 t2) (parent-of? t2 t1))]
|
||||
[(_ _) #t]))
|
||||
|
||||
|
||||
;; Type Type -> Boolean
|
||||
|
|
|
|||
4
typed-racket-test/succeed/gh-issue-542.rkt
Normal file
4
typed-racket-test/succeed/gh-issue-542.rkt
Normal file
|
|
@ -0,0 +1,4 @@
|
|||
#lang typed/racket
|
||||
(struct (A) S ([f : A]))
|
||||
|
||||
(define-type T (∩ (S Nonnegative-Integer) (S Nonpositive-Integer)))
|
||||
Loading…
Reference in New Issue
Block a user