Speed up and improve tc-literal. Now uses expected types more, and more sensibly.
Closes PR 12586. original commit: a8bdb9d6ce5fb03a40f8d1a4caa0cf6d8c392389
This commit is contained in:
Sam Tobin-Hochstadt
parent
4f2353d93f
commit
c681b3c91f
|
|
@ -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"
|
||||
|
|
|
|||
|
|
@ -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*)
|
||||
|
|
|
|||
|
|
@ -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 '()) _)
|
||||
|
|
|
|||
|
|
@ -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)]))
|
||||
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
Loading…
Reference in New Issue
Block a user