From 1334e8dcc77854ac826306d3f6a36150cb0bf0c1 Mon Sep 17 00:00:00 2001 From: Eric Dobson Date: Tue, 19 Feb 2013 00:12:57 -0800 Subject: [PATCH] Reduce usage of check-below. This pushes almost all uses of check below into tc-expr and tc-expr/check. This means that the optimizer sees more precise types and can make more optimizations. --- .../optimizer/missed-optimizations/fixnum.rkt | 2 +- .../optimizer/missed-optimizations/pair.rkt | 16 +- .../missed-optimizations/precision-loss.rkt | 26 +- .../optimizer/tests/annotations.rkt | 18 + .../optimizer/tests/vector-length.rkt | 7 +- .../typecheck/tc-app/tc-app-apply.rkt | 2 +- .../typecheck/tc-app/tc-app-eq.rkt | 2 +- .../typecheck/tc-app/tc-app-hetero.rkt | 18 +- .../typecheck/tc-app/tc-app-list.rkt | 4 +- .../typecheck/tc-app/tc-app-main.rkt | 6 +- .../typecheck/tc-app/tc-app-objects.rkt | 2 +- .../typecheck/tc-app/tc-app-special.rkt | 8 +- .../typecheck/tc-app/tc-app-values.rkt | 2 +- .../typed-racket/typecheck/tc-expr-unit.rkt | 455 +++++++++--------- collects/typed-racket/typecheck/tc-if.rkt | 43 +- .../typed-racket/typecheck/tc-lambda-unit.rkt | 10 +- .../typed-racket/typecheck/tc-let-unit.rkt | 10 +- 17 files changed, 317 insertions(+), 314 deletions(-) create mode 100644 collects/tests/typed-racket/optimizer/tests/annotations.rkt diff --git a/collects/tests/typed-racket/optimizer/missed-optimizations/fixnum.rkt b/collects/tests/typed-racket/optimizer/missed-optimizations/fixnum.rkt index b0bf6a91b5..d6cff2200b 100644 --- a/collects/tests/typed-racket/optimizer/missed-optimizations/fixnum.rkt +++ b/collects/tests/typed-racket/optimizer/missed-optimizations/fixnum.rkt @@ -37,7 +37,7 @@ TR opt: fixnum.rkt 43:17 (+ 301 302) -- fixnum bounded expr ;; this should not, (+ Fixnum Byte), but it may look like it should (+ (ann z Fixnum) 234) (* (ann x Index) (ann y Index)) -(fx* (ann x Index) (ann y Index)) ; not reported, by design +(fx* (values (ann x Index)) (values (ann y Index))) ; not reported, by design (abs (ann -3 Fixnum)) (+ (+ 300 301) (+ 301 302)) (fx+ (+ 300 301) (+ 301 302)) ; not reported, by design diff --git a/collects/tests/typed-racket/optimizer/missed-optimizations/pair.rkt b/collects/tests/typed-racket/optimizer/missed-optimizations/pair.rkt index 779c2678ca..884bae6718 100644 --- a/collects/tests/typed-racket/optimizer/missed-optimizations/pair.rkt +++ b/collects/tests/typed-racket/optimizer/missed-optimizations/pair.rkt @@ -13,18 +13,18 @@ TR missed opt: pair.rkt 64:16 (cdr (cdr (cdr (cdr (list 1 2 3))))) -- car/cdr on TR opt: pair.rkt 64:21 (cdr (cdr (cdr (list 1 2 3)))) -- pair TR opt: pair.rkt 64:26 (cdr (cdr (list 1 2 3))) -- pair TR opt: pair.rkt 64:31 (cdr (list 1 2 3)) -- pair -TR missed opt: pair.rkt 67:0 (mcar (ann (mlist 1) (MListof Byte))) -- car/cdr on a potentially empty list -- caused by: 67:0 (mcar (ann (mlist 1) (MListof Byte))) +TR missed opt: pair.rkt 67:0 (mcar (values (ann (mlist 1) (MListof Byte)))) -- car/cdr on a potentially empty list -- caused by: 67:6 (values (ann (mlist 1) (MListof Byte))) TR opt: pair.rkt 68:0 (mcar (mlist 1 2 3)) -- pair -TR missed opt: pair.rkt 69:0 (mcdr (ann (mlist 1) (MListof Byte))) -- car/cdr on a potentially empty list -- caused by: 69:0 (mcdr (ann (mlist 1) (MListof Byte))) +TR missed opt: pair.rkt 69:0 (mcdr (values (ann (mlist 1) (MListof Byte)))) -- car/cdr on a potentially empty list -- caused by: 69:6 (values (ann (mlist 1) (MListof Byte))) TR opt: pair.rkt 70:0 (mcdr (mlist 1 2 3)) -- pair TR opt: pair.rkt 71:0 (mcdr (mcdr (mlist 1 2 3))) -- pair TR opt: pair.rkt 71:6 (mcdr (mlist 1 2 3)) -- pair TR opt: pair.rkt 72:0 (mcdr (mcdr (mcdr (mlist 1 2 3)))) -- pair TR opt: pair.rkt 72:6 (mcdr (mcdr (mlist 1 2 3))) -- pair TR opt: pair.rkt 72:12 (mcdr (mlist 1 2 3)) -- pair -TR missed opt: pair.rkt 73:0 (set-mcar! (ann (mlist 2) (MListof Byte)) 2) -- car/cdr on a potentially empty list -- caused by: 73:0 (set-mcar! (ann (mlist 2) (MListof Byte)) 2) +TR missed opt: pair.rkt 73:0 (set-mcar! (values (ann (mlist 2) (MListof Byte))) 2) -- car/cdr on a potentially empty list -- caused by: 73:11 (values (ann (mlist 2) (MListof Byte))) TR opt: pair.rkt 74:0 (set-mcar! (mlist 2 3 4) 2) -- pair -TR missed opt: pair.rkt 75:0 (set-mcdr! (ann (mlist 2) (MListof Byte)) (ann (mlist 2) (MListof Byte))) -- car/cdr on a potentially empty list -- caused by: 75:0 (set-mcdr! (ann (mlist 2) (MListof Byte)) (ann (mlist 2) (MListof Byte))) +TR missed opt: pair.rkt 75:0 (set-mcdr! (values (ann (mlist 2) (MListof Byte))) (values (ann (mlist 2) (MListof Byte)))) -- car/cdr on a potentially empty list -- caused by: 75:11 (values (ann (mlist 2) (MListof Byte))) TR opt: pair.rkt 77:0 (mcar (mcons 2 3)) -- pair TR opt: pair.rkt 78:0 (mcdr (mcons 2 3)) -- pair TR opt: pair.rkt 79:0 (set-mcar! (mcons 2 3) 3) -- pair @@ -64,15 +64,15 @@ TR missed opt: pair.rkt 84:17 (set-mcdr! (ann (quote ()) (MListof Integer)) (ann (define (dummy) (cdr (cdr (cdr (cdr (list 1 2 3)))))) ; unsafe, so missed opt ;; similar for mpairs -(mcar (ann (mlist 1) (MListof Byte))) +(mcar (values (ann (mlist 1) (MListof Byte)))) (mcar (mlist 1 2 3)) -(mcdr (ann (mlist 1) (MListof Byte))) +(mcdr (values (ann (mlist 1) (MListof Byte)))) (mcdr (mlist 1 2 3)) (mcdr (mcdr (mlist 1 2 3))) (mcdr (mcdr (mcdr (mlist 1 2 3)))) -(set-mcar! (ann (mlist 2) (MListof Byte)) 2) +(set-mcar! (values (ann (mlist 2) (MListof Byte))) 2) (set-mcar! (mlist 2 3 4) 2) -(set-mcdr! (ann (mlist 2) (MListof Byte)) (ann (mlist 2) (MListof Byte))) +(set-mcdr! (values (ann (mlist 2) (MListof Byte))) (values (ann (mlist 2) (MListof Byte)))) (mcar (mcons 2 3)) (mcdr (mcons 2 3)) diff --git a/collects/tests/typed-racket/optimizer/missed-optimizations/precision-loss.rkt b/collects/tests/typed-racket/optimizer/missed-optimizations/precision-loss.rkt index 5d02a359fc..3ec8e63f57 100644 --- a/collects/tests/typed-racket/optimizer/missed-optimizations/precision-loss.rkt +++ b/collects/tests/typed-racket/optimizer/missed-optimizations/precision-loss.rkt @@ -10,15 +10,15 @@ TR opt: precision-loss.rkt 40:0 (+ (- 3/4) 2.0) -- binary float TR info: precision-loss.rkt 42:39 (+ 1/4 3/4) -- exact real arith TR missed opt: precision-loss.rkt 42:0 (+ (vector-ref (quote #(2/3 1/2 3/4)) (assert (+ 1/4 3/4) exact-integer?)) 2.0) -- all args float-arg-expr, result not Float -- caused by: 42:3 (vector-ref (quote #(2/3 1/2 3/4)) (assert (+ 1/4 3/4) exact-integer?)) TR info: precision-loss.rkt 42:39 (+ 1/4 3/4) -- exact real arith -TR missed opt: precision-loss.rkt 48:8 (* 3/4 2/3) -- all args float-arg-expr, result not Float -- caused by: 48:11 3/4, 48:15 2/3 -TR info: precision-loss.rkt 48:8 (* 3/4 2/3) -- exact real arith -TR opt: precision-loss.rkt 49:3 (car (list (* 2.0 (ann (* 3/4 2/3) Real)))) -- pair -TR missed opt: precision-loss.rkt 49:26 (* 3/4 2/3) -- all args float-arg-expr, result not Float -- caused by: 49:29 3/4, 49:33 2/3 -TR info: precision-loss.rkt 49:26 (* 3/4 2/3) -- exact real arith -TR missed opt: precision-loss.rkt 49:14 (* 2.0 (ann (* 3/4 2/3) Real)) -- all args float-arg-expr, result not Float -- caused by: 49:26 (* 3/4 2/3) -TR info: precision-loss.rkt 49:14 (* 2.0 (ann (* 3/4 2/3) Real)) -- exact real arith -TR missed opt: precision-loss.rkt 48:0 (* (ann (* 3/4 2/3) Real) (car (list (* 2.0 (ann (* 3/4 2/3) Real)))) 2.0) -- all args float-arg-expr, result not Float -- caused by: 48:8 (* 3/4 2/3), 49:3 (car (list (* 2.0 (ann (* 3/4 2/3) Real)))) -TR info: precision-loss.rkt 48:0 (* (ann (* 3/4 2/3) Real) (car (list (* 2.0 (ann (* 3/4 2/3) Real)))) 2.0) -- exact real arith +TR missed opt: precision-loss.rkt 48:3 (* (r 3/4) 2/3) -- all args float-arg-expr, result not Float -- caused by: 48:6 (r 3/4), 48:14 2/3 +TR info: precision-loss.rkt 48:3 (* (r 3/4) 2/3) -- exact real arith +TR opt: precision-loss.rkt 49:3 (car (list (* 2.0 (* (r 3/4) 2/3)))) -- pair +TR missed opt: precision-loss.rkt 49:21 (* (r 3/4) 2/3) -- all args float-arg-expr, result not Float -- caused by: 49:24 (r 3/4), 49:32 2/3 +TR info: precision-loss.rkt 49:21 (* (r 3/4) 2/3) -- exact real arith +TR missed opt: precision-loss.rkt 49:14 (* 2.0 (* (r 3/4) 2/3)) -- all args float-arg-expr, result not Float -- caused by: 49:21 (* (r 3/4) 2/3) +TR info: precision-loss.rkt 49:14 (* 2.0 (* (r 3/4) 2/3)) -- exact real arith +TR missed opt: precision-loss.rkt 48:0 (* (* (r 3/4) 2/3) (car (list (* 2.0 (* (r 3/4) 2/3)))) 2.0) -- all args float-arg-expr, result not Float -- caused by: 48:3 (* (r 3/4) 2/3), 49:3 (car (list (* 2.0 (* (r 3/4) 2/3)))) +TR info: precision-loss.rkt 48:0 (* (* (r 3/4) 2/3) (car (list (* 2.0 (* (r 3/4) 2/3)))) 2.0) -- exact real arith 2.5 2.75 1.25 @@ -27,9 +27,9 @@ TR info: precision-loss.rkt 48:0 (* (ann (* 3/4 2/3) Real) (car (list (* 2.0 (an ) - #lang typed/racket - +(: r (Real -> Real)) +(define (r x) x) ;; warn when the extra precision gained by doing exact computations would ;; be lost when the results are mixed with floats, resulting in extra ;; computation cost for (usually) no gain @@ -45,6 +45,6 @@ TR info: precision-loss.rkt 48:0 (* (ann (* 3/4 2/3) Real) (car (list (* 2.0 (an ;; in this case, the return type is Real, so we can't optimize ;; however, given that the return _value_ will be a float, the precision ;; is thrown away nonetheless, so a warning is warranted -(* (ann (* 3/4 2/3) Real) - (car (list (* 2.0 (ann (* 3/4 2/3) Real)))) +(* (* (r 3/4) 2/3) + (car (list (* 2.0 (* (r 3/4) 2/3)))) 2.0) diff --git a/collects/tests/typed-racket/optimizer/tests/annotations.rkt b/collects/tests/typed-racket/optimizer/tests/annotations.rkt new file mode 100644 index 0000000000..ea5060ff9c --- /dev/null +++ b/collects/tests/typed-racket/optimizer/tests/annotations.rkt @@ -0,0 +1,18 @@ +#; +( +TR opt: annotations.rkt 10:10 (+ 1.0 2.0) -- binary float +TR opt: annotations.rkt 13:10 (+ 1.0 2.0) -- binary float +TR opt: annotations.rkt 16:10 (+ 1.0 2.0) -- binary float +TR opt: annotations.rkt 18:15 (+ 1.0 2.0) -- binary float +) +#lang typed/racket #:optimize + +(define a (+ 1.0 2.0)) + +(: b Float) +(define b (+ 1.0 2.0)) + +(: c Any) +(define c (+ 1.0 2.0)) + +(define d (ann (+ 1.0 2.0) Any)) diff --git a/collects/tests/typed-racket/optimizer/tests/vector-length.rkt b/collects/tests/typed-racket/optimizer/tests/vector-length.rkt index fb31857fa9..f523b4f8b3 100644 --- a/collects/tests/typed-racket/optimizer/tests/vector-length.rkt +++ b/collects/tests/typed-racket/optimizer/tests/vector-length.rkt @@ -1,6 +1,10 @@ #; ( -TR opt: vector-length.rkt 10:0 (vector-length (vector 1 2 3)) -- vector-length +TR opt: vector-length.rkt 14:0 (vector-length (vector 1 2 3)) -- known-length vector-length +TR opt: vector-length.rkt 15:0 (vector-length (ann (vector 4 5 6) (Vectorof Integer))) -- known-length vector-length +'#(1 2 3) +3 +'#(4 5 6) 3 ) @@ -8,3 +12,4 @@ TR opt: vector-length.rkt 10:0 (vector-length (vector 1 2 3)) -- vector-length #:optimize (vector-length (vector 1 2 3)) +(vector-length (ann (vector 4 5 6) (Vectorof Integer))) diff --git a/collects/typed-racket/typecheck/tc-app/tc-app-apply.rkt b/collects/typed-racket/typecheck/tc-app/tc-app-apply.rkt index e07744550b..25dd768c83 100644 --- a/collects/typed-racket/typecheck/tc-app/tc-app-apply.rkt +++ b/collects/typed-racket/typecheck/tc-app/tc-app-apply.rkt @@ -5,7 +5,7 @@ "utils.rkt" syntax/parse racket/match syntax/parse/experimental/reflect - (typecheck signatures tc-funapp check-below) + (typecheck signatures tc-funapp) (types abbrev utils) (rep type-rep) diff --git a/collects/typed-racket/typecheck/tc-app/tc-app-eq.rkt b/collects/typed-racket/typecheck/tc-app/tc-app-eq.rkt index 6791fd1251..55cdc85fbf 100644 --- a/collects/typed-racket/typecheck/tc-app/tc-app-eq.rkt +++ b/collects/typed-racket/typecheck/tc-app/tc-app-eq.rkt @@ -5,7 +5,7 @@ "utils.rkt" syntax/parse racket/match syntax/parse/experimental/reflect - (typecheck signatures tc-funapp check-below) + (typecheck signatures tc-funapp) (types abbrev union utils) (rep type-rep) diff --git a/collects/typed-racket/typecheck/tc-app/tc-app-hetero.rkt b/collects/typed-racket/typecheck/tc-app/tc-app-hetero.rkt index d439a0a011..7b866e9f0a 100644 --- a/collects/typed-racket/typecheck/tc-app/tc-app-hetero.rkt +++ b/collects/typed-racket/typecheck/tc-app/tc-app-hetero.rkt @@ -53,10 +53,10 @@ (define i-bound (length es-t)) (cond [(valid-index? i-val i-bound) - (cond-check-below (ret (list-ref es-t i-val)) expected)] + (ret (list-ref es-t i-val))] [(not i-val) (check-below i-t -Integer) - (cond-check-below (ret (apply Un es-t)) expected)] + (ret (apply Un es-t))] [else (index-error i-val i-bound i-e vec-t expected name)])) @@ -66,7 +66,7 @@ (cond [(valid-index? i-val i-bound) (tc-expr/check val-e (ret (list-ref es-t i-val))) - (cond-check-below (ret -Void) expected)] + (ret -Void)] [(not i-val) (single-value val-e) (tc-error/expr @@ -108,7 +108,11 @@ [v-ty (tc/app-regular #'form expected)])) (pattern (~and form ((~or vector-immutable vector) args:expr ...)) (match expected - [(tc-result1: (app resolve (Vector: t))) (tc/app-regular #'form expected)] + [(tc-result1: (app resolve (Vector: t))) + (define es (syntax->list #'(args ...))) + (for ([e (in-list es)]) + (tc-expr/check e (ret t))) + (ret (make-HeterogeneousVector (map (λ (_) t) es)))] [(tc-result1: (app resolve (HeterogeneousVector: ts))) (unless (= (length ts) (length (syntax->list #'(args ...)))) (tc-error/expr "expected vector with ~a elements, but got ~a" @@ -131,8 +135,6 @@ [_ (continue)])] ;; since vectors are mutable, if there is no expected type, we want to generalize the element type [(or #f (tc-any-results:) (tc-result1: _)) - (cond-check-below - (ret (make-HeterogeneousVector (map (lambda (x) (generalize (tc-expr/t x))) - (syntax->list #'(args ...))))) - expected)] + (ret (make-HeterogeneousVector (map (lambda (x) (generalize (tc-expr/t x))) + (syntax->list #'(args ...)))))] [_ (int-err "bad expected: ~a" expected)]))) diff --git a/collects/typed-racket/typecheck/tc-app/tc-app-list.rkt b/collects/typed-racket/typecheck/tc-app/tc-app-list.rkt index a55e31904d..5408ffbbfe 100644 --- a/collects/typed-racket/typecheck/tc-app/tc-app-list.rkt +++ b/collects/typed-racket/typecheck/tc-app/tc-app-list.rkt @@ -7,7 +7,7 @@ syntax/parse racket/match syntax/parse/experimental/reflect (only-in '#%kernel [reverse k:reverse]) - (typecheck signatures tc-funapp check-below) + (typecheck signatures tc-funapp) (types abbrev utils union substitute) (rep type-rep) (env tvar-env) @@ -99,6 +99,6 @@ [_ (match (single-value #'arg) [(tc-result1: (List: ts)) - (cond-check-below (ret (-Tuple (reverse ts))) expected)] + (ret (-Tuple (reverse ts)))] [arg-ty (tc/funapp #'reverse #'(arg) (single-value #'reverse) (list arg-ty) expected)])]))) diff --git a/collects/typed-racket/typecheck/tc-app/tc-app-main.rkt b/collects/typed-racket/typecheck/tc-app/tc-app-main.rkt index 37830865d0..3561a3ee5f 100644 --- a/collects/typed-racket/typecheck/tc-app/tc-app-main.rkt +++ b/collects/typed-racket/typecheck/tc-app/tc-app-main.rkt @@ -5,7 +5,7 @@ "utils.rkt" syntax/parse racket/match syntax/parse/experimental/reflect - (typecheck signatures check-below tc-funapp tc-app-helper) + (typecheck signatures tc-funapp tc-app-helper) (types utils abbrev) (rep type-rep filter-rep object-rep rep-utils) (for-template racket/base)) @@ -81,6 +81,4 @@ (define (tc/app form) (tc/app/internal form #f)) ;; syntax tc-results/c -> tc-results/c -(define (tc/app/check form expected) - (define t (tc/app/internal form expected)) - (check-below t expected)) +(define (tc/app/check form expected) (tc/app/internal form expected)) diff --git a/collects/typed-racket/typecheck/tc-app/tc-app-objects.rkt b/collects/typed-racket/typecheck/tc-app/tc-app-objects.rkt index d770d28ad3..2ec11ece7f 100644 --- a/collects/typed-racket/typecheck/tc-app/tc-app-objects.rkt +++ b/collects/typed-racket/typecheck/tc-app/tc-app-objects.rkt @@ -5,7 +5,7 @@ "utils.rkt" syntax/parse racket/match unstable/sequence syntax/parse/experimental/reflect - (typecheck signatures tc-funapp check-below) + (typecheck signatures tc-funapp) (types abbrev union utils) (rep type-rep) (utils tc-utils) diff --git a/collects/typed-racket/typecheck/tc-app/tc-app-special.rkt b/collects/typed-racket/typecheck/tc-app/tc-app-special.rkt index ceb5424933..35c8e31483 100644 --- a/collects/typed-racket/typecheck/tc-app/tc-app-special.rkt +++ b/collects/typed-racket/typecheck/tc-app/tc-app-special.rkt @@ -6,7 +6,7 @@ syntax/parse racket/match syntax/parse/experimental/reflect unstable/list - (typecheck signatures tc-funapp check-below) + (typecheck signatures tc-funapp) (types abbrev utils) (private type-annotation) (rep type-rep filter-rep) @@ -32,13 +32,13 @@ (if (null? args) (ret Univ) (let* ([p (car args)] [pt (single-value p)] - [v (cadr args)] - [vt (single-value v)]) + [v (cadr args)]) (match pt [(tc-result1: (Param: a b)) - (check-below vt a) + (tc-expr/check v (ret a)) (loop (cddr args))] [(tc-result1: t) + (single-value v) (tc-error/expr #:return (or expected (ret Univ)) "expected Parameter, but got ~a" t) (loop (cddr args))]))))) ;; use the additional but normally ignored first argument to make-sequence diff --git a/collects/typed-racket/typecheck/tc-app/tc-app-values.rkt b/collects/typed-racket/typecheck/tc-app/tc-app-values.rkt index 45655ac243..24639bb96f 100644 --- a/collects/typed-racket/typecheck/tc-app/tc-app-values.rkt +++ b/collects/typed-racket/typecheck/tc-app/tc-app-values.rkt @@ -5,7 +5,7 @@ "utils.rkt" syntax/parse racket/match syntax/parse/experimental/reflect - (typecheck signatures tc-funapp check-below) + (typecheck signatures tc-funapp) (types abbrev utils) (rep type-rep) diff --git a/collects/typed-racket/typecheck/tc-expr-unit.rkt b/collects/typed-racket/typecheck/tc-expr-unit.rkt index 2a93b6992e..410141d24b 100644 --- a/collects/typed-racket/typecheck/tc-expr-unit.rkt +++ b/collects/typed-racket/typecheck/tc-expr-unit.rkt @@ -30,103 +30,97 @@ (pattern (~and i (~or :number :str :bytes)) #:fail-unless expected #f #:fail-unless (subtype (-val (syntax-e #'i)) expected) #f)) - (define r - (syntax-parse v-stx - [i:exp expected] - [i:boolean (-val (syntax-e #'i))] - [i:identifier (-val (syntax-e #'i))] - - ;; Numbers - [0 -Zero] - [1 -One] - [(~var i (3d (conjoin byte? positive?))) -PosByte] - [(~var i (3d byte?)) -Byte] - [(~var i (3d (conjoin portable-index? positive?))) -PosIndex] - [(~var i (3d (conjoin portable-fixnum? positive?))) -PosFixnum] - [(~var i (3d (conjoin portable-fixnum? negative?))) -NegFixnum] - [(~var i (3d exact-positive-integer?)) -PosInt] - [(~var i (3d (conjoin exact-integer? negative?))) -NegInt] - [(~var i (3d (conjoin number? exact? rational? positive?))) -PosRat] - [(~var i (3d (conjoin number? exact? rational? negative?))) -NegRat] - [(~var i (3d (lambda (x) (eqv? x 0.0)))) -FlonumPosZero] - [(~var i (3d (lambda (x) (eqv? x -0.0)))) -FlonumNegZero] - [(~var i (3d (lambda (x) (eqv? x +nan.0)))) -FlonumNan] - [(~var i (3d (lambda (x) (eqv? x +inf.0)))) (-val +inf.0)] - [(~var i (3d (lambda (x) (eqv? x -inf.0)))) (-val -inf.0)] - [(~var i (3d (conjoin flonum? positive?))) -PosFlonum] - [(~var i (3d (conjoin flonum? negative?))) -NegFlonum] - [(~var i (3d flonum?)) -Flonum] ; for nan - [(~var i (3d (lambda (x) (eqv? x 0.0f0)))) -SingleFlonumPosZero] - [(~var i (3d (lambda (x) (eqv? x -0.0f0)))) -SingleFlonumNegZero] - [(~var i (3d (lambda (x) (eqv? x +nan.f)))) -SingleFlonumNan] - [(~var i (3d (lambda (x) (eqv? x +inf.f)))) (-val +inf.f)] - [(~var i (3d (lambda (x) (eqv? x -inf.f)))) (-val -inf.f)] - [(~var i (3d (conjoin single-flonum? positive?))) -PosSingleFlonum] - [(~var i (3d (conjoin single-flonum? negative?))) -NegSingleFlonum] - [(~var i (3d single-flonum?)) -SingleFlonum] ; for nan - [(~var i (3d inexact-real?)) -InexactReal] ; catch-all, just in case - [(~var i (3d real?)) -Real] ; catch-all, just in case - ;; a complex number can't have a float imaginary part and an exact real part - [(~var i (3d (conjoin number? exact?))) - -ExactNumber] - [(~var i (3d (conjoin number? (lambda (x) (and (flonum? (imag-part x)) - (flonum? (real-part x))))))) - -FloatComplex] - [(~var i (3d (conjoin number? (lambda (x) (and (single-flonum? (imag-part x)) - (single-flonum? (real-part x))))))) - -SingleFlonumComplex] - ;; can't have real and imaginary parts that are both inexact, but not the same precision - [(~var i (3d number?)) -Number] ; otherwise, Number - - [i:str -String] - [i:char -Char] - [i:keyword (-val (syntax-e #'i))] - [i:bytes -Bytes] - [i:byte-pregexp -Byte-PRegexp] - [i:byte-regexp -Byte-Regexp] - [i:pregexp -PRegexp] - [i:regexp -Regexp] - [(~and i ()) (-val '())] - [(i . r) - (match (and expected (restrict expected (-pair Univ Univ) 'orig)) - [(Pair: a-ty d-ty) - (-pair - (tc-literal #'i a-ty) - (tc-literal #'r d-ty))] - [(Union: '()) - (tc-error/expr "expected ~a, but got" expected #:return expected)] - ;; errors are handled elsewhere - [t - (-pair (tc-literal #'i) (tc-literal #'r))])] - [(~var i (3d vector?)) - (match (and expected (restrict expected (-vec Univ) 'orig)) - [(Vector: t) - (make-Vector (apply Un - t ;; so that this isn't (Un) when we get no elems - (for/list ([l (in-vector (syntax-e #'i))]) - (tc-literal l t))))] - [(HeterogeneousVector: ts) - (make-HeterogeneousVector - (for/list ([l (in-vector (syntax-e #'i))] - [t (in-list ts)]) - (tc-literal l t)))] - ;; errors are handled elsewhere - [_ (make-HeterogeneousVector (for/list ([l (syntax-e #'i)]) - (generalize (tc-literal l #f))))])] - [(~var i (3d hash?)) - (match expected - [(Hashtable: k v) - (let* ([h (syntax-e #'i)] - [ks (hash-map h (lambda (x y) (tc-literal x k)))] - [vs (hash-map h (lambda (x y) (tc-literal y v)))]) - (make-Hashtable (generalize (check-below (apply Un ks) k)) (generalize (check-below (apply Un vs) v))))] - [_ (let* ([h (syntax-e #'i)] - [ks (hash-map h (lambda (x y) (tc-literal x)))] - [vs (hash-map h (lambda (x y) (tc-literal y)))]) - (make-Hashtable (generalize (apply Un ks)) (generalize (apply Un vs))))])] - [_ Univ])) - - (cond-check-below r expected)) + (syntax-parse v-stx + [i:exp expected] + [i:boolean (-val (syntax-e #'i))] + [i:identifier (-val (syntax-e #'i))] + ;; Numbers + [0 -Zero] + [1 -One] + [(~var i (3d (conjoin byte? positive?))) -PosByte] + [(~var i (3d byte?)) -Byte] + [(~var i (3d (conjoin portable-index? positive?))) -PosIndex] + [(~var i (3d (conjoin portable-fixnum? positive?))) -PosFixnum] + [(~var i (3d (conjoin portable-fixnum? negative?))) -NegFixnum] + [(~var i (3d exact-positive-integer?)) -PosInt] + [(~var i (3d (conjoin exact-integer? negative?))) -NegInt] + [(~var i (3d (conjoin number? exact? rational? positive?))) -PosRat] + [(~var i (3d (conjoin number? exact? rational? negative?))) -NegRat] + [(~var i (3d (lambda (x) (eqv? x 0.0)))) -FlonumPosZero] + [(~var i (3d (lambda (x) (eqv? x -0.0)))) -FlonumNegZero] + [(~var i (3d (lambda (x) (eqv? x +nan.0)))) -FlonumNan] + [(~var i (3d(lambda (x) (eqv? x +inf.0)))) (-val +inf.0)] + [(~var i (3d (lambda (x) (eqv? x -inf.0)))) (-val -inf.0)] + [(~var i (3d (conjoin flonum? positive?))) -PosFlonum] + [(~var i (3d (conjoin flonum? negative?))) -NegFlonum] + [(~var i (3d flonum?)) -Flonum] ; for nan + [(~var i (3d (lambda (x) (eqv? x 0.0f0)))) -SingleFlonumPosZero] + [(~var i (3d (lambda (x) (eqv? x -0.0f0)))) -SingleFlonumNegZero] + [(~var i (3d (lambda (x) (eqv? x +nan.f)))) -SingleFlonumNan] + [(~var i (3d(lambda (x) (eqv? x +inf.f)))) (-val +inf.f)] + [(~var i (3d (lambda (x) (eqv? x -inf.f)))) (-val -inf.f)] + [(~var i (3d (conjoin single-flonum? positive?))) -PosSingleFlonum] + [(~var i (3d (conjoin single-flonum? negative?))) -NegSingleFlonum] + [(~var i (3d single-flonum?)) -SingleFlonum] ; for nan + [(~var i (3d inexact-real?)) -InexactReal] ; catch-all, just in case + [(~var i (3d real?)) -Real] ; catch-all, just in case + ;; a complex number can't have a float imaginary part and an exact real part + [(~var i (3d (conjoin number? exact?))) + -ExactNumber] + [(~var i (3d (conjoin number? (lambda (x) (and (flonum? (imag-part x)) + (flonum? (real-part x))))))) + -FloatComplex] + [(~var i (3d (conjoin number? (lambda (x) (and (single-flonum? (imag-part x)) + (single-flonum? (real-part x))))))) + -SingleFlonumComplex] + ;; can't have real and imaginary parts that are both inexact, but not the same precision + [(~var i (3d number?)) -Number] ; otherwise, Number + + [i:str -String] + [i:char -Char] + [i:keyword (-val (syntax-e #'i))] + [i:bytes -Bytes] + [i:byte-pregexp -Byte-PRegexp] + [i:byte-regexp -Byte-Regexp] + [i:pregexp -PRegexp] + [i:regexp -Regexp] + [(~and i ()) (-val '())] + [(i . r) + (match (and expected (restrict expected (-pair Univ Univ) 'orig)) + [(Pair: a-ty d-ty) + (-pair + (tc-literal #'i a-ty) + (tc-literal #'r d-ty))] + [t + (-pair (tc-literal #'i) (tc-literal #'r))])] + [(~var i (3d vector?)) + (match (and expected (restrict expected (-vec Univ) 'orig)) + [(Vector: t) + (make-Vector (apply Un + t ;; so that this isn't (Un) when we get no elems + (for/list ([l (in-vector (syntax-e #'i))]) + (tc-literal l t))))] + [(HeterogeneousVector: ts) + (make-HeterogeneousVector + (for/list ([l (in-vector (syntax-e #'i))] + [t (in-list ts)]) + check-below (tc-literal l t) t))] + [_ (make-HeterogeneousVector (for/list ([l (syntax-e #'i)]) + (generalize (tc-literal l #f))))])] + [(~var i (3d hash?)) + (match expected + [(Hashtable: k v) + (let* ([h (syntax-e #'i)] + [ks (hash-map h (lambda (x y) (tc-literal x k)))] + [vs (hash-map h (lambda (x y) (tc-literal y v)))]) + (check-below (apply Un ks) k) + (check-below (apply Un vs) v) + expected)] + [_ (let* ([h (syntax-e #'i)] + [ks (hash-map h (lambda (x y) (tc-literal x)))] + [vs (hash-map h (lambda (x y) (tc-literal y)))]) + (make-Hashtable (generalize (apply Un ks)) (generalize (apply Un vs))))])] + [_ Univ])) ;; do-inst : syntax type -> type @@ -225,9 +219,9 @@ => (lambda (ann) (let* ([r (tc-expr/check/internal form* ann)] - [r* (check-below r expected)]) + [r* (check-below (check-below r ann) expected)]) ;; add this to the *original* form, since the newer forms aren't really in the program - (add-typeof-expr form ann) + (add-typeof-expr form r) ;; around again in case there is an instantiation ;; remove the ascription so we don't loop infinitely (loop (remove-ascription form*) r* #t)))] @@ -256,7 +250,7 @@ [else (define t (tc-expr/check/internal form* expected)) (add-typeof-expr form t) - t])))) + (check-below t expected)])))) (define (explicit-fail stx msg var) (cond [(and (identifier? var) (lookup-type/lexical var #:fail (λ _ #f))) @@ -284,126 +278,119 @@ ;; the argument must be syntax (unless (syntax? form) (int-err "bad form input to tc-expr: ~a" form)) - (let ([old-ret ret] - ;; a local version of ret that does the checking - [ret - (lambda args - (define te (apply ret args)) - (check-below te expected))]) - (syntax-parse form - #:literal-sets (kernel-literals) - #:literals (find-method/who) - [stx - #:when (syntax-property form 'typechecker:with-handlers) - (check-subforms/with-handlers/check form expected)] - [stx - #:when (syntax-property form 'typechecker:ignore-some) - (check-subforms/ignore form) - ;; We trust ignore to be only on syntax objects objects that are well typed - expected] - ;; explicit failure - [(quote-syntax ((~literal typecheck-fail-internal) stx msg:str var)) - (explicit-fail #'stx #'msg #'var)] - ;; data - [(quote #f) (ret (-val #f) false-filter)] - [(quote #t) (ret (-val #t) true-filter)] - [(quote val) (match expected - [(tc-result1: t) - (ret (tc-literal #'val t) true-filter)] - [_ ;; this isn't going to work, defer error handling - (check-below (ret (tc-literal #'val #f)) expected)])] - ;; syntax - [(quote-syntax datum) (ret (-Syntax (tc-literal #'datum)) true-filter)] - ;; mutation! - [(set! id val) - (match-let* ([(tc-result1: id-t) (single-value #'id)] - [(tc-result1: val-t) (single-value #'val)]) - (unless (subtype val-t id-t) - (tc-error/expr "Mutation only allowed with compatible types:\n~a is not a subtype of ~a" val-t id-t)) - (ret -Void))] - ;; top-level variable reference - occurs at top level - [(#%top . id) (check-below (tc-id #'id) expected)] - - [(#%variable-reference . _) - (ret -Variable-Reference)] - ;; identifiers - [x:identifier - (check-below (tc-id #'x) expected)] - ;; w-c-m - [(with-continuation-mark e1 e2 e3) - (define key-t (single-value #'e1)) - (match key-t - [(tc-result1: (Continuation-Mark-Keyof: rhs)) - (tc-expr/check/type #'e2 rhs) - (tc-expr/check #'e3 expected)] - [(? (λ (result) - (and (identifier? #'e1) - (free-identifier=? #'pz:pk #'e1)))) - (tc-expr/check/type #'e2 Univ) - (tc-expr/check #'e3 expected)] - [(tc-result1: key-t) - ;(check-below key-t -Symbol) - ;; FIXME -- would need to protect `e2` with any-wrap/c contract - ;; instead, just fail - - ;(tc-expr/check/type #'e2 Univ) - ;(tc-expr/check #'e3 expected) - (tc-error/expr "with-continuation-mark requires a continuation-mark-key, but got ~a" key-t - #:return expected)])] - ;; application - [(#%plain-app . _) (tc/app/check form expected)] - ;; #%expression - [(#%expression e) (tc-expr/check #'e expected)] - ;; syntax - ;; for now, we ignore the rhs of macros - [(letrec-syntaxes+values stxs vals . body) - (tc-expr/check (syntax/loc form (letrec-values vals . body)) expected)] - ;; begin - [(begin e . es) (tc-exprs/check (syntax->list #'(e . es)) expected)] - [(begin0 e . es) - (begin (tc-exprs/check (syntax->list #'es) (old-ret Univ)) - (tc-expr/check #'e expected))] - ;; if - [(if tst thn els) (tc/if-twoarm #'tst #'thn #'els expected)] - ;; lambda - [(#%plain-lambda formals . body) - (tc/lambda/check form #'(formals) #'(body) expected)] - [(case-lambda [formals . body] ...) - (tc/lambda/check form #'(formals ...) #'(body ...) expected)] - ;; send - [(let-values (((_) meth)) - (let-values (((_) rcvr)) - (let-values (((_) (~and find-app (#%plain-app find-method/who _ _ _)))) - (#%plain-app _ _ args ...)))) - (tc/send #'find-app #'rcvr #'meth #'(args ...) expected)] - ;; kw/opt function def - [(let-values ([(_) fun]) - . body) - #:when (or (syntax-property form 'kw-lambda) - (syntax-property form 'opt-lambda)) - (match expected - [(tc-result1: (and f (or (Function: _) - (Poly: _ (Function: _))))) - (tc-expr/check/type #'fun (kw-convert f #:split #t))] - [(or (tc-results: _) (tc-any-results:)) - (tc-error/expr "Keyword functions must have function type, given ~a" expected)]) - expected] - ;; let - [(let-values ([(name ...) expr] ...) . body) - (tc/let-values #'((name ...) ...) #'(expr ...) #'body form expected)] - [(letrec-values ([(name) expr]) name*) - #:when (and (identifier? #'name*) (free-identifier=? #'name #'name*) - (value-restriction? #'expr #'name)) - (match expected - [(tc-result1: t) - (with-lexical-env/extend (list #'name) (list t) (tc-expr/check #'expr expected))] - [(tc-results: ts) - (tc-error/expr #:return (ret (Un)) "Expected ~a values, but got only 1" (length ts))])] - [(letrec-values ([(name ...) expr] ...) . body) - (tc/letrec-values #'((name ...) ...) #'(expr ...) #'body form expected)] - ;; other - [_ (tc-error/expr #:return (ret expected) "cannot typecheck unknown form : ~a\n" (syntax->datum form))] - )))) + (syntax-parse form + #:literal-sets (kernel-literals) + #:literals (find-method/who) + [stx + #:when (syntax-property form 'typechecker:with-handlers) + (check-subforms/with-handlers/check form expected)] + [stx + #:when (syntax-property form 'typechecker:ignore-some) + (check-subforms/ignore form) + ;; We trust ignore to be only on syntax objects objects that are well typed + expected] + ;; explicit failure + [(quote-syntax ((~literal typecheck-fail-internal) stx msg:str var)) + (explicit-fail #'stx #'msg #'var)] + ;; data + [(quote #f) (ret (-val #f) false-filter)] + [(quote #t) (ret (-val #t) true-filter)] + [(quote val) + (match expected + [(tc-result1: t) + (ret (tc-literal #'val t) true-filter)] + [_ + (ret (tc-literal #'val #f))])] + ;; syntax + [(quote-syntax datum) (ret (-Syntax (tc-literal #'datum)) true-filter)] + ;; mutation! + [(set! id val) + (match-let* ([(tc-result1: id-t) (single-value #'id)] + [(tc-result1: val-t) (single-value #'val)]) + (unless (subtype val-t id-t) + (tc-error/expr "Mutation only allowed with compatible types:\n~a is not a subtype of ~a" val-t id-t)) + (ret -Void))] + ;; top-level variable reference - occurs at top level + [(#%top . id) (tc-id #'id)] + [(#%variable-reference . _) + (ret -Variable-Reference)] + ;; identifiers + [x:identifier (tc-id #'x)] + ;; w-c-m + [(with-continuation-mark e1 e2 e3) + (define key-t (single-value #'e1)) + (match key-t + [(tc-result1: (Continuation-Mark-Keyof: rhs)) + (tc-expr/check/type #'e2 rhs) + (tc-expr/check #'e3 expected)] + [(? (λ (result) + (and (identifier? #'e1) + (free-identifier=? #'pz:pk #'e1)))) + (tc-expr/check/type #'e2 Univ) + (tc-expr/check #'e3 expected)] + [(tc-result1: key-t) + ;(check-below key-t -Symbol) + ;; FIXME -- would need to protect `e2` with any-wrap/c contract + ;; instead, just fail + + ;(tc-expr/check/type #'e2 Univ) + ;(tc-expr/check #'e3 expected) + (tc-error/expr "with-continuation-mark requires a continuation-mark-key, but got ~a" key-t + #:return expected)])] + ;; application + [(#%plain-app . _) (tc/app/check form expected)] + ;; #%expression + [(#%expression e) (tc-expr/check #'e expected)] + ;; syntax + ;; for now, we ignore the rhs of macros + [(letrec-syntaxes+values stxs vals . body) + (tc-expr/check (syntax/loc form (letrec-values vals . body)) expected)] + ;; begin + [(begin e . es) (tc-exprs/check (syntax->list #'(e . es)) expected)] + [(begin0 e . es) + (tc-exprs/check (syntax->list #'es) tc-any-results) + (tc-expr/check #'e expected)] + ;; if + [(if tst thn els) (tc/if-twoarm #'tst #'thn #'els expected)] + ;; lambda + [(#%plain-lambda formals . body) + (tc/lambda/check form #'(formals) #'(body) expected)] + [(case-lambda [formals . body] ...) + (tc/lambda/check form #'(formals ...) #'(body ...) expected)] + ;; send + [(let-values (((_) meth)) + (let-values (((_) rcvr)) + (let-values (((_) (~and find-app (#%plain-app find-method/who _ _ _)))) + (#%plain-app _ _ args ...)))) + (tc/send #'find-app #'rcvr #'meth #'(args ...) expected)] + ;; kw/opt function def + [(let-values ([(_) fun]) + . body) + #:when (or (syntax-property form 'kw-lambda) + (syntax-property form 'opt-lambda)) + (match expected + [(tc-result1: (and f (or (Function: _) + (Poly: _ (Function: _))))) + (tc-expr/check/type #'fun (kw-convert f #:split #t))] + [(or (tc-results: _) (tc-any-results:)) + (tc-error/expr "Keyword functions must have function type, given ~a" expected)]) + expected] + ;; let + [(let-values ([(name ...) expr] ...) . body) + (tc/let-values #'((name ...) ...) #'(expr ...) #'body form expected)] + [(letrec-values ([(name) expr]) name*) + #:when (and (identifier? #'name*) (free-identifier=? #'name #'name*) + (value-restriction? #'expr #'name)) + (match expected + [(tc-result1: t) + (with-lexical-env/extend (list #'name) (list t) (tc-expr/check #'expr expected))] + [(tc-results: ts) + (tc-error/expr #:return (ret (Un)) "Expected ~a values, but got only 1" (length ts))])] + [(letrec-values ([(name ...) expr] ...) . body) + (tc/letrec-values #'((name ...) ...) #'(expr ...) #'body form expected)] + ;; other + [_ (tc-error/expr #:return (ret expected) "cannot typecheck unknown form : ~a\n" (syntax->datum form))] + ))) ;; type check form in the current type environment ;; if there is a type error in form, or if it has the wrong annotation, error @@ -513,18 +500,19 @@ (unless (syntax? form) (int-err "bad form input to tc-expr: ~a" form)) ;; typecheck form - (let ([ty (cond [(type-ascription form) => (lambda (ann) - (tc-expr/check form ann))] - [else (internal-tc-expr form)])]) - (match ty - [(tc-any-results:) - (add-typeof-expr form ty) - ty] - [(tc-results: ts fs os) - (let* ([ts* (do-inst form ts)] - [r (ret ts* fs os)]) - (add-typeof-expr form r) - r)])))) + (cond + [(type-ascription form) => (lambda (ann) (tc-expr/check form ann))] + [else + (let ([ty (internal-tc-expr form)]) + (match ty + [(tc-any-results:) + (add-typeof-expr form ty) + ty] + [(tc-results: ts fs os) + (let* ([ts* (do-inst form ts)] + [r (ret ts* fs os)]) + (add-typeof-expr form r) + r)]))]))) (define/cond-contract (tc/send form rcvr method args [expected #f]) (-->* (syntax? syntax? syntax? syntax?) ((-or/c tc-results/c #f)) tc-results/c) @@ -534,8 +522,7 @@ [(tc-result1: (Value: (? symbol? s))) (let* ([ftype (cond [(assq s methods) => cadr] [else (tc-error/expr "send: method ~a not understood by class ~a" s c)])] - [ret-ty (tc/funapp rcvr args (ret ftype) (map tc-expr (syntax->list args)) expected)] - [retval (cond-check-below ret-ty expected)]) + [retval (tc/funapp rcvr args (ret ftype) (map tc-expr (syntax->list args)) expected)]) (add-typeof-expr form retval) retval)] [(tc-result1: t) (int-err "non-symbol methods not supported by Typed Racket: ~a" t)])] diff --git a/collects/typed-racket/typecheck/tc-if.rkt b/collects/typed-racket/typecheck/tc-if.rkt index 3e7a634ff6..f35637ee48 100644 --- a/collects/typed-racket/typecheck/tc-if.rkt +++ b/collects/typed-racket/typecheck/tc-if.rkt @@ -1,6 +1,6 @@ #lang racket/unit (require (rename-in "../utils/utils.rkt" [infer r:infer]) - "signatures.rkt" "check-below.rkt" + "signatures.rkt" (rep type-rep filter-rep object-rep) (types abbrev subtype union utils filter-ops) (env lexical-env type-env-structs) @@ -76,34 +76,33 @@ [else (add-neither tst)]) (match* (results-t results-u) - [((tc-any-results:) _) (cond-check-below tc-any-results expected)] - [(_ (tc-any-results:)) (cond-check-below tc-any-results expected)] + [((tc-any-results:) _) tc-any-results] + [(_ (tc-any-results:)) tc-any-results] [((tc-results: ts fs2 os2) (tc-results: us fs3 os3)) ;; if we have the same number of values in both cases (cond [(= (length ts) (length us)) - (let ([r (combine-results - (for/list ([f2 fs2] [f3 fs3] [t2 ts] [t3 us] [o2 os2] [o3 os3]) - (let ([filter - (match* (f2 f3) - [((NoFilter:) _) - (-FS -top -top)] - [(_ (NoFilter:)) - (-FS -top -top)] - [((FilterSet: f2+ f2-) (FilterSet: f3+ f3-)) - ;(printf "f2- ~a f+ ~a\n" f2- fs+) - (-FS (-or (apply -and fs+ f2+ new-thn-props) (apply -and fs- f3+ new-els-props)) - (-or (apply -and fs+ f2- new-thn-props) (apply -and fs- f3- new-els-props)))])] - [type (Un t2 t3)] - [object (if (object-equal? o2 o3) o2 (make-Empty))]) - ;(printf "result filter is: ~a\n" filter) - (ret type filter object))))]) - (cond-check-below r expected))] + (combine-results + (for/list ([f2 fs2] [f3 fs3] [t2 ts] [t3 us] [o2 os2] [o3 os3]) + (let ([filter + (match* (f2 f3) + [((NoFilter:) _) + (-FS -top -top)] + [(_ (NoFilter:)) + (-FS -top -top)] + [((FilterSet: f2+ f2-) (FilterSet: f3+ f3-)) + ;(printf "f2- ~a f+ ~a\n" f2- fs+) + (-FS (-or (apply -and fs+ f2+ new-thn-props) (apply -and fs- f3+ new-els-props)) + (-or (apply -and fs+ f2- new-thn-props) (apply -and fs- f3- new-els-props)))])] + [type (Un t2 t3)] + [object (if (object-equal? o2 o3) o2 (make-Empty))]) + ;(printf "result filter is: ~a\n" filter) + (ret type filter object))))] ;; special case if one of the branches is unreachable [(and (= 1 (length us)) (type-equal? (car us) (Un))) - (cond-check-below (ret ts fs2 os2) expected)] + (ret ts fs2 os2)] [(and (= 1 (length ts)) (type-equal? (car ts) (Un))) - (cond-check-below (ret us fs3 os3) expected)] + (ret us fs3 os3)] ;; otherwise, error [else (tc-error/expr #:return (or expected (ret Err)) diff --git a/collects/typed-racket/typecheck/tc-lambda-unit.rkt b/collects/typed-racket/typecheck/tc-lambda-unit.rkt index 00ce4d1b7c..d6c21d98b5 100644 --- a/collects/typed-racket/typecheck/tc-lambda-unit.rkt +++ b/collects/typed-racket/typecheck/tc-lambda-unit.rkt @@ -3,7 +3,7 @@ (require (rename-in "../utils/utils.rkt" [infer r:infer]) "signatures.rkt" "tc-metafunctions.rkt" - "tc-subst.rkt" "check-below.rkt" + "tc-subst.rkt" racket/dict racket/list syntax/parse "parse-cl.rkt" racket/syntax unstable/struct syntax/stx @@ -270,9 +270,7 @@ [_ (go #f (syntax->list formals) (syntax->list bodies) null null null)]))) (define (tc/mono-lambda/type formals bodies expected) - (define t (make-Function (map lam-result->type (tc/mono-lambda formals bodies expected)))) - (cond-check-below (ret t true-filter) expected) - t) + (make-Function (map lam-result->type (tc/mono-lambda formals bodies expected)))) (define (plambda-prop stx) (define d (syntax-property stx 'typechecker:plambda)) @@ -330,7 +328,7 @@ (extend-tvars tvars (maybe-loop form formals bodies (ret expected*)))) t)] - [(or (tc-any-results:) #f) + [(or (tc-result1: _) (tc-any-results:) #f) (match (map syntax-e (syntax->list (plambda-prop form))) [(list tvars ... dotted-var '...) (let* ([ty (extend-indexes dotted-var @@ -345,8 +343,6 @@ (tc/mono-lambda/type formals bodies #f))]) ;(printf "plambda: ~a ~a ~a \n" literal-tvars new-tvars ty) (make-Poly fresh-tvars ty #:original-names tvars))])] - [(tc-result1: t) - (check-below (tc/plambda form formals bodies #f) t)] [_ (int-err "not a good expected value: ~a" expected)])) ;; typecheck a sequence of case-lambda clauses, which is possibly polymorphic diff --git a/collects/typed-racket/typecheck/tc-let-unit.rkt b/collects/typed-racket/typecheck/tc-let-unit.rkt index e79fc24bd2..9cfae75f89 100644 --- a/collects/typed-racket/typecheck/tc-let-unit.rkt +++ b/collects/typed-racket/typecheck/tc-let-unit.rkt @@ -2,7 +2,6 @@ (require (rename-in "../utils/utils.rkt" [infer r:infer]) "signatures.rkt" "tc-metafunctions.rkt" "tc-subst.rkt" - "check-below.rkt" (types utils abbrev union) (private type-annotation parse-type) (env lexical-env type-alias-env global-env type-env-structs) @@ -92,11 +91,10 @@ expected-types ; types w/o undefined (append p1 p2) ;; typecheck the body - (if expected - (check-below - (run (tc-exprs/check (syntax->list body) (erase-filter expected))) - expected) - (run (tc-exprs (syntax->list body)))))))) + (run + (if expected + (tc-exprs/check (syntax->list body) (erase-filter expected)) + (tc-exprs (syntax->list body)))))))) (define (tc-expr/maybe-expected/t e name) (define expecteds