8 sig |
8 sig |
9 |
9 |
10 val take_random : int -> 'a list -> 'a list |
10 val take_random : int -> 'a list -> 'a list |
11 |
11 |
12 datatype outcome = GenuineCex | PotentialCex | NoCex | Donno | Timeout | Error | Solved | Unsolved |
12 datatype outcome = GenuineCex | PotentialCex | NoCex | Donno | Timeout | Error | Solved | Unsolved |
13 type timing = (string * int) list |
13 type timings = (string * int) list |
14 |
14 |
15 type mtd = string * (theory -> term -> outcome * (timing * (int * Quickcheck.report list) list option)) |
15 type mtd = string * (theory -> term -> outcome * timings) |
16 |
16 |
17 type mutant_subentry = term * (string * (outcome * (timing * Quickcheck.report option))) list |
17 type mutant_subentry = term * (string * (outcome * timings)) list |
18 type detailed_entry = string * bool * term * mutant_subentry list |
18 type detailed_entry = string * bool * term * mutant_subentry list |
19 |
19 |
20 type subentry = string * int * int * int * int * int * int |
20 type subentry = string * int * int * int * int * int * int |
21 type entry = string * bool * subentry list |
21 type entry = string * bool * subentry list |
22 type report = entry list |
22 type report = entry list |
101 | string_of_outcome Timeout = "Timeout" |
101 | string_of_outcome Timeout = "Timeout" |
102 | string_of_outcome Error = "Error" |
102 | string_of_outcome Error = "Error" |
103 | string_of_outcome Solved = "Solved" |
103 | string_of_outcome Solved = "Solved" |
104 | string_of_outcome Unsolved = "Unsolved" |
104 | string_of_outcome Unsolved = "Unsolved" |
105 |
105 |
106 type timing = (string * int) list |
106 type timings = (string * int) list |
107 |
107 |
108 type mtd = string * (theory -> term -> outcome * (timing * (int * Quickcheck.report list) list option)) |
108 type mtd = string * (theory -> term -> outcome * timings) |
109 |
109 |
110 type mutant_subentry = term * (string * (outcome * (timing * Quickcheck.report option))) list |
110 type mutant_subentry = term * (string * (outcome * timings)) list |
111 type detailed_entry = string * bool * term * mutant_subentry list |
111 type detailed_entry = string * bool * term * mutant_subentry list |
112 |
112 |
113 type subentry = string * int * int * int * int * int * int |
113 type subentry = string * int * int * int * int * int * int |
114 type entry = string * bool * subentry list |
114 type entry = string * bool * subentry list |
115 type report = entry list |
115 type report = entry list |
119 (** quickcheck **) |
119 (** quickcheck **) |
120 |
120 |
121 fun invoke_quickcheck change_options quickcheck_generator thy t = |
121 fun invoke_quickcheck change_options quickcheck_generator thy t = |
122 TimeLimit.timeLimit (seconds (!Auto_Tools.time_limit)) |
122 TimeLimit.timeLimit (seconds (!Auto_Tools.time_limit)) |
123 (fn _ => |
123 (fn _ => |
124 case Quickcheck.test_goal_terms (change_options (ProofContext.init_global thy)) |
124 let |
125 (false, false) [] [(t, [])] of |
125 val [result] = Quickcheck.test_goal_terms (change_options (ProofContext.init_global thy)) |
126 (NONE, _) => (NoCex, ([], NONE)) |
126 (false, false) [] [(t, [])] |
127 | (SOME _, _) => (GenuineCex, ([], NONE))) () |
127 in |
|
128 case Quickcheck.counterexample_of result of |
|
129 NONE => (NoCex, Quickcheck.timings_of result) |
|
130 | SOME _ => (GenuineCex, Quickcheck.timings_of result) |
|
131 end) () |
128 handle TimeLimit.TimeOut => |
132 handle TimeLimit.TimeOut => |
129 (Timeout, ([("timelimit", Real.floor (!Auto_Tools.time_limit))], NONE)) |
133 (Timeout, [("timelimit", Real.floor (!Auto_Tools.time_limit))]) |
130 |
134 |
131 fun quickcheck_mtd change_options quickcheck_generator = |
135 fun quickcheck_mtd change_options quickcheck_generator = |
132 ("quickcheck_" ^ quickcheck_generator, invoke_quickcheck change_options quickcheck_generator) |
136 ("quickcheck_" ^ quickcheck_generator, invoke_quickcheck change_options quickcheck_generator) |
133 |
137 |
134 (** solve direct **) |
138 (** solve direct **) |
136 fun invoke_solve_direct thy t = |
140 fun invoke_solve_direct thy t = |
137 let |
141 let |
138 val state = Proof.theorem NONE (K I) (map (single o rpair []) [t]) (ProofContext.init_global thy) |
142 val state = Proof.theorem NONE (K I) (map (single o rpair []) [t]) (ProofContext.init_global thy) |
139 in |
143 in |
140 case Solve_Direct.solve_direct false state of |
144 case Solve_Direct.solve_direct false state of |
141 (true, _) => (Solved, ([], NONE)) |
145 (true, _) => (Solved, []) |
142 | (false, _) => (Unsolved, ([], NONE)) |
146 | (false, _) => (Unsolved, []) |
143 end |
147 end |
144 |
148 |
145 val solve_direct_mtd = ("solve_direct", invoke_solve_direct) |
149 val solve_direct_mtd = ("solve_direct", invoke_solve_direct) |
146 |
150 |
147 (** try **) |
151 (** try **) |
149 fun invoke_try thy t = |
153 fun invoke_try thy t = |
150 let |
154 let |
151 val state = Proof.theorem NONE (K I) (map (single o rpair []) [t]) (ProofContext.init_global thy) |
155 val state = Proof.theorem NONE (K I) (map (single o rpair []) [t]) (ProofContext.init_global thy) |
152 in |
156 in |
153 case Try.invoke_try (SOME (seconds 5.0)) ([], [], []) state of |
157 case Try.invoke_try (SOME (seconds 5.0)) ([], [], []) state of |
154 true => (Solved, ([], NONE)) |
158 true => (Solved, []) |
155 | false => (Unsolved, ([], NONE)) |
159 | false => (Unsolved, []) |
156 end |
160 end |
157 |
161 |
158 val try_mtd = ("try", invoke_try) |
162 val try_mtd = ("try", invoke_try) |
159 |
163 |
160 (** sledgehammer **) |
164 (** sledgehammer **) |
196 val state = Proof.init ctxt |
200 val state = Proof.init ctxt |
197 val (res, _) = Nitpick.pick_nits_in_term state |
201 val (res, _) = Nitpick.pick_nits_in_term state |
198 (Nitpick_Isar.default_params thy []) false 1 1 1 [] [] t |
202 (Nitpick_Isar.default_params thy []) false 1 1 1 [] [] t |
199 val _ = Output.urgent_message ("Nitpick: " ^ res) |
203 val _ = Output.urgent_message ("Nitpick: " ^ res) |
200 in |
204 in |
201 rpair ([], NONE) (case res of |
205 (rpair []) (case res of |
202 "genuine" => GenuineCex |
206 "genuine" => GenuineCex |
203 | "likely_genuine" => GenuineCex |
207 | "likely_genuine" => GenuineCex |
204 | "potential" => PotentialCex |
208 | "potential" => PotentialCex |
205 | "none" => NoCex |
209 | "none" => NoCex |
206 | "unknown" => Donno |
210 | "unknown" => Donno |
345 in (res, (time :: timing, reports)) end |
349 in (res, (time :: timing, reports)) end |
346 *) |
350 *) |
347 fun safe_invoke_mtd thy (mtd_name, invoke_mtd) t = |
351 fun safe_invoke_mtd thy (mtd_name, invoke_mtd) t = |
348 let |
352 let |
349 val _ = Output.urgent_message ("Invoking " ^ mtd_name) |
353 val _ = Output.urgent_message ("Invoking " ^ mtd_name) |
350 val (res, (timing, reports)) = (*cpu_time "total time" |
354 val (res, timing) = (*cpu_time "total time" |
351 (fn () => *)case try (invoke_mtd thy) t of |
355 (fn () => *)case try (invoke_mtd thy) t of |
352 SOME (res, (timing, reports)) => (res, (timing, reports)) |
356 SOME (res, timing) => (res, timing) |
353 | NONE => (Output.urgent_message ("**** PROBLEMS WITH " ^ Syntax.string_of_term_global thy t); |
357 | NONE => (Output.urgent_message ("**** PROBLEMS WITH " ^ Syntax.string_of_term_global thy t); |
354 (Error, ([], NONE))) |
358 (Error, [])) |
355 val _ = Output.urgent_message (" Done") |
359 val _ = Output.urgent_message (" Done") |
356 in (res, (timing, reports)) end |
360 in (res, timing) end |
357 |
361 |
358 (* theory -> term list -> mtd -> subentry *) |
362 (* theory -> term list -> mtd -> subentry *) |
359 |
363 |
360 fun test_mutants_using_one_method thy mutants (mtd_name, invoke_mtd) = |
364 fun test_mutants_using_one_method thy mutants (mtd_name, invoke_mtd) = |
361 let |
365 let |
429 (* string -> string *) |
433 (* string -> string *) |
430 val unyxml = XML.content_of o YXML.parse_body |
434 val unyxml = XML.content_of o YXML.parse_body |
431 |
435 |
432 fun string_of_mutant_subentry' thy thm_name (t, results) = |
436 fun string_of_mutant_subentry' thy thm_name (t, results) = |
433 let |
437 let |
434 fun string_of_report (Quickcheck.Report {iterations = i, raised_match_errors = e, |
438 (* fun string_of_report (Quickcheck.Report {iterations = i, raised_match_errors = e, |
435 satisfied_assms = s, positive_concl_tests = p}) = |
439 satisfied_assms = s, positive_concl_tests = p}) = |
436 "errors: " ^ string_of_int e ^ "; conclusion tests: " ^ string_of_int p |
440 "errors: " ^ string_of_int e ^ "; conclusion tests: " ^ string_of_int p |
437 fun string_of_reports NONE = "" |
441 fun string_of_reports NONE = "" |
438 | string_of_reports (SOME reports) = |
442 | string_of_reports (SOME reports) = |
439 cat_lines (map (fn (size, [report]) => |
443 cat_lines (map (fn (size, [report]) => |
440 "size " ^ string_of_int size ^ ": " ^ string_of_report report) (rev reports)) |
444 "size " ^ string_of_int size ^ ": " ^ string_of_report report) (rev reports))*) |
441 fun string_of_mtd_result (mtd_name, (outcome, (timing, reports))) = |
445 fun string_of_mtd_result (mtd_name, (outcome, timing)) = |
442 mtd_name ^ ": " ^ string_of_outcome outcome |
446 mtd_name ^ ": " ^ string_of_outcome outcome |
443 (*" with time " ^ " (" ^ space_implode "; " (map (fn (s, t) => (s ^ ": " ^ string_of_int t)) timing) ^ ")"*) |
447 (*" with time " ^ " (" ^ space_implode "; " (map (fn (s, t) => (s ^ ": " ^ string_of_int t)) timing) ^ ")"*) |
444 (*^ "\n" ^ string_of_reports reports*) |
448 (*^ "\n" ^ string_of_reports reports*) |
445 in |
449 in |
446 "mutant of " ^ thm_name ^ ":\n" |
450 "mutant of " ^ thm_name ^ ":\n" |