--- 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
()
*}
--- 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" *)
--- 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;
--- 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