suzanne.soy/typed-racket
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

Add contract generation for Evtof types

Browse Source 
original commit: 863f0c58025301312298fb52a6c5f0d4ccdbdb9c
This commit is contained in:
Asumu Takikawa 2014-10-08 01:04:42 -04:00
parent b4b666f9f2
commit 58b3c4f4f7
5 changed files with 99 additions and 3 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/private/type-contract.rkt
View File

@ -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")]))))

6
pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/static-contracts/combinators/structural.rkt
View File

@ -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))

4
pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typed-racket.rkt
View File

@ -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])

61
pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/utils/evt-contract.rkt Normal file
View File

@ -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))

29
pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/unit-tests/contract-tests.rkt
View File

@ -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")
))