From 08b2e5c7f908a2ced242251c5d08c149b8a1db2e Mon Sep 17 00:00:00 2001 From: Eric Dobson Date: Wed, 12 Mar 2014 21:31:41 -0700 Subject: [PATCH] Split opposite? into complementary? and contradictory? original commit: 3313b820bb6ab98551ce134c21c2e1fc53008bf9 --- .../typecheck/tc-metafunctions.rkt | 4 +- .../typed-racket/types/filter-ops.rkt | 33 ++++++---- .../typed-racket/unit-tests/filter-tests.rkt | 64 ++++++++++++------- 3 files changed, 64 insertions(+), 37 deletions(-) diff --git a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-metafunctions.rkt b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-metafunctions.rkt index 85857bb6..9037f618 100644 --- a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-metafunctions.rkt +++ b/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)) 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 3225fba5..27aa10f8 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 @@ -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) - (NotTypeFilter: t2 p1 i2)) - (and (name-ref=? i1 i2) - (subtype t1 t2))] - [((NotTypeFilter: t2 p1 i2) - (TypeFilter: t1 p1 i1)) - (and (name-ref=? i1 i2) - (subtype t1 t2))] - [(_ _) #f])) + [((TypeFilter: t1 p1 i1) (NotTypeFilter: t2 p1 i2)) + (and (name-ref=? i1 i2) (subtype t1 t2))] + [((NotTypeFilter: t2 p1 i2) (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)]) 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 5836ab74..f9143e0a 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 @@ -1,38 +1,59 @@ #lang racket/base (require "test-utils.rkt" - rackunit - (types abbrev union filter-ops)) + rackunit racket/format + (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? - (-filter -Symbol 0) - (-not-filter (Un -Symbol -String) 0)) - - (check opposite? - (-not-filter -Symbol 0) - (-filter -Symbol 0)) + (test-opposite #:not-complementary #:contradictory + (-filter -Symbol 0) + (-not-filter (Un -Symbol -String) 0)) - (check not-opposite? - (-filter -Symbol 1) - (-not-filter -Symbol 0)) + (test-opposite #:complementary #:not-contradictory + (-filter (Un -Symbol -String) 0) + (-not-filter -Symbol 0)) - (check not-opposite? - (-filter -String 0) - (-not-filter -Symbol 0)) + (test-opposite #:complementary #:contradictory + (-not-filter -Symbol 0) + (-filter -Symbol 0)) - (check not-opposite? - (-not-filter -Symbol 0) - (-filter -String 0)) - ) + (test-opposite #:not-complementary #:not-contradictory + (-filter -Symbol 1) + (-not-filter -Symbol 0)) + + (test-opposite #:not-complementary #:not-contradictory + (-not-filter -Symbol 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)) - ) - + ) ))