--- 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;