# HG changeset patch
# User bulwahn
# Date 1302273074 -7200
# Node ID c664cc5cc5e934a0e96cb646e676107c3e67c9c9
# Parent  74ea14d13247b66cb7d95f238ecb4bcdb23592d7
splitting exhaustive and full_exhaustive into separate type classes

diff -r 74ea14d13247 -r c664cc5cc5e9 src/HOL/Quickcheck_Exhaustive.thy
--- a/src/HOL/Quickcheck_Exhaustive.thy	Fri Apr 08 16:31:14 2011 +0200
+++ b/src/HOL/Quickcheck_Exhaustive.thy	Fri Apr 08 16:31:14 2011 +0200
@@ -17,9 +17,11 @@
 
 class exhaustive = term_of +
   fixes exhaustive :: "('a \<Rightarrow> term list option) \<Rightarrow> code_numeral \<Rightarrow> term list option"
+  
+class full_exhaustive = term_of +
   fixes full_exhaustive :: "('a * (unit => term) \<Rightarrow> term list option) \<Rightarrow> code_numeral \<Rightarrow> term list option"
 
-instantiation code_numeral :: exhaustive
+instantiation code_numeral :: full_exhaustive
 begin
 
 function full_exhaustive_code_numeral' :: "(code_numeral * (unit => term) => term list option) => code_numeral => code_numeral => term list option"
@@ -33,6 +35,13 @@
 
 definition "full_exhaustive f d = full_exhaustive_code_numeral' f d 0"
 
