--- a/src/HOL/TPTP/MaSh_Eval.thy Thu Jan 17 23:00:20 2013 +0100
+++ b/src/HOL/TPTP/MaSh_Eval.thy Thu Jan 17 23:29:17 2013 +0100
@@ -27,6 +27,7 @@
ML {*
val do_it = false (* switch to "true" to generate the files *)
val params = Sledgehammer_Isar.default_params @{context} []
+val range = (1, NONE)
val dir = "List"
val prefix = "/tmp/" ^ dir ^ "/"
val prob_dir = prefix ^ "mash_problems"
@@ -41,10 +42,15 @@
ML {*
if do_it then
- evaluate_mash_suggestions @{context} params (1, NONE)
+ evaluate_mash_suggestions @{context} params range
[MePoN, MaSh_IsarN, MaSh_ProverN, MeSh_IsarN, MeSh_ProverN, IsarN]
- (SOME prob_dir) (prefix ^ "mash_suggestions")
- (prefix ^ "mash_prover_suggestions") (prefix ^ "mash_eval")
+ (SOME prob_dir)
+ (prefix ^ "mepo_suggestions")
+ (prefix ^ "mash_suggestions")
+ (prefix ^ "mash_prover_suggestions")
+ (prefix ^ "mesh_suggestions")
+ (prefix ^ "mesh_prover_suggestions")
+ (prefix ^ "mash_eval")
else
()
*}
--- a/src/HOL/TPTP/mash_eval.ML Thu Jan 17 23:00:20 2013 +0100
+++ b/src/HOL/TPTP/mash_eval.ML Thu Jan 17 23:29:17 2013 +0100
@@ -17,7 +17,7 @@
val IsarN : string
val evaluate_mash_suggestions :
Proof.context -> params -> int * int option -> string list -> string option
- -> string -> string -> string -> unit
+ -> string -> string -> string -> string -> string -> string -> unit
end;
structure MaSh_Eval : MASH_EVAL =
@@ -41,7 +41,8 @@
j >= from andalso (to = NONE orelse j <= the to)
fun evaluate_mash_suggestions ctxt params range methods prob_dir_name
- isar_sugg_file_name prover_sugg_file_name report_file_name =
+ mepo_file_name mash_isar_file_name mash_prover_file_name
+ mesh_isar_file_name mesh_prover_file_name report_file_name =
let
val report_path = report_file_name |> Path.explode
val _ = File.write report_path ""
@@ -50,12 +51,18 @@
default_params ctxt []
val prover = hd provers
val slack_max_facts = generous_max_facts (the max_facts)
- val mash_isar_lines = Path.explode isar_sugg_file_name |> File.read_lines
- val mash_prover_lines =
- case Path.explode prover_sugg_file_name |> try File.read_lines of
- NONE => replicate (length mash_isar_lines) ""
- | SOME lines => lines
- val mash_lines = mash_isar_lines ~~ mash_prover_lines
+ val lines_of = Path.explode #> try File.read_lines #> these
+ val file_names =
+ [mepo_file_name, mash_isar_file_name, mash_prover_file_name,
+ mesh_isar_file_name, mesh_prover_file_name]
+ val lines as [mepo_lines, mash_isar_lines, mash_prover_lines,
+ mesh_isar_lines, mesh_prover_lines] =
+ map lines_of file_names
+ val num_lines = fold (Integer.max o length) lines 0
+ fun pad lines = lines @ replicate (num_lines - length lines) ""
+ val lines =
+ pad mepo_lines ~~ pad mash_isar_lines ~~ pad mash_prover_lines ~~
+ pad mesh_isar_lines ~~ pad mesh_prover_lines
val css = clasimpset_rule_table_of ctxt
val facts = all_facts ctxt true false Symtab.empty [] [] css
val name_tabs = build_name_tables nickname_of_thm facts
@@ -82,11 +89,19 @@
|> map index_str
|> space_implode " "))
end
- fun solve_goal (j, (mash_isar_line, mash_prover_line)) =
+ fun solve_goal (j, ((((mepo_line, mash_isar_line), mash_prover_line),
+ mesh_isar_line), mesh_prover_line)) =
if in_range range j then
let
- val (name, mash_isar_suggs) = extract_suggestions mash_isar_line
- val (_, mash_prover_suggs) = extract_suggestions mash_prover_line
+ val (name1, mepo_suggs) = extract_suggestions mepo_line
+ val (name2, mash_isar_suggs) = extract_suggestions mash_isar_line
+ val (name3, mash_prover_suggs) = extract_suggestions mash_prover_line
+ val (name4, mesh_isar_suggs) = extract_suggestions mesh_isar_line
+ val (name5, mesh_prover_suggs) = extract_suggestions mesh_prover_line
+ val [name] =
+ [name1, name2, name3, name4, name5]
+ |> filter (curry (op <>) "") |> distinct (op =)
+ handle General.Match => error "Input files out of sync."
val th =
case find_first (fn (_, th) => nickname_of_thm th = name) facts of
SOME (_, th) => th
@@ -95,24 +110,29 @@
val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal 1
val isar_deps = isar_dependencies_of name_tabs th
val facts = facts |> filter (fn (_, th') => thm_ord (th', th) = LESS)
+ fun get_facts [] compute = compute facts
+ | get_facts suggs _ = find_suggested_facts suggs facts
val mepo_facts =
- mepo_suggested_facts ctxt params prover slack_max_facts NONE hyp_ts
- concl_t facts
- |> weight_mepo_facts
+ get_facts mepo_suggs (fn _ =>
+ mepo_suggested_facts ctxt params prover slack_max_facts NONE
+ hyp_ts concl_t facts
+ |> weight_mepo_facts)
fun mash_of suggs =
- find_mash_suggestions slack_max_facts suggs facts [] []
- |>> weight_mash_facts
- val (mash_isar_facts, mash_isar_unks) = mash_of mash_isar_suggs
- val (mash_prover_facts, mash_prover_unks) = mash_of mash_prover_suggs
- fun mess_of mash_facts mash_unks =
+ get_facts suggs (fn _ =>
+ find_mash_suggestions slack_max_facts suggs facts [] []
+ |> fst |> weight_mash_facts)
+ val mash_isar_facts = mash_of mash_isar_suggs
+ val mash_prover_facts = mash_of mash_prover_suggs
+ fun mess_of mash_facts =
[(mepo_weight, (mepo_facts, [])),
- (mash_weight, (mash_facts, mash_unks))]
- fun mesh_of [] _ = []
- | mesh_of mash_facts mash_unks =
- mesh_facts (Thm.eq_thm_prop o pairself snd) slack_max_facts
- (mess_of mash_facts mash_unks)
- val mesh_isar_facts = mesh_of mash_isar_facts mash_isar_unks
- val mesh_prover_facts = mesh_of mash_prover_facts mash_prover_unks
+ (mash_weight, (mash_facts, []))]
+ fun mesh_of suggs mash_facts =
+ get_facts suggs (fn _ =>
+ mesh_facts (Thm.eq_thm_prop o pairself snd) slack_max_facts
+ (mess_of mash_facts)
+ |> map (rpair 1.0))
+ val mesh_isar_facts = mesh_of mesh_isar_suggs mash_isar_facts
+ val mesh_prover_facts = mesh_of mesh_prover_suggs mash_prover_facts
val isar_facts =
find_suggested_facts (map (rpair 1.0) isar_deps) facts
(* adapted from "mirabelle_sledgehammer.ML" *)
@@ -127,7 +147,7 @@
#> Config.put SMT_Config.debug_files (dir ^ "/" ^ prob_prefix)
end
| set_file_name _ NONE = I
- fun prove method get facts =
+ fun prove method facts =
if not (member (op =) methods method) orelse
(null facts andalso method <> IsarN) then
(str_of_method method ^ "Skipped", 0)
@@ -137,7 +157,7 @@
((K (encode_str (nickname_of_thm th)), stature), th)
val facts =
facts
- |> map (get #> nickify)
+ |> map (fst #> nickify)
|> maybe_instantiate_inducts ctxt hyp_ts concl_t
|> take (the max_facts)
val ctxt = ctxt |> set_file_name method prob_dir_name
@@ -146,12 +166,12 @@
val ok = if is_none outcome then 1 else 0
in (str_of_result method facts res, ok) end
val ress =
- [fn () => prove MePoN fst mepo_facts,
- fn () => prove MaSh_IsarN fst mash_isar_facts,
- fn () => prove MaSh_ProverN fst mash_prover_facts,
- fn () => prove MeSh_IsarN I mesh_isar_facts,
- fn () => prove MeSh_ProverN I mesh_prover_facts,
- fn () => prove IsarN fst isar_facts]
+ [fn () => prove MePoN mepo_facts,
+ fn () => prove MaSh_IsarN mash_isar_facts,
+ fn () => prove MaSh_ProverN mash_prover_facts,
+ fn () => prove MeSh_IsarN mesh_isar_facts,
+ fn () => prove MeSh_ProverN mesh_prover_facts,
+ fn () => prove IsarN isar_facts]
|> (* Par_List. *) map (fn f => f ())
in
"Goal " ^ string_of_int j ^ ": " ^ name :: map fst ress
@@ -175,7 +195,7 @@
"instantiate_inducts" |> not inst_inducts ? prefix "dont_"]
val _ = print " * * *";
val _ = print ("Options: " ^ commas options);
- val oks = Par_List.map solve_goal (tag_list 1 mash_lines)
+ val oks = Par_List.map solve_goal (tag_list 1 lines)
val n = length oks
val [mepo_ok, mash_isar_ok, mash_prover_ok, mesh_isar_ok, mesh_prover_ok,
isar_ok] =