suzanne.soy/racket
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

add stronger and random generation for integer-in

Browse Source
This commit is contained in:
Robby Findler 2014-12-25 22:07:05 -06:00
parent 3372ba3547
commit 94a450999a
3 changed files with 32 additions and 5 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
pkgs/racket-test/tests/racket/contract-rand-test.rkt
View File

@ -33,6 +33,8 @@
(check-not-exn (λ () (test-contract-generation (listof boolean?))))
(check-not-exn (λ () (test-contract-generation (listof number?))))
(check-not-exn (λ () (test-contract-generation (integer-in 0 100))))
(check-not-exn (λ () (test-contract-generation (integer-in 0 (expt 2 1000)))))
(check-not-exn (λ () (test-contract-generation (between/c 1 100))))
(check-not-exn (λ () (test-contract-generation (between/c 1.0 100.0))))
(check-not-exn (λ () (test-contract-generation (listof integer?))))

3
pkgs/racket-test/tests/racket/contract/stronger.rkt
View File

@ -10,6 +10,9 @@
(contract-eval '(define-contract-struct triple (a b c)))
(ctest #t contract-stronger? any/c any/c)
(ctest #t contract-stronger? (integer-in 0 4) (integer-in 0 4))
(ctest #t contract-stronger? (integer-in 1 3) (integer-in 0 4))
(ctest #f contract-stronger? (integer-in 0 4) (integer-in 1 3))
(ctest #t contract-stronger? (between/c 1 3) (between/c 0 4))
(ctest #f contract-stronger? (between/c 0 4) (between/c 1 3))
(ctest #t contract-stronger? (>=/c 3) (>=/c 2))

32
racket/collects/racket/contract/private/misc.rkt
View File

@ -515,13 +515,35 @@
(format "~a" (object-name pred2?))
1
arg1 arg2)))
(struct integer-in-ctc (start end)
#:property prop:flat-contract
(build-flat-contract-property
#:name (λ (ctc) `(integer-in ,(integer-in-ctc-start ctc)
,(integer-in-ctc-end ctc)))
#:first-order (λ (ctc)
(define start (integer-in-ctc-start ctc))
(define end (integer-in-ctc-end ctc))
(λ (x) (and (exact-integer? x)
(<= start x end))))
#:stronger (λ (this that)
(define this-start (integer-in-ctc-start this))
(define this-end (integer-in-ctc-end that))
(cond
[(integer-in-ctc? that)
(define that-start (integer-in-ctc-start that))
(define that-end (integer-in-ctc-end that))
(<= that-start this-start this-end that-end)]
[else #f]))
#:generate (λ (ctc)
(define start (integer-in-ctc-start ctc))
(define end (integer-in-ctc-end ctc))
(λ (fuel)
(λ ()
(+ start (random (min 4294967087 (+ (- end start) 1)))))))))
(define/final-prop (integer-in start end)
(check-two-args 'integer-in start end exact-integer? exact-integer?)
(flat-named-contract
`(integer-in ,start ,end)
(λ (x)
(and (exact-integer? x)
(<= start x end)))))
(integer-in-ctc start end))
(define/final-prop (real-in start end)
(check-two-args 'real-in start end real? real?)