src/HOL/Mutabelle/mutabelle_extra.ML
author haftmann
Mon Jun 05 15:59:41 2017 +0200 (2017-06-05)
changeset 66010 2f7d39285a1a
parent 65458 cf504b7a7aa7
child 66954 0230af0f3c59
permissions -rw-r--r--
executable domain membership checks
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 =
wenzelm@62519
   113
  Timeout.apply (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) ()
wenzelm@62519
   126
  handle Timeout.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@58843
   174
    val _ = writeln ("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
wenzelm@58843
   197
    val _ = writeln ("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) =
wenzelm@59582
   239
  let val consts = Term.add_const_names (Thm.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 =
wenzelm@59940
   250
[@{const_name HOL.induct_equal},
wenzelm@59940
   251
 @{const_name HOL.induct_implies},
wenzelm@59940
   252
 @{const_name HOL.induct_conj},
wenzelm@59940
   253
 @{const_name 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"}),
haftmann@63950
   286
   (@{const_name "Lattices.inf_class.inf"}, @{typ "prop => prop => prop"}),
krauss@44845
   287
   (@{const_name "Lattices.sup_class.sup"}, @{typ "prop => prop => prop"}),
bulwahn@40653
   288
   (@{const_name "Orderings.bot_class.bot"}, @{typ "prop => prop => prop"}),
bulwahn@40653
   289
   (@{const_name "Orderings.ord_class.min"}, @{typ "prop => prop => prop"}),
bulwahn@40653
   290
   (@{const_name "Orderings.ord_class.max"}, @{typ "prop => prop => prop"}),
haftmann@63950
   291
   (@{const_name "Rings.modulo"}, @{typ "prop => prop => prop"}),
haftmann@60352
   292
   (@{const_name Rings.divide}, @{typ "prop => prop => prop"}),
bulwahn@40653
   293
   (@{const_name "GCD.gcd_class.gcd"}, @{typ "prop => prop => prop"}),
bulwahn@40653
   294
   (@{const_name "GCD.gcd_class.lcm"}, @{typ "prop => prop => prop"}),
bulwahn@40653
   295
   (@{const_name "Orderings.bot_class.bot"}, @{typ "bool => prop"}),
bulwahn@40653
   296
   (@{const_name "Groups.one_class.one"}, @{typ "bool => prop"}),
bulwahn@46326
   297
   (@{const_name "Groups.zero_class.zero"},@{typ "bool => prop"}),
bulwahn@46326
   298
   (@{const_name "equal_class.equal"},@{typ "bool => bool => bool"})]
bulwahn@36255
   299
bulwahn@34965
   300
fun is_forbidden_mutant t =
bulwahn@36255
   301
  let
bulwahn@40653
   302
    val const_names = Term.add_const_names t []
bulwahn@40653
   303
    val consts = Term.add_consts t []
bulwahn@36255
   304
  in
bulwahn@40653
   305
    exists (String.isPrefix "Nitpick") const_names orelse
bulwahn@40653
   306
    exists (String.isSubstring "_sumC") const_names orelse
bulwahn@40653
   307
    exists (member (op =) forbidden_mutant_constnames) const_names orelse
bulwahn@40653
   308
    exists (member (op =) forbidden_mutant_consts) consts
bulwahn@34965
   309
  end
bulwahn@34965
   310
bulwahn@40653
   311
(* executable via quickcheck *)
bulwahn@40653
   312
bulwahn@40248
   313
fun is_executable_term thy t =
bulwahn@40653
   314
  let
wenzelm@42361
   315
    val ctxt = Proof_Context.init_global thy
bulwahn@40653
   316
  in
wenzelm@62519
   317
    can (Timeout.apply (seconds 30.0)
bulwahn@45159
   318
      (Quickcheck.test_terms
bulwahn@45165
   319
        ((Context.proof_map (Quickcheck.set_active_testers ["exhaustive"]) #>
bulwahn@45165
   320
          Config.put Quickcheck.finite_types true #>
bulwahn@41106
   321
          Config.put Quickcheck.finite_type_size 1 #>
bulwahn@40653
   322
          Config.put Quickcheck.size 1 #> Config.put Quickcheck.iterations 1) ctxt)
wenzelm@59970
   323
        (false, false) [])) (map (rpair [] o Object_Logic.atomize_term ctxt)
bulwahn@45159
   324
        (fst (Variable.import_terms true [t] ctxt)))
bulwahn@40653
   325
  end
bulwahn@40248
   326
wenzelm@59582
   327
fun is_executable_thm thy th = is_executable_term thy (Thm.prop_of th)
bulwahn@34965
   328
bulwahn@34965
   329
val freezeT =
bulwahn@34965
   330
  map_types (map_type_tvar (fn ((a, i), S) =>
bulwahn@34965
   331
    TFree (if i = 0 then a else a ^ "_" ^ string_of_int i, S)))
bulwahn@34965
   332
bulwahn@34965
   333
fun thms_of all thy =
bulwahn@34965
   334
  filter
wenzelm@65458
   335
    (fn th => (all orelse Thm.theory_name th = Context.theory_name thy)
bulwahn@34965
   336
      (* andalso is_executable_thm thy th *))
wenzelm@56161
   337
    (map snd (filter_out is_forbidden_theorem (Global_Theory.all_thms_of thy false)))
bulwahn@34965
   338
bulwahn@49441
   339
fun elapsed_time description e =
bulwahn@49441
   340
  let val ({elapsed, ...}, result) = Timing.timing e ()
bulwahn@49441
   341
  in (result, (description, Time.toMilliseconds elapsed)) end
bulwahn@40653
   342
(*
bulwahn@40653
   343
fun unsafe_invoke_mtd thy (mtd_name, invoke_mtd) t =
bulwahn@40653
   344
  let
wenzelm@58843
   345
    val _ = writeln ("Invoking " ^ mtd_name)
bulwahn@40653
   346
    val ((res, (timing, reports)), time) = cpu_time "total time" (fn () => invoke_mtd thy t
bulwahn@40653
   347
      handle ERROR s => (tracing s; (Error, ([], NONE))))
wenzelm@58843
   348
    val _ = writeln (" Done")
bulwahn@40653
   349
  in (res, (time :: timing, reports)) end
bulwahn@40653
   350
*)  
bulwahn@34965
   351
fun safe_invoke_mtd thy (mtd_name, invoke_mtd) t =
bulwahn@34965
   352
  let
wenzelm@58843
   353
    val _ = writeln ("Invoking " ^ mtd_name)
bulwahn@49441
   354
    val (res, timing) = elapsed_time "total time"
bulwahn@49441
   355
      (fn () => case try (invoke_mtd thy) t of
haftmann@51092
   356
          SOME (res, _) => res
wenzelm@58843
   357
        | NONE => (writeln ("**** PROBLEMS WITH " ^ Syntax.string_of_term_global thy t);
bulwahn@49441
   358
            Error))
wenzelm@58843
   359
    val _ = writeln (" Done")
bulwahn@49441
   360
  in (res, [timing]) end
bulwahn@34965
   361
bulwahn@40653
   362
(* creating entries *)
bulwahn@40653
   363
bulwahn@34965
   364
fun create_detailed_entry thy thm exec mutants mtds =
bulwahn@34965
   365
  let
bulwahn@34965
   366
    fun create_mutant_subentry mutant = (mutant,
bulwahn@34965
   367
      map (fn (mtd_name, invoke_mtd) =>
bulwahn@34965
   368
        (mtd_name, safe_invoke_mtd thy (mtd_name, invoke_mtd) mutant)) mtds)
bulwahn@34965
   369
  in
wenzelm@59582
   370
    (Thm.get_name_hint thm, exec, Thm.prop_of thm, map create_mutant_subentry mutants)
bulwahn@34965
   371
  end
bulwahn@34965
   372
bulwahn@34965
   373
(* (theory -> thm -> bool -> term list -> mtd list -> 'a) -> theory -> mtd list -> thm -> 'a *)
bulwahn@46454
   374
fun mutate_theorem create_entry thy (num_mutations, max_mutants) mtds thm =
bulwahn@34965
   375
  let
bulwahn@34965
   376
    val exec = is_executable_thm thy thm
wenzelm@43277
   377
    val _ = tracing (if exec then "EXEC" else "NOEXEC")
bulwahn@34965
   378
    val mutants =
bulwahn@34965
   379
          (if num_mutations = 0 then
bulwahn@34965
   380
             [Thm.prop_of thm]
bulwahn@34965
   381
           else
bulwahn@34965
   382
             Mutabelle.mutate_mix (Thm.prop_of thm) thy comms forbidden
bulwahn@34965
   383
                                  num_mutations)
bulwahn@40653
   384
             |> tap (fn muts => tracing ("mutants: " ^ string_of_int (length muts)))
bulwahn@34965
   385
             |> filter_out is_forbidden_mutant
bulwahn@34965
   386
    val mutants =
bulwahn@34965
   387
      if exec then
bulwahn@34965
   388
        let
wenzelm@58843
   389
          val _ = writeln ("BEFORE PARTITION OF " ^
wenzelm@41491
   390
                            string_of_int (length mutants) ^ " MUTANTS")
bulwahn@34965
   391
          val (execs, noexecs) = List.partition (is_executable_term thy) (take_random (20 * max_mutants) mutants)
wenzelm@41491
   392
          val _ = tracing ("AFTER PARTITION (" ^ string_of_int (length execs) ^
wenzelm@41491
   393
                           " vs " ^ string_of_int (length noexecs) ^ ")")
bulwahn@34965
   394
        in
bulwahn@34965
   395
          execs @ take_random (Int.max (0, max_mutants - length execs)) noexecs
bulwahn@34965
   396
        end
bulwahn@34965
   397
      else
bulwahn@34965
   398
        mutants
bulwahn@34965
   399
    val mutants = mutants
bulwahn@34965
   400
          |> map Mutabelle.freeze |> map freezeT
bulwahn@34965
   401
(*          |> filter (not o is_forbidden_mutant) *)
wenzelm@42429
   402
          |> map_filter (try (Sign.cert_term thy))
wenzelm@59621
   403
          |> filter (is_some o try (Thm.global_cterm_of thy))
wenzelm@42429
   404
          |> filter (is_some o try (Syntax.check_term (Proof_Context.init_global thy)))
bulwahn@40971
   405
          |> take_random max_mutants
wenzelm@58843
   406
    val _ = map (fn t => writeln ("MUTANT: " ^ Syntax.string_of_term_global thy t)) mutants
bulwahn@34965
   407
  in
bulwahn@34965
   408
    create_entry thy thm exec mutants mtds
bulwahn@34965
   409
  end
bulwahn@34965
   410
bulwahn@35324
   411
fun string_of_mutant_subentry' thy thm_name (t, results) =
bulwahn@35380
   412
  let
bulwahn@42089
   413
   (* fun string_of_report (Quickcheck.Report {iterations = i, raised_match_errors = e,
bulwahn@35380
   414
      satisfied_assms = s, positive_concl_tests = p}) =
bulwahn@35380
   415
      "errors: " ^ string_of_int e ^ "; conclusion tests: " ^ string_of_int p
bulwahn@35380
   416
    fun string_of_reports NONE = ""
bulwahn@35380
   417
      | string_of_reports (SOME reports) =
bulwahn@35380
   418
        cat_lines (map (fn (size, [report]) =>
bulwahn@42089
   419
          "size " ^ string_of_int size ^ ": " ^ string_of_report report) (rev reports))*)
bulwahn@42089
   420
    fun string_of_mtd_result (mtd_name, (outcome, timing)) =
bulwahn@40653
   421
      mtd_name ^ ": " ^ string_of_outcome outcome
bulwahn@49441
   422
      ^ "(" ^ space_implode "; " (map (fn (s, t) => (s ^ ": " ^ string_of_int t)) timing) ^ ")"
bulwahn@36255
   423
      (*^ "\n" ^ string_of_reports reports*)
bulwahn@35380
   424
  in
wenzelm@59433
   425
    "mutant of " ^ thm_name ^ ":\n" ^
wenzelm@59433
   426
      YXML.content_of (Syntax.string_of_term_global thy t) ^ "\n" ^
wenzelm@59433
   427
      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@58843
   458
    val _ = writeln "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;