Sequenceof type.

- inferencing and subtyping relation with vectors, lists, etc
- use in `make-sequence'
- add tests

collects/tests/typed-scheme/succeed/for-seq.rkt

@@ -0,0 +1,19 @@
+#lang typed/racket
+
+(: Approximate (Natural -> Void))
+(define (Approximate n) ; works
+ (for: : Void ([i : Integer (in-range 10)])
+     (display i)))
+
+(for: : Void ((i : Integer (ann '(1 2 3) (Sequenceof Integer))) ; doesn't
+             (j : Char "abc"))
+     (display (list i j)))
+
+
+(for: : Void ; doesn't
+     ([from-to : (List Symbol Symbol)
+               (ann '([a t] [c g]) (Sequenceof (List Symbol Symbol)))])
+     #t)
+
+
+(for/list: : (Listof Integer) ([i : Integer (in-range 10)]) i) ; works

collects/typed-scheme/infer/infer-unit.rkt

@@ -341,6 +341,29 @@
                (fail! S T))]
           [((Pair: a b) (Pair: a* b*))
            (cset-meet (cg a a*) (cg b b*))]
+          ;; sequences are covariant
+          [((Sequence: ts) (Sequence: ts*))
+           (cgen/list V X ts ts*)]
+          [((Listof: t) (Sequence: (list t*)))
+           (cg t t*)]
+          [((List: ts) (Sequence: (list t*)))
+           (cset-meet* (for/list ([t (in-list ts)])
+                         (cg t t*)))]
+          [((HeterogenousVector: ts) (Sequence: (list t*)))
+           (cset-meet* (for/list ([t (in-list ts)])
+                         (cg t t*)))]
+          [((Vector: t) (Sequence: (list t*)))
+           (cg t t*)]
+          [((Base: 'String _) (Sequence: (list t*)))
+           (cg -Char t*)]
+          [((Base: 'Bytes _) (Sequence: (list t*)))
+           (cg -Nat t*)]
+          [((Base: 'Input-Port _) (Sequence: (list t*)))
+           (cg -Nat t*)]
+          [((Vector: t) (Sequence: (list t*)))
+           (cg t t*)]
+          [((Hashtable: k v) (Sequence: (list k* v*)))
+           (cgen/list V X (list k v) (list k* v*))]
           ;; if we have two mu's, we rename them to have the same variable
           ;; and then compare the bodies
           [((Mu-unsafe: s) (Mu-unsafe: t)) 
@@ -386,7 +409,7 @@
              (move-vars-to-dmap new-cset dbound vars))]
           [((ValuesDots: ss s-dty dbound) (ValuesDots: ts t-dty dbound))
            (when (memq dbound X) (fail! ss ts))          
-           (cgen/list V X (cons s-dty ss) (cons t-dty ts))]
+           (cgen/list V X (cons s-dty ss) (cons t-dty ts))]          
           [((Vector: e) (Vector: e*))
            (cset-meet (cg e e*) (cg e* e))]
           [((Box: e) (Box: e*))

collects/typed-scheme/private/base-special-env.rkt

@@ -160,6 +160,8 @@
                              (-> Univ Univ)
                              (-> a Univ)
                              (-> Univ a Univ))))])
+            (-> Univ (-seq a) (seq-vals))
+            #;
             (cl->* (-> Univ (-lst a) (seq-vals))
                    (-> Univ (-vec a) (seq-vals))
                    (-> Univ -String (seq-vals -Char))

collects/typed-scheme/private/base-types-new.rkt

@@ -50,4 +50,5 @@
 [Nothing (Un)]
 [Pairof (-poly (a b) (-pair a b))]
 [MPairof (-poly (a b) (-mpair a b))]
+[Sequenceof (-poly (a) (-seq a))]
 

collects/typed-scheme/rep/type-rep.rkt

@@ -335,6 +335,13 @@
 ;; cls : Class
 (dt Instance ([cls Type/c]) [#:key 'instance])
 
+;; sequences
+;; includes lists, vectors, etc
+;; tys : sequence produces this set of values at each step
+(dt Sequence ([tys (listof Type/c)])
+    [#:frees (λ (f) (combine-frees (map f tys)))]
+    [#:key #f] [#:fold-rhs (*Sequence (map type-rec-id tys))])
+
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 
 ;; Ugly hack - should use units

collects/typed-scheme/types/abbrev.rkt

@@ -27,6 +27,7 @@
 (define -Param make-Param)
 (define -box make-Box)
 (define -vec make-Vector)
+(define (-seq . args) (make-Sequence args))
 
 (define-syntax *Un
   (syntax-rules ()

collects/typed-scheme/types/printer.rkt

@@ -211,6 +211,10 @@
     [(Result: t fs lo) (fp "(~a : ~a : ~a)" t fs lo)]
     [(Refinement: parent p? _)
      (fp "(Refinement ~a ~a)" parent (syntax-e p?))]
+    [(Sequence: ts)
+     (fp "(Sequenceof")
+     (for ([t ts]) (fp " ~a" t))
+     (fp ")")]
     [(Error:) (fp "Error")]
     [else (fp "(Unknown Type: ~a)" (struct->vector c))]
     ))

collects/typed-scheme/types/subtype.rkt

@@ -256,7 +256,26 @@
 	      [((Value: (? symbol? n)) (Base: 'Symbol _)) A0]
 	      [((Value: (? string? n)) (Base: 'String _)) A0]
 	      ;; tvars are equal if they are the same variable
-	      [((F: t) (F: t*)) (if (eq? t t*) A0 (fail! s t))]
+	      [((F: t) (F: t*)) (if (eq? t t*) A0 (fail! s t))]              
+              ;; sequences are covariant
+              [((Sequence: ts) (Sequence: ts*))
+               (subtypes* A0 ts ts*)]
+              [((Listof: t) (Sequence: (list t*)))
+               (subtype* A0 t t*)]
+              [((List: ts) (Sequence: (list t*)))
+               (subtypes* A0 ts (map (λ _ t*) ts))]
+              [((HeterogenousVector: ts) (Sequence: (list t*)))
+               (subtypes* A0 ts (map (λ _ t*) ts))]
+              [((Vector: t) (Sequence: (list t*)))
+               (subtype* A0 t t*)]
+              [((Base: 'String _) (Sequence: (list t*)))
+               (subtype* A0 -Char t*)]
+              [((Base: 'Bytes _) (Sequence: (list t*)))
+               (subtype* A0 -Nat t*)]
+              [((Base: 'Input-Port _) (Sequence: (list t*)))
+               (subtype* A0 -Nat t*)]
+              [((Hashtable: k v) (Sequence: (list k* v*)))
+               (subtypes* A0 (list k v) (list k* v*))]
               ;; special-case for case-lambda/union
               [((Function: arr1) (Function: (list arr2)))
                (when (null? arr1) (fail! s t))