adapting mutabelle; exporting more Quickcheck functions
authorbulwahn
Wed, 23 Mar 2011 08:50:32 +0100
changeset 42089 904897d0c5bd
parent 42088 8d00484551fe
child 42090 ef566ce50170
adapting mutabelle; exporting more Quickcheck functions
src/HOL/Mutabelle/mutabelle.ML
src/HOL/Mutabelle/mutabelle_extra.ML
src/Tools/quickcheck.ML
--- a/src/HOL/Mutabelle/mutabelle.ML	Wed Mar 23 08:50:31 2011 +0100
+++ b/src/HOL/Mutabelle/mutabelle.ML	Wed Mar 23 08:50:32 2011 +0100
@@ -507,11 +507,11 @@
 fun qc_recursive usedthy [] insts sz qciter acc = rev acc
  | qc_recursive usedthy (x::xs) insts sz qciter acc = qc_recursive usedthy xs insts sz qciter 
      (Output.urgent_message ("qc_recursive: " ^ string_of_int (length xs));
-     ((x, pretty (the_default [] (Option.map fst (fst (Quickcheck.test_term
+     ((x, pretty (the_default [] (Quickcheck.counterexample_of (Quickcheck.test_term
        ((Config.put Quickcheck.size sz #> Config.put Quickcheck.iterations qciter
         #> Config.put Quickcheck.tester (!testgen_name))
          (ProofContext.init_global usedthy))
-       (true, false) (preprocess usedthy insts x, [])))))) :: acc))
+       (true, false) (preprocess usedthy insts x, []))))) :: acc))
           handle ERROR msg => (Output.urgent_message msg; qc_recursive usedthy xs insts sz qciter acc);
 
 
--- a/src/HOL/Mutabelle/mutabelle_extra.ML	Wed Mar 23 08:50:31 2011 +0100
+++ b/src/HOL/Mutabelle/mutabelle_extra.ML	Wed Mar 23 08:50:32 2011 +0100
@@ -10,11 +10,11 @@
 val take_random : int -> 'a list -> 'a list
 
 datatype outcome = GenuineCex | PotentialCex | NoCex | Donno | Timeout | Error | Solved | Unsolved
-type timing = (string * int) list
+type timings = (string * int) list
 
-type mtd = string * (theory -> term -> outcome * (timing * (int * Quickcheck.report list) list option))
+type mtd = string * (theory -> term -> outcome * timings)
 
-type mutant_subentry = term * (string * (outcome * (timing * Quickcheck.report option))) list
+type mutant_subentry = term * (string * (outcome * timings)) list
 type detailed_entry = string * bool * term * mutant_subentry list
 
 type subentry = string * int * int * int * int * int * int
@@ -103,11 +103,11 @@
   | string_of_outcome Solved = "Solved"
   | string_of_outcome Unsolved = "Unsolved"
 
-type timing = (string * int) list
+type timings = (string * int) list
 
-type mtd = string * (theory -> term -> outcome * (timing * (int * Quickcheck.report list) list option))
+type mtd = string * (theory -> term -> outcome * timings)
 
-type mutant_subentry = term * (string * (outcome * (timing * Quickcheck.report option))) list
+type mutant_subentry = term * (string * (outcome * timings)) list
 type detailed_entry = string * bool * term * mutant_subentry list
 
 type subentry = string * int * int * int * int * int * int
@@ -121,12 +121,16 @@
 fun invoke_quickcheck change_options quickcheck_generator thy t =
   TimeLimit.timeLimit (seconds (!Auto_Tools.time_limit))
       (fn _ =>
-          case Quickcheck.test_goal_terms (change_options (ProofContext.init_global thy))
-              (false, false) [] [(t, [])] of
-            (NONE, _) => (NoCex, ([], NONE))
-          | (SOME _, _) => (GenuineCex, ([], NONE))) ()
+          let
+            val [result] = Quickcheck.test_goal_terms (change_options (ProofContext.init_global thy))
+              (false, false) [] [(t, [])]
+          in
+            case Quickcheck.counterexample_of result of 
+              NONE => (NoCex, Quickcheck.timings_of result)
+            | SOME _ => (GenuineCex, Quickcheck.timings_of result)
+          end) ()
   handle TimeLimit.TimeOut =>
-         (Timeout, ([("timelimit", Real.floor (!Auto_Tools.time_limit))], NONE))
+         (Timeout, [("timelimit", Real.floor (!Auto_Tools.time_limit))])
 
 fun quickcheck_mtd change_options quickcheck_generator =
   ("quickcheck_" ^ quickcheck_generator, invoke_quickcheck change_options quickcheck_generator)
@@ -138,8 +142,8 @@
     val state = Proof.theorem NONE (K I) (map (single o rpair []) [t]) (ProofContext.init_global thy) 
   in
     case Solve_Direct.solve_direct false state of
