# HG changeset patch
# User berghofe
# Date 1199988561 -3600
# Node ID 6fbc3f54f8198aeef6a618e237f965d9f6310822
# Parent  a69e665b7df8ef4974d27adcc8d398fabbc5139b
New interface for test data generators.

diff -r a69e665b7df8 -r 6fbc3f54f819 src/HOL/Code_Setup.thy
--- 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) {*
diff -r a69e665b7df8 -r 6fbc3f54f819 src/HOL/Library/Efficient_Nat.thy
--- 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
diff -r a69e665b7df8 -r 6fbc3f54f819 src/HOL/Library/Executable_Set.thy
--- 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;
 *}
 
 
diff -r a69e665b7df8 -r 6fbc3f54f819 src/HOL/List.thy
--- 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" ("(_ ::/ _)")
diff -r a69e665b7df8 -r 6fbc3f54f819 src/HOL/Numeral.thy
--- 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 {*
diff -r a69e665b7df8 -r 6fbc3f54f819 src/HOL/Product_Type.thy
--- 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
diff -r a69e665b7df8 -r 6fbc3f54f819 src/HOL/Real/Rational.thy
--- 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;
 *}
 
diff -r a69e665b7df8 -r 6fbc3f54f819 src/HOL/Real/RealDef.thy
--- 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;
 *}