adding file quickcheck_common to carry common functions of all quickcheck generators
--- a/src/HOL/IsaMakefile Fri Mar 11 15:21:13 2011 +0100
+++ b/src/HOL/IsaMakefile Fri Mar 11 15:21:13 2011 +0100
@@ -469,8 +469,9 @@
Library/While_Combinator.thy Library/Zorn.thy \
$(SRC)/Tools/adhoc_overloading.ML Library/positivstellensatz.ML \
Library/reflection.ML Library/reify_data.ML \
- Library/LSC.thy $(SRC)/HOL/Tools/LSC/lazysmallcheck.ML \
- $(SRC)/HOL/Tools/LSC/LazySmallCheck.hs \
+ Library/Quickcheck_Narrowing.thy \
+ Tools/Quickcheck/narrowing_generators.ML \
+ Tools/Quickcheck/Narrowing_Engine.hs \
Library/document/root.bib Library/document/root.tex
@cd Library; $(ISABELLE_TOOL) usedir -b $(OUT)/HOL HOL-Library
@@ -617,7 +618,7 @@
Number_Theory/UniqueFactorization.thy \
Number_Theory/ROOT.ML
@$(ISABELLE_TOOL) usedir -g true $(OUT)/HOL Number_Theory
-
+
## HOL-Old_Number_Theory
@@ -1039,11 +1040,11 @@
ex/InductiveInvariant.thy ex/InductiveInvariant_examples.thy \
ex/Interpretation_with_Defs.thy ex/Intuitionistic.thy ex/Lagrange.thy \
ex/List_to_Set_Comprehension_Examples.thy ex/LocaleTest2.thy \
- ex/LSC_Examples.thy \
ex/MT.thy ex/MergeSort.thy ex/Meson_Test.thy ex/MonoidGroup.thy \
ex/Multiquote.thy ex/NatSum.thy ex/Normalization_by_Evaluation.thy \
ex/Numeral.thy ex/PER.thy ex/PresburgerEx.thy ex/Primrec.thy \
ex/Quickcheck_Examples.thy ex/Quickcheck_Lattice_Examples.thy \
+ ex/Quickcheck_Narrowing_Examples.thy \
ex/Quicksort.thy ex/ROOT.ML ex/Recdefs.thy ex/Records.thy \
ex/ReflectionEx.thy ex/Refute_Examples.thy ex/SAT_Examples.thy \
ex/SVC_Oracle.thy ex/Serbian.thy ex/Set_Algebras.thy ex/Sqrt.thy \
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/Quickcheck/quickcheck_common.ML Fri Mar 11 15:21:13 2011 +0100
@@ -0,0 +1,54 @@
+(* Title: HOL/Tools/Quickcheck/quickcheck_common.ML
+ Author: Florian Haftmann, Lukas Bulwahn, TU Muenchen
+
+Common functions for quickcheck's generators
+
+*)
+
+signature QUICKCHECK_COMMON =
+sig
+ val perhaps_constrain: theory -> (typ * sort) list -> (string * sort) list
+ -> (string * sort -> string * sort) option
+ val ensure_sort_datatype:
+ sort * (Datatype.config -> Datatype.descr -> (string * sort) list -> string list -> string ->
+ string list * string list -> typ list * typ list -> theory -> theory)
+ -> Datatype.config -> string list -> theory -> theory
+end;
+
+structure Quickcheck_Common : QUICKCHECK_COMMON =
+struct
+
+fun perhaps_constrain thy insts raw_vs =
+ let
+ fun meet (T, sort) = Sorts.meet_sort (Sign.classes_of thy)
+ (Logic.varifyT_global T, sort);
+ val vtab = Vartab.empty
+ |> fold (fn (v, sort) => Vartab.update ((v, 0), sort)) raw_vs
+ |> fold meet insts;
+ in SOME (fn (v, _) => (v, (the o Vartab.lookup vtab) (v, 0)))
+ end handle Sorts.CLASS_ERROR _ => NONE;
+
+fun ensure_sort_datatype (sort, instantiate_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 sort_insts = (map (rpair sort) 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) tycos;
+ in if has_inst then thy
+ else case perhaps_constrain thy (sort_insts @ term_of_insts) typerep_vs
+ of SOME constrain => instantiate_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
+ | NONE => thy
+ end;
+
+end;
--- a/src/HOL/Tools/Quickcheck/random_generators.ML Fri Mar 11 15:21:13 2011 +0100
+++ b/src/HOL/Tools/Quickcheck/random_generators.ML Fri Mar 11 15:21:13 2011 +0100
@@ -10,12 +10,6 @@
val random_fun: typ -> typ -> ('a -> 'a -> bool) -> ('a -> term)
-> (seed -> ('b * (unit -> term)) * seed) -> (seed -> seed * seed)
-> seed -> (('a -> 'b) * (unit -> term)) * seed
- val perhaps_constrain: theory -> (typ * sort) list -> (string * sort) list
- -> (string * sort -> string * sort) option
- val ensure_sort_datatype:
- sort * (Datatype.config -> Datatype.descr -> (string * sort) list -> string list -> string ->
- string list * string list -> typ list * typ list -> theory -> theory)
- -> Datatype.config -> string list -> theory -> theory
val compile_generator_expr:
Proof.context -> term -> int -> term list option * Quickcheck.report option
val put_counterexample: (unit -> int -> seed -> term list option * seed)
@@ -272,39 +266,6 @@
|> Class.prove_instantiation_exit (K (Class.intro_classes_tac []))
end;
-fun perhaps_constrain thy insts raw_vs =
- let
- fun meet (T, sort) = Sorts.meet_sort (Sign.classes_of thy)
- (Logic.varifyT_global T, sort);
- val vtab = Vartab.empty
- |> fold (fn (v, sort) => Vartab.update ((v, 0), sort)) raw_vs
- |> fold meet insts;
- in SOME (fn (v, _) => (v, (the o Vartab.lookup vtab) (v, 0)))
- end handle Sorts.CLASS_ERROR _ => NONE;
-
-fun ensure_sort_datatype (sort, instantiate_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 sort_insts = (map (rpair sort) 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) tycos;
- in if has_inst then thy
- else case perhaps_constrain thy (sort_insts @ term_of_insts) typerep_vs
- of SOME constrain => instantiate_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
- | NONE => thy
- end;
-
(** building and compiling generator expressions **)
(* FIXME just one data slot (record) per program unit *)