diff --git a/collects/typed-scheme/private/base-types-extra.rkt b/collects/typed-scheme/private/base-types-extra.rkt index f76ca4e7..de39e172 100644 --- a/collects/typed-scheme/private/base-types-extra.rkt +++ b/collects/typed-scheme/private/base-types-extra.rkt @@ -12,7 +12,7 @@ ;; special type names that are not bound to particular types (define-other-types - -> U Rec All Opaque + -> U Rec All Opaque Vector Parameterof List Class Values Instance Refinement pred) diff --git a/collects/typed-scheme/private/parse-type.rkt b/collects/typed-scheme/private/parse-type.rkt index 14937262..77287839 100644 --- a/collects/typed-scheme/private/parse-type.rkt +++ b/collects/typed-scheme/private/parse-type.rkt @@ -99,7 +99,7 @@ (syntax-parse stx #:literals (t:Class t:Refinement t:Instance t:List cons t:pred t:-> : case-lambda - t:Rec t:U t:All t:Opaque t:Parameter quote) + t:Rec t:U t:All t:Opaque t:Parameter t:Vector quote) [t #:declare t (3d Type?) (attribute t.datum)] @@ -136,6 +136,9 @@ [((~and kw t:List) ts ...) (add-type-name-reference #'kw) (-Tuple (map parse-type (syntax->list #'(ts ...))))] + [((~and kw t:Vector) ts ...) + (add-type-name-reference #'kw) + (make-HeterogenousVector (map parse-type (syntax->list #'(ts ...))))] [((~and kw cons) fst rst) (add-type-name-reference #'kw) (-pair (parse-type #'fst) (parse-type #'rst))] diff --git a/collects/typed-scheme/rep/type-rep.rkt b/collects/typed-scheme/rep/type-rep.rkt index 49596a8a..4a076230 100644 --- a/collects/typed-scheme/rep/type-rep.rkt +++ b/collects/typed-scheme/rep/type-rep.rkt @@ -76,6 +76,12 @@ [#:frees (make-invariant (free-vars* elem)) (make-invariant (free-idxs* elem))] [#:key 'vector]) +;; elems are all Types +(dt HeterogenousVector ([elems (listof Type/c)]) + [#:frees (make-invariant (combine-frees (map free-vars* elems))) (make-invariant (combine-frees (map free-idxs* elems)))] + [#:key 'vector] + [#:fold-rhs (*HeterogenousVector (map type-rec-id elems))]) + ;; elem is a Type (dt Box ([elem Type/c]) [#:frees (make-invariant (free-vars* elem)) (make-invariant (free-idxs* elem))] [#:key 'box]) diff --git a/collects/typed-scheme/typecheck/tc-app.rkt b/collects/typed-scheme/typecheck/tc-app.rkt index cfe72ae9..bc429eca 100644 --- a/collects/typed-scheme/typecheck/tc-app.rkt +++ b/collects/typed-scheme/typecheck/tc-app.rkt @@ -415,7 +415,7 @@ (syntax-parse form #:literals (#%plain-app #%plain-lambda letrec-values quote values apply k:apply not list list* call-with-values do-make-object make-object cons - andmap ormap reverse extend-parameterization) + andmap ormap reverse extend-parameterization vector-ref) [(#%plain-app extend-parameterization pmz args ...) (let loop ([args (syntax->list #'(args ...))]) (if (null? args) (ret Univ) @@ -430,6 +430,54 @@ [(tc-result1: t) (tc-error/expr #:ret (or expected (ret Univ)) "expected Parameter, but got ~a" t) (loop (cddr args))]))))] + ;; vector-ref on het vectors + [(#%plain-app (~and op vector-ref) v e:expr) + (let ([e-t (single-value #'e)]) + (match (single-value #'v) + [(tc-result1: (and t (HeterogenousVector: es))) + (let ([ival (or (and (number? (syntax-e #'i)) (syntax-e #'i)) + (match e-t + [(tc-result1: (Value: (? number? i))) i] + [_ #f]))]) + (cond [(not ival) + (check-below e-t -Nat) + (if expected + (check-below (apply Un es) expected) + (apply (Un es)))] + [(and (integer? ival) (exact? ival) (<= 0 ival (sub1 (length es)))) + (if expected + (check-below (ret (list-ref es ival)) expected) + (ret (list-ref es ival)))] + [(not (and (integer? ival) (exact? ival))) + (tc-error/expr #:ret (or expected (ret (Un))) "expected exact integer for vector index, but got ~a" ival)] + [(< ival 0) + (tc-error/expr #:ret (or expected (ret (Un))) "index ~a too small for vector ~a" ival t)] + [(not (<= ival (sub1 (length es)))) + (tc-error/expr #:ret (or expected (ret (Un))) "index ~a too large for vector ~a" ival t)]))] + [v-ty + (let ([arg-tys (list v-ty e-t)]) + (tc/funapp #'op #'args (single-value #'op) arg-tys expected))]))] + [(#%plain-app (~literal vector) args:expr ...) + (match expected + [#f + (ret (make-HeterogenousVector (map tc-expr/t (syntax->list #'(args ...)))))] + [(tc-result1: (Vector: t)) + (for ([e (in-list (syntax->list #'(args ...)))]) + (tc-expr/check e t)) + expected] + [(tc-result1: (HeterogenousVector: ts)) + (unless (= (length ts) (length (syntax->list #'(args ...)))) + (tc-error/expr "expected vector with ~a elements, but got ~a" + (length ts) + (make-HeterogenousVector (map tc-expr/t (syntax->list #'(args ...)))))) + (for ([e (in-list (syntax->list #'(args ...)))] + [t (in-list ts)]) + (tc-expr/check e t)) + expected] + [(tc-result1: t) + (tc-error/expr "expected ~a, but got ~a" t (make-HeterogenousVector (map tc-expr/t (syntax->list #'(args ...))))) + expected] + [_ (int-err "bad expected: ~a" expected)])] ;; call-with-values [(#%plain-app call-with-values prod con) (match (tc/funapp #'prod #'() (single-value #'prod) null #f) diff --git a/collects/typed-scheme/typecheck/tc-expr-unit.rkt b/collects/typed-scheme/typecheck/tc-expr-unit.rkt index 7bc7b709..c17ecb00 100644 --- a/collects/typed-scheme/typecheck/tc-expr-unit.rkt +++ b/collects/typed-scheme/typecheck/tc-expr-unit.rkt @@ -62,12 +62,17 @@ (match expected [(Vector: t) (make-Vector (apply Un - (for/list ([l (syntax-e #'i)]) + (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-Vector (apply Un - (for/list ([l (syntax-e #'i)]) - (tc-literal l #f))))])] + [_ (make-HeterogenousVector + (for/list ([l (in-vector (syntax-e #'i))]) + (tc-literal l #f)))])] [(~var i (3d hash?)) (let* ([h (syntax-e #'i)] [ks (hash-map h (lambda (x y) (tc-literal x)))] diff --git a/collects/typed-scheme/types/printer.rkt b/collects/typed-scheme/types/printer.rkt index 6982be45..61d92dd9 100644 --- a/collects/typed-scheme/types/printer.rkt +++ b/collects/typed-scheme/types/printer.rkt @@ -168,6 +168,10 @@ (fp ")")]))] [(arr: _ _ _ _ _) (fp "(arr ") (print-arr c) (fp ")")] [(Vector: e) (fp "(Vectorof ~a)" e)] + [(HeterogenousVector: e) (fp "(Vector") + (for ([i (in-list e)]) + (fp " ~a" i)) + (fp ")")] [(Box: e) (fp "(Boxof ~a)" e)] [(Union: elems) (fp "~a" (cons 'U elems))] [(Pair: l r) (fp "(Pairof ~a ~a)" l r)] diff --git a/collects/typed-scheme/types/subtype.rkt b/collects/typed-scheme/types/subtype.rkt index acb52b14..9cb832da 100644 --- a/collects/typed-scheme/types/subtype.rkt +++ b/collects/typed-scheme/types/subtype.rkt @@ -317,6 +317,9 @@ A0] [((Box: _) (BoxTop:)) A0] [((Vector: _) (VectorTop:)) A0] + [((HeterogenousVector: _) (VectorTop:)) A0] + [((HeterogenousVector: (list e ...)) (Vector: e*)) + (if (andmap (lambda (e0) (type-equal? e0 e*)) e) A0 (fail! s t))] [((MPair: _ _) (MPairTop:)) A0] [((Hashtable: _ _) (HashtableTop:)) A0] ;; subtyping on structs follows the declared hierarchy