Split opposite? into complementary? and contradictory?

pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-metafunctions.rkt

@@ -190,7 +190,7 @@
          (if (null? ps)
              (apply -and result)
              (let ([p (car ps)])
-               (cond [(opposite? a p) -bot]
+               (cond [(contradictory? a p) -bot]
                      [(implied-atomic? p a) (loop (cdr ps) result)]
                      [else (loop (cdr ps) (cons p result))]))))]
       [_ prop])))
@@ -229,7 +229,7 @@
                       (cond
                         [(null? ps) (apply -or result)]
                         [(for/or ([other-p (in-list (append derived-props derived-atoms))])
-                             (opposite? (car ps) other-p))
+                             (complementary? (car ps) other-p))
                          (or-loop (cdr ps) result)]
                         [(for/or ([other-p (in-list derived-atoms)])
                              (implied-atomic? (car ps) other-p))

pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/types/filter-ops.rkt

@@ -15,18 +15,25 @@
   (or (TypeFilter? p) (NotTypeFilter? p)
       (Top? p) (Bot? p)))
 
-(define (opposite? f1 f2)
+;; contradictory: Filter/c Filter/c -> boolean?
+;; Returns true if the AND of the two filters is equivalent to Bot
+(define (contradictory? f1 f2)
   (match* (f1 f2)
-          [((TypeFilter: t1 p1 i1)
+    [((TypeFilter: t1 p1 i1) (NotTypeFilter: t2 p1 i2))
-            (NotTypeFilter: t2 p1 i2))
+     (and (name-ref=? i1 i2) (subtype t1 t2))]
-           (and (name-ref=? i1 i2)
+    [((NotTypeFilter: t2 p1 i2) (TypeFilter: t1 p1 i1))
-                (subtype t1 t2))]
+     (and (name-ref=? i1 i2) (subtype t1 t2))]
-          [((NotTypeFilter: t2 p1 i2)
+    [(_ _) #f]))
-            (TypeFilter: t1 p1 i1))
-           (and (name-ref=? i1 i2)
-                (subtype t1 t2))]
-          [(_ _) #f]))
 
+;; complementary: Filter/c Filter/c -> boolean?
+;; Returns true if the OR of the two filters is equivalent to Top
+(define (complementary? f1 f2)
+  (match* (f1 f2)
+    [((TypeFilter: t1 p1 i1) (NotTypeFilter: t2 p1 i2))
+     (and (name-ref=? i1 i2) (subtype t2 t1))]
+    [((NotTypeFilter: t2 p1 i2) (TypeFilter: t1 p1 i1))
+     (and (name-ref=? i1 i2) (subtype t2 t1))]
+    [(_ _) #f]))
 
 (define (name-ref=? a b)
   (or (equal? a b)
@@ -131,7 +138,7 @@
           [(Bot:) (loop (cdr fs) result)]
           [t
            (cond [(for/or ([f (in-list (append (cdr fs) result))])
-                    (opposite? f t))
+                    (complementary? f t))
                   -top]
                  [(let ([t-seq (Rep-seq t)])
                     (for/or ([f (in-list result)])
@@ -151,7 +158,7 @@
           [(list) -top]
           [(list f) f]
           ;; don't think this is useful here
-          [(list f1 f2) (if (opposite? f1 f2)
+          [(list f1 f2) (if (contradictory? f1 f2)
                             -bot
                             (if (filter-equal? f1 f2)
                                 f1
@@ -172,7 +179,7 @@
           [(AndFilter: fs*) (loop (cdr fs) (append fs* result))]
           [(Top:) (loop (cdr fs) result)]
           [t (cond [(for/or ([f (in-list (append (cdr fs) result))])
-                      (opposite? f t))
+                      (contradictory? f t))
                     -bot]
                    [(let ([t-seq (Rep-seq t)])
                       (for/or ([f (in-list result)])

pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/unit-tests/filter-tests.rkt

@@ -1,38 +1,59 @@
 #lang racket/base
 
 (require "test-utils.rkt"
-         rackunit 
+         rackunit racket/format
-         (types abbrev union filter-ops))
+         (types abbrev union filter-ops)
+         (for-syntax racket/base syntax/parse))
 
 (provide tests)
 (gen-test-main)
 
-(define (not-opposite? x y) (not (opposite? x y)))
 (define (not-implied-atomic? x y) (not (implied-atomic? x y)))
 
+(define-syntax (test-opposite stx)
+  (define-syntax-class complementary
+     (pattern #:complementary #:with check #'check-true)
+     (pattern #:not-complementary #:with check #'check-false))
+  (define-syntax-class contradictory
+     (pattern #:contradictory #:with check #'check-true)
+     (pattern #:not-contradictory #:with check #'check-false))
+  (syntax-parse stx
+    [(_ comp:complementary contr:contradictory f1* f2*)
+     (syntax/loc stx
+       (test-case (~a '(opposite f1* f2*))
+         (define f1 f1*)
+         (define f2 f2*)
+         (comp.check (complementary? f1 f2) "Complementary")
+         (contr.check (contradictory? f1 f2) "Contradictory")))]))
+
+
 (define tests
   (test-suite "Filters"
     (test-suite "Opposite"
-      (check opposite?
+      (test-opposite #:not-complementary #:contradictory
-             (-filter -Symbol 0)
+        (-filter -Symbol 0)
-             (-not-filter (Un -Symbol -String) 0))
+        (-not-filter (Un -Symbol -String) 0))
 
-      (check opposite?
+      (test-opposite #:complementary #:not-contradictory
-             (-not-filter -Symbol 0)
+        (-filter (Un -Symbol -String) 0)
-             (-filter -Symbol 0))
+        (-not-filter -Symbol 0))
 
-      (check not-opposite?
+      (test-opposite #:complementary #:contradictory
-             (-filter -Symbol 1)
+        (-not-filter -Symbol 0)
-             (-not-filter -Symbol 0))
+        (-filter -Symbol 0))
 
-      (check not-opposite?
+      (test-opposite #:not-complementary #:not-contradictory
-             (-filter -String 0)
+        (-filter -Symbol 1)
-             (-not-filter -Symbol 0))
+        (-not-filter -Symbol 0))
 
-      (check not-opposite?
+      (test-opposite #:not-complementary #:not-contradictory
-             (-not-filter -Symbol 0)
+        (-not-filter -Symbol 0)
-             (-filter -String 0))
+        (-filter -String 0))
-      )
+
+      (test-opposite #:not-complementary #:not-contradictory
+        (-not-filter -Symbol 0)
+        (-filter -String 0))
+    )
 
     (test-suite "Implied Atomic"
       (check implied-atomic?
@@ -68,6 +89,5 @@
       (check implied-atomic?
              (-or (-filter -Symbol 1) (-filter -Symbol #'x))
              (-filter -Symbol #'x))
-      )
+    )
-
   ))