From 6f16d9e2d6429f015f2129cfa93bec278f48dd5f Mon Sep 17 00:00:00 2001
From: Sam Tobin-Hochstadt <samth@racket-lang.org>
Date: Thu, 13 May 2010 18:35:02 -0400
Subject: [PATCH] more sensible version of het vectors. add vector-length,
 vector-set!

original commit: 7ac925695fadf3c8af20b2d65037c8bc6310f9b4
---
 .../tests/typed-scheme/succeed/het-vec2.ss    | 19 +++++++++++
 collects/typed-scheme/private/base-env.rkt    |  2 +-
 collects/typed-scheme/typecheck/tc-app.rkt    | 34 ++++++++++++++++---
 3 files changed, 49 insertions(+), 6 deletions(-)
 create mode 100644 collects/tests/typed-scheme/succeed/het-vec2.ss

diff --git a/collects/tests/typed-scheme/succeed/het-vec2.ss b/collects/tests/typed-scheme/succeed/het-vec2.ss
new file mode 100644
index 00000000..3531b980
--- /dev/null
+++ b/collects/tests/typed-scheme/succeed/het-vec2.ss
@@ -0,0 +1,19 @@
+#lang typed/racket
+
+(ann (vector 1 2 3) (U String (Vector Integer Integer Integer) (Vectorof Number)))
+
+(define v (ann (vector 1 2 3) (Vector Integer Integer Integer)))
+
+(vector-ref v 2)
+(vector-ref v 0)
+(define: x : Natural 0)
+(define: x* : 0 0)
+
+(vector-ref (vector 1 2 3) x)
+(vector-ref v x*)
+
+;(vector-set! v x 7)
+(vector-set! v x* 7)
+
+
+(vector-length v)
diff --git a/collects/typed-scheme/private/base-env.rkt b/collects/typed-scheme/private/base-env.rkt
index 60bfa34e..7ec93a66 100644
--- a/collects/typed-scheme/private/base-env.rkt
+++ b/collects/typed-scheme/private/base-env.rkt
@@ -362,7 +362,7 @@
 
 [vector->list (-poly (a) (-> (-vec a) (-lst a)))]
 [list->vector (-poly (a) (-> (-lst a) (-vec a)))]
-[vector-length (-poly (a) ((-vec a) . -> . -Nat))]
+[vector-length ((make-VectorTop) . -> . -Nat)]
 [vector (-poly (a) (->* (list) a (-vec a)))]
 [vector-immutable (-poly (a) (->* (list) a (-vec a)))]
 [vector->immutable-vector (-poly (a) (-> (-vec a) (-vec a)))]
diff --git a/collects/typed-scheme/typecheck/tc-app.rkt b/collects/typed-scheme/typecheck/tc-app.rkt
index 08ec7707..a7fe1749 100644
--- a/collects/typed-scheme/typecheck/tc-app.rkt
+++ b/collects/typed-scheme/typecheck/tc-app.rkt
@@ -431,7 +431,7 @@
                 (tc-error/expr #:return (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)
+    [(#%plain-app (~and op (~literal vector-ref)) v e:expr)
      (let ([e-t (single-value #'e)])
        (match (single-value #'v)
          [(tc-result1: (and t (HeterogenousVector: es)))
@@ -457,10 +457,34 @@
          [v-ty
           (let ([arg-tys (list v-ty e-t)])
             (tc/funapp #'op #'args (single-value #'op) arg-tys expected))]))]
+    [(#%plain-app (~and op (~literal vector-set!)) v e:expr val:expr)
+     (let ([e-t (single-value #'e)])
+       (match (single-value #'v)
+         [(tc-result1: (and t (HeterogenousVector: es)))
+          (let ([ival (or (syntax-parse #'e [((~literal quote) i:number) (syntax-e #'i)] [_ #f])
+                          (match e-t
+                            [(tc-result1: (Value: (? number? i))) i]
+                            [_ #f]))])
+            (cond [(not ival)
+                   (tc-error/expr #:stx #'e
+                                  #:return (or expected (ret -Void))
+                                  "expected statically known index for heterogenous vector, but got ~a" (match e-t [(tc-result1: t) t]))]
+                  [(and (integer? ival) (exact? ival) (<= 0 ival (sub1 (length es))))
+                   (tc-expr/check #'val (ret (list-ref es ival)))
+                   (if expected 
+                       (check-below (ret -Void) expected)
+                       (ret -Void))]
+                  [(not (and (integer? ival) (exact? ival)))
+                   (tc-error/expr #:stx #'e #:return (or expected (ret (Un))) "expected exact integer for vector index, but got ~a" ival)]
+                  [(< ival 0)
+                   (tc-error/expr #:stx #'e #:return (or expected (ret (Un))) "index ~a too small for vector ~a" ival t)]
+                  [(not (<= ival (sub1 (length es))))
+                   (tc-error/expr #:stx #'e #:return (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 (~and op (~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 (ret t)))
@@ -474,10 +498,10 @@
               [t (in-list ts)])
           (tc-expr/check e (ret t)))
         expected]
-       [(tc-result1: t)
+       [(or #f (tc-result1: _))
         (let ([arg-tys (map single-value (syntax->list #'(args ...)))])
             (tc/funapp #'op #'(args ...) (single-value #'op) arg-tys expected))
-        #;
+        #;#;
         (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)])]