From 06f43b2f4135ff573463f9168d8fcbc6768893d4 Mon Sep 17 00:00:00 2001 From: Asumu Takikawa Date: Mon, 5 Nov 2012 14:31:17 -0500 Subject: [PATCH] Add Top types for prompt tags and mark keys original commit: 41b59cb46a4b6f6d30cd57f0586fe73f79ef7584 --- collects/typed-racket/base-env/base-env.rkt | 25 ++++++++++++--------- collects/typed-racket/rep/type-rep.rkt | 3 +++ collects/typed-racket/types/abbrev.rkt | 1 - collects/typed-racket/types/printer.rkt | 2 ++ collects/typed-racket/types/subtype.rkt | 4 ++++ 5 files changed, 23 insertions(+), 12 deletions(-) diff --git a/collects/typed-racket/base-env/base-env.rkt b/collects/typed-racket/base-env/base-env.rkt index 6a3f31fc..5eb06017 100644 --- a/collects/typed-racket/base-env/base-env.rkt +++ b/collects/typed-racket/base-env/base-env.rkt @@ -38,7 +38,9 @@ make-CustodianBox make-HeterogeneousVector make-Continuation-Mark-Key + make-Continuation-Mark-KeyTop make-Prompt-Tag + make-Prompt-TagTop make-ListDots)) ;Section 9.2 @@ -2023,7 +2025,7 @@ ;Section 9.4 (Continuations) [call-with-continuation-barrier (-poly (a) (-> (-> a) a))] -[continuation-prompt-available? (-> -Prompt-Tag B)] +[continuation-prompt-available? (-> (make-Prompt-TagTop) B)] [call-with-continuation-prompt (-polydots (a b d c) @@ -2039,33 +2041,34 @@ (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)] +;[default-continuation-prompt-tag (-> (make-Prompt-Tag Univ (-> ManyUniv Univ)))] +[continuation-prompt-tag? (make-pred-ty (make-Prompt-TagTop))] [dynamic-wind (-poly (a) (-> (-> ManyUniv) (-> a) (-> ManyUniv) a))] ;Section 9.5 (Continuation Marks) ;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-marks (->opt (Un (-val #f) -Thread) [(make-Prompt-TagTop)] -Cont-Mark-Set)] +[current-continuation-marks (->opt [(make-Prompt-TagTop)] -Cont-Mark-Set)] [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))))] + (->opt -Cont-Mark-Set (make-Continuation-Mark-Key a) [(make-Prompt-TagTop)] (-lst a)) + (->opt -Cont-Mark-Set Univ [(make-Prompt-TagTop)] (-lst Univ))))] [continuation-mark-set->list* (-poly (a b) (cl->* - (->opt -Cont-Mark-Set (-lst (make-Continuation-Mark-Key a)) [b -Prompt-Tag] + (->opt -Cont-Mark-Set (-lst (make-Continuation-Mark-Key a)) [b (make-Prompt-TagTop)] (-lst (-vec (Un a b)))) - (->opt -Cont-Mark-Set (-lst Univ) [Univ -Prompt-Tag] (-lst (-vec Univ)))))] + (->opt -Cont-Mark-Set (-lst Univ) [Univ (make-Prompt-TagTop)] (-lst (-vec Univ)))))] [continuation-mark-set-first (-poly (a b) (cl->* (-> (-opt -Cont-Mark-Set) (make-Continuation-Mark-Key a) (-opt a)) - (->opt (-opt -Cont-Mark-Set) (make-Continuation-Mark-Key a) [b -Prompt-Tag] + (->opt (-opt -Cont-Mark-Set) (make-Continuation-Mark-Key a) [b (make-Prompt-TagTop)] (Un a b)) - (->opt (-opt -Cont-Mark-Set) Univ [Univ -Prompt-Tag] Univ)))] + (->opt (-opt -Cont-Mark-Set) Univ [Univ (make-Prompt-TagTop)] Univ)))] [call-with-immediate-continuation-mark (-poly (a) (->opt Univ (-> Univ a) [Univ] a))] +[continuation-mark-key? (make-pred-ty (make-Continuation-Mark-KeyTop))] [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/rep/type-rep.rkt b/collects/typed-racket/rep/type-rep.rkt index 54f2cb9c..2f94ab58 100644 --- a/collects/typed-racket/rep/type-rep.rkt +++ b/collects/typed-racket/rep/type-rep.rkt @@ -323,6 +323,9 @@ (def-type MPairTop () [#:fold-rhs #:base] [#:key 'mpair]) (def-type StructTop ([name Struct?]) [#:key 'struct]) (def-type ThreadCellTop () [#:fold-rhs #:base] [#:key 'thread-cell]) +(def-type Prompt-TagTop () [#:fold-rhs #:base] [#:key 'prompt-tag]) +(def-type Continuation-Mark-KeyTop () + [#:fold-rhs #:base] [#:key 'continuation-mark-key]) ;; v : Racket Value (def-type Value (v) [#:frees #f] [#:fold-rhs #:base] [#:key (cond [(number? v) 'number] diff --git a/collects/typed-racket/types/abbrev.rkt b/collects/typed-racket/types/abbrev.rkt index 30e8258a..449fce6b 100644 --- a/collects/typed-racket/types/abbrev.rkt +++ b/collects/typed-racket/types/abbrev.rkt @@ -144,7 +144,6 @@ (conjoin compiled-expression? (negate compiled-module-expression?)) #'-Compiled-Non-Module-Expression)) (define -Compiled-Expression (Un -Compiled-Module-Expression -Compiled-Non-Module-Expression)) -(define -Prompt-Tag (make-Base 'Prompt-Tag #'continuation-prompt-tag? continuation-prompt-tag? #'-Prompt-Tag)) (define -Cont-Mark-Set (make-Base 'Continuation-Mark-Set #'continuation-mark-set? continuation-mark-set? #'-Cont-Mark-Set)) (define -Path (make-Base 'Path #'path? path? #'-Path)) (define -OtherSystemPath (make-Base 'OtherSystemPath diff --git a/collects/typed-racket/types/printer.rkt b/collects/typed-racket/types/printer.rkt index f1c8d93d..f0c69dd5 100644 --- a/collects/typed-racket/types/printer.rkt +++ b/collects/typed-racket/types/printer.rkt @@ -226,6 +226,8 @@ [(ThreadCellTop:) (fp "ThreadCell")] [(VectorTop:) (fp "Vector")] [(MPairTop:) (fp "MPair")] + [(Prompt-TagTop:) (fp "Prompt-Tag")] + [(Continuation-Mark-KeyTop:) (fp "Continuation-Mark-Key")] [(App: rator rands stx) (fp "~a" (list* rator rands))] ;; special cases for lists diff --git a/collects/typed-racket/types/subtype.rkt b/collects/typed-racket/types/subtype.rkt index cae93039..cd2bbcc3 100644 --- a/collects/typed-racket/types/subtype.rkt +++ b/collects/typed-racket/types/subtype.rkt @@ -421,6 +421,10 @@ (if (andmap (lambda (e0) (type-equal? e0 e*)) e) A0 (fail! s t))] [((MPair: _ _) (MPairTop:)) A0] [((Hashtable: _ _) (HashtableTop:)) A0] + ;; TODO: subtyping for two `Prompt-Tagof`s with recursive types + ;; may be rejected unnecessarily + [((Prompt-Tag: _ _) (Prompt-TagTop:)) A0] + [((Continuation-Mark-Key: _) (Continuation-Mark-KeyTop:)) A0] ;; subtyping on structs follows the declared hierarchy [((Struct: nm (? Type? parent) _ _ _ _) other) ;(dprintf "subtype - hierarchy : ~a ~a ~a\n" nm parent other)