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

Reduce usage of check-below.

Browse Source 
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.
This commit is contained in:
Eric Dobson 2013-02-19 00:12:57 -08:00
parent 1fd21ef640
commit 1334e8dcc7
17 changed files with 317 additions and 314 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
collects/tests/typed-racket/optimizer/missed-optimizations/fixnum.rkt
View File

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

16
collects/tests/typed-racket/optimizer/missed-optimizations/pair.rkt
View File

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

26
collects/tests/typed-racket/optimizer/missed-optimizations/precision-loss.rkt
View File

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

18
collects/tests/typed-racket/optimizer/tests/annotations.rkt Normal file
View File

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

7
collects/tests/typed-racket/optimizer/tests/vector-length.rkt
View File

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

2
collects/typed-racket/typecheck/tc-app/tc-app-apply.rkt
View File

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

2
collects/typed-racket/typecheck/tc-app/tc-app-eq.rkt
View File

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

18
collects/typed-racket/typecheck/tc-app/tc-app-hetero.rkt
View File

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

4
collects/typed-racket/typecheck/tc-app/tc-app-list.rkt
View File

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

6
collects/typed-racket/typecheck/tc-app/tc-app-main.rkt
View File

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

2
collects/typed-racket/typecheck/tc-app/tc-app-objects.rkt
View File

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

8
collects/typed-racket/typecheck/tc-app/tc-app-special.rkt
View File

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

2
collects/typed-racket/typecheck/tc-app/tc-app-values.rkt
View File

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

455
collects/typed-racket/typecheck/tc-expr-unit.rkt
View File

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

43
collects/typed-racket/typecheck/tc-if.rkt
View File

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

10
collects/typed-racket/typecheck/tc-lambda-unit.rkt
View File

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

10
collects/typed-racket/typecheck/tc-let-unit.rkt
View File

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