From 40dbb6389cd22c6f6dff42a20bdf23e32b2ba0d2 Mon Sep 17 00:00:00 2001 From: Sam Tobin-Hochstadt Date: Mon, 24 May 2010 15:39:51 -0700 Subject: [PATCH] First attempts at adding ListDots (and, incidentally, List*) types. --- .../typed-scheme/private/base-types-extra.rkt | 2 +- collects/typed-scheme/private/parse-type.rkt | 43 +++++++++++++++++-- collects/typed-scheme/rep/type-rep.rkt | 11 +++++ collects/typed-scheme/types/abbrev.rkt | 3 ++ collects/typed-scheme/types/printer.rkt | 2 + 5 files changed, 57 insertions(+), 4 deletions(-) diff --git a/collects/typed-scheme/private/base-types-extra.rkt b/collects/typed-scheme/private/base-types-extra.rkt index 43ba28ad41..5e8eef63cb 100644 --- a/collects/typed-scheme/private/base-types-extra.rkt +++ b/collects/typed-scheme/private/base-types-extra.rkt @@ -13,7 +13,7 @@ ;; special type names that are not bound to particular types (define-other-types -> U Rec All Opaque Vector - Parameterof List Class Values Instance Refinement + Parameterof List List* Class Values Instance Refinement pred) (provide (rename-out [All ∀] diff --git a/collects/typed-scheme/private/parse-type.rkt b/collects/typed-scheme/private/parse-type.rkt index 093ac6748a..6e2c4f3e95 100644 --- a/collects/typed-scheme/private/parse-type.rkt +++ b/collects/typed-scheme/private/parse-type.rkt @@ -6,7 +6,7 @@ (utils tc-utils stxclass-util) syntax/stx (prefix-in c: scheme/contract) syntax/parse - (env type-env-structs tvar-env dotted-env type-name-env type-alias-env lexical-env) + (env type-env-structs tvar-env type-name-env type-alias-env lexical-env) scheme/match unstable/debug (for-template scheme/base "colon.ss") ;; needed at this phase for tests @@ -111,7 +111,7 @@ (parameterize ([current-orig-stx stx]) (syntax-parse stx - #:literals (t:Class t:Refinement t:Instance t:List cons t:pred t:-> : case-lambda + #:literals (t:Class t:Refinement t:Instance t:List t:List* cons t:pred t:-> : case-lambda t:Rec t:U t:All t:Opaque t:Parameter t:Vector quote) [t #:declare t (3d Type?) @@ -148,7 +148,10 @@ (make-Instance v)))] [((~and kw t:List) ts ...) (add-type-name-reference #'kw) - (-Tuple (map parse-type (syntax->list #'(ts ...))))] + (parse-list-type stx)] + [((~and kw t:List*) ts ... t) + (add-type-name-reference #'kw) + (-Tuple* (map parse-type (syntax->list #'(ts ...))) (parse-type #'t))] [((~and kw t:Vector) ts ...) (add-type-name-reference #'kw) (make-HeterogenousVector (map parse-type (syntax->list #'(ts ...))))] @@ -346,6 +349,40 @@ (-val (syntax-e #'t))] [_ (tc-error "not a valid type: ~a" (syntax->datum stx))]))) +(define (parse-list-type stx) + (parameterize ([current-orig-stx stx]) + (syntax-parse stx #:literals (t:List) + [((~and kw t:List) tys ... dty :ddd/bound) + (add-type-name-reference #'kw) + (let ([var (lookup (current-tvars) (syntax-e #'bound) (lambda (_) #f))]) + (if (not (Dotted? var)) + (tc-error/stx #'bound "Used a type variable (~a) not bound with ... as a bound on a ..." (syntax-e #'bound)) + (-Tuple* (map parse-type (syntax->list #'(tys ...))) + (make-ListDots + (parameterize ([current-tvars (extend-env (list (syntax-e #'bound)) + (list (make-DottedBoth (make-F (syntax-e #'bound)))) + (current-tvars))]) + (parse-type #'dty)) + (syntax-e #'bound)))))] + [((~and kw t:List) tys ... dty _:ddd) + (add-type-name-reference #'kw) + (let ([bounds (env-keys+vals (env-filter (compose Dotted? cdr) (current-tvars)))]) + (when (null? bounds) + (tc-error/stx stx "No type variable bound with ... in scope for ... type")) + (unless (null? (cdr bounds)) + (tc-error/stx stx "Cannot infer bound for ... type")) + (match-let ([(cons var (struct Dotted (t))) (car bounds)]) + (-Tuple* (map parse-type (syntax->list #'(tys ...))) + (make-ListDots + (parameterize ([current-tvars (extend-env (list var) + (list (make-DottedBoth t)) + (current-tvars))]) + (parse-type #'dty)) + var))))] + [((~and kw t:List) tys ...) + (add-type-name-reference #'kw) + (-Tuple (map parse-type (syntax->list #'(tys ...))))]))) + (define (parse-values-type stx) (parameterize ([current-orig-stx stx]) (syntax-parse stx #:literals (values t:All) diff --git a/collects/typed-scheme/rep/type-rep.rkt b/collects/typed-scheme/rep/type-rep.rkt index 5c9df27563..b1f825fe4f 100644 --- a/collects/typed-scheme/rep/type-rep.rkt +++ b/collects/typed-scheme/rep/type-rep.rkt @@ -66,6 +66,11 @@ ;; left and right are Types (dt Pair ([left Type/c] [right Type/c]) [#:key 'pair]) +;; dotted list -- after expansion, becomes normal Pair-based list type +(dt ListDots ([dty Type/c] [dbound (or/c symbol? natural-number/c)]) + [#:frees (λ (f) (f dty))] + [#:fold-rhs (*ListDots (type-rec-id dty) dbound)]) + ;; *mutable* pairs - distinct from regular pairs ;; left and right are Types (dt MPair ([left Type/c] [right Type/c]) [#:key 'mpair]) @@ -442,6 +447,9 @@ (*ValuesDots (map sb rs) (sb dty) (if (eq? dbound name) (+ count outer) dbound))] + [#:ListDots dty dbound + (*ListDots (sb dty) + (if (eq? dbound name) (+ count outer) dbound))] [#:Mu (Scope: body) (*Mu (*Scope (loop (add1 outer) body)))] [#:PolyDots n body* (let ([body (remove-scopes n body*)]) @@ -490,6 +498,9 @@ (*ValuesDots (map sb rs) (sb dty) (if (eqv? dbound (+ count outer)) (F-n image) dbound))] + [#:ListDots dty dbound + (*ListDots (sb dty) + (if (eqv? dbound (+ count outer)) (F-n image) dbound))] [#:Mu (Scope: body) (*Mu (*Scope (loop (add1 outer) body)))] [#:PolyDots n body* (let ([body (remove-scopes n body*)]) diff --git a/collects/typed-scheme/types/abbrev.rkt b/collects/typed-scheme/types/abbrev.rkt index d760dd9d1a..c2608c17e6 100644 --- a/collects/typed-scheme/types/abbrev.rkt +++ b/collects/typed-scheme/types/abbrev.rkt @@ -45,6 +45,9 @@ (define (-Tuple l) (foldr -pair (-val '()) l)) +(define (-Tuple* l b) + (foldr -pair b l)) + (define (untuple t) (match (resolve t) [(Value: '()) null] diff --git a/collects/typed-scheme/types/printer.rkt b/collects/typed-scheme/types/printer.rkt index 1892423e36..ebfe338878 100644 --- a/collects/typed-scheme/types/printer.rkt +++ b/collects/typed-scheme/types/printer.rkt @@ -171,6 +171,8 @@ [(Channel: e) (fp "(Channelof ~a)" e)] [(Union: elems) (fp "~a" (cons 'U elems))] [(Pair: l r) (fp "(Pairof ~a ~a)" l r)] + [(ListDots: dty dbound) + (fp "(List ~a ...~a~a)" dty (if (special-dots-printing?) "" " ") dbound)] [(F: nm) (fp "~a" nm)] ;; FIXME [(Values: (list v)) (fp "~a" v)]