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

Improve filter simplification.

Browse Source 
(T @ x) => (! S @ x) when their intersection is empty.
Rearrange how we look through filters in -and so this rule applies more.

original commit: 5fa263b232c03b050e724185179e159c3f00685d
This commit is contained in:
Eric Dobson 2014-05-28 21:41:44 -07:00
parent 4e4fc660c7
commit df0b694cfd
2 changed files with 24 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

16
pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/types/filter-ops.rkt
View File

@ -62,6 +62,10 @@
(NotTypeFilter: t1 p1 i1))
(and (name-ref=? i1 i2)
(subtype t2 t1))]
[((NotTypeFilter: t1 p1 i1)
(TypeFilter: t2 p1 i2))
(and (name-ref=? i1 i2)
(not (overlap t1 t2)))]
[(_ _) #f]))
(define (hash-name-ref i)
@ -173,7 +177,16 @@
(case-lambda [() -top]
[(f) f]
[fs (make-AndFilter fs)]))
(let loop ([fs (remove-duplicates args eq? #:key Rep-seq)] [result null])
(define (flatten-ands fs)
(let loop ([fs fs] [results null])
(match fs
[(list) results]
[(cons (AndFilter: fs*) fs) (loop fs (append fs* results))]
[(cons f fs) (loop fs (cons f results))])))
;; Move all the type filters up front as they are the stronger props
(define-values (f-args other-args)
(partition TypeFilter? (flatten-ands (remove-duplicates args eq? #:key Rep-seq))))
(let loop ([fs (append f-args other-args)] [result null])
(if (null? fs)
(match result
[(list) -top]
@ -197,7 +210,6 @@
(apply mk (compact (append not-atomic* atomic) #f)))])
(match (car fs)
[(and t (Bot:)) t]
[(AndFilter: fs*) (loop (cdr fs) (append fs* result))]
[(Top:) (loop (cdr fs) result)]
[t (cond [(for/or ([f (in-list (append (cdr fs) result))])
(contradictory? f t))

10
pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/unit-tests/filter-tests.rkt
View File

@ -106,6 +106,9 @@
(check implied-atomic?
(-filter -Symbol #'x)
(-and (-filter -Symbol 1) (-filter -Symbol #'x)))
(check implied-atomic?
(-not-filter (-val #f) #'x)
(-filter -Symbol #'x))
)
(test-suite "Implication"
@ -122,4 +125,11 @@
(make-ImpFilter (-not-filter -Symbol #'x)
(-not-filter -Symbol #'y))))
(test-suite "Simplification"
(check-equal?
(-and (-filter -Symbol #'x) (-not-filter (-val #f) #'x))
(-filter -Symbol #'x))
(check-equal?
(-and (-not-filter (-val #f) #'x) (-filter -Symbol #'x))
(-filter -Symbol #'x)))
))