# HG changeset patch # User bulwahn # Date 1299853273 -3600 # Node ID 8759e9d043f9582f7896a3c3b4a209d503ba186d # Parent b09a67a3dc1e1ea1ab080d30c08cfac86bb5f8ba adding file quickcheck_common to carry common functions of all quickcheck generators diff -r b09a67a3dc1e -r 8759e9d043f9 src/HOL/IsaMakefile --- 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 \ diff -r b09a67a3dc1e -r 8759e9d043f9 src/HOL/Tools/Quickcheck/quickcheck_common.ML --- /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; diff -r b09a67a3dc1e -r 8759e9d043f9 src/HOL/Tools/Quickcheck/random_generators.ML --- 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 *)