From e16c33e1a6fe13bd9992447f3b74f9fafb0f7fb8 Mon Sep 17 00:00:00 2001 From: Sam Tobin-Hochstadt Date: Tue, 8 Jun 2010 19:30:10 -0400 Subject: [PATCH] Sequenceof type. - inferencing and subtyping relation with vectors, lists, etc - use in `make-sequence' - add tests original commit: 78023d08f99bd423a17e532b6ff9b1ded758b658 --- .../tests/typed-scheme/succeed/for-seq.rkt | 19 ++++++++++++++ collects/typed-scheme/infer/infer-unit.rkt | 25 ++++++++++++++++++- .../typed-scheme/private/base-special-env.rkt | 2 ++ .../typed-scheme/private/base-types-new.rkt | 1 + collects/typed-scheme/rep/type-rep.rkt | 7 ++++++ collects/typed-scheme/types/abbrev.rkt | 1 + collects/typed-scheme/types/printer.rkt | 4 +++ collects/typed-scheme/types/subtype.rkt | 21 +++++++++++++++- 8 files changed, 78 insertions(+), 2 deletions(-) create mode 100644 collects/tests/typed-scheme/succeed/for-seq.rkt diff --git a/collects/tests/typed-scheme/succeed/for-seq.rkt b/collects/tests/typed-scheme/succeed/for-seq.rkt new file mode 100644 index 00000000..a5e11bea --- /dev/null +++ b/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 diff --git a/collects/typed-scheme/infer/infer-unit.rkt b/collects/typed-scheme/infer/infer-unit.rkt index 165bcdc3..d45d75d3 100644 --- a/collects/typed-scheme/infer/infer-unit.rkt +++ b/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*)) diff --git a/collects/typed-scheme/private/base-special-env.rkt b/collects/typed-scheme/private/base-special-env.rkt index 6575c55f..c4933663 100644 --- a/collects/typed-scheme/private/base-special-env.rkt +++ b/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)) diff --git a/collects/typed-scheme/private/base-types-new.rkt b/collects/typed-scheme/private/base-types-new.rkt index 98d22dec..84e29ede 100644 --- a/collects/typed-scheme/private/base-types-new.rkt +++ b/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))] diff --git a/collects/typed-scheme/rep/type-rep.rkt b/collects/typed-scheme/rep/type-rep.rkt index 4a076230..49cf247a 100644 --- a/collects/typed-scheme/rep/type-rep.rkt +++ b/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 diff --git a/collects/typed-scheme/types/abbrev.rkt b/collects/typed-scheme/types/abbrev.rkt index 43bcdbbe..9585f9d4 100644 --- a/collects/typed-scheme/types/abbrev.rkt +++ b/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 () diff --git a/collects/typed-scheme/types/printer.rkt b/collects/typed-scheme/types/printer.rkt index ba991333..2b0d2c0b 100644 --- a/collects/typed-scheme/types/printer.rkt +++ b/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))] )) diff --git a/collects/typed-scheme/types/subtype.rkt b/collects/typed-scheme/types/subtype.rkt index 9cb832da..ccaaf720 100644 --- a/collects/typed-scheme/types/subtype.rkt +++ b/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))