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

Starting on control typing.

Browse Source
This commit is contained in:
Sam Tobin-Hochstadt 2012-10-31 15:57:39 -04:00 committed by Asumu Takikawa
parent b3b56fa3c8
commit 29d54fb0d0
6 changed files with 74 additions and 13 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

22
collects/typed-racket/base-env/base-env.rkt
View File

@ -37,6 +37,7 @@
make-Ephemeron
make-CustodianBox
make-HeterogeneousVector
make-Continuation-Mark-Key
make-ListDots))
;Section 9.2
@ -2031,11 +2032,26 @@
;continuation-marks needs type for continuations as other possible first argument
[continuation-marks (->opt (Un (-val #f) -Thread) [-Prompt-Tag] -Cont-Mark-Set)]
[current-continuation-marks (->opt [-Prompt-Tag] -Cont-Mark-Set)]
[continuation-mark-set->list (->opt -Cont-Mark-Set Univ [-Prompt-Tag] (-lst Univ))]
[continuation-mark-set->list* (->opt -Cont-Mark-Set (-lst Univ) [Univ -Prompt-Tag] (-lst (-vec Univ)))]
[continuation-mark-set-first (->opt (-opt -Cont-Mark-Set) Univ [Univ -Prompt-Tag] Univ)]
[continuation-mark-set->list
(-poly (a)
(cl->*
(->opt -Cont-Mark-Set (make-Continuation-Mark-Key a) [-Prompt-Tag] (-lst a))
(->opt -Cont-Mark-Set Univ [-Prompt-Tag] (-lst Univ))))]
[continuation-mark-set->list*
(-poly (a b)
(cl->*
(->opt -Cont-Mark-Set (-lst (make-Continuation-Mark-Key a)) [b -Prompt-Tag]
(-lst (-vec (Un a b))))
(->opt -Cont-Mark-Set (-lst Univ) [Univ -Prompt-Tag] (-lst (-vec Univ)))))]
[continuation-mark-set-first
(-poly (a b)
(cl->*
(->opt (-opt -Cont-Mark-Set) (make-Continuation-Mark-Key a) [b -Prompt-Tag]
(Un a b))
(->opt (-opt -Cont-Mark-Set) Univ [Univ -Prompt-Tag] Univ)))]
[call-with-immediate-continuation-mark (-poly (a) (->opt Univ (-> Univ a) [Univ] a))]
[continuation-mark-set? (make-pred-ty -Cont-Mark-Set)]
[make-continuation-mark-key (-poly (a) (->opt [-Symbol] (make-Continuation-Mark-Key a)))]
[continuation-mark-set->context (-> -Cont-Mark-Set (-lst (-pair (-opt Sym) Univ)))] ;TODO add srcloc

1
collects/typed-racket/base-env/base-types.rkt
View File

@ -170,3 +170,4 @@
[Thread-Cellof (-poly (a) (-thread-cell a))]
[Custodian-Boxof (-poly (a) (make-CustodianBox a))]
[Continuation-Mark-Key (-poly (a) (make-Continuation-Mark-Key a))]

4
collects/typed-racket/infer/infer-unit.rkt
View File

@ -535,6 +535,10 @@
(cset-meet (cg e e*) (cg e* e))]
[((ThreadCell: e) (ThreadCell: e*))
(cset-meet (cg e e*) (cg e* e))]
[((Continuation-Mark-Key: e) (Continuation-Mark-Key: e*))
(cset-meet (cg e e*) (cg e* e))]
[((Prompt-Tag: s t) (Prompt-Tag: s* t*))
(cset-meet* (list (cg s s*) (cg s* s) (cg t t*) (cg t* t)))]
[((Promise: e) (Promise: e*))
(cg e e*)]
[((Ephemeron: e) (Ephemeron: e*))

14
collects/typed-racket/rep/type-rep.rkt
View File

@ -410,6 +410,20 @@
(def-type Future ([t Type/c]) [#:key 'future])
;; body: the type of the body
;; handler: the type of the prompt handler
;; prompts with this tag will return a union of `body`
;; and the codomains of `handler`
(def-type Prompt-Tag ([body Type/c] [handler Function?])
[#:key 'prompt-tag]
[#:frees (λ (f) (combine-frees (make-invariant (f body))
(make-invariant (f handler))))])
;; value: the type of allowable values
(def-type Continuation-Mark-Key ([value Type/c])
[#:frees (λ (f) (make-invariant (f value)))]
[#:key 'continuation-mark-key])
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; remove-dups: List[Type] -> List[Type]

43
collects/typed-racket/typecheck/tc-expr-unit.rkt
View File

@ -14,9 +14,9 @@
(env lexical-env type-env-structs tvar-env index-env)
racket/private/class-internal
(except-in syntax/parse id)
unstable/function #;unstable/debug
unstable/function #;unstable/debug
(only-in srfi/1 split-at)
(for-template "internal-forms.rkt"))
(for-template "internal-forms.rkt" (only-in '#%paramz [parameterization-key pz:pk])))
(require (for-template racket/base racket/private/class-internal))
@ -323,12 +323,27 @@
(ret -Variable-Reference)]
;; identifiers
[x:identifier
(check-below (tc-id #'x) expected)]
(check-below (tc-id #'x) expected)]
;; w-c-m
[(with-continuation-mark e1 e2 e3)
(begin (tc-expr/check/type #'e1 Univ)
(tc-expr/check/type #'e2 Univ)
(tc-expr/check #'e3 expected))]
(define key-t (single-value #'e1))
(match key-t
[(tc-result1: (Continuation-Mark-Key: rhs))
(tc-expr/check/type #'e2 rhs)
(tc-expr/check #'e3 expected)]
[(? (λ _ (and (identifier? #'e1)
(free-identifier=? #'pz:pk #'e1))))
(tc-expr/check/type #'e2 Univ)
(tc-expr/check #'e3 expected)]
[(tc-result1: key-t)
;(check-below key-t -Symbol)
;; FIXME -- would need to protect `e2` with any-wrap/c contract
;; instead, just fail
;(tc-expr/check/type #'e2 Univ)
;(tc-expr/check #'e3 expected)
(tc-error/expr "with-continuation-mark requires a continuation-mark-key, but got ~a" key-t
#:return expected)])]
;; application
[(#%plain-app . _) (tc/app/check form expected)]
;; #%expression
@ -417,9 +432,19 @@
[(quote-syntax datum) (ret (-Syntax (tc-literal #'datum)) true-filter)]
;; w-c-m
[(with-continuation-mark e1 e2 e3)
(begin (tc-expr/check/type #'e1 Univ)
(tc-expr/check/type #'e2 Univ)
(tc-expr #'e3))]
(define key-t (single-value #'e1))
(match key-t
[(tc-result1: (Continuation-Mark-Key: rhs))
(tc-expr/check/type #'e2 rhs)
(tc-expr #'e3)]
[(? (λ _ (and (identifier? #'e1)
(free-identifier=? #'pz:pk #'e1))))
(tc-expr/check/type #'e2 Univ)
(tc-expr #'e3)]
[(tc-result1: key-t)
;; see comments in the /check variant
(tc-error/expr "with-continuation-mark requires a continuation-mark-key, but got ~a" key-t
#:return (ret (Un)))])]
;; lambda
[(#%plain-lambda formals . body)
(tc/lambda form #'(formals) #'(body))]

3
collects/typed-racket/types/printer.rkt
View File

@ -279,7 +279,8 @@
(fp "(Parameterof ~a)" in)
(fp "(Parameterof ~a ~a)" in out))]
[(Hashtable: k v) (fp "(HashTable ~a ~a)" k v)]
[(Continuation-Mark-Key: rhs)
(fp "(Continuation-Mark-Key ~a)" rhs)]
#;[(Poly-unsafe: n b) (fp "(unsafe-poly ~a ~a ~a)" (Type-seq c) n b)]
[(Poly-names: names body)
#;(eprintf "POLY SEQ: ~a\n" (Type-seq body))