adding function generation to SmallCheck; activating exhaustive search space testing

--- a/src/HOL/Smallcheck.thy	Mon Nov 22 10:41:57 2010 +0100
+++ b/src/HOL/Smallcheck.thy	Mon Nov 22 10:41:58 2010 +0100
@@ -16,7 +16,7 @@
 instantiation unit :: small
 begin
 
-definition "find_first f d = f ()"
+definition "small f d = f ()"
 
 instance ..
 
@@ -48,6 +48,73 @@
 
 end
 
+section {* full small value generator type classes *}
+
+class full_small = term_of +
+fixes full_small :: "('a * (unit => term) \<Rightarrow> term list option) \<Rightarrow> code_numeral \<Rightarrow> term list option"
+
+instantiation unit :: full_small
+begin
+
+definition "full_small f d = f (Code_Evaluation.valtermify ())"
+
+instance ..
+
+end
+
+instantiation int :: full_small
+begin
+
+function full_small' :: "(int * (unit => term) => term list option) => int => int => term list option"
+  where "full_small' f d i = (if d < i then None else (case f (i, %_. Code_Evaluation.term_of i) of Some t => Some t | None => full_small' f d (i + 1)))"
+by pat_completeness auto
+
+termination 
+  by (relation "measure (%(_, d, i). nat (d + 1 - i))") auto
+
+definition "full_small f d = full_small' f (Code_Numeral.int_of d) (- (Code_Numeral.int_of d))"
+
+instance ..
+
+end
+
+instantiation prod :: (full_small, full_small) full_small
+begin
+ML {* @{const_name "Pair"} *}
+definition
+  "full_small f d = full_small (%(x, t1). full_small (%(y, t2). f ((x, y),
+    %u. Code_Evaluation.App (Code_Evaluation.App (Code_Evaluation.term_of (Pair :: 'a => 'b => ('a * 'b))) (t1 ())) (t2 ()))) d) d"
+
+instance ..
+
+end
+
+instantiation "fun" :: ("{equal, full_small}", full_small) full_small
+begin
+
+fun full_small_fun' :: "(('a => 'b) * (unit => term) => term list option) => code_numeral => code_numeral => term list option"
+where
+  "full_small_fun' f i d = (if i > 1 then
+    full_small (%(a, at). full_small (%(b, bt).
+      full_small_fun' (%(g, gt). f (g(a := b),
+        (%_. let T1 = (Typerep.typerep (TYPE('a))); T2 = (Typerep.typerep (TYPE('b))) in Code_Evaluation.App (Code_Evaluation.App (Code_Evaluation.App
+         
+(Code_Evaluation.Const (STR ''Fun.fun_upd'')
+
+(Typerep.Typerep (STR ''fun'') [Typerep.Typerep (STR ''fun'') [T1, T2], Typerep.Typerep (STR ''fun'') [T1, Typerep.Typerep (STR ''fun'') [T2, Typerep.Typerep (STR ''fun'') [T1, T2]]]]))
+
+ (gt ())) (at ())) (bt ())))) (i - 1) d) d) d else (if i > 0 then
+  full_small (%(b, t). f (%_. b, %_. Code_Evaluation.Abs (STR ''x'') (Typerep.typerep TYPE('a)) (t ()))) d else None))"
+
+definition full_small_fun :: "(('a => 'b) * (unit => term) => term list option) => code_numeral => term list option"
+where
+  "full_small_fun f d = full_small_fun' f d d" 
+
+
+instance ..
+
+end
+
 subsection {* Defining combinators for any first-order data type *}
 
 definition catch_match :: "term list option => term list option => term list option"
@@ -59,7 +126,7 @@
 
 use "Tools/smallvalue_generators.ML"
 
-(* We do not activate smallcheck yet. 
+(* We do not activate smallcheck yet.
 setup {* Smallvalue_Generators.setup *}
 *)
 

--- a/src/HOL/Tools/smallvalue_generators.ML	Mon Nov 22 10:41:57 2010 +0100
+++ b/src/HOL/Tools/smallvalue_generators.ML	Mon Nov 22 10:41:58 2010 +0100
@@ -6,7 +6,6 @@
 
 signature SMALLVALUE_GENERATORS =
 sig
-  val ensure_smallvalue_datatype: Datatype.config -> string list -> theory -> theory
   val compile_generator_expr:
     Proof.context -> term -> int -> term list option * (bool list * bool)
   val put_counterexample: (unit -> int -> term list option)
@@ -51,10 +50,12 @@
 
 (** abstract syntax **)
 
+fun termifyT T = HOLogic.mk_prodT (T, @{typ "unit => Code_Evaluation.term"});
+
 val size = @{term "i :: code_numeral"}
 val size_pred = @{term "(i :: code_numeral) - 1"}
 val size_ge_zero = @{term "(i :: code_numeral) > 0"}
-fun test_function T = Free ("f", T --> @{typ "term list option"})
+fun test_function T = Free ("f", termifyT T --> @{typ "term list option"})
 
 fun mk_none_continuation (x, y) =
   let
@@ -75,16 +76,23 @@
 fun smallT T = (T --> @{typ "Code_Evaluation.term list option"}) --> @{typ code_numeral}
   --> @{typ "Code_Evaluation.term list option"}
 
+val full_smallN = "full_small";
+
+fun full_smallT T = (termifyT T --> @{typ "Code_Evaluation.term list option"})
+  --> @{typ code_numeral} --> @{typ "Code_Evaluation.term list option"}
+ 
 fun mk_equations thy descr vs tycos (names, auxnames) (Ts, Us) =
   let
-    val smallsN = map (prefix (smallN ^ "_")) (names @ auxnames);
-    val smalls = map2 (fn name => fn T => Free (name, smallT T))
+    val smallsN = map (prefix (full_smallN ^ "_")) (names @ auxnames);
+    val smalls = map2 (fn name => fn T => Free (name, full_smallT T))
       smallsN (Ts @ Us)
     fun mk_small_call T =
       let
-        val small = Const (@{const_name "Smallcheck.small_class.small"}, smallT T)        
+        val small = Const (@{const_name "Smallcheck.full_small_class.full_small"}, full_smallT T)        
       in
-        (T, (fn t => small $ absdummy (T, t) $ size_pred))
+        (T, (fn t => small $
+          (HOLogic.split_const (T, @{typ "unit => Code_Evaluation.term"}, @{typ "Code_Evaluation.term list option"})
+          $ absdummy (T, absdummy (@{typ "unit => Code_Evaluation.term"}, t))) $ size_pred))
       end
     fun mk_small_aux_call fTs (k, _) (tyco, Ts) =
       let
@@ -92,14 +100,23 @@
         val _ = if not (null fTs) then raise FUNCTION_TYPE else ()
         val small = nth smalls k
       in
-        (T, (fn t => small $ absdummy (T, t) $ size_pred))
+       (T, (fn t => small $
+          (HOLogic.split_const (T, @{typ "unit => Code_Evaluation.term"}, @{typ "Code_Evaluation.term list option"})
+            $ absdummy (T, absdummy (@{typ "unit => Code_Evaluation.term"}, t))) $ size_pred))  
       end
     fun mk_consexpr simpleT (c, xs) =
       let
         val (Ts, fns) = split_list xs
         val constr = Const (c, Ts ---> simpleT)
-        val bounds = map Bound (((length xs) - 1) downto 0)
-        val start_term = test_function simpleT $ (list_comb (constr, bounds))
+        val bounds = map (fn x => Bound (2 * x + 1)) (((length xs) - 1) downto 0)
+        val term_bounds = map (fn x => Bound (2 * x)) (((length xs) - 1) downto 0)
+        val Eval_App = Const ("Code_Evaluation.App", HOLogic.termT --> HOLogic.termT --> HOLogic.termT)
+        val Eval_Const = Const ("Code_Evaluation.Const", HOLogic.literalT --> @{typ typerep} --> HOLogic.termT)
+        val term = fold (fn u => fn t => Eval_App $ t $ (u $ @{term "()"}))
+          bounds (Eval_Const $ HOLogic.mk_literal c $ HOLogic.mk_typerep (Ts ---> simpleT))
+        val start_term = test_function simpleT $ 
+        (HOLogic.pair_const simpleT @{typ "unit => Code_Evaluation.term"}
+          $ (list_comb (constr, bounds)) $ absdummy (@{typ unit}, term))
       in fold_rev (fn f => fn t => f t) fns start_term end
     fun mk_rhs exprs =
         @{term "If :: bool => term list option => term list option => term list option"}
@@ -129,7 +146,7 @@
         PRIMITIVE (Drule.cterm_instantiate [(cert (Var v), rel')]) st'
       end
   | _ => Seq.empty;
-
+  
 fun instantiate_smallvalue_datatype config descr vs tycos prfx (names, auxnames) (Ts, Us) thy =
   let
     val _ = Datatype_Aux.message config "Creating smallvalue generators ...";
@@ -155,45 +172,22 @@
       Pat_Completeness.pat_completeness_tac ctxt 1
       THEN auto_tac (clasimpset_of ctxt)
   in
-    thy
-    |> Class.instantiation (tycos, vs, @{sort small})
+    (thy
+    |> Class.instantiation (tycos, vs, @{sort full_small})
     |> Function.add_function
       (map (fn (T, (name, _)) =>
-          Syntax.no_syn (Binding.conceal (Binding.name name), SOME (smallT T))) eqs)
+          Syntax.no_syn (Binding.conceal (Binding.name name), SOME (full_smallT T))) eqs)
         (map (pair (apfst Binding.conceal Attrib.empty_binding) o snd o snd) eqs)
         Function_Common.default_config pat_completeness_auto
     |> snd
     |> Local_Theory.restore
     |> (fn lthy => Function.prove_termination NONE (termination_tac lthy) lthy)
     |> snd
-    |> Class.prove_instantiation_exit (K (Class.intro_classes_tac []))
-  end;
-
-fun ensure_smallvalue_datatype config raw_tycos thy =
-  let
-    val algebra = Sign.classes_of thy;
-    val (descr, raw_vs, tycos, prfx, (names, auxnames), raw_TUs) =
-      Datatype.the_descr thy raw_tycos;
-    val typerep_vs = (map o apsnd)
-      (curry (Sorts.inter_sort algebra) @{sort typerep}) raw_vs;
-    val smallvalue_insts = (map (rpair @{sort small}) o flat o maps snd o maps snd)
-      (Datatype_Aux.interpret_construction descr typerep_vs
-        { atyp = single, dtyp = (K o K o K) [] });
-    (*val term_of_insts = (map (rpair @{sort term_of}) o flat o maps snd o maps snd)
-      (Datatype_Aux.interpret_construction descr typerep_vs
-        { atyp = K [], dtyp = K o K });*)
-    val has_inst = exists (fn tyco =>
-      can (Sorts.mg_domain algebra tyco) @{sort small}) tycos;
-  in if has_inst then thy
-    else case Quickcheck_Generators.perhaps_constrain thy smallvalue_insts typerep_vs
-     of SOME constrain => (instantiate_smallvalue_datatype config descr
-          (map constrain typerep_vs) tycos prfx (names, auxnames)
-            ((pairself o map o map_atyps) (fn TFree v => TFree (constrain v)) raw_TUs) thy
-            handle FUNCTION_TYPE =>
-              (Datatype_Aux.message config
-                "Creation of smallvalue generators failed because the datatype contains a function type";
-              thy))
-      | NONE => thy
+    |> Class.prove_instantiation_exit (K (Class.intro_classes_tac [])))
+    handle FUNCTION_TYPE =>
+    (Datatype_Aux.message config
+      "Creation of smallvalue generators failed because the datatype contains a function type";
+    thy)
   end;
 
 (** building and compiling generator expressions **)
@@ -209,19 +203,20 @@
 fun mk_generator_expr thy prop Ts =
   let
     val bound_max = length Ts - 1;
-    val bounds = map Bound (bound_max downto 0)
-    val result = list_comb (prop, bounds);
-    val terms = HOLogic.mk_list @{typ term} (map2 HOLogic.mk_term_of Ts bounds);
+    val bounds = map_index (fn (i, ty) =>
+      (2 * (bound_max - i) + 1, 2 * (bound_max - i), 2 * i, ty)) Ts;
+    val result = list_comb (prop, map (fn (i, _, _, _) => Bound i) bounds);
+    val terms = HOLogic.mk_list @{typ term} (map (fn (_, i, _, _) => Bound i $ @{term "()"}) bounds);
     val check =
       @{term "Smallcheck.catch_match :: term list option => term list option => term list option"} $
         (@{term "If :: bool => term list option => term list option => term list option"}
-        $ result $ @{term "None :: term list option"}
-        $ (@{term "Some :: term list => term list option"} $ terms))
+        $ result $ @{term "None :: term list option"} $ (@{term "Some :: term list => term list option"} $ terms))
       $ @{term "None :: term list option"};
-    fun mk_small_closure (depth, T) t =
-      Const (@{const_name "Smallcheck.small_class.small"}, smallT T)
-        $ absdummy (T, t) $ depth
-  in Abs ("d", @{typ code_numeral}, fold_rev mk_small_closure (rev bounds ~~ Ts) check) end
+    fun mk_small_closure (_, _, i, T) t =
+      Const (@{const_name "Smallcheck.full_small_class.full_small"}, full_smallT T)
+        $ (HOLogic.split_const (T, @{typ "unit => term"}, @{typ "term list option"}) 
+        $ absdummy (T, absdummy (@{typ "unit => term"}, t))) $ Bound i
+  in Abs ("d", @{typ code_numeral}, fold_rev mk_small_closure bounds check) end
 
 fun compile_generator_expr ctxt t =
   let
@@ -242,7 +237,8 @@
 (** setup **)
 
 val setup =
-  Datatype.interpretation ensure_smallvalue_datatype
+  Datatype.interpretation
+    (Quickcheck_Generators.ensure_sort_datatype (@{sort full_small}, instantiate_smallvalue_datatype))
   #> Context.theory_map
     (Quickcheck.add_generator ("small", compile_generator_expr));