add `contract-out'

This commit is contained in:
Matthew Flatt 2011-09-24 13:50:11 +09:00
parent 9d27b21f91
commit e226dd7e26
24 changed files with 579 additions and 449 deletions

View File

@ -12,7 +12,8 @@
"private/guts.rkt"
"private/prop.rkt"
"private/opters.rkt" ;; required for effect to install the opters
"private/opt.rkt")
"private/opt.rkt"
"private/out.rkt")
(provide
(except-out (all-from-out "private/arrow.rkt")
@ -36,7 +37,9 @@
(except-out (all-from-out "private/misc.rkt")
check-between/c
check-unary-between/c)
(all-from-out "private/provide.rkt")
provide/contract
(for-syntax make-provide/contract-transformer) ;; not documented!
contract-out
;; from private/opt.rkt:
opt/c define-opt/c

View File

@ -0,0 +1,46 @@
#lang racket/base
(require (for-syntax racket/base
racket/provide-transform)
"provide.rkt")
(provide contract-out)
(define-syntax contract-out
(make-provide-pre-transformer
(lambda (stx modes)
;; For now, only work in the base phase of the `contract-out'
;; binding. To generalize, we'll need to parameterize `true-provide'
;; over the phase where it should match, shift references, and
;; shift lifts (by wrapping them with `begin-for-syntax'es).
(unless (or (null? modes)
(and (= 1 (length modes))
(zero? (car modes))))
(raise-syntax-error #f
"allowed only in relative phase-level 0"
stx))
;; lifts need to go after lifts for `provide's:
(define lifts null)
;; use `provide/contract' expander:
(let ([expanded (true-provide/contract stx (lambda (stx)
(set! lifts (cons stx lifts))))])
;; pull out `provide's to return, and lift
;; the rest as a module-end declaration:
(define-values (decls provides)
(let loop ([expanded expanded])
(syntax-case expanded (begin provide)
[(begin expr ...)
(let ([boths
(map (lambda (e)
(define-values (ds ps) (loop e))
(cons ds ps))
(syntax->list #'(expr ...)))])
(values (apply append (map car boths))
(apply append (map cdr boths))))]
[(provide p ...)
(values null (syntax->list #'(p ...)))]
[else
(values (list expanded) null)])))
(for ([decl (in-list decls)])
(syntax-local-lift-module-end-declaration decl))
(for ([decl (in-list (reverse lifts))])
(syntax-local-lift-module-end-declaration decl))
#`(combine-out #,@provides)))))

View File

@ -1,7 +1,8 @@
#lang racket/base
(provide provide/contract
(for-syntax make-provide/contract-transformer))
(protect-out (for-syntax true-provide/contract
make-provide/contract-transformer)))
(require (for-syntax racket/base
racket/list
@ -102,7 +103,7 @@
;; expressions:
(quasisyntax/loc stx (#%expression #,stx)))))))
(define-for-syntax (true-provide/contract provide-stx)
(define-for-syntax (true-provide/contract provide-stx lift-end-declaration)
(syntax-case provide-stx ()
[(_ p/c-ele ...)
(let ()
@ -723,7 +724,7 @@
'provide/contract-original-contract
(vector #'external-name #'ctrct))])
(syntax-local-lift-module-end-declaration
(lift-end-declaration
#`(begin
(unless extra-test
(contract contract-id id pos-module-source 'ignored 'id
@ -783,7 +784,7 @@
#`(begin (define-values () (values)) ;; force us into the 'module' local context
#,stx)]
[(module) ;; the good case
(true-provide/contract stx)]
(true-provide/contract stx syntax-local-lift-module-end-declaration)]
[else ;; expression or internal definition
(raise-syntax-error 'provide/contract
(format "not allowed in a ~a context"

View File

@ -6,12 +6,13 @@
(define-struct basic-customer (id name address) #:mutable)
;; interface
(provide/contract
[id? (-> any/c boolean?)]
[id-equal? (-> id? id? boolean?)]
[struct basic-customer ((id id?)
(name string?)
(address string?))])
(provide
(contract-out
[id? (-> any/c boolean?)]
[id-equal? (-> id? id? boolean?)]
[struct basic-customer ((id id?)
(name string?)
(address string?))]))
;; end of interface

View File

@ -35,25 +35,26 @@
(define c0 0)
;; end of implementation
(provide/contract
;; how many customers are in the db?
[count natural-number/c]
;; is the customer with this id active?
[active? (-> id? boolean?)]
;; what is the name of the customer with this id?
[name (-> (and/c id? active?) string?)]
;; change the name of the customer with this id
[set-name (->d ([id id?] [nn string?])
()
[result any/c] ;; result contract
#:post-cond
(string=? (name id) nn))]
(provide
(contract-out
;; how many customers are in the db?
[count natural-number/c]
;; is the customer with this id active?
[active? (-> id? boolean?)]
;; what is the name of the customer with this id?
[name (-> (and/c id? active?) string?)]
;; change the name of the customer with this id
[set-name (->d ([id id?] [nn string?])
()
[result any/c] ;; result contract
#:post-cond
(string=? (name id) nn))]
[add (->d ([bc (and/c basic-customer? not-active?)])
()
;; A pre-post condition contract must use
;; a side-effect to express this contract
;; via post-conditions
#:pre-cond (set! c0 count)
[result any/c] ;; result contract
#:post-cond (> count c0))])
[add (->d ([bc (and/c basic-customer? not-active?)])
()
;; A pre-post condition contract must use
;; a side-effect to express this contract
;; via post-conditions
#:pre-cond (set! c0 count)
[result any/c] ;; result contract
#:post-cond (> count c0))]))

View File

@ -17,57 +17,58 @@
(stack-eq s)))
(define (top s) (car (stack-list s)))
(provide/contract
;; predicate
[stack? (-> any/c boolean?)]
;; primitive queries
;; how many items are on the stack?
[count (-> stack? natural-number/c)]
;; which item is at the given position?
[item-at
(->d ([s stack?] [i (and/c positive? (<=/c (count s)))])
()
[result (stack-p? s)])]
;; derived queries
;; is the stack empty?
[is-empty?
(->d ([s stack?])
()
[result (eq/c (= (count s) 0))])]
;; which item is at the top of the stack
[top
(->d ([s (and/c stack? not-empty?)])
()
[t (stack-p? s)] ;; a stack item, t is its name
#:post-cond
([stack-eq s] t (item-at s (count s))))]
;; creation
[initialize
(->d ([p contract?] [s (p p . -> . boolean?)])
()
;; Mitchell and McKim use (= (count s) 0) here to express
;; the post-condition in terms of a primitive query
[result (and/c stack? is-empty?)])]
;; commands
;; add an item to the top of the stack
[push
(->d ([s stack?] [x (stack-p? s)])
()
[sn stack?] ;; result kind
#:post-cond
(and (= (+ (count s) 1) (count sn))
([stack-eq s] x (top sn))))]
;; remove the item at the top of the stack
[pop
(->d ([s (and/c stack? not-empty?)])
()
[sn stack?] ;; result kind
#:post-cond
(= (- (count s) 1) (count sn)))])
(provide
(contract-out
;; predicate
[stack? (-> any/c boolean?)]
;; primitive queries
;; how many items are on the stack?
[count (-> stack? natural-number/c)]
;; which item is at the given position?
[item-at
(->d ([s stack?] [i (and/c positive? (<=/c (count s)))])
()
[result (stack-p? s)])]
;; derived queries
;; is the stack empty?
[is-empty?
(->d ([s stack?])
()
[result (eq/c (= (count s) 0))])]
;; which item is at the top of the stack
[top
(->d ([s (and/c stack? not-empty?)])
()
[t (stack-p? s)] ;; a stack item, t is its name
#:post-cond
([stack-eq s] t (item-at s (count s))))]
;; creation
[initialize
(->d ([p contract?] [s (p p . -> . boolean?)])
()
;; Mitchell and McKim use (= (count s) 0) here to express
;; the post-condition in terms of a primitive query
[result (and/c stack? is-empty?)])]
;; commands
;; add an item to the top of the stack
[push
(->d ([s stack?] [x (stack-p? s)])
()
[sn stack?] ;; result kind
#:post-cond
(and (= (+ (count s) 1) (count sn))
([stack-eq s] x (top sn))))]
;; remove the item at the top of the stack
[pop
(->d ([s (and/c stack? not-empty?)])
()
[sn stack?] ;; result kind
#:post-cond
(= (- (count s) 1) (count sn)))]))

View File

@ -30,47 +30,48 @@
;; end of implementation
;; interface
(provide/contract
;; predicates
[dictionary? (-> any/c boolean?)]
;; basic queries
;; how many items are in the dictionary?
[count (-> dictionary? natural-number/c)]
;; does the dictionary define key k?
[has? (->d ([d dictionary?] [k symbol?])
()
[result boolean?]
#:post-cond
((zero? (count d)) . . (not result)))]
;; what is the value of key k in this dictionary?
[value-for (->d ([d dictionary?]
[k (and/c symbol? (lambda (k) (has? d k)))])
()
[result (dictionary-value? d)])]
;; initialization
;; post condition: for all k in symbol, (has? d k) is false.
[initialize (->d ([p contract?] [eq (p p . -> . boolean?)])
()
[result (and/c dictionary? (compose zero? count))])]
;; commands
;; Mitchell and McKim say that put shouldn't consume Void (null ptr)
;; for v. We allow the client to specify a contract for all values
;; via initialize. We could do the same via a key? parameter
;; (exercise). add key k with value v to this dictionary
[put (->d ([d dictionary?]
[k (and symbol? (not-has? d))]
[v (dictionary-value? d)])
()
[result dictionary?]
#:post-cond
(and (has? result k)
(= (count d) (- (count result) 1))
([dictionary-eq? d] (value-for result k) v)))]
;; remove key k from this dictionary
[rem (->d ([d dictionary?]
[k (and/c symbol? (lambda (k) (has? d k)))])
()
[result (and/c dictionary? not-has?)]
#:post-cond
(= (count d) (+ (count result) 1)))])
(provide
(contract-out
;; predicates
[dictionary? (-> any/c boolean?)]
;; basic queries
;; how many items are in the dictionary?
[count (-> dictionary? natural-number/c)]
;; does the dictionary define key k?
[has? (->d ([d dictionary?] [k symbol?])
()
[result boolean?]
#:post-cond
((zero? (count d)) . . (not result)))]
;; what is the value of key k in this dictionary?
[value-for (->d ([d dictionary?]
[k (and/c symbol? (lambda (k) (has? d k)))])
()
[result (dictionary-value? d)])]
;; initialization
;; post condition: for all k in symbol, (has? d k) is false.
[initialize (->d ([p contract?] [eq (p p . -> . boolean?)])
()
[result (and/c dictionary? (compose zero? count))])]
;; commands
;; Mitchell and McKim say that put shouldn't consume Void (null ptr)
;; for v. We allow the client to specify a contract for all values
;; via initialize. We could do the same via a key? parameter
;; (exercise). add key k with value v to this dictionary
[put (->d ([d dictionary?]
[k (and symbol? (not-has? d))]
[v (dictionary-value? d)])
()
[result dictionary?]
#:post-cond
(and (has? result k)
(= (count d) (- (count result) 1))
([dictionary-eq? d] (value-for result k) v)))]
;; remove key k from this dictionary
[rem (->d ([d dictionary?]
[k (and/c symbol? (lambda (k) (has? d k)))])
()
[result (and/c dictionary? not-has?)]
#:post-cond
(= (count d) (+ (count result) 1)))]))
;; end of interface

View File

@ -26,57 +26,58 @@
(define (head s) (car (queue-list s)))
;; interface
(provide/contract
;; predicate
[queue? (-> any/c boolean?)]
;; primitive queries
;; Imagine providing this 'query' for the interface of the module
;; only. Then in Racket there is no reason to have count or is-empty?
;; around (other than providing it to clients). After all items is
;; exactly as cheap as count.
[items (->d ([q queue?]) () [result (listof (queue-p? q))])]
;; derived queries
[count (->d ([q queue?])
;; We could express this second part of the post
;; condition even if count were a module "attribute"
;; in the language of Eiffel; indeed it would use the
;; exact same syntax (minus the arrow and domain).
()
[result (and/c natural-number/c
(=/c (length (items q))))])]
[is-empty? (->d ([q queue?])
()
[result (and/c boolean?
(eq/c (null? (items q))))])]
[head (->d ([q (and/c queue? (compose not is-empty?))])
()
[result (and/c (queue-p? q)
(eq/c (car (items q))))])]
;; creation
[initialize (-> contract?
(contract? contract? . -> . boolean?)
(and/c queue? (compose null? items)))]
;; commands
[put (->d ([oldq queue?] [i (queue-p? oldq)])
()
[result
(and/c
queue?
(lambda (q)
(define old-items (items oldq))
(equal? (items q) (append old-items (list i)))))])]
(provide
(contract-out
;; predicate
[queue? (-> any/c boolean?)]
;; primitive queries
;; Imagine providing this 'query' for the interface of the module
;; only. Then in Racket there is no reason to have count or is-empty?
;; around (other than providing it to clients). After all items is
;; exactly as cheap as count.
[items (->d ([q queue?]) () [result (listof (queue-p? q))])]
;; derived queries
[count (->d ([q queue?])
;; We could express this second part of the post
;; condition even if count were a module "attribute"
;; in the language of Eiffel; indeed it would use the
;; exact same syntax (minus the arrow and domain).
()
[result (and/c natural-number/c
(=/c (length (items q))))])]
[is-empty? (->d ([q queue?])
()
[result (and/c boolean?
(eq/c (null? (items q))))])]
[head (->d ([q (and/c queue? (compose not is-empty?))])
()
[result (and/c (queue-p? q)
(eq/c (car (items q))))])]
;; creation
[initialize (-> contract?
(contract? contract? . -> . boolean?)
(and/c queue? (compose null? items)))]
;; commands
[put (->d ([oldq queue?] [i (queue-p? oldq)])
()
[result
(and/c
queue?
(lambda (q)
(define old-items (items oldq))
(equal? (items q) (append old-items (list i)))))])]
[rem (->d ([oldq (and/c queue? (compose not is-empty?))])
()
[result
(and/c queue?
(lambda (q)
(equal? (cdr (items oldq)) (items q))))])])
[rem (->d ([oldq (and/c queue? (compose not is-empty?))])
()
[result
(and/c queue?
(lambda (q)
(equal? (cdr (items oldq)) (items q))))])]))
;; end of interface

View File

@ -6,8 +6,9 @@
(define (argmax f lov)
(old:argmax f lov))
(provide/contract
[argmax (-> (-> any/c real?) (and/c pair? list?) any/c)]))
(provide
(contract-out
[argmax (-> (-> any/c real?) (and/c pair? list?) any/c)])))
(module b racket/base
(require 'a)

View File

@ -9,13 +9,14 @@
(define r (old:argmax f lov))
(if (and (number? r) (= r 1/4)) 1/5 r)) ;; a bug
(provide/contract
(provide
(contract-out
[argmax
(->i ([f (-> any/c real?)] [lov (and/c pair? list?)]) ()
(r (f lov)
(lambda (r)
(define f@r (f r))
(for/and ((v lov)) (>= f@r (f v))))))]))
(for/and ((v lov)) (>= f@r (f v))))))])))
(module b racket/base
(require 'a)

View File

@ -9,15 +9,16 @@
(define r (old:argmax f lov))
(if (and (number? r) (= r 1/4)) 1 r)) ;; yet another bug
(provide/contract
[argmax
(->i ([f (-> any/c real?)] [lov (and/c pair? list?)]) ()
(r (f lov)
(lambda (r)
(define f@r (f r))
(and
(memq r lov)
(for/and ((v lov)) (>= f@r (f v)))))))]))
(provide
(contract-out
[argmax
(->i ([f (-> any/c real?)] [lov (and/c pair? list?)]) ()
(r (f lov)
(lambda (r)
(define f@r (f r))
(and
(memq r lov)
(for/and ((v lov)) (>= f@r (f v)))))))])))
(module b racket/base
(require 'a)

View File

@ -11,15 +11,16 @@
'(3 oranges)
r)) ;; yet another bug
(provide/contract
[argmax
(->i ([f (-> any/c real?)] [lov (and/c pair? list?)]) ()
(r (f lov)
(lambda (r)
(define f@r (f r))
(and (for/and ((v lov)) (>= f@r (f v)))
(eq? (first (memf (lambda (v) (= (f v) f@r)) lov))
r)))))]))
(provide
(contract-out
[argmax
(->i ([f (-> any/c real?)] [lov (and/c pair? list?)]) ()
(r (f lov)
(lambda (r)
(define f@r (f r))
(and (for/and ((v lov)) (>= f@r (f v)))
(eq? (first (memf (lambda (v) (= (f v) f@r)) lov))
r)))))])))
(module b racket/base
(require 'a)

View File

@ -11,14 +11,15 @@
'(3 oranges)
r)) ;; yet another bug
(provide/contract
[argmax
(->i ([f (-> any/c real?)] [lov (and/c pair? list?)]) ()
(r (f lov)
(lambda (r)
(define f@r (f r))
(and (is-first-max? r f@r f lov)
(dominates-all f@r f lov)))))])
(provide
(contract-out
[argmax
(->i ([f (-> any/c real?)] [lov (and/c pair? list?)]) ()
(r (f lov)
(lambda (r)
(define f@r (f r))
(and (is-first-max? r f@r f lov)
(dominates-all f@r f lov)))))]))
;; @code:comment{where}

View File

@ -12,15 +12,16 @@
r)]))
(provide/contract
[argmax
(->i ([f (-> any/c real?)] [lov (and/c pair? list?)]) ()
(r (f lov)
(lambda (r)
(define f@r (f r))
(define flov (map f lov))
(and (is-first-max? r f@r (map list lov flov))
(dominates-all f@r flov)))))])
(provide
(contract-out
[argmax
(->i ([f (-> any/c real?)] [lov (and/c pair? list?)]) ()
(r (f lov)
(lambda (r)
(define f@r (f r))
(define flov (map f lov))
(and (is-first-max? r f@r (map list lov flov))
(dominates-all f@r flov)))))]))
; f@r is greater or equal to all f@v in flov
(define (dominates-all f@r flov)

View File

@ -11,18 +11,19 @@
'(3 oranges) ;; a bug
r)]))
(provide/contract
[argmax
(->i ([f (-> any/c real?)] [lov (and/c pair? list?)]) ()
(r (f lov)
(lambda (r)
(cond
(provide
(contract-out
[argmax
(->i ([f (-> any/c real?)] [lov (and/c pair? list?)]) ()
(r (f lov)
(lambda (r)
(cond
[(empty? (rest lov)) (eq? (first lov) r)]
[else
(define f@r (f r))
(define flov (map f lov))
(and (is-first-max? r f@r (map list lov flov))
(dominates-all f@r flov))]))))])
(dominates-all f@r flov))]))))]))
; f@r is greater or equal to all f@v in flov
(define (dominates-all f@r flov)

View File

@ -16,7 +16,7 @@ for your data structures.
cannot easily type unicode characters; in DrRacket, typing
@tt{\exists} followed by either alt-\ or control-\ (depending
on your platform) will produce @racket[∃].}
The @racket[provide/contract] form allows you to write
The @racket[contract-out] form allows you to write
@racketblock[#:∃ _name-of-a-new-contract] as one of its clauses. This declaration
introduces the variable @racket[_name-of-a-new-contract], binding it to a new
contract that hides information about the values it protects.
@ -29,12 +29,13 @@ As an example, consider this (simple) implementation of a stack datastructure:
(define (deq queue) (cdr queue))
(define (empty? queue) (null? queue))
(provide/contract
[empty (listof integer?)]
[enq (-> integer? (listof integer?) (listof integer?))]
[next (-> (listof integer?) integer?)]
[deq (-> (listof integer?) (listof integer?))]
[empty? (-> (listof integer?) boolean?)])]
(provide
(contract-out
[empty (listof integer?)]
[enq (-> integer? (listof integer?) (listof integer?))]
[next (-> (listof integer?) integer?)]
[deq (-> (listof integer?) (listof integer?))]
[empty? (-> (listof integer?) boolean?)]))]
This code implements a queue purely in terms of lists, meaning that clients
of this data structure might use @racket[car] and @racket[cdr] directly on the
data structure (perhaps accidentally) and thus any change in the representation
@ -42,14 +43,15 @@ data structure (perhaps accidentally) and thus any change in the representation
enqueue and dequeue operations) might break client code.
To ensure that the stack representation is abstract, we can use @racket[#:∃] in the
@racket[provide/contract] expression, like this:
@racketblock[(provide/contract
#:∃ stack
[empty stack]
[enq (-> integer? stack stack)]
[next (-> stack integer?)]
[deq (-> stack (listof integer?))]
[empty? (-> stack boolean?)])]
@racket[contract-out] expression, like this:
@racketblock[(provide
(contract-out
#:∃ stack
[empty stack]
[enq (-> integer? stack stack)]
[next (-> stack integer?)]
[deq (-> stack (listof integer?))]
[empty? (-> stack boolean?)]))]
Now, if clients of the data structure try to use @racket[car] and @racket[cdr], they
receive an error, rather than mucking about with the internals of the queues.

View File

@ -31,8 +31,9 @@ racket
(define (argmax f lov) ...)
(provide/contract
[argmax (-> (-> any/c real?) (and/c pair? list?) any/c)])
(provide
(contract-out
[argmax (-> (-> any/c real?) (and/c pair? list?) any/c)]))
]
This contract captures two essential conditions of the informal
description of @racket[argmax]:
@ -56,13 +57,14 @@ racket
(define (argmax f lov) ...)
(provide/contract
(provide
(contract-out
[argmax
(->i ([f (-> any/c real?)] [lov (and/c pair? list?)]) ()
(r (f lov)
(lambda (r)
(define f@r (f r))
(for/and ([v lov]) (>= f@r (f v))))))])
(for/and ([v lov]) (>= f@r (f v))))))]))
]
It is a @emph{dependent} contract that names the two arguments and uses
the names to impose a predicate on the result. This predicate computes
@ -78,14 +80,15 @@ racket
(define (argmax f lov) ...)
(provide/contract
(provide
(contract-out
[argmax
(->i ([f (-> any/c real?)] [lov (and/c pair? list?)]) ()
(r (f lov)
(lambda (r)
(define f@r (f r))
(and (memq r lov)
(for/and ([v lov]) (>= f@r (f v)))))))])
(for/and ([v lov]) (>= f@r (f v)))))))]))
]
The @racket[memq] function ensures that @racket[r] is @emph{intensionally equal}
@margin-note*{That is, "pointer equality" for those who prefer to think at
@ -106,7 +109,8 @@ racket
(define (argmax f lov) ...)
(provide/contract
(provide
(contract-out
[argmax
(->i ([f (-> any/c real?)] [lov (and/c pair? list?)]) ()
(r (f lov)
@ -114,7 +118,7 @@ racket
(define f@r (f r))
(and (for/and ([v lov]) (>= f@r (f v)))
(eq? (first (memf (lambda (v) (= (f v) f@r)) lov))
r)))))])
r)))))]))
]
That is, the @racket[memf] function determines the first element of
@racket[lov] whose value under @racket[f] is equal to @racket[r]'s value
@ -143,14 +147,15 @@ racket
(define (argmax f lov) ...)
(provide/contract
(provide
(contract-out
[argmax
(->i ([f (-> any/c real?)] [lov (and/c pair? list?)]) ()
(r (f lov)
(lambda (r)
(define f@r (f r))
(and (is-first-max? r f@r f lov)
(dominates-all f@r f lov)))))])
(dominates-all f@r f lov)))))]))
@code:comment{where}
@ -184,7 +189,8 @@ racket
(define (argmax f lov) ...)
(provide/contract
(provide
(contract-out
[argmax
(->i ([f (-> any/c real?)] [lov (and/c pair? list?)]) ()
(r (f lov)
@ -192,7 +198,7 @@ racket
(define f@r (f r))
(define flov (map f lov))
(and (is-first-max? r f@r (map list lov flov))
(dominates-all f@r flov)))))])
(dominates-all f@r flov)))))]))
@code:comment{where}
@ -237,7 +243,8 @@ racket
(first lov)
...))
(provide/contract
(provide
(contract-out
[argmax
(->i ([f (-> any/c real?)] [lov (and/c pair? list?)]) ()
(r (f lov)
@ -248,7 +255,7 @@ racket
(define f@r (f r))
(define flov (map f lov))
(and (is-first-max? r f@r (map list lov flov))
(dominates-all f@r flov))]))))])
(dominates-all f@r flov))]))))]))
@code:comment{where}

