Added automatic blame-tracking to poly/c contract in unstable (and updated use in Typed Scheme).
svn: r18075
This commit is contained in:
Carl Eastlund
parent
90c8fcff11
commit
1b28ea1a6c
|
|
@ -122,18 +122,14 @@
|
|||
#`(cons/c #,(t->c t1) #,(t->c t2))]
|
||||
[(Opaque: p? cert)
|
||||
#`(flat-named-contract (quote #,(syntax-e p?)) #,(cert p?))]
|
||||
[(F: v) (cond [(assoc v (vars)) => (if pos? second third)]
|
||||
[(F: v) (cond [(assoc v (vars)) => second]
|
||||
[else (int-err "unknown var: ~a" v)])]
|
||||
[(Poly: vs (and b (Function: _)))
|
||||
(match-let ([(Poly-names: vs-nm _) ty])
|
||||
(with-syntax ([(vs+ ...) (generate-temporaries (for/list ([v vs-nm]) (format-symbol "~a+" v)))]
|
||||
[(vs- ...) (generate-temporaries (for/list ([v vs-nm]) (format-symbol "~a-" v)))])
|
||||
(parameterize ([vars (append (map list
|
||||
vs
|
||||
(syntax->list #'(vs+ ...))
|
||||
(syntax->list #'(vs- ...)))
|
||||
(with-syntax ([(v ...) (generate-temporaries vs-nm)])
|
||||
(parameterize ([vars (append (map list vs (syntax->list #'(v ...)))
|
||||
(vars))])
|
||||
#`(poly/c ([vs- vs+] ...) #,(t->c b)))))]
|
||||
#`(poly/c (v ...) #,(t->c b)))))]
|
||||
[(Mu: n b)
|
||||
(match-let ([(Mu-name: n-nm _) ty])
|
||||
(with-syntax ([(n*) (generate-temporaries (list n-nm))])
|
||||
|
|
|
|||
|
|
@ -1,73 +1,87 @@
|
|||
#lang scheme/base
|
||||
|
||||
(require scheme/contract (for-syntax scheme/base))
|
||||
(require scheme/bool scheme/contract)
|
||||
|
||||
(provide memory/c apply/c poly/c)
|
||||
(provide poly/c parametric/c opaque/c memory/c)
|
||||
|
||||
(with-contract
|
||||
poly-internals
|
||||
([memory/c
|
||||
(->*
|
||||
[]
|
||||
[ #:name any/c
|
||||
#:to any/c
|
||||
#:from any/c
|
||||
#:weak boolean?
|
||||
#:equal (or/c 'eq 'eqv 'equal)
|
||||
#:table (-> (and/c hash? (not/c immutable?))) ]
|
||||
(values flat-contract? flat-contract?))]
|
||||
[apply/c (->* [any/c] [#:name any/c] contract?)])
|
||||
(define-syntax-rule (poly/c [x ...] c)
|
||||
(make-polymorphic-contract 'poly/c
|
||||
memory/c
|
||||
'(x ...)
|
||||
(lambda (x ...) c)))
|
||||
|
||||
(define (memory/c
|
||||
#:name [name "memory/c"]
|
||||
#:to [to (format "~a:to" name)]
|
||||
#:from [from (format "~a:from" name)]
|
||||
#:weak [weak? #t]
|
||||
#:equal [equal 'eq]
|
||||
#:table [make-table
|
||||
(case equal
|
||||
[(eq) (if weak? make-weak-hasheq make-hasheq)]
|
||||
[(eqv) (if weak? make-weak-hasheqv make-hasheqv)]
|
||||
[(equal) (if weak? make-weak-hash make-hash)])])
|
||||
(let* ([table (make-table)])
|
||||
(values
|
||||
(flat-named-contract from
|
||||
(lambda (v) (hash-set! table v #t) #t))
|
||||
(flat-named-contract to
|
||||
(lambda (v) (hash-ref table v #f))))))
|
||||
(define-syntax-rule (parametric/c [x ...] c)
|
||||
(make-polymorphic-contract 'parametric/c
|
||||
opaque/c
|
||||
'(x ...)
|
||||
(lambda (x ...) c)))
|
||||
|
||||
(define (apply/c c
|
||||
#:name [name (build-compound-type-name 'apply/c c)])
|
||||
(simple-contract
|
||||
#:name name
|
||||
#:projection
|
||||
(lambda (blame)
|
||||
(lambda (p)
|
||||
(let* ([ctc (coerce-contract 'apply/c c)]
|
||||
[thunk
|
||||
(lambda ()
|
||||
(((contract-projection ctc) blame) p))])
|
||||
(make-keyword-procedure
|
||||
(lambda (keys vals . args) (keyword-apply (thunk) keys vals args))
|
||||
(case-lambda
|
||||
[() ((thunk))]
|
||||
[(a) ((thunk) a)]
|
||||
[(a b) ((thunk) a b)]
|
||||
[(a b c) ((thunk) a b c)]
|
||||
[(a b c d) ((thunk) a b c d)]
|
||||
[(a b c d e) ((thunk) a b c d e)]
|
||||
[(a b c d e f) ((thunk) a b c d e f)]
|
||||
[(a b c d e f g) ((thunk) a b c d e f g)]
|
||||
[(a b c d e f g h) ((thunk) a b c d e f g h)]
|
||||
[args (apply (thunk) args)])))))
|
||||
#:first-order procedure?)))
|
||||
(define-struct polymorphic-contract [title barrier vars body]
|
||||
#:property prop:contract
|
||||
(build-contract-property
|
||||
#:name
|
||||
(lambda (c)
|
||||
(list (polymorphic-contract-title c)
|
||||
(polymorphic-contract-vars c)
|
||||
'...))
|
||||
#:projection
|
||||
(lambda (c)
|
||||
(lambda (b)
|
||||
|
||||
(define-syntax (poly/c stx)
|
||||
(syntax-case stx ()
|
||||
[(_ opts ... ([c- c+] ...) c)
|
||||
(quasisyntax/loc stx
|
||||
(apply/c
|
||||
#:name (quote #,stx)
|
||||
(recursive-contract
|
||||
(let-values ([(c- c+) (memory/c #:from 'c- #:to 'c+ opts ...)] ...)
|
||||
c))))]))
|
||||
(define (wrap p)
|
||||
;; values in polymorphic types come in from negative position,
|
||||
;; relative to the poly/c contract
|
||||
(define negative? (blame-swapped? b))
|
||||
(define barrier/c (polymorphic-contract-barrier c))
|
||||
(define instances
|
||||
(for/list ([var (in-list (polymorphic-contract-vars c))])
|
||||
(barrier/c negative? var)))
|
||||
(define protector
|
||||
(apply (polymorphic-contract-body c) instances))
|
||||
(((contract-projection protector) b) p))
|
||||
|
||||
(lambda (p)
|
||||
(unless (procedure? p)
|
||||
(raise-blame-error b p "expected a procedure; got: ~e" p))
|
||||
(make-keyword-procedure
|
||||
(lambda (keys vals . args) (keyword-apply (wrap p) keys vals args))
|
||||
(case-lambda
|
||||
[() ((wrap p))]
|
||||
[(a) ((wrap p) a)]
|
||||
[(a b) ((wrap p) a b)]
|
||||
[(a b c) ((wrap p) a b c)]
|
||||
[(a b c d) ((wrap p) a b c d)]
|
||||
[(a b c d e) ((wrap p) a b c d e)]
|
||||
[(a b c d e f) ((wrap p) a b c d e f)]
|
||||
[(a b c d e f g) ((wrap p) a b c d e f g)]
|
||||
[(a b c d e f g h) ((wrap p) a b c d e f g h)]
|
||||
[args (apply (wrap p) args)])))))))
|
||||
|
||||
(define (memory/c positive? name)
|
||||
(define memory (make-weak-hasheq))
|
||||
(define (make x) (hash-set! memory x #t) x)
|
||||
(define (pred x) (hash-has-key? memory x))
|
||||
(define (get x) x)
|
||||
(make-barrier-contract name positive? make pred get))
|
||||
|
||||
(define (opaque/c positive? name)
|
||||
(define-values [ type make pred getter setter ]
|
||||
(make-struct-type name #f 1 0))
|
||||
(define (get x) (getter x 0))
|
||||
(make-barrier-contract name positive? make pred get))
|
||||
|
||||
(define-struct barrier-contract [name positive? make pred get]
|
||||
#:property prop:contract
|
||||
(build-contract-property
|
||||
#:name (lambda (c) (barrier-contract-name c))
|
||||
#:projection
|
||||
(lambda (c)
|
||||
(lambda (b)
|
||||
(if (boolean=? (blame-original? b) (barrier-contract-positive? c))
|
||||
(lambda (x)
|
||||
((barrier-contract-make c) x))
|
||||
(lambda (x)
|
||||
(if ((barrier-contract-pred c) x)
|
||||
((barrier-contract-get c) x)
|
||||
(raise-blame-error b x "expected a(n) ~a; got: ~e"
|
||||
(barrier-contract-name c) x))))))))
|
||||
|
|
|
|||
|
|
@ -5,60 +5,91 @@
|
|||
scheme/contract
|
||||
scheme/base))
|
||||
|
||||
@title[#:tag "poly-c"]{Anaphoric Contracts}
|
||||
@title[#:tag "poly-c"]{Polymorphic Contracts}
|
||||
|
||||
@(define the-eval (make-base-eval))
|
||||
@(the-eval '(require unstable/poly-c scheme/contract))
|
||||
@(define (build-eval)
|
||||
(let* ([e (make-base-eval)])
|
||||
(e '(require unstable/poly-c scheme/contract))
|
||||
e))
|
||||
|
||||
@defmodule[unstable/poly-c]
|
||||
|
||||
@unstable[@author+email["Sam Tobin-Hochstadt" "samth@ccs.neu.edu"]
|
||||
@author+email["Carl Eastlund" "cce@ccs.neu.edu"]]
|
||||
|
||||
@defform[(poly/c (x ...) c)]{
|
||||
|
||||
@defform[(poly/c ([id+ id-] ...) cnt)]{
|
||||
Creates an ``anaphoric'' contract, using the @scheme[id+ ...] as the
|
||||
positive positions, and the @scheme[id- ...] as the negative positions.
|
||||
Creates a contract for polymorphic functions that may inspect their arguments.
|
||||
Each function is protected by @scheme[c], where each @scheme[x] is bound in
|
||||
@scheme[c] and refers to a polymorphic type that is instantiated each time the
|
||||
function is applied.
|
||||
|
||||
Anaphoric contracts verify that only values provided to a given
|
||||
positive position flow out of the corresponding negative position.
|
||||
At each application of a function, the @scheme[poly/c] contract constructs a new
|
||||
weak, @scheme[eq?]-based hash table for each @scheme[x]. Values flowing into
|
||||
the polymorphic function (i.e. values protected by some @scheme[x] in negative
|
||||
position with respect to @scheme[poly/c]) are stored in the hash table. Values
|
||||
flowing out of the polymorphic function (i.e. protected by some @scheme[x] in
|
||||
positive position with respect to @scheme[poly/c]) are checked for their
|
||||
presence in the hash table. If they are present, they are returned; otherwise,
|
||||
a contract violation is signalled.
|
||||
|
||||
@examples[#:eval the-eval
|
||||
(define/contract (f x) (poly/c ([in out]) (in . -> . out))
|
||||
(if (equal? x 17) 18 x))
|
||||
(f 1)
|
||||
(f #f)
|
||||
(f 17)
|
||||
@examples[#:eval (build-eval)
|
||||
(define/contract (check x y) (poly/c [X] (boolean? X . -> . X))
|
||||
(if (or (not x) (equal? y 'surprise))
|
||||
'invalid
|
||||
y))
|
||||
(check #t 'ok)
|
||||
(check #f 'ignored)
|
||||
(check #t 'surprise)
|
||||
]
|
||||
|
||||
}
|
||||
|
||||
@defproc[(apply/c [cnt any/c]
|
||||
[#:name name any/c
|
||||
(build-compound-type-name 'apply/c c)]) contract?]{
|
||||
Produces a procedure contract that is like @scheme[cnt], but any delayed
|
||||
evalutation in @scheme[cnt] is re-done on every
|
||||
application of the contracted function.
|
||||
@defform[(parametric/c (x ...) c)]{
|
||||
|
||||
Creates a contract for parametric polymorphic functions. Each function is
|
||||
protected by @scheme[c], where each @scheme[x] is bound in @scheme[c] and refers
|
||||
to a polymorphic type that is instantiated each time the function is applied.
|
||||
|
||||
At each application of a function, the @scheme[parametric/c] contract constructs
|
||||
a new opaque wrapper for each @scheme[x]; values flowing into the polymorphic
|
||||
function (i.e. values protected by some @scheme[x] in negative position with
|
||||
respect to @scheme[parametric/c]) are wrapped in the corresponding opaque
|
||||
wrapper. Values flowing out of the polymorphic function (i.e. values protected
|
||||
by some @scheme[x] in positive position with respect to @scheme[parametric/c])
|
||||
are checked for the appropriate wrapper. If they have it, they are unwrapped;
|
||||
if they do not, a contract violation is signalled.
|
||||
|
||||
@examples[#:eval (build-eval)
|
||||
(define/contract (check x y) (parametric/c [X] (boolean? X . -> . X))
|
||||
(if (or (not x) (equal? y 'surprise))
|
||||
'invalid
|
||||
y))
|
||||
(check #t 'ok)
|
||||
(check #f 'ignored)
|
||||
(check #t 'surprise)
|
||||
]
|
||||
|
||||
}
|
||||
|
||||
@defproc[(memory/c [#:name name any/c "memory/c"]
|
||||
[#:from from any/c (format "~a:from" name)]
|
||||
[#:to to any/c (format "~a:to" name)]
|
||||
[#:weak weak? any/c #t]
|
||||
[#:equal equal (or/c 'eq 'eqv 'equal) 'eq]
|
||||
[#:table make-table (-> hash?)
|
||||
(case equal
|
||||
[(eq) (if weak? make-weak-hasheq make-hasheq)]
|
||||
[(eqv) (if weak? make-weak-hasheqv make-hasheqv)]
|
||||
[(equal) (if weak? make-weak-hash make-hash)])]
|
||||
)
|
||||
(values flat-contract? flat-contract?)]{
|
||||
@defproc[(memory/c [positive? boolean?] [name any/c]) contract?]{
|
||||
|
||||
Produces a pair of contracts. The first contract remembers all values
|
||||
that flow into it, and rejects nothing. The second accepts only
|
||||
values that have previously been passed to the first contract.
|
||||
This function constructs a contract that records values flowing in one direction
|
||||
in a fresh, weak hash table, and looks up values flowing in the other direction,
|
||||
signalling a contract violation if those values are not in the table.
|
||||
|
||||
If @scheme[weak?] is not @scheme[#f], the first contract holds onto
|
||||
the values only weakly. @scheme[from] and @scheme[to] are the names
|
||||
of the of the two contracts. }
|
||||
If @scheme[positive?] is true, values in positive position get stored and values
|
||||
in negative position are checked. Otherwise, the reverse happens.
|
||||
|
||||
}
|
||||
|
||||
@defproc[(opaque/c [positive? boolean?] [name any/c]) contract?]{
|
||||
|
||||
This function constructs a contract that wraps values flowing in one direction
|
||||
in a unique, opaque wrapper, and unwraps values flowing in the other direction,
|
||||
signalling a contract violation if those values are not wrapped.
|
||||
|
||||
If @scheme[positive?] is true, values in positive position get wrapped and
|
||||
values in negative position get unwrapped. Otherwise, the reverse happens.
|
||||
|
||||
}
|
||||
|
|
|
|||
Loading…
Reference in New Issue
Block a user