mostly done with heterogenous vectors

original commit: 2c03f2223b55483bc02d66946097ed17e63529f3
This commit is contained in:
Sam Tobin-Hochstadt 2010-05-10 19:17:42 -04:00
parent 15b1f6378b
commit 2fdcb1ef9a
7 changed files with 76 additions and 7 deletions

View File

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

View File

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

View File

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

View File

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

View File

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

View File

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

View File

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