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