moving some common functions from quickcheck to the more HOL-specific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
1 (* Title: HOL/Mutabelle/mutabelle_extra.ML
2 Author: Stefan Berghofer, Jasmin Blanchette, Lukas Bulwahn, TU Muenchen
4 Invokation of Counterexample generators.
7 signature MUTABELLE_EXTRA =
10 val take_random : int -> 'a list -> 'a list
12 datatype outcome = GenuineCex | PotentialCex | NoCex | Donno | Timeout | Error | Solved | Unsolved
13 type timings = (string * int) list
15 type mtd = string * (theory -> term -> outcome * timings)
17 type mutant_subentry = term * (string * (outcome * timings)) list
18 type detailed_entry = string * bool * term * mutant_subentry list
20 type subentry = string * int * int * int * int * int * int
21 type entry = string * bool * subentry list
22 type report = entry list
24 val quickcheck_mtd : (Proof.context -> Proof.context) -> string -> mtd
26 val solve_direct_mtd : mtd
27 val try_methods_mtd : mtd
29 val sledgehammer_mtd : mtd
37 val freezeT : term -> term
38 val thms_of : bool -> theory -> thm list
40 val string_for_report : report -> string
41 val write_report : string -> report -> unit
42 val mutate_theorems_and_write_report :
43 theory -> mtd list -> thm list -> string -> unit
45 val random_seed : real Unsynchronized.ref
48 structure MutabelleExtra : MUTABELLE_EXTRA =
51 (* Own seed; can't rely on the Isabelle one to stay the same *)
52 val random_seed = Unsynchronized.ref 1.0;
55 (* mutation options *)
57 val num_mutations = 1*)
58 (* soundness check: *)
62 (* quickcheck options *)
63 (*val quickcheck_generator = "SML"*)
65 (* Another Random engine *)
69 fun rmod x y = x - y * Real.realFloor (x / y);
76 fun random () = CRITICAL (fn () =>
77 let val r = rmod (a * ! random_seed) m
78 in (random_seed := r; r) end);
82 fun random_range l h =
83 if h < l orelse l < 0 then raise RANDOM
84 else l + Real.floor (rmod (random ()) (real (h - l + 1)));
86 fun take_random 0 _ = []
87 | take_random _ [] = []
89 let val j = random_range 0 (length xs - 1) in
90 Library.nth xs j :: take_random (n - 1) (nth_drop j xs)
93 (* possible outcomes *)
95 datatype outcome = GenuineCex | PotentialCex | NoCex | Donno | Timeout | Error | Solved | Unsolved
97 fun string_of_outcome GenuineCex = "GenuineCex"
98 | string_of_outcome PotentialCex = "PotentialCex"
99 | string_of_outcome NoCex = "NoCex"
100 | string_of_outcome Donno = "Donno"
101 | string_of_outcome Timeout = "Timeout"
102 | string_of_outcome Error = "Error"
103 | string_of_outcome Solved = "Solved"
104 | string_of_outcome Unsolved = "Unsolved"
106 type timings = (string * int) list
108 type mtd = string * (theory -> term -> outcome * timings)
110 type mutant_subentry = term * (string * (outcome * timings)) list
111 type detailed_entry = string * bool * term * mutant_subentry list
113 type subentry = string * int * int * int * int * int * int
114 type entry = string * bool * subentry list
115 type report = entry list
117 (* possible invocations *)
121 fun invoke_quickcheck change_options quickcheck_generator thy t =
122 TimeLimit.timeLimit (seconds (!Try.auto_time_limit))
125 val ctxt' = change_options (Proof_Context.init_global thy)
126 val [result] = case Quickcheck.active_testers ctxt' of
127 [] => error "No active testers for quickcheck"
128 | [tester] => tester ctxt' (false, false) [] [(t, [])]
129 | _ => error "Multiple active testers for quickcheck"
131 case Quickcheck.counterexample_of result of
132 NONE => (NoCex, Quickcheck.timings_of result)
133 | SOME _ => (GenuineCex, Quickcheck.timings_of result)
135 handle TimeLimit.TimeOut =>
136 (Timeout, [("timelimit", Real.floor (!Try.auto_time_limit))])
138 fun quickcheck_mtd change_options quickcheck_generator =
139 ("quickcheck_" ^ quickcheck_generator, invoke_quickcheck change_options quickcheck_generator)
143 fun invoke_solve_direct thy t =
145 val state = Proof.theorem NONE (K I) (map (single o rpair []) [t]) (Proof_Context.init_global thy)
147 case Solve_Direct.solve_direct state of
148 (true, _) => (Solved, [])
149 | (false, _) => (Unsolved, [])
152 val solve_direct_mtd = ("solve_direct", invoke_solve_direct)
156 fun invoke_try_methods thy t =
158 val state = Proof.theorem NONE (K I) (map (single o rpair []) [t]) (Proof_Context.init_global thy)
160 case Try_Methods.try_methods (SOME (seconds 5.0)) ([], [], [], []) state of
162 | false => (Unsolved, [])
165 val try_methods_mtd = ("try_methods", invoke_try_methods)
169 fun invoke_sledgehammer thy t =
170 if can (Goal.prove_global thy (Term.add_free_names t []) [] t)
171 (fn {context, ...} => Sledgehammer_Tactics.sledgehammer_with_metis_tac context 1) then
174 (Unsolved, ([], NONE))
176 val sledgehammer_mtd = ("sledgehammer", invoke_sledgehammer)
179 fun invoke_refute thy t =
181 val res = MyRefute.refute_term thy [] t
182 val _ = Output.urgent_message ("Refute: " ^ res)
185 "genuine" => GenuineCex
186 | "likely_genuine" => GenuineCex
187 | "potential" => PotentialCex
192 handle MyRefute.REFUTE (loc, details) =>
193 (error ("Unhandled Refute error (" ^ quote loc ^ "): " ^ details ^
195 val refute_mtd = ("refute", invoke_refute)
200 fun invoke_nitpick thy t =
202 val ctxt = Proof_Context.init_global thy
203 val state = Proof.init ctxt
204 val (res, _) = Nitpick.pick_nits_in_term state
205 (Nitpick_Isar.default_params thy []) Nitpick.Normal 1 1 1 [] [] t
206 val _ = Output.urgent_message ("Nitpick: " ^ res)
208 (rpair []) (case res of
209 "genuine" => GenuineCex
210 | "likely_genuine" => GenuineCex
211 | "potential" => PotentialCex
217 val nitpick_mtd = ("nitpick", invoke_nitpick)
219 (* filtering forbidden theorems and mutants *)
221 val comms = [@{const_name HOL.eq}, @{const_name HOL.disj}, @{const_name HOL.conj}]
224 [(* (@{const_name "power"}, "'a"), *)
225 (*(@{const_name induct_equal}, "'a"),
226 (@{const_name induct_implies}, "'a"),
227 (@{const_name induct_conj}, "'a"),*)
228 (@{const_name "undefined"}, "'a"),
229 (@{const_name "default"}, "'a"),
230 (@{const_name "dummy_pattern"}, "'a::{}"),
231 (@{const_name "HOL.simp_implies"}, "prop => prop => prop"),
232 (@{const_name "bot_fun_inst.bot_fun"}, "'a"),
233 (@{const_name "top_fun_inst.top_fun"}, "'a"),
234 (@{const_name "Pure.term"}, "'a"),
235 (@{const_name "top_class.top"}, "'a"),
236 (@{const_name "Quotient.Quot_True"}, "'a")(*,
237 (@{const_name "uminus"}, "'a"),
238 (@{const_name "Nat.size"}, "'a"),
239 (@{const_name "Groups.abs"}, "'a") *)]
242 ["finite_intvl_succ_class",
245 val forbidden_consts =
246 [@{const_name nibble_pair_of_char}, @{const_name "TYPE"}]
248 fun is_forbidden_theorem (s, th) =
249 let val consts = Term.add_const_names (prop_of th) [] in
250 exists (member (op =) (space_explode "." s)) forbidden_thms orelse
251 exists (member (op =) forbidden_consts) consts orelse
252 length (space_explode "." s) <> 2 orelse
253 String.isPrefix "type_definition" (List.last (space_explode "." s)) orelse
254 String.isSuffix "_def" s orelse
255 String.isSuffix "_raw" s orelse
256 String.isPrefix "term_of" (List.last (space_explode "." s))
259 val forbidden_mutant_constnames =
261 "HOL.induct_implies",
263 @{const_name undefined},
264 @{const_name default},
265 @{const_name dummy_pattern},
266 @{const_name "HOL.simp_implies"},
267 @{const_name "bot_fun_inst.bot_fun"},
268 @{const_name "top_fun_inst.top_fun"},
269 @{const_name "Pure.term"},
270 @{const_name "top_class.top"},
271 (*@{const_name "HOL.equal"},*)
272 @{const_name "Quotient.Quot_True"},
273 @{const_name "equal_fun_inst.equal_fun"},
274 @{const_name "equal_bool_inst.equal_bool"},
275 @{const_name "ord_fun_inst.less_eq_fun"},
276 @{const_name "ord_fun_inst.less_fun"},
277 @{const_name Meson.skolem},
278 @{const_name ATP.fequal},
279 @{const_name transfer_morphism},
280 @{const_name enum_prod_inst.enum_all_prod},
281 @{const_name enum_prod_inst.enum_ex_prod}
282 (*@{const_name "==>"}, @{const_name "=="}*)]
284 val forbidden_mutant_consts =
286 (@{const_name "Groups.zero_class.zero"}, @{typ "prop => prop => prop"}),
287 (@{const_name "Groups.one_class.one"}, @{typ "prop => prop => prop"}),
288 (@{const_name "Groups.plus_class.plus"}, @{typ "prop => prop => prop"}),
289 (@{const_name "Groups.minus_class.minus"}, @{typ "prop => prop => prop"}),
290 (@{const_name "Groups.times_class.times"}, @{typ "prop => prop => prop"}),
291 (@{const_name "Fields.inverse_class.divide"}, @{typ "prop => prop => prop"}),
292 (@{const_name "Lattices.inf_class.inf"}, @{typ "prop => prop => prop"}),
293 (@{const_name "Lattices.sup_class.sup"}, @{typ "prop => prop => prop"}),
294 (@{const_name "Orderings.bot_class.bot"}, @{typ "prop => prop => prop"}),
295 (@{const_name "Orderings.ord_class.min"}, @{typ "prop => prop => prop"}),
296 (@{const_name "Orderings.ord_class.max"}, @{typ "prop => prop => prop"}),
297 (@{const_name "Divides.div_class.mod"}, @{typ "prop => prop => prop"}),
298 (@{const_name "Divides.div_class.div"}, @{typ "prop => prop => prop"}),
299 (@{const_name "GCD.gcd_class.gcd"}, @{typ "prop => prop => prop"}),
300 (@{const_name "GCD.gcd_class.lcm"}, @{typ "prop => prop => prop"}),
301 (@{const_name "Orderings.bot_class.bot"}, @{typ "bool => prop"}),
302 (@{const_name "Groups.one_class.one"}, @{typ "bool => prop"}),
303 (@{const_name "Groups.zero_class.zero"},@{typ "bool => prop"})]
305 fun is_forbidden_mutant t =
307 val const_names = Term.add_const_names t []
308 val consts = Term.add_consts t []
310 exists (String.isPrefix "Nitpick") const_names orelse
311 exists (String.isSubstring "_sumC") const_names orelse
312 exists (member (op =) forbidden_mutant_constnames) const_names orelse
313 exists (member (op =) forbidden_mutant_consts) consts
316 (* executable via quickcheck *)
318 fun is_executable_term thy t =
320 val ctxt = Proof_Context.init_global thy
322 can (TimeLimit.timeLimit (seconds 2.0)
323 (Quickcheck.test_terms
324 ((Config.put Quickcheck.finite_types true #>
325 Config.put Quickcheck.finite_type_size 1 #>
326 Config.put Quickcheck.size 1 #> Config.put Quickcheck.iterations 1) ctxt)
327 (false, false) [])) (map (rpair [] o Object_Logic.atomize_term thy)
328 (fst (Variable.import_terms true [t] ctxt)))
331 fun is_executable_thm thy th = is_executable_term thy (prop_of th)
334 map_types (map_type_tvar (fn ((a, i), S) =>
335 TFree (if i = 0 then a else a ^ "_" ^ string_of_int i, S)))
337 fun thms_of all thy =
339 (fn th => (all orelse Context.theory_name (theory_of_thm th) = Context.theory_name thy)
340 (* andalso is_executable_thm thy th *))
341 (map snd (filter_out is_forbidden_theorem (Mutabelle.all_unconcealed_thms_of thy)))
343 fun count x = (length oo filter o equal) x
345 fun cpu_time description e =
346 let val ({cpu, ...}, result) = Timing.timing e ()
347 in (result, (description, Time.toMilliseconds cpu)) end
349 fun unsafe_invoke_mtd thy (mtd_name, invoke_mtd) t =
351 val _ = Output.urgent_message ("Invoking " ^ mtd_name)
352 val ((res, (timing, reports)), time) = cpu_time "total time" (fn () => invoke_mtd thy t
353 handle ERROR s => (tracing s; (Error, ([], NONE))))
354 val _ = Output.urgent_message (" Done")
355 in (res, (time :: timing, reports)) end
357 fun safe_invoke_mtd thy (mtd_name, invoke_mtd) t =
359 val _ = Output.urgent_message ("Invoking " ^ mtd_name)
360 val (res, timing) = (*cpu_time "total time"
361 (fn () => *)case try (invoke_mtd thy) t of
362 SOME (res, timing) => (res, timing)
363 | NONE => (Output.urgent_message ("**** PROBLEMS WITH " ^ Syntax.string_of_term_global thy t);
365 val _ = Output.urgent_message (" Done")
368 (* theory -> term list -> mtd -> subentry *)
370 fun test_mutants_using_one_method thy mutants (mtd_name, invoke_mtd) =
372 val res = map (fst o safe_invoke_mtd thy (mtd_name, invoke_mtd)) mutants
374 (mtd_name, count GenuineCex res, count PotentialCex res, count NoCex res,
375 count Donno res, count Timeout res, count Error res)
378 (* creating entries *)
380 fun create_entry thy thm exec mutants mtds =
381 (Thm.get_name_hint thm, exec, map (test_mutants_using_one_method thy mutants) mtds)
383 fun create_detailed_entry thy thm exec mutants mtds =
385 fun create_mutant_subentry mutant = (mutant,
386 map (fn (mtd_name, invoke_mtd) =>
387 (mtd_name, safe_invoke_mtd thy (mtd_name, invoke_mtd) mutant)) mtds)
389 (Thm.get_name_hint thm, exec, prop_of thm, map create_mutant_subentry mutants)
392 (* (theory -> thm -> bool -> term list -> mtd list -> 'a) -> theory -> mtd list -> thm -> 'a *)
393 fun mutate_theorem create_entry thy mtds thm =
395 val exec = is_executable_thm thy thm
396 val _ = tracing (if exec then "EXEC" else "NOEXEC")
398 (if num_mutations = 0 then
401 Mutabelle.mutate_mix (Thm.prop_of thm) thy comms forbidden
403 |> tap (fn muts => tracing ("mutants: " ^ string_of_int (length muts)))
404 |> filter_out is_forbidden_mutant
408 val _ = Output.urgent_message ("BEFORE PARTITION OF " ^
409 string_of_int (length mutants) ^ " MUTANTS")
410 val (execs, noexecs) = List.partition (is_executable_term thy) (take_random (20 * max_mutants) mutants)
411 val _ = tracing ("AFTER PARTITION (" ^ string_of_int (length execs) ^
412 " vs " ^ string_of_int (length noexecs) ^ ")")
414 execs @ take_random (Int.max (0, max_mutants - length execs)) noexecs
418 val mutants = mutants
419 |> map Mutabelle.freeze |> map freezeT
420 (* |> filter (not o is_forbidden_mutant) *)
421 |> map_filter (try (Sign.cert_term thy))
422 |> filter (is_some o try (Thm.cterm_of thy))
423 |> filter (is_some o try (Syntax.check_term (Proof_Context.init_global thy)))
424 |> take_random max_mutants
425 val _ = map (fn t => Output.urgent_message ("MUTANT: " ^ Syntax.string_of_term_global thy t)) mutants
427 create_entry thy thm exec mutants mtds
430 (* theory -> mtd list -> thm list -> report *)
431 val mutate_theorems = map ooo mutate_theorem
433 fun string_of_mutant_subentry thy thm_name (t, results) =
434 "mutant: " ^ Syntax.string_of_term_global thy t ^ "\n" ^
436 (map (fn (mtd_name, (outcome, timing)) => mtd_name ^ ": " ^ string_of_outcome outcome) results) ^
439 (* string -> string *)
440 val unyxml = XML.content_of o YXML.parse_body
442 fun string_of_mutant_subentry' thy thm_name (t, results) =
444 (* fun string_of_report (Quickcheck.Report {iterations = i, raised_match_errors = e,
445 satisfied_assms = s, positive_concl_tests = p}) =
446 "errors: " ^ string_of_int e ^ "; conclusion tests: " ^ string_of_int p
447 fun string_of_reports NONE = ""
448 | string_of_reports (SOME reports) =
449 cat_lines (map (fn (size, [report]) =>
450 "size " ^ string_of_int size ^ ": " ^ string_of_report report) (rev reports))*)
451 fun string_of_mtd_result (mtd_name, (outcome, timing)) =
452 mtd_name ^ ": " ^ string_of_outcome outcome
453 (*" with time " ^ " (" ^ space_implode "; " (map (fn (s, t) => (s ^ ": " ^ string_of_int t)) timing) ^ ")"*)
454 (*^ "\n" ^ string_of_reports reports*)
456 "mutant of " ^ thm_name ^ ":\n"
457 ^ unyxml (Syntax.string_of_term_global thy t) ^ "\n" ^ space_implode "; " (map string_of_mtd_result results)
460 fun string_of_detailed_entry thy (thm_name, exec, t, mutant_subentries) =
461 thm_name ^ " " ^ (if exec then "[exe]" else "[noexe]") ^ ": " ^
462 Syntax.string_of_term_global thy t ^ "\n" ^
463 cat_lines (map (string_of_mutant_subentry' thy thm_name) mutant_subentries) ^ "\n"
465 fun theoryfile_string_of_mutant_subentry thy thm_name (i, (t, results)) =
466 "lemma " ^ thm_name ^ "_" ^ string_of_int (i + 1) ^ ":\n" ^
467 "\"" ^ unyxml (Syntax.string_of_term_global thy t) ^
468 "\" \nquickcheck\noops\n"
470 fun theoryfile_string_of_detailed_entry thy (thm_name, exec, t, mutant_subentries) =
471 "subsubsection {* mutants of " ^ thm_name ^ " *}\n\n" ^
473 (theoryfile_string_of_mutant_subentry thy thm_name) mutant_subentries) ^ "\n"
475 (* subentry -> string *)
476 fun string_for_subentry (mtd_name, genuine_cex, potential_cex, no_cex, donno,
478 " " ^ mtd_name ^ ": " ^ string_of_int genuine_cex ^ "+ " ^
479 string_of_int potential_cex ^ "= " ^ string_of_int no_cex ^ "- " ^
480 string_of_int donno ^ "? " ^ string_of_int timeout ^ "T " ^
481 string_of_int error ^ "!"
483 (* entry -> string *)
484 fun string_for_entry (thm_name, exec, subentries) =
485 thm_name ^ " " ^ (if exec then "[exe]" else "[noexe]") ^ ":\n" ^
486 cat_lines (map string_for_subentry subentries) ^ "\n"
488 (* report -> string *)
489 fun string_for_report report = cat_lines (map string_for_entry report)
491 (* string -> report -> unit *)
492 fun write_report file_name =
493 File.write (Path.explode file_name) o string_for_report
495 (* theory -> mtd list -> thm list -> string -> unit *)
496 fun mutate_theorems_and_write_report thy mtds thms file_name =
498 val _ = Output.urgent_message "Starting Mutabelle..."
499 val ctxt = Proof_Context.init_global thy
500 val path = Path.explode file_name
501 (* for normal report: *)
503 val (gen_create_entry, gen_string_for_entry) = (create_entry, string_for_entry)
505 (* for detailled report: *)
506 val (gen_create_entry, gen_string_for_entry) = (create_detailed_entry, string_of_detailed_entry thy)
507 (* for theory creation: *)
508 (*val (gen_create_entry, gen_string_for_entry) = (create_detailed_entry, theoryfile_string_of_detailed_entry thy)*)
511 "Mutation options = " ^
512 "max_mutants: " ^ string_of_int max_mutants ^
513 "; num_mutations: " ^ string_of_int num_mutations ^ "\n" ^
515 (*"quickcheck_generator: " ^ quickcheck_generator ^ ";*)
516 "size: " ^ string_of_int (Config.get ctxt Quickcheck.size) ^
517 "; iterations: " ^ string_of_int (Config.get ctxt Quickcheck.iterations) ^ "\n" ^
518 "Isabelle environment = ISABELLE_GHC: " ^ getenv "ISABELLE_GHC" ^ "\n");
519 map (File.append path o gen_string_for_entry o mutate_theorem gen_create_entry thy mtds) thms;