From 29d54fb0d0650c62abf05729674d138c53ffefd8 Mon Sep 17 00:00:00 2001 From: Sam Tobin-Hochstadt Date: Wed, 31 Oct 2012 15:57:39 -0400 Subject: [PATCH] Starting on control typing. --- collects/typed-racket/base-env/base-env.rkt | 22 ++++++++-- collects/typed-racket/base-env/base-types.rkt | 1 + collects/typed-racket/infer/infer-unit.rkt | 4 ++ collects/typed-racket/rep/type-rep.rkt | 14 ++++++ .../typed-racket/typecheck/tc-expr-unit.rkt | 43 +++++++++++++++---- collects/typed-racket/types/printer.rkt | 3 +- 6 files changed, 74 insertions(+), 13 deletions(-) diff --git a/collects/typed-racket/base-env/base-env.rkt b/collects/typed-racket/base-env/base-env.rkt index debd4ba87f..52e9719343 100644 --- a/collects/typed-racket/base-env/base-env.rkt +++ b/collects/typed-racket/base-env/base-env.rkt @@ -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 diff --git a/collects/typed-racket/base-env/base-types.rkt b/collects/typed-racket/base-env/base-types.rkt index 0bc1f7b2f3..01b3028665 100644 --- a/collects/typed-racket/base-env/base-types.rkt +++ b/collects/typed-racket/base-env/base-types.rkt @@ -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))] \ No newline at end of file diff --git a/collects/typed-racket/infer/infer-unit.rkt b/collects/typed-racket/infer/infer-unit.rkt index a529bf6167..2a42733f19 100644 --- a/collects/typed-racket/infer/infer-unit.rkt +++ b/collects/typed-racket/infer/infer-unit.rkt @@ -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*)) diff --git a/collects/typed-racket/rep/type-rep.rkt b/collects/typed-racket/rep/type-rep.rkt index 4d54268f49..ec1f14932e 100644 --- a/collects/typed-racket/rep/type-rep.rkt +++ b/collects/typed-racket/rep/type-rep.rkt @@ -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] diff --git a/collects/typed-racket/typecheck/tc-expr-unit.rkt b/collects/typed-racket/typecheck/tc-expr-unit.rkt index c3fa034850..84c458fcf0 100644 --- a/collects/typed-racket/typecheck/tc-expr-unit.rkt +++ b/collects/typed-racket/typecheck/tc-expr-unit.rkt @@ -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))] diff --git a/collects/typed-racket/types/printer.rkt b/collects/typed-racket/types/printer.rkt index 56b9420193..dedc4e230f 100644 --- a/collects/typed-racket/types/printer.rkt +++ b/collects/typed-racket/types/printer.rkt @@ -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))