# HG changeset patch
# User bulwahn
# Date 1329823233 -3600
# Node ID ad21900e0ee9a3c0f12eea67b0c9482b8888320e
# Parent  daa915508f63375c10106fe1d9b33e2738c9a4d0
subtype preprocessing in Quickcheck;
adding option use_subtype;
tuned

diff -r daa915508f63 -r ad21900e0ee9 src/HOL/Library/Dlist.thy
--- a/src/HOL/Library/Dlist.thy	Tue Feb 21 11:25:48 2012 +0100
+++ b/src/HOL/Library/Dlist.thy	Tue Feb 21 12:20:33 2012 +0100
@@ -182,7 +182,7 @@
 
 subsection {* Quickcheck generators *}
 
-quickcheck_generator dlist constructors: empty, insert
+quickcheck_generator dlist predicate: distinct constructors: empty, insert
 
 hide_const (open) member fold foldr empty insert remove map filter null member length fold
 
diff -r daa915508f63 -r ad21900e0ee9 src/HOL/Library/RBT.thy
--- a/src/HOL/Library/RBT.thy	Tue Feb 21 11:25:48 2012 +0100
+++ b/src/HOL/Library/RBT.thy	Tue Feb 21 12:20:33 2012 +0100
@@ -171,6 +171,6 @@
 
 subsection {* Quickcheck generators *}
 
-quickcheck_generator rbt constructors: empty, insert
+quickcheck_generator rbt predicate: is_rbt constructors: empty, insert
 
 end
diff -r daa915508f63 -r ad21900e0ee9 src/HOL/Tools/Quickcheck/abstract_generators.ML
--- a/src/HOL/Tools/Quickcheck/abstract_generators.ML	Tue Feb 21 11:25:48 2012 +0100
+++ b/src/HOL/Tools/Quickcheck/abstract_generators.ML	Tue Feb 21 12:20:33 2012 +0100
@@ -32,8 +32,9 @@
   let
     val ctxt = Proof_Context.init_global thy
     val tyco = prep_tyco ctxt tyco_raw
+    val opt_pred = Option.map (prep_term ctxt) opt_pred_raw
     val constrs = map (prep_term ctxt) constrs_raw
-    val _ = check_constrs ctxt tyco constrs 
+    val _ = check_constrs ctxt tyco constrs
     val vs = map dest_TFree (snd (dest_Type (body_type (fastype_of (hd constrs)))))
     val name = Long_Name.base_name tyco 
     fun mk_dconstrs (Const (s, T)) =
@@ -53,7 +54,9 @@
   in
     thy
     |> ensure_sort (@{sort full_exhaustive}, Exhaustive_Generators.instantiate_full_exhaustive_datatype)
+    |> ensure_sort (@{sort exhaustive}, Exhaustive_Generators.instantiate_exhaustive_datatype)
     |> ensure_sort (@{sort random}, Random_Generators.instantiate_random_datatype)
+    |> (case opt_pred of NONE => I | SOME t => Context.theory_map (Quickcheck_Common.register_predicate (t, tyco)))
   end
 
 val quickcheck_generator = gen_quickcheck_generator (K I) (K I)
diff -r daa915508f63 -r ad21900e0ee9 src/HOL/Tools/Quickcheck/exhaustive_generators.ML
--- a/src/HOL/Tools/Quickcheck/exhaustive_generators.ML	Tue Feb 21 11:25:48 2012 +0100
+++ b/src/HOL/Tools/Quickcheck/exhaustive_generators.ML	Tue Feb 21 12:20:33 2012 +0100
@@ -23,6 +23,9 @@
   
   val instantiate_full_exhaustive_datatype : Datatype_Aux.config -> Datatype_Aux.descr ->
     (string * sort) list -> string list -> string -> string list * string list -> typ list * typ list -> theory -> theory
+  val instantiate_exhaustive_datatype : Datatype_Aux.config -> Datatype_Aux.descr ->
+    (string * sort) list -> string list -> string -> string list * string list -> typ list * typ list -> theory -> theory
+
 end;
 
 structure Exhaustive_Generators : EXHAUSTIVE_GENERATORS =
diff -r daa915508f63 -r ad21900e0ee9 src/HOL/Tools/Quickcheck/quickcheck_common.ML
--- a/src/HOL/Tools/Quickcheck/quickcheck_common.ML	Tue Feb 21 11:25:48 2012 +0100
+++ b/src/HOL/Tools/Quickcheck/quickcheck_common.ML	Tue Feb 21 12:20:33 2012 +0100
@@ -14,6 +14,7 @@
     -> (string * sort -> string * sort) option
   val instantiate_goals: Proof.context -> (string * typ) list -> (term * term list) list
     -> (typ option * (term * term list)) list list
