added scheme/exists lang and some docs in the guide about #:exists contracts
svn: r15879
This commit is contained in:
parent
bc404aaa54
commit
5f688d1144
|
@ -27,6 +27,7 @@ differences from v3:
|
||||||
check-procedure
|
check-procedure
|
||||||
check-procedure/more)
|
check-procedure/more)
|
||||||
(except-out (all-from-out "private/contract.ss")
|
(except-out (all-from-out "private/contract.ss")
|
||||||
|
∃?
|
||||||
check-between/c
|
check-between/c
|
||||||
check-unary-between/c))
|
check-unary-between/c))
|
||||||
|
|
||||||
|
|
255
collects/scheme/exists/lang.ss
Normal file
255
collects/scheme/exists/lang.ss
Normal file
|
@ -0,0 +1,255 @@
|
||||||
|
#lang scheme
|
||||||
|
|
||||||
|
(require "../private/contract.ss")
|
||||||
|
|
||||||
|
;; this code builds the list of predicates (in case it changes, this may need to be re-run)
|
||||||
|
#;
|
||||||
|
(define predicates
|
||||||
|
(let ([fn (build-path (collection-path "scheme")
|
||||||
|
"compiled"
|
||||||
|
"main_ss.zo")])
|
||||||
|
(let-values ([(vars stx)
|
||||||
|
(module-compiled-exports
|
||||||
|
(parameterize ([read-accept-compiled #t])
|
||||||
|
(call-with-input-file fn read)))])
|
||||||
|
|
||||||
|
(filter (λ (sym)
|
||||||
|
(let ([str (symbol->string sym)])
|
||||||
|
(and (not (equal? str ""))
|
||||||
|
(regexp-match #rx"[?]$" str)
|
||||||
|
(not (regexp-match #rx"[=<>][?]$" str)))))
|
||||||
|
(map car (cdr (assoc 0 vars)))))))
|
||||||
|
|
||||||
|
|
||||||
|
(define-for-syntax predicates
|
||||||
|
'(absolute-path?
|
||||||
|
arity-at-least?
|
||||||
|
bitwise-bit-set?
|
||||||
|
boolean?
|
||||||
|
box?
|
||||||
|
byte-pregexp?
|
||||||
|
byte-ready?
|
||||||
|
byte-regexp?
|
||||||
|
byte?
|
||||||
|
bytes-converter?
|
||||||
|
bytes?
|
||||||
|
channel?
|
||||||
|
char-alphabetic?
|
||||||
|
char-blank?
|
||||||
|
char-graphic?
|
||||||
|
char-iso-control?
|
||||||
|
char-lower-case?
|
||||||
|
char-numeric?
|
||||||
|
char-punctuation?
|
||||||
|
char-ready?
|
||||||
|
char-symbolic?
|
||||||
|
char-title-case?
|
||||||
|
char-upper-case?
|
||||||
|
char-whitespace?
|
||||||
|
char?
|
||||||
|
class?
|
||||||
|
compiled-expression?
|
||||||
|
compiled-module-expression?
|
||||||
|
complete-path?
|
||||||
|
complex?
|
||||||
|
cons?
|
||||||
|
continuation-mark-set?
|
||||||
|
continuation-prompt-available?
|
||||||
|
continuation-prompt-tag?
|
||||||
|
continuation?
|
||||||
|
contract-first-order-passes?
|
||||||
|
contract-stronger?
|
||||||
|
contract?
|
||||||
|
custodian-box?
|
||||||
|
custodian-memory-accounting-available?
|
||||||
|
custodian?
|
||||||
|
custom-write?
|
||||||
|
date-dst?
|
||||||
|
date?
|
||||||
|
dict-can-functional-set?
|
||||||
|
dict-can-remove-keys?
|
||||||
|
dict-mutable?
|
||||||
|
dict?
|
||||||
|
directory-exists?
|
||||||
|
empty?
|
||||||
|
eof-object?
|
||||||
|
ephemeron?
|
||||||
|
eq?
|
||||||
|
equal?
|
||||||
|
eqv?
|
||||||
|
even?
|
||||||
|
evt?
|
||||||
|
exact-integer?
|
||||||
|
exact-nonnegative-integer?
|
||||||
|
exact-positive-integer?
|
||||||
|
exact?
|
||||||
|
exn:break?
|
||||||
|
exn:fail:contract2?
|
||||||
|
exn:fail:contract:arity?
|
||||||
|
exn:fail:contract:continuation?
|
||||||
|
exn:fail:contract:divide-by-zero?
|
||||||
|
exn:fail:contract:variable?
|
||||||
|
exn:fail:contract?
|
||||||
|
exn:fail:filesystem:exists?
|
||||||
|
exn:fail:filesystem:version?
|
||||||
|
exn:fail:filesystem?
|
||||||
|
exn:fail:network?
|
||||||
|
exn:fail:object?
|
||||||
|
exn:fail:out-of-memory?
|
||||||
|
exn:fail:read:eof?
|
||||||
|
exn:fail:read:non-char?
|
||||||
|
exn:fail:read?
|
||||||
|
exn:fail:syntax?
|
||||||
|
exn:fail:unsupported?
|
||||||
|
exn:fail:user?
|
||||||
|
exn:fail?
|
||||||
|
exn:misc:match?
|
||||||
|
exn:srclocs?
|
||||||
|
exn?
|
||||||
|
false?
|
||||||
|
file-exists?
|
||||||
|
file-stream-port?
|
||||||
|
fixnum?
|
||||||
|
flat-contract?
|
||||||
|
flat-pred?
|
||||||
|
generic?
|
||||||
|
handle-evt?
|
||||||
|
hash-eq?
|
||||||
|
hash-eqv?
|
||||||
|
hash-has-key?
|
||||||
|
hash-placeholder?
|
||||||
|
hash-weak?
|
||||||
|
hash?
|
||||||
|
identifier?
|
||||||
|
immutable?
|
||||||
|
implementation?
|
||||||
|
inexact-real?
|
||||||
|
inexact?
|
||||||
|
input-port?
|
||||||
|
inspector?
|
||||||
|
integer?
|
||||||
|
interface-extension?
|
||||||
|
interface?
|
||||||
|
internal-definition-context?
|
||||||
|
is-a?
|
||||||
|
keyword?
|
||||||
|
link-exists?
|
||||||
|
list?
|
||||||
|
log-level?
|
||||||
|
log-receiver?
|
||||||
|
logger?
|
||||||
|
member-name-key?
|
||||||
|
method-in-interface?
|
||||||
|
module-path-index?
|
||||||
|
module-path?
|
||||||
|
module-provide-protected?
|
||||||
|
mpair?
|
||||||
|
name-pred?
|
||||||
|
namespace-anchor?
|
||||||
|
namespace?
|
||||||
|
negative?
|
||||||
|
null?
|
||||||
|
number?
|
||||||
|
object-method-arity-includes?
|
||||||
|
object?
|
||||||
|
odd?
|
||||||
|
output-port?
|
||||||
|
pair?
|
||||||
|
parameter?
|
||||||
|
parameterization?
|
||||||
|
path-for-some-system?
|
||||||
|
path-string?
|
||||||
|
path?
|
||||||
|
placeholder?
|
||||||
|
port-closed?
|
||||||
|
port-provides-progress-evts?
|
||||||
|
port-writes-atomic?
|
||||||
|
port-writes-special?
|
||||||
|
port?
|
||||||
|
positive?
|
||||||
|
pregexp?
|
||||||
|
pretty-print-style-table?
|
||||||
|
primitive-closure?
|
||||||
|
primitive?
|
||||||
|
procedure-arity-includes?
|
||||||
|
procedure-arity?
|
||||||
|
procedure-closure-contents-eq?
|
||||||
|
procedure-struct-type?
|
||||||
|
procedure?
|
||||||
|
proj-pred?
|
||||||
|
promise-forced?
|
||||||
|
promise-running?
|
||||||
|
promise?
|
||||||
|
pseudo-random-generator?
|
||||||
|
rational?
|
||||||
|
readtable?
|
||||||
|
real?
|
||||||
|
regexp-match-exact?
|
||||||
|
regexp-match?
|
||||||
|
regexp?
|
||||||
|
relative-path?
|
||||||
|
rename-transformer?
|
||||||
|
resolved-module-path?
|
||||||
|
security-guard?
|
||||||
|
semaphore-try-wait?
|
||||||
|
semaphore?
|
||||||
|
sequence?
|
||||||
|
set!-transformer?
|
||||||
|
special-comment?
|
||||||
|
srcloc?
|
||||||
|
string?
|
||||||
|
stronger-pred?
|
||||||
|
struct-accessor-procedure?
|
||||||
|
struct-constructor-procedure?
|
||||||
|
struct-mutator-procedure?
|
||||||
|
struct-predicate-procedure?
|
||||||
|
struct-type-property?
|
||||||
|
struct-type?
|
||||||
|
struct?
|
||||||
|
subclass?
|
||||||
|
subprocess?
|
||||||
|
symbol-interned?
|
||||||
|
symbol?
|
||||||
|
syntax-local-transforming-module-provides?
|
||||||
|
syntax-original?
|
||||||
|
syntax-transforming?
|
||||||
|
syntax?
|
||||||
|
system-big-endian?
|
||||||
|
tcp-accept-ready?
|
||||||
|
tcp-listener?
|
||||||
|
tcp-port?
|
||||||
|
terminal-port?
|
||||||
|
thread-cell?
|
||||||
|
thread-dead?
|
||||||
|
thread-group?
|
||||||
|
thread-running?
|
||||||
|
thread?
|
||||||
|
udp-bound?
|
||||||
|
udp-connected?
|
||||||
|
udp?
|
||||||
|
unit?
|
||||||
|
unknown?
|
||||||
|
variable-reference?
|
||||||
|
vector?
|
||||||
|
void?
|
||||||
|
weak-box?
|
||||||
|
will-executor?
|
||||||
|
zero?))
|
||||||
|
|
||||||
|
(define-syntax (predicates/provide stx)
|
||||||
|
(with-syntax ([(predicates ...) predicates]
|
||||||
|
[(-predicates ...) (map (λ (x) (string->symbol (format "-~a" x))) predicates)])
|
||||||
|
#'(begin
|
||||||
|
(define -predicates
|
||||||
|
(let ([predicates (λ (x)
|
||||||
|
(if (∃? x)
|
||||||
|
(error 'predicates "supplied with a wrapped value ~e" x)
|
||||||
|
(predicates x)))])
|
||||||
|
predicates))
|
||||||
|
...
|
||||||
|
(provide (rename-out (-predicates predicates) ...)
|
||||||
|
(except-out (all-from-out scheme)
|
||||||
|
define-struct
|
||||||
|
predicates ...)))))
|
||||||
|
|
||||||
|
(predicates/provide)
|
2
collects/scheme/exists/lang/reader.ss
Normal file
2
collects/scheme/exists/lang/reader.ss
Normal file
|
@ -0,0 +1,2 @@
|
||||||
|
#lang s-exp syntax/module-reader
|
||||||
|
scheme/exists/lang
|
|
@ -16,7 +16,8 @@ improve method arity mismatch contract violation error messages?
|
||||||
define/contract
|
define/contract
|
||||||
with-contract
|
with-contract
|
||||||
current-contract-region
|
current-contract-region
|
||||||
new-∃/c)
|
new-∃/c
|
||||||
|
∃?)
|
||||||
|
|
||||||
(require (for-syntax scheme/base)
|
(require (for-syntax scheme/base)
|
||||||
(for-syntax "contract-opt-guts.ss")
|
(for-syntax "contract-opt-guts.ss")
|
||||||
|
@ -2654,8 +2655,10 @@ improve method arity mismatch contract violation error messages?
|
||||||
#:property stronger-prop
|
#:property stronger-prop
|
||||||
(λ (this that) #f))
|
(λ (this that) #f))
|
||||||
|
|
||||||
|
(define-struct ∃ ())
|
||||||
|
|
||||||
(define (new-∃/c raw-name)
|
(define (new-∃/c raw-name)
|
||||||
(define name (string->symbol (format "~a/∃" raw-name)))
|
(define name (string->symbol (format "~a/∃" raw-name)))
|
||||||
(define-values (struct-type constructor predicate accessor mutator)
|
(define-values (struct-type constructor predicate accessor mutator)
|
||||||
(make-struct-type name #f 1 0))
|
(make-struct-type name struct:∃ 1 0))
|
||||||
(make-∃/c constructor (λ (x) (accessor x 0)) predicate raw-name))
|
(make-∃/c constructor (λ (x) (accessor x 0)) predicate raw-name))
|
||||||
|
|
60
collects/scribblings/guide/contracts-exists.scrbl
Normal file
60
collects/scribblings/guide/contracts-exists.scrbl
Normal file
|
@ -0,0 +1,60 @@
|
||||||
|
#lang scribble/doc
|
||||||
|
@(require scribble/manual
|
||||||
|
scribble/eval
|
||||||
|
"guide-utils.ss"
|
||||||
|
"contracts-utils.ss"
|
||||||
|
(for-label scheme/contract))
|
||||||
|
|
||||||
|
@title[#:tag "contracts-exists"]{Abstract Contracts using @scheme[#:exists] and @scheme[#:∃]}
|
||||||
|
|
||||||
|
The contract system provides existential contracts that can
|
||||||
|
protect abstractions, ensuring that clients of your module
|
||||||
|
cannot depend on the precise representation choices you make
|
||||||
|
for your data structures.
|
||||||
|
|
||||||
|
@ctc-section{Getting started, with a stack example}
|
||||||
|
|
||||||
|
@margin-note{
|
||||||
|
You can type @scheme[#:exists] instead of @scheme[#:∃] if you
|
||||||
|
cannot easily type unicode characters; in DrScheme, typing
|
||||||
|
@tt{\exists} followed by either alt-\ or control-\ (depending
|
||||||
|
on your platform) will produce @scheme[∃].}.
|
||||||
|
The @scheme[provide/contract] form allows you to write
|
||||||
|
@schemeblock[#:∃ name-of-a-new-contract] as one of its clauses. This declaration
|
||||||
|
introduces the variable @scheme[name-of-a-new-contract], binding it to a new
|
||||||
|
contract that hides information about the values it protects.
|
||||||
|
|
||||||
|
As an example, consider this (simple) implementation of a stack datastructure:
|
||||||
|
@schememod[scheme
|
||||||
|
(define empty '())
|
||||||
|
(define (enq top queue) (append queue (list top)))
|
||||||
|
(define (next queue) (car queue))
|
||||||
|
(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?)])]
|
||||||
|
This code implements a queue purely in terms of lists, meaning that clients
|
||||||
|
of this data structure might use @scheme[car] and @scheme[cdr] directly on the
|
||||||
|
data structure (perhaps accidentally) and thus any change in the representation
|
||||||
|
(say to a more efficient representation that supports amortized constant time
|
||||||
|
enqueue and dequeue operations) might break client code.
|
||||||
|
|
||||||
|
To ensure that the stack representation is abstact, we can use @scheme[#:∃] in the
|
||||||
|
@scheme[provide/contract] expression, like this:
|
||||||
|
@schemeblock[(provide/contract
|
||||||
|
#:∃ 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 @scheme[car] and @scheme[cdr], they
|
||||||
|
receive an error, rather than mucking about with the internals of the queues.
|
||||||
|
|
||||||
|
See also @ctc-link["exists-gotcha"].
|
|
@ -52,6 +52,27 @@ the @scheme[eq?] call would return @scheme[#t].
|
||||||
|
|
||||||
Moral: do not use @scheme[eq?] on values that have contracts.
|
Moral: do not use @scheme[eq?] on values that have contracts.
|
||||||
|
|
||||||
|
@ctc-section[#:tag "exists-gotcha"]{Exists contracts and predicates}
|
||||||
|
|
||||||
|
Much like the @scheme[eq?] example above, @scheme[#:∃] contracts
|
||||||
|
can change the behavior of a program.
|
||||||
|
|
||||||
|
Specifically,
|
||||||
|
the @scheme[null?] predicate (and many other predicates) return @scheme[#f]
|
||||||
|
for @scheme[#:∃] contracts, and changing one of those contracts to @scheme[any/c]
|
||||||
|
means that @scheme[null?] might now return @scheme[#t] instead, resulting in
|
||||||
|
arbitrarily different behavior depending on this boolean might flow around
|
||||||
|
in the program.
|
||||||
|
|
||||||
|
@defmodulelang[scheme/exists]
|
||||||
|
|
||||||
|
To work around the above problem, the
|
||||||
|
@schememodname[scheme/exists] library behaves just like the @schememodname[scheme],
|
||||||
|
but where predicates signal errors when given @scheme[#:∃] contracts.
|
||||||
|
|
||||||
|
Moral: do not use predicates on @scheme[#:∃] contracts, but if you're not sure, use
|
||||||
|
@schememodname[scheme/exists] to be safe.
|
||||||
|
|
||||||
@ctc-section{Defining recursive contracts}
|
@ctc-section{Defining recursive contracts}
|
||||||
|
|
||||||
When defining a self-referential contract, it is natural to use
|
When defining a self-referential contract, it is natural to use
|
||||||
|
|
|
@ -40,5 +40,6 @@ update string-pad-center to show examples via REPL notation:
|
||||||
@include-section["contracts-simple-function.scrbl"]
|
@include-section["contracts-simple-function.scrbl"]
|
||||||
@include-section["contracts-general-function.scrbl"]
|
@include-section["contracts-general-function.scrbl"]
|
||||||
@include-section["contracts-structure.scrbl"]
|
@include-section["contracts-structure.scrbl"]
|
||||||
|
@include-section["contracts-exists.scrbl"]
|
||||||
@include-section["contracts-examples.scrbl"]
|
@include-section["contracts-examples.scrbl"]
|
||||||
@include-section["contracts-gotchas.scrbl"]
|
@include-section["contracts-gotchas.scrbl"]
|
||||||
|
|
Loading…
Reference in New Issue
Block a user