# HG changeset patch # User bulwahn # Date 1267102894 -3600 # Node ID 6ac5b81a763d719ccff13ef2447244f646d17949 # Parent d0c779d012dc26846401106b45e75fd7c3143a10 adopting Mutabelle to quickcheck reporting; improving quickcheck reporting diff -r d0c779d012dc -r 6ac5b81a763d src/HOL/Mutabelle/mutabelle_extra.ML --- a/src/HOL/Mutabelle/mutabelle_extra.ML Thu Feb 25 10:04:50 2010 +0100 +++ b/src/HOL/Mutabelle/mutabelle_extra.ML Thu Feb 25 14:01:34 2010 +0100 @@ -12,9 +12,9 @@ datatype outcome = GenuineCex | PotentialCex | NoCex | Donno | Timeout | Error type timing = (string * int) list -type mtd = string * (theory -> term -> outcome * timing) +type mtd = string * (theory -> term -> outcome * (timing * (int * Quickcheck.report list) list option)) -type mutant_subentry = term * (string * (outcome * timing)) list +type mutant_subentry = term * (string * (outcome * (timing * Quickcheck.report option))) list type detailed_entry = string * bool * term * mutant_subentry list type subentry = string * int * int * int * int * int * int @@ -54,7 +54,7 @@ (* quickcheck options *) (*val quickcheck_generator = "SML"*) -val iterations = 1 +val iterations = 100 val size = 5 exception RANDOM; @@ -79,9 +79,9 @@ datatype outcome = GenuineCex | PotentialCex | NoCex | Donno | Timeout | Error type timing = (string * int) list -type mtd = string * (theory -> term -> outcome * timing) +type mtd = string * (theory -> term -> outcome * (timing * (int * Quickcheck.report list) list option)) -type mutant_subentry = term * (string * (outcome * timing)) list +type mutant_subentry = term * (string * (outcome * (timing * Quickcheck.report option))) list type detailed_entry = string * bool * term * mutant_subentry list type subentry = string * int * int * int * int * int * int @@ -97,11 +97,11 @@ fun invoke_quickcheck quickcheck_generator thy t = TimeLimit.timeLimit (Time.fromSeconds (! Auto_Counterexample.time_limit)) (fn _ => - case Quickcheck.timed_test_term (ProofContext.init thy) false (SOME quickcheck_generator) + case Quickcheck.gen_test_term (ProofContext.init thy) true true (SOME quickcheck_generator) size iterations (preprocess thy [] t) of - (NONE, time_report) => (NoCex, time_report) - | (SOME _, time_report) => (GenuineCex, time_report)) () - handle TimeLimit.TimeOut => (Timeout, [("timelimit", !Auto_Counterexample.time_limit)]) + (NONE, (time_report, report)) => (NoCex, (time_report, report)) + | (SOME _, (time_report, report)) => (GenuineCex, (time_report, report))) () + handle TimeLimit.TimeOut => (Timeout, ([("timelimit", !Auto_Counterexample.time_limit)], NONE)) fun quickcheck_mtd quickcheck_generator = ("quickcheck_" ^ quickcheck_generator, invoke_quickcheck quickcheck_generator) @@ -258,13 +258,13 @@ fun safe_invoke_mtd thy (mtd_name, invoke_mtd) t = let val _ = priority ("Invoking " ^ mtd_name) - val ((res, timing), time) = cpu_time "total time" + val ((res, (timing, reports)), time) = cpu_time "total time" (fn () => case try (invoke_mtd thy) t of - SOME (res, timing) => (res, timing) + SOME (res, (timing, reports)) => (res, (timing, reports)) | NONE => (priority ("**** PROBLEMS WITH " ^ Syntax.string_of_term_global thy t); - (Error , []))) + (Error , ([], NONE)))) val _ = priority (" Done") - in (res, time :: timing) end + in (res, (time :: timing, reports)) end (* theory -> term list -> mtd -> subentry *) (* @@ -341,10 +341,21 @@ "\n" fun string_of_mutant_subentry' thy thm_name (t, results) = - "mutant of " ^ thm_name ^ ":" ^ - cat_lines (map (fn (mtd_name, (outcome, timing)) => + let + 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))) = mtd_name ^ ": " ^ string_of_outcome outcome ^ "; " ^ - space_implode "; " (map (fn (s, t) => (s ^ ": " ^ string_of_int t)) timing)) results) + space_implode "; " (map (fn (s, t) => (s ^ ": " ^ string_of_int t)) timing) + ^ "\n" ^ string_of_reports reports + in + "mutant of " ^ thm_name ^ ":\n" ^ cat_lines (map string_of_mtd_result results) + end fun string_of_detailed_entry thy (thm_name, exec, t, mutant_subentries) = thm_name ^ " " ^ (if exec then "[exe]" else "[noexe]") ^ ": " ^ diff -r d0c779d012dc -r 6ac5b81a763d src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML Thu Feb 25 10:04:50 2010 +0100 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML Thu Feb 25 14:01:34 2010 +0100 @@ -217,7 +217,7 @@ fun try' j = if j <= i then let - val _ = priority ("Executing depth " ^ string_of_int j) + val _ = if quiet then () else priority ("Executing depth " ^ string_of_int j) in case f j handle Match => (if quiet then () else warning "Exception Match raised during quickcheck"; NONE) diff -r d0c779d012dc -r 6ac5b81a763d src/Tools/quickcheck.ML --- a/src/Tools/quickcheck.ML Thu Feb 25 10:04:50 2010 +0100 +++ b/src/Tools/quickcheck.ML Thu Feb 25 14:01:34 2010 +0100 @@ -12,7 +12,7 @@ { iterations : int, raised_match_errors : int, satisfied_assms : int list, positive_concl_tests : int } val gen_test_term: Proof.context -> bool -> bool -> string option -> int -> int -> term -> - ((string * term) list option * ((string * int) list * (int * report list) list)) + (string * term) list option * ((string * int) list * ((int * report list) list) option) val test_term: Proof.context -> bool -> string option -> int -> int -> term -> (string * term) list option val add_generator: @@ -167,7 +167,7 @@ (fn result => case result of NONE => NONE | SOME ts => SOME (names ~~ ts)) (with_size 1 [])) in - (result, ([exec_time, comp_time], reports)) + (result, ([exec_time, comp_time], if report then SOME reports else NONE)) end; fun test_term ctxt quiet generator_name size i t = @@ -226,11 +226,12 @@ Pretty.chunks (Pretty.str (string_of_int (i + 1) ^ ". generator:\n") :: pretty_report report)) reports -fun pretty_reports ctxt reports = +fun pretty_reports ctxt (SOME reports) = Pretty.chunks (Pretty.str "Quickcheck report:" :: maps (fn (size, reports) => Pretty.str ("size " ^ string_of_int size ^ ":") :: pretty_reports' reports @ [Pretty.brk 1]) (rev reports)) + | pretty_reports ctxt NONE = Pretty.str "" fun pretty_counterex_and_reports ctxt (cex, (timing, reports)) = Pretty.chunks [pretty_counterex ctxt cex, pretty_reports ctxt reports]