From 6f376407d988e9ecf947f1fc60d4e02fc9386b0a Mon Sep 17 00:00:00 2001
From: Asumu Takikawa <asumu@ccs.neu.edu>
Date: Fri, 2 Nov 2012 15:20:45 -0400
Subject: [PATCH] Typecheck prompt tags

original commit: 4b5d6e71fdfe68dea748b296c4427209d54a920f
---
 collects/typed-racket/base-env/base-env.rkt   | 21 ++++++++++++++++---
 collects/typed-racket/base-env/base-types.rkt |  4 ++--
 .../typed-racket/private/type-contract.rkt    |  4 ++++
 collects/typed-racket/rep/type-rep.rkt        |  6 +++---
 collects/typed-racket/types/printer.rkt       |  2 ++
 5 files changed, 29 insertions(+), 8 deletions(-)

diff --git a/collects/typed-racket/base-env/base-env.rkt b/collects/typed-racket/base-env/base-env.rkt
index 5021961f..6a3f31fc 100644
--- a/collects/typed-racket/base-env/base-env.rkt
+++ b/collects/typed-racket/base-env/base-env.rkt
@@ -38,6 +38,7 @@
           make-CustodianBox
           make-HeterogeneousVector
           make-Continuation-Mark-Key
+          make-Prompt-Tag
           make-ListDots))
 
 ;Section 9.2
@@ -593,6 +594,7 @@
                        (make-ListDots a 'a)
                        (-values (list (-pair b (-val '())) -Nat -Nat -Nat)))))]
 
+
 [call/cc (-poly (a b) (((a . -> . (Un)) . -> . b) . -> . (Un a b)))]
 [call/ec (-poly (a b) (((a . -> . (Un)) . -> . b) . -> . (Un a b)))]
 [call-with-current-continuation (-poly (a b) (((a . -> . (Un)) . -> . b) . -> . (Un a b)))]
@@ -2023,9 +2025,22 @@
 [call-with-continuation-barrier (-poly (a) (-> (-> a) a))]
 [continuation-prompt-available? (-> -Prompt-Tag B)]
 
-[make-continuation-prompt-tag (->opt [Sym] -Prompt-Tag)]
-[default-continuation-prompt-tag (-> -Prompt-Tag)]
-[continuation-prompt-tag? (make-pred-ty -Prompt-Tag)]
+[call-with-continuation-prompt
+ (-polydots (a b d c)
+   (cl->*
+    (-> (-> b) (make-Prompt-Tag b (->... '() (c c) d)) (->... '() (c c) d)
+        (Un b d))
+    (-> (-> b) Univ)))]
+[abort-current-continuation
+ (-polydots (a b d e c)
+   (->... (list (make-Prompt-Tag b (->... '() (c c) d))) (c c) e))]
+[call-with-composable-continuation
+ (-polydots (b c a)
+   (cl->*
+    (-> (->... '() (a a) b) (make-Prompt-Tag b c) (make-ValuesDots '() a 'a))))]
+[make-continuation-prompt-tag (-poly (a b) (->opt [Sym] (make-Prompt-Tag a b)))]
+[default-continuation-prompt-tag (-> (make-Prompt-Tag Univ (-> ManyUniv Univ)))]
+;[continuation-prompt-tag? (make-pred-ty -Prompt-Tag)]
 [dynamic-wind (-poly (a) (-> (-> ManyUniv) (-> a) (-> ManyUniv) a))]
 
 ;Section 9.5 (Continuation Marks)
diff --git a/collects/typed-racket/base-env/base-types.rkt b/collects/typed-racket/base-env/base-types.rkt
index 01b30286..fd618e94 100644
--- a/collects/typed-racket/base-env/base-types.rkt
+++ b/collects/typed-racket/base-env/base-types.rkt
@@ -143,7 +143,6 @@
 [Place-Channel -Place-Channel]
 [Place -Place]
 [Will-Executor -Will-Executor]
-[Prompt-Tag -Prompt-Tag]
 
 
 [Listof -Listof]
@@ -170,4 +169,5 @@
 [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
+[Continuation-Mark-Key (-poly (a) (make-Continuation-Mark-Key a))]
+[Prompt-Tag (-poly (a b) (make-Prompt-Tag a b))]
\ No newline at end of file
diff --git a/collects/typed-racket/private/type-contract.rkt b/collects/typed-racket/private/type-contract.rkt
index 60b1c1af..75ab85f7 100644
--- a/collects/typed-racket/private/type-contract.rkt
+++ b/collects/typed-racket/private/type-contract.rkt
@@ -342,6 +342,10 @@
         [(Continuation-Mark-Key: t)
          (set-chaperone!)
          #`(continuation-mark-key/c #,(t->c t))]
+        ;; TODO: this is not quite right for case->
+        [(Prompt-Tag: s (Function: (list (arr: (list ts ...) _ _ _ _))))
+         (set-chaperone!)
+         #`(prompt-tag/c #,@(map t->c ts) #:call/cc #,(t->c s))]
         ;; TODO
         [(F: v) (cond [(assoc v (vars)) => second]
                       [else (int-err "unknown var: ~a" v)])]
diff --git a/collects/typed-racket/rep/type-rep.rkt b/collects/typed-racket/rep/type-rep.rkt
index ec1f1493..54f2cb9c 100644
--- a/collects/typed-racket/rep/type-rep.rkt
+++ b/collects/typed-racket/rep/type-rep.rkt
@@ -415,9 +415,9 @@
 ;;   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))))])
+  [#:frees (λ (f) (combine-frees (list (make-invariant (f body))
+                                       (make-invariant (f handler)))))]
+  [#:key 'prompt-tag])
 
 ;; value: the type of allowable values
 (def-type Continuation-Mark-Key ([value Type/c])  
diff --git a/collects/typed-racket/types/printer.rkt b/collects/typed-racket/types/printer.rkt
index dedc4e23..f1c8d93d 100644
--- a/collects/typed-racket/types/printer.rkt
+++ b/collects/typed-racket/types/printer.rkt
@@ -281,6 +281,8 @@
     [(Hashtable: k v) (fp "(HashTable ~a ~a)" k v)]
     [(Continuation-Mark-Key: rhs)
      (fp "(Continuation-Mark-Key ~a)" rhs)]
+    [(Prompt-Tag: body handler)
+     (fp "(Prompt-Tag ~a ~a)" body handler)]
     #;[(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))