# HG changeset patch
# User bulwahn
# Date 1310978061 -7200
# Node ID eeb10fdd95355ddae4ccd09798b114666f2c0d5d
# Parent  abd1f074cb986602f140068fe8e93b5e45fcddcd
changed every tester to have a configuration in quickcheck; enabling parallel testing of different testers in quickcheck

diff -r abd1f074cb98 -r eeb10fdd9535 src/HOL/Tools/Quickcheck/exhaustive_generators.ML
--- a/src/HOL/Tools/Quickcheck/exhaustive_generators.ML	Mon Jul 18 10:34:21 2011 +0200
+++ b/src/HOL/Tools/Quickcheck/exhaustive_generators.ML	Mon Jul 18 10:34:21 2011 +0200
@@ -492,6 +492,8 @@
   
 (* setup *)
 
+val active = Attrib.setup_config_bool @{binding quickcheck_exhaustive_active} (K true);
+
 val setup =
   Datatype.interpretation (Quickcheck_Common.ensure_sort_datatype
       (((@{sort typerep}, @{sort term_of}), @{sort full_exhaustive}), instantiate_full_exhaustive_datatype))
@@ -501,7 +503,7 @@
       (((@{sort typerep}, @{sort term_of}), @{sort fast_exhaustive}), instantiate_fast_exhaustive_datatype))
   #> Datatype.interpretation (Quickcheck_Common.ensure_sort_datatype
       (((@{sort type}, @{sort type}), @{sort bounded_forall}), instantiate_bounded_forall_datatype))*)
-  #> Context.theory_map (Quickcheck.add_tester ("exhaustive", test_goals))
+  #> Context.theory_map (Quickcheck.add_tester ("exhaustive", (active, test_goals)))
   #> Context.theory_map (Quickcheck.add_batch_generator ("exhaustive", compile_generator_exprs))
   #> Context.theory_map (Quickcheck.add_batch_validator ("exhaustive", compile_validator_exprs));
 
diff -r abd1f074cb98 -r eeb10fdd9535 src/HOL/Tools/Quickcheck/narrowing_generators.ML
--- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Mon Jul 18 10:34:21 2011 +0200
+++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Mon Jul 18 10:34:21 2011 +0200
@@ -461,11 +461,13 @@
 
 (* setup *)
 
+val active = Attrib.setup_config_bool @{binding quickcheck_narrowing_active} (K true);
+
 val setup =
   Code.datatype_interpretation ensure_partial_term_of
   #> Code.datatype_interpretation ensure_partial_term_of_code
   #> Datatype.interpretation (Quickcheck_Common.ensure_sort_datatype
     (((@{sort typerep}, @{sort term_of}), @{sort narrowing}), instantiate_narrowing_datatype))
-  #> Context.theory_map (Quickcheck.add_tester ("narrowing", test_goals))
+  #> Context.theory_map (Quickcheck.add_tester ("narrowing", (active, test_goals)))
     
 end;
\ No newline at end of file
diff -r abd1f074cb98 -r eeb10fdd9535 src/HOL/Tools/Quickcheck/random_generators.ML
--- a/src/HOL/Tools/Quickcheck/random_generators.ML	Mon Jul 18 10:34:21 2011 +0200
+++ b/src/HOL/Tools/Quickcheck/random_generators.ML	Mon Jul 18 10:34:21 2011 +0200
@@ -442,10 +442,12 @@
   
 (** setup **)
 
+val active = Attrib.setup_config_bool @{binding quickcheck_random_active} (K false);
+
 val setup =
   Datatype.interpretation (Quickcheck_Common.ensure_sort_datatype
     (((@{sort typerep}, @{sort term_of}), @{sort random}), instantiate_random_datatype))
   #> Code_Target.extend_target (target, (Code_Runtime.target, K I))
-  #> Context.theory_map (Quickcheck.add_tester ("random", test_goals));
+  #> Context.theory_map (Quickcheck.add_tester ("random", (active, test_goals)));
 
 end;
diff -r abd1f074cb98 -r eeb10fdd9535 src/HOL/Tools/inductive_codegen.ML
--- a/src/HOL/Tools/inductive_codegen.ML	Mon Jul 18 10:34:21 2011 +0200
+++ b/src/HOL/Tools/inductive_codegen.ML	Mon Jul 18 10:34:21 2011 +0200
@@ -862,6 +862,8 @@
       NONE => deepen bound f (i + 1)
     | SOME x => SOME x);
 
+val active = Attrib.setup_config_bool @{binding quickcheck_inductive_SML_active} (K false);
+    
 val depth_bound = Attrib.setup_config_int @{binding ind_quickcheck_depth} (K 10);
 val depth_start = Attrib.setup_config_int @{binding ind_quickcheck_depth_start} (K 1);
 val random_values = Attrib.setup_config_int @{binding ind_quickcheck_random} (K 5);
