# HG changeset patch # User bulwahn # Date 1301921051 -7200 # Node ID 9ca13615c619999ac4aad8b9e9fe61e88d8a0a26 # Parent bac7733a13c909648ea1e70b79074057ff96b34b refactoring generator definition in quickcheck and removing clone diff -r bac7733a13c9 -r 9ca13615c619 src/HOL/Tools/Quickcheck/exhaustive_generators.ML --- a/src/HOL/Tools/Quickcheck/exhaustive_generators.ML Mon Apr 04 14:37:20 2011 +0200 +++ b/src/HOL/Tools/Quickcheck/exhaustive_generators.ML Mon Apr 04 14:44:11 2011 +0200 @@ -23,10 +23,6 @@ structure Exhaustive_Generators : EXHAUSTIVE_GENERATORS = struct -(* static options *) - -val define_foundationally = false - (* dynamic options *) val (smart_quantifier, setup_smart_quantifier) = @@ -71,8 +67,7 @@ let val (T as Type(@{type_name "option"}, [T'])) = fastype_of x in - Const (@{const_name "Quickcheck_Exhaustive.orelse"}, T --> T --> T) - $ x $ y + Const (@{const_name "Quickcheck_Exhaustive.orelse"}, T --> T --> T) $ x $ y end (** datatypes **) @@ -157,11 +152,6 @@ (HOL_basic_ss addsimps [@{thm in_measure}, @{thm o_def}, @{thm snd_conv}, @{thm nat_mono_iff}, less_int_pred] @ @{thms sum.cases}) 1)) -fun pat_completeness_auto ctxt = - Pat_Completeness.pat_completeness_tac ctxt 1 - THEN auto_tac (clasimpset_of ctxt) - - (* creating the instances *) fun instantiate_exhaustive_datatype config descr vs tycos prfx (names, auxnames) (Ts, Us) thy = @@ -171,39 +161,9 @@ in thy |> Class.instantiation (tycos, vs, @{sort exhaustive}) - |> (if define_foundationally then - let - val exhaustives = map2 (fn name => fn T => Free (name, exhaustiveT T)) exhaustivesN (Ts @ Us) - val eqs = mk_equations descr vs tycos exhaustives (Ts, Us) - in - Function.add_function - (map (fn (name, T) => - Syntax.no_syn (Binding.conceal (Binding.name name), SOME (exhaustiveT T))) - (exhaustivesN ~~ (Ts @ Us))) - (map (pair (apfst Binding.conceal Attrib.empty_binding)) eqs) - Function_Common.default_config pat_completeness_auto - #> snd - #> Local_Theory.restore - #> (fn lthy => Function.prove_termination NONE (termination_tac lthy) lthy) - #> snd - end - else - fold_map (fn (name, T) => Local_Theory.define - ((Binding.conceal (Binding.name name), NoSyn), - (apfst Binding.conceal Attrib.empty_binding, mk_undefined (exhaustiveT T))) - #> apfst fst) (exhaustivesN ~~ (Ts @ Us)) - #> (fn (exhaustives, lthy) => - let - val eqs_t = mk_equations descr vs tycos exhaustives (Ts, Us) - val eqs = map (fn eq => Goal.prove lthy ["f", "i"] [] eq - (fn _ => Skip_Proof.cheat_tac (ProofContext.theory_of lthy))) eqs_t - in - fold (fn (name, eq) => Local_Theory.note - ((Binding.conceal (Binding.qualify true prfx - (Binding.qualify true name (Binding.name "simps"))), - Code.add_default_eqn_attrib :: map (Attrib.internal o K) - [Simplifier.simp_add, Nitpick_Simps.add]), [eq]) #> snd) (exhaustivesN ~~ eqs) lthy - end)) + |> Quickcheck_Common.define_functions + (fn exhaustives => mk_equations descr vs tycos exhaustives (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 diff -r bac7733a13c9 -r 9ca13615c619 src/HOL/Tools/Quickcheck/narrowing_generators.ML --- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML Mon Apr 04 14:37:20 2011 +0200 +++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML Mon Apr 04 14:44:11 2011 +0200 @@ -21,9 +21,6 @@ val (finite_functions, setup_finite_functions) = Attrib.config_bool "quickcheck_finite_functions" (K true) - -fun mk_undefined T = Const(@{const_name undefined}, T) - (* narrowing specific names and types *) exception FUNCTION_TYPE; @@ -57,12 +54,7 @@ fun mk_equations descr vs tycos narrowings (Ts, Us) = let fun mk_call T = - let - val narrowing = - Const (@{const_name "Quickcheck_Narrowing.narrowing_class.narrowing"}, narrowingT T) - in - (T, narrowing) - end + (T, Const (@{const_name "Quickcheck_Narrowing.narrowing_class.narrowing"}, narrowingT T)) fun mk_aux_call fTs (k, _) (tyco, Ts) = let val T = Type (tyco, Ts) @@ -86,8 +78,7 @@ in eqs end - - + fun instantiate_narrowing_datatype config descr vs tycos prfx (names, auxnames) (Ts, Us) thy = let val _ = Datatype_Aux.message config "Creating narrowing generators ..."; @@ -95,22 +86,9 @@ in thy |> Class.instantiation (tycos, vs, @{sort narrowing}) - |> (fold_map (fn (name, T) => Local_Theory.define - ((Binding.conceal (Binding.name name), NoSyn), - (apfst Binding.conceal Attrib.empty_binding, mk_undefined (narrowingT T))) - #> apfst fst) (narrowingsN ~~ (Ts @ Us)) - #> (fn (narrowings, lthy) => - let - val eqs_t = mk_equations descr vs tycos narrowings (Ts, Us) - val eqs = map (fn eq => Goal.prove lthy ["f", "i"] [] eq - (fn _ => Skip_Proof.cheat_tac (ProofContext.theory_of lthy))) eqs_t - in - fold (fn (name, eq) => Local_Theory.note - ((Binding.conceal (Binding.qualify true prfx - (Binding.qualify true name (Binding.name "simps"))), - Code.add_default_eqn_attrib :: map (Attrib.internal o K) - [Simplifier.simp_add, Nitpick_Simps.add]), [eq]) #> snd) (narrowingsN ~~ eqs) lthy - end)) + |> Quickcheck_Common.define_functions + (fn narrowings => mk_equations descr vs tycos narrowings (Ts, Us), NONE) + prfx [] narrowingsN (map narrowingT (Ts @ Us)) |> Class.prove_instantiation_exit (K (Class.intro_classes_tac [])) end; diff -r bac7733a13c9 -r 9ca13615c619 src/HOL/Tools/Quickcheck/quickcheck_common.ML --- a/src/HOL/Tools/Quickcheck/quickcheck_common.ML Mon Apr 04 14:37:20 2011 +0200 +++ b/src/HOL/Tools/Quickcheck/quickcheck_common.ML Mon Apr 04 14:44:11 2011 +0200 @@ -7,6 +7,8 @@ signature QUICKCHECK_COMMON = sig val strip_imp : term -> (term list * term) + val define_functions : ((term list -> term list) * (Proof.context -> tactic) option) + -> string -> string list -> string list -> typ list -> Proof.context -> Proof.context val perhaps_constrain: theory -> (typ * sort) list -> (string * sort) list -> (string * sort -> string * sort) option val ensure_sort_datatype: @@ -21,11 +23,57 @@ structure Quickcheck_Common : QUICKCHECK_COMMON = struct +(* static options *) + +val define_foundationally = false + (* HOLogic's term functions *) fun strip_imp (Const(@{const_name HOL.implies},_) $ A $ B) = apfst (cons A) (strip_imp B) | strip_imp A = ([], A) +fun mk_undefined T = Const(@{const_name undefined}, T) + +(* defining functions *) + +fun pat_completeness_auto ctxt = + Pat_Completeness.pat_completeness_tac ctxt 1 + THEN auto_tac (clasimpset_of ctxt) + +fun define_functions (mk_equations, termination_tac) prfx argnames names Ts = + if define_foundationally andalso is_some termination_tac then + let + val eqs_t = mk_equations (map2 (fn name => fn T => Free (name, T)) names Ts) + in + Function.add_function + (map (fn (name, T) => + Syntax.no_syn (Binding.conceal (Binding.name name), SOME T)) + (names ~~ Ts)) + (map (pair (apfst Binding.conceal Attrib.empty_binding)) eqs_t) + Function_Common.default_config pat_completeness_auto + #> snd + #> Local_Theory.restore + #> (fn lthy => Function.prove_termination NONE (the termination_tac lthy) lthy) + #> snd + end + else + fold_map (fn (name, T) => Local_Theory.define + ((Binding.conceal (Binding.name name), NoSyn), + (apfst Binding.conceal Attrib.empty_binding, mk_undefined T)) + #> apfst fst) (names ~~ Ts) + #> (fn (consts, lthy) => + let + val eqs_t = mk_equations consts + val eqs = map (fn eq => Goal.prove lthy argnames [] eq + (fn _ => Skip_Proof.cheat_tac (ProofContext.theory_of lthy))) eqs_t + in + fold (fn (name, eq) => Local_Theory.note + ((Binding.conceal (Binding.qualify true prfx + (Binding.qualify true name (Binding.name "simps"))), + Code.add_default_eqn_attrib :: map (Attrib.internal o K) + [Simplifier.simp_add, Nitpick_Simps.add]), [eq]) #> snd) (names ~~ eqs) lthy + end) + (** ensuring sort constraints **) fun perhaps_constrain thy insts raw_vs =