--- a/src/HOL/Mutabelle/mutabelle_extra.ML Sat Feb 11 11:36:21 2012 +0100
+++ b/src/HOL/Mutabelle/mutabelle_extra.ML Sat Feb 11 11:36:23 2012 +0100
@@ -38,7 +38,7 @@
val string_for_report : report -> string
val write_report : string -> report -> unit
val mutate_theorems_and_write_report :
- theory -> mtd list -> thm list -> string -> unit
+ theory -> int -> mtd list -> thm list -> string -> unit
val random_seed : real Unsynchronized.ref
end;
@@ -51,7 +51,6 @@
(* mutation options *)
-val max_mutants = 4
val num_mutations = 1
(* soundness check: *)
(*val max_mutants = 10
@@ -396,7 +395,7 @@
end
(* (theory -> thm -> bool -> term list -> mtd list -> 'a) -> theory -> mtd list -> thm -> 'a *)
-fun mutate_theorem create_entry thy mtds thm =
+fun mutate_theorem create_entry thy max_mutants mtds thm =
let
val exec = is_executable_thm thy thm
val _ = tracing (if exec then "EXEC" else "NOEXEC")
@@ -434,7 +433,7 @@
end
(* theory -> mtd list -> thm list -> report *)
-val mutate_theorems = map ooo mutate_theorem
+val mutate_theorems = map oooo mutate_theorem
fun string_of_mutant_subentry thy thm_name (t, results) =
"mutant: " ^ Syntax.string_of_term_global thy t ^ "\n" ^
@@ -499,7 +498,7 @@
File.write (Path.explode file_name) o string_for_report
(* theory -> mtd list -> thm list -> string -> unit *)
-fun mutate_theorems_and_write_report thy mtds thms file_name =
+fun mutate_theorems_and_write_report thy max_mutants mtds thms file_name =
let
val _ = Output.urgent_message "Starting Mutabelle..."
val ctxt = Proof_Context.init_global thy
@@ -522,7 +521,7 @@
"size: " ^ string_of_int (Config.get ctxt Quickcheck.size) ^
"; iterations: " ^ string_of_int (Config.get ctxt Quickcheck.iterations) ^ "\n" ^
"Isabelle environment = ISABELLE_GHC: " ^ getenv "ISABELLE_GHC" ^ "\n");
- map (File.append path o gen_string_for_entry o mutate_theorem gen_create_entry thy mtds) thms;
+ map (File.append path o gen_string_for_entry o mutate_theorem gen_create_entry thy max_mutants mtds) thms;
()
end