@@ -927,6 +929,6 @@
 val test_goal = Quickcheck.generator_test_goal_terms test_term;
 
 val quickcheck_setup =
-  Context.theory_map (Quickcheck.add_tester ("SML_inductive", test_goal));
+  Context.theory_map (Quickcheck.add_tester ("SML_inductive", (active, test_goal)));
 
 end;
diff -r abd1f074cb98 -r eeb10fdd9535 src/Tools/quickcheck.ML
--- a/src/Tools/quickcheck.ML	Mon Jul 18 10:34:21 2011 +0200
+++ b/src/Tools/quickcheck.ML	Mon Jul 18 10:34:21 2011 +0200
@@ -42,17 +42,14 @@
   val add_timing : (string * int) -> result Unsynchronized.ref -> unit
   val counterexample_of : result -> (string * term) list option
   val timings_of : result -> (string * int) list
-  (* registering generators *)
-  (*val add_generator:
-    string * (Proof.context -> (term * term list) list -> int list -> term list option * report option)
-      -> Context.generic -> Context.generic*)
-  val add_tester:
-    string * (Proof.context -> bool * bool -> (string * typ) list -> (term * term list) list -> result list)
-      -> Context.generic -> Context.generic
-  val add_batch_generator:
+  (* registering testers & generators *) 
+  type tester =
+    Proof.context -> bool * bool -> (string * typ) list -> (term * term list) list -> result list
+  val add_tester : string * (bool Config.T * tester) -> Context.generic -> Context.generic
+  val add_batch_generator :
     string * (Proof.context -> term list -> (int -> term list option) list)
       -> Context.generic -> Context.generic
-  val add_batch_validator:
+  val add_batch_validator :
     string * (Proof.context -> term list -> (int -> bool) list)
       -> Context.generic -> Context.generic
   (* basic operations *)
@@ -61,13 +58,12 @@
   val limit : Time.time -> (bool * bool) -> (unit -> 'a) -> (unit -> 'a) -> unit -> 'a  
   val instantiate_goals: Proof.context -> (string * typ) list -> (term * term list) list
     -> (typ option * (term * term list)) list list
-  val collect_results: ('a -> result) -> 'a list -> result list -> result list
-  val generator_test_goal_terms: compile_generator ->
+  val collect_results : ('a -> result) -> 'a list -> result list -> result list
+  val generator_test_goal_terms : compile_generator ->
     Proof.context -> bool * bool -> (string * typ) list -> (term * term list) list -> result list
   (* testing terms and proof states *)
   val test_term: compile_generator -> Proof.context -> bool * bool -> term * term list -> result
-  val test_goal_terms:
-    Proof.context -> bool * bool -> (string * typ) list -> (term * term list) list -> result list
+  (*val test_goal_terms : tester*)
   val quickcheck: (string * string list) list -> int -> Proof.state -> (string * term) list option
   (* testing a batch of terms *)
   val test_terms:
@@ -193,11 +189,13 @@
   make_test_params
     (merge (op =) (default_type1, default_type2), merge_expectation (expect1, expect2));
 
+type tester =
+  Proof.context -> bool * bool -> (string * typ) list -> (term * term list) list -> result list
+
 structure Data = Generic_Data
 (
   type T =
-    ((string * (Proof.context -> bool * bool ->
-      (string * typ) list -> (term * term list) list -> result list)) list
+    ((string * (bool Config.T * tester)) list
       * ((string * (Proof.context -> term list -> (int -> term list option) list)) list
       * ((string * (Proof.context -> term list -> (int -> bool) list)) list)))
       * test_params;
@@ -476,10 +474,22 @@
         (maps (map snd) correct_inst_goals) []
   end;
 
+  
+fun active_testers ctxt =
+  let
+    val testers = (map snd o fst o fst o Data.get o Context.Proof) ctxt
+  in
+    map snd (filter (fn (active, _) => Config.get ctxt active) testers)
+  end
+  
 fun test_goal_terms ctxt (limit_time, is_interactive) insts goals =
-  case lookup_tester ctxt (Config.get ctxt tester) of
+  (*case lookup_tester ctxt of
     SOME test_goal_terms => test_goal_terms ctxt (limit_time, is_interactive) insts goals
-  | NONE => error ("Unknown tester: " ^ Config.get ctxt tester)
+  | NONE => error ("Unknown tester: " ^ Config.get ctxt tester)*)
+  case active_testers ctxt of
+    [] => error "No active tester for quickcheck"
+  | testers => testers |> ParList.find_some (fn tester =>
+      find_first found_counterexample (tester ctxt (limit_time, is_interactive) insts goals))
 
 fun test_goal (time_limit, is_interactive) (insts, eval_terms) i state =
   let