--- a/src/HOL/Mutabelle/MutabelleExtra.thy Mon Nov 22 11:34:58 2010 +0100
+++ b/src/HOL/Mutabelle/MutabelleExtra.thy Mon Nov 22 11:34:59 2010 +0100
@@ -1,58 +1,144 @@
theory MutabelleExtra
-imports Complex_Main SML_Quickcheck
-(*
- "~/Downloads/Jinja/J/TypeSafe"
- "~/Downloads/Jinja/J/Annotate"
- (* FIXME "Example" *)
- "~/Downloads/Jinja/J/execute_Bigstep"
- "~/Downloads/Jinja/J/execute_WellType"
- "~/Downloads/Jinja/JVM/JVMDefensive"
- "~/Downloads/Jinja/JVM/JVMListExample"
- "~/Downloads/Jinja/BV/BVExec"
- "~/Downloads/Jinja/BV/LBVJVM"
- "~/Downloads/Jinja/BV/BVNoTypeError"
- "~/Downloads/Jinja/BV/BVExample"
- "~/Downloads/Jinja/Compiler/TypeComp"
-*)
-(*"~/Downloads/NormByEval/NBE"*)
-uses "mutabelle.ML"
+imports Complex_Main
+(* "~/repos/afp/thys/AVL-Trees/AVL"
+ "~/repos/afp/thys/BinarySearchTree/BinaryTree"
+ "~/repos/afp/thys/Huffman/Huffman"
+ "~/repos/afp/thys/List-Index/List_Index"
+ "~/repos/afp/thys/Matrix/Matrix"
+ "~/repos/afp/thys/NormByEval/NBE"
+ "~/repos/afp/thys/Polynomials/Polynomial"
+ "~/repos/afp/thys/Presburger-Automata/Presburger_Automata"
+ "~/repos/afp/thys/Abstract-Rewriting/Abstract_Rewriting"*)
+uses
+ "mutabelle.ML"
"mutabelle_extra.ML"
begin
-(* FIXME !?!?! *)
-ML {* val old_tr = !Output.Private_Hooks.tracing_fn *}
-ML {* val old_wr = !Output.Private_Hooks.writeln_fn *}
-ML {* val old_ur = !Output.Private_Hooks.urgent_message_fn *}
-ML {* val old_wa = !Output.Private_Hooks.warning_fn *}
+
+section {* configuration *}
-quickcheck_params [size = 5, iterations = 1000]
+ML {* val log_directory = "" *}
+
+
+quickcheck_params [quiet, finite_types = false, report = false, size = 5, iterations = 1000]
+
(*
nitpick_params [timeout = 5, sat_solver = MiniSat, no_overlord, verbose, card = 1-5, iter = 1,2,4,8,12]
refute_params [maxtime = 10, minsize = 1, maxsize = 5, satsolver = jerusat]
*)
ML {* Auto_Tools.time_limit := 10 *}
+ML {* val mtds = [
+ MutabelleExtra.quickcheck_mtd (Config.put Quickcheck.finite_types false) "random",
+ MutabelleExtra.quickcheck_mtd (Config.put Quickcheck.finite_types true) "random",
+ MutabelleExtra.quickcheck_mtd (Config.put Quickcheck.finite_types false) "small",
+ MutabelleExtra.quickcheck_mtd (Config.put Quickcheck.finite_types true) "small"
+]
+*}
+
+ML {*
+fun mutation_testing_of (name, thy) =
+ (MutabelleExtra.random_seed := 1.0;
+ MutabelleExtra.thms_of false thy
+ |> MutabelleExtra.take_random 200
+ |> (fn thms => MutabelleExtra.mutate_theorems_and_write_report
+ @{theory} mtds thms (log_directory ^ "/" ^ name)))
+*}
+
text {* Uncomment the following ML code to check the counterexample generation with all theorems of Complex_Main. *}
+(*
ML {*
-(*
+
MutabelleExtra.random_seed := 1.0;
MutabelleExtra.thms_of true @{theory Complex_Main}
|> MutabelleExtra.take_random 1000000
|> (fn thms => List.drop (thms, 1000))
|> (fn thms => MutabelleExtra.mutate_theorems_and_write_report
- @{theory} [MutabelleExtra.quickcheck_mtd "SML",
- MutabelleExtra.quickcheck_mtd "code"
+ @{theory} [
+ MutabelleExtra.quickcheck_mtd "code",
+ MutabelleExtra.smallcheck_mtd
(*MutabelleExtra.refute_mtd,
MutabelleExtra.nitpick_mtd*)] thms "/tmp/muta.out")
+
+ *}
*)
+
+section {* Mutation testing Isabelle theories *}
+
+subsection {* List theory *}
+
+(*
+ML {*
+mutation_testing_of ("List", @{theory List})
*}
+*)
+
+section {* Mutation testing AFP theories *}
+
+subsection {* AVL-Trees *}
+
+(*
+ML {*
+mutation_testing_of ("AVL-Trees", @{theory AVL})
+ *}
+*)
+
+subsection {* BinaryTree *}
+
+(*
+ML {*
+mutation_testing_of ("BinaryTree", @{theory BinaryTree})
+ *}
+*)
+
+subsection {* Huffman *}
+
+(*
+ML {*
+mutation_testing_of ("Huffman", @{theory Huffman})
+ *}
+*)
-(* FIXME !?!?! *)
-ML {* Output.Private_Hooks.tracing_fn := old_tr *}
-ML {* Output.Private_Hooks.writeln_fn := old_wr *}
-ML {* Output.Private_Hooks.urgent_message_fn := old_ur *}
-ML {* Output.Private_Hooks.warning_fn := old_wa *}
+subsection {* List_Index *}
+
+(*
+ML {*
+mutation_testing_of ("List_Index", @{theory List_Index})
+ *}
+*)
+
+subsection {* Matrix *}
+
+(*
+ML {*
+mutation_testing_of ("Matrix", @{theory Matrix})
+ *}
+*)
+
+subsection {* NBE *}
+
+(*
+ML {*
+mutation_testing_of ("NBE", @{theory NBE})
+ *}
+*)
+
+subsection {* Polynomial *}
+
+(*
+ML {*
+mutation_testing_of ("Polynomial", @{theory Polynomial})
+ *}
+*)
+
+subsection {* Presburger Automata *}
+
+(*
+ML {*
+mutation_testing_of ("Presburger_Automata", @{theory Presburger_Automata})
+ *}
+*)
end
--- a/src/HOL/Mutabelle/mutabelle_extra.ML Mon Nov 22 11:34:58 2010 +0100
+++ b/src/HOL/Mutabelle/mutabelle_extra.ML Mon Nov 22 11:34:59 2010 +0100
@@ -8,7 +8,7 @@
val take_random : int -> 'a list -> 'a list
-datatype outcome = GenuineCex | PotentialCex | NoCex | Donno | Timeout | Error
+datatype outcome = GenuineCex | PotentialCex | NoCex | Donno | Timeout | Error | Solved | Unsolved
type timing = (string * int) list
type mtd = string * (theory -> term -> outcome * (timing * (int * Quickcheck.report list) list option))
@@ -20,7 +20,10 @@
type entry = string * bool * subentry list
type report = entry list
-val quickcheck_mtd : string -> mtd
+val quickcheck_mtd : (Proof.context -> Proof.context) -> string -> mtd
+
+val solve_direct_mtd : mtd
+val try_mtd : mtd
(*
val refute_mtd : mtd
val nitpick_mtd : mtd
@@ -45,15 +48,17 @@
(* mutation options *)
-val max_mutants = 4
-val num_mutations = 1
+(*val max_mutants = 4
+val num_mutations = 1*)
(* soundness check: *)
-(*val max_mutants = 1
-val num_mutations = 0*)
+val max_mutants = 10
+val num_mutations = 1
(* quickcheck options *)
(*val quickcheck_generator = "SML"*)
+(* Another Random engine *)
+
exception RANDOM;
fun rmod x y = x - y * Real.realFloor (x / y);
@@ -73,7 +78,26 @@
if h < l orelse l < 0 then raise RANDOM
else l + Real.floor (rmod (random ()) (real (h - l + 1)));
-datatype outcome = GenuineCex | PotentialCex | NoCex | Donno | Timeout | Error
+fun take_random 0 _ = []
+ | take_random _ [] = []
+ | take_random n xs =
+ let val j = random_range 0 (length xs - 1) in
+ Library.nth xs j :: take_random (n - 1) (nth_drop j xs)
+ end
+
+(* possible outcomes *)
+
+datatype outcome = GenuineCex | PotentialCex | NoCex | Donno | Timeout | Error | Solved | Unsolved
+
+fun string_of_outcome GenuineCex = "GenuineCex"
+ | string_of_outcome PotentialCex = "PotentialCex"
+ | string_of_outcome NoCex = "NoCex"
+ | string_of_outcome Donno = "Donno"
+ | string_of_outcome Timeout = "Timeout"
+ | string_of_outcome Error = "Error"
+ | string_of_outcome Solved = "Solved"
+ | string_of_outcome Unsolved = "Unsolved"
+
type timing = (string * int) list
type mtd = string * (theory -> term -> outcome * (timing * (int * Quickcheck.report list) list option))
@@ -85,25 +109,49 @@
type entry = string * bool * subentry list
type report = entry list
-fun inst_type insts (Type (s, Ts)) = Type (s, map (inst_type insts) Ts)
- | inst_type insts T = the_default HOLogic.intT (AList.lookup op = insts T)
+(* possible invocations *)
-fun preprocess thy insts t = Object_Logic.atomize_term thy
- (map_types (inst_type insts) (Mutabelle.freeze t));
+(** quickcheck **)
-fun invoke_quickcheck quickcheck_generator thy t =
+fun invoke_quickcheck change_options quickcheck_generator thy t =
TimeLimit.timeLimit (Time.fromSeconds (!Auto_Tools.time_limit))
(fn _ =>
- case Quickcheck.test_term (ProofContext.init_global thy)
- (SOME quickcheck_generator) (preprocess thy [] t) of
- (NONE, (time_report, report)) => (NoCex, (time_report, report))
- | (SOME _, (time_report, report)) => (GenuineCex, (time_report, report))) ()
+ case Quickcheck.test_goal_terms (change_options (ProofContext.init_global thy))
+ (SOME quickcheck_generator, []) [t] of
+ (NONE, _) => (NoCex, ([], NONE))
+ | (SOME _, _) => (GenuineCex, ([], NONE))) ()
handle TimeLimit.TimeOut => (Timeout, ([("timelimit", !Auto_Tools.time_limit)], NONE))
-fun quickcheck_mtd quickcheck_generator =
- ("quickcheck_" ^ quickcheck_generator, invoke_quickcheck quickcheck_generator)
+fun quickcheck_mtd change_options quickcheck_generator =
+ ("quickcheck_" ^ quickcheck_generator, invoke_quickcheck change_options quickcheck_generator)
+
+(** solve direct **)
+
+fun invoke_solve_direct thy t =
+ let
+ 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))
+ end
- (*
+val solve_direct_mtd = ("solve_direct", invoke_solve_direct)
+
+(** try **)
+
+fun invoke_try thy t =
+ let
+ val state = Proof.theorem NONE (K I) (map (single o rpair []) [t]) (ProofContext.init_global thy)
+ in
+ case Try.invoke_try NONE state of
+ true => (Solved, ([], NONE))
+ | false => (Unsolved, ([], NONE))
+ end
+
+val try_mtd = ("try", invoke_try)
+
+(*
fun invoke_refute thy t =
let
val res = MyRefute.refute_term thy [] t
@@ -185,6 +233,8 @@
val nitpick_mtd = ("nitpick", invoke_nitpick)
*)
+(* filtering forbidden theorems and mutants *)
+
val comms = [@{const_name HOL.eq}, @{const_name HOL.disj}, @{const_name HOL.conj}]
val forbidden =
@@ -200,7 +250,6 @@
(@{const_name "top_fun_inst.top_fun"}, "'a"),
(@{const_name "Pure.term"}, "'a"),
(@{const_name "top_class.top"}, "'a"),
- (@{const_name "HOL.equal"}, "'a"),
(@{const_name "Quotient.Quot_True"}, "'a")(*,
(@{const_name "uminus"}, "'a"),
(@{const_name "Nat.size"}, "'a"),
@@ -211,7 +260,7 @@
"nibble"]
val forbidden_consts =
- [@{const_name nibble_pair_of_char}]
+ [@{const_name nibble_pair_of_char}, @{const_name "TYPE"}]
fun is_forbidden_theorem (s, th) =
let val consts = Term.add_const_names (prop_of th) [] in
@@ -220,7 +269,8 @@
length (space_explode "." s) <> 2 orelse
String.isPrefix "type_definition" (List.last (space_explode "." s)) orelse
String.isSuffix "_def" s orelse
- String.isSuffix "_raw" s
+ String.isSuffix "_raw" s orelse
+ String.isPrefix "term_of" (List.last (space_explode "." s))
end
val forbidden_mutant_constnames =
@@ -235,23 +285,54 @@
@{const_name "top_fun_inst.top_fun"},
@{const_name "Pure.term"},
@{const_name "top_class.top"},
- @{const_name "HOL.equal"},
- @{const_name "Quotient.Quot_True"}]
+ (*@{const_name "HOL.equal"},*)
+ @{const_name "Quotient.Quot_True"}
+ (*@{const_name "==>"}, @{const_name "=="}*)]
+
+val forbidden_mutant_consts =
+ [
+ (@{const_name "Groups.zero_class.zero"}, @{typ "prop => prop => prop"}),
+ (@{const_name "Groups.one_class.one"}, @{typ "prop => prop => prop"}),
+ (@{const_name "Groups.plus_class.plus"}, @{typ "prop => prop => prop"}),
+ (@{const_name "Groups.minus_class.minus"}, @{typ "prop => prop => prop"}),
+ (@{const_name "Groups.times_class.times"}, @{typ "prop => prop => prop"}),
+ (@{const_name "Rings.inverse_class.divide"}, @{typ "prop => prop => prop"}),
+ (@{const_name "Lattices.semilattice_inf_class.inf"}, @{typ "prop => prop => prop"}),
+ (@{const_name "Lattices.semilattice_sup_class.sup"}, @{typ "prop => prop => prop"}),
+ (@{const_name "Orderings.bot_class.bot"}, @{typ "prop => prop => prop"}),
+ (@{const_name "Orderings.ord_class.min"}, @{typ "prop => prop => prop"}),
+ (@{const_name "Orderings.ord_class.max"}, @{typ "prop => prop => prop"}),
+ (@{const_name "Divides.div_class.mod"}, @{typ "prop => prop => prop"}),
+ (@{const_name "Divides.div_class.div"}, @{typ "prop => prop => prop"}),
+ (@{const_name "GCD.gcd_class.gcd"}, @{typ "prop => prop => prop"}),
+ (@{const_name "GCD.gcd_class.lcm"}, @{typ "prop => prop => prop"}),
+ (@{const_name "Orderings.bot_class.bot"}, @{typ "bool => prop"}),
+ (@{const_name "Groups.one_class.one"}, @{typ "bool => prop"}),
+ (@{const_name "Groups.zero_class.zero"},@{typ "bool => prop"})]
fun is_forbidden_mutant t =
let
- val consts = Term.add_const_names t []
+ val const_names = Term.add_const_names t []
+ val consts = Term.add_consts t []
in
- exists (String.isPrefix "Nitpick") consts orelse
- exists (String.isSubstring "_sumC") consts orelse
- exists (member (op =) forbidden_mutant_constnames) consts
+ exists (String.isPrefix "Nitpick") const_names orelse
+ exists (String.isSubstring "_sumC") const_names orelse
+ exists (member (op =) forbidden_mutant_constnames) const_names orelse
+ exists (member (op =) forbidden_mutant_consts) consts
end
+(* executable via quickcheck *)
+
fun is_executable_term thy t =
- can (TimeLimit.timeLimit (seconds 2.0)
- (Quickcheck.test_term
- (Context.proof_map (Quickcheck.map_test_params (apfst (K (1, 0)))) (ProofContext.init_global thy))
- (SOME "SML"))) (preprocess thy [] t)
+ let
+ val ctxt = ProofContext.init_global thy
+ in
+ can (TimeLimit.timeLimit (seconds 2.0)
+ (Quickcheck.test_goal_terms
+ ((Config.put Quickcheck.finite_types true #>
+ Config.put Quickcheck.size 1 #> Config.put Quickcheck.iterations 1) ctxt)
+ (SOME "random" , []))) (map (Object_Logic.atomize_term thy) (fst (Variable.import_terms true [t] ctxt)))
+ end
fun is_executable_thm thy th = is_executable_term thy (prop_of th)
@@ -267,44 +348,47 @@
val count = length oo filter o equal
-fun take_random 0 _ = []
- | take_random _ [] = []
- | take_random n xs =
- let val j = random_range 0 (length xs - 1) in
- Library.nth xs j :: take_random (n - 1) (nth_drop j xs)
- end
-
fun cpu_time description f =
let
val start = start_timing ()
val result = Exn.capture f ()
val time = Time.toMilliseconds (#cpu (end_timing start))
in (Exn.release result, (description, time)) end
-
+(*
+fun unsafe_invoke_mtd thy (mtd_name, invoke_mtd) t =
+ let
+ val _ = Output.urgent_message ("Invoking " ^ mtd_name)
+ val ((res, (timing, reports)), time) = cpu_time "total time" (fn () => invoke_mtd thy t
+ handle ERROR s => (tracing s; (Error, ([], NONE))))
+ val _ = Output.urgent_message (" Done")
+ in (res, (time :: timing, reports)) end
+*)
fun safe_invoke_mtd thy (mtd_name, invoke_mtd) t =
let
val _ = Output.urgent_message ("Invoking " ^ mtd_name)
- val ((res, (timing, reports)), time) = cpu_time "total time"
- (fn () => case try (invoke_mtd thy) t of
+ val (res, (timing, reports)) = (*cpu_time "total time"
+ (fn () => *)case try (invoke_mtd thy) t of
SOME (res, (timing, reports)) => (res, (timing, reports))
| NONE => (Output.urgent_message ("**** PROBLEMS WITH " ^ Syntax.string_of_term_global thy t);
- (Error , ([], NONE))))
+ (Error, ([], NONE)))
val _ = Output.urgent_message (" Done")
- in (res, (time :: timing, reports)) end
+ in (res, (timing, reports)) end
(* theory -> term list -> mtd -> subentry *)
-(*
+
fun test_mutants_using_one_method thy mutants (mtd_name, invoke_mtd) =
let
- val res = map (safe_invoke_mtd thy (mtd_name, invoke_mtd)) mutants
+ val res = map (fst o safe_invoke_mtd thy (mtd_name, invoke_mtd)) mutants
in
(mtd_name, count GenuineCex res, count PotentialCex res, count NoCex res,
count Donno res, count Timeout res, count Error res)
end
+(* creating entries *)
+
fun create_entry thy thm exec mutants mtds =
(Thm.get_name_hint thm, exec, map (test_mutants_using_one_method thy mutants) mtds)
-*)
+
fun create_detailed_entry thy thm exec mutants mtds =
let
fun create_mutant_subentry mutant = (mutant,
@@ -318,13 +402,14 @@
fun mutate_theorem create_entry thy mtds thm =
let
val exec = is_executable_thm thy thm
- val _ = Output.urgent_message (if exec then "EXEC" else "NOEXEC")
+ val _ = Output.tracing (if exec then "EXEC" else "NOEXEC")
val mutants =
(if num_mutations = 0 then
[Thm.prop_of thm]
else
Mutabelle.mutate_mix (Thm.prop_of thm) thy comms forbidden
num_mutations)
+ |> tap (fn muts => tracing ("mutants: " ^ string_of_int (length muts)))
|> filter_out is_forbidden_mutant
val mutants =
if exec then
@@ -344,6 +429,7 @@
|> map Mutabelle.freeze |> map freezeT
(* |> filter (not o is_forbidden_mutant) *)
|> List.mapPartial (try (Sign.cert_term thy))
+ |> List.filter (is_some o try (cterm_of thy))
val _ = map (fn t => Output.urgent_message ("MUTANT: " ^ Syntax.string_of_term_global thy t)) mutants
in
create_entry thy thm exec mutants mtds
@@ -352,13 +438,6 @@
(* theory -> mtd list -> thm list -> report *)
val mutate_theorems = map ooo mutate_theorem
-fun string_of_outcome GenuineCex = "GenuineCex"
- | string_of_outcome PotentialCex = "PotentialCex"
- | string_of_outcome NoCex = "NoCex"
- | string_of_outcome Donno = "Donno"
- | string_of_outcome Timeout = "Timeout"
- | string_of_outcome Error = "Error"
-
fun string_of_mutant_subentry thy thm_name (t, results) =
"mutant: " ^ Syntax.string_of_term_global thy t ^ "\n" ^
space_implode "; "
@@ -378,12 +457,12 @@
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)
+ 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*)
in
"mutant of " ^ thm_name ^ ":\n"
- ^ unyxml (Syntax.string_of_term_global thy t) ^ "\n" ^ cat_lines (map string_of_mtd_result results)
+ ^ unyxml (Syntax.string_of_term_global thy t) ^ "\n" ^ space_implode "; " (map string_of_mtd_result results)
end
fun string_of_detailed_entry thy (thm_name, exec, t, mutant_subentries) =
@@ -394,8 +473,7 @@
fun theoryfile_string_of_mutant_subentry thy thm_name (i, (t, results)) =
"lemma " ^ thm_name ^ "_" ^ string_of_int (i + 1) ^ ":\n" ^
"\"" ^ unyxml (Syntax.string_of_term_global thy t) ^
- "\" \nquickcheck[generator = SML]\nquickcheck[generator = predicate_compile_wo_ff]\n" ^
- "quickcheck[generator = predicate_compile_ff_nofs]\noops\n"
+ "\" \nquickcheck\noops\n"
fun theoryfile_string_of_detailed_entry thy (thm_name, exec, t, mutant_subentries) =
"subsubsection {* mutants of " ^ thm_name ^ " *}\n\n" ^
@@ -409,10 +487,12 @@
Int.toString potential_cex ^ "= " ^ Int.toString no_cex ^ "- " ^
Int.toString donno ^ "? " ^ Int.toString timeout ^ "T " ^
Int.toString error ^ "!"
+
(* entry -> string *)
fun string_for_entry (thm_name, exec, subentries) =
thm_name ^ " " ^ (if exec then "[exe]" else "[noexe]") ^ ":\n" ^
cat_lines (map string_for_subentry subentries) ^ "\n"
+
(* report -> string *)
fun string_for_report report = cat_lines (map string_for_entry report)
@@ -424,15 +504,16 @@
fun mutate_theorems_and_write_report thy mtds thms file_name =
let
val _ = Output.urgent_message "Starting Mutabelle..."
- val Quickcheck.Test_Params test_params = Quickcheck.test_params_of (ProofContext.init_global thy)
+ val ctxt = ProofContext.init_global thy
val path = Path.explode file_name
(* for normal report: *)
- (*val (gen_create_entry, gen_string_for_entry) = (create_entry, string_for_entry)*)
- (*for detailled report: *)
- val (gen_create_entry, gen_string_for_entry) =
- (create_detailed_entry, string_of_detailed_entry thy)
- val (gen_create_entry, gen_string_for_entry) =
- (create_detailed_entry, theoryfile_string_of_detailed_entry thy)
+ (*
+ val (gen_create_entry, gen_string_for_entry) = (create_entry, string_for_entry)
+ *)
+ (* for detailled report: *)
+ val (gen_create_entry, gen_string_for_entry) = (create_detailed_entry, string_of_detailed_entry thy)
+ (* for theory creation: *)
+ (*val (gen_create_entry, gen_string_for_entry) = (create_detailed_entry, theoryfile_string_of_detailed_entry thy)*)
in
File.write path (
"Mutation options = " ^
@@ -440,8 +521,8 @@
"; num_mutations: " ^ string_of_int num_mutations ^ "\n" ^
"QC options = " ^
(*"quickcheck_generator: " ^ quickcheck_generator ^ ";*)
- "size: " ^ string_of_int (#size test_params) ^
- "; iterations: " ^ string_of_int (#iterations test_params) ^ "\n");
+ "size: " ^ string_of_int (Config.get ctxt Quickcheck.size) ^
+ "; iterations: " ^ string_of_int (Config.get ctxt Quickcheck.iterations) ^ "\n");
map (File.append path o gen_string_for_entry o mutate_theorem gen_create_entry thy mtds) thms;
()
end