From c681b3c91f5bc6c42cc656d4f74c3abe074d6895 Mon Sep 17 00:00:00 2001 From: Sam Tobin-Hochstadt Date: Mon, 20 Feb 2012 13:19:53 -0500 Subject: [PATCH] Speed up and improve `tc-literal`. Now uses expected types more, and more sensibly. Closes PR 12586. original commit: a8bdb9d6ce5fb03a40f8d1a4caa0cf6d8c392389 --- .../unit-tests/typecheck-tests.rkt | 2 + collects/typed-racket/infer/restrict.rkt | 39 ++-- .../typed-racket/typecheck/tc-app-helper.rkt | 2 +- collects/typed-racket/typecheck/tc-app.rkt | 3 +- .../typed-racket/typecheck/tc-expr-unit.rkt | 183 +++++++++--------- 5 files changed, 117 insertions(+), 112 deletions(-) diff --git a/collects/tests/typed-racket/unit-tests/typecheck-tests.rkt b/collects/tests/typed-racket/unit-tests/typecheck-tests.rkt index 8dd3cfdc..59f3ceac 100644 --- a/collects/tests/typed-racket/unit-tests/typecheck-tests.rkt +++ b/collects/tests/typed-racket/unit-tests/typecheck-tests.rkt @@ -1398,6 +1398,8 @@ [tc-e (vector-append #(1) #(2)) (-vec -Integer)] + [tc-e/t (ann #() (Vectorof Integer)) + (-vec -Integer)] ) (test-suite "check-type tests" diff --git a/collects/typed-racket/infer/restrict.rkt b/collects/typed-racket/infer/restrict.rkt index b918048d..2592eb87 100644 --- a/collects/typed-racket/infer/restrict.rkt +++ b/collects/typed-racket/infer/restrict.rkt @@ -9,29 +9,30 @@ (import infer^) (export restrict^) - -;; NEW IMPL -;; restrict t1 to be a subtype of t2 -;; if `f' is 'new, use t2 when giving up, otherwise use t1 -(define (restrict* t1 t2 [f 'new]) - ;; we don't use union map directly, since that might produce too many elements +;; we don't use union map directly, since that might produce too many elements (define (union-map f l) (match l [(Union: es) (let ([l (map f es)]) (apply Un l))])) - (match* (t1 t2) - [(_ (? (lambda _ (subtype t1 t2)))) t1] ;; already a subtype - [(_ (Poly: vars t)) - (let ([subst (infer vars null (list t1) (list t) t1)]) - (and subst (restrict* t1 (subst-all subst t1) f)))] - [((Union: _) _) (union-map (lambda (e) (restrict* e t2 f)) t1)] - [(_ (Union: _)) (union-map (lambda (e) (restrict* t1 e f)) t2)] - [((? needs-resolving?) _) (restrict* (resolve-once t1) t2 f)] - [(_ (? needs-resolving?)) (restrict* t1 (resolve-once t2) f)] - [(_ _) - (cond [(subtype t2 t1) t2] ;; we don't actually want this - want something that's a part of t1 - [(not (overlap t1 t2)) (Un)] ;; there's no overlap, so the restriction is empty - [else (if (eq? f 'new) t2 t1)])])) ;; t2 and t1 have a complex relationship, so we punt + +;; NEW IMPL +;; restrict t1 to be a subtype of t2 +;; if `f' is 'new, use t2 when giving up, otherwise use t1 +(define (restrict* t1 t2 [f 'new]) + (cond + [(subtype t1 t2) t1] ;; already a subtype + [(match t2 + [(Poly: vars t) + (let ([subst (infer vars null (list t1) (list t) t1)]) + (and subst (restrict* t1 (subst-all subst t1) f)))] + [_ #f])] + [(Union? t1) (union-map (lambda (e) (restrict* e t2 f)) t1)] + [(Union? t2) (union-map (lambda (e) (restrict* t1 e f)) t2)] + [(needs-resolving? t1) (restrict* (resolve-once t1) t2 f)] + [(needs-resolving? t2) (restrict* t1 (resolve-once t2) f)] + [(subtype t2 t1) t2] ;; we don't actually want this - want something that's a part of t1 + [(not (overlap t1 t2)) (Un)] ;; there's no overlap, so the restriction is empty + [else (if (eq? f 'new) t2 t1)])) ;; t2 and t1 have a complex relationship, so we punt (define restrict restrict*) diff --git a/collects/typed-racket/typecheck/tc-app-helper.rkt b/collects/typed-racket/typecheck/tc-app-helper.rkt index a4c68ed0..3001eb0f 100644 --- a/collects/typed-racket/typecheck/tc-app-helper.rkt +++ b/collects/typed-racket/typecheck/tc-app-helper.rkt @@ -40,7 +40,7 @@ ta))]) (define-values (t-r f-r o-r) (for/lists (t-r f-r o-r) - ([r (in-list results)]) + ([r (in-list results)]) (open-Result r o-a t-a))) (ret t-r f-r o-r)))] [((arr: _ _ _ drest '()) _) diff --git a/collects/typed-racket/typecheck/tc-app.rkt b/collects/typed-racket/typecheck/tc-app.rkt index b93a451d..ba376698 100644 --- a/collects/typed-racket/typecheck/tc-app.rkt +++ b/collects/typed-racket/typecheck/tc-app.rkt @@ -153,7 +153,8 @@ (define (type->list t) (match t - [(Pair: (Value: (? keyword? k)) b) (cons k (type->list b))] + [(Pair: (Value: (? keyword? k)) b) + (cons k (type->list b))] [(Value: '()) null] [_ (int-err "bad value in type->list: ~a" t)])) diff --git a/collects/typed-racket/typecheck/tc-expr-unit.rkt b/collects/typed-racket/typecheck/tc-expr-unit.rkt index c0606843..d5d43aba 100644 --- a/collects/typed-racket/typecheck/tc-expr-unit.rkt +++ b/collects/typed-racket/typecheck/tc-expr-unit.rkt @@ -23,98 +23,99 @@ (export tc-expr^) ;; return the type of a literal value -;; scheme-value -> type +;; scheme-value [type] -> type (define (tc-literal v-stx [expected #f]) - (define-syntax-class exp - (pattern i - #:fail-unless expected #f - #:attr datum (syntax-e #'i) - #:fail-unless (subtype (-val (attribute datum)) expected) #f)) - (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) (eq? x 0.0)))) -FlonumPosZero] - [(~var i (3d (lambda (x) (eq? x -0.0)))) -FlonumNegZero] - [(~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) (eq? x 0.0f0)))) -SingleFlonumPosZero] - [(~var i (3d (lambda (x) (eq? x -0.0f0)))) -SingleFlonumNegZero] - [(~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))))))) - -InexactComplex] - [(~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] - [(i ...) - (match expected - [(Mu: var (Union: (list (Value: '()) (Pair: elem-ty (F: var))))) - (-Tuple - (for/list ([l (in-list (syntax->list #'(i ...)))]) - (tc-literal l elem-ty)))] - ;; errors are handled elsewhere - [_ (-Tuple - (for/list ([l (in-list (syntax->list #'(i ...)))]) - (tc-literal l #f)))])] - [(~var i (3d vector?)) - (match expected - [(Vector: t) - (make-Vector (apply Un - (for/list ([l (in-vector (syntax-e #'i))]) - (tc-literal l t))))] - [(HeterogenousVector: ts) - (make-HeterogenousVector - (for/list ([l (in-vector (syntax-e #'i))] - [t (in-list ts)]) - (tc-literal l t)))] - ;; errors are handled elsewhere - [_ (make-HeterogenousVector (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)))))] - [_ (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))))])] - [(a . b) (-pair (tc-literal #'a) (tc-literal #'b))] - [_ Univ])) + (define r + (syntax-parse v-stx + [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) (eq? x 0.0)))) -FlonumPosZero] + [(~var i (3d (lambda (x) (eq? x -0.0)))) -FlonumNegZero] + [(~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) (eq? x 0.0f0)))) -SingleFlonumPosZero] + [(~var i (3d (lambda (x) (eq? x -0.0f0)))) -SingleFlonumNegZero] + [(~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))))))) + -InexactComplex] + [(~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))))] + [(HeterogenousVector: ts) + (make-HeterogenousVector + (for/list ([l (in-vector (syntax-e #'i))] + [t (in-list ts)]) + (tc-literal l t)))] + ;; errors are handled elsewhere + [_ (make-HeterogenousVector (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)))))] + [_ (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])) + + (if expected + (check-below r expected) + r)) ;; do-inst : syntax type -> type