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

Improve restrict, and allow caller to control what type is returned for failure.

Browse Source 
original commit: 74c9265d66a964e82513e1c53d597b6644560f00
This commit is contained in:
Sam Tobin-Hochstadt 2012-02-20 13:19:15 -05:00
parent 4c849a4eda
commit 4f2353d93f
1 changed files with 17 additions and 17 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

34
collects/typed-racket/infer/restrict.rkt
View File

@ -2,7 +2,7 @@
(require "../utils/utils.rkt")
(require (rep type-rep)
(types utils union subtype remove-intersect resolve substitute)
(types utils union subtype remove-intersect resolve substitute abbrev)
"signatures.rkt"
racket/match mzlib/trace)
@ -12,26 +12,26 @@
;; NEW IMPL
;; restrict t1 to be a subtype of t2
(define (restrict* t1 t2)
;; if `f' is 'new, use t2 when giving up, otherwise use t1
(define (restrict* t1 t2 [f 'new])
;; we don't use union map directly, since that might produce too many elements
(define (union-map f l)
(match l
[(Union: es)
(let ([l (map f es)])
(apply Un l))]))
(cond
[(subtype t1 t2) t1] ;; already a subtype
[(match t2
[(Poly: vars t)
(let ([subst (infer vars null (list t1) (list t) t1)])
(and subst (restrict* t1 (subst-all subst t1))))]
[_ #f])]
[(Union? t1) (union-map (lambda (e) (restrict* e t2)) t1)]
[(needs-resolving? t1) (restrict* (resolve-once t1) t2)]
[(needs-resolving? t2) (restrict* t1 (resolve-once t2))]
[(subtype t2 t1) t2] ;; we don't actually want this - want something that's a part of t1
[(not (overlap t1 t2)) (Un)] ;; there's no overlap, so the restriction is empty
[else t2] ;; t2 and t1 have a complex relationship, so we punt
))
(match* (t1 t2)
[(_ (? (lambda _ (subtype t1 t2)))) t1] ;; already a subtype
[(_ (Poly: vars t))
(let ([subst (infer vars null (list t1) (list t) t1)])
(and subst (restrict* t1 (subst-all subst t1) f)))]
[((Union: _) _) (union-map (lambda (e) (restrict* e t2 f)) t1)]
[(_ (Union: _)) (union-map (lambda (e) (restrict* t1 e f)) t2)]
[((? needs-resolving?) _) (restrict* (resolve-once t1) t2 f)]
[(_ (? needs-resolving?)) (restrict* t1 (resolve-once t2) f)]
[(_ _)
(cond [(subtype t2 t1) t2] ;; we don't actually want this - want something that's a part of t1
[(not (overlap t1 t2)) (Un)] ;; there's no overlap, so the restriction is empty
[else (if (eq? f 'new) t2 t1)])])) ;; t2 and t1 have a complex relationship, so we punt
(define restrict restrict*)
;(trace restrict*)