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