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

have overlap use a current-seen list

Browse Source
This commit is contained in:
Andrew Kent 2016-07-13 15:21:17 -04:00
parent 3f372c3b04
commit a5c4ad2f77
2 changed files with 151 additions and 75 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

165
typed-racket-lib/typed-racket/types/overlap.rkt
View File

@ -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

61
typed-racket-test/succeed/pr403.rkt Normal file
View File

@ -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)))))))))