+  val register_predicate : term * string -> Context.generic -> Context.generic
   val mk_safe_if : term -> term -> term * term * (bool -> term) -> bool -> term
   val collect_results : ('a -> Quickcheck.result) -> 'a list -> Quickcheck.result list -> Quickcheck.result list
   type result = (bool * term list) option * Quickcheck.report option
@@ -96,9 +97,11 @@
           val _ = Quickcheck.verbose_message ctxt
             ("[Quickcheck-" ^ name ^ "] Test data size: " ^ string_of_int k)
           val _ = current_size := k
-          val ((result, report), timing) =
+          val ((result, report), time) =
             cpu_time ("size " ^ string_of_int k) (fn () => test_fun genuine_only [1, k - 1])
-          val _ = Quickcheck.add_timing timing current_result
+          val _ = if Config.get ctxt Quickcheck.timing then
+            Quickcheck.verbose_message ctxt (fst time ^ ": " ^ string_of_int (snd time) ^ " ms") else ()
+          val _ = Quickcheck.add_timing time current_result
           val _ = Quickcheck.add_report k report current_result
         in
           case result of
@@ -277,6 +280,37 @@
     subst_bounds (map Free (rev vs'), body)
   end
 
+  
+structure Subtype_Predicates = Generic_Data
+(
+  type T = (term * string) list
+  val empty = []
+  val extend = I
+  val merge = AList.merge (op =) (K true)
+)
+
+val register_predicate = Subtype_Predicates.map o AList.update (op =)
+
+fun subtype_preprocess ctxt (T, (t, ts)) =
+  let
+    val preds = Subtype_Predicates.get (Context.Proof ctxt)
+    fun matches (p $ x) = AList.defined Term.could_unify preds p  
+    fun get_match (p $ x) = Option.map (rpair x) (AList.lookup Term.could_unify preds p)
+    fun subst_of (tyco, v as Free (x, repT)) =
+      let
+        val [(info, _)] = Typedef.get_info ctxt tyco
+        val repT' = Logic.varifyT_global (#rep_type info)
+        val substT = Sign.typ_match (Proof_Context.theory_of ctxt) (repT', repT) Vartab.empty 
+        val absT = Envir.subst_type substT (Logic.varifyT_global (#abs_type info))
+      in (v, Const (#Rep_name info, absT --> repT) $ Free (x, absT)) end
+    val (prems, concl) = strip_imp t
+    val subst = map subst_of (map_filter get_match prems)
+    val t' = Term.subst_free subst
+     (fold_rev (curry HOLogic.mk_imp) (filter_out matches prems) concl)
+  in
+    (T, (t', ts))
+  end
+
 (* instantiation of type variables with concrete types *)
  
 fun instantiate_goals lthy insts goals =
@@ -333,6 +367,7 @@
 
 fun generator_test_goal_terms generator ctxt catch_code_errors insts goals =
   let
+    val use_subtype = Config.get ctxt Quickcheck.use_subtype
     fun add_eval_term t ts = if is_Free t then ts else ts @ [t]
     fun add_equation_eval_terms (t, eval_terms) =
       case try HOLogic.dest_eq (snd (strip_imp t)) of
@@ -343,6 +378,7 @@
         [(NONE, t)] => test_term generator ctxt catch_code_errors t
       | ts => test_term_with_cardinality generator ctxt catch_code_errors (map snd ts)
     val goals' = instantiate_goals ctxt insts goals
+      |> (if use_subtype then map (map (subtype_preprocess ctxt)) else I)
       |> map (map (apsnd add_equation_eval_terms))
   in
     if Config.get ctxt Quickcheck.finite_types then
diff -r daa915508f63 -r ad21900e0ee9 src/Tools/quickcheck.ML
--- a/src/Tools/quickcheck.ML	Tue Feb 21 11:25:48 2012 +0100
+++ b/src/Tools/quickcheck.ML	Tue Feb 21 12:20:33 2012 +0100
@@ -19,13 +19,14 @@
   val depth : int Config.T
   val no_assms : bool Config.T
   val report : bool Config.T
+  val timeout : real Config.T
   val timing : bool Config.T
   val genuine_only : bool Config.T
   val abort_potential : bool Config.T  
   val quiet : bool Config.T
   val verbose : bool Config.T
-  val timeout : real Config.T
-  val allow_function_inversion : bool Config.T;
+  val use_subtype : bool Config.T
+  val allow_function_inversion : bool Config.T
   val finite_types : bool Config.T
   val finite_type_size : int Config.T
   val set_active_testers: string list -> Context.generic -> Context.generic
@@ -177,11 +178,16 @@
 val no_assms = Attrib.setup_config_bool @{binding quickcheck_no_assms} (K false)
 val report = Attrib.setup_config_bool @{binding quickcheck_report} (K true)
 val timing = Attrib.setup_config_bool @{binding quickcheck_timing} (K false)
+val timeout = Attrib.setup_config_real @{binding quickcheck_timeout} (K 30.0)
+
 val genuine_only = Attrib.setup_config_bool @{binding quickcheck_genuine_only} (K false)
 val abort_potential = Attrib.setup_config_bool @{binding quickcheck_abort_potential} (K false)
+
 val quiet = Attrib.setup_config_bool @{binding quickcheck_quiet} (K false)
 val verbose = Attrib.setup_config_bool @{binding quickcheck_verbose} (K false)
-val timeout = Attrib.setup_config_real @{binding quickcheck_timeout} (K 30.0)
+
+val use_subtype = Attrib.setup_config_bool @{binding quickcheck_use_subtype} (K false)
+
 val allow_function_inversion =
   Attrib.setup_config_bool @{binding quickcheck_allow_function_inversion} (K false)
 val finite_types = Attrib.setup_config_bool @{binding quickcheck_finite_types} (K true)
@@ -438,6 +444,7 @@
   | parse_test_param ("abort_potential", [arg]) = apsnd (Config.put_generic abort_potential (read_bool arg))
   | parse_test_param ("quiet", [arg]) = apsnd (Config.put_generic quiet (read_bool arg))
   | parse_test_param ("verbose", [arg]) = apsnd (Config.put_generic verbose (read_bool arg))
+  | parse_test_param ("use_subtype", [arg]) = apsnd (Config.put_generic use_subtype (read_bool arg))  
   | parse_test_param ("timeout", [arg]) = apsnd (Config.put_generic timeout (read_real arg))
   | parse_test_param ("finite_types", [arg]) = apsnd (Config.put_generic finite_types (read_bool arg))
   | parse_test_param ("allow_function_inversion", [arg]) =