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