Add script to find good p-values, adjust models.
The definition of good at this point is that the average is close to the maximum counterexample size.
This commit is contained in:
parent
3d2a9794b4
commit
34c3eed615
|
@ -942,8 +942,8 @@
|
||||||
(judgment-holds (tc · · ,e t)))
|
(judgment-holds (tc · · ,e t)))
|
||||||
|
|
||||||
|
|
||||||
(define (generate-enum-term)
|
(define (generate-enum-term [p-value 0.125])
|
||||||
(generate-term abort-lang e #:i-th (pick-an-index 0.125)))
|
(generate-term abort-lang e #:i-th (pick-an-index p-value)))
|
||||||
|
|
||||||
(define (ordered-enum-generator)
|
(define (ordered-enum-generator)
|
||||||
(define index -1)
|
(define index -1)
|
||||||
|
|
|
@ -940,8 +940,8 @@
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
(define (generate-enum-term)
|
(define (generate-enum-term [p-value 0.125])
|
||||||
(generate-term abort-lang e #:i-th (pick-an-index 0.125)))
|
(generate-term abort-lang e #:i-th (pick-an-index p-value)))
|
||||||
|
|
||||||
(define (ordered-enum-generator)
|
(define (ordered-enum-generator)
|
||||||
(define index -1)
|
(define index -1)
|
||||||
|
|
|
@ -940,8 +940,8 @@
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
(define (generate-enum-term)
|
(define (generate-enum-term [p-value 0.125])
|
||||||
(generate-term abort-lang e #:i-th (pick-an-index 0.125)))
|
(generate-term abort-lang e #:i-th (pick-an-index p-value)))
|
||||||
|
|
||||||
(define (ordered-enum-generator)
|
(define (ordered-enum-generator)
|
||||||
(define index -1)
|
(define index -1)
|
||||||
|
|
|
@ -937,8 +937,8 @@
|
||||||
(define (type-check e)
|
(define (type-check e)
|
||||||
(judgment-holds (tc · · ,e t)))
|
(judgment-holds (tc · · ,e t)))
|
||||||
|
|
||||||
(define (generate-enum-term)
|
(define (generate-enum-term [p-value 0.125])
|
||||||
(generate-term abort-lang e #:i-th (pick-an-index 0.125)))
|
(generate-term abort-lang e #:i-th (pick-an-index p-value)))
|
||||||
|
|
||||||
(define (ordered-enum-generator)
|
(define (ordered-enum-generator)
|
||||||
(define index -1)
|
(define index -1)
|
||||||
|
|
|
@ -518,8 +518,8 @@ Generators
|
||||||
M]
|
M]
|
||||||
[#f #f]))))
|
[#f #f]))))
|
||||||
|
|
||||||
(define (generate-enum-term)
|
(define (generate-enum-term [p-value 0.035])
|
||||||
(generate-term stlc M #:i-th (pick-an-index 0.035)))
|
(generate-term stlc M #:i-th (pick-an-index p-value)))
|
||||||
|
|
||||||
(define (ordered-enum-generator)
|
(define (ordered-enum-generator)
|
||||||
(let ([index 0])
|
(let ([index 0])
|
||||||
|
|
|
@ -513,8 +513,8 @@ Generators
|
||||||
M]
|
M]
|
||||||
[#f #f]))))
|
[#f #f]))))
|
||||||
|
|
||||||
(define (generate-enum-term)
|
(define (generate-enum-term [p-value 0.035])
|
||||||
(generate-term stlc M #:i-th (pick-an-index 0.035)))
|
(generate-term stlc M #:i-th (pick-an-index p-value)))
|
||||||
|
|
||||||
(define (ordered-enum-generator)
|
(define (ordered-enum-generator)
|
||||||
(let ([index 0])
|
(let ([index 0])
|
||||||
|
|
|
@ -518,8 +518,8 @@ Generators
|
||||||
M]
|
M]
|
||||||
[#f #f]))))
|
[#f #f]))))
|
||||||
|
|
||||||
(define (generate-enum-term)
|
(define (generate-enum-term [p-value 0.035])
|
||||||
(generate-term stlc M #:i-th (pick-an-index 0.035)))
|
(generate-term stlc M #:i-th (pick-an-index p-value)))
|
||||||
|
|
||||||
(define (ordered-enum-generator)
|
(define (ordered-enum-generator)
|
||||||
(let ([index 0])
|
(let ([index 0])
|
||||||
|
|
|
@ -520,8 +520,8 @@ Generators
|
||||||
M]
|
M]
|
||||||
[#f #f]))))
|
[#f #f]))))
|
||||||
|
|
||||||
(define (generate-enum-term)
|
(define (generate-enum-term [p-value 0.035])
|
||||||
(generate-term stlc M #:i-th (pick-an-index 0.035)))
|
(generate-term stlc M #:i-th (pick-an-index p-value)))
|
||||||
|
|
||||||
(define (ordered-enum-generator)
|
(define (ordered-enum-generator)
|
||||||
(let ([index 0])
|
(let ([index 0])
|
||||||
|
|
|
@ -520,8 +520,8 @@ Generators
|
||||||
M]
|
M]
|
||||||
[#f #f]))))
|
[#f #f]))))
|
||||||
|
|
||||||
(define (generate-enum-term)
|
(define (generate-enum-term [p-value 0.035])
|
||||||
(generate-term stlc M #:i-th (pick-an-index 0.035)))
|
(generate-term stlc M #:i-th (pick-an-index p-value)))
|
||||||
|
|
||||||
(define (ordered-enum-generator)
|
(define (ordered-enum-generator)
|
||||||
(let ([index 0])
|
(let ([index 0])
|
||||||
|
|
|
@ -518,8 +518,8 @@ Generators
|
||||||
M]
|
M]
|
||||||
[#f #f]))))
|
[#f #f]))))
|
||||||
|
|
||||||
(define (generate-enum-term)
|
(define (generate-enum-term [p-value 0.035])
|
||||||
(generate-term stlc M #:i-th (pick-an-index 0.035)))
|
(generate-term stlc M #:i-th (pick-an-index p-value)))
|
||||||
|
|
||||||
(define (ordered-enum-generator)
|
(define (ordered-enum-generator)
|
||||||
(let ([index 0])
|
(let ([index 0])
|
||||||
|
|
|
@ -519,8 +519,8 @@ Generators
|
||||||
M]
|
M]
|
||||||
[#f #f]))))
|
[#f #f]))))
|
||||||
|
|
||||||
(define (generate-enum-term)
|
(define (generate-enum-term [p-value 0.035])
|
||||||
(generate-term stlc M #:i-th (pick-an-index 0.035)))
|
(generate-term stlc M #:i-th (pick-an-index p-value)))
|
||||||
|
|
||||||
(define (ordered-enum-generator)
|
(define (ordered-enum-generator)
|
||||||
(let ([index 0])
|
(let ([index 0])
|
||||||
|
|
|
@ -518,8 +518,8 @@ Generators
|
||||||
M]
|
M]
|
||||||
[#f #f]))))
|
[#f #f]))))
|
||||||
|
|
||||||
(define (generate-enum-term)
|
(define (generate-enum-term [p-value 0.035])
|
||||||
(generate-term stlc M #:i-th (pick-an-index 0.035)))
|
(generate-term stlc M #:i-th (pick-an-index p-value)))
|
||||||
|
|
||||||
(define (ordered-enum-generator)
|
(define (ordered-enum-generator)
|
||||||
(let ([index 0])
|
(let ([index 0])
|
||||||
|
|
|
@ -433,8 +433,8 @@
|
||||||
p]
|
p]
|
||||||
[#f #f]))
|
[#f #f]))
|
||||||
|
|
||||||
(define (generate-enum-term)
|
(define (generate-enum-term [p-value 0.5])
|
||||||
(generate-term list-machine-typing (l0 : ι p) #:i-th (pick-an-index 0.5)))
|
(generate-term list-machine-typing (l0 : ι p) #:i-th (pick-an-index p-value)))
|
||||||
|
|
||||||
(define (ordered-enum-generator)
|
(define (ordered-enum-generator)
|
||||||
(let ([index 0])
|
(let ([index 0])
|
||||||
|
|
|
@ -433,8 +433,8 @@
|
||||||
p]
|
p]
|
||||||
[#f #f]))
|
[#f #f]))
|
||||||
|
|
||||||
(define (generate-enum-term)
|
(define (generate-enum-term [p-value 0.5])
|
||||||
(generate-term list-machine-typing (l0 : ι p) #:i-th (pick-an-index 0.5)))
|
(generate-term list-machine-typing (l0 : ι p) #:i-th (pick-an-index p-value)))
|
||||||
|
|
||||||
(define (ordered-enum-generator)
|
(define (ordered-enum-generator)
|
||||||
(let ([index 0])
|
(let ([index 0])
|
||||||
|
|
|
@ -429,8 +429,8 @@
|
||||||
p]
|
p]
|
||||||
[#f #f]))
|
[#f #f]))
|
||||||
|
|
||||||
(define (generate-enum-term)
|
(define (generate-enum-term [p-value 0.5])
|
||||||
(generate-term list-machine-typing (l0 : ι p) #:i-th (pick-an-index 0.5)))
|
(generate-term list-machine-typing (l0 : ι p) #:i-th (pick-an-index p-value)))
|
||||||
|
|
||||||
(define (ordered-enum-generator)
|
(define (ordered-enum-generator)
|
||||||
(let ([index 0])
|
(let ([index 0])
|
||||||
|
|
|
@ -429,8 +429,8 @@
|
||||||
p]
|
p]
|
||||||
[#f #f]))
|
[#f #f]))
|
||||||
|
|
||||||
(define (generate-enum-term)
|
(define (generate-enum-term [p-value 0.5])
|
||||||
(generate-term list-machine-typing (l0 : ι p) #:i-th (pick-an-index 0.5)))
|
(generate-term list-machine-typing (l0 : ι p) #:i-th (pick-an-index p-value)))
|
||||||
|
|
||||||
(define (ordered-enum-generator)
|
(define (ordered-enum-generator)
|
||||||
(let ([index 0])
|
(let ([index 0])
|
||||||
|
|
|
@ -0,0 +1,125 @@
|
||||||
|
#lang racket
|
||||||
|
|
||||||
|
(require math/statistics)
|
||||||
|
|
||||||
|
#|
|
||||||
|
|
||||||
|
From the command line, for example:
|
||||||
|
racket p-calc.rkt stlc
|
||||||
|
|
||||||
|
Finds a p-value such that the average size of generated terms
|
||||||
|
is within 0.5 of the maximum counterexample size for that model.
|
||||||
|
This target size will likely need to change.
|
||||||
|
(Also makes sure that the standard error in the mean is less than 0.5.)
|
||||||
|
|
||||||
|
Doesn't work well with rbtrees, which has an extremely large standard deviation.
|
||||||
|
|
||||||
|
|#
|
||||||
|
|
||||||
|
(module+
|
||||||
|
main
|
||||||
|
(command-line
|
||||||
|
#:args (dir)
|
||||||
|
(printf "p-value: ~s\n"
|
||||||
|
(exact->inexact
|
||||||
|
(model-p-value
|
||||||
|
(string->symbol
|
||||||
|
(string-append
|
||||||
|
"redex/examples/benchmark/"
|
||||||
|
dir)))))))
|
||||||
|
|
||||||
|
(define (model-p-value mod-path)
|
||||||
|
(define target-size (max-cexp-size mod-path))
|
||||||
|
(define base (test-mod-path->base mod-path))
|
||||||
|
(define enum-gen (dynamic-require base 'generate-enum-term))
|
||||||
|
(find-p-value enum-gen target-size))
|
||||||
|
|
||||||
|
(define (find-p-value enum-gen target-size)
|
||||||
|
(fpv-search enum-gen target-size 0 1 100))
|
||||||
|
|
||||||
|
(define (fpv-search gen size l r num-samples)
|
||||||
|
(define mid (/ (+ l r) 2))
|
||||||
|
(printf "Target: ~s, current interval: (~s ~s)\n" size l r)
|
||||||
|
(define-values (m e) (sample-sizes gen mid num-samples))
|
||||||
|
(printf "At ~s, mean: ~s, stderr: ~s, with ~s samples\n" mid m e num-samples)
|
||||||
|
(cond
|
||||||
|
[(e . > . 0.5)
|
||||||
|
(fpv-search gen size l r (* num-samples 2))]
|
||||||
|
[((abs (- size m)) . < . 0.5)
|
||||||
|
mid]
|
||||||
|
[(m . < . size)
|
||||||
|
(fpv-search gen size l mid num-samples)]
|
||||||
|
[(m . > . size)
|
||||||
|
(fpv-search gen size mid r num-samples)]))
|
||||||
|
|
||||||
|
(define (sample-sizes enum-gen p-value num-samples)
|
||||||
|
(define sizes
|
||||||
|
(for/list ([_ (in-range num-samples)])
|
||||||
|
(count-size
|
||||||
|
(enum-gen p-value))))
|
||||||
|
(values (mean sizes)
|
||||||
|
(/ (stddev sizes)
|
||||||
|
(sqrt num-samples))))
|
||||||
|
|
||||||
|
(module+
|
||||||
|
test
|
||||||
|
(require rackunit)
|
||||||
|
(define stlc-path 'redex/examples/benchmark/stlc)
|
||||||
|
(define stlc-base 'redex/examples/benchmark/stlc/stlc-base)
|
||||||
|
(define stlc-gen (dynamic-require stlc-base 'generate-enum-term))
|
||||||
|
(define-values (m e) (sample-sizes stlc-gen 0.03125 100))
|
||||||
|
(check-not-false
|
||||||
|
((abs (- m 15)) . < . (* 2 e))))
|
||||||
|
|
||||||
|
(define max-bug-num 20)
|
||||||
|
|
||||||
|
(define (test-paths t-m-p)
|
||||||
|
(for/list ([n (in-range 1 max-bug-num)])
|
||||||
|
(string->symbol
|
||||||
|
(string-append
|
||||||
|
(test-mod-path->stem t-m-p)
|
||||||
|
(number->string n)))))
|
||||||
|
|
||||||
|
(define (test-mod-path->base t-m-p)
|
||||||
|
(string->symbol
|
||||||
|
(string-append
|
||||||
|
(test-mod-path->stem t-m-p)
|
||||||
|
"base")))
|
||||||
|
|
||||||
|
(define (test-mod-path->stem t-m-p)
|
||||||
|
(define tms (symbol->string t-m-p))
|
||||||
|
(define name (second (regexp-match #rx"^.*/(.*)$" tms)))
|
||||||
|
(string-append tms "/" name "-"))
|
||||||
|
|
||||||
|
(define (cexps t-m-p)
|
||||||
|
(filter
|
||||||
|
values
|
||||||
|
(map
|
||||||
|
(λ (p)
|
||||||
|
(with-handlers
|
||||||
|
([exn:fail:filesystem?
|
||||||
|
(λ (e)
|
||||||
|
(if (regexp-match? #rx"No such file"
|
||||||
|
(exn-message e))
|
||||||
|
#f
|
||||||
|
(raise e)))])
|
||||||
|
(dynamic-require p 'small-counter-example)))
|
||||||
|
(test-paths t-m-p))))
|
||||||
|
|
||||||
|
(define (count-size l)
|
||||||
|
(cond
|
||||||
|
[(list? l) (apply + 1 (map count-size l))]
|
||||||
|
[else 1]))
|
||||||
|
|
||||||
|
(define (cexp-sizes t-m-p)
|
||||||
|
(map count-size (cexps t-m-p)))
|
||||||
|
|
||||||
|
(define (max-cexp-size t-m-p)
|
||||||
|
(apply max (cexp-sizes t-m-p)))
|
||||||
|
|
||||||
|
(module+
|
||||||
|
test
|
||||||
|
(check-equal? (test-mod-path->stem stlc-path)
|
||||||
|
"redex/examples/benchmark/stlc/stlc-")
|
||||||
|
(define stlc-size (max-cexp-size stlc-path))
|
||||||
|
(check-equal? stlc-size 15))
|
|
@ -282,8 +282,8 @@
|
||||||
(let ([red-type (type-check red-t)])
|
(let ([red-type (type-check red-t)])
|
||||||
(equal? t-type red-type))))))))))
|
(equal? t-type red-type))))))))))
|
||||||
|
|
||||||
(define (generate-enum-term)
|
(define (generate-enum-term [p-value 0.065])
|
||||||
(generate-term poly-stlc M #:i-th (pick-an-index 0.065)))
|
(generate-term poly-stlc M #:i-th (pick-an-index p-value)))
|
||||||
|
|
||||||
(define (ordered-enum-generator)
|
(define (ordered-enum-generator)
|
||||||
(let ([index 0])
|
(let ([index 0])
|
||||||
|
|
|
@ -280,8 +280,8 @@
|
||||||
(let ([red-type (type-check red-t)])
|
(let ([red-type (type-check red-t)])
|
||||||
(equal? t-type red-type))))))))))
|
(equal? t-type red-type))))))))))
|
||||||
|
|
||||||
(define (generate-enum-term)
|
(define (generate-enum-term [p-value 0.065])
|
||||||
(generate-term poly-stlc M #:i-th (pick-an-index 0.065)))
|
(generate-term poly-stlc M #:i-th (pick-an-index p-value)))
|
||||||
|
|
||||||
(define (ordered-enum-generator)
|
(define (ordered-enum-generator)
|
||||||
(let ([index 0])
|
(let ([index 0])
|
||||||
|
|
|
@ -282,8 +282,8 @@
|
||||||
(let ([red-type (type-check red-t)])
|
(let ([red-type (type-check red-t)])
|
||||||
(equal? t-type red-type))))))))))
|
(equal? t-type red-type))))))))))
|
||||||
|
|
||||||
(define (generate-enum-term)
|
(define (generate-enum-term [p-value 0.065])
|
||||||
(generate-term poly-stlc M #:i-th (pick-an-index 0.065)))
|
(generate-term poly-stlc M #:i-th (pick-an-index p-value)))
|
||||||
|
|
||||||
(define (ordered-enum-generator)
|
(define (ordered-enum-generator)
|
||||||
(let ([index 0])
|
(let ([index 0])
|
||||||
|
|
|
@ -282,8 +282,8 @@
|
||||||
(let ([red-type (type-check red-t)])
|
(let ([red-type (type-check red-t)])
|
||||||
(equal? t-type red-type))))))))))
|
(equal? t-type red-type))))))))))
|
||||||
|
|
||||||
(define (generate-enum-term)
|
(define (generate-enum-term [p-value 0.065])
|
||||||
(generate-term poly-stlc M #:i-th (pick-an-index 0.065)))
|
(generate-term poly-stlc M #:i-th (pick-an-index p-value)))
|
||||||
|
|
||||||
(define (ordered-enum-generator)
|
(define (ordered-enum-generator)
|
||||||
(let ([index 0])
|
(let ([index 0])
|
||||||
|
|
|
@ -282,8 +282,8 @@
|
||||||
(let ([red-type (type-check red-t)])
|
(let ([red-type (type-check red-t)])
|
||||||
(equal? t-type red-type))))))))))
|
(equal? t-type red-type))))))))))
|
||||||
|
|
||||||
(define (generate-enum-term)
|
(define (generate-enum-term [p-value 0.065])
|
||||||
(generate-term poly-stlc M #:i-th (pick-an-index 0.065)))
|
(generate-term poly-stlc M #:i-th (pick-an-index p-value)))
|
||||||
|
|
||||||
(define (ordered-enum-generator)
|
(define (ordered-enum-generator)
|
||||||
(let ([index 0])
|
(let ([index 0])
|
||||||
|
|
|
@ -282,8 +282,8 @@
|
||||||
(let ([red-type (type-check red-t)])
|
(let ([red-type (type-check red-t)])
|
||||||
(equal? t-type red-type))))))))))
|
(equal? t-type red-type))))))))))
|
||||||
|
|
||||||
(define (generate-enum-term)
|
(define (generate-enum-term [p-value 0.065])
|
||||||
(generate-term poly-stlc M #:i-th (pick-an-index 0.065)))
|
(generate-term poly-stlc M #:i-th (pick-an-index p-value)))
|
||||||
|
|
||||||
(define (ordered-enum-generator)
|
(define (ordered-enum-generator)
|
||||||
(let ([index 0])
|
(let ([index 0])
|
||||||
|
|
|
@ -281,8 +281,8 @@
|
||||||
(let ([red-type (type-check red-t)])
|
(let ([red-type (type-check red-t)])
|
||||||
(equal? t-type red-type))))))))))
|
(equal? t-type red-type))))))))))
|
||||||
|
|
||||||
(define (generate-enum-term)
|
(define (generate-enum-term [p-value 0.065])
|
||||||
(generate-term poly-stlc M #:i-th (pick-an-index 0.065)))
|
(generate-term poly-stlc M #:i-th (pick-an-index p-value)))
|
||||||
|
|
||||||
(define (ordered-enum-generator)
|
(define (ordered-enum-generator)
|
||||||
(let ([index 0])
|
(let ([index 0])
|
||||||
|
|
|
@ -282,8 +282,8 @@
|
||||||
(let ([red-type (type-check red-t)])
|
(let ([red-type (type-check red-t)])
|
||||||
(equal? t-type red-type))))))))))
|
(equal? t-type red-type))))))))))
|
||||||
|
|
||||||
(define (generate-enum-term)
|
(define (generate-enum-term [p-value 0.065])
|
||||||
(generate-term poly-stlc M #:i-th (pick-an-index 0.065)))
|
(generate-term poly-stlc M #:i-th (pick-an-index p-value)))
|
||||||
|
|
||||||
(define (ordered-enum-generator)
|
(define (ordered-enum-generator)
|
||||||
(let ([index 0])
|
(let ([index 0])
|
||||||
|
|
|
@ -282,8 +282,8 @@
|
||||||
(let ([red-type (type-check red-t)])
|
(let ([red-type (type-check red-t)])
|
||||||
(equal? t-type red-type))))))))))
|
(equal? t-type red-type))))))))))
|
||||||
|
|
||||||
(define (generate-enum-term)
|
(define (generate-enum-term [p-value 0.065])
|
||||||
(generate-term poly-stlc M #:i-th (pick-an-index 0.065)))
|
(generate-term poly-stlc M #:i-th (pick-an-index p-value)))
|
||||||
|
|
||||||
(define (ordered-enum-generator)
|
(define (ordered-enum-generator)
|
||||||
(let ([index 0])
|
(let ([index 0])
|
||||||
|
|
|
@ -282,8 +282,8 @@
|
||||||
(let ([red-type (type-check red-t)])
|
(let ([red-type (type-check red-t)])
|
||||||
(equal? t-type red-type))))))))))
|
(equal? t-type red-type))))))))))
|
||||||
|
|
||||||
(define (generate-enum-term)
|
(define (generate-enum-term [p-value 0.065])
|
||||||
(generate-term poly-stlc M #:i-th (pick-an-index 0.065)))
|
(generate-term poly-stlc M #:i-th (pick-an-index p-value)))
|
||||||
|
|
||||||
(define (ordered-enum-generator)
|
(define (ordered-enum-generator)
|
||||||
(let ([index 0])
|
(let ([index 0])
|
||||||
|
|
|
@ -289,8 +289,8 @@
|
||||||
(or (not t)
|
(or (not t)
|
||||||
(implies (type-check t) (ins-preserves-rb-tree t))))
|
(implies (type-check t) (ins-preserves-rb-tree t))))
|
||||||
|
|
||||||
(define (generate-enum-term)
|
(define (generate-enum-term [p-value 0.25])
|
||||||
(generate-term rbtrees t #:i-th (pick-an-index 0.25)))
|
(generate-term rbtrees t #:i-th (pick-an-index p-value)))
|
||||||
|
|
||||||
(define (ordered-enum-generator)
|
(define (ordered-enum-generator)
|
||||||
(let ([index 0])
|
(let ([index 0])
|
||||||
|
|
|
@ -287,8 +287,8 @@
|
||||||
(or (not t)
|
(or (not t)
|
||||||
(implies (type-check t) (ins-preserves-rb-tree t))))
|
(implies (type-check t) (ins-preserves-rb-tree t))))
|
||||||
|
|
||||||
(define (generate-enum-term)
|
(define (generate-enum-term [p-value 0.25])
|
||||||
(generate-term rbtrees t #:i-th (pick-an-index 0.25)))
|
(generate-term rbtrees t #:i-th (pick-an-index p-value)))
|
||||||
|
|
||||||
(define (ordered-enum-generator)
|
(define (ordered-enum-generator)
|
||||||
(let ([index 0])
|
(let ([index 0])
|
||||||
|
|
|
@ -289,8 +289,8 @@
|
||||||
(or (not t)
|
(or (not t)
|
||||||
(implies (type-check t) (ins-preserves-rb-tree t))))
|
(implies (type-check t) (ins-preserves-rb-tree t))))
|
||||||
|
|
||||||
(define (generate-enum-term)
|
(define (generate-enum-term [p-value 0.25])
|
||||||
(generate-term rbtrees t #:i-th (pick-an-index 0.25)))
|
(generate-term rbtrees t #:i-th (pick-an-index p-value)))
|
||||||
|
|
||||||
(define (ordered-enum-generator)
|
(define (ordered-enum-generator)
|
||||||
(let ([index 0])
|
(let ([index 0])
|
||||||
|
|
|
@ -289,8 +289,8 @@
|
||||||
(or (not t)
|
(or (not t)
|
||||||
(implies (type-check t) (ins-preserves-rb-tree t))))
|
(implies (type-check t) (ins-preserves-rb-tree t))))
|
||||||
|
|
||||||
(define (generate-enum-term)
|
(define (generate-enum-term [p-value 0.25])
|
||||||
(generate-term rbtrees t #:i-th (pick-an-index 0.25)))
|
(generate-term rbtrees t #:i-th (pick-an-index p-value)))
|
||||||
|
|
||||||
(define (ordered-enum-generator)
|
(define (ordered-enum-generator)
|
||||||
(let ([index 0])
|
(let ([index 0])
|
||||||
|
|
|
@ -473,8 +473,8 @@
|
||||||
(define (typed-generator)
|
(define (typed-generator)
|
||||||
(error "not currently implemented for rvm in the benchmark"))
|
(error "not currently implemented for rvm in the benchmark"))
|
||||||
|
|
||||||
(define (generate-enum-term)
|
(define (generate-enum-term [p-value 0.03])
|
||||||
(fix (generate-term bytecode e #:i-th (pick-an-index 0.03))))
|
(fix (generate-term bytecode e #:i-th (pick-an-index p-value))))
|
||||||
|
|
||||||
(define (ordered-enum-generator)
|
(define (ordered-enum-generator)
|
||||||
(let ([index 0])
|
(let ([index 0])
|
||||||
|
|
|
@ -470,8 +470,8 @@
|
||||||
(define (typed-generator)
|
(define (typed-generator)
|
||||||
(error "not currently implemented for rvm in the benchmark"))
|
(error "not currently implemented for rvm in the benchmark"))
|
||||||
|
|
||||||
(define (generate-enum-term)
|
(define (generate-enum-term [p-value 0.03])
|
||||||
(fix (generate-term bytecode e #:i-th (pick-an-index 0.03))))
|
(fix (generate-term bytecode e #:i-th (pick-an-index p-value))))
|
||||||
|
|
||||||
(define (ordered-enum-generator)
|
(define (ordered-enum-generator)
|
||||||
(let ([index 0])
|
(let ([index 0])
|
||||||
|
|
|
@ -469,8 +469,8 @@
|
||||||
(define (typed-generator)
|
(define (typed-generator)
|
||||||
(error "not currently implemented for rvm in the benchmark"))
|
(error "not currently implemented for rvm in the benchmark"))
|
||||||
|
|
||||||
(define (generate-enum-term)
|
(define (generate-enum-term [p-value 0.03])
|
||||||
(fix (generate-term bytecode e #:i-th (pick-an-index 0.03))))
|
(fix (generate-term bytecode e #:i-th (pick-an-index p-value))))
|
||||||
|
|
||||||
(define (ordered-enum-generator)
|
(define (ordered-enum-generator)
|
||||||
(let ([index 0])
|
(let ([index 0])
|
||||||
|
|
|
@ -468,8 +468,8 @@
|
||||||
(define (typed-generator)
|
(define (typed-generator)
|
||||||
(error "not currently implemented for rvm in the benchmark"))
|
(error "not currently implemented for rvm in the benchmark"))
|
||||||
|
|
||||||
(define (generate-enum-term)
|
(define (generate-enum-term [p-value 0.03])
|
||||||
(fix (generate-term bytecode e #:i-th (pick-an-index 0.03))))
|
(fix (generate-term bytecode e #:i-th (pick-an-index p-value))))
|
||||||
|
|
||||||
(define (ordered-enum-generator)
|
(define (ordered-enum-generator)
|
||||||
(let ([index 0])
|
(let ([index 0])
|
||||||
|
|
|
@ -469,8 +469,8 @@
|
||||||
(define (typed-generator)
|
(define (typed-generator)
|
||||||
(error "not currently implemented for rvm in the benchmark"))
|
(error "not currently implemented for rvm in the benchmark"))
|
||||||
|
|
||||||
(define (generate-enum-term)
|
(define (generate-enum-term [p-value 0.03])
|
||||||
(fix (generate-term bytecode e #:i-th (pick-an-index 0.03))))
|
(fix (generate-term bytecode e #:i-th (pick-an-index p-value))))
|
||||||
|
|
||||||
(define (ordered-enum-generator)
|
(define (ordered-enum-generator)
|
||||||
(let ([index 0])
|
(let ([index 0])
|
||||||
|
|
|
@ -469,8 +469,8 @@
|
||||||
(define (typed-generator)
|
(define (typed-generator)
|
||||||
(error "not currently implemented for rvm in the benchmark"))
|
(error "not currently implemented for rvm in the benchmark"))
|
||||||
|
|
||||||
(define (generate-enum-term)
|
(define (generate-enum-term [p-value 0.03])
|
||||||
(fix (generate-term bytecode e #:i-th (pick-an-index 0.03))))
|
(fix (generate-term bytecode e #:i-th (pick-an-index p-value))))
|
||||||
|
|
||||||
(define (ordered-enum-generator)
|
(define (ordered-enum-generator)
|
||||||
(let ([index 0])
|
(let ([index 0])
|
||||||
|
|
|
@ -469,8 +469,8 @@
|
||||||
(define (typed-generator)
|
(define (typed-generator)
|
||||||
(error "not currently implemented for rvm in the benchmark"))
|
(error "not currently implemented for rvm in the benchmark"))
|
||||||
|
|
||||||
(define (generate-enum-term)
|
(define (generate-enum-term [p-value 0.03])
|
||||||
(fix (generate-term bytecode e #:i-th (pick-an-index 0.03))))
|
(fix (generate-term bytecode e #:i-th (pick-an-index p-value))))
|
||||||
|
|
||||||
(define (ordered-enum-generator)
|
(define (ordered-enum-generator)
|
||||||
(let ([index 0])
|
(let ([index 0])
|
||||||
|
|
|
@ -468,8 +468,8 @@
|
||||||
(define (typed-generator)
|
(define (typed-generator)
|
||||||
(error "not currently implemented for rvm in the benchmark"))
|
(error "not currently implemented for rvm in the benchmark"))
|
||||||
|
|
||||||
(define (generate-enum-term)
|
(define (generate-enum-term [p-value 0.03])
|
||||||
(fix (generate-term bytecode e #:i-th (pick-an-index 0.03))))
|
(fix (generate-term bytecode e #:i-th (pick-an-index p-value))))
|
||||||
|
|
||||||
(define (ordered-enum-generator)
|
(define (ordered-enum-generator)
|
||||||
(let ([index 0])
|
(let ([index 0])
|
||||||
|
|
|
@ -300,8 +300,8 @@
|
||||||
(and (equal? (type-check a1) M-type)
|
(and (equal? (type-check a1) M-type)
|
||||||
(equal? (type-check a2) M-type)))))))))))
|
(equal? (type-check a2) M-type)))))))))))
|
||||||
|
|
||||||
(define (generate-enum-term)
|
(define (generate-enum-term [p-value 0.035])
|
||||||
(generate-term stlc M #:i-th (pick-an-index 0.035)))
|
(generate-term stlc M #:i-th (pick-an-index p-value)))
|
||||||
|
|
||||||
(define small-counter-example
|
(define small-counter-example
|
||||||
(term ((λ (x int) x) 1)))
|
(term ((λ (x int) x) 1)))
|
||||||
|
|
|
@ -303,8 +303,8 @@
|
||||||
(and (equal? (type-check a1) M-type)
|
(and (equal? (type-check a1) M-type)
|
||||||
(equal? (type-check a2) M-type)))))))))))
|
(equal? (type-check a2) M-type)))))))))))
|
||||||
|
|
||||||
(define (generate-enum-term)
|
(define (generate-enum-term [p-value 0.035])
|
||||||
(generate-term stlc M #:i-th (pick-an-index 0.035)))
|
(generate-term stlc M #:i-th (pick-an-index p-value)))
|
||||||
|
|
||||||
(define small-counter-example
|
(define small-counter-example
|
||||||
(term ((λ (x int) (λ (y int) y)) 1)))
|
(term ((λ (x int) (λ (y int) y)) 1)))
|
||||||
|
|
|
@ -302,8 +302,8 @@
|
||||||
(and (equal? (type-check a1) M-type)
|
(and (equal? (type-check a1) M-type)
|
||||||
(equal? (type-check a2) M-type)))))))))))
|
(equal? (type-check a2) M-type)))))))))))
|
||||||
|
|
||||||
(define (generate-enum-term)
|
(define (generate-enum-term [p-value 0.035])
|
||||||
(generate-term stlc M #:i-th (pick-an-index 0.035)))
|
(generate-term stlc M #:i-th (pick-an-index p-value)))
|
||||||
|
|
||||||
(define small-counter-example
|
(define small-counter-example
|
||||||
(term ((λ (x int) (+ 1)) 1)))
|
(term ((λ (x int) (+ 1)) 1)))
|
||||||
|
|
|
@ -302,8 +302,8 @@
|
||||||
(and (equal? (type-check a1) M-type)
|
(and (equal? (type-check a1) M-type)
|
||||||
(equal? (type-check a2) M-type)))))))))))
|
(equal? (type-check a2) M-type)))))))))))
|
||||||
|
|
||||||
(define (generate-enum-term)
|
(define (generate-enum-term [p-value 0.035])
|
||||||
(generate-term stlc M #:i-th (pick-an-index 0.035)))
|
(generate-term stlc M #:i-th (pick-an-index p-value)))
|
||||||
|
|
||||||
(define small-counter-example
|
(define small-counter-example
|
||||||
(term ((λ (z int) (((λ (y1 int) (λ (y int) y)) z) 1)) 0)))
|
(term ((λ (z int) (((λ (y1 int) (λ (y int) y)) z) 1)) 0)))
|
||||||
|
|
|
@ -302,8 +302,8 @@
|
||||||
(and (equal? (type-check a1) M-type)
|
(and (equal? (type-check a1) M-type)
|
||||||
(equal? (type-check a2) M-type)))))))))))
|
(equal? (type-check a2) M-type)))))))))))
|
||||||
|
|
||||||
(define (generate-enum-term)
|
(define (generate-enum-term [p-value 0.035])
|
||||||
(generate-term stlc M #:i-th (pick-an-index 0.035)))
|
(generate-term stlc M #:i-th (pick-an-index p-value)))
|
||||||
|
|
||||||
(define small-counter-example
|
(define small-counter-example
|
||||||
(term ((λ (x int) (λ (y (list int)) (hd y))) 1)))
|
(term ((λ (x int) (λ (y (list int)) (hd y))) 1)))
|
||||||
|
|
|
@ -289,8 +289,8 @@
|
||||||
(let ([red-type (type-check red-t)])
|
(let ([red-type (type-check red-t)])
|
||||||
(equal? t-type red-type))))))))))
|
(equal? t-type red-type))))))))))
|
||||||
|
|
||||||
(define (generate-enum-term)
|
(define (generate-enum-term [p-value 0.035])
|
||||||
(generate-term stlc M #:i-th (pick-an-index 0.035)))
|
(generate-term stlc M #:i-th (pick-an-index p-value)))
|
||||||
|
|
||||||
(define small-counter-example
|
(define small-counter-example
|
||||||
(term ((λ (x int) x) 1)))
|
(term ((λ (x int) x) 1)))
|
||||||
|
|
|
@ -292,8 +292,8 @@
|
||||||
(let ([red-type (type-check red-t)])
|
(let ([red-type (type-check red-t)])
|
||||||
(equal? t-type red-type))))))))))
|
(equal? t-type red-type))))))))))
|
||||||
|
|
||||||
(define (generate-enum-term)
|
(define (generate-enum-term [p-value 0.035])
|
||||||
(generate-term stlc M #:i-th (pick-an-index 0.035)))
|
(generate-term stlc M #:i-th (pick-an-index p-value)))
|
||||||
|
|
||||||
(define small-counter-example
|
(define small-counter-example
|
||||||
(term ((λ (x int) (λ (y int) y)) 1)))
|
(term ((λ (x int) (λ (y int) y)) 1)))
|
||||||
|
|
|
@ -291,8 +291,8 @@
|
||||||
(let ([red-type (type-check red-t)])
|
(let ([red-type (type-check red-t)])
|
||||||
(equal? t-type red-type))))))))))
|
(equal? t-type red-type))))))))))
|
||||||
|
|
||||||
(define (generate-enum-term)
|
(define (generate-enum-term [p-value 0.035])
|
||||||
(generate-term stlc M #:i-th (pick-an-index 0.035)))
|
(generate-term stlc M #:i-th (pick-an-index p-value)))
|
||||||
|
|
||||||
(define small-counter-example
|
(define small-counter-example
|
||||||
(term ((λ (x int) (+ 1)) 1)))
|
(term ((λ (x int) (+ 1)) 1)))
|
||||||
|
|
|
@ -291,8 +291,8 @@
|
||||||
(let ([red-type (type-check red-t)])
|
(let ([red-type (type-check red-t)])
|
||||||
(equal? t-type red-type))))))))))
|
(equal? t-type red-type))))))))))
|
||||||
|
|
||||||
(define (generate-enum-term)
|
(define (generate-enum-term [p-value 0.035])
|
||||||
(generate-term stlc M #:i-th (pick-an-index 0.035)))
|
(generate-term stlc M #:i-th (pick-an-index p-value)))
|
||||||
|
|
||||||
(define small-counter-example
|
(define small-counter-example
|
||||||
(term ((λ (a (list int)) (λ (x int) x)) nil)))
|
(term ((λ (a (list int)) (λ (x int) x)) nil)))
|
||||||
|
|
|
@ -302,8 +302,8 @@
|
||||||
(and (equal? (type-check a1) M-type)
|
(and (equal? (type-check a1) M-type)
|
||||||
(equal? (type-check a2) M-type)))))))))))
|
(equal? (type-check a2) M-type)))))))))))
|
||||||
|
|
||||||
(define (generate-enum-term)
|
(define (generate-enum-term [p-value 0.035])
|
||||||
(generate-term stlc M #:i-th (pick-an-index 0.035)))
|
(generate-term stlc M #:i-th (pick-an-index p-value)))
|
||||||
|
|
||||||
(define (ordered-enum-generator)
|
(define (ordered-enum-generator)
|
||||||
(let ([index 0])
|
(let ([index 0])
|
||||||
|
|
|
@ -258,8 +258,8 @@
|
||||||
(let ([red-type (type-check red-t)])
|
(let ([red-type (type-check red-t)])
|
||||||
(equal? t-type red-type))))))))))
|
(equal? t-type red-type))))))))))
|
||||||
|
|
||||||
(define (generate-enum-term)
|
(define (generate-enum-term [p-value 0.035])
|
||||||
(generate-term stlc M #:i-th (pick-an-index 0.035)))
|
(generate-term stlc M #:i-th (pick-an-index p-value)))
|
||||||
|
|
||||||
(define (ordered-enum-generator)
|
(define (ordered-enum-generator)
|
||||||
(let ([index 0])
|
(let ([index 0])
|
||||||
|
|
|
@ -258,8 +258,8 @@
|
||||||
(let ([red-type (type-check red-t)])
|
(let ([red-type (type-check red-t)])
|
||||||
(equal? t-type red-type))))))))))
|
(equal? t-type red-type))))))))))
|
||||||
|
|
||||||
(define (generate-enum-term)
|
(define (generate-enum-term [p-value 0.035])
|
||||||
(generate-term stlc M #:i-th (pick-an-index 0.035)))
|
(generate-term stlc M #:i-th (pick-an-index p-value)))
|
||||||
|
|
||||||
(define (ordered-enum-generator)
|
(define (ordered-enum-generator)
|
||||||
(let ([index 0])
|
(let ([index 0])
|
||||||
|
|
|
@ -259,8 +259,8 @@
|
||||||
(let ([red-type (type-check red-t)])
|
(let ([red-type (type-check red-t)])
|
||||||
(equal? t-type red-type))))))))))
|
(equal? t-type red-type))))))))))
|
||||||
|
|
||||||
(define (generate-enum-term)
|
(define (generate-enum-term [p-value 0.035])
|
||||||
(generate-term stlc M #:i-th (pick-an-index 0.035)))
|
(generate-term stlc M #:i-th (pick-an-index p-value)))
|
||||||
|
|
||||||
(define (ordered-enum-generator)
|
(define (ordered-enum-generator)
|
||||||
(let ([index 0])
|
(let ([index 0])
|
||||||
|
|
|
@ -259,8 +259,8 @@
|
||||||
(let ([red-type (type-check red-t)])
|
(let ([red-type (type-check red-t)])
|
||||||
(equal? t-type red-type))))))))))
|
(equal? t-type red-type))))))))))
|
||||||
|
|
||||||
(define (generate-enum-term)
|
(define (generate-enum-term [p-value 0.035])
|
||||||
(generate-term stlc M #:i-th (pick-an-index 0.035)))
|
(generate-term stlc M #:i-th (pick-an-index p-value)))
|
||||||
|
|
||||||
(define (ordered-enum-generator)
|
(define (ordered-enum-generator)
|
||||||
(let ([index 0])
|
(let ([index 0])
|
||||||
|
|
|
@ -258,8 +258,8 @@
|
||||||
(let ([red-type (type-check red-t)])
|
(let ([red-type (type-check red-t)])
|
||||||
(equal? t-type red-type))))))))))
|
(equal? t-type red-type))))))))))
|
||||||
|
|
||||||
(define (generate-enum-term)
|
(define (generate-enum-term [p-value 0.035])
|
||||||
(generate-term stlc M #:i-th (pick-an-index 0.035)))
|
(generate-term stlc M #:i-th (pick-an-index p-value)))
|
||||||
|
|
||||||
(define (ordered-enum-generator)
|
(define (ordered-enum-generator)
|
||||||
(let ([index 0])
|
(let ([index 0])
|
||||||
|
|
|
@ -258,8 +258,8 @@
|
||||||
(let ([red-type (type-check red-t)])
|
(let ([red-type (type-check red-t)])
|
||||||
(equal? t-type red-type))))))))))
|
(equal? t-type red-type))))))))))
|
||||||
|
|
||||||
(define (generate-enum-term)
|
(define (generate-enum-term [p-value 0.035])
|
||||||
(generate-term stlc M #:i-th (pick-an-index 0.035)))
|
(generate-term stlc M #:i-th (pick-an-index p-value)))
|
||||||
|
|
||||||
(define (ordered-enum-generator)
|
(define (ordered-enum-generator)
|
||||||
(let ([index 0])
|
(let ([index 0])
|
||||||
|
|
|
@ -257,8 +257,8 @@
|
||||||
(let ([red-type (type-check red-t)])
|
(let ([red-type (type-check red-t)])
|
||||||
(equal? t-type red-type))))))))))
|
(equal? t-type red-type))))))))))
|
||||||
|
|
||||||
(define (generate-enum-term)
|
(define (generate-enum-term [p-value 0.035])
|
||||||
(generate-term stlc M #:i-th (pick-an-index 0.035)))
|
(generate-term stlc M #:i-th (pick-an-index p-value)))
|
||||||
|
|
||||||
(define (ordered-enum-generator)
|
(define (ordered-enum-generator)
|
||||||
(let ([index 0])
|
(let ([index 0])
|
||||||
|
|
|
@ -258,8 +258,8 @@
|
||||||
(let ([red-type (type-check red-t)])
|
(let ([red-type (type-check red-t)])
|
||||||
(equal? t-type red-type))))))))))
|
(equal? t-type red-type))))))))))
|
||||||
|
|
||||||
(define (generate-enum-term)
|
(define (generate-enum-term [p-value 0.035])
|
||||||
(generate-term stlc M #:i-th (pick-an-index 0.035)))
|
(generate-term stlc M #:i-th (pick-an-index p-value)))
|
||||||
|
|
||||||
(define (ordered-enum-generator)
|
(define (ordered-enum-generator)
|
||||||
(let ([index 0])
|
(let ([index 0])
|
||||||
|
|
|
@ -258,8 +258,8 @@
|
||||||
(let ([red-type (type-check red-t)])
|
(let ([red-type (type-check red-t)])
|
||||||
(equal? t-type red-type))))))))))
|
(equal? t-type red-type))))))))))
|
||||||
|
|
||||||
(define (generate-enum-term)
|
(define (generate-enum-term [p-value 0.035])
|
||||||
(generate-term stlc M #:i-th (pick-an-index 0.035)))
|
(generate-term stlc M #:i-th (pick-an-index p-value)))
|
||||||
|
|
||||||
(define (ordered-enum-generator)
|
(define (ordered-enum-generator)
|
||||||
(let ([index 0])
|
(let ([index 0])
|
||||||
|
|
|
@ -259,8 +259,8 @@
|
||||||
(let ([red-type (type-check red-t)])
|
(let ([red-type (type-check red-t)])
|
||||||
(equal? t-type red-type))))))))))
|
(equal? t-type red-type))))))))))
|
||||||
|
|
||||||
(define (generate-enum-term)
|
(define (generate-enum-term [p-value 0.035])
|
||||||
(generate-term stlc M #:i-th (pick-an-index 0.035)))
|
(generate-term stlc M #:i-th (pick-an-index p-value)))
|
||||||
|
|
||||||
(define (ordered-enum-generator)
|
(define (ordered-enum-generator)
|
||||||
(let ([index 0])
|
(let ([index 0])
|
||||||
|
|
Loading…
Reference in New Issue
Block a user