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

combine-filter

Browse Source 
update

svn: r13992

original commit: d293635cb7f2894111ec06339422a24c7fb7ef39
This commit is contained in:
Sam Tobin-Hochstadt 2009-03-06 20:54:39 +00:00
parent af10c650fa
commit 89f647fde1
2 changed files with 75 additions and 4 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

44
collects/typed-scheme/typecheck/tc-envops.ss Normal file
View File

@ -0,0 +1,44 @@
#lang scheme/base
(require (rename-in "../utils/utils.ss" [infer infer-in]))
(require (rename-in (types subtype convenience remove-intersect)
[-> -->]
[->* -->*]
[one-of/c -one-of/c])
(infer-in infer)
(rep type-rep)
scheme/contract scheme/match
stxclass/util
(for-syntax scheme/base))
(define (replace-nth l i f)
(cond [(null? l) (error 'replace-nth "list not long enough" l i f)]
[(zero? i) (cons (f (car l)) (cdr l))]
[else (cons (car l) (replace-nth (cdr l) (sub1 i) f))]))
(define/contract (update t lo)
(Type/c Filter/c . -> . Type/c)
(match* (t lo)
;; pair ops
[((Pair: t s) (TypeFilter: u (list* (CarPE:) rst) x))
(make-Pair (update t (make-TypeFilter u rst x)) s)]
[((Pair: t s) (NotTypeFilter: u (list* (CarPE:) rst) x))
(make-Pair (update t (make-NotTypeFilter u rst x)) s)]
[((Pair: t s) (TypeFilter: u (list* (CarPE:) rst) x))
(make-Pair t (update s (make-TypeFilter u rst x)))]
[((Pair: t s) (NotTypeFilter: u (list* (CdrPE:) rst) x))
(make-Pair t (update s (make-NotTypeFilter u rst x)))]
;; struct ops
[((Struct: nm par flds proc poly pred cert)
(TypeFilter: u (list* (StructPE: (? (lambda (s) (subtype t s)) s) idx) rst) x))
(make-Struct nm par (replace-nth flds idx (lambda (e) (update e (make-TypeFilter u rst x)))))]
[((Struct: nm par flds proc poly pred cert)
(NotTypeFilter: u (list* (StructPE: (? (lambda (s) (subtype t s)) s) idx) rst) x))
(make-Struct nm par (replace-nth flds idx (lambda (e) (update e (make-NotTypeFilter u rst x)))))]
;; otherwise
[(t (TypeFilter: u (list) _))
(restrict t u)]
[(t (NotTypeFilter: u (list) _))
(remove t u)]))

35
collects/typed-scheme/typecheck/tc-metafunctions.ss
View File

@ -39,8 +39,8 @@
(lambda (stx) #'(? (lambda (id) (free-identifier=? id x)))))
(match f
[(Bot:) (list (make-LBot))]
[(TypeFilter: t p (=x)) (list (make-LTypeFilter t p))]
[(NotTypeFilter: t p (=x)) (list (make-LNotTypeFilter t p))]
[(TypeFilter: t p (=x)) (list (make-LTypeFilter t p idx))]
[(NotTypeFilter: t p (=x)) (list (make-LNotTypeFilter t p idx))]
[_ null]))
(define/contract (apply-filter lfs t o)
@ -58,5 +58,32 @@
[((LNotTypeFilter: (? (lambda (t) (subtype s t))) (list) _) _ _) (list (make-Bot))]
[((LTypeFilter: (? (lambda (t) (not (overlap s t)))) (list) _) _ _) (list (make-Bot))]
[(_ _ (Empty:)) null]
[((LTypeFilter: t pi* _) _ (Path: pi x)) (make-TypeFilter t (append pi* pi) x)]
[((LNotTypeFilter: t pi* _) _ (Path: pi x)) (make-NotTypeFilter t (append pi* pi) x)]))
[((LTypeFilter: t pi* _) _ (Path: pi x)) (list (make-TypeFilter t (append pi* pi) x))]
[((LNotTypeFilter: t pi* _) _ (Path: pi x)) (list (make-NotTypeFilter t (append pi* pi) x))]))
(define-match-expander T-FS:
(lambda (stx) #'(FilterSet: _ (list (Bot:)))))
(define-match-expander F-FS:
(lambda (stx) #'(FilterSet: (list (Bot:)) _)))
(define/contract (combine-filter f1 f2 f3)
(FilterSet? FilterSet? FilterSet? . -> . FilterSet?)
(match* (f1 f2 f3)
[(f (T-FS:) (F-FS:)) f] ;; the student expansion
[((T-FS:) f _) f]
[((F-FS:) _ f) f]
;; skipping the general or/predicate rule because it's really complicated
;; or/predicate special case for one elem lists
;; note that we are relying on equal? on identifiers here
[((FilterSet: (list (TypeFilter: t pi x)) (list (NotTypeFilter: t pi x)))
(T-FS:)
(FilterSet: (list (TypeFilter: s pi x)) (list (NotTypeFilter: s pi x))))
(make-FilterSet (list (make-TypeFilter (Un t s) pi x)) (list (make-NotTypeFilter (Un t s) pi x)))]
;; or
[((FilterSet: f1+ f1-) (T-FS:) (FilterSet: f3+ f3-)) (combine null (append f1- f3-))]
;; and
[((FilterSet: f1+ f1-) (FilterSet: f2+ f2-) (F-FS:)) (combine (append f1+ f2+) null)]
[(f f* f*) f*]
[(_ _ _)
;; could intersect f2 and f3 here
(make-FilterSet null null)]))