diff --git a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/types/filter-ops.rkt b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/types/filter-ops.rkt index e5497051..9be9845e 100644 --- a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/types/filter-ops.rkt +++ b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/types/filter-ops.rkt @@ -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)) diff --git a/pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/unit-tests/filter-tests.rkt b/pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/unit-tests/filter-tests.rkt index 57fdabb7..4772e780 100644 --- a/pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/unit-tests/filter-tests.rkt +++ b/pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/unit-tests/filter-tests.rkt @@ -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))) ))