diff --git a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/private/type-contract.rkt b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/private/type-contract.rkt index 91e88330..fca59e1d 100644 --- a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/private/type-contract.rkt +++ b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/private/type-contract.rkt @@ -468,6 +468,8 @@ (hash/sc (t->sc k) (t->sc v))] [(Channel: t) (channel/sc (t->sc t))] + [(Evt: t) + (evt/sc (t->sc t))] [else (fail #:reason "contract generation not supported for this type")])))) diff --git a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/static-contracts/combinators/structural.rkt b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/static-contracts/combinators/structural.rkt index 5a8c84c3..a19ccc3b 100644 --- a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/static-contracts/combinators/structural.rkt +++ b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/static-contracts/combinators/structural.rkt @@ -13,7 +13,8 @@ (for-template racket/base racket/contract/base racket/set - unstable/contract) + unstable/contract + "../../utils/evt-contract.rkt") racket/contract) @@ -157,4 +158,5 @@ ((parameter/sc (#:contravariant) (#:covariant)) parameter/c #:chaperone) ((sequence/sc . (#:covariant)) sequence/c #:impersonator) ((channel/sc . (#:invariant)) channel/c #:chaperone) - ((continuation-mark-key/sc (#:invariant)) continuation-mark-key/c #:chaperone)) + ((continuation-mark-key/sc (#:invariant)) continuation-mark-key/c #:chaperone) + ((evt/sc (#:covariant)) tr:evt/c #:chaperone)) diff --git a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typed-racket.rkt b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typed-racket.rkt index 0f26589f..0b896195 100644 --- a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typed-racket.rkt +++ b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typed-racket.rkt @@ -10,7 +10,9 @@ (submod "private/type-contract.rkt" predicates) "utils/utils.rkt" (for-syntax "utils/utils.rkt") - "utils/any-wrap.rkt" "utils/struct-type-c.rkt" unstable/contract racket/contract/parametric) + "utils/any-wrap.rkt" "utils/struct-type-c.rkt" + "utils/evt-contract.rkt" + unstable/contract racket/contract/parametric) (provide (rename-out [module-begin #%module-begin] [top-interaction #%top-interaction]) diff --git a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/utils/evt-contract.rkt b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/utils/evt-contract.rkt new file mode 100644 index 00000000..d3e00a6c --- /dev/null +++ b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/utils/evt-contract.rkt @@ -0,0 +1,61 @@ +#lang racket/base + +;; A custom evt/c for TR that is stricter than the one that +;; comes with Racket. In particular, this will prevent the channel's +;; writing end from being used once it's been exported as an Evtof. + +(require racket/contract) + +(provide tr:evt/c) + +;; tr:evt/c : Contract * -> Contract +(define (tr:evt/c maybe-ctc) + (define ctc (coerce-contract 'evt/c maybe-ctc)) + (unless (chaperone-contract? ctc) + (raise-argument-error 'evt/c "chaperone-contract?" ctc)) + (make-tr-evt/c ctc)) + +;; evt/c-proj : Contract -> (Blame -> Any -> Any) +(define (evt/c-proj ctc) + (define real-evt/c (evt/c (tr-evt/c-ctc ctc))) + (define real-proj (contract-projection real-evt/c)) + (λ (blame) + (define real-proj* (real-proj blame)) + (λ (v) + ;; Must not allow a value of type (Evtof X) to be used as + ;; a value of any type that is invariant in X (i.e., has a + ;; writing end). For now, this is just channels. + ;; + ;; If we support custom evts via struct properties, then + ;; we may need to tighten this restrictions. + (if (channel? v) + (real-proj* + (chaperone-channel + v + (λ (ch) (values ch values)) + (λ (ch val) + (raise-blame-error + blame ch + "cannot put on a channel used as a typed evt")))) + (real-proj* v))))) + +;; evt/c-first-order : Contract -> Any -> Boolean +(define ((evt/c-first-order ctc) v) (evt? v)) + +;; evt/c-name : Contract -> Sexp +(define (evt/c-name ctc) + (build-compound-type-name 'evt/c (tr-evt/c-ctc ctc))) + +;; evt/c-stronger? : Contract Contract -> Boolean +(define (evt/c-stronger? this that) + (define this-ctcs (tr-evt/c-ctc this)) + (define that-ctcs (tr-evt/c-ctc that)) + (contract-stronger? this that)) + +(define-struct tr-evt/c (ctc) + #:property prop:chaperone-contract + (build-chaperone-contract-property + #:projection evt/c-proj + #:first-order evt/c-first-order + #:stronger evt/c-stronger? + #:name evt/c-name)) diff --git a/pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/unit-tests/contract-tests.rkt b/pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/unit-tests/contract-tests.rkt index 121fb7d9..430e1851 100644 --- a/pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/unit-tests/contract-tests.rkt +++ b/pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/unit-tests/contract-tests.rkt @@ -60,6 +60,7 @@ (namespace-require 'racket/contract) (namespace-require 'unstable/contract) (namespace-require 'typed-racket/utils/any-wrap) + (namespace-require 'typed-racket/utils/evt-contract) (namespace-require '(submod typed-racket/private/type-contract predicates)) (current-namespace))) @@ -204,6 +205,7 @@ (member-spec 'inherit-field 'y integer/sc)) #f null null)) + ;; typed/untyped interaction tests (t-int (-poly (a) (-> a a)) (λ (f) (f 1)) (λ (x) 1) @@ -218,4 +220,31 @@ (λ (f) (f "a" "b")) (case-lambda [xs (car xs)] [(sym . xs) sym])) + (t-int (make-Evt -String) + (λ (x) (channel-get x)) + (let ([ch (make-channel)]) + (thread (λ () (channel-put ch "ok"))) + ch) + #:untyped) + (t-int/fail (make-Evt -String) + (λ (x) (channel-get x)) + (let ([ch (make-channel)]) + (thread (λ () (channel-put ch 'bad))) + ch) + #:untyped + #:msg #rx"promised: String.*produced: 'bad") + (t-int/fail (make-Evt (-> -String -String)) + (λ (x) ((sync x) 'bad)) + (let ([ch (make-channel)]) + (thread + (λ () + (channel-put ch (λ (x) (string-append x "x"))))) + ch) + #:typed + #:msg #rx"expected: String.*given: 'bad") + (t-int/fail (make-Evt -String) + (λ (x) (channel-put x "bad")) + (make-channel) + #:untyped + #:msg #rx"cannot put on a channel") ))