New interface for test data generators.
--- a/src/HOL/Code_Setup.thy Thu Jan 10 17:06:41 2008 +0100
+++ b/src/HOL/Code_Setup.thy Thu Jan 10 19:09:21 2008 +0100
@@ -20,7 +20,9 @@
fun term_of_bool b = if b then HOLogic.true_const else HOLogic.false_const;
*}
attach (test) {*
-fun gen_bool i = one_of [false, true];
+fun gen_bool i =
+ let val b = one_of [false, true]
+ in (b, fn () => term_of_bool b) end;
*}
"prop" ("bool")
attach (term_of) {*
--- a/src/HOL/Library/Efficient_Nat.thy Thu Jan 10 17:06:41 2008 +0100
+++ b/src/HOL/Library/Efficient_Nat.thy Thu Jan 10 19:09:21 2008 +0100
@@ -183,7 +183,9 @@
val term_of_nat = HOLogic.mk_number HOLogic.natT;
*}
attach (test) {*
-fun gen_nat i = random_range 0 i;
+fun gen_nat i =
+ let val n = random_range 0 i
+ in (n, fn () => term_of_nat n) end;
*}
consts_code
--- a/src/HOL/Library/Executable_Set.thy Thu Jan 10 17:06:41 2008 +0100
+++ b/src/HOL/Library/Executable_Set.thy Thu Jan 10 19:09:21 2008 +0100
@@ -250,9 +250,17 @@
T --> Type ("set", [T]) --> Type ("set", [T])) $ f x $ term_of_set f T xs;
*}
attach (test) {*
-fun gen_set' aG i j = frequency
- [(i, fn () => aG j :: gen_set' aG (i-1) j), (1, fn () => [])] ()
-and gen_set aG i = gen_set' aG i i;
+fun gen_set' aG aT i j = frequency
+ [(i, fn () =>
+ let
+ val (x, t) = aG j;
+ val (xs, ts) = gen_set' aG aT (i-1) j
+ in
+ (x :: xs, fn () => Const ("insert",
+ aT --> Type ("set", [aT]) --> Type ("set", [aT])) $ t () $ ts ())
+ end),
+ (1, fn () => ([], fn () => Const ("{}", Type ("set", [aT]))))] ()
+and gen_set aG aT i = gen_set' aG aT i i;
*}
--- a/src/HOL/List.thy Thu Jan 10 17:06:41 2008 +0100
+++ b/src/HOL/List.thy Thu Jan 10 19:09:21 2008 +0100
@@ -3100,16 +3100,23 @@
fun term_of_list f T = HOLogic.mk_list T o map f;
*}
attach (test) {*
-fun gen_list' aG i j = frequency
- [(i, fn () => aG j :: gen_list' aG (i-1) j), (1, fn () => [])] ()
-and gen_list aG i = gen_list' aG i i;
+fun gen_list' aG aT i j = frequency
+ [(i, fn () =>
+ let
+ val (x, t) = aG j;
+ val (xs, ts) = gen_list' aG aT (i-1) j
+ in (x :: xs, fn () => HOLogic.cons_const aT $ t () $ ts ()) end),
+ (1, fn () => ([], fn () => HOLogic.nil_const aT))] ()
+and gen_list aG aT i = gen_list' aG aT i i;
*}
"char" ("string")
attach (term_of) {*
val term_of_char = HOLogic.mk_char o ord;
*}
attach (test) {*
-fun gen_char i = chr (random_range (ord "a") (Int.min (ord "a" + i, ord "z")));
+fun gen_char i =
+ let val j = random_range (ord "a") (Int.min (ord "a" + i, ord "z"))
+ in (chr j, fn () => HOLogic.mk_char j) end;
*}
consts_code "Cons" ("(_ ::/ _)")
--- a/src/HOL/Numeral.thy Thu Jan 10 17:06:41 2008 +0100
+++ b/src/HOL/Numeral.thy Thu Jan 10 19:09:21 2008 +0100
@@ -644,7 +644,9 @@
val term_of_int = HOLogic.mk_number HOLogic.intT;
*}
attach (test) {*
-fun gen_int i = one_of [~1, 1] * random_range 0 i;
+fun gen_int i =
+ let val j = one_of [~1, 1] * random_range 0 i
+ in (j, fn () => term_of_int j) end;
*}
setup {*
--- a/src/HOL/Product_Type.thy Thu Jan 10 17:06:41 2008 +0100
+++ b/src/HOL/Product_Type.thy Thu Jan 10 19:09:21 2008 +0100
@@ -941,10 +941,14 @@
types_code
"*" ("(_ */ _)")
attach (term_of) {*
-fun term_of_id_42 f T g U (x, y) = HOLogic.pair_const T U $ f x $ g y;
+fun term_of_id_42 aF aT bF bT (x, y) = HOLogic.pair_const aT bT $ aF x $ bF y;
*}
attach (test) {*
-fun gen_id_42 aG bG i = (aG i, bG i);
+fun gen_id_42 aG aT bG bT i =
+ let
+ val (x, t) = aG i;
+ val (y, u) = bG i
+ in ((x, y), fn () => HOLogic.pair_const aT bT $ t () $ u ()) end;
*}
consts_code
--- a/src/HOL/Real/Rational.thy Thu Jan 10 17:06:41 2008 +0100
+++ b/src/HOL/Real/Rational.thy Thu Jan 10 19:09:21 2008 +0100
@@ -713,7 +713,7 @@
val rT = Type ("Rational.rat", [])
in
if q = 1 orelse p = 0 then HOLogic.mk_number rT p
- else Const ("HOL.inverse_class.divide", rT --> rT --> rT) $
+ else @{term "op / \<Colon> rat \<Rightarrow> rat \<Rightarrow> rat"} $
HOLogic.mk_number rT p $ HOLogic.mk_number rT q
end;
*}
@@ -725,9 +725,10 @@
val g = Integer.gcd p q;
val p' = p div g;
val q' = q div g;
+ val r = (if one_of [true, false] then p' else ~ p',
+ if p' = 0 then 0 else q')
in
- (if one_of [true, false] then p' else ~ p',
- if p' = 0 then 0 else q')
+ (r, fn () => term_of_rat r)
end;
*}
--- a/src/HOL/Real/RealDef.thy Thu Jan 10 17:06:41 2008 +0100
+++ b/src/HOL/Real/RealDef.thy Thu Jan 10 19:09:21 2008 +0100
@@ -1051,9 +1051,10 @@
val g = Integer.gcd p q;
val p' = p div g;
val q' = q div g;
+ val r = (if one_of [true, false] then p' else ~ p',
+ if p' = 0 then 0 else q')
in
- (if one_of [true, false] then p' else ~ p',
- if p' = 0 then 0 else q')
+ (r, fn () => term_of_real r)
end;
*}