# HG changeset patch
# User bulwahn
# Date 1310978061 -7200
# Node ID 485d2ad43528bc35abcba7699028918a91c3c228
# Parent  74f1f2dd8f52d3273f5fb87ed69638b37d1f80bb
adding random, exhaustive and SML quickcheck as testers

diff -r 74f1f2dd8f52 -r 485d2ad43528 src/HOL/Library/SML_Quickcheck.thy
--- a/src/HOL/Library/SML_Quickcheck.thy	Sun Jul 17 22:25:14 2011 +0200
+++ b/src/HOL/Library/SML_Quickcheck.thy	Mon Jul 18 10:34:21 2011 +0200
@@ -23,6 +23,7 @@
                 case result of NONE => iterate size (j - 1) | SOME q => SOME q
               end
      in fn [_, size] => (iterate size iterations, NONE) end))
+  #> Context.theory_map (Quickcheck.add_tester ("SML", Quickcheck.generator_test_goal_terms))  
 *}
 
 end
diff -r 74f1f2dd8f52 -r 485d2ad43528 src/HOL/Tools/Quickcheck/exhaustive_generators.ML
--- a/src/HOL/Tools/Quickcheck/exhaustive_generators.ML	Sun Jul 17 22:25:14 2011 +0200
+++ b/src/HOL/Tools/Quickcheck/exhaustive_generators.ML	Mon Jul 18 10:34:21 2011 +0200
@@ -488,6 +488,8 @@
       thy (SOME target) (K I) (HOLogic.mk_list @{typ "code_numeral => bool"} ts') []
   end;
 
+val test_goals = Quickcheck.generator_test_goal_terms;
+  
 (* setup *)
 
 val setup =
@@ -500,6 +502,7 @@
   #> Datatype.interpretation (Quickcheck_Common.ensure_sort_datatype
       (((@{sort type}, @{sort type}), @{sort bounded_forall}), instantiate_bounded_forall_datatype))*)
   #> Context.theory_map (Quickcheck.add_generator ("exhaustive", compile_generator_expr))
+  #> Context.theory_map (Quickcheck.add_tester ("exhaustive", 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 74f1f2dd8f52 -r 485d2ad43528 src/HOL/Tools/Quickcheck/random_generators.ML
--- a/src/HOL/Tools/Quickcheck/random_generators.ML	Sun Jul 17 22:25:14 2011 +0200
+++ b/src/HOL/Tools/Quickcheck/random_generators.ML	Mon Jul 18 10:34:21 2011 +0200
@@ -438,14 +438,15 @@
       end
   end;
 
-
+val test_goals = Quickcheck.generator_test_goal_terms;
+  
 (** setup **)
 
 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_generator ("random", compile_generator_expr));
+  #> Context.theory_map (Quickcheck.add_generator ("random", compile_generator_expr))
+  #> Context.theory_map (Quickcheck.add_tester ("random", test_goals));
 
 end;
diff -r 74f1f2dd8f52 -r 485d2ad43528 src/Tools/quickcheck.ML
--- a/src/Tools/quickcheck.ML	Sun Jul 17 22:25:14 2011 +0200
+++ b/src/Tools/quickcheck.ML	Mon Jul 18 10:34:21 2011 +0200
@@ -60,6 +60,8 @@
   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: Proof.context -> bool * bool -> (string * typ) list ->
+    (term * term list) list -> result list
   (* testing terms and proof states *)
   val test_term: Proof.context -> bool * bool -> term * term list -> result
   val test_goal_terms:
@@ -469,7 +471,7 @@
         collect_results f ts (result :: results)
     end  
 
-fun test_goal_terms ctxt (limit_time, is_interactive) insts goals =
+fun generator_test_goal_terms ctxt (limit_time, is_interactive) insts goals =
   let
     fun test_term' goal =
       case goal of
@@ -477,15 +479,18 @@
       | ts => test_term_with_increasing_cardinality ctxt (limit_time, is_interactive) (map snd ts)
     val correct_inst_goals = instantiate_goals ctxt insts goals
   in
-    case lookup_tester ctxt (Config.get ctxt tester) of
-      SOME test_goal_terms => test_goal_terms ctxt (limit_time, is_interactive) insts goals
-    | NONE =>
-        if Config.get ctxt finite_types then
-          collect_results test_term' correct_inst_goals []
-        else
-          collect_results (test_term ctxt (limit_time, is_interactive)) (maps (map snd) correct_inst_goals) []
+    if Config.get ctxt finite_types then
+      collect_results test_term' correct_inst_goals []
+    else
+      collect_results (test_term ctxt (limit_time, is_interactive))
+        (maps (map snd) correct_inst_goals) []
   end;
 
+fun test_goal_terms ctxt (limit_time, is_interactive) insts goals =
+  case lookup_tester ctxt (Config.get ctxt tester) of
+    SOME test_goal_terms => test_goal_terms ctxt (limit_time, is_interactive) insts goals
+  | NONE => error ("Unknown tester: " ^ Config.get ctxt tester)
+
 fun test_goal (time_limit, is_interactive) (insts, eval_terms) i state =
   let
     val lthy = Proof.context_of state;