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