View File

@ -18,12 +18,13 @@ Take a look at this excerpt from a string-processing module, inspired by the
@racketmod[
racket
(provide/contract
(code:comment @#,t{pad the given str left and right with})
(code:comment @#,t{the (optional) char so that it is centered})
[string-pad-center (->* (string? natural-number/c)
(char?)
string?)])
(provide
(contract-out
(code:comment @#,t{pad the given str left and right with})
(code:comment @#,t{the (optional) char so that it is centered})
[string-pad-center (->* (string? natural-number/c)
(char?)
string?)]))
(define (string-pad-center str width [pad #\space])
(define field-width (min width (string-length str)))
@ -86,8 +87,9 @@ contract on a list of arguments after the required and optional
arguments:
@racketblock[
(provide/contract
[max-abs (->* (real?) () #:rest (listof real?) real?)])
(provide
(contract-out
[max-abs (->* (real?) () #:rest (listof real?) real?)]))
]
As always for @racket[->*], the contracts for the required arguments
@ -131,14 +133,14 @@ racket/gui
(send d show #t)
answer)
(provide/contract
[ask-yes-or-no-question
(-> string?
#:default boolean?
#:title string?
#:width exact-integer?
#:height exact-integer?
boolean?)])
(provide (contract-out
[ask-yes-or-no-question
(-> string?
#:default boolean?
#:title string?
#:width exact-integer?
#:height exact-integer?
boolean?)]))
]
@margin-note{If you really want to ask a yes-or-no question
@ -187,16 +189,15 @@ sections. In this case, we have the mandatory keyword
@racket[#:height]. So, we write the contract like this:
@racketblock[
(provide/contract
[ask-yes-or-no-question
(->* (string?
#:default boolean?)
(provide (contract-out
[ask-yes-or-no-question
(->* (string?
#:default boolean?)
(#:title string?
#:width exact-integer?
#:height exact-integer?)
(#:title string?
#:width exact-integer?
#:height exact-integer?)
boolean?)])
boolean?)]))
]
That is, we put the mandatory keywords in the first section, and we
@ -225,11 +226,11 @@ of numbers or a string into a new string:
The contract for such a function is formed with the @racket[case->]
combinator, which combines as many functional contracts as needed:
@racketblock[
(provide/contract
[report-cost
(case->
(integer? integer? . -> . string?)
(string? . -> . string?))])
(provide (contract-out
[report-cost
(case->
(integer? integer? . -> . string?)
(string? . -> . string?))]))
]
As you can see, the contract for @racket[report-cost] combines two
function contracts, which is just as many clauses as the explanation
@ -244,7 +245,8 @@ In the case of @racket[substring1], we also know that the indices
adding such constraints is just a matter of strengthening the individual
contracts:
<racket>
(provide/contract
(provide
(contract-out
[substring1 (case->
(string? . -> . string?)
(->r ([s string?]
@ -255,7 +257,7 @@ In the case of @racket[substring1], we also know that the indices
[o (and/c natural-number/c
(>=/c a)
(</c (string-length s)))])
string?))])
string?))]))
</racket>
Here we used @racket[->r] to name the parameters and express the
numeric constraints on them.
@ -266,9 +268,10 @@ In the case of @racket[substring1], we also know that the indices
The following is an excerpt from an imaginary numerics module:
@racketblock[
(provide/contract
[real-sqrt (->i ([argument (>=/c 1)])
[result (argument) (<=/c argument)])])
(provide
(contract-out
[real-sqrt (->i ([argument (>=/c 1)])
[result (argument) (<=/c argument)])]))
]
The contract for the exported function @racket[real-sqrt] uses the
@ -298,10 +301,10 @@ withdrawal operation. The improved bank-account module includes a
@racket[account] structure type and the following functions:
@racketblock[
(provide/contract
[balance (-> account? amount/c)]
[withdraw (-> account? amount/c account?)]
[deposit (-> account? amount/c account?)])
(provide (contract-out
[balance (-> account? amount/c)]
[withdraw (-> account? amount/c account?)]
[deposit (-> account? amount/c account?)]))
]
Besides requiring that a client provide a valid amount for a
@ -320,23 +323,24 @@ racket
(define amount/c natural-number/c)
(code:comment "section 2: the exports")
(provide/contract
[create (amount/c . -> . account?)]
[balance (account? . -> . amount/c)]
[withdraw (->i ([acc account?]
[amt (acc) (and/c amount/c (<=/c (balance acc)))])
[result (acc amt)
(and/c account?
(lambda (res)
(>= (balance res)
(- (balance acc) amt))))])]
[deposit (->i ([acc account?]
[amt amount/c])
[result (acc amt)
(and/c account?
(lambda (res)
(>= (balance res)
(+ (balance acc) amt))))])])
(provide
(contract-out
[create (amount/c . -> . account?)]
[balance (account? . -> . amount/c)]
[withdraw (->i ([acc account?]
[amt (acc) (and/c amount/c (<=/c (balance acc)))])
[result (acc amt)
(and/c account?
(lambda (res)
(>= (balance res)
(- (balance acc) amt))))])]
[deposit (->i ([acc account?]
[amt amount/c])
[result (acc amt)
(and/c account?
(lambda (res)
(>= (balance res)
(+ (balance acc) amt))))])]))
(code:comment "section 3: the function definitions")
(define balance account-balance)
@ -386,16 +390,17 @@ racket
(flat-named-contract (format msg balance0) ctr))
(code:comment "section 2: the exports")
(provide/contract
[create (amount/c . -> . account?)]
[balance (account? . -> . amount/c)]
[withdraw (->i ([acc account?]
[amt (acc) (and/c amount/c (<=/c (balance acc)))])
[result (acc amt) (mk-account-contract acc amt >= msg>)])]
[deposit (->i ([acc account?]
[amt amount/c])
[result (acc amt)
(mk-account-contract acc amt <= msg<)])])
(provide
(contract-out
[create (amount/c . -> . account?)]
[balance (account? . -> . amount/c)]
[withdraw (->i ([acc account?]
[amt (acc) (and/c amount/c (<=/c (balance acc)))])
[result (acc amt) (mk-account-contract acc amt >= msg>)])]
[deposit (->i ([acc account?]
[amt amount/c])
[result (acc amt)
(mk-account-contract acc amt <= msg<)])]))
(code:comment "section 3: the function definitions")
(define balance account-balance)
@ -452,9 +457,10 @@ racket
(define x '())
(define (get-x) x)
(define (f) (set! x (cons 'f x)))
(provide/contract
[f (->i () [_ (begin (set! x (cons 'ctc x)) any/c)])]
[get-x (-> (listof symbol?))])
(provide
(contract-out
[f (->i () [_ (begin (set! x (cons 'ctc x)) any/c)])]
[get-x (-> (listof symbol?))]))
]
If you were to require this module, call @racket[f], then
the result of @racket[get-x] would be @racket['(f ctc)]. In
@ -486,18 +492,18 @@ function arrow @racket[->], since @racket[->]
treats @racket[values] specially when it appears as the
last result:
@racketblock[
(provide/contract
[split (-> (listof char?)
(values string? (listof char?)))])
(provide (contract-out
[split (-> (listof char?)
(values string? (listof char?)))]))
]
The contract for such a function can also be written
using @racket[->*]:
@racketblock[
(provide/contract
[split (->* ((listof char?))
()
(values string? (listof char?)))])
(provide (contract-out
[split (->* ((listof char?))
()
(values string? (listof char?)))]))
]
As before, the contract for the argument with @racket[->*] is wrapped in an
extra pair of parentheses (and must always be wrapped like
@ -518,10 +524,11 @@ Now, suppose that we also want to ensure that the first result of
(<= (string-length s2) s)
(equal? (substring s 0 (string-length s2)) s2)))))
(provide/contract
[split (->i ([fl (listof char?)])
(values [s (fl) (substring-of (list->string fl))]
[c (listof char?)]))])
(provide
(contract-out
[split (->i ([fl (listof char?)])
(values [s (fl) (substring-of (list->string fl))]
[c (listof char?)]))]))
]
Like @racket[->*], the @racket[->i] combinator uses a function over the
argument to create the range contracts. Yes, it doesn't just return one
@ -534,10 +541,11 @@ Now, suppose that we also want to ensure that the first result of
This contract is expensive to check, of course. Here is a slightly
cheaper version:
@racketblock[
(provide/contract
[split (->i ([fl (listof char?)])
(values [s (fl) (string-len/c (length fl))]
[c (listof char?)]))])
(provide
(contract-out
[split (->i ([fl (listof char?)])
(values [s (fl) (string-len/c (length fl))]
[c (listof char?)]))]))
]
@ -603,16 +611,17 @@ because the given function accepts only one argument.
domain. It is then possible to combine this contract with an arity test to
specify the correct @racket[n-step]'s contract:
@racketblock[
(provide/contract
[n-step
(->i ([proc (inits)
(and/c (unconstrained-domain->
(or/c false/c number?))
(λ (f) (procedure-arity-includes?
f
(length inits))))]
[inits (listof number?)])
()
any)])
(provide
(contract-out
[n-step
(->i ([proc (inits)
(and/c (unconstrained-domain->
(or/c false/c number?))
(λ (f) (procedure-arity-includes?
f
(length inits))))]
[inits (listof number?)])
()
any)]))
]

View File

@ -30,7 +30,8 @@ racket
(if (= 1 x)
add1
(lambda (y) (+ x y))))
(provide/contract [make-adder (-> number? (-> number? number?))])
(provide (contract-out
[make-adder (-> number? (-> number? number?))]))
]
It exports the @racket[make-adder] function that is the usual curried
@ -107,10 +108,10 @@ checked, long enough to ensure that @racket[stream/c] is defined.
See also @ctc-link["lazy-contracts"].
@ctc-section{Mixing @racket[set!] and @racket[provide/contract]}
@ctc-section{Mixing @racket[set!] and @racket[contract-out]}
The contract library assumes that variables exported via
@racket[provide/contract] are not assigned to, but does not enforce
@racket[contract-out] are not assigned to, but does not enforce
it. Accordingly, if you try to @racket[set!] those variables, you
may be surprised. Consider the following example:
@ -118,8 +119,8 @@ may be surprised. Consider the following example:
(module server racket
(define (inc-x!) (set! x (+ x 1)))
(define x 0)
(provide/contract [inc-x! (-> void?)]
[x integer?]))
(provide (contract-out [inc-x! (-> void?)]
[x integer?])))
(module client racket
(require 'server)
@ -146,8 +147,8 @@ racket
(define (get-x) x)
(define (inc-x!) (set! x (+ x 1)))
(define x 0)
(provide/contract [inc-x! (-> void?)]
[get-x (-> integer?)])
(provide (contract-out [inc-x! (-> void?)]
[get-x (-> integer?)]))
]
Moral: This is a bug that we will address in a future release.

View File

@ -20,8 +20,8 @@ of exported values. For example, the export specification
@racketmod[
racket
(provide/contract
[amount positive?])
(provide (contract-out [amount positive?]))
(define amount ...)
]
@ -39,8 +39,8 @@ require the contracts library like this:
racket/base
(require racket/contract) (code:comment "now we can write contracts")
(provide/contract
[amount positive?])
(provide (contract-out [amount positive?]))
(define amount ...)
]
@ -51,8 +51,8 @@ If we bind @racket[amount] to a number that is not positive,
@racketmod[
racket
(provide/contract
[amount positive?])
(provide (contract-out [amount positive?]))
(define amount 0)]
then, when the module is required, the monitoring
@ -67,8 +67,8 @@ to a non-number value:
@racketmod[
racket
(provide/contract
[amount positive?])
(provide (contract-out [amount positive?]))
(define amount 'amount)
]
@ -80,8 +80,7 @@ values, we can ensure that the value is both a number and is
positive, combining the two contracts with @racket[and/c]:
@racketblock[
(provide/contract
[amount (and/c number? positive?)])
(provide (contract-out [amount (and/c number? positive?)]))
]
@;{
@ -215,7 +214,7 @@ this section as follows:
racket/load
(module m racket
(provide/contract [amount (and/c number? positive?)])
(provide (contract-out [amount (and/c number? positive?)]))
(define amount 150))
(module n racket

View File

@ -28,9 +28,9 @@ Here is a module that might represent a bank account:
@racketmod[
racket
(provide/contract
[deposit (-> number? any)]
[balance (-> number?)])
(provide (contract-out
[deposit (-> number? any)]
[balance (-> number?)]))
(define amount 0)
(define (deposit a) (set! amount (+ amount a)))
@ -79,8 +79,8 @@ If you are used to mathematical function, you may prefer a contract
people's code:
@racketblock[
(provide/contract
[deposit (number? . -> . any)])
(provide (contract-out
[deposit (number? . -> . any)]))
]
If a Racket S-expression contains two dots with a symbol in the middle,
@ -159,12 +159,12 @@ racket
(define (amount? a)
(and (number? a) (integer? a) (exact? a) (>= a 0)))
(provide/contract
(code:comment "an amount is a natural number of cents")
(code:comment "is the given number an amount?")
[deposit (-> amount? any)]
[amount? (-> any/c boolean?)]
[balance (-> amount?)])
(provide (contract-out
(code:comment "an amount is a natural number of cents")
(code:comment "is the given number an amount?")
[deposit (-> amount? any)]
[amount? (-> any/c boolean?)]
[balance (-> amount?)]))
(define amount 0)
(define (deposit a) (set! amount (+ amount a)))
@ -190,9 +190,9 @@ In this case, we could also have used @racket[natural-number/c] in
place of @racket[amount?], since it implies exactly the same check:
@racketblock[
(provide/contract
[deposit (-> natural-number/c any)]
[balance (-> natural-number/c)])
(provide (contract-out
[deposit (-> natural-number/c any)]
[balance (-> natural-number/c)]))
]
Every function that accepts one argument can be treated as a predicate
@ -205,9 +205,9 @@ to write the contracts above:
(define amount/c
(and/c number? integer? exact? (or/c positive? zero?)))
(provide/contract
[deposit (-> amount/c any)]
[balance (-> amount/c)])
(provide (contract-out
[deposit (-> amount/c any)]
[balance (-> amount/c)]))
]
Other values also serve double duty as contracts. For example, if a
@ -229,14 +229,14 @@ racket
(and (>= L 3)
(char=? #\. (string-ref str (- L 3)))))
(provide/contract
(code:comment "convert a random number to a string")
[format-number (-> number? string?)]
(provide (contract-out
(code:comment "convert a random number to a string")
[format-number (-> number? string?)]
(code:comment "convert an amount into a string with a decimal")
(code:comment "point, as in an amount of US currency")
[format-nat (-> natural-number/c
(and/c string? has-decimal?))])
(code:comment "convert an amount into a string with a decimal")
(code:comment "point, as in an amount of US currency")
[format-nat (-> natural-number/c
(and/c string? has-decimal?))]))
]
The contract of the exported function @racket[format-number] specifies
that the function consumes a number and produces a string. The
@ -270,13 +270,13 @@ racket
....
(provide/contract
....
(code:comment "convert an amount (natural number) of cents")
(code:comment "into a dollar based string")
[format-nat (-> natural-number/c
(and/c string?
is-decimal-string?))])
(provide (contract-out
....
(code:comment "convert an amount (natural number) of cents")
(code:comment "into a dollar-based string")
[format-nat (-> natural-number/c
(and/c string?
is-decimal-string?))]))
]
Alternately, in this case, we could use a regular expression as a
@ -285,12 +285,13 @@ contract:
@racketmod[
racket
(provide/contract
(provide
(contract-out
....
(code:comment "convert an amount (natural number) of cents")
(code:comment "into a dollar based string")
(code:comment "into a dollar-based string")
[format-nat (-> natural-number/c
(and/c string? #rx"[0-9]*\\.[0-9][0-9]"))])
(and/c string? #rx"[0-9]*\\.[0-9][0-9]"))]))
]
@; ------------------------------------------------------------------------
@ -337,10 +338,11 @@ piece of art:
@racketmod[
racket
(provide/contract
[deposit (-> (lambda (x)
(and (number? x) (integer? x) (>= x 0)))
any)])
(provide
(contract-out
[deposit (-> (lambda (x)
(and (number? x) (integer? x) (>= x 0)))
any)]))
(define this 0)
(define (deposit a) ...)
@ -372,8 +374,7 @@ racket
(define (amount? x) (and (number? x) (integer? x) (>= x 0)))
(define amount (flat-named-contract 'amount amount?))
(provide/contract
[deposit (amount . -> . any)])
(provide (contract-out [deposit (amount . -> . any)]))
(define this 0)
(define (deposit a) ...)

View File

@ -26,8 +26,8 @@ racket
(define origin (make-posn 0 0))
(provide/contract
[origin (struct/c posn zero? zero?)])
(provide (contract-out
[origin (struct/c posn zero? zero?)]))
]
In this example, the module imports a library for representing positions, which
@ -48,10 +48,10 @@ informal data definition as follows:
racket
(struct posn (x y))
(provide/contract
[struct posn ((x number?) (y number?))]
[p-okay posn?]
[p-sick posn?])
(provide (contract-out
[struct posn ((x number?) (y number?))]
[p-okay posn?]
[p-sick posn?]))
(define p-okay (posn 10 20))
(define p-sick (posn 'a 'b))
@ -110,9 +110,10 @@ If we want to fix the contract for @racket[p-sick] so that the error
is caught when @racket[sick] is exported, a single change suffices:
@racketblock[
(provide/contract
...
[p-sick (struct/c posn number? number?)])
(provide
(contract-out
...
[p-sick (struct/c posn number? number?)]))
]
That is, instead of exporting @racket[p-sick] as a plain
@ -166,9 +167,9 @@ racket
(define (bst? b) (bst-between? b -inf.0 +inf.0))
(provide (struct node (val left right)))
(provide/contract
[bst? (any/c . -> . boolean?)]
[in? (number? bst? . -> . boolean?)])
(provide (contract-out
[bst? (any/c . -> . boolean?)]
[in? (number? bst? . -> . boolean?)]))
]
In a full binary search tree, this means that
@ -231,9 +232,9 @@ racket
(define bst/c (bst-between/c -inf.0 +inf.0))
(provide make-node node-left node-right node-val node?)
(provide/contract
[bst/c contract?]
[in? (number? bst/c . -> . boolean?)])
(provide (contract-out
[bst/c contract?]
[in? (number? bst/c . -> . boolean?)]))
]
In general, each use of @racket[node/dc] must name the

View File

@ -15,7 +15,7 @@
The contract system guards one part of a program from
another. Programmers specify the behavior of a module's exports via
@racket[provide/contract], and the contract system enforces those
@racket[(provide (contract-out ....))], and the contract system enforces those
constraints.
@(define-syntax-rule
@ -721,13 +721,14 @@ function itself.
For example, the contract
@racketblock[
(provide/contract
[f (->d ([size natural-number/c]
[proc (and/c (unconstrained-domain-> number?)
(lambda (p)
(procedure-arity-includes? p size)))])
()
number?)])
(provide
(contract-out
[f (->d ([size natural-number/c]
[proc (and/c (unconstrained-domain-> number?)
(lambda (p)
(procedure-arity-includes? p size)))])
()
number?)]))
]
says that the function @racket[f] accepts a natural number
@ -760,7 +761,7 @@ be blamed using the above contract:
@declare-exporting-ctc[racket/contract/parametric]
The most convenient way to use parametric contract is to use
@racket[provide/contract]'s @racket[#:exists] keyword.
@racket[contract-out]'s @racket[#:exists] keyword.
The @racketmodname[racket/contract/parametric] provides a few more,
general-purpose parametric contracts.
@ -920,7 +921,8 @@ racket
(product (kons-tl l))))]))
(provide kons? kons kons-hd kons-tl)
(provide/contract [product (-> (sorted-list/gt -inf.0) number?)])
(provide
(contract-out [product (-> (sorted-list/gt -inf.0) number?)]))
])
The module provides a single function, @racket[product] whose contract
@ -940,7 +942,7 @@ lazy contract.
@defform/subs[
#:literals (struct rename)
(provide/contract p/c-item ...)
(contract-out p/c-item ...)
([p/c-item
(struct id ((id contract-expr) ...))
(struct (id identifier) ((id contract-expr) ...))
@ -951,25 +953,30 @@ lazy contract.
[exists-variables identifier
(identifier ...)])]{
Can only appear at the top-level of a @racket[module]. As with
@racket[provide], each @racket[id] is provided from the module. In
A @racket[_provide-spec] for use in @racket[provide] (currently only for
the same @tech{phase level} as the @racket[provide] form; for example,
@racket[contract-out] cannot be nested within @racket[for-syntax]). Each @racket[id]
is provided from the module. In
addition, clients of the module must live up to the contract specified
by @racket[contract-expr] for each export.
The @racket[provide/contract] form treats modules as units of
The @racket[contract-out] form treats modules as units of
blame. The module that defines the provided variable is expected to
meet the positive (co-variant) positions of the contract. Each module
that imports the provided variable must obey the negative
(contra-variant) positions of the contract.
(contra-variant) positions of the contract. Each @racket[contract-expr]
in a @racket[contract-out] form is effectively moved to the end of the
enclosing module, so a @racket[contract-expr] can refer to variables
that are defined later in the same module.
Only uses of the contracted variable outside the module are
checked. Inside the module, no contract checking occurs.
The @racket[rename] form of a @racket[provide/contract] exports the
The @racket[rename] form of @racket[contract-out] exports the
first variable (the internal name) with the name specified by the
second variable (the external name).
The @racket[struct] form of a @racket[provide/contract] clause
The @racket[struct] form of @racket[contract-out]
provides a structure-type definition, and each field has a contract
that dictates the contents of the fields. The structure-type
definition must appear before the @racket[provide] clause within the
@ -985,11 +992,11 @@ exported structure-type name always doubles as a constructor, even if
the original structure-type name does not act as a constructor.
The @racket[#:∃] and @racket[#:exists] clauses define new abstract
contracts. The variables are bound in the remainder of the @racket[provide/contract]
expression to new contracts that hide the values they accept and
contracts. The variables are bound in the remainder of the @racket[contract-out]
form to new contracts that hide the values they accept and
ensure that the exported functions are treated parametrically.
The implementation of @racket[provide/contract] attaches uses
The implementation of @racket[contract-out] attaches uses
@racket[syntax-property] to attach properties to the code it generates
that records the syntax of the contracts in the fully expanded program.
Specifically, the symbol @racket['provide/contract-original-contract]
@ -998,6 +1005,13 @@ syntax object for the expression that produces the contract controlling
the export.
}
@defform[(provide/contract p/c-item ...)]{
A legacy shorthand for @racket[(provide (contract-out p/c-item ...))],
except that a @racket[_contract-expr] within @racket[provide/contract]
is evaluated at the position of the @racket[provide/contract] form
instead of at the end of the enclosing module.}
@subsection{Nested Contract Boundaries}
@defmodule*/no-declare[(racket/contract/region)]
@declare-exporting-ctc[racket/contract/region]

View File

@ -54,11 +54,19 @@
;; tests a passing specification
(define (test/spec-passed name expression)
(printf "testing: ~s\n" name)
(contract-eval
`(,test
(void)
(let ([for-each-eval (lambda (l) (for-each eval l))]) for-each-eval)
(list ',expression '(void))))
(parameterize ([compile-enforce-module-constants #f])
(contract-eval
`(,test
(void)
(let ([for-each-eval (lambda (l) (for-each eval l))]) for-each-eval)
(list ',expression '(void))))
(let ([new-expression (rewrite-out expression)])
(unless (equal? new-expression expression)
(contract-eval
`(,test
(void)
(let ([for-each-eval (lambda (l) (for-each eval l))]) for-each-eval)
(list ',new-expression '(void)))))))
(let/ec k
(contract-eval
`(,test (void)
@ -76,6 +84,19 @@
eval
',(rewrite expression k)))))
;; rewrites `provide/contract' to use `contract-out'
(define (rewrite-out exp)
(let loop ([exp exp])
(cond
[(null? exp) null]
[(list? exp)
(case (car exp)
[(provide/contract) `(provide (contract-out . ,(cdr exp)))]
[else (map loop exp)])]
[(pair? exp) (cons (loop (car exp))
(loop (cdr exp)))]
[else exp])))
;; rewrites `contract' to use opt/c. If there is a module definition in there, we skip that test.
(define (rewrite exp k)
(let loop ([exp exp])
@ -11579,7 +11600,20 @@ so that propagation occurs.
(compose blame-positive exn:fail:contract:blame-object)
(with-handlers ((void values)) (contract not #t 'pos 'neg))))
;; check that `contract-out' contracts can use contracts
;; defined later in the module
(test/spec-passed/result
'contract-out1
'(begin
(eval '(module contract-out1-m racket/base
(require racket/contract)
(provide (contract-out [f (-> ok? ok?)]))
(define (f x) (+ x 1))
(define (ok? v) (exact-integer? v))))
(eval '(require 'contract-out1-m))
(eval '(f 10)))
11)
;
;