adding creation of exhaustive generators for records; simplifying dependencies in Main theory

--- a/src/HOL/Main.thy	Thu May 05 10:24:12 2011 +0200
+++ b/src/HOL/Main.thy	Thu May 05 10:47:31 2011 +0200
@@ -1,7 +1,7 @@
 header {* Main HOL *}
 
 theory Main
-imports Plain Record Predicate_Compile Quickcheck_Exhaustive Nitpick
+imports Plain Predicate_Compile Nitpick
 begin
 
 text {*

--- a/src/HOL/Record.thy	Thu May 05 10:24:12 2011 +0200
+++ b/src/HOL/Record.thy	Thu May 05 10:47:31 2011 +0200
@@ -9,7 +9,7 @@
 header {* Extensible records with structural subtyping *}
 
 theory Record
-imports Plain Quickcheck
+imports Plain Quickcheck_Exhaustive
 uses ("Tools/record.ML")
 begin
 

--- a/src/HOL/Tools/record.ML	Thu May 05 10:24:12 2011 +0200
+++ b/src/HOL/Tools/record.ML	Thu May 05 10:47:31 2011 +0200
@@ -1795,7 +1795,7 @@
 
 (* code generation *)
 
-fun instantiate_random_record tyco vs extN Ts thy =
+fun mk_random_eq tyco vs extN Ts =
   let
     val size = @{term "i::code_numeral"};
     fun termifyT T = HOLogic.mk_prodT (T, @{typ "unit => term"});
@@ -1810,26 +1810,52 @@
         (map (fn (v, T') =>
           ((HOLogic.mk_random T' size, @{typ Random.seed}), SOME (v, termifyT T'))) params)
         tc @{typ Random.seed} (SOME Tm, @{typ Random.seed});
-    val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs));
+  in
+    (lhs, rhs)
+  end
+
+fun mk_full_exhaustive_eq tyco vs extN Ts =
+  let
+    val size = @{term "i::code_numeral"};
+    fun termifyT T = HOLogic.mk_prodT (T, @{typ "unit => term"});
+    val T = Type (tyco, map TFree vs);
+    val test_function = Free ("f", termifyT T --> @{typ "term list option"});
+    val params = Name.names Name.context "x" Ts;
+    fun full_exhaustiveT T = (termifyT T --> @{typ "Code_Evaluation.term list option"})
+      --> @{typ code_numeral} --> @{typ "Code_Evaluation.term list option"}
+    fun mk_full_exhaustive T =
+      Const (@{const_name "Quickcheck_Exhaustive.full_exhaustive_class.full_exhaustive"},
+        full_exhaustiveT T)
+    val lhs = mk_full_exhaustive T $ test_function $ size;
+    val tc = test_function $ (HOLogic.mk_valtermify_app extN params T);
+    val rhs = fold_rev (fn (v, T) => fn cont =>
+        mk_full_exhaustive T $ (lambda (Free (v, termifyT T)) cont) $ size) params tc
+  in
+    (lhs, rhs)
+  end
+
+fun instantiate_sort_record (sort, mk_eq) tyco vs extN Ts thy =
+  let
+    val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (mk_eq tyco vs extN Ts));
   in
     thy
-    |> Class.instantiation ([tyco], vs, @{sort random})
+    |> Class.instantiation ([tyco], vs, sort)
     |> `(fn lthy => Syntax.check_term lthy eq)
     |-> (fn eq => Specification.definition (NONE, (apfst Binding.conceal Attrib.empty_binding, eq)))
     |> snd
     |> Class.prove_instantiation_exit (K (Class.intro_classes_tac []))
-  end;
-
-fun ensure_random_record ext_tyco vs extN Ts thy =
+  end
+
+fun ensure_sort_record (sort, mk_eq) ext_tyco vs extN Ts thy =
   let
     val algebra = Sign.classes_of thy;
-    val has_inst = can (Sorts.mg_domain algebra ext_tyco) @{sort random};
+    val has_inst = can (Sorts.mg_domain algebra ext_tyco) sort;
   in
     if has_inst then thy
     else
-      (case Quickcheck_Common.perhaps_constrain thy (map (rpair @{sort random}) Ts) vs of
+      (case Quickcheck_Common.perhaps_constrain thy (map (rpair sort) Ts) vs of
         SOME constrain =>
-          instantiate_random_record ext_tyco (map constrain vs) extN
+          instantiate_sort_record (sort, mk_eq) ext_tyco (map constrain vs) extN
             ((map o map_atyps) (fn TFree v => TFree (constrain v)) Ts) thy
       | NONE => thy)
   end;
@@ -1851,6 +1877,8 @@
       |> Thm.instantiate
         ([pairself (ctyp_of thy) (TVar (("'a", 0), @{sort equal}), Logic.varifyT_global extT)], [])
       |> AxClass.unoverload thy;
+    val ensure_random_record = ensure_sort_record (@{sort random}, mk_random_eq)
+    val ensure_exhaustive_record = ensure_sort_record (@{sort full_exhaustive}, mk_full_exhaustive_eq)
   in
     thy
     |> Code.add_datatype [ext]
@@ -1866,6 +1894,7 @@
           thy |> Code.del_eqn eq_def |> Code.add_default_eqn (mk_eq thy eq_def))
     |> (fn thy => Code.add_nbe_default_eqn (mk_eq_refl thy) thy)
     |> ensure_random_record ext_tyco vs (fst ext) (binder_types (snd ext))
+    |> ensure_exhaustive_record ext_tyco vs (fst ext) (binder_types (snd ext))
   end;