-      (true, _) => (Solved, ([], NONE))
-    | (false, _) => (Unsolved, ([], NONE))
+      (true, _) => (Solved, [])
+    | (false, _) => (Unsolved, [])
   end
 
 val solve_direct_mtd = ("solve_direct", invoke_solve_direct) 
@@ -151,8 +155,8 @@
     val state = Proof.theorem NONE (K I) (map (single o rpair []) [t]) (ProofContext.init_global thy)
   in
     case Try.invoke_try (SOME (seconds 5.0)) ([], [], []) state of
-      true => (Solved, ([], NONE))
-    | false => (Unsolved, ([], NONE))
+      true => (Solved, [])
+    | false => (Unsolved, [])
   end
 
 val try_mtd = ("try", invoke_try)
@@ -198,7 +202,7 @@
       (Nitpick_Isar.default_params thy []) false 1 1 1 [] [] t
     val _ = Output.urgent_message ("Nitpick: " ^ res)
   in
-    rpair ([], NONE) (case res of
+    (rpair []) (case res of
       "genuine" => GenuineCex
     | "likely_genuine" => GenuineCex
     | "potential" => PotentialCex
@@ -347,13 +351,13 @@
 fun safe_invoke_mtd thy (mtd_name, invoke_mtd) t =
   let
     val _ = Output.urgent_message ("Invoking " ^ mtd_name)
-    val (res, (timing, reports)) = (*cpu_time "total time"
+    val (res, timing) = (*cpu_time "total time"
       (fn () => *)case try (invoke_mtd thy) t of
-          SOME (res, (timing, reports)) => (res, (timing, reports))
+          SOME (res, timing) => (res, timing)
         | NONE => (Output.urgent_message ("**** PROBLEMS WITH " ^ Syntax.string_of_term_global thy t);
-           (Error, ([], NONE)))
+           (Error, []))
     val _ = Output.urgent_message (" Done")
-  in (res, (timing, reports)) end
+  in (res, timing) end
 
 (* theory -> term list -> mtd -> subentry *)
 
@@ -431,14 +435,14 @@
 
 fun string_of_mutant_subentry' thy thm_name (t, results) =
   let
-    fun string_of_report (Quickcheck.Report {iterations = i, raised_match_errors = e,
+   (* fun string_of_report (Quickcheck.Report {iterations = i, raised_match_errors = e,
       satisfied_assms = s, positive_concl_tests = p}) =
       "errors: " ^ string_of_int e ^ "; conclusion tests: " ^ string_of_int p
     fun string_of_reports NONE = ""
       | string_of_reports (SOME reports) =
         cat_lines (map (fn (size, [report]) =>
-          "size " ^ string_of_int size ^ ": " ^ string_of_report report) (rev reports))
-    fun string_of_mtd_result (mtd_name, (outcome, (timing, reports))) =
+          "size " ^ string_of_int size ^ ": " ^ string_of_report report) (rev reports))*)
+    fun string_of_mtd_result (mtd_name, (outcome, timing)) =
       mtd_name ^ ": " ^ string_of_outcome outcome
       (*" with time " ^ " (" ^ space_implode "; " (map (fn (s, t) => (s ^ ": " ^ string_of_int t)) timing) ^ ")"*)
       (*^ "\n" ^ string_of_reports reports*)
--- a/src/Tools/quickcheck.ML	Wed Mar 23 08:50:31 2011 +0100
+++ b/src/Tools/quickcheck.ML	Wed Mar 23 08:50:32 2011 +0100
@@ -19,33 +19,36 @@
   val timeout : real Config.T
   val finite_types : bool Config.T
   val finite_type_size : int Config.T
-  datatype report = Report of
-    { iterations : int, raised_match_errors : int,
-      satisfied_assms : int list, positive_concl_tests : int }
   datatype expectation = No_Expectation | No_Counterexample | Counterexample;
   datatype test_params = Test_Params of {default_type: typ list, expect : expectation};
   val test_params_of : Proof.context -> test_params
   val map_test_params : (typ list * expectation -> typ list * expectation)
     -> Context.generic -> Context.generic
+  datatype report = Report of
+    { iterations : int, raised_match_errors : int,
+      satisfied_assms : int list, positive_concl_tests : int }
+  (* registering generators *)
   val add_generator:
     string * (Proof.context -> term * term list -> int -> term list option * report option)
       -> Context.generic -> Context.generic
   val add_batch_generator:
     string * (Proof.context -> term list -> (int -> term list option) list)
       -> Context.generic -> Context.generic
+  (* quickcheck's result *)
   datatype result =
     Result of
      {counterexample : (string * term) list option,
       evaluation_terms : (term * term) list option,
       timings : (string * int) list,
       reports : (int * report) list}
+  val counterexample_of : result -> (string * term) list option
+  val timings_of : result -> (string * int) list
   (* testing terms and proof states *)
   val test_term: 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 quickcheck: (string * string list) list -> int -> Proof.state -> (string * term) list option
-  
   (* testing a batch of terms *)
   val test_terms: Proof.context -> term list -> (string * term) list option list option
 end;