From df0b694cfd7243f2b2d563ccb41c82672da5ce78 Mon Sep 17 00:00:00 2001
From: Eric Dobson <eric.n.dobson@gmail.com>
Date: Wed, 28 May 2014 21:41:44 -0700
Subject: [PATCH] Improve filter simplification.

(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
---
 .../typed-racket/types/filter-ops.rkt            | 16 ++++++++++++++--
 .../typed-racket/unit-tests/filter-tests.rkt     | 10 ++++++++++
 2 files changed, 24 insertions(+), 2 deletions(-)

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)))
   ))