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

Strengthen simplification of filters in tc-subst.

Browse Source 
original commit: c2e706277bd09e5c328fd598fcc67e179041ec83
This commit is contained in:
Eric Dobson 2014-06-25 20:40:03 -07:00
parent 4290c9bd2f
commit d035fd0f3e
2 changed files with 11 additions and 9 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -61,11 +61,13 @@
;; This is essentially ψ+|ψ- [o/x] from the paper
(define/cond-contract (subst-filter-set fs k o polarity [t Univ])
(->* ((or/c FilterSet? NoFilter?) name-ref/c Object? boolean?) (Type/c) FilterSet?)
(define extra-filter (-filter t k))
(define (add-extra-filter f)
(define f* (-and (-filter t k) f))
(match f*
[(Bot:) f*]
[_ f]))
(define f* (-and f extra-filter))
(cond
[(filter-equal? f* extra-filter) -top]
[(Bot? f*) -bot]
[else f]))
(match fs
[(FilterSet: f+ f-)
(-FS (subst-filter (add-extra-filter f+) k o polarity)

10
pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/unit-tests/typecheck-tests.rkt
View File

@ -573,7 +573,7 @@
[tc-e/t (let ([x 1]) x) -One]
[tc-e (let ([x 1]) (boolean? x)) #:ret (ret -Boolean -false-filter)]
[tc-e (boolean? number?) #:ret (ret -Boolean (-FS -bot (-not-filter -Boolean #'number?)))]
[tc-e (boolean? number?) #:ret (ret -Boolean -false-filter)]
[tc-e (let: ([x : (Option Number) #f]) x) (t:Un -Number (-val #f))]
[tc-e (let: ([x : Any 12]) (not (not x))) -Boolean]
@ -917,7 +917,7 @@
#:ret (ret -Number)]
[tc-err (call-with-values 5
(lambda: ([x : Number] [y : Number]) (+ x y)))
#:ret (ret -Number -bot-filter)]
#:ret (ret -Number)]
[tc-err (call-with-values (lambda () (values 2))
5)]
[tc-err (call-with-values (lambda () (values 2 1))
@ -1360,7 +1360,7 @@
;(tc-e (false? #t) #:ret (ret -Boolean -false-filter))
(tc-e (boolean? true) #:ret (ret -Boolean (-FS (-filter -Boolean #'true) -bot)))
(tc-e (boolean? true) #:ret (ret -Boolean -true-filter))
(tc-e (boolean? 6) #:ret (ret -Boolean -false-filter))
(tc-e (immutable? (cons 3 4)) -Boolean)
@ -1533,12 +1533,12 @@
(tc-e (namespace-anchor? 3) #:ret (ret -Boolean -false-filter))
(tc-e/t (lambda: ((x : Namespace-Anchor)) (namespace-anchor? x))
(t:-> -Namespace-Anchor -Boolean : (-FS (-filter -Namespace-Anchor 0) -bot)))
(t:-> -Namespace-Anchor -Boolean : -true-filter))
(tc-e (variable-reference? 3) #:ret (ret -Boolean -false-filter))
(tc-e/t (lambda: ((x : Variable-Reference)) (variable-reference? x))
(t:-> -Variable-Reference -Boolean : (-FS (-filter -Variable-Reference 0) -bot)))
(t:-> -Variable-Reference -Boolean : -true-filter))
(tc-e (system-type 'os) (one-of/c 'unix 'windows 'macosx))
(tc-e (system-type 'gc) (one-of/c 'cgc '3m))