Add call/cc contracts to prompt-tag/c
This commit is contained in:
parent
616d49124c
commit
0d30c43a68
|
@ -957,34 +957,56 @@
|
||||||
(define/final-prop none/c (make-none/c 'none/c))
|
(define/final-prop none/c (make-none/c 'none/c))
|
||||||
|
|
||||||
;; prompt-tag/c
|
;; prompt-tag/c
|
||||||
(define/subexpression-pos-prop (prompt-tag/c . ctc-args)
|
(define-syntax prompt-tag/c
|
||||||
(define ctcs
|
(syntax-rules (values)
|
||||||
(map (λ (ctc-arg)
|
[(_ ?ctc ... #:call/cc (values ?call/cc ...))
|
||||||
(coerce-contract 'prompt-tag/c ctc-arg))
|
(-prompt-tag/c (list ?ctc ...) (list ?call/cc ...))]
|
||||||
ctc-args))
|
[(_ ?ctc ... #:call/cc ?call/cc)
|
||||||
(cond [(andmap chaperone-contract? ctcs)
|
(-prompt-tag/c (list ?ctc ...) (list ?call/cc))]
|
||||||
(chaperone-prompt-tag/c ctcs)]
|
[(_ ?ctc ...) (-prompt-tag/c (list ?ctc ...) (list))]))
|
||||||
|
|
||||||
|
;; procedural part of the contract
|
||||||
|
;; takes two lists of contracts (abort & call/cc contracts)
|
||||||
|
(define/subexpression-pos-prop (-prompt-tag/c ctc-args call/ccs)
|
||||||
|
(define ctcs (coerce-contracts 'prompt-tag/c ctc-args))
|
||||||
|
(define call/cc-ctcs (coerce-contracts 'prompt-tag/c call/ccs))
|
||||||
|
(cond [(and (andmap chaperone-contract? ctcs)
|
||||||
|
(andmap chaperone-contract? call/cc-ctcs))
|
||||||
|
(chaperone-prompt-tag/c ctcs call/cc-ctcs)]
|
||||||
[else
|
[else
|
||||||
(impersonator-prompt-tag/c ctcs)]))
|
(impersonator-prompt-tag/c ctcs call/cc-ctcs)]))
|
||||||
|
|
||||||
(define (prompt-tag/c-name ctc)
|
(define (prompt-tag/c-name ctc)
|
||||||
(apply build-compound-type-name
|
(apply build-compound-type-name
|
||||||
(cons 'prompt-tag/c (base-prompt-tag/c-ctcs ctc))))
|
(append (list 'prompt-tag/c) (base-prompt-tag/c-ctcs ctc)
|
||||||
|
(list '#:call/cc) (base-prompt-tag/c-call/ccs ctc))))
|
||||||
|
|
||||||
(define ((prompt-tag/c-proj proxy) ctc)
|
;; build a projection for prompt tags
|
||||||
|
(define ((prompt-tag/c-proj chaperone?) ctc)
|
||||||
|
(define proxy (if chaperone? chaperone-prompt-tag impersonate-prompt-tag))
|
||||||
|
(define proc-proxy (if chaperone? chaperone-procedure impersonate-procedure))
|
||||||
(define ho-projs
|
(define ho-projs
|
||||||
(map contract-projection (base-prompt-tag/c-ctcs ctc)))
|
(map contract-projection (base-prompt-tag/c-ctcs ctc)))
|
||||||
|
(define call/cc-projs
|
||||||
|
(map contract-projection (base-prompt-tag/c-call/ccs ctc)))
|
||||||
(λ (blame)
|
(λ (blame)
|
||||||
(define proj1
|
(define (make-proj projs swap?)
|
||||||
(λ vs
|
(λ vs
|
||||||
(define vs2 (for/list ([proj ho-projs] [v vs])
|
(define vs2 (for/list ([proj projs] [v vs])
|
||||||
((proj blame) v)))
|
((proj (if swap? (blame-swap blame) blame)) v)))
|
||||||
(apply values vs2)))
|
(apply values vs2)))
|
||||||
(define proj2
|
;; prompt/abort projections
|
||||||
(λ vs
|
(define proj1 (make-proj ho-projs #f))
|
||||||
(define vs2 (for/list ([proj ho-projs] [v vs])
|
(define proj2 (make-proj ho-projs #t))
|
||||||
((proj (blame-swap blame)) v)))
|
;; call/cc projections
|
||||||
(apply values vs2)))
|
(define call/cc-guard (make-proj call/cc-projs #f))
|
||||||
|
(define call/cc-proxy
|
||||||
|
(λ (f)
|
||||||
|
(proc-proxy
|
||||||
|
f
|
||||||
|
(λ args
|
||||||
|
(apply values (make-proj call/cc-projs #t) args)))))
|
||||||
|
;; now do the actual wrapping
|
||||||
(λ (val)
|
(λ (val)
|
||||||
(unless (contract-first-order-passes? ctc val)
|
(unless (contract-first-order-passes? ctc val)
|
||||||
(raise-blame-error
|
(raise-blame-error
|
||||||
|
@ -992,7 +1014,7 @@
|
||||||
'(expected: "~s" given: "~e")
|
'(expected: "~s" given: "~e")
|
||||||
(contract-name ctc)
|
(contract-name ctc)
|
||||||
val))
|
val))
|
||||||
(proxy val proj1 proj2))))
|
(proxy val proj1 proj2 call/cc-guard call/cc-proxy))))
|
||||||
|
|
||||||
(define ((prompt-tag/c-first-order ctc) v)
|
(define ((prompt-tag/c-first-order ctc) v)
|
||||||
(continuation-prompt-tag? v))
|
(continuation-prompt-tag? v))
|
||||||
|
@ -1001,14 +1023,18 @@
|
||||||
(and (base-prompt-tag/c? that)
|
(and (base-prompt-tag/c? that)
|
||||||
(andmap (λ (this that) (contract-stronger? this that))
|
(andmap (λ (this that) (contract-stronger? this that))
|
||||||
(base-prompt-tag/c-ctcs this)
|
(base-prompt-tag/c-ctcs this)
|
||||||
(base-prompt-tag/c-ctcs that))))
|
(base-prompt-tag/c-ctcs that))
|
||||||
|
(andmap (λ (this that) (contract-stronger? this that))
|
||||||
|
(base-prompt-tag/c-call/ccs this)
|
||||||
|
(base-prompt-tag/c-call/ccs that))))
|
||||||
|
|
||||||
(define-struct base-prompt-tag/c (ctcs))
|
;; (listof contract) (listof contract)
|
||||||
|
(define-struct base-prompt-tag/c (ctcs call/ccs))
|
||||||
|
|
||||||
(define-struct (chaperone-prompt-tag/c base-prompt-tag/c) ()
|
(define-struct (chaperone-prompt-tag/c base-prompt-tag/c) ()
|
||||||
#:property prop:chaperone-contract
|
#:property prop:chaperone-contract
|
||||||
(build-chaperone-contract-property
|
(build-chaperone-contract-property
|
||||||
#:projection (prompt-tag/c-proj chaperone-prompt-tag)
|
#:projection (prompt-tag/c-proj #t)
|
||||||
#:first-order prompt-tag/c-first-order
|
#:first-order prompt-tag/c-first-order
|
||||||
#:stronger prompt-tag/c-stronger?
|
#:stronger prompt-tag/c-stronger?
|
||||||
#:name prompt-tag/c-name))
|
#:name prompt-tag/c-name))
|
||||||
|
@ -1016,7 +1042,7 @@
|
||||||
(define-struct (impersonator-prompt-tag/c base-prompt-tag/c) ()
|
(define-struct (impersonator-prompt-tag/c base-prompt-tag/c) ()
|
||||||
#:property prop:contract
|
#:property prop:contract
|
||||||
(build-contract-property
|
(build-contract-property
|
||||||
#:projection (prompt-tag/c-proj impersonate-prompt-tag)
|
#:projection (prompt-tag/c-proj #f)
|
||||||
#:first-order prompt-tag/c-first-order
|
#:first-order prompt-tag/c-first-order
|
||||||
#:stronger prompt-tag/c-stronger?
|
#:stronger prompt-tag/c-stronger?
|
||||||
#:name prompt-tag/c-name))
|
#:name prompt-tag/c-name))
|
||||||
|
|
|
@ -520,7 +520,12 @@ to the input. The result will be a copy for immutable hash tables, and either a
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|
||||||
@defproc[(prompt-tag/c [contract contract?] ...) contract?]{
|
@defform/subs[#:literals (values)
|
||||||
|
(prompt-tag/c contract ... maybe-call/cc)
|
||||||
|
([maybe-call/cc (code:line)
|
||||||
|
(code:line #:call/cc contract)
|
||||||
|
(code:line #:call/cc (values contract ...))])
|
||||||
|
#:contracts ([contract contract?])]{
|
||||||
Takes any number of contracts and returns a contract that recognizes
|
Takes any number of contracts and returns a contract that recognizes
|
||||||
continuation prompt tags and will check any aborts or prompt handlers that
|
continuation prompt tags and will check any aborts or prompt handlers that
|
||||||
use the contracted prompt tag.
|
use the contracted prompt tag.
|
||||||
|
@ -533,6 +538,10 @@ If all of the @racket[contract]s are chaperone contracts, the resulting
|
||||||
contract will also be a @tech{chaperone} contract. Otherwise, the contract is
|
contract will also be a @tech{chaperone} contract. Otherwise, the contract is
|
||||||
an @tech{impersonator} contract.
|
an @tech{impersonator} contract.
|
||||||
|
|
||||||
|
If @racket[maybe-call/cc] is provided, then the provided contracts
|
||||||
|
are used to check the return values from a continuation captured with
|
||||||
|
@racket[call-with-current-continuation].
|
||||||
|
|
||||||
@examples[#:eval (contract-eval)
|
@examples[#:eval (contract-eval)
|
||||||
(define/contract tag
|
(define/contract tag
|
||||||
(prompt-tag/c (-> number? string?))
|
(prompt-tag/c (-> number? string?))
|
||||||
|
|
|
@ -4166,6 +4166,58 @@
|
||||||
pt
|
pt
|
||||||
(λ (x y) (values x y)))))
|
(λ (x y) (values x y)))))
|
||||||
|
|
||||||
|
(test/spec-passed
|
||||||
|
'prompt-tag/c-call/cc-1
|
||||||
|
'(let* ([pt (contract (prompt-tag/c string?
|
||||||
|
#:call/cc string?)
|
||||||
|
(make-continuation-prompt-tag)
|
||||||
|
'pos
|
||||||
|
'neg)]
|
||||||
|
[abort-k (call-with-continuation-prompt
|
||||||
|
(λ () (call/cc (λ (k) k) pt))
|
||||||
|
pt)])
|
||||||
|
(call-with-continuation-prompt
|
||||||
|
(λ () (abort-k "ok"))
|
||||||
|
pt
|
||||||
|
(λ (s) (string-append s "post")))))
|
||||||
|
|
||||||
|
(test/spec-passed
|
||||||
|
'prompt-tag/c-call/cc-2
|
||||||
|
'(let* ([pt (contract (prompt-tag/c string?
|
||||||
|
#:call/cc (values string? integer?))
|
||||||
|
(make-continuation-prompt-tag)
|
||||||
|
'pos
|
||||||
|
'neg)]
|
||||||
|
[abort-k (call-with-continuation-prompt
|
||||||
|
(λ () (call/cc (λ (k) k) pt))
|
||||||
|
pt)])
|
||||||
|
(call-with-continuation-prompt
|
||||||
|
(λ () (abort-k "ok" 5))
|
||||||
|
pt
|
||||||
|
(λ (s n) (string-append s "post")))))
|
||||||
|
|
||||||
|
(test/neg-blame
|
||||||
|
'prompt-tag/c-call/cc-2
|
||||||
|
'(letrec ([pt (make-continuation-prompt-tag)]
|
||||||
|
[do-test (λ ()
|
||||||
|
(+ 1
|
||||||
|
(call-with-continuation-prompt
|
||||||
|
(lambda ()
|
||||||
|
(+ 1 (abort-k 1)))
|
||||||
|
pt)))]
|
||||||
|
[cpt (contract (prompt-tag/c #:call/cc number?)
|
||||||
|
pt
|
||||||
|
'pos
|
||||||
|
'neg)]
|
||||||
|
[abort-k (call-with-continuation-prompt
|
||||||
|
(λ ()
|
||||||
|
(let ([v (call/cc (lambda (k) k) cpt)])
|
||||||
|
(if (procedure? v)
|
||||||
|
v
|
||||||
|
(format "~a" v))))
|
||||||
|
pt)])
|
||||||
|
(do-test)))
|
||||||
|
|
||||||
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
|
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
|
||||||
;;
|
;;
|
||||||
;; continuation-mark-key/c
|
;; continuation-mark-key/c
|
||||||
|
|
Loading…
Reference in New Issue
Block a user