suzanne.soy/racket
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

First attempts at adding ListDots (and, incidentally, List*) types.

Browse Source
This commit is contained in:
Sam Tobin-Hochstadt 2010-05-24 15:39:51 -07:00
parent 50f93b9ed7
commit 40dbb6389c
5 changed files with 57 additions and 4 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
collects/typed-scheme/private/base-types-extra.rkt
View File

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

43
collects/typed-scheme/private/parse-type.rkt
View File

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

11
collects/typed-scheme/rep/type-rep.rkt
View File

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

3
collects/typed-scheme/types/abbrev.rkt
View File

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

2
collects/typed-scheme/types/printer.rkt
View File

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