# HG changeset patch # User blanchet # Date 1358461757 -3600 # Node ID 2a990baa09af4fa2b468b49d353cf4d2b7fa2a53 # Parent 23ed79fc2b4da01582aefefd6b7d33a2757b99c7 use precomputed MaSh/MePo data whenever available diff -r 23ed79fc2b4d -r 2a990baa09af src/HOL/TPTP/MaSh_Eval.thy --- 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 () *} diff -r 23ed79fc2b4d -r 2a990baa09af src/HOL/TPTP/MaSh_Export.thy --- a/src/HOL/TPTP/MaSh_Export.thy Thu Jan 17 23:00:20 2013 +0100 +++ b/src/HOL/TPTP/MaSh_Export.thy Thu Jan 17 23:29:17 2013 +0100 @@ -31,7 +31,7 @@ val prover = hd provers val range = (1, NONE) val step = 1 -val max_suggestions = 1536 +val max_suggestions = 1024 val dir = "List" val prefix = "/tmp/" ^ dir ^ "/" *} diff -r 23ed79fc2b4d -r 2a990baa09af src/HOL/TPTP/mash_eval.ML --- 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] =