# HG changeset patch # User blanchet # Date 1357857259 -3600 # Node ID 4247cbd78aaf3f9ca3eda559404a38916faa0c3a # Parent b6659475b5afb4748f50187ac76b28346a3fb790 export MeSh data as well diff -r b6659475b5af -r 4247cbd78aaf src/HOL/TPTP/MaSh_Export.thy --- a/src/HOL/TPTP/MaSh_Export.thy Thu Jan 10 23:02:58 2013 +0100 +++ b/src/HOL/TPTP/MaSh_Export.thy Thu Jan 10 23:34:19 2013 +0100 @@ -29,6 +29,7 @@ val thys = [@{theory List}] val params as {provers, ...} = Sledgehammer_Isar.default_params @{context} [] val prover = hd provers +val max_suggestions = 1024 val dir = "List" val prefix = "/tmp/" ^ dir ^ "/" *} @@ -70,9 +71,17 @@ *} ML {* +if true orelse do_it then + generate_mepo_suggestions @{context} params thys max_suggestions + (prefix ^ "mepo_suggestions") +else + () +*} + +ML {* if do_it then - generate_mepo_suggestions @{context} params thys 1024 - (prefix ^ "mash_mepo_suggestions") + generate_mesh_suggestions max_suggestions (prefix ^ "mash_suggestions") + (prefix ^ "mepo_suggestions") (prefix ^ "mesh_suggestions") else () *} diff -r b6659475b5af -r 4247cbd78aaf src/HOL/TPTP/mash_eval.ML --- a/src/HOL/TPTP/mash_eval.ML Thu Jan 10 23:02:58 2013 +0100 +++ b/src/HOL/TPTP/mash_eval.ML Thu Jan 10 23:34:19 2013 +0100 @@ -42,8 +42,7 @@ default_params ctxt [] val prover = hd provers val slack_max_facts = generous_max_facts (the max_facts) - val sugg_path = sugg_file_name |> Path.explode - val lines = sugg_path |> File.read_lines + val lines = Path.explode sugg_file_name |> File.read_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 @@ -88,8 +87,11 @@ val (mash_facts, mash_unks) = find_mash_suggestions slack_max_facts suggs facts [] [] |>> weight_mash_facts - val mess = [(0.5, (mepo_facts, [])), (0.5, (mash_facts, mash_unks))] - val mesh_facts = mesh_facts slack_max_facts mess + val mess = + [(mepo_weight, (mepo_facts, [])), + (mash_weight, (mash_facts, mash_unks))] + val mesh_facts = + mesh_facts (Thm.eq_thm o pairself snd) slack_max_facts mess val isar_facts = find_suggested_facts (map (rpair 1.0) isar_deps) facts (* adapted from "mirabelle_sledgehammer.ML" *) diff -r b6659475b5af -r 4247cbd78aaf src/HOL/TPTP/mash_export.ML --- a/src/HOL/TPTP/mash_export.ML Thu Jan 10 23:02:58 2013 +0100 +++ b/src/HOL/TPTP/mash_export.ML Thu Jan 10 23:34:19 2013 +0100 @@ -24,6 +24,7 @@ Proof.context -> params -> int * int option -> theory list -> string -> unit val generate_mepo_suggestions : Proof.context -> params -> theory list -> int -> string -> unit + val generate_mesh_suggestions : int -> string -> string -> string -> unit end; structure MaSh_Export : MASH_EXPORT = @@ -164,16 +165,17 @@ generate_isar_or_prover_commands ctxt prover (SOME params) fun generate_mepo_suggestions ctxt (params as {provers = prover :: _, ...}) thys - max_facts file_name = + max_suggs file_name = let val ho_atp = Sledgehammer_Provers.is_ho_atp ctxt prover val path = file_name |> Path.explode val facts = all_facts ctxt val (new_facts, old_facts) = facts |> List.partition (has_thys thys o snd) val name_tabs = build_name_tables nickname_of_thm facts - fun do_fact ((_, th), old_facts) = + fun do_fact (j, ((_, th), old_facts)) = let val name = nickname_of_thm th + val _ = tracing ("Fact " ^ string_of_int j ^ ": " ^ name) val goal = goal_of_thm (Proof_Context.theory_of ctxt) th val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal 1 val isar_deps = isar_dependencies_of name_tabs th @@ -185,13 +187,38 @@ val suggs = old_facts |> Sledgehammer_MePo.mepo_suggested_facts ctxt params prover - max_facts NONE hyp_ts concl_t + max_suggs NONE hyp_ts concl_t |> map (nickname_of_thm o snd) in escape_meta name ^ ": " ^ escape_metas suggs ^ "\n" end end fun accum x (yss as ys :: _) = (x :: ys) :: yss val old_factss = tl (fold accum new_facts [old_facts]) - val lines = Par_List.map do_fact (new_facts ~~ rev old_factss) + val lines = Par_List.map do_fact (tag_list 1 (new_facts ~~ rev old_factss)) in File.write_list path lines end +fun generate_mesh_suggestions max_suggs mash_file_name mepo_file_name + mesh_file_name = + let + val mesh_path = Path.explode mesh_file_name + val _ = File.write mesh_path "" + fun do_fact (mash_line, mepo_line) = + let + val (mash_name, mash_suggs) = + extract_suggestions mash_line + ||> (map fst #> weight_mash_facts) + val (mepo_name, mepo_suggs) = + extract_suggestions mepo_line + ||> (map fst #> weight_mash_facts) + val _ = + if mash_name = mepo_name then () else error "Input files out of sync." + val mess = + [(mepo_weight, (mepo_suggs, [])), + (mash_weight, (mash_suggs, []))] + val mesh_suggs = mesh_facts (op =) max_suggs mess + val mesh_line = mash_name ^ ": " ^ space_implode " " mesh_suggs ^ "\n" + in File.append mesh_path mesh_line end + val mash_lines = Path.explode mash_file_name |> File.read_lines + val mepo_lines = Path.explode mepo_file_name |> File.read_lines + in List.app do_fact (mash_lines ~~ mepo_lines) end + end; diff -r b6659475b5af -r 4247cbd78aaf src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Thu Jan 10 23:02:58 2013 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Thu Jan 10 23:34:19 2013 +0100 @@ -49,8 +49,8 @@ val find_suggested_facts : (string * 'a) list -> ('b * thm) list -> (('b * thm) * 'a) list val mesh_facts : - int -> (real * ((('a * thm) * real) list * ('a * thm) list)) list - -> ('a * thm) list + ('a * 'a -> bool) -> int -> (real * (('a * real) list * 'a list)) list + -> 'a list val theory_ord : theory * theory -> order val thm_ord : thm * thm -> order val goal_of_thm : theory -> thm -> thm @@ -81,6 +81,8 @@ val is_mash_enabled : unit -> bool val mash_can_suggest_facts : Proof.context -> bool val generous_max_facts : int -> int + val mepo_weight : real + val mash_weight : real val relevant_facts : Proof.context -> params -> string -> int -> fact_override -> term list -> term -> fact list -> fact list @@ -444,13 +446,13 @@ map (apsnd (curry Real.* (1.0 / avg))) xs end -fun mesh_facts max_facts [(_, (sels, unks))] = +fun mesh_facts _ max_facts [(_, (sels, unks))] = map fst (take max_facts sels) @ take (max_facts - length sels) unks - | mesh_facts max_facts mess = + | mesh_facts eq max_facts mess = let val mess = mess |> map (apsnd (apfst (normalize_scores max_facts #> `length))) - val fact_eq = Thm.eq_thm o pairself snd + val fact_eq = eq fun score_in fact (global_weight, ((sel_len, sels), unks)) = let fun score_at j = @@ -769,7 +771,7 @@ val unknown = raw_unknown |> fold (subtract (Thm.eq_thm_prop o pairself snd)) [chained, proximity] - in (mesh_facts max_facts mess, unknown) end + in (mesh_facts (Thm.eq_thm o pairself snd) max_facts mess, unknown) end fun mash_suggested_facts ctxt ({overlord, ...} : params) prover max_facts hyp_ts concl_t facts = @@ -1054,6 +1056,9 @@ later for various reasons. *) fun generous_max_facts max_facts = max_facts + Int.min (50, max_facts div 2) +val mepo_weight = 0.5 +val mash_weight = 0.5 + (* The threshold should be large enough so that MaSh doesn't kick in for Auto Sledgehammer and Try. *) val min_secs_for_learning = 15 @@ -1106,10 +1111,12 @@ hyp_ts concl_t facts |>> weight_mash_facts val mess = - [] |> (if fact_filter <> mashN then cons (0.5, (mepo (), [])) else I) - |> (if fact_filter <> mepoN then cons (0.5, (mash ())) else I) + [] |> (if fact_filter <> mashN then cons (mepo_weight, (mepo (), [])) + else I) + |> (if fact_filter <> mepoN then cons (mash_weight, (mash ())) + else I) in - mesh_facts max_facts mess + mesh_facts (Thm.eq_thm o pairself snd) max_facts mess |> not (null add_ths) ? prepend_facts add_ths end