1.1 --- a/src/HOL/TPTP/mash_import.ML Wed Jul 11 09:32:29 2012 +0200
1.2 +++ b/src/HOL/TPTP/mash_import.ML Wed Jul 11 11:28:10 2012 +0200
1.3 @@ -30,11 +30,17 @@
1.4
1.5 val of_fact_name = unescape_meta
1.6
1.7 +val depN = "Dependencies"
1.8 +val mengN = "Meng & Paulson"
1.9 +val mashN = "MaSh"
1.10 +val meng_mashN = "M&P+MaSh"
1.11 +
1.12 val max_relevant_slack = 2
1.13
1.14 fun import_and_evaluate_mash_suggestions ctxt thy file_name =
1.15 let
1.16 - val params as {provers, max_relevant, relevance_thresholds, ...} =
1.17 + val params as {provers, max_relevant, relevance_thresholds,
1.18 + slice, type_enc, lam_trans, timeout, ...} =
1.19 Sledgehammer_Isar.default_params ctxt []
1.20 val prover_name = hd provers
1.21 val path = file_name |> Path.explode
1.22 @@ -42,6 +48,10 @@
1.23 val facts = non_tautological_facts_of thy
1.24 val all_names = facts |> map (Thm.get_name_hint o snd)
1.25 val i = 1
1.26 + val meng_ok = Unsynchronized.ref 0
1.27 + val mash_ok = Unsynchronized.ref 0
1.28 + val meng_mash_ok = Unsynchronized.ref 0
1.29 + val dep_ok = Unsynchronized.ref 0
1.30 fun find_sugg facts sugg =
1.31 find_first (fn (_, th) => Thm.get_name_hint th = sugg) facts
1.32 fun sugg_facts hyp_ts concl_t facts =
1.33 @@ -49,7 +59,7 @@
1.34 #> take (max_relevant_slack * the max_relevant)
1.35 #> Sledgehammer_Filter.maybe_instantiate_inducts ctxt hyp_ts concl_t
1.36 #> map (apfst (apfst (fn name => name ())))
1.37 - fun hybrid_facts fs1 fs2 =
1.38 + fun meng_mash_facts fs1 fs2 =
1.39 let
1.40 val fact_eq = (op =) o pairself fst
1.41 fun score_in f fs =
1.42 @@ -69,22 +79,33 @@
1.43 " " ^ label ^ ": " ^
1.44 (if is_none outcome then
1.45 "Success (" ^ ATP_Util.string_from_time run_time ^ "): " ^
1.46 - space_implode " " (used_facts |> map (with_index facts o fst)
1.47 - |> sort (int_ord o pairself fst)
1.48 - |> map index_string)
1.49 + (used_facts |> map (with_index facts o fst)
1.50 + |> sort (int_ord o pairself fst)
1.51 + |> map index_string
1.52 + |> space_implode " ") ^
1.53 + (if length facts < the max_relevant then
1.54 + " (of " ^ string_of_int (length facts) ^ ")"
1.55 + else
1.56 + "")
1.57 else
1.58 - "Failure: " ^ space_implode " " (map (fst o fst) facts))
1.59 - fun run_sh heading facts goal =
1.60 + "Failure: " ^
1.61 + (facts |> map (fst o fst)
1.62 + |> tag_list 1
1.63 + |> map index_string
1.64 + |> space_implode " "))
1.65 + fun run_sh ok heading facts goal =
1.66 let
1.67 val problem =
1.68 {state = Proof.init ctxt, goal = goal, subgoal = i, subgoal_count = 1,
1.69 - facts = facts |> map Sledgehammer_Provers.Untranslated_Fact}
1.70 + facts = facts |> take (the max_relevant)
1.71 + |> map Sledgehammer_Provers.Untranslated_Fact}
1.72 val prover =
1.73 Sledgehammer_Run.get_minimizing_prover ctxt
1.74 Sledgehammer_Provers.Normal prover_name
1.75 val res as {outcome, ...} = prover params (K (K (K ""))) problem
1.76 - in (str_of_res heading facts res, is_none outcome) end
1.77 - fun solve_goal name suggs =
1.78 + val _ = if is_none outcome then ok := !ok + 1 else ()
1.79 + in str_of_res heading facts res end
1.80 + fun solve_goal j name suggs =
1.81 let
1.82 val name = of_fact_name name
1.83 val th =
1.84 @@ -101,19 +122,42 @@
1.85 (max_relevant_slack * the max_relevant) relevance_thresholds goal
1.86 i facts
1.87 val mash_facts = sugg_facts hyp_ts concl_t facts suggs
1.88 - val hybrid_facts = hybrid_facts meng_facts mash_facts
1.89 - val (dep_s, dep_ok) = run_sh "Dependencies" deps_facts goal
1.90 - val (meng_s, meng_ok) = run_sh "Meng & Paulson" meng_facts goal
1.91 - val (mash_s, mash_ok) = run_sh "MaSh" mash_facts goal
1.92 - val (hybrid_s, hybrid_ok) = run_sh "Hybrid" hybrid_facts goal
1.93 + val meng_mash_facts = meng_mash_facts meng_facts mash_facts
1.94 + val meng_s = run_sh meng_ok mengN meng_facts goal
1.95 + val mash_s = run_sh mash_ok mashN mash_facts goal
1.96 + val meng_mash_s = run_sh meng_mash_ok meng_mashN meng_mash_facts goal
1.97 + val dep_s = run_sh dep_ok depN deps_facts goal
1.98 in
1.99 - tracing (cat_lines ["Goal: ", name, dep_s, meng_s, mash_s, hybrid_s])
1.100 + ["Goal " ^ string_of_int j ^ ": " ^ name, meng_s, mash_s, meng_mash_s,
1.101 + dep_s]
1.102 + |> cat_lines |> tracing
1.103 end
1.104 val explode_suggs = space_explode " " #> filter_out (curry (op =) "")
1.105 - fun do_line line =
1.106 + fun do_line (j, line) =
1.107 case space_explode ":" line of
1.108 - [goal_name, suggs] => solve_goal goal_name (explode_suggs suggs)
1.109 + [goal_name, suggs] => solve_goal j goal_name (explode_suggs suggs)
1.110 | _ => ()
1.111 - in List.app do_line lines end
1.112 + fun total_of heading ok n =
1.113 + " " ^ heading ^ ": " ^ string_of_int (!ok) ^ " (" ^
1.114 + Real.fmt (StringCvt.FIX (SOME 1))
1.115 + (100.0 * Real.fromInt (!ok) / Real.fromInt n) ^ "%)"
1.116 + val inst_inducts = Config.get ctxt Sledgehammer_Filter.instantiate_inducts
1.117 + val params =
1.118 + [prover_name, string_of_int (the max_relevant) ^ " facts",
1.119 + "slice" |> not slice ? prefix "dont_", the_default "smart" type_enc,
1.120 + the_default "smart" lam_trans, ATP_Util.string_from_time timeout,
1.121 + "instantiate_inducts" |> not inst_inducts ? prefix "dont_"]
1.122 + val n = length lines
1.123 + in
1.124 + tracing " * * *";
1.125 + tracing ("Options: " ^ commas params);
1.126 + List.app do_line (tag_list 1 lines);
1.127 + ["Successes (of " ^ string_of_int n ^ " goals)",
1.128 + total_of mengN meng_ok n,
1.129 + total_of mashN mash_ok n,
1.130 + total_of meng_mashN meng_mash_ok n,
1.131 + total_of depN dep_ok n]
1.132 + |> cat_lines |> tracing
1.133 + end
1.134
1.135 end;