added invariant-contract

Jay implemented this
This commit is contained in:
Robby Findler 2014-05-30 21:01:26 -05:00
parent 2eef2ce409
commit ddb7477494
3 changed files with 51 additions and 5 deletions

View File

@ -6,7 +6,7 @@
@(define contract-eval
(lambda ()
(let ([the-eval (make-base-eval)])
(the-eval '(require racket/contract racket/contract/parametric))
(the-eval '(require racket/contract racket/contract/parametric racket/list))
the-eval)))
@title[#:tag "contracts" #:style 'toc]{Contracts}
@ -1430,6 +1430,7 @@ inside the @racket[body] will be protected with contracts that
blame the context of the @racket[with-contract] form for the positive
positions and the @racket[with-contract] form for the negative ones.}
@(define furlongs->feet-eval (contract-eval))
@defform*[[(define/contract id contract-expr free-var-list init-value-expr)
(define/contract (head args) contract-expr free-var-list body ...+)]]{
Works like @racket[define], except that the contract
@ -1437,7 +1438,7 @@ Works like @racket[define], except that the contract
definition of @racket[head] and @racket[args], see @racket[define].
For the definition of @racket[free-var-list], see @racket[with-contract].
@examples[#:eval (contract-eval)
@examples[#:eval furlongs->feet-eval
(define/contract distance (>=/c 0) 43.52)
(define/contract (furlongs->feet fr)
(-> real? real?)
@ -1508,6 +1509,39 @@ The @racket[define-struct/contract] form only allows a subset of the
(make-salmon #f 'pacific)
]}
@defform[(invariant-contract contract-expr expr)]{
Establishes an invariant of @racket[expr], determined by @racket[contract-expr].
Unlike other ways to attach contracts to values, an
@racket[invariant-contract] does not establish a boundary
between two parties. Instead, it simply puts the contract
on the value, treating the module containing the
@racket[invariant-contract] expression as the party to be blamed
for any violations of the contract.
This means, for example, that the contract is checked on
recursive calls, when an invariant is used on the right-hand
side of a definition.
@examples[#:eval
furlongs->feet-eval
(define furlongss->feets
(invariant-contract
(-> (listof real?) (listof real?))
(λ (l)
(cond
[(empty? l) empty]
[else
(if (= 327 (car l))
(furlongss->feets (list "wha?"))
(cons (furlongs->feet (first l))
(furlongss->feets (rest l))))]))))
(furlongss->feets (list 1 2 3))
(furlongss->feets (list 1 327 3))]
}
@defidform[current-contract-region]{
Bound by @racket[define-syntax-parameter], this contains
information about the current contract region, used by

View File

@ -2,9 +2,10 @@
(provide contract
(rename-out [-recursive-contract recursive-contract])
current-contract-region)
current-contract-region
invariant-contract)
(require (for-syntax racket/base syntax/name)
(require (for-syntax racket/base syntax/name syntax/srcloc)
racket/stxparam
syntax/srcloc
syntax/location
@ -88,6 +89,16 @@
(procedure-rename new-val vs-name)])]
[else new-val])))
(define-syntax (invariant-contract stx)
(syntax-case stx ()
[(_ ctc e)
(quasisyntax/loc stx
(let ([me (quote-module-name)])
(contract ctc e
me me
'#,(syntax-local-infer-name stx)
'#,(build-source-location-vector #'ctc))))]))
(define-syntax (-recursive-contract stx)
(define (do-recursive-contract arg type name)
(define local-name (syntax-local-infer-name stx))

View File

@ -3,7 +3,8 @@
(provide define-struct/contract
define/contract
with-contract
current-contract-region)
current-contract-region
invariant-contract)
(require (for-syntax racket/base
racket/struct-info