diff --git a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-let-unit.rkt b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-let-unit.rkt index ccc1d990c2..294c428513 100644 --- a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-let-unit.rkt +++ b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-let-unit.rkt @@ -45,8 +45,8 @@ (for/list ([n (in-list names)] [f+ (in-list fs+)] [f- (in-list fs-)]) - (list (make-ImpFilter (-not-filter (-val #f) n) f+) - (make-ImpFilter (-filter (-val #f) n) f-)))))] + (list (-imp (-not-filter (-val #f) n) f+) + (-imp (-filter (-val #f) n) f-)))))] [((tc-results: ts (NoFilter:) _) (tc-results: e-ts (NoFilter:) _)) (values ts e-ts null)])))) (with-cond-contract append-region ([p1 (listof Filter?)] diff --git a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-subst.rkt b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-subst.rkt index 3ab2120365..52bc7575c6 100644 --- a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-subst.rkt +++ b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-subst.rkt @@ -109,7 +109,7 @@ [else f])])) (match f [(ImpFilter: ant consq) - (make-ImpFilter (subst-filter ant k o (not polarity)) (ap consq))] + (-imp (subst-filter ant k o (not polarity)) (ap consq))] [(AndFilter: fs) (apply -and (map ap fs))] [(OrFilter: fs) (apply -or (map ap fs))] [(Bot:) -bot] 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 f21204c036..c7de9b7e39 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 @@ -114,7 +114,10 @@ (define (-imp p1 p2) (match* (p1 p2) [((Bot:) _) -top] + [(_ (Top:)) -top] [((Top:) _) p2] + [((TypeFilter: t p o) (Bot:)) (-not-filter t o p)] + [((NotTypeFilter: t p o) (Bot:)) (-filter t o p)] [(_ _) (make-ImpFilter p1 p2)])) (define (-or . args) 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 533eaabebc..12910bcf26 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 @@ -2,6 +2,7 @@ (require "test-utils.rkt" rackunit racket/format + (rep filter-rep) (types abbrev union filter-ops) (for-syntax racket/base syntax/parse)) @@ -103,4 +104,17 @@ (-or (-filter -Symbol 1) (-filter -Symbol #'x)) (-filter -Symbol #'x)) ) + + (test-suite "Implication" + (check-equal? (-imp -bot (-filter -Symbol #'x)) -top) + (check-equal? (-imp -top (-filter -Symbol #'x)) (-filter -Symbol #'x)) + (check-equal? (-imp (-filter -Symbol #'x) -top) -top) + (check-equal? (-imp (-filter -Symbol #'x) -bot) (-not-filter -Symbol #'x)) + (check-equal? (-imp (-not-filter -Symbol #'x) -bot) (-filter -Symbol #'x)) + (check-equal? + (-imp (-not-filter -Symbol #'x) + (-not-filter -Symbol #'y)) + (make-ImpFilter (-not-filter -Symbol #'x) + (-not-filter -Symbol #'y)))) + ))