clean up and export support for exercising values with contracts
This commit is contained in:
parent
9a6970043a
commit
0f16f31db9
|
@ -12,4 +12,5 @@
|
||||||
"contract/region.rkt"
|
"contract/region.rkt"
|
||||||
"contract/private/legacy.rkt"
|
"contract/private/legacy.rkt"
|
||||||
"contract/private/ds.rkt")
|
"contract/private/ds.rkt")
|
||||||
contract-random-generate)
|
contract-random-generate
|
||||||
|
contract-exercise)
|
||||||
|
|
|
@ -784,28 +784,6 @@
|
||||||
[else
|
[else
|
||||||
(λ (fuel) (values void '()))]))
|
(λ (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 (base->-name ctc)
|
||||||
(define rngs (base->-rngs ctc))
|
(define rngs (base->-rngs ctc))
|
||||||
(define rng-sexp
|
(define rng-sexp
|
||||||
|
|
|
@ -9,11 +9,23 @@
|
||||||
(provide generate-env
|
(provide generate-env
|
||||||
env-stash
|
env-stash
|
||||||
contract-random-generate
|
contract-random-generate
|
||||||
|
contract-exercise
|
||||||
generate/direct
|
generate/direct
|
||||||
generate/choose
|
generate/choose
|
||||||
make-generate-ctc-fail
|
make-generate-ctc-fail
|
||||||
generate-ctc-fail?
|
generate-ctc-fail?
|
||||||
with-definitely-available-contracts)
|
with-definitely-available-contracts
|
||||||
|
can-generate/env?
|
||||||
|
try/env)
|
||||||
|
|
||||||
|
(define (contract-exercise v [fuel 10])
|
||||||
|
(define ctc (value-contract v))
|
||||||
|
(when ctc
|
||||||
|
(define-values (go ctcs)
|
||||||
|
(parameterize ([generate-env (make-hash)])
|
||||||
|
((contract-struct-exercise ctc) fuel)))
|
||||||
|
(for ([x (in-range fuel)])
|
||||||
|
(go v))))
|
||||||
|
|
||||||
;; a stash of values and the contracts that they correspond to
|
;; a stash of values and the contracts that they correspond to
|
||||||
;; that generation has produced earlier in the process
|
;; that generation has produced earlier in the process
|
||||||
|
@ -54,15 +66,21 @@
|
||||||
; #f if no value could be generated
|
; #f if no value could be generated
|
||||||
(define (generate/choose ctc fuel)
|
(define (generate/choose ctc fuel)
|
||||||
(define direct (generate/direct ctc fuel))
|
(define direct (generate/direct ctc fuel))
|
||||||
(define env (generate/env ctc fuel))
|
(define env-can? (can-generate/env? ctc))
|
||||||
|
(define env (generate-env))
|
||||||
(cond
|
(cond
|
||||||
[(and direct env)
|
[direct
|
||||||
(λ ()
|
(λ ()
|
||||||
(if (zero? (rand 2))
|
(define use-direct? (zero? (rand 2)))
|
||||||
|
(if use-direct?
|
||||||
(direct)
|
(direct)
|
||||||
(env)))]
|
(try/env ctc env direct)))]
|
||||||
[else
|
[env-can?
|
||||||
(or direct env)]))
|
(λ ()
|
||||||
|
(try/env
|
||||||
|
ctc env
|
||||||
|
(λ () (error 'generate/choose "internal generation failure"))))]
|
||||||
|
[else #f]))
|
||||||
|
|
||||||
; generate/direct :: contract nonnegative-int -> (or/c #f (-> val))
|
; generate/direct :: contract nonnegative-int -> (or/c #f (-> val))
|
||||||
;; generate directly via the contract's built-in generator, if possible
|
;; generate directly via the contract's built-in generator, if possible
|
||||||
|
@ -84,3 +102,17 @@
|
||||||
(when (null? available)
|
(when (null? available)
|
||||||
(error 'generate.rkt "internal error: no values satisfying ~s available" ctc))
|
(error 'generate.rkt "internal error: no values satisfying ~s available" ctc))
|
||||||
(oneof available)))))
|
(oneof available)))))
|
||||||
|
|
||||||
|
(define (try/env ctc env fail)
|
||||||
|
(define available
|
||||||
|
(for/list ([(avail-ctc vs) (in-hash env)]
|
||||||
|
#:when (contract-stronger? avail-ctc ctc)
|
||||||
|
[v (in-list vs)])
|
||||||
|
v))
|
||||||
|
(cond
|
||||||
|
[(null? available) (fail)]
|
||||||
|
[else (oneof available)]))
|
||||||
|
|
||||||
|
(define (can-generate/env? ctc)
|
||||||
|
(for/or ([avail-ctc (in-list (definitely-available-contracts))])
|
||||||
|
(contract-stronger? avail-ctc ctc)))
|
||||||
|
|
|
@ -132,18 +132,33 @@
|
||||||
(loop (cdr ho-contracts))]))))
|
(loop (cdr ho-contracts))]))))
|
||||||
'())))
|
'())))
|
||||||
|
|
||||||
(define (or/c-generate ctcs)
|
(define ((or/c-generate ctcs) fuel)
|
||||||
(λ (fuel)
|
(define directs
|
||||||
(define choices
|
(filter
|
||||||
(filter
|
values
|
||||||
values
|
(for/list ([ctc (in-list ctcs)])
|
||||||
(for/list ([ctc (in-list ctcs)])
|
(generate/direct ctc fuel))))
|
||||||
(generate/choose ctc fuel))))
|
(define can-generate?
|
||||||
(cond
|
(or (pair? directs)
|
||||||
[(null? choices) #f]
|
(for/or ([ctc (in-list ctcs)])
|
||||||
[else
|
(can-generate/env? ctc))))
|
||||||
(lambda ()
|
(cond
|
||||||
((oneof choices)))])))
|
[can-generate?
|
||||||
|
(define options (append directs ctcs))
|
||||||
|
(define env (generate-env))
|
||||||
|
(λ ()
|
||||||
|
(let loop ([options (permute options)])
|
||||||
|
(cond
|
||||||
|
[(null? options) (error 'or/c-generate "shouldn't fail!")]
|
||||||
|
[else
|
||||||
|
(define option (car options))
|
||||||
|
(cond
|
||||||
|
[(contract? option)
|
||||||
|
(try/env
|
||||||
|
option env
|
||||||
|
(λ ()
|
||||||
|
(loop (cdr options))))]
|
||||||
|
[else (option)])])))]))
|
||||||
|
|
||||||
(define-struct single-or/c (name pred flat-ctcs ho-ctc)
|
(define-struct single-or/c (name pred flat-ctcs ho-ctc)
|
||||||
#:property prop:orc-contract
|
#:property prop:orc-contract
|
||||||
|
|
Loading…
Reference in New Issue
Block a user