Factor out grammar to generate well-typed terms with higher probability.
Allows us to test integer-specific functions.
This commit is contained in:
parent
f7e8b090e6
commit
3e9595e910
|
@ -22,82 +22,159 @@
|
||||||
[n real]
|
[n real]
|
||||||
;; randomly generate F, not E, because literal numbers self-evaluate
|
;; randomly generate F, not E, because literal numbers self-evaluate
|
||||||
;; (i.e. generates a useless test)
|
;; (i.e. generates a useless test)
|
||||||
[E n F]
|
[E* n E F I]
|
||||||
#;; racket/math
|
;; racket/math
|
||||||
[F (degrees->radians E)
|
;; [E (degrees->radians E)
|
||||||
(radians->degrees E)
|
;; (radians->degrees E)
|
||||||
(exact-round E)
|
;; (exact-round E)
|
||||||
(exact-floor E)
|
;; (exact-floor E)
|
||||||
(exact-ceiling E)
|
;; (exact-ceiling E)
|
||||||
(exact-truncate E)
|
;; (exact-truncate E)
|
||||||
(sinh E)
|
;; (sinh E)
|
||||||
(cosh E)
|
;; (cosh E)
|
||||||
(tanh E)
|
;; (tanh E)
|
||||||
(nan? E)
|
;; (nan? E)
|
||||||
(infinite? E)
|
;; (infinite? E)
|
||||||
|
;; ]
|
||||||
|
;; more likely to be floats
|
||||||
|
[F* (real->double-flonum n) F] ; TODO fix pre-processing to avoid cast
|
||||||
|
[F (* F*)
|
||||||
|
(* F* F*)
|
||||||
|
(* F* F* F*)
|
||||||
|
(+ F*)
|
||||||
|
(+ F* F*)
|
||||||
|
(+ F* F* F*)
|
||||||
|
(- F*)
|
||||||
|
(- F* F*)
|
||||||
|
(- F* F* F*)
|
||||||
|
(/ F*)
|
||||||
|
(/ F* F*)
|
||||||
|
(/ F* F* F*)
|
||||||
|
(max F*)
|
||||||
|
(max F* F*)
|
||||||
|
(max F* F* F*)
|
||||||
|
(min F*)
|
||||||
|
(min F* F*)
|
||||||
|
(min F* F* F*)
|
||||||
|
(add1 F*)
|
||||||
|
(sub1 F*)
|
||||||
|
(abs F*)
|
||||||
|
(floor F*)
|
||||||
|
(ceiling F*)
|
||||||
|
(truncate F*)
|
||||||
|
(round F*)
|
||||||
|
(cos F*)
|
||||||
|
(sin F*)
|
||||||
|
(tan F*)
|
||||||
|
(sqr F*)
|
||||||
|
(flabs F*)
|
||||||
|
(flround F*)
|
||||||
|
(flfloor F*)
|
||||||
|
(flceiling F*)
|
||||||
|
(fltruncate F*)
|
||||||
|
(flsin F*)
|
||||||
|
(flcos F*)
|
||||||
|
(fltan F*)
|
||||||
|
(flatan F*)
|
||||||
|
(flasin F*)
|
||||||
|
(flacos F*)
|
||||||
|
(fllog F*)
|
||||||
|
(flexp F*)
|
||||||
|
(flsqrt F*)
|
||||||
|
(unsafe-flabs F*)
|
||||||
|
(unsafe-flmin F* F*)
|
||||||
|
(unsafe-flmax F* F*)
|
||||||
|
(unsafe-flsqrt F*)
|
||||||
|
(fl+ F* F*)
|
||||||
|
(fl- F* F*)
|
||||||
|
(fl* F* F*)
|
||||||
|
(fl/ F* F*)
|
||||||
|
(flmin F* F*)
|
||||||
|
(flmax F* F*)
|
||||||
|
(flexpt F* F*)
|
||||||
|
(unsafe-fl+ F* F*)
|
||||||
|
(unsafe-fl- F* F*)
|
||||||
|
(unsafe-fl* F* F*)
|
||||||
|
(unsafe-fl/ F* F*)]
|
||||||
|
;; more likely to be integers
|
||||||
|
[I* (exact-round n) I] ; TODO fix pre-processing to avoid cast
|
||||||
|
[I (* I*)
|
||||||
|
(* I* I*)
|
||||||
|
(* I* I* I*)
|
||||||
|
(+ I*)
|
||||||
|
(+ I* I*)
|
||||||
|
(+ I* I* I*)
|
||||||
|
(- I*)
|
||||||
|
(- I* I*)
|
||||||
|
(- I* I* I*)
|
||||||
|
(max I*)
|
||||||
|
(max I* I*)
|
||||||
|
(max I* I* I*)
|
||||||
|
(min I*)
|
||||||
|
(min I* I*)
|
||||||
|
(min I* I* I*)
|
||||||
|
(add1 I*)
|
||||||
|
(sub1 I*)
|
||||||
|
(abs I*)
|
||||||
|
(floor I*)
|
||||||
|
(ceiling I*)
|
||||||
|
(truncate I*)
|
||||||
|
(round I*)
|
||||||
|
(sqr I*)
|
||||||
|
(modulo I* I*)
|
||||||
|
(remainder I* I*)
|
||||||
|
(quotient I* I*)
|
||||||
|
(gcd I*)
|
||||||
|
(gcd I* I*)
|
||||||
|
(gcd I* I* I*)
|
||||||
|
(lcm I*)
|
||||||
|
(lcm I* I*)
|
||||||
|
(lcm I* I* I*)
|
||||||
|
(arithmetic-shift I* I*)
|
||||||
|
(bitwise-and I*)
|
||||||
|
(bitwise-and I* I*)
|
||||||
|
(bitwise-and I* I* I*)
|
||||||
|
(bitwise-ior I*)
|
||||||
|
(bitwise-ior I* I*)
|
||||||
|
(bitwise-ior I* I* I*)
|
||||||
|
(bitwise-xor I*)
|
||||||
|
(bitwise-xor I* I*)
|
||||||
|
(bitwise-xor I* I* I*)
|
||||||
|
(bitwise-not I*)
|
||||||
|
(integer-length I*)
|
||||||
]
|
]
|
||||||
;; racket/base, racket/flonum, racket/unsafe/ops
|
[E (* E*)
|
||||||
[F (* E)
|
(* E* E*)
|
||||||
(* E E)
|
(* E* E* E*)
|
||||||
(* E E E)
|
(+ E*)
|
||||||
(+ E)
|
(+ E* E*)
|
||||||
(+ E E)
|
(+ E* E* E*)
|
||||||
(+ E E E)
|
(- E*)
|
||||||
(- E)
|
(- E* E*)
|
||||||
(- E E)
|
(- E* E* E*)
|
||||||
(- E E E)
|
(/ E*)
|
||||||
(/ E)
|
(/ E* E*)
|
||||||
(/ E E)
|
(/ E* E* E*)
|
||||||
(/ E E E)
|
(max E*)
|
||||||
(max E)
|
(max E* E*)
|
||||||
(max E E)
|
(max E* E* E*)
|
||||||
(max E E E)
|
(min E*)
|
||||||
(min E)
|
(min E* E*)
|
||||||
(min E E)
|
(min E* E* E*)
|
||||||
(min E E E)
|
(add1 E*)
|
||||||
(add1 E)
|
(sub1 E*)
|
||||||
(sub1 E)
|
(abs E*)
|
||||||
(abs E)
|
(floor E*)
|
||||||
(floor E)
|
(ceiling E*)
|
||||||
(ceiling E)
|
(truncate E*)
|
||||||
(truncate E)
|
(round E*)
|
||||||
(round E)
|
(sqrt E*)
|
||||||
(sqrt E)
|
(log E*)
|
||||||
(log E)
|
(exp E*)
|
||||||
(exp E)
|
(cos E*)
|
||||||
(cos E)
|
(sin E*)
|
||||||
(sin E)
|
(tan E*)
|
||||||
(tan E)
|
(sqr E*)
|
||||||
(sqr E)
|
|
||||||
(flabs E)
|
|
||||||
(flround E)
|
|
||||||
(flfloor E)
|
|
||||||
(flceiling E)
|
|
||||||
(fltruncate E)
|
|
||||||
(flsin E)
|
|
||||||
(flcos E)
|
|
||||||
(fltan E)
|
|
||||||
(flatan E)
|
|
||||||
(flasin E)
|
|
||||||
(flacos E)
|
|
||||||
(fllog E)
|
|
||||||
(flexp E)
|
|
||||||
(flsqrt E)
|
|
||||||
(unsafe-flabs E)
|
|
||||||
(unsafe-flmin E E)
|
|
||||||
(unsafe-flmax E E)
|
|
||||||
(unsafe-flsqrt E)
|
|
||||||
(fl+ E E)
|
|
||||||
(fl- E E)
|
|
||||||
(fl* E E)
|
|
||||||
(fl/ E E)
|
|
||||||
(flmin E E)
|
|
||||||
(flmax E E)
|
|
||||||
(flexpt E E)
|
|
||||||
(unsafe-fl+ E E)
|
|
||||||
(unsafe-fl- E E)
|
|
||||||
(unsafe-fl* E E)
|
|
||||||
(unsafe-fl/ E E)
|
|
||||||
])
|
])
|
||||||
;; generated from: (map car (file->list "base-env-parts"))
|
;; generated from: (map car (file->list "base-env-parts"))
|
||||||
|
|
||||||
|
@ -176,7 +253,7 @@
|
||||||
(call-with-limits
|
(call-with-limits
|
||||||
#f 1000
|
#f 1000
|
||||||
(lambda ()
|
(lambda ()
|
||||||
(redex-check tr-arith F (check-all-reals (term F))
|
(redex-check tr-arith E (check-all-reals (term E))
|
||||||
#:attempts n-attempts
|
#:attempts n-attempts
|
||||||
#:prepare exp->real-exp)))
|
#:prepare exp->real-exp)))
|
||||||
|
|
||||||
|
|
Loading…
Reference in New Issue
Block a user