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

Improve filters generated for true values in tc-id and tc-let.

Browse Source
This commit is contained in:
Eric Dobson 2014-06-25 21:31:39 -07:00
parent 0c187c52b7
commit 76f9175fc3
4 changed files with 87 additions and 77 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

16
pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-expr-unit.rkt
View File

@ -5,9 +5,9 @@
racket/match (prefix-in - (contract-req)) racket/match (prefix-in - (contract-req))
"signatures.rkt" "signatures.rkt"
"check-below.rkt" "tc-app-helper.rkt" "../types/kw-types.rkt" "check-below.rkt" "tc-app-helper.rkt" "../types/kw-types.rkt"
(types utils abbrev union subtype type-table classes filter-ops) (types utils abbrev union subtype type-table classes filter-ops remove-intersect)
(private-in parse-type type-annotation syntax-properties) (private-in parse-type type-annotation syntax-properties)
(rep type-rep filter-rep object-rep) (rep type-rep filter-rep object-rep rep-utils)
(utils tc-utils) (utils tc-utils)
(env lexical-env tvar-env index-env scoped-tvar-env) (env lexical-env tvar-env index-env scoped-tvar-env)
racket/format racket/list racket/format racket/list
@ -39,11 +39,13 @@
(--> identifier? full-tc-results/c) (--> identifier? full-tc-results/c)
(define rename-id (contract-rename-id-property id)) (define rename-id (contract-rename-id-property id))
(define id* (or rename-id id)) (define id* (or rename-id id))
(let* ([ty (lookup-type/lexical id*)]) (define ty (lookup-type/lexical id*))
(ret ty (define obj (-id-path id*))
(make-FilterSet (-not-filter (-val #f) id) (ret ty
(-filter (-val #f) id)) (if (overlap ty (-val #f))
(-id-path id)))) (-FS (-not-filter (-val #f) obj) (-filter (-val #f) obj))
-true-filter)
obj))
;; typecheck an expression, but throw away the effect ;; typecheck an expression, but throw away the effect
;; tc-expr/t : Expr -> Type ;; tc-expr/t : Expr -> Type

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

@ -1,7 +1,7 @@
#lang racket/unit #lang racket/unit
(require "../utils/utils.rkt" (require "../utils/utils.rkt"
(except-in (types utils abbrev union filter-ops) -> ->* one-of/c) (except-in (types utils subtype abbrev union filter-ops remove-intersect) -> ->* one-of/c)
(only-in (types abbrev) (-> t:->) [->* t:->*]) (only-in (types abbrev) (-> t:->) [->* t:->*])
(private type-annotation parse-type syntax-properties) (private type-annotation parse-type syntax-properties)
(env lexical-env type-alias-env type-alias-helper mvar-env (env lexical-env type-alias-env type-alias-helper mvar-env
@ -52,12 +52,17 @@
(values e-ts (values e-ts
(apply append (apply append
(for/list ([n (in-list names)] (for/list ([n (in-list names)]
[t (in-list e-ts)]
[f+ (in-list fs+)] [f+ (in-list fs+)]
[f- (in-list fs-)]) [f- (in-list fs-)])
(if (is-var-mutated? n) (cond
(list) [(not (overlap t (-val #f)))
(list (-imp (-not-filter (-val #f) n) f+) (list f+)]
(-imp (-filter (-val #f) n) f-))))))] [(is-var-mutated? n)
(list)]
[else
(list (-imp (-not-filter (-val #f) n) f+)
(-imp (-filter (-val #f) n) f-))]))))]
[(list (tc-result: e-ts (NoFilter:) _) ...) [(list (tc-result: e-ts (NoFilter:) _) ...)
(values e-ts null)])))) (values e-ts null)]))))
;; extend the lexical environment for checking the body ;; extend the lexical environment for checking the body

6
pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/unit-tests/class-tests.rkt
View File

@ -929,7 +929,8 @@
#:row (make-Row null `([x ,-Integer]) null null #f)) #:row (make-Row null `([x ,-Integer]) null null #f))
(-class (-class
#:row (make-Row null `([x ,-Integer]) null null #f) #:row (make-Row null `([x ,-Integer]) null null #f)
#:field ([x -Integer]))))] #:field ([x -Integer])))
-true-filter)]
;; fails, mixin argument is missing required field ;; fails, mixin argument is missing required field
[tc-err (let () [tc-err (let ()
(: f (All (A #:row (field x)) (: f (All (A #:row (field x))
@ -999,7 +1000,8 @@
#:row (make-Row null `([x ,-Integer]) null null #f)) #:row (make-Row null `([x ,-Integer]) null null #f))
(-class (-class
#:row (make-Row null `([x ,-Integer]) null null #f) #:row (make-Row null `([x ,-Integer]) null null #f)
#:field ([x -Integer]))))] #:field ([x -Integer])))
-true-filter)]
;; Check simple use of pubment ;; Check simple use of pubment
[tc-e (let () [tc-e (let ()
(define c% (define c%

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

@ -426,13 +426,13 @@
(tc-e (real->extfl #e-1e-8192) -NonPosExtFlonum) (tc-e (real->extfl #e-1e-8192) -NonPosExtFlonum)
(tc-err (let: ([z : 10000000000000 10000000000000]) z)) ; unsafe (tc-err (let: ([z : 10000000000000 10000000000000]) z)) ; unsafe
(tc-err (let: ([z : -4611686018427387904 -4611686018427387904]) z)) ; unsafe (tc-err (let: ([z : -4611686018427387904 -4611686018427387904]) z)) ; unsafe
(tc-e (let: ([z : -4611686018427387905 -4611686018427387905]) z) (-val -4611686018427387905)) (tc-e/t (let: ([z : -4611686018427387905 -4611686018427387905]) z) (-val -4611686018427387905))
(tc-err (let: ([z : -1073741825 -1073741825]) z)) ; unsafe (tc-err (let: ([z : -1073741825 -1073741825]) z)) ; unsafe
(tc-e (let: ([z : -1073741824 -1073741824]) z) (-val -1073741824)) (tc-e/t (let: ([z : -1073741824 -1073741824]) z) (-val -1073741824))
(tc-e (let: ([z : 268435455 268435455]) z) (-val 268435455)) (tc-e/t (let: ([z : 268435455 268435455]) z) (-val 268435455))
(tc-err (let: ([z : 268435456 268435456]) z)) ; unsafe (tc-err (let: ([z : 268435456 268435456]) z)) ; unsafe
(tc-err (let: ([z : 4611686018427387903 4611686018427387903]) z)) ; unsafe (tc-err (let: ([z : 4611686018427387903 4611686018427387903]) z)) ; unsafe
(tc-e (let: ([z : 4611686018427387904 4611686018427387904]) z) (-val 4611686018427387904)) (tc-e/t (let: ([z : 4611686018427387904 4611686018427387904]) z) (-val 4611686018427387904))
[tc-e/t (lambda: () 3) (t:-> -PosByte : -true-filter)] [tc-e/t (lambda: () 3) (t:-> -PosByte : -true-filter)]
[tc-e/t (lambda: ([x : Number]) 3) (t:-> -Number -PosByte : -true-filter)] [tc-e/t (lambda: ([x : Number]) 3) (t:-> -Number -PosByte : -true-filter)]
@ -475,7 +475,7 @@
(make-Poly '(a) (t:-> (make-Listof (-v a)) (-v a)))] (make-Poly '(a) (t:-> (make-Listof (-v a)) (-v a)))]
[tc-e/t (case-lambda: [([a : Number] [b : Number]) (+ a b)]) (t:-> -Number -Number -Number)] [tc-e/t (case-lambda: [([a : Number] [b : Number]) (+ a b)]) (t:-> -Number -Number -Number)]
[tc-e/t (tr:case-lambda [([a : Number] [b : Number]) (+ a b)]) (t:-> -Number -Number -Number)] [tc-e/t (tr:case-lambda [([a : Number] [b : Number]) (+ a b)]) (t:-> -Number -Number -Number)]
[tc-e (let: ([x : Number 5]) x) -Number] [tc-e/t (let: ([x : Number 5]) x) -Number]
[tc-e (let-values ([(x) 4]) (+ x 1)) -PosIndex] [tc-e (let-values ([(x) 4]) (+ x 1)) -PosIndex]
[tc-e (let-values ([(x y) (values 3 #t)]) (and (= x 1) (not y))) [tc-e (let-values ([(x y) (values 3 #t)]) (and (= x 1) (not y)))
#:ret (ret -Boolean -false-filter)] #:ret (ret -Boolean -false-filter)]
@ -657,7 +657,7 @@
-Number] -Number]
[tc-e null #:ret (-path -Null #'null)] [tc-e null #:ret (ret (-val null) -true-filter (-id-path #'null))]
[tc-e/t (let* ([sym 'squarf] [tc-e/t (let* ([sym 'squarf]
[x (if (= 1 2) 3 sym)]) [x (if (= 1 2) 3 sym)])
@ -668,24 +668,24 @@
;; eq? as predicate ;; eq? as predicate
[tc-e (let: ([x : (Un 'foo Number) 'foo]) [tc-e/t (let: ([x : (Un 'foo Number) 'foo])
(if (eq? x 'foo) 3 x)) (if (eq? x 'foo) 3 x))
-Number] -Number]
[tc-e (let: ([x : (Un 'foo Number) 'foo]) [tc-e/t (let: ([x : (Un 'foo Number) 'foo])
(if (eq? 'foo x) 3 x)) (if (eq? 'foo x) 3 x))
-Number] -Number]
[tc-err (let: ([x : (U String 'foo) 'foo]) [tc-err (let: ([x : (U String 'foo) 'foo])
(if (string=? x 'foo) (if (string=? x 'foo)
"foo" "foo"
x)) x))
#:ret (ret (t:Un -String (-val 'foo)))] #:ret (ret (t:Un -String (-val 'foo)) -true-filter)]
[tc-e (let: ([x : (U String 5) 5]) [tc-e/t (let: ([x : (U String 5) 5])
(if (eq? x 5) (if (eq? x 5)
"foo" "foo"
x)) x))
(t:Un -String (-val 5))] (t:Un -String (-val 5))]
[tc-e (let* ([sym 'squarf] [tc-e (let* ([sym 'squarf]
[x (if (= 1 2) 3 sym)]) [x (if (= 1 2) 3 sym)])
@ -696,12 +696,12 @@
(if (eq? sym x) 3 x)) (if (eq? sym x) 3 x))
#:ret (ret -PosByte -true-filter)] #:ret (ret -PosByte -true-filter)]
;; equal? as predicate for symbols ;; equal? as predicate for symbols
[tc-e (let: ([x : (Un 'foo Number) 'foo]) [tc-e/t (let: ([x : (Un 'foo Number) 'foo])
(if (equal? x 'foo) 3 x)) (if (equal? x 'foo) 3 x))
-Number] -Number]
[tc-e (let: ([x : (Un 'foo Number) 'foo]) [tc-e/t (let: ([x : (Un 'foo Number) 'foo])
(if (equal? 'foo x) 3 x)) (if (equal? 'foo x) 3 x))
-Number] -Number]
[tc-e (let* ([sym 'squarf] [tc-e (let* ([sym 'squarf]
[x (if (= 1 2) 3 sym)]) [x (if (= 1 2) 3 sym)])
@ -872,18 +872,18 @@
(: y Symbol) (: y Symbol)
(define y x) (define y x)
y) y)
#:ret (ret -Symbol) #:ret (ret -Symbol -true-filter)
#:msg #rx"expected: String|expected: Symbol"] #:msg #rx"expected: String|expected: Symbol"]
;; Test ill-typed code in letrec RHS ;; Test ill-typed code in letrec RHS
[tc-err (let () (: x String) (define x 'foo) x) [tc-err (let () (: x String) (define x 'foo) x)
#:ret (ret -String) #:ret (ret -String -true-filter)
#:msg #rx"expected: String.*given: 'foo"] #:msg #rx"expected: String.*given: 'foo"]
[tc-err (let ([x (add1 5)]) [tc-err (let ([x (add1 5)])
(set! x "foo") (set! x "foo")
x) x)
#:ret (ret -Integer)] #:ret (ret -Integer -true-filter)]
;; w-c-m ;; w-c-m
[tc-e/t (with-continuation-mark [tc-e/t (with-continuation-mark
((inst make-continuation-mark-key Symbol)) 'mark ((inst make-continuation-mark-key Symbol)) 'mark
@ -1047,13 +1047,13 @@
(-polydots (z x y) (t:-> (cl->* (-polydots (z x y) (t:-> (cl->*
((t:-> x z) (-pair x (-lst x)) . t:-> . (-pair z (-lst z))) ((t:-> x z) (-pair x (-lst x)) . t:-> . (-pair z (-lst z)))
((list ((list x) (y y) . ->... . z) (-lst x)) ((-lst y) y) . ->... . (-lst z))) ((list ((list x) (y y) . ->... . z) (-lst x)) ((-lst y) y) . ->... . (-lst z)))
: (-FS (-not-filter (-val #f) #'map) (-filter (-val #f) #'map)) : -true-filter
: (make-Path null #'map)))] : (-id-path #'map)))]
;; error tests ;; error tests
[tc-err (+ 3 #f)] [tc-err (+ 3 #f)]
[tc-err (let: ([x : Number #f]) x) [tc-err (let: ([x : Number #f]) x)
#:ret (ret -Number)] #:ret (ret -Number -true-filter)]
[tc-err (let: ([x : Number #f]) (+ 1 x)) [tc-err (let: ([x : Number #f]) (+ 1 x))
#:ret (ret -Number)] #:ret (ret -Number)]
@ -1243,12 +1243,12 @@
#f) #f)
#:ret (ret -Void -top-filter -empty-obj)] #:ret (ret -Void -top-filter -empty-obj)]
[tc-err (apply +)] [tc-err (apply +)]
[tc-e [tc-e/t
(let ([x eof]) (let ([x eof])
(if (procedure? x) (if (procedure? x)
x x
(lambda (z) (eq? x z)))) (lambda (z) (eq? x z))))
#:ret (ret (make-pred-ty (-val eof)) (-FS (-not-filter top-func #'eof) -bot))] (make-pred-ty (-val eof))]
[tc-e ((inst map Number (Pairof Number Number)) car (ann (list (cons 1 2) (cons 2 3) (cons 4 5)) (Listof (Pairof Number Number)))) [tc-e ((inst map Number (Pairof Number Number)) car (ann (list (cons 1 2) (cons 2 3) (cons 4 5)) (Listof (Pairof Number Number))))
(-lst -Number)] (-lst -Number)]
[tc-err (list (values 1 2)) [tc-err (list (values 1 2))
@ -2177,16 +2177,17 @@
[tc-e (touch (future (λ () "foo"))) -String] [tc-e (touch (future (λ () "foo"))) -String]
[tc-e (current-future) (-opt (-future Univ))] [tc-e (current-future) (-opt (-future Univ))]
[tc-e (add1 (processor-count)) -PosInt] [tc-e (add1 (processor-count)) -PosInt]
[tc-e/t (assert (current-future) future?) (-future Univ)] [tc-e (assert (current-future) future?)
#:ret (ret (-future Univ) -true-filter)]
[tc-e (futures-enabled?) -Boolean] [tc-e (futures-enabled?) -Boolean]
[tc-e (place-enabled?) -Boolean] [tc-e (place-enabled?) -Boolean]
[tc-e (dynamic-place "a.rkt" 'a #:at #f) -Place] [tc-e (dynamic-place "a.rkt" 'a #:at #f) -Place]
[tc-e (dynamic-place (string->path "a.rkt") 'a #:at #f) -Place] [tc-e (dynamic-place (string->path "a.rkt") 'a #:at #f) -Place]
[tc-e (let-values [tc-e/t (let-values
([(p _1 _2 _3) ([(p _1 _2 _3)
(dynamic-place* "a.rkt" 'a #:in (open-input-string "hi"))]) (dynamic-place* "a.rkt" 'a #:in (open-input-string "hi"))])
p) p)
-Place] -Place]
[tc-e (let ([p (dynamic-place "a.rkt" 'a)]) [tc-e (let ([p (dynamic-place "a.rkt" 'a)])
(place-break p) (place-break p)
(place-break p 'terminate) (place-break p 'terminate)
@ -2251,12 +2252,12 @@
(-HT -Symbol -String)] (-HT -Symbol -String)]
;; for/hash doesn't always need a return annotation inside ;; for/hash doesn't always need a return annotation inside
[tc-e (let () [tc-e/t (let ()
(tr:define h : (HashTable Any Any) (tr:define h : (HashTable Any Any)
(for/hash ([(k v) (in-hash #hash(("a" . a)))]) (for/hash ([(k v) (in-hash #hash(("a" . a)))])
(values v k))) (values v k)))
h) h)
(-HT Univ Univ)] (-HT Univ Univ)]
;; call-with-input-string and friends - PR 14050 ;; call-with-input-string and friends - PR 14050
[tc-e (call-with-input-string "abcd" (lambda: ([input : Input-Port]) (values 'a 'b))) [tc-e (call-with-input-string "abcd" (lambda: ([input : Input-Port]) (values 'a 'b)))
@ -2443,7 +2444,7 @@
-String] -String]
[tc-e (let* ([y 'y] [x : String "foo"]) (string-append x "bar")) [tc-e (let* ([y 'y] [x : String "foo"]) (string-append x "bar"))
-String] -String]
[tc-e (letrec ([x "foo"]) x) -String] [tc-e/t (letrec ([x "foo"]) x) -String]
[tc-e (letrec ([x : String "foo"]) (string-append x "bar")) [tc-e (letrec ([x : String "foo"]) (string-append x "bar"))
-String] -String]
[tc-e (letrec ([x : String "foo"] [y 'y]) (string-append x "bar")) [tc-e (letrec ([x : String "foo"] [y 'y]) (string-append x "bar"))
@ -2460,8 +2461,8 @@
[tc-e (let-values ([([x : String] [y : String]) (values "foo" "bar")]) [tc-e (let-values ([([x : String] [y : String]) (values "foo" "bar")])
(string-append x y)) (string-append x y))
-String] -String]
[tc-e (letrec-values ([(x y) (values "foo" "bar")]) x) [tc-e/t (letrec-values ([(x y) (values "foo" "bar")]) x)
-String] -String]
[tc-e (letrec-values ([(x y) (values "foo" "bar")] [tc-e (letrec-values ([(x y) (values "foo" "bar")]
[([z : String]) (values "baz")]) [([z : String]) (values "baz")])
(string-append x y z)) (string-append x y z))
@ -2634,19 +2635,19 @@
"foo") "foo")
(foo)) (foo))
-String] -String]
[tc-e (letrec-values ([(a b) (values x y)] [tc-e/t (letrec-values ([(a b) (values x y)]
[(x y) (values "x" "y")]) [(x y) (values "x" "y")])
a) a)
-String] -String]
[tc-e (letrec-values ([(a b) (values x "b")] [tc-e/t (letrec-values ([(a b) (values x "b")]
[(x y) (values "x" "y")]) [(x y) (values "x" "y")])
a) a)
-String] -String]
[tc-e (letrec-values ([(a b) (values "a" "b")] [tc-e/t (letrec-values ([(a b) (values "a" "b")]
[(x y) (values z z)] [(x y) (values z z)]
[(z) a]) [(z) a])
z) z)
-String] -String]
[tc-err (letrec-values ([(a b) (values x "b")] [tc-err (letrec-values ([(a b) (values x "b")]
[(x y) (values a b)]) [(x y) (values a b)])
a) a)
@ -2913,7 +2914,7 @@
(apply f (first xs) xs))) (apply f (first xs) xs)))
(-polydots (a b) (t:-> (make-ListDots a 'b) -Void))] (-polydots (a b) (t:-> (make-ListDots a 'b) -Void))]
[tc-e [tc-e/t
(let () (let ()
(: a Symbol) (: a Symbol)
(define a b) (define a b)
@ -3000,7 +3001,7 @@
[tc-e [tc-e
((letrec ([lp (lambda (x) lp)]) lp) 'y) ((letrec ([lp (lambda (x) lp)]) lp) 'y)
#:ret (ret (t:-> -Symbol Univ)) #:ret (ret (t:-> -Symbol Univ) -true-filter)
#:expected (ret (t:-> -Symbol Univ) -no-filter -no-obj)] #:expected (ret (t:-> -Symbol Univ) -no-filter -no-obj)]
[tc-e [tc-e
@ -3120,7 +3121,7 @@
(: y String) (: y String)
(define y (for/fold: ((x : String null)) ((v : String null)) x)) (define y (for/fold: ((x : String null)) ((v : String null)) x))
y) y)
#:ret (ret -String) #:ret (ret -String -true-filter)
#:msg #rx"expected: String.*given: (Null|'\\(\\))"] #:msg #rx"expected: String.*given: (Null|'\\(\\))"]
) )