# HG changeset patch
# User haftmann
# Date 1202118760 -3600
# Node ID 55a02586776d964fd0755dafd6724aa5dcf18ab7
# Parent  8bf9e480a7b81144496350436700925313b2ad3c
towards quickcheck

diff -r 8bf9e480a7b8 -r 55a02586776d src/HOL/ex/Random.thy
--- a/src/HOL/ex/Random.thy	Mon Feb 04 10:52:39 2008 +0100
+++ b/src/HOL/ex/Random.thy	Mon Feb 04 10:52:40 2008 +0100
@@ -2,59 +2,97 @@
     Author:     Florian Haftmann, TU Muenchen
 *)
 
-header {* A simple random engine *}
+header {* A simple term generator *}
 
 theory Random
-imports State_Monad Code_Integer
+imports State_Monad Code_Index List Eval
 begin
 
-fun
-  pick :: "(nat \<times> 'a) list \<Rightarrow> nat \<Rightarrow> 'a"
-where
-  pick_undef: "pick [] n = undefined"
-  | pick_simp: "pick ((k, v)#xs) n = (if n < k then v else pick xs (n - k))"
-lemmas [code func del] = pick_undef
+subsection {* The random engine *}
+
+types seed = "index \<times> index"
 
-typedecl randseed
-
-axiomatization
-  random_shift :: "randseed \<Rightarrow> randseed"
-
-axiomatization
-  random_seed :: "randseed \<Rightarrow> nat"
+definition
+  "next" :: "seed \<Rightarrow> index \<times> seed"
+where
+  "next s = (let
+     (v, w) = s;
+     k = v div 53668;
+     v' = 40014 * (v - k * 53668) - k * 12211;
+     v'' = (if v' < 0 then v' + 2147483563 else v');
+     l = w div 52774;
+     w' = 40692 * (w - l * 52774) - l * 3791;
+     w'' = (if w' < 0 then w' + 2147483399 else w');
+     z = v'' - w'';
+     z' = (if z < 1 then z + 2147483562 else z)
+   in (z',  (v'', w'')))"
 
 definition
-  random :: "nat \<Rightarrow> randseed \<Rightarrow> nat \<times> randseed" where
-  "random n s = (random_seed s mod n, random_shift s)"
+  split_seed :: "seed \<Rightarrow> seed \<times> seed"
+where
+  "split_seed s = (let
+     (v, w) = s;
+     (v', w') = snd (next s);
+     v'' = (if v = 2147483562 then 1 else v + 1);
+     s'' = (v'', w');
+     w'' = (if w = 2147483398 then 1 else w + 1);
+     s''' = (v', w'')
+   in (s'', s'''))"
+
+text {* Base selectors *}
+
+primrec
+  pick :: "(nat \<times> 'a) list \<Rightarrow> nat \<Rightarrow> 'a"
+where
+  "pick (x#xs) n = (if n < fst x then snd x else pick xs (n - fst x))"
 
-lemma random_bound:
-  assumes "0 < n"
-  shows "fst (random n s) < n"
-proof -
-  from prems mod_less_divisor have "!!m .m mod n < n" by auto
-  then show ?thesis unfolding random_def by simp 
-qed
+function
+  iLogBase :: "index \<Rightarrow> index \<Rightarrow> index"
+where
+  "iLogBase b i = (if b \<le> 1 \<or> i < b then 1 else 1 + iLogBase b (i div b))"
+by pat_completeness auto
+termination
+  by (relation "measure (nat_of_index o snd)")
+    (auto simp add: index)
 
-lemma random_random_seed [simp]:
-  "snd (random n s) = random_shift s" unfolding random_def by simp
+function
+  range_aux :: "index \<Rightarrow> index \<Rightarrow> seed \<Rightarrow> index \<times> seed"
+where
+  "range_aux k l s = (if k = 0 then (l, s) else
+    let (v, s') = next s
+  in range_aux (k - 1) (v + l * 2147483561) s')"
+by pat_completeness auto
+termination
+  by (relation "measure (nat_of_index o fst)")
+    (auto simp add: index)
 
 definition
-  select :: "'a list \<Rightarrow> randseed \<Rightarrow> 'a \<times> randseed" where
-  [simp]: "select xs = (do
-      n \<leftarrow> random (length xs);
-      return (nth xs n)
-    done)"
+  range :: "index \<Rightarrow> seed \<Rightarrow> index \<times> seed"
+where
+  "range k s = (let
+    b = 2147483561;
+    n = iLogBase b k;
+    (v, s') = range_aux n 1 s
+  in (v mod k, s'))"
+
 definition
-  select_weight :: "(nat \<times> 'a) list \<Rightarrow> randseed \<Rightarrow> 'a \<times> randseed" where
-  [simp]: "select_weight xs = (do
-      n \<leftarrow> random (foldl (op +) 0 (map fst xs));
-      return (pick xs n)
-    done)"
+  select :: "'a list \<Rightarrow> seed \<Rightarrow> 'a \<times> seed"
+where
+  [simp]: "select xs s = (let
+    (k, s') = range (index_of_nat (length xs)) s
+  in (nth xs (nat_of_index k), s'))"
 
-lemma
+definition
+  select_weight :: "(nat \<times> 'a) list \<Rightarrow> seed \<Rightarrow> 'a \<times> seed"
+where
+  [simp]: "select_weight xs s = (let
+    (k, s') = range (foldr (op + \<circ> index_of_nat \<circ> fst) xs 0) s
+  in (pick xs (nat_of_index k), s'))"
+
+(*lemma
   "select (x#xs) s = select_weight (map (Pair 1) (x#xs)) s"
 proof (induct xs)
-  case Nil show ?case by (simp add: monad_collapse random_def)
+  case Nil show ?case apply (auto simp add: Let_def split_def) 
 next
   have map_fst_Pair: "!!xs y. map fst (map (Pair y) xs) = replicate (length xs) y"
   proof -
@@ -115,71 +153,300 @@
   case (Cons x xs) then show ?case
     unfolding select_weight_def sum_length pick_nth_random_do
     by simp
-qed
-
-definition
-  random_int :: "int \<Rightarrow> randseed \<Rightarrow> int * randseed" where
-  "random_int k = (do n \<leftarrow> random (nat k); return (int n) done)"
+qed*)
 
-lemma random_nat [code]:
-  "random n = (do k \<leftarrow> random_int (int n); return (nat k) done)"
-unfolding random_int_def by simp
-
-axiomatization
-  run_random :: "(randseed \<Rightarrow> 'a * randseed) \<Rightarrow> 'a"
+text {* The @{text ML} interface *}
 
 ML {*
-signature RANDOM =
-sig
-  type seed = int;
-  val seed: unit -> seed;
-  val value: int -> seed -> int * seed;
-end;
-
-structure Random : RANDOM =
+structure Quickcheck =
 struct
 
-exception RANDOM;
-
-type seed = int;
-
-local
-  val a = 16807;
-  val m = 2147483647;
-in
-  fun next s = (a * s) mod m;
-end;
+type seed = int * int;
 
 local
-  val seed_ref = ref 1;
+
+val seed = ref (0, 0);
+
+fun init () =
+  let
+    val now = Time.toNanoseconds (Time.now ());
+    val (q, s1) = IntInf.divMod (now, 2147483562);
+    val s2 = q mod 2147483398;
+  in seed := (s1 + 1, s2 + 1) end;
+  
 in
-  fun seed () = CRITICAL (fn () =>
-    let
-      val r = next (!seed_ref)
-    in
-      (seed_ref := r; r)
-    end);
+
+val seed = seed; (* FIXME *)
+
+fun run f =
+  let
+    val (x, seed') = f (!seed);
+    val _ = seed := seed'
+    val _ = if fst (! seed) = 0 orelse snd (! seed) = 0 then
+      (warning "broken random seed"; init ())
+      else ()
+  in x end;
+
 end;
 
-fun value h s =
-  if h < 1 then raise RANDOM
-  else (s mod (h - 1), seed ());
-
 end;
 *}
 
-code_reserved SML Random
+
+subsection {* The @{text random} class *}
+
+class random = type +
+  fixes random :: "index \<Rightarrow> seed \<Rightarrow> 'a \<times> seed"
+
+-- {* FIXME dummy implementations *}
+
+instantiation nat :: random
+begin
+
+definition
+  "random k = apfst nat_of_index \<circ> range k"
+
+instance ..
+
+end
+
+instantiation bool :: random
+begin
+
+definition
+  "random _ = apfst (op = 0) \<circ> range 2"
+
+instance ..
+
+end
 
-code_type randseed
-  (SML "Random.seed")
-types_code randseed ("Random.seed")
+instantiation unit :: random
+begin
+
+definition
+  "random _ = Pair ()"
+
+instance ..
+
+end
+
+instantiation "+" :: (random, random) random
+begin
+
+definition
+  "random n = (do
+     k \<leftarrow> next;
+     let l = k div 2;
+     (if k mod 2 = 0 then do 
+       x \<leftarrow> random l;
+       return (Inl x)
+     done else do
+       x \<leftarrow> random l;
+       return (Inr x)
+     done)
+   done)"
+
+instance ..
+
+end
 
-code_const random_int
-  (SML "Random.value")
-consts_code random_int ("Random.value")
+instantiation "*" :: (random, random) random
+begin
+
+definition
+  "random n = (do
+     x \<leftarrow> random n;
+     y \<leftarrow> random n;
+     return (x, y)
+   done)"
+
+instance ..
+
+end
+
+instantiation int :: random
+begin
+
+definition
+  "random n = (do
+     (b, m) \<leftarrow> random n;
+     return (if b then int m else - int m)
+   done)"
+
+instance ..
+
+end
+
+instantiation list :: (random) random
+begin
 
-code_const run_random
-  (SML "case (Random.seed ()) of (x, '_) => _ x")
-consts_code run_random ("case (Random.seed ()) of (x, '_) => _ x")
+primrec
+  random_list_aux
+where
+  "random_list_aux 0 = Pair []"
+  | "random_list_aux (Suc n) = (do
+       x \<leftarrow> random (index_of_nat (Suc n));
+       xs \<leftarrow> random_list_aux n;
+       return (x#xs)
+     done)"
+
+definition
+  [code func del]: "random n = random_list_aux (nat_of_index n)"
+
+lemma [code func]:
+  "random n = (if n = 0 then return ([]::'a list)
+    else do
+       x \<leftarrow> random n;
+       xs \<leftarrow> random (n - 1);
+       return (x#xs)
+     done)"
+unfolding random_list_def
+by (cases "nat_of_index n", auto)
+  (cases n, auto)+
+
+(*fun
+  random_list
+where
+  "random_list n = (if n = 0 then (\<lambda>_. ([]::'a list)) 
+    else random n \<guillemotright>=\<^isub>R (\<lambda>x::'a. random_list (n - 1) \<guillemotright>=\<^isub>R (\<lambda>(xs::'a list) _. x#xs)))"*)
+
+instance ..
 
 end
+
+code_reserved SML Quickcheck
+
+
+subsection {* Quickcheck generator *}
+
+ML {*
+structure Quickcheck =
+struct
+
+open Quickcheck;
+
+val eval_ref : (unit -> int -> int * int -> term list option * (int * int)) option ref = ref NONE;
+
+fun mk_generator_expr prop tys =
+  let
+    val bounds = map_index (fn (i, ty) => (i, ty)) tys;
+    val result = list_comb (prop, map (fn (i, _) => Bound (length tys - i - 1)) bounds);
+    val terms = map (fn (i, ty) => Const (@{const_name Eval.term_of}, ty --> @{typ term}) $ Bound (length tys - i - 1)) bounds;
+    val check = @{term "If \<Colon> bool \<Rightarrow> term list option \<Rightarrow> term list option \<Rightarrow> term list option"}
+      $ result $ @{term "None \<Colon> term list option"} $ (@{term "Some \<Colon> term list \<Rightarrow> term list option "} $ HOLogic.mk_list @{typ term} terms);
+    val return = @{term "Pair \<Colon> term list option \<Rightarrow> seed \<Rightarrow> term list option \<times> seed"};
+    fun mk_bindtyp ty = @{typ seed} --> HOLogic.mk_prodT (ty, @{typ seed});
+    fun mk_bindclause (i, ty) t = Const (@{const_name mbind}, mk_bindtyp ty
+      --> (ty --> mk_bindtyp @{typ "term list option"}) --> mk_bindtyp @{typ "term list option"})
+      $ (Const (@{const_name random}, @{typ index} --> mk_bindtyp ty)
+        $ Bound i) $ Abs ("a", ty, t);
+    val t = fold_rev mk_bindclause bounds (return $ check);
+  in Abs ("n", @{typ index}, t) end;
+
+fun compile_generator_expr thy prop tys =
+  let
+    val f = CodePackage.eval_term ("Quickcheck.eval_ref", eval_ref) thy
+      (mk_generator_expr prop tys) [];
+  in f #> run #> (Option.map o map) (Code.postprocess_term thy) end;
+
+end
+*}
+
+ML {* val f = Quickcheck.compile_generator_expr @{theory}
+  @{term "\<lambda>(n::nat) (m::nat) (q::nat). n = m + q + 1"} [@{typ nat}, @{typ nat}, @{typ nat}] *}
+
+ML {* f 5 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
+ML {* f 5 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
+ML {* f 20 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
+ML {* f 20 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
+ML {* f 20 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
+ML {* f 20 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
+ML {* f 25 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
+ML {* f 1 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
+ML {* f 1 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
+ML {* f 2 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
+ML {* f 2 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
+
+ML {* val f = Quickcheck.compile_generator_expr @{theory}
+  @{term "\<lambda>(n::int) (m::int) (q::int). n = m + q + 1"} [@{typ int}, @{typ int}, @{typ int}] *}
+
+ML {* f 5 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
+ML {* f 5 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
+ML {* f 20 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
+ML {* f 20 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
+ML {* f 20 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
+ML {* f 20 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
+ML {* f 25 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
+ML {* f 1 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
+ML {* f 1 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
+ML {* f 2 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
+ML {* f 2 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
+
+
+subsection {* Incremental function generator *}
+
+ML {*
+structure Quickcheck =
+struct
+
+open Quickcheck;
+
+fun random_fun (eq : 'a -> 'a -> bool)
+    (random : seed -> 'b * seed)
+    (random_split : seed -> seed * seed)
+    (seed : seed) =
+  let
+    val (seed', seed'') = random_split seed;
+    val state = ref (seed', []);
+    fun random_fun' x =
+      let
+        val (seed, fun_map) = ! state;
+      in case AList.lookup (uncurry eq) fun_map x
+       of SOME y => y
+        | NONE => let
+              val (y, seed') = random seed;
+              val _ = state := (seed', (x, y) :: fun_map);
+            in y end
+      end;
+  in (random_fun', seed'') end;
+
+end
+*}
+
+axiomatization
+  random_fun_aux :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> (seed \<Rightarrow> 'b \<times> seed)
+    \<Rightarrow> (seed \<Rightarrow> seed \<times> seed) \<Rightarrow> seed \<Rightarrow> ('a \<Rightarrow> 'b) \<times> seed"
+
+code_const random_fun_aux (SML "Quickcheck.random'_fun")
+
+instantiation "fun" :: (term_of, term_of) term_of
+begin
+
+instance ..
+
+end
+
+code_const "Eval.term_of :: ('a\<Colon>term_of \<Rightarrow> 'b\<Colon>term_of) \<Rightarrow> _"
+  (SML "(fn '_ => Const (\"arbitrary\", dummyT))")
+
+instantiation "fun" :: (eq, random) random
+begin
+
+definition
+  "random n = random_fun_aux (op =) (random n) split_seed"
+
+instance ..
+
+end
+
+ML {* val f = Quickcheck.compile_generator_expr @{theory}
+  @{term "\<lambda>f k. int (f k) = k"} [@{typ "int \<Rightarrow> nat"}, @{typ int}] *}
+
+ML {* f 20 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
+ML {* f 20 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
+ML {* f 20 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
+ML {* f 20 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
+ML {* f 20 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
+ML {* f 20 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
+
+end