+instance ..
+
+end
+
+instantiation code_numeral :: exhaustive
+begin
+
 function exhaustive_code_numeral' :: "(code_numeral => term list option) => code_numeral => code_numeral => term list option"
   where "exhaustive_code_numeral' f d i =
     (if d < i then None
@@ -44,7 +53,6 @@
 
 definition "exhaustive f d = exhaustive_code_numeral' f d 0"
 
-
 instance ..
 
 end
@@ -54,6 +62,13 @@
 
 definition "exhaustive f d = exhaustive (%x. f (Code_Numeral.nat_of x)) d"
 
+instance ..
+
+end
+
+instantiation nat :: full_exhaustive
+begin
+
 definition "full_exhaustive f d = full_exhaustive (%(x, xt). f (Code_Numeral.nat_of x, %_. Code_Evaluation.term_of (Code_Numeral.nat_of x))) d"
 
 instance ..
@@ -72,6 +87,13 @@
 
 definition "exhaustive f d = exhaustive' f (Code_Numeral.int_of d) (- (Code_Numeral.int_of d))"
 
+instance ..
+
+end
+
+instantiation int :: full_exhaustive
+begin
+
 function full_exhaustive' :: "(int * (unit => term) => term list option) => int => int => term list option"
   where "full_exhaustive' f d i = (if d < i then None else (case f (i, %_. Code_Evaluation.term_of i) of Some t => Some t | None => full_exhaustive' f d (i + 1)))"
 by pat_completeness auto
@@ -91,6 +113,13 @@
 definition
   "exhaustive f d = exhaustive (%x. exhaustive (%y. f ((x, y))) d) d"
 
+instance ..
+
+end
+
+instantiation prod :: (full_exhaustive, full_exhaustive) full_exhaustive
+begin
+
 definition
   "full_exhaustive f d = full_exhaustive (%(x, t1). full_exhaustive (%(y, t2). f ((x, y),
     %u. let T1 = (Typerep.typerep (TYPE('a)));
@@ -118,6 +147,12 @@
 where
   "exhaustive_fun f d = exhaustive_fun' f d d" 
 
+instance ..
+
+end
+
+instantiation "fun" :: ("{equal, full_exhaustive}", full_exhaustive) full_exhaustive
+begin
 
 fun full_exhaustive_fun' :: "(('a => 'b) * (unit => term) => term list option) => code_numeral => code_numeral => term list option"
 where
diff -r 74ea14d13247 -r c664cc5cc5e9 src/HOL/Tools/Quickcheck/exhaustive_generators.ML
--- a/src/HOL/Tools/Quickcheck/exhaustive_generators.ML	Fri Apr 08 16:31:14 2011 +0200
+++ b/src/HOL/Tools/Quickcheck/exhaustive_generators.ML	Fri Apr 08 16:31:14 2011 +0200
@@ -187,7 +187,7 @@
     fun mk_call T =
       let
         val full_exhaustive =
-          Const (@{const_name "Quickcheck_Exhaustive.exhaustive_class.full_exhaustive"},
+          Const (@{const_name "Quickcheck_Exhaustive.full_exhaustive_class.full_exhaustive"},
             full_exhaustiveT T)
       in
         (T, (fn t => full_exhaustive $
@@ -251,13 +251,26 @@
   let
     val _ = Datatype_Aux.message config "Creating exhaustive generators...";
     val exhaustivesN = map (prefix (exhaustiveN ^ "_")) (names @ auxnames)
-    val full_exhaustivesN = map (prefix (full_exhaustiveN ^ "_")) (names @ auxnames)
   in
     thy
     |> Class.instantiation (tycos, vs, @{sort exhaustive})
     |> Quickcheck_Common.define_functions
         (fn functerms => mk_equations functerms (descr, vs, Ts @ Us), SOME termination_tac)
         prfx ["f", "i"] exhaustivesN (map exhaustiveT (Ts @ Us))
+    |> Class.prove_instantiation_exit (K (Class.intro_classes_tac []))
+  end handle FUNCTION_TYPE =>
+    (Datatype_Aux.message config
+      "Creation of exhaustive generators failed because the datatype contains a function type";
+    thy)
+
+
+fun instantiate_full_exhaustive_datatype config descr vs tycos prfx (names, auxnames) (Ts, Us) thy =
+  let
+    val _ = Datatype_Aux.message config "Creating exhaustive generators...";
+    val full_exhaustivesN = map (prefix (full_exhaustiveN ^ "_")) (names @ auxnames)
+  in
+    thy
+    |> Class.instantiation (tycos, vs, @{sort full_exhaustive})
     |> Quickcheck_Common.define_functions
         (fn functerms => mk_full_equations functerms (descr, vs, Ts @ Us), SOME termination_tac)
         prfx ["f", "i"] full_exhaustivesN (map full_exhaustiveT (Ts @ Us))
@@ -266,7 +279,7 @@
     (Datatype_Aux.message config
       "Creation of exhaustive generators failed because the datatype contains a function type";
     thy)
-
+     
 fun instantiate_fast_exhaustive_datatype config descr vs tycos prfx (names, auxnames) (Ts, Us) thy =
   let
     val _ = Datatype_Aux.message config "Creating fast exhaustive generators...";
@@ -549,9 +562,11 @@
   Datatype.interpretation (Quickcheck_Common.ensure_sort_datatype
       (((@{sort typerep}, @{sort term_of}), @{sort exhaustive}), instantiate_exhaustive_datatype))
   #> Datatype.interpretation (Quickcheck_Common.ensure_sort_datatype
-      (((@{sort type}, @{sort type}), @{sort bounded_forall}), instantiate_bounded_forall_datatype))
+      (((@{sort typerep}, @{sort term_of}), @{sort full_exhaustive}), instantiate_full_exhaustive_datatype))
   #> Datatype.interpretation (Quickcheck_Common.ensure_sort_datatype
       (((@{sort typerep}, @{sort term_of}), @{sort fast_exhaustive}), instantiate_fast_exhaustive_datatype))
+  #> Datatype.interpretation (Quickcheck_Common.ensure_sort_datatype
+      (((@{sort type}, @{sort type}), @{sort bounded_forall}), instantiate_bounded_forall_datatype))
   #> setup_smart_quantifier
   #> setup_full_support
   #> setup_fast