--- 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
--- 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