src/HOL/Mutabelle/mutabelle_extra.ML
author huffman
Fri Mar 30 12:32:35 2012 +0200 (2012-03-30)
changeset 47220 52426c62b5d0
parent 47108 2a1953f0d20d
child 47715 04400144c6fc
permissions -rw-r--r--
replace lemmas eval_nat_numeral with a simpler reformulation
     1 (*  Title:      HOL/Mutabelle/mutabelle_extra.ML
     2     Author:     Stefan Berghofer, Jasmin Blanchette, Lukas Bulwahn, TU Muenchen
     3 
     4 Invokation of Counterexample generators.
     5 *)
     6 
     7 signature MUTABELLE_EXTRA =
     8 sig
     9 
    10 val take_random : int -> 'a list -> 'a list
    11 
    12 datatype outcome = GenuineCex | PotentialCex | NoCex | Donno | Timeout | Error | Solved | Unsolved
    13 type timings = (string * int) list
    14 
    15 type mtd = string * (theory -> term -> outcome * timings)
    16 
    17 type mutant_subentry = term * (string * (outcome * timings)) list
    18 type detailed_entry = string * bool * term * mutant_subentry list
    19 
    20 type subentry = string * int * int * int * int * int * int
    21 type entry = string * bool * subentry list
    22 type report = entry list
    23 
    24 val quickcheck_mtd : (Proof.context -> Proof.context) -> string -> mtd
    25 
    26 val solve_direct_mtd : mtd
    27 val try0_mtd : mtd
    28 (*
    29 val sledgehammer_mtd : mtd
    30 *)
    31 val nitpick_mtd : mtd
    32 
    33 val refute_mtd : mtd
    34 
    35 val freezeT : term -> term
    36 val thms_of : bool -> theory -> thm list
    37 
    38 val string_for_report : report -> string
    39 val write_report : string -> report -> unit
    40 val mutate_theorems_and_write_report :
    41   theory -> int * int -> mtd list -> thm list -> string -> unit
    42 
    43 val random_seed : real Unsynchronized.ref
    44 end;
    45 
    46 structure MutabelleExtra : MUTABELLE_EXTRA =
    47 struct
    48 
    49 (* Own seed; can't rely on the Isabelle one to stay the same *)
    50 val random_seed = Unsynchronized.ref 1.0;
    51 
    52 (* Another Random engine *)
    53 
    54 exception RANDOM;
    55 
    56 fun rmod x y = x - y * Real.realFloor (x / y);
    57 
    58 local
    59   val a = 16807.0;
    60   val m = 2147483647.0;
    61 in
    62 
    63 fun random () = CRITICAL (fn () =>
    64   let val r = rmod (a * ! random_seed) m
    65   in (random_seed := r; r) end);
    66 
    67 end;
    68 
    69 fun random_range l h =
    70   if h < l orelse l < 0 then raise RANDOM
    71   else l + Real.floor (rmod (random ()) (real (h - l + 1)));
    72 
    73 fun take_random 0 _ = []
    74   | take_random _ [] = []
    75   | take_random n xs =
    76     let val j = random_range 0 (length xs - 1) in
    77       Library.nth xs j :: take_random (n - 1) (nth_drop j xs)
    78     end
    79   
    80 (* possible outcomes *)
    81 
    82 datatype outcome = GenuineCex | PotentialCex | NoCex | Donno | Timeout | Error | Solved | Unsolved
    83 
    84 fun string_of_outcome GenuineCex = "GenuineCex"
    85   | string_of_outcome PotentialCex = "PotentialCex"
    86   | string_of_outcome NoCex = "NoCex"
    87   | string_of_outcome Donno = "Donno"
    88   | string_of_outcome Timeout = "Timeout"
    89   | string_of_outcome Error = "Error"
    90   | string_of_outcome Solved = "Solved"
    91   | string_of_outcome Unsolved = "Unsolved"
    92 
    93 type timings = (string * int) list
    94 
    95 type mtd = string * (theory -> term -> outcome * timings)
    96 
    97 type mutant_subentry = term * (string * (outcome * timings)) list
    98 type detailed_entry = string * bool * term * mutant_subentry list
    99 
   100 type subentry = string * int * int * int * int * int * int
   101 type entry = string * bool * subentry list
   102 type report = entry list
   103 
   104 (* possible invocations *)
   105 
   106 (** quickcheck **)
   107 
   108 fun invoke_quickcheck change_options quickcheck_generator thy t =
   109   TimeLimit.timeLimit (seconds 30.0)
   110       (fn _ =>
   111           let
   112             val ctxt' = change_options (Proof_Context.init_global thy)
   113             val (result :: _) = case Quickcheck.active_testers ctxt' of
   114               [] => error "No active testers for quickcheck"
   115             | [tester] => tester ctxt' false [] [(t, [])]
   116             | _ => error "Multiple active testers for quickcheck"
   117           in
   118             case Quickcheck.counterexample_of result of 
   119               NONE => (NoCex, Quickcheck.timings_of result)
   120             | SOME _ => (GenuineCex, Quickcheck.timings_of result)
   121           end) ()
   122   handle TimeLimit.TimeOut =>
   123          (Timeout, [("timelimit", Real.floor (!Try.auto_time_limit))])
   124 
   125 fun quickcheck_mtd change_options quickcheck_generator =
   126   ("quickcheck_" ^ quickcheck_generator, invoke_quickcheck change_options quickcheck_generator)
   127 
   128 (** solve direct **)
   129  
   130 fun invoke_solve_direct thy t =
   131   let
   132     val state = Proof.theorem NONE (K I) (map (single o rpair []) [t]) (Proof_Context.init_global thy) 
   133   in
   134     case Solve_Direct.solve_direct state of
   135       (true, _) => (Solved, [])
   136     | (false, _) => (Unsolved, [])
   137   end
   138 
   139 val solve_direct_mtd = ("solve_direct", invoke_solve_direct) 
   140 
   141 (** try0 **)
   142 
   143 fun invoke_try0 thy t =
   144   let
   145     val state = Proof.theorem NONE (K I) (map (single o rpair []) [t]) (Proof_Context.init_global thy)
   146   in
   147     case Try0.try0 (SOME (seconds 5.0)) ([], [], [], []) state of
   148       true => (Solved, [])
   149     | false => (Unsolved, [])
   150   end
   151 
   152 val try0_mtd = ("try0", invoke_try0)
   153 
   154 (** sledgehammer **)
   155 (*
   156 fun invoke_sledgehammer thy t =
   157   if can (Goal.prove_global thy (Term.add_free_names t [])  [] t)
   158       (fn {context, ...} => Sledgehammer_Tactics.sledgehammer_with_metis_tac context 1) then
   159     (Solved, ([], NONE))
   160   else
   161     (Unsolved, ([], NONE))
   162 
   163 val sledgehammer_mtd = ("sledgehammer", invoke_sledgehammer)
   164 *)
   165 
   166 fun invoke_refute thy t =
   167   let
   168     val params = []
   169     val res = Refute.refute_term (Proof_Context.init_global thy) params [] t
   170     val _ = Output.urgent_message ("Refute: " ^ res)
   171   in
   172     (rpair []) (case res of
   173       "genuine" => GenuineCex
   174     | "likely_genuine" => GenuineCex
   175     | "potential" => PotentialCex
   176     | "none" => NoCex
   177     | "unknown" => Donno
   178     | _ => Error)
   179   end
   180   handle Refute.REFUTE (loc, details) =>
   181          (error ("Unhandled Refute error (" ^ quote loc ^ "): " ^ details ^
   182                    "."))
   183 val refute_mtd = ("refute", invoke_refute)
   184 
   185 (** nitpick **)
   186 
   187 fun invoke_nitpick thy t =
   188   let
   189     val ctxt = Proof_Context.init_global thy
   190     val state = Proof.init ctxt
   191     val (res, _) = Nitpick.pick_nits_in_term state
   192       (Nitpick_Isar.default_params thy []) Nitpick.Normal 1 1 1 [] [] t
   193     val _ = Output.urgent_message ("Nitpick: " ^ res)
   194   in
   195     (rpair []) (case res of
   196       "genuine" => GenuineCex
   197     | "likely_genuine" => GenuineCex
   198     | "potential" => PotentialCex
   199     | "none" => NoCex
   200     | "unknown" => Donno
   201     | _ => Error)
   202   end
   203 
   204 val nitpick_mtd = ("nitpick", invoke_nitpick)
   205 
   206 (* filtering forbidden theorems and mutants *)
   207 
   208 val comms = [@{const_name HOL.eq}, @{const_name HOL.disj}, @{const_name HOL.conj}]
   209 
   210 val forbidden =
   211  [(* (@{const_name "power"}, "'a"), *)
   212   (*(@{const_name induct_equal}, "'a"),
   213   (@{const_name induct_implies}, "'a"),
   214   (@{const_name induct_conj}, "'a"),*)
   215   (@{const_name "undefined"}, "'a"),
   216   (@{const_name "default"}, "'a"),
   217   (@{const_name "dummy_pattern"}, "'a::{}"),
   218   (@{const_name "HOL.simp_implies"}, "prop => prop => prop"),
   219   (@{const_name "bot_fun_inst.bot_fun"}, "'a"),
   220   (@{const_name "top_fun_inst.top_fun"}, "'a"),
   221   (@{const_name "Pure.term"}, "'a"),
   222   (@{const_name "top_class.top"}, "'a"),
   223   (@{const_name "Quotient.Quot_True"}, "'a")(*,
   224   (@{const_name "uminus"}, "'a"),
   225   (@{const_name "Nat.size"}, "'a"),
   226   (@{const_name "Groups.abs"}, "'a") *)]
   227 
   228 val forbidden_thms =
   229  ["finite_intvl_succ_class",
   230   "nibble"]
   231 
   232 val forbidden_consts =
   233  [@{const_name nibble_pair_of_char}, @{const_name "TYPE"},
   234   @{const_name Datatype.dsum}, @{const_name Datatype.usum}]
   235 
   236 fun is_forbidden_theorem (s, th) =
   237   let val consts = Term.add_const_names (prop_of th) [] in
   238     exists (member (op =) (Long_Name.explode s)) forbidden_thms orelse
   239     exists (member (op =) forbidden_consts) consts orelse
   240     length (Long_Name.explode s) <> 2 orelse
   241     String.isPrefix "type_definition" (List.last (Long_Name.explode s)) orelse
   242     String.isSuffix "_def" s orelse
   243     String.isSuffix "_raw" s orelse
   244     String.isPrefix "term_of" (List.last (Long_Name.explode s))
   245   end
   246 
   247 val forbidden_mutant_constnames =
   248  ["HOL.induct_equal",
   249   "HOL.induct_implies",
   250   "HOL.induct_conj",
   251   "HOL.induct_forall",
   252  @{const_name undefined},
   253  @{const_name default},
   254  @{const_name dummy_pattern},
   255  @{const_name "HOL.simp_implies"},
   256  @{const_name "bot_fun_inst.bot_fun"},
   257  @{const_name "top_fun_inst.top_fun"},
   258  @{const_name "Pure.term"},
   259  @{const_name "top_class.top"},
   260  (*@{const_name "HOL.equal"},*)
   261  @{const_name "Quotient.Quot_True"},
   262  @{const_name "equal_fun_inst.equal_fun"},
   263  @{const_name "equal_bool_inst.equal_bool"},
   264  @{const_name "ord_fun_inst.less_eq_fun"},
   265  @{const_name "ord_fun_inst.less_fun"},
   266  @{const_name Meson.skolem},
   267  @{const_name ATP.fequal},
   268  @{const_name ATP.fEx},
   269  @{const_name transfer_morphism},
   270  @{const_name enum_prod_inst.enum_all_prod},
   271  @{const_name enum_prod_inst.enum_ex_prod},
   272  @{const_name Quickcheck.catch_match},
   273  @{const_name Quickcheck_Exhaustive.unknown},
   274  @{const_name Num.Bit0}, @{const_name Num.Bit1}
   275  (*@{const_name "==>"}, @{const_name "=="}*)]
   276 
   277 val forbidden_mutant_consts =
   278   [
   279    (@{const_name "Groups.zero_class.zero"}, @{typ "prop => prop => prop"}),
   280    (@{const_name "Groups.one_class.one"}, @{typ "prop => prop => prop"}),
   281    (@{const_name "Groups.plus_class.plus"}, @{typ "prop => prop => prop"}),
   282    (@{const_name "Groups.minus_class.minus"}, @{typ "prop => prop => prop"}),
   283    (@{const_name "Groups.times_class.times"}, @{typ "prop => prop => prop"}),
   284    (@{const_name "Fields.inverse_class.divide"}, @{typ "prop => prop => prop"}),
   285    (@{const_name "Lattices.inf_class.inf"}, @{typ "prop => prop => prop"}),
   286    (@{const_name "Lattices.sup_class.sup"}, @{typ "prop => prop => prop"}),
   287    (@{const_name "Orderings.bot_class.bot"}, @{typ "prop => prop => prop"}),
   288    (@{const_name "Orderings.ord_class.min"}, @{typ "prop => prop => prop"}),
   289    (@{const_name "Orderings.ord_class.max"}, @{typ "prop => prop => prop"}),
   290    (@{const_name "Divides.div_class.mod"}, @{typ "prop => prop => prop"}),
   291    (@{const_name "Divides.div_class.div"}, @{typ "prop => prop => prop"}),
   292    (@{const_name "GCD.gcd_class.gcd"}, @{typ "prop => prop => prop"}),
   293    (@{const_name "GCD.gcd_class.lcm"}, @{typ "prop => prop => prop"}),
   294    (@{const_name "Orderings.bot_class.bot"}, @{typ "bool => prop"}),
   295    (@{const_name "Groups.one_class.one"}, @{typ "bool => prop"}),
   296    (@{const_name "Groups.zero_class.zero"},@{typ "bool => prop"}),
   297    (@{const_name "equal_class.equal"},@{typ "bool => bool => bool"})]
   298 
   299 fun is_forbidden_mutant t =
   300   let
   301     val const_names = Term.add_const_names t []
   302     val consts = Term.add_consts t []
   303   in
   304     exists (String.isPrefix "Nitpick") const_names orelse
   305     exists (String.isSubstring "_sumC") const_names orelse
   306     exists (member (op =) forbidden_mutant_constnames) const_names orelse
   307     exists (member (op =) forbidden_mutant_consts) consts
   308   end
   309 
   310 (* executable via quickcheck *)
   311 
   312 fun is_executable_term thy t =
   313   let
   314     val ctxt = Proof_Context.init_global thy
   315   in
   316     can (TimeLimit.timeLimit (seconds 30.0)
   317       (Quickcheck.test_terms
   318         ((Context.proof_map (Quickcheck.set_active_testers ["exhaustive"]) #>
   319           Config.put Quickcheck.finite_types true #>
   320           Config.put Quickcheck.finite_type_size 1 #>
   321           Config.put Quickcheck.size 1 #> Config.put Quickcheck.iterations 1) ctxt)
   322         (false, false) [])) (map (rpair [] o Object_Logic.atomize_term thy)
   323         (fst (Variable.import_terms true [t] ctxt)))
   324   end
   325 
   326 fun is_executable_thm thy th = is_executable_term thy (prop_of th)
   327 
   328 val freezeT =
   329   map_types (map_type_tvar (fn ((a, i), S) =>
   330     TFree (if i = 0 then a else a ^ "_" ^ string_of_int i, S)))
   331 
   332 fun thms_of all thy =
   333   filter
   334     (fn th => (all orelse Context.theory_name (theory_of_thm th) = Context.theory_name thy)
   335       (* andalso is_executable_thm thy th *))
   336     (map snd (filter_out is_forbidden_theorem (Mutabelle.all_unconcealed_thms_of thy)))
   337 
   338 fun count x = (length oo filter o equal) x
   339 
   340 fun cpu_time description e =
   341   let val ({cpu, ...}, result) = Timing.timing e ()
   342   in (result, (description, Time.toMilliseconds cpu)) end
   343 (*
   344 fun unsafe_invoke_mtd thy (mtd_name, invoke_mtd) t =
   345   let
   346     val _ = Output.urgent_message ("Invoking " ^ mtd_name)
   347     val ((res, (timing, reports)), time) = cpu_time "total time" (fn () => invoke_mtd thy t
   348       handle ERROR s => (tracing s; (Error, ([], NONE))))
   349     val _ = Output.urgent_message (" Done")
   350   in (res, (time :: timing, reports)) end
   351 *)  
   352 fun safe_invoke_mtd thy (mtd_name, invoke_mtd) t =
   353   let
   354     val _ = Output.urgent_message ("Invoking " ^ mtd_name)
   355     val (res, timing) = (*cpu_time "total time"
   356       (fn () => *)case try (invoke_mtd thy) t of
   357           SOME (res, timing) => (res, timing)
   358         | NONE => (Output.urgent_message ("**** PROBLEMS WITH " ^ Syntax.string_of_term_global thy t);
   359            (Error, []))
   360     val _ = Output.urgent_message (" Done")
   361   in (res, timing) end
   362 
   363 (* theory -> term list -> mtd -> subentry *)
   364 
   365 fun test_mutants_using_one_method thy mutants (mtd_name, invoke_mtd) =
   366   let
   367      val res = map (fst o safe_invoke_mtd thy (mtd_name, invoke_mtd)) mutants
   368   in
   369     (mtd_name, count GenuineCex res, count PotentialCex res, count NoCex res,
   370      count Donno res, count Timeout res, count Error res)
   371   end
   372 
   373 (* creating entries *)
   374 
   375 fun create_entry thy thm exec mutants mtds =
   376   (Thm.get_name_hint thm, exec, map (test_mutants_using_one_method thy mutants) mtds)
   377 
   378 fun create_detailed_entry thy thm exec mutants mtds =
   379   let
   380     fun create_mutant_subentry mutant = (mutant,
   381       map (fn (mtd_name, invoke_mtd) =>
   382         (mtd_name, safe_invoke_mtd thy (mtd_name, invoke_mtd) mutant)) mtds)
   383   in
   384     (Thm.get_name_hint thm, exec, prop_of thm, map create_mutant_subentry mutants)
   385   end
   386 
   387 (* (theory -> thm -> bool -> term list -> mtd list -> 'a) -> theory -> mtd list -> thm -> 'a *)
   388 fun mutate_theorem create_entry thy (num_mutations, max_mutants) mtds thm =
   389   let
   390     val exec = is_executable_thm thy thm
   391     val _ = tracing (if exec then "EXEC" else "NOEXEC")
   392     val mutants =
   393           (if num_mutations = 0 then
   394              [Thm.prop_of thm]
   395            else
   396              Mutabelle.mutate_mix (Thm.prop_of thm) thy comms forbidden
   397                                   num_mutations)
   398              |> tap (fn muts => tracing ("mutants: " ^ string_of_int (length muts)))
   399              |> filter_out is_forbidden_mutant
   400     val mutants =
   401       if exec then
   402         let
   403           val _ = Output.urgent_message ("BEFORE PARTITION OF " ^
   404                             string_of_int (length mutants) ^ " MUTANTS")
   405           val (execs, noexecs) = List.partition (is_executable_term thy) (take_random (20 * max_mutants) mutants)
   406           val _ = tracing ("AFTER PARTITION (" ^ string_of_int (length execs) ^
   407                            " vs " ^ string_of_int (length noexecs) ^ ")")
   408         in
   409           execs @ take_random (Int.max (0, max_mutants - length execs)) noexecs
   410         end
   411       else
   412         mutants
   413     val mutants = mutants
   414           |> map Mutabelle.freeze |> map freezeT
   415 (*          |> filter (not o is_forbidden_mutant) *)
   416           |> map_filter (try (Sign.cert_term thy))
   417           |> filter (is_some o try (Thm.cterm_of thy))
   418           |> filter (is_some o try (Syntax.check_term (Proof_Context.init_global thy)))
   419           |> take_random max_mutants
   420     val _ = map (fn t => Output.urgent_message ("MUTANT: " ^ Syntax.string_of_term_global thy t)) mutants
   421   in
   422     create_entry thy thm exec mutants mtds
   423   end
   424 
   425 (* theory -> mtd list -> thm list -> report *)
   426 val mutate_theorems = map oooo mutate_theorem
   427 
   428 fun string_of_mutant_subentry thy thm_name (t, results) =
   429   "mutant: " ^ Syntax.string_of_term_global thy t ^ "\n" ^
   430   space_implode "; "
   431     (map (fn (mtd_name, (outcome, timing)) => mtd_name ^ ": " ^ string_of_outcome outcome) results) ^
   432   "\n"
   433 
   434 (* string -> string *)
   435 val unyxml = XML.content_of o YXML.parse_body
   436 
   437 fun string_of_mutant_subentry' thy thm_name (t, results) =
   438   let
   439    (* fun string_of_report (Quickcheck.Report {iterations = i, raised_match_errors = e,
   440       satisfied_assms = s, positive_concl_tests = p}) =
   441       "errors: " ^ string_of_int e ^ "; conclusion tests: " ^ string_of_int p
   442     fun string_of_reports NONE = ""
   443       | string_of_reports (SOME reports) =
   444         cat_lines (map (fn (size, [report]) =>
   445           "size " ^ string_of_int size ^ ": " ^ string_of_report report) (rev reports))*)
   446     fun string_of_mtd_result (mtd_name, (outcome, timing)) =
   447       mtd_name ^ ": " ^ string_of_outcome outcome
   448       (*" with time " ^ " (" ^ space_implode "; " (map (fn (s, t) => (s ^ ": " ^ string_of_int t)) timing) ^ ")"*)
   449       (*^ "\n" ^ string_of_reports reports*)
   450   in
   451     "mutant of " ^ thm_name ^ ":\n"
   452     ^ unyxml (Syntax.string_of_term_global thy t) ^ "\n" ^ space_implode "; " (map string_of_mtd_result results)
   453   end
   454 
   455 fun string_of_detailed_entry thy (thm_name, exec, t, mutant_subentries) = 
   456    thm_name ^ " " ^ (if exec then "[exe]" else "[noexe]") ^ ": " ^
   457    Syntax.string_of_term_global thy t ^ "\n" ^                                    
   458    cat_lines (map (string_of_mutant_subentry' thy thm_name) mutant_subentries) ^ "\n"
   459 
   460 fun theoryfile_string_of_mutant_subentry thy thm_name (i, (t, results)) =
   461   "lemma " ^ thm_name ^ "_" ^ string_of_int (i + 1) ^ ":\n" ^
   462   "\"" ^ unyxml (Syntax.string_of_term_global thy t) ^
   463   "\" \nquickcheck\noops\n"
   464 
   465 fun theoryfile_string_of_detailed_entry thy (thm_name, exec, t, mutant_subentries) =
   466   "subsubsection {* mutants of " ^ thm_name ^ " *}\n\n" ^
   467   cat_lines (map_index
   468     (theoryfile_string_of_mutant_subentry thy thm_name) mutant_subentries) ^ "\n"
   469 
   470 (* subentry -> string *)
   471 fun string_for_subentry (mtd_name, genuine_cex, potential_cex, no_cex, donno,
   472                          timeout, error) =
   473   "    " ^ mtd_name ^ ": " ^ string_of_int genuine_cex ^ "+ " ^
   474   string_of_int potential_cex ^ "= " ^ string_of_int no_cex ^ "- " ^
   475   string_of_int donno ^ "? " ^ string_of_int timeout ^ "T " ^
   476   string_of_int error ^ "!"
   477 
   478 (* entry -> string *)
   479 fun string_for_entry (thm_name, exec, subentries) =
   480   thm_name ^ " " ^ (if exec then "[exe]" else "[noexe]") ^ ":\n" ^
   481   cat_lines (map string_for_subentry subentries) ^ "\n"
   482 
   483 (* report -> string *)
   484 fun string_for_report report = cat_lines (map string_for_entry report)
   485 
   486 (* string -> report -> unit *)
   487 fun write_report file_name =
   488   File.write (Path.explode file_name) o string_for_report
   489 
   490 (* theory -> mtd list -> thm list -> string -> unit *)
   491 fun mutate_theorems_and_write_report thy (num_mutations, max_mutants) mtds thms file_name =
   492   let
   493     val _ = Output.urgent_message "Starting Mutabelle..."
   494     val ctxt = Proof_Context.init_global thy
   495     val path = Path.explode file_name
   496     (* for normal report: *)
   497     (*
   498     val (gen_create_entry, gen_string_for_entry) = (create_entry, string_for_entry)
   499     *)
   500     (* for detailled report: *)
   501     val (gen_create_entry, gen_string_for_entry) = (create_detailed_entry, string_of_detailed_entry thy)
   502     (* for theory creation: *)
   503     (*val (gen_create_entry, gen_string_for_entry) = (create_detailed_entry, theoryfile_string_of_detailed_entry thy)*)
   504   in
   505     File.write path (
   506     "Mutation options = "  ^
   507       "max_mutants: " ^ string_of_int max_mutants ^
   508       "; num_mutations: " ^ string_of_int num_mutations ^ "\n" ^
   509     "QC options = " ^
   510       (*"quickcheck_generator: " ^ quickcheck_generator ^ ";*)
   511       "size: " ^ string_of_int (Config.get ctxt Quickcheck.size) ^
   512       "; iterations: " ^ string_of_int (Config.get ctxt Quickcheck.iterations) ^ "\n" ^
   513     "Isabelle environment = ISABELLE_GHC: " ^ getenv "ISABELLE_GHC" ^ "\n");
   514     map (File.append path o gen_string_for_entry o mutate_theorem gen_create_entry thy (num_mutations, max_mutants) mtds) thms;
   515     ()
   516   end
   517 
   518 end;