generalize the random contract generation so that it can exercise
a function to get more interesting values and then use those values to guarantee it can generate things it couldn't before For example, it can now generate a function with this contract: (-> (-> is-eleven?) is-eleven?) without knowing what the is-eleven? predicate does -- instead it can figure out to call the argument thunk and then pipe that result around
This commit is contained in:
parent
6343159701
commit
d4c60e8608
|
@ -2238,14 +2238,23 @@ is expected to be the contract on the value).
|
|||
(or/c (-> contract? contract? boolean?) #f)
|
||||
#f]
|
||||
[#:generate
|
||||
generator
|
||||
generate
|
||||
(->i ([c contract?])
|
||||
([generator
|
||||
(c)
|
||||
(-> (and/c positive? real?)
|
||||
(or/c #f
|
||||
(-> c)))]))
|
||||
#f])
|
||||
#f]
|
||||
[#:exercise
|
||||
exercise
|
||||
(->i ([c contract?])
|
||||
([result
|
||||
(c)
|
||||
(-> (and/c positive? real?)
|
||||
(values
|
||||
(-> c void?)
|
||||
(listof contract?)))]))])
|
||||
flat-contract-property?]
|
||||
@defproc[(build-chaperone-contract-property
|
||||
[#:name
|
||||
|
@ -2276,14 +2285,23 @@ is expected to be the contract on the value).
|
|||
(or/c (-> contract? contract? boolean?) #f)
|
||||
#f]
|
||||
[#:generate
|
||||
generator
|
||||
generate
|
||||
(->i ([c contract?])
|
||||
([generator
|
||||
(c)
|
||||
(-> (and/c positive? real?)
|
||||
(or/c #f
|
||||
(-> c)))]))
|
||||
#f])
|
||||
#f]
|
||||
[#:exercise
|
||||
exercise
|
||||
(->i ([c contract?])
|
||||
([result
|
||||
(c)
|
||||
(-> (and/c positive? real?)
|
||||
(values
|
||||
(-> c void?)
|
||||
(listof contract?)))]))])
|
||||
chaperone-contract-property?]
|
||||
@defproc[(build-contract-property
|
||||
[#:name
|
||||
|
@ -2314,14 +2332,23 @@ is expected to be the contract on the value).
|
|||
(or/c (-> contract? contract? boolean?) #f)
|
||||
#f]
|
||||
[#:generate
|
||||
generator
|
||||
generate
|
||||
(->i ([c contract?])
|
||||
([generator
|
||||
(c)
|
||||
(-> (and/c positive? real?)
|
||||
(or/c #f
|
||||
(-> c)))]))
|
||||
#f])
|
||||
#f]
|
||||
[#:exercise
|
||||
exercise
|
||||
(->i ([c contract?])
|
||||
([result
|
||||
(c)
|
||||
(-> (and/c positive? real?)
|
||||
(values
|
||||
(-> c void?)
|
||||
(listof contract?)))]))])
|
||||
contract-property?])]{
|
||||
|
||||
@italic{The precise details of the
|
||||
|
@ -2342,9 +2369,12 @@ which produces a description to @racket[write] as part of a contract violation;
|
|||
produces a blame-tracking projection defining the behavior of the contract;
|
||||
@racket[stronger], which is a predicate that determines whether this contract
|
||||
(passed in the first argument) is stronger than some other contract (passed
|
||||
in the second argument); and @racket[generate], which returns a thunk
|
||||
in the second argument); @racket[generate], which returns a thunk
|
||||
that generates random values matching the contract or @racket[#f], indicating
|
||||
that random generation for this contract isn't supported.
|
||||
that random generation for this contract isn't supported; and @racket[exercise],
|
||||
which returns a function that exercises values matching the contract (e.g.,
|
||||
if it is a function contract, it may call the function) and a list of contracts
|
||||
whose values will be generated by this process.
|
||||
|
||||
These accessors are passed as (optional) keyword arguments to
|
||||
@racket[build-contract-property], and are applied to instances of the
|
||||
|
|
|
@ -72,3 +72,33 @@
|
|||
(check-exn cannot-generate-exn? (λ () (test-contract-generation
|
||||
(or/c some-crazy-predicate?
|
||||
some-crazy-predicate?))))
|
||||
|
||||
(check-not-exn
|
||||
(λ ()
|
||||
(define eleven
|
||||
((test-contract-generation (-> (-> some-crazy-predicate?) some-crazy-predicate?))
|
||||
(λ () 11)))
|
||||
(unless (= eleven 11)
|
||||
(error 'contract-rand-test.rkt "expected 11 got ~s" eleven))))
|
||||
|
||||
(check-not-exn
|
||||
(λ ()
|
||||
(define eleven
|
||||
((test-contract-generation (-> (-> number? boolean? some-crazy-predicate?)
|
||||
some-crazy-predicate?))
|
||||
(λ (n b) 11)))
|
||||
(unless (= eleven 11)
|
||||
(error 'contract-rand-test.rkt "expected 11 got ~s" eleven))))
|
||||
|
||||
(check-not-exn
|
||||
(λ ()
|
||||
(define eleven
|
||||
((test-contract-generation (-> (non-empty-listof some-crazy-predicate?)
|
||||
some-crazy-predicate?))
|
||||
(list 11)))
|
||||
(unless (= eleven 11)
|
||||
(error 'contract-rand-test.rkt "expected 11 got ~s" eleven))))
|
||||
|
||||
(check-exn cannot-generate-exn? (λ () (test-contract-generation
|
||||
(-> (listof some-crazy-predicate?)
|
||||
some-crazy-predicate?))))
|
||||
|
|
|
@ -716,9 +716,15 @@
|
|||
(define dom-ctcs (base->-doms ctc))
|
||||
(define doms-l (length dom-ctcs))
|
||||
(λ (fuel)
|
||||
(define dom-exers '())
|
||||
(define addl-available dom-ctcs)
|
||||
(for ([c (in-list (base->-doms ctc))])
|
||||
(define-values (exer ctcs) ((contract-struct-exercise c) fuel))
|
||||
(set! dom-exers (cons exer dom-exers))
|
||||
(set! addl-available (append ctcs addl-available)))
|
||||
(define rngs-gens
|
||||
(with-definitely-available-contracts
|
||||
dom-ctcs
|
||||
(with-definitely-available-contracts
|
||||
addl-available
|
||||
(λ ()
|
||||
(for/list ([c (in-list (base->-rngs ctc))])
|
||||
(generate/choose c fuel)))))
|
||||
|
@ -729,41 +735,76 @@
|
|||
(define env (generate-env))
|
||||
(procedure-reduce-arity
|
||||
(λ args
|
||||
; Make sure that the args match the contract
|
||||
(unless ((contract-struct-exercise ctc) args (/ fuel 2))
|
||||
(error '->-generate "Arg(s) ~a do(es) not match contract ~a\n" ctc))
|
||||
; Stash the valid value
|
||||
(parameterize ([generate-env env])
|
||||
(for ([ctc (in-list dom-ctcs)]
|
||||
[arg (in-list args)])
|
||||
(env-stash ctc arg))
|
||||
(define results
|
||||
(for/list ([rng-gen (in-list rngs-gens)])
|
||||
(rng-gen)))
|
||||
(apply values results)))
|
||||
; stash the arguments for use by other generators
|
||||
(for ([ctc (in-list dom-ctcs)]
|
||||
[arg (in-list args)])
|
||||
(env-stash env ctc arg))
|
||||
; exercise the arguments
|
||||
(for ([arg (in-list args)]
|
||||
[dom-exer (in-list dom-exers)])
|
||||
(dom-exer arg))
|
||||
; compute the results
|
||||
(define results
|
||||
(for/list ([rng-gen (in-list rngs-gens)])
|
||||
(rng-gen)))
|
||||
; return the results
|
||||
(apply values results))
|
||||
doms-l))]
|
||||
[else #f]))]
|
||||
[else (λ (fuel) #f)]))
|
||||
|
||||
(define (->-exercise ctc)
|
||||
(λ (args fuel)
|
||||
(let* ([new-fuel (/ fuel 2)]
|
||||
[gen-if-fun (λ (c v)
|
||||
; If v is a function we need to gen the domain and call
|
||||
(if (procedure? v)
|
||||
(let ([newargs (map (λ (c) (contract-random-generate c new-fuel))
|
||||
(base->-doms c))])
|
||||
(let* ([result (call-with-values
|
||||
(λ () (apply v newargs))
|
||||
list)]
|
||||
[rngs (base->-rngs c)])
|
||||
(andmap (λ (c v)
|
||||
((contract-struct-exercise c) v new-fuel))
|
||||
rngs
|
||||
result)))
|
||||
; Delegate to check-ctc-val
|
||||
((contract-struct-exercise c) v new-fuel)))])
|
||||
(andmap gen-if-fun (base->-doms ctc) args))))
|
||||
(define (->-exercise ctc)
|
||||
(define dom-ctcs (base->-doms ctc))
|
||||
(define rng-ctcs (base->-rngs ctc))
|
||||
(cond
|
||||
[(and (equal? (length dom-ctcs) (base->-min-arity ctc))
|
||||
(not (base->-rest ctc)))
|
||||
(λ (fuel)
|
||||
(define gens
|
||||
(for/list ([dom-ctc (in-list dom-ctcs)])
|
||||
((contract-struct-generate dom-ctc) fuel)))
|
||||
(define env (generate-env))
|
||||
(cond
|
||||
[(andmap values gens)
|
||||
(values
|
||||
(λ (f)
|
||||
(call-with-values
|
||||
(λ ()
|
||||
(apply
|
||||
f
|
||||
(for/list ([gen (in-list gens)])
|
||||
(gen))))
|
||||
(λ results
|
||||
(for ([res-ctc (in-list rng-ctcs)]
|
||||
[result (in-list results)])
|
||||
(env-stash env res-ctc result)))))
|
||||
(base->-rngs ctc))]
|
||||
[else
|
||||
(values void '())]))]
|
||||
[else
|
||||
(λ (fuel) (values void '()))]))
|
||||
|
||||
#|
|
||||
|
||||
(λ (v)
|
||||
(let* ([new-fuel (/ fuel 2)]
|
||||
[gen-if-fun (λ (c v)
|
||||
; If v is a function we need to gen the domain and call
|
||||
(if (procedure? v)
|
||||
(let ([newargs (map (λ (c) (contract-random-generate c new-fuel))
|
||||
(base->-doms c))])
|
||||
(let* ([result (call-with-values
|
||||
(λ () (apply v newargs))
|
||||
list)]
|
||||
[rngs (base->-rngs c)])
|
||||
(andmap (λ (c v)
|
||||
((contract-struct-exercise c) v new-fuel))
|
||||
rngs
|
||||
result)))
|
||||
; Delegate to check-ctc-val
|
||||
((contract-struct-exercise c) v new-fuel)))])
|
||||
(andmap gen-if-fun (base->-doms ctc) args)))))]
|
||||
|#
|
||||
|
||||
(define (base->-name ctc)
|
||||
(define rngs (base->-rngs ctc))
|
||||
|
|
|
@ -17,7 +17,7 @@
|
|||
|
||||
;; a stash of values and the contracts that they correspond to
|
||||
;; that generation has produced earlier in the process
|
||||
(define generate-env (make-parameter #f))
|
||||
(define generate-env (make-parameter 'generate-env-not-currently-set))
|
||||
|
||||
;; (parameter/c (listof contract?))
|
||||
;; contracts in this will definitely have values available
|
||||
|
@ -27,8 +27,7 @@
|
|||
|
||||
; Adds a new contract and value to the environment if
|
||||
; they don't already exist
|
||||
(define (env-stash ctc val)
|
||||
(define env (generate-env))
|
||||
(define (env-stash env ctc val)
|
||||
(define curvals (hash-ref env ctc '()))
|
||||
(hash-set! env ctc (cons val curvals)))
|
||||
|
||||
|
@ -36,7 +35,7 @@
|
|||
(parameterize ([definitely-available-contracts
|
||||
(append ctcs (definitely-available-contracts))])
|
||||
(thunk)))
|
||||
|
||||
|
||||
; generate : contract int -> ctc value or error
|
||||
(define (contract-random-generate ctc fuel
|
||||
[fail (λ ()
|
||||
|
@ -71,11 +70,12 @@
|
|||
; Attemps to find a value with the given contract in the environment.
|
||||
;; NB: this doesn't yet try to call things in the environment to generate
|
||||
(define (generate/env ctc fuel)
|
||||
(define env (generate-env))
|
||||
(for/or ([avail-ctc (in-list (definitely-available-contracts))])
|
||||
(and (contract-stronger? avail-ctc ctc)
|
||||
(λ ()
|
||||
(define available
|
||||
(for/list ([(avail-ctc vs) (in-hash (generate-env))]
|
||||
(for/list ([(avail-ctc vs) (in-hash env)]
|
||||
#:when (contract-stronger? avail-ctc ctc)
|
||||
[v (in-list vs)])
|
||||
v))
|
||||
|
|
|
@ -386,10 +386,7 @@
|
|||
(predicate-contract-name ctc)))
|
||||
(λ (fuel)
|
||||
(and built-in-generator
|
||||
(λ () (built-in-generator fuel))))])))
|
||||
#:exercise (λ (ctc)
|
||||
(λ (val fuel)
|
||||
((predicate-contract-pred ctc) val)))))
|
||||
(λ () (built-in-generator fuel))))])))))
|
||||
|
||||
(define (check-flat-named-contract predicate) (coerce-flat-contract 'flat-named-contract predicate))
|
||||
(define (check-flat-contract predicate) (coerce-flat-contract 'flat-contract predicate))
|
||||
|
|
|
@ -751,10 +751,6 @@
|
|||
[else (loop (cons (eg) so-far))])))
|
||||
(λ () '()))))
|
||||
|
||||
(define (listof-exercise el-ctc)
|
||||
(λ (f n-tests size env)
|
||||
#t))
|
||||
|
||||
(define (non-empty-listof-generate elem-ctc)
|
||||
(λ (fuel)
|
||||
(define eg (generate/choose elem-ctc fuel))
|
||||
|
@ -766,43 +762,54 @@
|
|||
[else (loop (cons (eg) so-far))])))
|
||||
#f)))
|
||||
|
||||
(define (*-listof predicate? name generate)
|
||||
(define (non-empty-listof-exercise elem-ctc)
|
||||
(λ (fuel)
|
||||
(define env (generate-env))
|
||||
(values
|
||||
(λ (lst)
|
||||
(env-stash env elem-ctc (oneof lst)))
|
||||
(list elem-ctc))))
|
||||
|
||||
(define (*-listof predicate? name generate exercise)
|
||||
(λ (input)
|
||||
(let* ([ctc (coerce-contract name input)]
|
||||
[ctc-name (build-compound-type-name name ctc)]
|
||||
[proj (contract-projection ctc)])
|
||||
(define ((listof-*-ho-check check-all) blame)
|
||||
(let ([p-app (proj (blame-add-listof-*-context blame))])
|
||||
(λ (val)
|
||||
(unless (predicate? val)
|
||||
((listof-*/fail blame val predicate?) #f))
|
||||
(check-all p-app val))))
|
||||
|
||||
(define (fo-check x)
|
||||
(and (predicate? x)
|
||||
(for/and ([v (in-list x)])
|
||||
(contract-first-order-passes? ctc v))))
|
||||
(cond
|
||||
[(flat-contract? ctc)
|
||||
(make-flat-contract
|
||||
#:name ctc-name
|
||||
#:first-order fo-check
|
||||
#:projection (listof-*-ho-check (λ (p v) (for-each p v) v))
|
||||
#:val-first-projection (listof-*-val-first-flat-proj predicate? ctc)
|
||||
#:generate (generate ctc))]
|
||||
[(chaperone-contract? ctc)
|
||||
(make-chaperone-contract
|
||||
#:name ctc-name
|
||||
#:first-order fo-check
|
||||
#:projection (listof-*-ho-check (λ (p v) (map p v)))
|
||||
#:val-first-projection (listof-*-val-first-ho-proj predicate? ctc)
|
||||
#:generate (generate ctc))]
|
||||
[else
|
||||
(make-contract
|
||||
#:name ctc-name
|
||||
#:first-order fo-check
|
||||
#:val-first-projection (listof-*-val-first-ho-proj predicate? ctc)
|
||||
#:projection (listof-*-ho-check (λ (p v) (map p v))))]))))
|
||||
(define ctc (coerce-contract name input))
|
||||
(define ctc-name (build-compound-type-name name ctc))
|
||||
(define proj (contract-projection ctc))
|
||||
(define ((listof-*-ho-check check-all) blame)
|
||||
(let ([p-app (proj (blame-add-listof-*-context blame))])
|
||||
(λ (val)
|
||||
(unless (predicate? val)
|
||||
((listof-*/fail blame val predicate?) #f))
|
||||
(check-all p-app val))))
|
||||
|
||||
(define (fo-check x)
|
||||
(and (predicate? x)
|
||||
(for/and ([v (in-list x)])
|
||||
(contract-first-order-passes? ctc v))))
|
||||
(cond
|
||||
[(flat-contract? ctc)
|
||||
(make-flat-contract
|
||||
#:name ctc-name
|
||||
#:first-order fo-check
|
||||
#:projection (listof-*-ho-check (λ (p v) (for-each p v) v))
|
||||
#:val-first-projection (listof-*-val-first-flat-proj predicate? ctc)
|
||||
#:generate (generate ctc)
|
||||
#:exercise (exercise ctc))]
|
||||
[(chaperone-contract? ctc)
|
||||
(make-chaperone-contract
|
||||
#:name ctc-name
|
||||
#:first-order fo-check
|
||||
#:projection (listof-*-ho-check (λ (p v) (map p v)))
|
||||
#:val-first-projection (listof-*-val-first-ho-proj predicate? ctc)
|
||||
#:generate (generate ctc)
|
||||
#:exercise (exercise ctc))]
|
||||
[else
|
||||
(make-contract
|
||||
#:name ctc-name
|
||||
#:first-order fo-check
|
||||
#:val-first-projection (listof-*-val-first-ho-proj predicate? ctc)
|
||||
#:projection (listof-*-ho-check (λ (p v) (map p v)))
|
||||
#:exercise (exercise ctc))])))
|
||||
|
||||
(define (listof-*-val-first-flat-proj predicate? ctc)
|
||||
(define vf-proj (get/build-val-first-projection ctc))
|
||||
|
@ -841,12 +848,14 @@
|
|||
(define (blame-add-listof-*-context blame) (blame-add-context blame "an element of"))
|
||||
(define (non-empty-list? x) (and (pair? x) (list? x)))
|
||||
|
||||
(define listof-func (*-listof list? 'listof listof-generate))
|
||||
(define (no-exercise ctc) (λ (size) (values void '())))
|
||||
(define listof-func (*-listof list? 'listof listof-generate no-exercise))
|
||||
(define/subexpression-pos-prop (listof x) (listof-func x))
|
||||
|
||||
(define non-empty-listof-func (*-listof non-empty-list?
|
||||
'non-empty-listof
|
||||
non-empty-listof-generate))
|
||||
non-empty-listof-generate
|
||||
non-empty-listof-exercise))
|
||||
(define/subexpression-pos-prop (non-empty-listof a) (non-empty-listof-func a))
|
||||
|
||||
(define (blame-add-car-context blame) (blame-add-context blame "the car of"))
|
||||
|
|
|
@ -104,11 +104,11 @@
|
|||
#f))
|
||||
|
||||
(define (contract-struct-exercise c)
|
||||
(let* ([prop (contract-struct-property c)]
|
||||
[exercise (contract-property-exercise prop)])
|
||||
(if (procedure? exercise)
|
||||
(exercise c)
|
||||
(make-generate-ctc-fail))))
|
||||
(define prop (contract-struct-property c))
|
||||
(define exercise (contract-property-exercise prop))
|
||||
(if (procedure? exercise)
|
||||
(exercise c)
|
||||
(λ (fuel) (values void '()))))
|
||||
|
||||
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
|
||||
;;
|
||||
|
@ -203,8 +203,8 @@
|
|||
#:projection [get-projection #f]
|
||||
#:val-first-projection [get-val-first-projection #f]
|
||||
#:stronger [stronger #f]
|
||||
#:generate [generate (make-generate-ctc-fail)]
|
||||
#:exercise [exercise (make-generate-ctc-fail)])
|
||||
#:generate [generate (λ (ctc) (λ (fuel) #f))]
|
||||
#:exercise [exercise (λ (ctc) (λ (fuel) (values void '())))])
|
||||
|
||||
;; this code is here to help me find the combinators that
|
||||
;; are still using only #:projection and not #:val-first-projection
|
||||
|
@ -312,8 +312,8 @@
|
|||
#:projection (lambda (c) (make-contract-projection c))
|
||||
#:val-first-projection (lambda (c) (make-contract-val-first-projection c))
|
||||
#:stronger (lambda (a b) ((make-contract-stronger a) a b))
|
||||
#:generate (lambda (c) ((make-contract-generate c)))
|
||||
#:exercise (lambda (c) ((make-contract-exercise c)))))
|
||||
#:generate (lambda (c) (make-contract-generate c))
|
||||
#:exercise (lambda (c) (make-contract-exercise c))))
|
||||
|
||||
(define-struct make-chaperone-contract [ name first-order projection val-first-projection
|
||||
stronger generate exercise ]
|
||||
|
@ -357,8 +357,8 @@
|
|||
#:projection [projection #f]
|
||||
#:val-first-projection [val-first-projection #f]
|
||||
#:stronger [stronger #f]
|
||||
#:generate [generate (make-generate-ctc-fail)]
|
||||
#:exercise [exercise (make-generate-ctc-fail)] )
|
||||
#:generate [generate (λ (ctc) (λ (fuel) #f))]
|
||||
#:exercise [exercise (λ (ctc) (λ (fuel) (values void '())))])
|
||||
|
||||
(let* ([name (or name default-name)]
|
||||
[first-order (or first-order any?)]
|
||||
|
@ -397,5 +397,4 @@
|
|||
(define make-chaperone-contract
|
||||
(build-contract make-make-chaperone-contract 'anonymous-chaperone-contract))
|
||||
|
||||
(define make-flat-contract
|
||||
(build-contract make-make-flat-contract 'anonymous-flat-contract))
|
||||
(define make-flat-contract (build-contract make-make-flat-contract 'anonymous-flat-contract))
|
||||
|
|
Loading…
Reference in New Issue
Block a user