suzanne.soy/racket
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

Make -imp simplify more, and use it in more places.

Browse Source 
Also add filter tests for implication.
This commit is contained in:
Eric Dobson 2014-03-24 22:08:42 -07:00
parent fcedc4ab59
commit 049057edd9
4 changed files with 20 additions and 3 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-let-unit.rkt
View File

@ -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?)]

2
pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-subst.rkt
View File

@ -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]

3
pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/types/filter-ops.rkt
View File

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

14
pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/unit-tests/filter-tests.rkt
View File

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