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

Split opposite? into complementary? and contradictory?

Browse Source 
original commit: 3313b820bb6ab98551ce134c21c2e1fc53008bf9
This commit is contained in:
Eric Dobson 2014-03-12 21:31:41 -07:00
parent e881466654
commit 08b2e5c7f9
3 changed files with 64 additions and 37 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-metafunctions.rkt
View File

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

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

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

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

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