subtype preprocessing in Quickcheck;
authorbulwahn
Tue Feb 21 12:20:33 2012 +0100 (2012-02-21)
changeset 46565ad21900e0ee9
parent 46564 daa915508f63
child 46566 46124c9b5663
subtype preprocessing in Quickcheck;
adding option use_subtype;
tuned
src/HOL/Library/Dlist.thy
src/HOL/Library/RBT.thy
src/HOL/Tools/Quickcheck/abstract_generators.ML
src/HOL/Tools/Quickcheck/exhaustive_generators.ML
src/HOL/Tools/Quickcheck/quickcheck_common.ML
src/Tools/quickcheck.ML
     1.1 --- a/src/HOL/Library/Dlist.thy	Tue Feb 21 11:25:48 2012 +0100
     1.2 +++ b/src/HOL/Library/Dlist.thy	Tue Feb 21 12:20:33 2012 +0100
     1.3 @@ -182,7 +182,7 @@
     1.4  
     1.5  subsection {* Quickcheck generators *}
     1.6  
     1.7 -quickcheck_generator dlist constructors: empty, insert
     1.8 +quickcheck_generator dlist predicate: distinct constructors: empty, insert
     1.9  
    1.10  hide_const (open) member fold foldr empty insert remove map filter null member length fold
    1.11  
     2.1 --- a/src/HOL/Library/RBT.thy	Tue Feb 21 11:25:48 2012 +0100
     2.2 +++ b/src/HOL/Library/RBT.thy	Tue Feb 21 12:20:33 2012 +0100
     2.3 @@ -171,6 +171,6 @@
     2.4  
     2.5  subsection {* Quickcheck generators *}
     2.6  
     2.7 -quickcheck_generator rbt constructors: empty, insert
     2.8 +quickcheck_generator rbt predicate: is_rbt constructors: empty, insert
     2.9  
    2.10  end
     3.1 --- a/src/HOL/Tools/Quickcheck/abstract_generators.ML	Tue Feb 21 11:25:48 2012 +0100
     3.2 +++ b/src/HOL/Tools/Quickcheck/abstract_generators.ML	Tue Feb 21 12:20:33 2012 +0100
     3.3 @@ -32,8 +32,9 @@
     3.4    let
     3.5      val ctxt = Proof_Context.init_global thy
     3.6      val tyco = prep_tyco ctxt tyco_raw
     3.7 +    val opt_pred = Option.map (prep_term ctxt) opt_pred_raw
     3.8      val constrs = map (prep_term ctxt) constrs_raw
     3.9 -    val _ = check_constrs ctxt tyco constrs 
    3.10 +    val _ = check_constrs ctxt tyco constrs
    3.11      val vs = map dest_TFree (snd (dest_Type (body_type (fastype_of (hd constrs)))))
    3.12      val name = Long_Name.base_name tyco 
    3.13      fun mk_dconstrs (Const (s, T)) =
    3.14 @@ -53,7 +54,9 @@
    3.15    in
    3.16      thy
    3.17      |> ensure_sort (@{sort full_exhaustive}, Exhaustive_Generators.instantiate_full_exhaustive_datatype)
    3.18 +    |> ensure_sort (@{sort exhaustive}, Exhaustive_Generators.instantiate_exhaustive_datatype)
    3.19      |> ensure_sort (@{sort random}, Random_Generators.instantiate_random_datatype)
    3.20 +    |> (case opt_pred of NONE => I | SOME t => Context.theory_map (Quickcheck_Common.register_predicate (t, tyco)))
    3.21    end
    3.22  
    3.23  val quickcheck_generator = gen_quickcheck_generator (K I) (K I)
     4.1 --- a/src/HOL/Tools/Quickcheck/exhaustive_generators.ML	Tue Feb 21 11:25:48 2012 +0100
     4.2 +++ b/src/HOL/Tools/Quickcheck/exhaustive_generators.ML	Tue Feb 21 12:20:33 2012 +0100
     4.3 @@ -23,6 +23,9 @@
     4.4    
     4.5    val instantiate_full_exhaustive_datatype : Datatype_Aux.config -> Datatype_Aux.descr ->
     4.6      (string * sort) list -> string list -> string -> string list * string list -> typ list * typ list -> theory -> theory
     4.7 +  val instantiate_exhaustive_datatype : Datatype_Aux.config -> Datatype_Aux.descr ->
     4.8 +    (string * sort) list -> string list -> string -> string list * string list -> typ list * typ list -> theory -> theory
     4.9 +
    4.10  end;
    4.11  
    4.12  structure Exhaustive_Generators : EXHAUSTIVE_GENERATORS =
     5.1 --- a/src/HOL/Tools/Quickcheck/quickcheck_common.ML	Tue Feb 21 11:25:48 2012 +0100
     5.2 +++ b/src/HOL/Tools/Quickcheck/quickcheck_common.ML	Tue Feb 21 12:20:33 2012 +0100
     5.3 @@ -14,6 +14,7 @@
     5.4      -> (string * sort -> string * sort) option
     5.5    val instantiate_goals: Proof.context -> (string * typ) list -> (term * term list) list
     5.6      -> (typ option * (term * term list)) list list
     5.7 +  val register_predicate : term * string -> Context.generic -> Context.generic
     5.8    val mk_safe_if : term -> term -> term * term * (bool -> term) -> bool -> term
     5.9    val collect_results : ('a -> Quickcheck.result) -> 'a list -> Quickcheck.result list -> Quickcheck.result list
    5.10    type result = (bool * term list) option * Quickcheck.report option
    5.11 @@ -96,9 +97,11 @@
    5.12            val _ = Quickcheck.verbose_message ctxt
    5.13              ("[Quickcheck-" ^ name ^ "] Test data size: " ^ string_of_int k)
    5.14            val _ = current_size := k
    5.15 -          val ((result, report), timing) =
    5.16 +          val ((result, report), time) =
    5.17              cpu_time ("size " ^ string_of_int k) (fn () => test_fun genuine_only [1, k - 1])
    5.18 -          val _ = Quickcheck.add_timing timing current_result
    5.19 +          val _ = if Config.get ctxt Quickcheck.timing then
    5.20 +            Quickcheck.verbose_message ctxt (fst time ^ ": " ^ string_of_int (snd time) ^ " ms") else ()
    5.21 +          val _ = Quickcheck.add_timing time current_result
    5.22            val _ = Quickcheck.add_report k report current_result
    5.23          in
    5.24            case result of
    5.25 @@ -277,6 +280,37 @@
    5.26      subst_bounds (map Free (rev vs'), body)
    5.27    end
    5.28  
    5.29 +  
    5.30 +structure Subtype_Predicates = Generic_Data
    5.31 +(
    5.32 +  type T = (term * string) list
    5.33 +  val empty = []
    5.34 +  val extend = I
    5.35 +  val merge = AList.merge (op =) (K true)
    5.36 +)
    5.37 +
    5.38 +val register_predicate = Subtype_Predicates.map o AList.update (op =)
    5.39 +
    5.40 +fun subtype_preprocess ctxt (T, (t, ts)) =
    5.41 +  let
    5.42 +    val preds = Subtype_Predicates.get (Context.Proof ctxt)
    5.43 +    fun matches (p $ x) = AList.defined Term.could_unify preds p  
    5.44 +    fun get_match (p $ x) = Option.map (rpair x) (AList.lookup Term.could_unify preds p)
    5.45 +    fun subst_of (tyco, v as Free (x, repT)) =
    5.46 +      let
    5.47 +        val [(info, _)] = Typedef.get_info ctxt tyco
    5.48 +        val repT' = Logic.varifyT_global (#rep_type info)
    5.49 +        val substT = Sign.typ_match (Proof_Context.theory_of ctxt) (repT', repT) Vartab.empty 
    5.50 +        val absT = Envir.subst_type substT (Logic.varifyT_global (#abs_type info))
    5.51 +      in (v, Const (#Rep_name info, absT --> repT) $ Free (x, absT)) end
    5.52 +    val (prems, concl) = strip_imp t
    5.53 +    val subst = map subst_of (map_filter get_match prems)
    5.54 +    val t' = Term.subst_free subst
    5.55 +     (fold_rev (curry HOLogic.mk_imp) (filter_out matches prems) concl)
    5.56 +  in
    5.57 +    (T, (t', ts))
    5.58 +  end
    5.59 +
    5.60  (* instantiation of type variables with concrete types *)
    5.61   
    5.62  fun instantiate_goals lthy insts goals =
    5.63 @@ -333,6 +367,7 @@
    5.64  
    5.65  fun generator_test_goal_terms generator ctxt catch_code_errors insts goals =
    5.66    let
    5.67 +    val use_subtype = Config.get ctxt Quickcheck.use_subtype
    5.68      fun add_eval_term t ts = if is_Free t then ts else ts @ [t]
    5.69      fun add_equation_eval_terms (t, eval_terms) =
    5.70        case try HOLogic.dest_eq (snd (strip_imp t)) of
    5.71 @@ -343,6 +378,7 @@
    5.72          [(NONE, t)] => test_term generator ctxt catch_code_errors t
    5.73        | ts => test_term_with_cardinality generator ctxt catch_code_errors (map snd ts)
    5.74      val goals' = instantiate_goals ctxt insts goals
    5.75 +      |> (if use_subtype then map (map (subtype_preprocess ctxt)) else I)
    5.76        |> map (map (apsnd add_equation_eval_terms))
    5.77    in
    5.78      if Config.get ctxt Quickcheck.finite_types then
     6.1 --- a/src/Tools/quickcheck.ML	Tue Feb 21 11:25:48 2012 +0100
     6.2 +++ b/src/Tools/quickcheck.ML	Tue Feb 21 12:20:33 2012 +0100
     6.3 @@ -19,13 +19,14 @@
     6.4    val depth : int Config.T
     6.5    val no_assms : bool Config.T
     6.6    val report : bool Config.T
     6.7 +  val timeout : real Config.T
     6.8    val timing : bool Config.T
     6.9    val genuine_only : bool Config.T
    6.10    val abort_potential : bool Config.T  
    6.11    val quiet : bool Config.T
    6.12    val verbose : bool Config.T
    6.13 -  val timeout : real Config.T
    6.14 -  val allow_function_inversion : bool Config.T;
    6.15 +  val use_subtype : bool Config.T
    6.16 +  val allow_function_inversion : bool Config.T
    6.17    val finite_types : bool Config.T
    6.18    val finite_type_size : int Config.T
    6.19    val set_active_testers: string list -> Context.generic -> Context.generic
    6.20 @@ -177,11 +178,16 @@
    6.21  val no_assms = Attrib.setup_config_bool @{binding quickcheck_no_assms} (K false)
    6.22  val report = Attrib.setup_config_bool @{binding quickcheck_report} (K true)
    6.23  val timing = Attrib.setup_config_bool @{binding quickcheck_timing} (K false)
    6.24 +val timeout = Attrib.setup_config_real @{binding quickcheck_timeout} (K 30.0)
    6.25 +
    6.26  val genuine_only = Attrib.setup_config_bool @{binding quickcheck_genuine_only} (K false)
    6.27  val abort_potential = Attrib.setup_config_bool @{binding quickcheck_abort_potential} (K false)
    6.28 +
    6.29  val quiet = Attrib.setup_config_bool @{binding quickcheck_quiet} (K false)
    6.30  val verbose = Attrib.setup_config_bool @{binding quickcheck_verbose} (K false)
    6.31 -val timeout = Attrib.setup_config_real @{binding quickcheck_timeout} (K 30.0)
    6.32 +
    6.33 +val use_subtype = Attrib.setup_config_bool @{binding quickcheck_use_subtype} (K false)
    6.34 +
    6.35  val allow_function_inversion =
    6.36    Attrib.setup_config_bool @{binding quickcheck_allow_function_inversion} (K false)
    6.37  val finite_types = Attrib.setup_config_bool @{binding quickcheck_finite_types} (K true)
    6.38 @@ -438,6 +444,7 @@
    6.39    | parse_test_param ("abort_potential", [arg]) = apsnd (Config.put_generic abort_potential (read_bool arg))
    6.40    | parse_test_param ("quiet", [arg]) = apsnd (Config.put_generic quiet (read_bool arg))
    6.41    | parse_test_param ("verbose", [arg]) = apsnd (Config.put_generic verbose (read_bool arg))
    6.42 +  | parse_test_param ("use_subtype", [arg]) = apsnd (Config.put_generic use_subtype (read_bool arg))  
    6.43    | parse_test_param ("timeout", [arg]) = apsnd (Config.put_generic timeout (read_real arg))
    6.44    | parse_test_param ("finite_types", [arg]) = apsnd (Config.put_generic finite_types (read_bool arg))
    6.45    | parse_test_param ("allow_function_inversion", [arg]) =