blanchet@49249: (* Title: HOL/TPTP/mash_import.ML blanchet@49249: Author: Jasmin Blanchette, TU Muenchen blanchet@49249: Copyright 2012 blanchet@49249: blanchet@49249: Import proof suggestions from MaSh (Machine-learning for Sledgehammer) and blanchet@49249: evaluate them. blanchet@49249: *) blanchet@49249: blanchet@49249: signature MASH_IMPORT = blanchet@49249: sig blanchet@49250: val import_and_evaluate_mash_suggestions : blanchet@49250: Proof.context -> theory -> string -> unit blanchet@49249: end; blanchet@49249: blanchet@49249: structure MaSh_Import : MASH_IMPORT = blanchet@49249: struct blanchet@49250: blanchet@49255: open MaSh_Export blanchet@49255: blanchet@49250: val unescape_meta = blanchet@49250: let blanchet@49250: fun un accum [] = String.implode (rev accum) blanchet@49250: | un accum (#"\\" :: d1 :: d2 :: d3 :: cs) = blanchet@49250: (case Int.fromString (String.implode [d1, d2, d3]) of blanchet@49250: SOME n => un (Char.chr n :: accum) cs blanchet@49250: | NONE => "" (* error *)) blanchet@49250: | un _ (#"\\" :: _) = "" (* error *) blanchet@49250: | un accum (c :: cs) = un (c :: accum) cs blanchet@49250: in un [] o String.explode end blanchet@49250: blanchet@49250: val of_fact_name = unescape_meta blanchet@49250: blanchet@49256: val depN = "Dependencies" blanchet@49256: val mengN = "Meng & Paulson" blanchet@49256: val mashN = "MaSh" blanchet@49256: val meng_mashN = "M&P+MaSh" blanchet@49256: blanchet@49254: val max_relevant_slack = 2 blanchet@49250: blanchet@49250: fun import_and_evaluate_mash_suggestions ctxt thy file_name = blanchet@49250: let blanchet@49260: val {provers, max_relevant, slice, type_enc, lam_trans, timeout, ...} = blanchet@49254: Sledgehammer_Isar.default_params ctxt [] blanchet@49254: val prover_name = hd provers blanchet@49250: val path = file_name |> Path.explode blanchet@49250: val lines = path |> File.read_lines blanchet@49250: val facts = non_tautological_facts_of thy blanchet@49250: val all_names = facts |> map (Thm.get_name_hint o snd) blanchet@49256: val meng_ok = Unsynchronized.ref 0 blanchet@49256: val mash_ok = Unsynchronized.ref 0 blanchet@49256: val meng_mash_ok = Unsynchronized.ref 0 blanchet@49256: val dep_ok = Unsynchronized.ref 0 blanchet@49250: fun find_sugg facts sugg = blanchet@49250: find_first (fn (_, th) => Thm.get_name_hint th = sugg) facts blanchet@49251: fun sugg_facts hyp_ts concl_t facts = blanchet@49250: map_filter (find_sugg facts o of_fact_name) blanchet@49254: #> take (max_relevant_slack * the max_relevant) blanchet@49265: #> Sledgehammer_Fact.maybe_instantiate_inducts ctxt hyp_ts concl_t blanchet@49250: #> map (apfst (apfst (fn name => name ()))) blanchet@49256: fun meng_mash_facts fs1 fs2 = blanchet@49250: let blanchet@49250: val fact_eq = (op =) o pairself fst blanchet@49250: fun score_in f fs = blanchet@49250: case find_index (curry fact_eq f) fs of blanchet@49250: ~1 => length fs blanchet@49250: | j => j blanchet@49250: fun score_of f = score_in f fs1 + score_in f fs2 blanchet@49250: in blanchet@49250: union fact_eq fs1 fs2 blanchet@49251: |> map (`score_of) |> sort (int_ord o pairself fst) |> map snd blanchet@49254: |> take (the max_relevant) blanchet@49250: end blanchet@49250: fun with_index facts s = blanchet@49250: (find_index (fn ((s', _), _) => s = s') facts + 1, s) blanchet@49250: fun index_string (j, s) = s ^ "@" ^ string_of_int j blanchet@49255: fun str_of_res label facts {outcome, run_time, used_facts, ...} = blanchet@49255: " " ^ label ^ ": " ^ blanchet@49255: (if is_none outcome then blanchet@49255: "Success (" ^ ATP_Util.string_from_time run_time ^ "): " ^ blanchet@49256: (used_facts |> map (with_index facts o fst) blanchet@49256: |> sort (int_ord o pairself fst) blanchet@49256: |> map index_string blanchet@49256: |> space_implode " ") ^ blanchet@49256: (if length facts < the max_relevant then blanchet@49256: " (of " ^ string_of_int (length facts) ^ ")" blanchet@49256: else blanchet@49256: "") blanchet@49255: else blanchet@49256: "Failure: " ^ blanchet@49256: (facts |> map (fst o fst) blanchet@49260: |> take (the max_relevant) blanchet@49256: |> tag_list 1 blanchet@49256: |> map index_string blanchet@49256: |> space_implode " ")) blanchet@49256: fun run_sh ok heading facts goal = blanchet@49254: let blanchet@49260: val facts = facts |> take (the max_relevant) blanchet@49260: val res as {outcome, ...} = run_sledgehammer ctxt facts goal blanchet@49256: val _ = if is_none outcome then ok := !ok + 1 else () blanchet@49256: in str_of_res heading facts res end blanchet@49256: fun solve_goal j name suggs = blanchet@49250: let blanchet@49250: val name = of_fact_name name blanchet@49250: val th = blanchet@49250: case find_first (fn (_, th) => Thm.get_name_hint th = name) facts of blanchet@49250: SOME (_, th) => th blanchet@49250: | NONE => error ("No fact called \"" ^ name ^ "\"") blanchet@49250: val deps = dependencies_of all_names th blanchet@49265: val goal = goal_of_thm thy th blanchet@49260: val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal 1 blanchet@49250: val facts = facts |> filter (fn (_, th') => thm_ord (th', th) = LESS) blanchet@49251: val deps_facts = sugg_facts hyp_ts concl_t facts deps blanchet@49254: val meng_facts = blanchet@49260: meng_paulson_facts ctxt (max_relevant_slack * the max_relevant) goal blanchet@49260: facts blanchet@49251: val mash_facts = sugg_facts hyp_ts concl_t facts suggs blanchet@49256: val meng_mash_facts = meng_mash_facts meng_facts mash_facts blanchet@49256: val meng_s = run_sh meng_ok mengN meng_facts goal blanchet@49256: val mash_s = run_sh mash_ok mashN mash_facts goal blanchet@49256: val meng_mash_s = run_sh meng_mash_ok meng_mashN meng_mash_facts goal blanchet@49256: val dep_s = run_sh dep_ok depN deps_facts goal blanchet@49250: in blanchet@49256: ["Goal " ^ string_of_int j ^ ": " ^ name, meng_s, mash_s, meng_mash_s, blanchet@49256: dep_s] blanchet@49256: |> cat_lines |> tracing blanchet@49250: end blanchet@49250: val explode_suggs = space_explode " " #> filter_out (curry (op =) "") blanchet@49256: fun do_line (j, line) = blanchet@49250: case space_explode ":" line of blanchet@49256: [goal_name, suggs] => solve_goal j goal_name (explode_suggs suggs) blanchet@49250: | _ => () blanchet@49256: fun total_of heading ok n = blanchet@49256: " " ^ heading ^ ": " ^ string_of_int (!ok) ^ " (" ^ blanchet@49256: Real.fmt (StringCvt.FIX (SOME 1)) blanchet@49256: (100.0 * Real.fromInt (!ok) / Real.fromInt n) ^ "%)" blanchet@49265: val inst_inducts = Config.get ctxt Sledgehammer_Fact.instantiate_inducts blanchet@49260: val options = blanchet@49256: [prover_name, string_of_int (the max_relevant) ^ " facts", blanchet@49256: "slice" |> not slice ? prefix "dont_", the_default "smart" type_enc, blanchet@49256: the_default "smart" lam_trans, ATP_Util.string_from_time timeout, blanchet@49256: "instantiate_inducts" |> not inst_inducts ? prefix "dont_"] blanchet@49256: val n = length lines blanchet@49256: in blanchet@49256: tracing " * * *"; blanchet@49260: tracing ("Options: " ^ commas options); blanchet@49256: List.app do_line (tag_list 1 lines); blanchet@49256: ["Successes (of " ^ string_of_int n ^ " goals)", blanchet@49256: total_of mengN meng_ok n, blanchet@49256: total_of mashN mash_ok n, blanchet@49256: total_of meng_mashN meng_mash_ok n, blanchet@49256: total_of depN dep_ok n] blanchet@49256: |> cat_lines |> tracing blanchet@49256: end blanchet@49250: blanchet@49249: end;