refactoring generator definition in quickcheck and removing clone
authorbulwahn
Mon Apr 04 14:44:11 2011 +0200 (2011-04-04)
changeset 422149ca13615c619
parent 42213 bac7733a13c9
child 42215 de9d43c427ae
refactoring generator definition in quickcheck and removing clone
src/HOL/Tools/Quickcheck/exhaustive_generators.ML
src/HOL/Tools/Quickcheck/narrowing_generators.ML
src/HOL/Tools/Quickcheck/quickcheck_common.ML
     1.1 --- a/src/HOL/Tools/Quickcheck/exhaustive_generators.ML	Mon Apr 04 14:37:20 2011 +0200
     1.2 +++ b/src/HOL/Tools/Quickcheck/exhaustive_generators.ML	Mon Apr 04 14:44:11 2011 +0200
     1.3 @@ -23,10 +23,6 @@
     1.4  structure Exhaustive_Generators : EXHAUSTIVE_GENERATORS =
     1.5  struct
     1.6  
     1.7 -(* static options *)
     1.8 -
     1.9 -val define_foundationally = false
    1.10 -
    1.11  (* dynamic options *)
    1.12  
    1.13  val (smart_quantifier, setup_smart_quantifier) =
    1.14 @@ -71,8 +67,7 @@
    1.15    let
    1.16      val (T as Type(@{type_name "option"}, [T'])) = fastype_of x
    1.17    in
    1.18 -    Const (@{const_name "Quickcheck_Exhaustive.orelse"}, T --> T --> T)
    1.19 -      $ x $ y
    1.20 +    Const (@{const_name "Quickcheck_Exhaustive.orelse"}, T --> T --> T) $ x $ y
    1.21    end
    1.22  
    1.23  (** datatypes **)
    1.24 @@ -157,11 +152,6 @@
    1.25      (HOL_basic_ss addsimps [@{thm in_measure}, @{thm o_def}, @{thm snd_conv},
    1.26       @{thm nat_mono_iff}, less_int_pred] @ @{thms sum.cases}) 1))
    1.27  
    1.28 -fun pat_completeness_auto ctxt =
    1.29 -  Pat_Completeness.pat_completeness_tac ctxt 1
    1.30 -  THEN auto_tac (clasimpset_of ctxt)    
    1.31 -
    1.32 -
    1.33  (* creating the instances *)
    1.34  
    1.35  fun instantiate_exhaustive_datatype config descr vs tycos prfx (names, auxnames) (Ts, Us) thy =
    1.36 @@ -171,39 +161,9 @@
    1.37    in
    1.38      thy
    1.39      |> Class.instantiation (tycos, vs, @{sort exhaustive})
    1.40 -    |> (if define_foundationally then
    1.41 -      let
    1.42 -        val exhaustives = map2 (fn name => fn T => Free (name, exhaustiveT T)) exhaustivesN (Ts @ Us)
    1.43 -        val eqs = mk_equations descr vs tycos exhaustives (Ts, Us)
    1.44 -      in
    1.45 -        Function.add_function
    1.46 -          (map (fn (name, T) =>
    1.47 -              Syntax.no_syn (Binding.conceal (Binding.name name), SOME (exhaustiveT T)))
    1.48 -                (exhaustivesN ~~ (Ts @ Us)))
    1.49 -            (map (pair (apfst Binding.conceal Attrib.empty_binding)) eqs)
    1.50 -          Function_Common.default_config pat_completeness_auto
    1.51 -        #> snd
    1.52 -        #> Local_Theory.restore
    1.53 -        #> (fn lthy => Function.prove_termination NONE (termination_tac lthy) lthy)
    1.54 -        #> snd
    1.55 -      end
    1.56 -    else
    1.57 -      fold_map (fn (name, T) => Local_Theory.define
    1.58 -          ((Binding.conceal (Binding.name name), NoSyn),
    1.59 -            (apfst Binding.conceal Attrib.empty_binding, mk_undefined (exhaustiveT T)))
    1.60 -        #> apfst fst) (exhaustivesN ~~ (Ts @ Us))
    1.61 -      #> (fn (exhaustives, lthy) =>
    1.62 -        let
    1.63 -          val eqs_t = mk_equations descr vs tycos exhaustives (Ts, Us)
    1.64 -          val eqs = map (fn eq => Goal.prove lthy ["f", "i"] [] eq
    1.65 -            (fn _ => Skip_Proof.cheat_tac (ProofContext.theory_of lthy))) eqs_t
    1.66 -        in
    1.67 -          fold (fn (name, eq) => Local_Theory.note
    1.68 -          ((Binding.conceal (Binding.qualify true prfx
    1.69 -             (Binding.qualify true name (Binding.name "simps"))),
    1.70 -             Code.add_default_eqn_attrib :: map (Attrib.internal o K)
    1.71 -               [Simplifier.simp_add, Nitpick_Simps.add]), [eq]) #> snd) (exhaustivesN ~~ eqs) lthy
    1.72 -        end))
    1.73 +    |> Quickcheck_Common.define_functions
    1.74 +        (fn exhaustives => mk_equations descr vs tycos exhaustives (Ts, Us), SOME termination_tac)
    1.75 +        prfx ["f", "i"] exhaustivesN (map exhaustiveT (Ts @ Us))
    1.76      |> Class.prove_instantiation_exit (K (Class.intro_classes_tac []))
    1.77    end handle FUNCTION_TYPE =>
    1.78      (Datatype_Aux.message config
     2.1 --- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Mon Apr 04 14:37:20 2011 +0200
     2.2 +++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Mon Apr 04 14:44:11 2011 +0200
     2.3 @@ -21,9 +21,6 @@
     2.4  val (finite_functions, setup_finite_functions) =
     2.5    Attrib.config_bool "quickcheck_finite_functions" (K true)
     2.6  
     2.7 -
     2.8 -fun mk_undefined T = Const(@{const_name undefined}, T)
     2.9 -
    2.10  (* narrowing specific names and types *)
    2.11  
    2.12  exception FUNCTION_TYPE;
    2.13 @@ -57,12 +54,7 @@
    2.14  fun mk_equations descr vs tycos narrowings (Ts, Us) =
    2.15    let
    2.16      fun mk_call T =
    2.17 -      let
    2.18 -        val narrowing =
    2.19 -          Const (@{const_name "Quickcheck_Narrowing.narrowing_class.narrowing"}, narrowingT T)
    2.20 -      in
    2.21 -        (T, narrowing)
    2.22 -      end
    2.23 +      (T, Const (@{const_name "Quickcheck_Narrowing.narrowing_class.narrowing"}, narrowingT T))
    2.24      fun mk_aux_call fTs (k, _) (tyco, Ts) =
    2.25        let
    2.26          val T = Type (tyco, Ts)
    2.27 @@ -86,8 +78,7 @@
    2.28    in
    2.29      eqs
    2.30    end
    2.31 -
    2.32 -
    2.33 +  
    2.34  fun instantiate_narrowing_datatype config descr vs tycos prfx (names, auxnames) (Ts, Us) thy =
    2.35    let
    2.36      val _ = Datatype_Aux.message config "Creating narrowing generators ...";
    2.37 @@ -95,22 +86,9 @@
    2.38    in
    2.39      thy
    2.40      |> Class.instantiation (tycos, vs, @{sort narrowing})
    2.41 -    |> (fold_map (fn (name, T) => Local_Theory.define
    2.42 -          ((Binding.conceal (Binding.name name), NoSyn),
    2.43 -            (apfst Binding.conceal Attrib.empty_binding, mk_undefined (narrowingT T)))
    2.44 -        #> apfst fst) (narrowingsN ~~ (Ts @ Us))
    2.45 -      #> (fn (narrowings, lthy) =>
    2.46 -        let
    2.47 -          val eqs_t = mk_equations descr vs tycos narrowings (Ts, Us)
    2.48 -          val eqs = map (fn eq => Goal.prove lthy ["f", "i"] [] eq
    2.49 -            (fn _ => Skip_Proof.cheat_tac (ProofContext.theory_of lthy))) eqs_t
    2.50 -        in
    2.51 -          fold (fn (name, eq) => Local_Theory.note
    2.52 -          ((Binding.conceal (Binding.qualify true prfx
    2.53 -             (Binding.qualify true name (Binding.name "simps"))),
    2.54 -             Code.add_default_eqn_attrib :: map (Attrib.internal o K)
    2.55 -               [Simplifier.simp_add, Nitpick_Simps.add]), [eq]) #> snd) (narrowingsN ~~ eqs) lthy
    2.56 -        end))
    2.57 +    |> Quickcheck_Common.define_functions
    2.58 +      (fn narrowings => mk_equations descr vs tycos narrowings (Ts, Us), NONE)
    2.59 +      prfx [] narrowingsN (map narrowingT (Ts @ Us))
    2.60      |> Class.prove_instantiation_exit (K (Class.intro_classes_tac []))
    2.61    end;
    2.62  
     3.1 --- a/src/HOL/Tools/Quickcheck/quickcheck_common.ML	Mon Apr 04 14:37:20 2011 +0200
     3.2 +++ b/src/HOL/Tools/Quickcheck/quickcheck_common.ML	Mon Apr 04 14:44:11 2011 +0200
     3.3 @@ -7,6 +7,8 @@
     3.4  signature QUICKCHECK_COMMON =
     3.5  sig
     3.6    val strip_imp : term -> (term list * term)
     3.7 +  val define_functions : ((term list -> term list) * (Proof.context -> tactic) option)
     3.8 +    -> string -> string list -> string list -> typ list -> Proof.context -> Proof.context 
     3.9    val perhaps_constrain: theory -> (typ * sort) list -> (string * sort) list
    3.10      -> (string * sort -> string * sort) option
    3.11    val ensure_sort_datatype:
    3.12 @@ -21,11 +23,57 @@
    3.13  structure Quickcheck_Common : QUICKCHECK_COMMON =
    3.14  struct
    3.15  
    3.16 +(* static options *)
    3.17 +
    3.18 +val define_foundationally = false
    3.19 +
    3.20  (* HOLogic's term functions *)
    3.21  
    3.22  fun strip_imp (Const(@{const_name HOL.implies},_) $ A $ B) = apfst (cons A) (strip_imp B)
    3.23    | strip_imp A = ([], A)
    3.24  
    3.25 +fun mk_undefined T = Const(@{const_name undefined}, T)
    3.26 +  
    3.27 +(* defining functions *)
    3.28 +
    3.29 +fun pat_completeness_auto ctxt =
    3.30 +  Pat_Completeness.pat_completeness_tac ctxt 1
    3.31 +  THEN auto_tac (clasimpset_of ctxt)    
    3.32 +
    3.33 +fun define_functions (mk_equations, termination_tac) prfx argnames names Ts =
    3.34 +  if define_foundationally andalso is_some termination_tac then
    3.35 +    let
    3.36 +      val eqs_t = mk_equations (map2 (fn name => fn T => Free (name, T)) names Ts)
    3.37 +    in
    3.38 +      Function.add_function
    3.39 +        (map (fn (name, T) =>
    3.40 +            Syntax.no_syn (Binding.conceal (Binding.name name), SOME T))
    3.41 +              (names ~~ Ts))
    3.42 +          (map (pair (apfst Binding.conceal Attrib.empty_binding)) eqs_t)
    3.43 +        Function_Common.default_config pat_completeness_auto
    3.44 +      #> snd
    3.45 +      #> Local_Theory.restore
    3.46 +      #> (fn lthy => Function.prove_termination NONE (the termination_tac lthy) lthy)
    3.47 +      #> snd
    3.48 +    end
    3.49 +  else
    3.50 +    fold_map (fn (name, T) => Local_Theory.define
    3.51 +        ((Binding.conceal (Binding.name name), NoSyn),
    3.52 +          (apfst Binding.conceal Attrib.empty_binding, mk_undefined T))
    3.53 +      #> apfst fst) (names ~~ Ts)
    3.54 +    #> (fn (consts, lthy) =>
    3.55 +      let
    3.56 +        val eqs_t = mk_equations consts
    3.57 +        val eqs = map (fn eq => Goal.prove lthy argnames [] eq
    3.58 +          (fn _ => Skip_Proof.cheat_tac (ProofContext.theory_of lthy))) eqs_t
    3.59 +      in
    3.60 +        fold (fn (name, eq) => Local_Theory.note
    3.61 +        ((Binding.conceal (Binding.qualify true prfx
    3.62 +           (Binding.qualify true name (Binding.name "simps"))),
    3.63 +           Code.add_default_eqn_attrib :: map (Attrib.internal o K)
    3.64 +             [Simplifier.simp_add, Nitpick_Simps.add]), [eq]) #> snd) (names ~~ eqs) lthy
    3.65 +      end)
    3.66 +
    3.67  (** ensuring sort constraints **)
    3.68  
    3.69  fun perhaps_constrain thy insts raw_vs =