Speed up and improve tc-literal. Now uses expected types more, and more sensibly.

Closes PR 12586.
This commit is contained in:
Sam Tobin-Hochstadt 2012-02-20 13:19:53 -05:00
parent 74c9265d66
commit a8bdb9d6ce
5 changed files with 117 additions and 112 deletions

View File

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

View File

@ -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
(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))
;; 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)))]
[((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
[_ #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
[else (if (eq? f 'new) t2 t1)])) ;; t2 and t1 have a complex relationship, so we punt
(define restrict restrict*)

View File

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

View File

@ -23,15 +23,10 @@
(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))
(define r
(syntax-parse v-stx
[i:exp expected]
[i:boolean (-val (syntax-e #'i))]
[i:identifier (-val (syntax-e #'i))]
@ -78,20 +73,23 @@
[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)))]
[(~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
[_ (-Tuple
(for/list ([l (in-list (syntax->list #'(i ...)))])
(tc-literal l #f)))])]
[t
(-pair (tc-literal #'i) (tc-literal #'r))])]
[(~var i (3d vector?))
(match expected
(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)
@ -113,9 +111,12 @@
[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]))
(if expected
(check-below r expected)
r))
;; do-inst : syntax type -> type
(define (do-inst stx ty)