use aux function to avoid generating useless filters
This commit is contained in:
parent
fe10457f4e
commit
c031729e4b
|
@ -27,30 +27,30 @@
|
|||
(match* ((resolve t) lo)
|
||||
;; pair ops
|
||||
[((Pair: t s) (TypeFilter: u (list rst ... (CarPE:)) x))
|
||||
(make-Pair (update t (make-TypeFilter u rst x)) s)]
|
||||
(make-Pair (update t (-filter u x rst)) s)]
|
||||
[((Pair: t s) (NotTypeFilter: u (list rst ... (CarPE:)) x))
|
||||
(make-Pair (update t (make-NotTypeFilter u rst x)) s)]
|
||||
(make-Pair (update t (-not-filter u x rst)) s)]
|
||||
[((Pair: t s) (TypeFilter: u (list rst ... (CdrPE:)) x))
|
||||
(make-Pair t (update s (make-TypeFilter u rst x)))]
|
||||
(make-Pair t (update s (-filter u x rst)))]
|
||||
[((Pair: t s) (NotTypeFilter: u (list rst ... (CdrPE:)) x))
|
||||
(make-Pair t (update s (make-NotTypeFilter u rst x)))]
|
||||
(make-Pair t (update s (-not-filter u x rst)))]
|
||||
|
||||
;; syntax ops
|
||||
[((Syntax: t) (TypeFilter: u (list rst ... (SyntaxPE:)) x))
|
||||
(make-Syntax (update t (make-TypeFilter u rst x)))]
|
||||
(make-Syntax (update t (-filter u x rst)))]
|
||||
[((Syntax: t) (NotTypeFilter: u (list rst ... (SyntaxPE:)) x))
|
||||
(make-Syntax (update t (make-NotTypeFilter u rst x)))]
|
||||
(make-Syntax (update t (-not-filter u x rst)))]
|
||||
|
||||
;; struct ops
|
||||
[((Struct: nm par flds proc poly pred cert acc-ids maker-id)
|
||||
(TypeFilter: u (list rst ... (StructPE: (? (lambda (s) (subtype t s)) s) idx)) x))
|
||||
(make-Struct nm par
|
||||
(replace-nth flds idx
|
||||
(lambda (e) (update e (make-TypeFilter u rst x))))
|
||||
(lambda (e) (update e (-filter u x rst))))
|
||||
proc poly pred cert acc-ids maker-id)]
|
||||
[((Struct: nm par flds proc poly pred cert acc-ids maker-id)
|
||||
(NotTypeFilter: u (list rst ... (StructPE: (? (lambda (s) (subtype t s)) s) idx)) x))
|
||||
(make-Struct nm par (replace-nth flds idx (lambda (e) (update e (make-NotTypeFilter u rst x)))) proc poly pred cert acc-ids maker-id)]
|
||||
(make-Struct nm par (replace-nth flds idx (lambda (e) (update e (-not-filter u x rst)))) proc poly pred cert acc-ids maker-id)]
|
||||
|
||||
;; otherwise
|
||||
[(t (TypeFilter: u (list) _))
|
||||
|
|
|
@ -141,8 +141,8 @@
|
|||
(define (tc-id id)
|
||||
(let* ([ty (lookup-type/lexical id)])
|
||||
(ret ty
|
||||
(make-FilterSet (make-NotTypeFilter (-val #f) null id)
|
||||
(make-TypeFilter (-val #f) null id))
|
||||
(make-FilterSet (-not-filter (-val #f) id)
|
||||
(-filter (-val #f) id))
|
||||
(make-Path null id))))
|
||||
|
||||
;; typecheck an expression, but throw away the effect
|
||||
|
|
|
@ -42,8 +42,8 @@
|
|||
(for/list ([n names]
|
||||
[f+ fs+]
|
||||
[f- fs-])
|
||||
(list (make-ImpFilter (make-NotTypeFilter (-val #f) null n) f+)
|
||||
(make-ImpFilter (make-TypeFilter (-val #f) null n) f-)))))]))))
|
||||
(list (make-ImpFilter (-not-filter (-val #f) n) f+)
|
||||
(make-ImpFilter (-filter (-val #f) n) f-)))))]))))
|
||||
;; extend the lexical environment for checking the body
|
||||
(with-lexical-env/extend/props
|
||||
;; the list of lists of name
|
||||
|
|
|
@ -69,10 +69,10 @@
|
|||
(filter-case (#:Type sb-t #:Filter rec) f
|
||||
[#:TypeFilter
|
||||
t p (lookup: idx)
|
||||
(make-TypeFilter t p idx)]
|
||||
(-filter t idx p)]
|
||||
[#:NotTypeFilter
|
||||
t p (lookup: idx)
|
||||
(make-NotTypeFilter t p idx)]))
|
||||
(-filter t idx p)]))
|
||||
|
||||
(define (merge-filter-sets fs)
|
||||
(match fs
|
||||
|
|
|
@ -80,8 +80,8 @@
|
|||
(cond [(name-ref=? i k)
|
||||
(maker
|
||||
(subst-type t k o polarity)
|
||||
(append p p*)
|
||||
i*)]
|
||||
i*
|
||||
(append p p*))]
|
||||
[(index-free-in? k t) (if polarity -top -bot)]
|
||||
[else f])]))
|
||||
(match f
|
||||
|
@ -92,9 +92,9 @@
|
|||
[(Bot:) -bot]
|
||||
[(Top:) -top]
|
||||
[(TypeFilter: t p i)
|
||||
(tf-matcher t p i k o polarity make-TypeFilter)]
|
||||
(tf-matcher t p i k o polarity -filter)]
|
||||
[(NotTypeFilter: t p i)
|
||||
(tf-matcher t p i k o polarity make-NotTypeFilter)]))
|
||||
(tf-matcher t p i k o polarity -not-filter)]))
|
||||
|
||||
(define (index-free-in? k type)
|
||||
(let/ec
|
||||
|
|
|
@ -268,7 +268,15 @@
|
|||
|
||||
(d/c (-filter t i [p null])
|
||||
(c:->* (Type/c name-ref/c) ((listof PathElem?)) Filter/c)
|
||||
(make-TypeFilter t p i))
|
||||
(if (type-equal? Univ t)
|
||||
-top
|
||||
(make-TypeFilter t p i)))
|
||||
|
||||
(d/c (-not-filter t i [p null])
|
||||
(c:->* (Type/c name-ref/c) ((listof PathElem?)) Filter/c)
|
||||
(if (type-equal? (make-Union null) t)
|
||||
-top
|
||||
(make-NotTypeFilter t p i)))
|
||||
|
||||
(define (-filter-at t o)
|
||||
(match o
|
||||
|
@ -279,11 +287,6 @@
|
|||
[(Path: p i) (-not-filter t i p)]
|
||||
[_ -top]))
|
||||
|
||||
|
||||
(d/c (-not-filter t i [p null])
|
||||
(c:->* (Type/c name-ref/c) ((listof PathElem?)) Filter/c)
|
||||
(make-NotTypeFilter t p i))
|
||||
|
||||
(define (asym-pred dom rng filter)
|
||||
(make-Function (list (make-arr* (list dom) rng #:filters filter))))
|
||||
|
||||
|
|
|
@ -69,7 +69,7 @@
|
|||
[(and p (TypeFilter: t1 f1 x) (? (lambda _ or?)))
|
||||
(hash-update! tf-map
|
||||
(list f1 (hash-name-ref x))
|
||||
(match-lambda [(TypeFilter: t2 _ _) (make-TypeFilter (Un t1 t2) f1 x)]
|
||||
(match-lambda [(TypeFilter: t2 _ _) (-filter (Un t1 t2) x f1)]
|
||||
[p (int-err "got something that isn't a typefilter ~a" p)])
|
||||
p)
|
||||
(loop (cdr props) others)]
|
||||
|
@ -80,16 +80,17 @@
|
|||
(list -bot)]
|
||||
[(TypeFilter: t2 _ _)
|
||||
(hash-set! tf-map (list f1 (hash-name-ref x))
|
||||
(make-TypeFilter (restrict t1 t2) f1 x))
|
||||
(-filter (restrict t1 t2) x f1))
|
||||
(loop (cdr props) others)]
|
||||
[#f
|
||||
(hash-set! tf-map (list f1 (hash-name-ref x))
|
||||
(make-TypeFilter t1 f1 x))
|
||||
(-filter t1 x f1))
|
||||
(loop (cdr props) others)])]
|
||||
[(and p (NotTypeFilter: t1 f1 x) (? (lambda _ (not or?))))
|
||||
(hash-update! ntf-map
|
||||
(list f1 (hash-name-ref x))
|
||||
(match-lambda [(NotTypeFilter: t2 _ _) (make-NotTypeFilter (Un t1 t2) f1 x)]
|
||||
(match-lambda [(NotTypeFilter: t2 _ _)
|
||||
(-not-filter (Un t1 t2) x f1)]
|
||||
[p (int-err "got something that isn't a nottypefilter ~a" p)])
|
||||
p)
|
||||
(loop (cdr props) others)]
|
||||
|
|
Loading…
Reference in New Issue
Block a user