From a5c4ad2f776419835b01a1af358c9976b6f16610 Mon Sep 17 00:00:00 2001 From: Andrew Kent Date: Wed, 13 Jul 2016 15:21:17 -0400 Subject: [PATCH] have overlap use a current-seen list --- .../typed-racket/types/overlap.rkt | 165 ++++++++++-------- typed-racket-test/succeed/pr403.rkt | 61 +++++++ 2 files changed, 151 insertions(+), 75 deletions(-) create mode 100644 typed-racket-test/succeed/pr403.rkt diff --git a/typed-racket-lib/typed-racket/types/overlap.rkt b/typed-racket-lib/typed-racket/types/overlap.rkt index fcb1a227..7f40ddf1 100644 --- a/typed-racket-lib/typed-racket/types/overlap.rkt +++ b/typed-racket-lib/typed-racket/types/overlap.rkt @@ -21,6 +21,18 @@ (void? v) (eof-object? v))) +;; 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))))) +(define-syntax-rule (with-updated-seen t1 t2 body ...) + (parameterize ([current-seen (cons (cons t1 t2) (current-seen))]) + body ...)) + ;; overlap? ;; Type Type -> Boolean ;; a conservative check to see if two types @@ -37,86 +49,89 @@ [(and (pair? k1) (pair? k2) (for/and ([i (in-list k1)]) (not (memq i k2)))) #f] + [(seen? t1 t2) #t] [else - (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 (? Name? s)) - #:no-order - (overlap? t (resolve-once s))] - [((? Mu? t) s) #:no-order (overlap? (unfold t) s)] - [((Refinement: t _) s) #:no-order (overlap? t s)] - [((Union: ts) s) - #:no-order - (ormap (λ (t) (overlap? t s)) ts)] - [((Intersection: ts) s) - #:no-order - (for/and ([t (in-immutable-set ts)]) - (overlap? t s))] - [((? Poly?) _) #:no-order #t] ;; conservative - [((Base: s1 _ _ _) (Base: s2 _ _ _)) (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: _) (Value: v)) #:no-order (sequence? v)] - ;; hash tables are two-valued sequences - [((Sequence: (or (list _) (list _ _ _ ...))) - (or (? Hashtable?) (? HashtableTop?))) + (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 (? Name? s)) + #:no-order + (overlap? t (resolve-once s))] + [((? Mu? t) s) #:no-order (overlap? (unfold t) s)] + [((Refinement: t _) s) #:no-order (overlap? t s)] + [((Union: ts) s) + #:no-order + (ormap (λ (t) (overlap? t s)) ts)] + [((Intersection: ts) s) + #:no-order + (for/and ([t (in-immutable-set ts)]) + (overlap? t s))] + [((? Poly?) _) #:no-order #t] ;; conservative + [((Base: s1 _ _ _) (Base: s2 _ _ _)) (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: _) (Value: 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?))) + ;; 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: _) (Value: v)) #:no-order (evt? v)] - [((Pair: _ _) _) #:no-order #f] - [((Value: (? simple-datum? v1)) - (Value: (? simple-datum? v2))) - (equal? v1 v2)] - [((Value: (? simple-datum?)) - (or (? Struct?) (? StructTop?) (? Function?))) - #:no-order - #f] - [((Value: (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] - ;; 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] - [((and t1 (Struct: _ _ _ _ _ _)) - (and t2 (Struct: _ _ _ _ _ _))) - (or (subtype t1 t2) (subtype t2 t1) - (parent-of? t1 t2) (parent-of? t2 t1))] - [(_ _) #t])])) + ;; be conservative about other kinds of sequences + [((Sequence: _) _) #:no-order #t] + ;; Values where evt? produces #f cannot be Evt + [((Evt: _) (Value: v)) #:no-order (evt? v)] + [((Pair: _ _) _) #:no-order #f] + [((Value: (? simple-datum? v1)) + (Value: (? simple-datum? v2))) + (equal? v1 v2)] + [((Value: (? simple-datum?)) + (or (? Struct?) (? StructTop?) (? Function?))) + #:no-order + #f] + [((Value: (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] + ;; 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] + [((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 ;; Given two struct types, check if the second is a parent struct diff --git a/typed-racket-test/succeed/pr403.rkt b/typed-racket-test/succeed/pr403.rkt new file mode 100644 index 00000000..23f52788 --- /dev/null +++ b/typed-racket-test/succeed/pr403.rkt @@ -0,0 +1,61 @@ +#lang typed/racket + +;; https://github.com/racket/typed-racket/issues/403 +;; Ran forever, fix involved making overlap +;; keep a "current-seen" list to not +;; keep resolving types it had already seen before. + +(define-type (List3-Maybe Start Mid End) + (Listof* Start + (U Null + (Pairof Mid (Listof End))))) + +(define-type (List3 Start Mid End) + (Listof* Start + (Pairof Mid (Listof End)))) + +(define-type (Listof* Start End) + (Rec R (U (Pairof Start R) + End))) + +(: replace-first (∀ (A B1 B2 C D) + (case→ + (→ C + (Listof (U A B1)) + (→ (U A B1) Any : #:+ B1 #:- (! B1)) + (List3-Maybe A C (U A B1))) + (→ C + (Listof* A (U Null (Pairof B2 D))) + (→ (U A B2) Any : #:+ (! A) ;; ∴ (and (! A) B2) + #:- (! B2)) + (Listof* A (U Null (Pairof C D)))) + (→ C + (Listof* A (Pairof B2 D)) + (→ (U A B2) Any : #:+ (! A) ;; ∴ (and (! A) B2) + #:- (! B2)) + (Listof* A (Pairof C D))) + (→ C + (Listof A) + (→ (U A B1) Any) + (List3-Maybe A C (U A B1))) + (→ A + C + (Listof A) + (List3-Maybe A C (U A B1))) + (→ A + C + (Listof A) + (→ A (U A B1) Any) + (List3-Maybe A C (U A B1)))))) +(define (replace-first a1 a2 a3 [a4 eq?]) + (if (list? a3) + (replace-first a2 a3 (λ ([x : (U A B1)]) (a4 a1 x))) + (let ([to a1] + [pred? a3]) + (let rec ([l a2]) + (if (null? l) + '() + (if (pred? (car l)) + (cons to (cdr l)) + (cons (car l) + (rec (cdr l)))))))))