haftmann@37744: (*  Title:      HOL/Mutabelle/mutabelle_extra.ML
bulwahn@34965:     Author:     Stefan Berghofer, Jasmin Blanchette, Lukas Bulwahn, TU Muenchen
bulwahn@34965: 
wenzelm@41408: Invokation of Counterexample generators.
bulwahn@34965: *)
wenzelm@41408: 
bulwahn@34965: signature MUTABELLE_EXTRA =
bulwahn@34965: sig
bulwahn@34965: 
bulwahn@34965: val take_random : int -> 'a list -> 'a list
bulwahn@34965: 
bulwahn@40653: datatype outcome = GenuineCex | PotentialCex | NoCex | Donno | Timeout | Error | Solved | Unsolved
bulwahn@42089: type timings = (string * int) list
bulwahn@34965: 
bulwahn@42089: type mtd = string * (theory -> term -> outcome * timings)
bulwahn@35324: 
bulwahn@42089: type mutant_subentry = term * (string * (outcome * timings)) list
bulwahn@34965: type detailed_entry = string * bool * term * mutant_subentry list
bulwahn@34965: 
bulwahn@34965: type subentry = string * int * int * int * int * int * int
bulwahn@34965: type entry = string * bool * subentry list
bulwahn@34965: type report = entry list
bulwahn@34965: 
bulwahn@40653: val quickcheck_mtd : (Proof.context -> Proof.context) -> string -> mtd
bulwahn@40653: 
bulwahn@40653: val solve_direct_mtd : mtd
blanchet@46641: val try0_mtd : mtd
bulwahn@40974: (*
bulwahn@40971: val sledgehammer_mtd : mtd
bulwahn@40974: *)
bulwahn@41190: val nitpick_mtd : mtd
bulwahn@41190: 
bulwahn@34965: val refute_mtd : mtd
bulwahn@34965: 
bulwahn@34965: val freezeT : term -> term
bulwahn@34965: val thms_of : bool -> theory -> thm list
bulwahn@34965: 
bulwahn@34965: val string_for_report : report -> string
bulwahn@34965: val write_report : string -> report -> unit
bulwahn@34965: val mutate_theorems_and_write_report :
bulwahn@46454:   theory -> int * int -> mtd list -> thm list -> string -> unit
bulwahn@34965: 
wenzelm@56147: val init_random : real -> unit
bulwahn@34965: end;
bulwahn@34965: 
bulwahn@34965: structure MutabelleExtra : MUTABELLE_EXTRA =
bulwahn@34965: struct
bulwahn@34965: 
bulwahn@40653: (* Another Random engine *)
bulwahn@40653: 
bulwahn@34965: exception RANDOM;
bulwahn@34965: 
bulwahn@34965: fun rmod x y = x - y * Real.realFloor (x / y);
bulwahn@34965: 
bulwahn@34965: local
wenzelm@56147:   (* Own seed; can't rely on the Isabelle one to stay the same *)
wenzelm@56147:   val random_seed = Synchronized.var "random_seed" 1.0;
wenzelm@56147: 
bulwahn@34965:   val a = 16807.0;
bulwahn@34965:   val m = 2147483647.0;
bulwahn@34965: in
bulwahn@34965: 
wenzelm@56147: fun init_random r = Synchronized.change random_seed (K r);
wenzelm@56147: 
wenzelm@56147: fun random () =
wenzelm@56147:   Synchronized.change_result random_seed
wenzelm@56147:     (fn s =>
wenzelm@56147:       let val r = rmod (a * s) m
wenzelm@56147:       in (r, r) end);
bulwahn@34965: 
bulwahn@34965: end;
bulwahn@34965: 
bulwahn@34965: fun random_range l h =
bulwahn@34965:   if h < l orelse l < 0 then raise RANDOM
bulwahn@34965:   else l + Real.floor (rmod (random ()) (real (h - l + 1)));
bulwahn@34965: 
bulwahn@40653: fun take_random 0 _ = []
bulwahn@40653:   | take_random _ [] = []
bulwahn@40653:   | take_random n xs =
bulwahn@40653:     let val j = random_range 0 (length xs - 1) in
bulwahn@40653:       Library.nth xs j :: take_random (n - 1) (nth_drop j xs)
bulwahn@40653:     end
bulwahn@40653:   
bulwahn@40653: (* possible outcomes *)
bulwahn@40653: 
bulwahn@40653: datatype outcome = GenuineCex | PotentialCex | NoCex | Donno | Timeout | Error | Solved | Unsolved
bulwahn@40653: 
bulwahn@40653: fun string_of_outcome GenuineCex = "GenuineCex"
bulwahn@40653:   | string_of_outcome PotentialCex = "PotentialCex"
bulwahn@40653:   | string_of_outcome NoCex = "NoCex"
bulwahn@40653:   | string_of_outcome Donno = "Donno"
bulwahn@40653:   | string_of_outcome Timeout = "Timeout"
bulwahn@40653:   | string_of_outcome Error = "Error"
bulwahn@40653:   | string_of_outcome Solved = "Solved"
bulwahn@40653:   | string_of_outcome Unsolved = "Unsolved"
bulwahn@40653: 
bulwahn@42089: type timings = (string * int) list
bulwahn@34965: 
bulwahn@42089: type mtd = string * (theory -> term -> outcome * timings)
bulwahn@35324: 
bulwahn@42089: type mutant_subentry = term * (string * (outcome * timings)) list
bulwahn@34965: type detailed_entry = string * bool * term * mutant_subentry list
bulwahn@34965: 
bulwahn@34965: type subentry = string * int * int * int * int * int * int
bulwahn@34965: type entry = string * bool * subentry list
bulwahn@34965: type report = entry list
bulwahn@34965: 
bulwahn@40653: (* possible invocations *)
bulwahn@34965: 
bulwahn@40653: (** quickcheck **)
bulwahn@34965: 
haftmann@51092: fun invoke_quickcheck change_options thy t =
bulwahn@46452:   TimeLimit.timeLimit (seconds 30.0)
bulwahn@34965:       (fn _ =>
bulwahn@42089:           let
bulwahn@45159:             val ctxt' = change_options (Proof_Context.init_global thy)
bulwahn@46376:             val (result :: _) = case Quickcheck.active_testers ctxt' of
bulwahn@45159:               [] => error "No active testers for quickcheck"
bulwahn@45428:             | [tester] => tester ctxt' false [] [(t, [])]
bulwahn@45159:             | _ => error "Multiple active testers for quickcheck"
bulwahn@42089:           in
bulwahn@42089:             case Quickcheck.counterexample_of result of 
bulwahn@42089:               NONE => (NoCex, Quickcheck.timings_of result)
bulwahn@42089:             | SOME _ => (GenuineCex, Quickcheck.timings_of result)
bulwahn@42089:           end) ()
blanchet@40931:   handle TimeLimit.TimeOut =>
wenzelm@56467:          (Timeout, [("timelimit", Real.floor (Options.default_real @{system_option auto_time_limit}))])
bulwahn@34965: 
bulwahn@40653: fun quickcheck_mtd change_options quickcheck_generator =
haftmann@51092:   ("quickcheck_" ^ quickcheck_generator, invoke_quickcheck change_options)
bulwahn@40653: 
bulwahn@40653: (** solve direct **)
bulwahn@40653:  
bulwahn@40653: fun invoke_solve_direct thy t =
bulwahn@40653:   let
wenzelm@42361:     val state = Proof.theorem NONE (K I) (map (single o rpair []) [t]) (Proof_Context.init_global thy) 
bulwahn@40653:   in
blanchet@43030:     case Solve_Direct.solve_direct state of
bulwahn@42089:       (true, _) => (Solved, [])
bulwahn@42089:     | (false, _) => (Unsolved, [])
bulwahn@40653:   end
bulwahn@34965: 
bulwahn@40653: val solve_direct_mtd = ("solve_direct", invoke_solve_direct) 
bulwahn@40653: 
blanchet@46641: (** try0 **)
bulwahn@40653: 
blanchet@46641: fun invoke_try0 thy t =
bulwahn@40653:   let
wenzelm@42361:     val state = Proof.theorem NONE (K I) (map (single o rpair []) [t]) (Proof_Context.init_global thy)
bulwahn@40653:   in
blanchet@46641:     case Try0.try0 (SOME (seconds 5.0)) ([], [], [], []) state of
bulwahn@42089:       true => (Solved, [])
bulwahn@42089:     | false => (Unsolved, [])
bulwahn@40653:   end
bulwahn@40653: 
blanchet@46641: val try0_mtd = ("try0", invoke_try0)
bulwahn@40653: 
bulwahn@40971: (** sledgehammer **)
bulwahn@40974: (*
bulwahn@40971: fun invoke_sledgehammer thy t =
bulwahn@40971:   if can (Goal.prove_global thy (Term.add_free_names t [])  [] t)
bulwahn@40971:       (fn {context, ...} => Sledgehammer_Tactics.sledgehammer_with_metis_tac context 1) then
bulwahn@40971:     (Solved, ([], NONE))
bulwahn@40971:   else
bulwahn@40971:     (Unsolved, ([], NONE))
bulwahn@40971: 
bulwahn@40971: val sledgehammer_mtd = ("sledgehammer", invoke_sledgehammer)
bulwahn@40974: *)
blanchet@45397: 
bulwahn@34965: fun invoke_refute thy t =
bulwahn@34965:   let
blanchet@45397:     val params = []
blanchet@45397:     val res = Refute.refute_term (Proof_Context.init_global thy) params [] t
wenzelm@58843:     val _ = writeln ("Refute: " ^ res)
bulwahn@34965:   in
blanchet@45397:     (rpair []) (case res of
bulwahn@34965:       "genuine" => GenuineCex
bulwahn@34965:     | "likely_genuine" => GenuineCex
bulwahn@34965:     | "potential" => PotentialCex
bulwahn@34965:     | "none" => NoCex
bulwahn@34965:     | "unknown" => Donno
blanchet@45397:     | _ => Error)
bulwahn@34965:   end
blanchet@45397:   handle Refute.REFUTE (loc, details) =>
bulwahn@34965:          (error ("Unhandled Refute error (" ^ quote loc ^ "): " ^ details ^
bulwahn@34965:                    "."))
bulwahn@34965: val refute_mtd = ("refute", invoke_refute)
bulwahn@34965: 
bulwahn@41190: (** nitpick **)
bulwahn@34965: 
bulwahn@34965: fun invoke_nitpick thy t =
bulwahn@34965:   let
wenzelm@42361:     val ctxt = Proof_Context.init_global thy
bulwahn@34965:     val state = Proof.init ctxt
bulwahn@41190:     val (res, _) = Nitpick.pick_nits_in_term state
blanchet@55199:       (Nitpick_Commands.default_params thy []) Nitpick.Normal 1 1 1 [] [] [] t
wenzelm@58843:     val _ = writeln ("Nitpick: " ^ res)
bulwahn@34965:   in
bulwahn@42089:     (rpair []) (case res of
bulwahn@41190:       "genuine" => GenuineCex
bulwahn@41190:     | "likely_genuine" => GenuineCex
bulwahn@41190:     | "potential" => PotentialCex
bulwahn@41190:     | "none" => NoCex
bulwahn@41190:     | "unknown" => Donno
bulwahn@41190:     | _ => Error)
bulwahn@34965:   end
bulwahn@41190: 
bulwahn@34965: val nitpick_mtd = ("nitpick", invoke_nitpick)
bulwahn@34965: 
bulwahn@40653: (* filtering forbidden theorems and mutants *)
bulwahn@40653: 
haftmann@38864: val comms = [@{const_name HOL.eq}, @{const_name HOL.disj}, @{const_name HOL.conj}]
bulwahn@34965: 
bulwahn@34965: val forbidden =
bulwahn@34965:  [(* (@{const_name "power"}, "'a"), *)
bulwahn@35325:   (*(@{const_name induct_equal}, "'a"),
bulwahn@35325:   (@{const_name induct_implies}, "'a"),
bulwahn@35325:   (@{const_name induct_conj}, "'a"),*)
bulwahn@34965:   (@{const_name "undefined"}, "'a"),
bulwahn@34965:   (@{const_name "default"}, "'a"),
wenzelm@56241:   (@{const_name "Pure.dummy_pattern"}, "'a::{}"),
bulwahn@36255:   (@{const_name "HOL.simp_implies"}, "prop => prop => prop"),
bulwahn@36255:   (@{const_name "bot_fun_inst.bot_fun"}, "'a"),
bulwahn@36255:   (@{const_name "top_fun_inst.top_fun"}, "'a"),
bulwahn@36255:   (@{const_name "Pure.term"}, "'a"),
bulwahn@36255:   (@{const_name "top_class.top"}, "'a"),
bulwahn@36255:   (@{const_name "Quotient.Quot_True"}, "'a")(*,
bulwahn@34965:   (@{const_name "uminus"}, "'a"),
bulwahn@34965:   (@{const_name "Nat.size"}, "'a"),
haftmann@35092:   (@{const_name "Groups.abs"}, "'a") *)]
bulwahn@34965: 
bulwahn@34965: val forbidden_thms =
bulwahn@34965:  ["finite_intvl_succ_class",
bulwahn@34965:   "nibble"]
bulwahn@34965: 
blanchet@58111: val forbidden_consts = [@{const_name Pure.type}]
bulwahn@34965: 
bulwahn@34965: fun is_forbidden_theorem (s, th) =
wenzelm@59582:   let val consts = Term.add_const_names (Thm.prop_of th) [] in
wenzelm@46711:     exists (member (op =) (Long_Name.explode s)) forbidden_thms orelse
haftmann@36692:     exists (member (op =) forbidden_consts) consts orelse
wenzelm@46711:     length (Long_Name.explode s) <> 2 orelse
wenzelm@46711:     String.isPrefix "type_definition" (List.last (Long_Name.explode s)) orelse
bulwahn@34965:     String.isSuffix "_def" s orelse
bulwahn@40653:     String.isSuffix "_raw" s orelse
wenzelm@46711:     String.isPrefix "term_of" (List.last (Long_Name.explode s))
bulwahn@34965:   end
bulwahn@34965: 
bulwahn@36255: val forbidden_mutant_constnames =
wenzelm@59940: [@{const_name HOL.induct_equal},
wenzelm@59940:  @{const_name HOL.induct_implies},
wenzelm@59940:  @{const_name HOL.induct_conj},
wenzelm@59940:  @{const_name HOL.induct_forall},
bulwahn@36255:  @{const_name undefined},
bulwahn@36255:  @{const_name default},
wenzelm@56241:  @{const_name Pure.dummy_pattern},
bulwahn@36255:  @{const_name "HOL.simp_implies"},
bulwahn@36255:  @{const_name "bot_fun_inst.bot_fun"},
bulwahn@36255:  @{const_name "top_fun_inst.top_fun"},
bulwahn@36255:  @{const_name "Pure.term"},
bulwahn@36255:  @{const_name "top_class.top"},
bulwahn@40653:  (*@{const_name "HOL.equal"},*)
bulwahn@40971:  @{const_name "Quotient.Quot_True"},
bulwahn@40971:  @{const_name "equal_fun_inst.equal_fun"},
bulwahn@40971:  @{const_name "equal_bool_inst.equal_bool"},
bulwahn@40971:  @{const_name "ord_fun_inst.less_eq_fun"},
bulwahn@40971:  @{const_name "ord_fun_inst.less_fun"},
bulwahn@40971:  @{const_name Meson.skolem},
blanchet@43111:  @{const_name ATP.fequal},
bulwahn@46326:  @{const_name ATP.fEx},
bulwahn@42435:  @{const_name transfer_morphism},
bulwahn@42435:  @{const_name enum_prod_inst.enum_all_prod},
bulwahn@46314:  @{const_name enum_prod_inst.enum_ex_prod},
haftmann@51126:  @{const_name Quickcheck_Random.catch_match},
bulwahn@46434:  @{const_name Quickcheck_Exhaustive.unknown},
huffman@47108:  @{const_name Num.Bit0}, @{const_name Num.Bit1}
wenzelm@56245:  (*@{const_name Pure.imp}, @{const_name Pure.eq}*)]
bulwahn@40653: 
bulwahn@40653: val forbidden_mutant_consts =
bulwahn@40653:   [
bulwahn@40653:    (@{const_name "Groups.zero_class.zero"}, @{typ "prop => prop => prop"}),
bulwahn@40653:    (@{const_name "Groups.one_class.one"}, @{typ "prop => prop => prop"}),
bulwahn@40653:    (@{const_name "Groups.plus_class.plus"}, @{typ "prop => prop => prop"}),
bulwahn@40653:    (@{const_name "Groups.minus_class.minus"}, @{typ "prop => prop => prop"}),
bulwahn@40653:    (@{const_name "Groups.times_class.times"}, @{typ "prop => prop => prop"}),
huffman@44064:    (@{const_name "Fields.inverse_class.divide"}, @{typ "prop => prop => prop"}),
krauss@44845:    (@{const_name "Lattices.inf_class.inf"}, @{typ "prop => prop => prop"}),
krauss@44845:    (@{const_name "Lattices.sup_class.sup"}, @{typ "prop => prop => prop"}),
bulwahn@40653:    (@{const_name "Orderings.bot_class.bot"}, @{typ "prop => prop => prop"}),
bulwahn@40653:    (@{const_name "Orderings.ord_class.min"}, @{typ "prop => prop => prop"}),
bulwahn@40653:    (@{const_name "Orderings.ord_class.max"}, @{typ "prop => prop => prop"}),
bulwahn@40653:    (@{const_name "Divides.div_class.mod"}, @{typ "prop => prop => prop"}),
bulwahn@40653:    (@{const_name "Divides.div_class.div"}, @{typ "prop => prop => prop"}),
bulwahn@40653:    (@{const_name "GCD.gcd_class.gcd"}, @{typ "prop => prop => prop"}),
bulwahn@40653:    (@{const_name "GCD.gcd_class.lcm"}, @{typ "prop => prop => prop"}),
bulwahn@40653:    (@{const_name "Orderings.bot_class.bot"}, @{typ "bool => prop"}),
bulwahn@40653:    (@{const_name "Groups.one_class.one"}, @{typ "bool => prop"}),
bulwahn@46326:    (@{const_name "Groups.zero_class.zero"},@{typ "bool => prop"}),
bulwahn@46326:    (@{const_name "equal_class.equal"},@{typ "bool => bool => bool"})]
bulwahn@36255: 
bulwahn@34965: fun is_forbidden_mutant t =
bulwahn@36255:   let
bulwahn@40653:     val const_names = Term.add_const_names t []
bulwahn@40653:     val consts = Term.add_consts t []
bulwahn@36255:   in
bulwahn@40653:     exists (String.isPrefix "Nitpick") const_names orelse
bulwahn@40653:     exists (String.isSubstring "_sumC") const_names orelse
bulwahn@40653:     exists (member (op =) forbidden_mutant_constnames) const_names orelse
bulwahn@40653:     exists (member (op =) forbidden_mutant_consts) consts
bulwahn@34965:   end
bulwahn@34965: 
bulwahn@40653: (* executable via quickcheck *)
bulwahn@40653: 
bulwahn@40248: fun is_executable_term thy t =
bulwahn@40653:   let
wenzelm@42361:     val ctxt = Proof_Context.init_global thy
bulwahn@40653:   in
bulwahn@46452:     can (TimeLimit.timeLimit (seconds 30.0)
bulwahn@45159:       (Quickcheck.test_terms
bulwahn@45165:         ((Context.proof_map (Quickcheck.set_active_testers ["exhaustive"]) #>
bulwahn@45165:           Config.put Quickcheck.finite_types true #>
bulwahn@41106:           Config.put Quickcheck.finite_type_size 1 #>
bulwahn@40653:           Config.put Quickcheck.size 1 #> Config.put Quickcheck.iterations 1) ctxt)
bulwahn@45159:         (false, false) [])) (map (rpair [] o Object_Logic.atomize_term thy)
bulwahn@45159:         (fst (Variable.import_terms true [t] ctxt)))
bulwahn@40653:   end
bulwahn@40248: 
wenzelm@59582: fun is_executable_thm thy th = is_executable_term thy (Thm.prop_of th)
bulwahn@34965: 
bulwahn@34965: val freezeT =
bulwahn@34965:   map_types (map_type_tvar (fn ((a, i), S) =>
bulwahn@34965:     TFree (if i = 0 then a else a ^ "_" ^ string_of_int i, S)))
bulwahn@34965: 
bulwahn@34965: fun thms_of all thy =
bulwahn@34965:   filter
wenzelm@59582:     (fn th => (all orelse Context.theory_name (Thm.theory_of_thm th) = Context.theory_name thy)
bulwahn@34965:       (* andalso is_executable_thm thy th *))
wenzelm@56161:     (map snd (filter_out is_forbidden_theorem (Global_Theory.all_thms_of thy false)))
bulwahn@34965: 
bulwahn@49441: fun elapsed_time description e =
bulwahn@49441:   let val ({elapsed, ...}, result) = Timing.timing e ()
bulwahn@49441:   in (result, (description, Time.toMilliseconds elapsed)) end
bulwahn@40653: (*
bulwahn@40653: fun unsafe_invoke_mtd thy (mtd_name, invoke_mtd) t =
bulwahn@40653:   let
wenzelm@58843:     val _ = writeln ("Invoking " ^ mtd_name)
bulwahn@40653:     val ((res, (timing, reports)), time) = cpu_time "total time" (fn () => invoke_mtd thy t
bulwahn@40653:       handle ERROR s => (tracing s; (Error, ([], NONE))))
wenzelm@58843:     val _ = writeln (" Done")
bulwahn@40653:   in (res, (time :: timing, reports)) end
bulwahn@40653: *)  
bulwahn@34965: fun safe_invoke_mtd thy (mtd_name, invoke_mtd) t =
bulwahn@34965:   let
wenzelm@58843:     val _ = writeln ("Invoking " ^ mtd_name)
bulwahn@49441:     val (res, timing) = elapsed_time "total time"
bulwahn@49441:       (fn () => case try (invoke_mtd thy) t of
haftmann@51092:           SOME (res, _) => res
wenzelm@58843:         | NONE => (writeln ("**** PROBLEMS WITH " ^ Syntax.string_of_term_global thy t);
bulwahn@49441:             Error))
wenzelm@58843:     val _ = writeln (" Done")
bulwahn@49441:   in (res, [timing]) end
bulwahn@34965: 
bulwahn@40653: (* creating entries *)
bulwahn@40653: 
bulwahn@34965: fun create_detailed_entry thy thm exec mutants mtds =
bulwahn@34965:   let
bulwahn@34965:     fun create_mutant_subentry mutant = (mutant,
bulwahn@34965:       map (fn (mtd_name, invoke_mtd) =>
bulwahn@34965:         (mtd_name, safe_invoke_mtd thy (mtd_name, invoke_mtd) mutant)) mtds)
bulwahn@34965:   in
wenzelm@59582:     (Thm.get_name_hint thm, exec, Thm.prop_of thm, map create_mutant_subentry mutants)
bulwahn@34965:   end
bulwahn@34965: 
bulwahn@34965: (* (theory -> thm -> bool -> term list -> mtd list -> 'a) -> theory -> mtd list -> thm -> 'a *)
bulwahn@46454: fun mutate_theorem create_entry thy (num_mutations, max_mutants) mtds thm =
bulwahn@34965:   let
bulwahn@34965:     val exec = is_executable_thm thy thm
wenzelm@43277:     val _ = tracing (if exec then "EXEC" else "NOEXEC")
bulwahn@34965:     val mutants =
bulwahn@34965:           (if num_mutations = 0 then
bulwahn@34965:              [Thm.prop_of thm]
bulwahn@34965:            else
bulwahn@34965:              Mutabelle.mutate_mix (Thm.prop_of thm) thy comms forbidden
bulwahn@34965:                                   num_mutations)
bulwahn@40653:              |> tap (fn muts => tracing ("mutants: " ^ string_of_int (length muts)))
bulwahn@34965:              |> filter_out is_forbidden_mutant
bulwahn@34965:     val mutants =
bulwahn@34965:       if exec then
bulwahn@34965:         let
wenzelm@58843:           val _ = writeln ("BEFORE PARTITION OF " ^
wenzelm@41491:                             string_of_int (length mutants) ^ " MUTANTS")
bulwahn@34965:           val (execs, noexecs) = List.partition (is_executable_term thy) (take_random (20 * max_mutants) mutants)
wenzelm@41491:           val _ = tracing ("AFTER PARTITION (" ^ string_of_int (length execs) ^
wenzelm@41491:                            " vs " ^ string_of_int (length noexecs) ^ ")")
bulwahn@34965:         in
bulwahn@34965:           execs @ take_random (Int.max (0, max_mutants - length execs)) noexecs
bulwahn@34965:         end
bulwahn@34965:       else
bulwahn@34965:         mutants
bulwahn@34965:     val mutants = mutants
bulwahn@34965:           |> map Mutabelle.freeze |> map freezeT
bulwahn@34965: (*          |> filter (not o is_forbidden_mutant) *)
wenzelm@42429:           |> map_filter (try (Sign.cert_term thy))
wenzelm@59621:           |> filter (is_some o try (Thm.global_cterm_of thy))
wenzelm@42429:           |> filter (is_some o try (Syntax.check_term (Proof_Context.init_global thy)))
bulwahn@40971:           |> take_random max_mutants
wenzelm@58843:     val _ = map (fn t => writeln ("MUTANT: " ^ Syntax.string_of_term_global thy t)) mutants
bulwahn@34965:   in
bulwahn@34965:     create_entry thy thm exec mutants mtds
bulwahn@34965:   end
bulwahn@34965: 
bulwahn@35324: fun string_of_mutant_subentry' thy thm_name (t, results) =
bulwahn@35380:   let
bulwahn@42089:    (* fun string_of_report (Quickcheck.Report {iterations = i, raised_match_errors = e,
bulwahn@35380:       satisfied_assms = s, positive_concl_tests = p}) =
bulwahn@35380:       "errors: " ^ string_of_int e ^ "; conclusion tests: " ^ string_of_int p
bulwahn@35380:     fun string_of_reports NONE = ""
bulwahn@35380:       | string_of_reports (SOME reports) =
bulwahn@35380:         cat_lines (map (fn (size, [report]) =>
bulwahn@42089:           "size " ^ string_of_int size ^ ": " ^ string_of_report report) (rev reports))*)
bulwahn@42089:     fun string_of_mtd_result (mtd_name, (outcome, timing)) =
bulwahn@40653:       mtd_name ^ ": " ^ string_of_outcome outcome
bulwahn@49441:       ^ "(" ^ space_implode "; " (map (fn (s, t) => (s ^ ": " ^ string_of_int t)) timing) ^ ")"
bulwahn@36255:       (*^ "\n" ^ string_of_reports reports*)
bulwahn@35380:   in
wenzelm@59433:     "mutant of " ^ thm_name ^ ":\n" ^
wenzelm@59433:       YXML.content_of (Syntax.string_of_term_global thy t) ^ "\n" ^
wenzelm@59433:       space_implode "; " (map string_of_mtd_result results)
bulwahn@35380:   end
bulwahn@35324: 
bulwahn@34965: fun string_of_detailed_entry thy (thm_name, exec, t, mutant_subentries) = 
bulwahn@34965:    thm_name ^ " " ^ (if exec then "[exe]" else "[noexe]") ^ ": " ^
bulwahn@36255:    Syntax.string_of_term_global thy t ^ "\n" ^                                    
bulwahn@35324:    cat_lines (map (string_of_mutant_subentry' thy thm_name) mutant_subentries) ^ "\n"
bulwahn@34965: 
bulwahn@34965: (* subentry -> string *)
bulwahn@34965: fun string_for_subentry (mtd_name, genuine_cex, potential_cex, no_cex, donno,
bulwahn@34965:                          timeout, error) =
wenzelm@41491:   "    " ^ mtd_name ^ ": " ^ string_of_int genuine_cex ^ "+ " ^
wenzelm@41491:   string_of_int potential_cex ^ "= " ^ string_of_int no_cex ^ "- " ^
wenzelm@41491:   string_of_int donno ^ "? " ^ string_of_int timeout ^ "T " ^
wenzelm@41491:   string_of_int error ^ "!"
bulwahn@40653: 
bulwahn@34965: (* entry -> string *)
bulwahn@34965: fun string_for_entry (thm_name, exec, subentries) =
bulwahn@34965:   thm_name ^ " " ^ (if exec then "[exe]" else "[noexe]") ^ ":\n" ^
bulwahn@34965:   cat_lines (map string_for_subentry subentries) ^ "\n"
bulwahn@40653: 
bulwahn@34965: (* report -> string *)
bulwahn@34965: fun string_for_report report = cat_lines (map string_for_entry report)
bulwahn@34965: 
bulwahn@34965: (* string -> report -> unit *)
bulwahn@34965: fun write_report file_name =
bulwahn@34965:   File.write (Path.explode file_name) o string_for_report
bulwahn@34965: 
bulwahn@34965: (* theory -> mtd list -> thm list -> string -> unit *)
bulwahn@46454: fun mutate_theorems_and_write_report thy (num_mutations, max_mutants) mtds thms file_name =
bulwahn@34965:   let
wenzelm@58843:     val _ = writeln "Starting Mutabelle..."
wenzelm@42361:     val ctxt = Proof_Context.init_global thy
bulwahn@34965:     val path = Path.explode file_name
bulwahn@34965:     (* for normal report: *)
bulwahn@40653:     (*
bulwahn@40653:     val (gen_create_entry, gen_string_for_entry) = (create_entry, string_for_entry)
bulwahn@40653:     *)
bulwahn@40653:     (* for detailled report: *)
bulwahn@40653:     val (gen_create_entry, gen_string_for_entry) = (create_detailed_entry, string_of_detailed_entry thy)
bulwahn@40653:     (* for theory creation: *)
bulwahn@40653:     (*val (gen_create_entry, gen_string_for_entry) = (create_detailed_entry, theoryfile_string_of_detailed_entry thy)*)
bulwahn@34965:   in
bulwahn@34965:     File.write path (
bulwahn@34965:     "Mutation options = "  ^
bulwahn@34965:       "max_mutants: " ^ string_of_int max_mutants ^
bulwahn@34965:       "; num_mutations: " ^ string_of_int num_mutations ^ "\n" ^
bulwahn@34965:     "QC options = " ^
bulwahn@34965:       (*"quickcheck_generator: " ^ quickcheck_generator ^ ";*)
bulwahn@40653:       "size: " ^ string_of_int (Config.get ctxt Quickcheck.size) ^
bulwahn@43244:       "; iterations: " ^ string_of_int (Config.get ctxt Quickcheck.iterations) ^ "\n" ^
bulwahn@43244:     "Isabelle environment = ISABELLE_GHC: " ^ getenv "ISABELLE_GHC" ^ "\n");
bulwahn@46454:     map (File.append path o gen_string_for_entry o mutate_theorem gen_create_entry thy (num_mutations, max_mutants) mtds) thms;
bulwahn@34965:     ()
bulwahn@34965:   end
bulwahn@34965: 
bulwahn@34965: end;