--- a/src/HOL/TPTP/mash_eval.ML Fri Jun 27 16:52:50 2014 +0200
+++ b/src/HOL/TPTP/mash_eval.ML Fri Jun 27 17:05:22 2014 +0200
@@ -15,8 +15,8 @@
val MeSh_IsarN : string
val MeSh_ProverN : string
val IsarN : string
- val evaluate_mash_suggestions : Proof.context -> params -> int * int option -> bool ->
- string list -> string option -> string -> string -> string -> string -> string -> string -> unit
+ val evaluate_mash_suggestions : Proof.context -> params -> int * int option -> string list ->
+ string option -> string -> string -> string -> string -> string -> string -> unit
end;
structure MaSh_Eval : MASH_EVAL =
@@ -41,9 +41,9 @@
fun in_range (from, to) j =
j >= from andalso (to = NONE orelse j <= the to)
-fun evaluate_mash_suggestions ctxt params range linearize methods prob_dir_name
- mepo_file_name mash_isar_file_name mash_prover_file_name
- mesh_isar_file_name mesh_prover_file_name report_file_name =
+fun evaluate_mash_suggestions ctxt params range methods prob_dir_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 thy = Proof_Context.theory_of ctxt
val zeros = [0, 0, 0, 0, 0, 0]
@@ -112,11 +112,7 @@
val goal = goal_of_thm (Proof_Context.theory_of ctxt) th
val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal goal 1 ctxt
val isar_deps = these (isar_dependencies_of name_tabs th)
- val facts =
- facts
- |> filter (fn (_, th') =>
- if linearize then crude_thm_ord (th', th) = LESS
- else thm_less (th', th))
+ val facts = facts |> filter (fn (_, th') => thm_less (th', th))
(* adapted from "mirabelle_sledgehammer.ML" *)
fun set_file_name method (SOME dir) =
let
--- a/src/HOL/TPTP/mash_export.ML Fri Jun 27 16:52:50 2014 +0200
+++ b/src/HOL/TPTP/mash_export.ML Fri Jun 27 17:05:22 2014 +0200
@@ -54,9 +54,9 @@
let
val path = Path.explode file_name
- fun do_fact (parents, fact) prevs =
+ fun do_fact (parents, fact) =
let val s = encode_str fact ^ ": " ^ encode_strs parents ^ "\n" in
- File.append path s; [fact]
+ File.append path s
end
val facts =
@@ -66,7 +66,7 @@
|> map (apsnd (nickname_of_thm o snd))
in
File.write path "";
- ignore (fold do_fact facts [])
+ List.app do_fact facts
end
fun generate_features ctxt thys file_name =
@@ -78,8 +78,7 @@
fun do_fact ((_, stature), th) =
let
val name = nickname_of_thm th
- val feats =
- features_of ctxt (theory_of_thm th) 0 Symtab.empty stature [prop_of th] |> map fst
+ val feats = features_of ctxt (theory_of_thm th) stature [prop_of th]
val s = encode_str name ^ ": " ^ encode_strs (sort string_ord feats) ^ "\n"
in
File.append path s
@@ -161,26 +160,23 @@
val path = Path.explode file_name
val facts = all_facts ctxt
val (new_facts, old_facts) = facts |> List.partition (has_thys thys o snd)
- val num_old_facts = length old_facts
val name_tabs = build_name_tables nickname_of_thm facts
- fun do_fact (j, (((name, (parents, ((_, stature), th))), prevs), const_tab)) =
+ fun do_fact (j, ((name, (parents, ((_, stature), th))), prevs)) =
if in_range range j then
let
val _ = tracing ("Fact " ^ string_of_int j ^ ": " ^ name)
val isar_deps = isar_dependencies_of name_tabs th
val do_query = not (is_bad_query ctxt ho_atp step j th isar_deps)
- val goal_feats =
- features_of ctxt (theory_of_thm th) (num_old_facts + j) const_tab stature [prop_of th]
- |> sort_wrt fst
+ val goal_feats = features_of ctxt (theory_of_thm th) stature [prop_of th]
val access_facts = filter_accessible_from th new_facts @ old_facts
val (marker, deps) =
smart_dependencies_of ctxt params_opt access_facts name_tabs th isar_deps
fun extra_features_of (((_, stature), th), weight) =
[prop_of th]
- |> features_of ctxt (theory_of_thm th) (num_old_facts + j) const_tab stature
- |> map (apsnd (fn r => weight * extra_feature_factor * r))
+ |> features_of ctxt (theory_of_thm th) stature
+ |> map (rpair (weight * extra_feature_factor))
val query =
if do_query then
@@ -192,7 +188,8 @@
|> rev
|> weight_facts_steeply
|> map extra_features_of
- |> rpair goal_feats |-> fold (union (eq_fst (op =)))
+ |> rpair (map (rpair 1.0) goal_feats)
+ |-> fold (union (eq_fst (op =)))
in
"? " ^ string_of_int max_suggs ^ " # " ^ encode_str name ^ ": " ^
encode_strs parents ^ "; " ^ encode_features query_feats ^ "\n"
@@ -200,8 +197,8 @@
else
""
val update =
- "! " ^ encode_str name ^ ": " ^ encode_strs parents ^ "; " ^
- encode_strs (map fst goal_feats) ^ "; " ^ marker ^ " " ^ encode_strs deps ^ "\n"
+ "! " ^ encode_str name ^ ": " ^ encode_strs parents ^ "; " ^ encode_strs goal_feats ^
+ "; " ^ marker ^ " " ^ encode_strs deps ^ "\n"
in query ^ update end
else
""
@@ -210,10 +207,7 @@
new_facts |> attach_parents_to_facts old_facts |> map (`(nickname_of_thm o snd o snd))
val hd_prevs = map (nickname_of_thm o snd) (the_list (try List.last old_facts))
val prevss = hd_prevs :: map (single o fst) new_facts |> split_last |> fst
- val hd_const_tabs = fold (add_const_counts o prop_of o snd) old_facts Symtab.empty
- val (const_tabs, _) =
- fold_map (`I oo add_const_counts o prop_of o snd o snd o snd) new_facts hd_const_tabs
- val lines = map do_fact (tag_list 1 (new_facts ~~ prevss ~~ const_tabs))
+ val lines = map do_fact (tag_list 1 (new_facts ~~ prevss))
in
File.write_list path lines
end
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Fri Jun 27 16:52:50 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Fri Jun 27 17:05:22 2014 +0200
@@ -54,8 +54,7 @@
val goal_of_thm : theory -> thm -> thm
val run_prover_for_mash : Proof.context -> params -> string -> string -> fact list -> thm ->
prover_result
- val features_of : Proof.context -> theory -> int -> int Symtab.table -> stature -> term list ->
- string list
+ val features_of : Proof.context -> theory -> stature -> term list -> string list
val trim_dependencies : string list -> string list option
val isar_dependencies_of : string Symtab.table * string Symtab.table -> thm -> string list option
val prover_dependencies_of : Proof.context -> params -> string -> int -> raw_fact list ->
@@ -68,7 +67,6 @@
val weight_facts_steeply : 'a list -> ('a * real) list
val find_mash_suggestions : Proof.context -> int -> string list -> ('b * thm) list ->
('b * thm) list -> ('b * thm) list -> ('b * thm) list * ('b * thm) list
- val add_const_counts : term -> int Symtab.table -> int Symtab.table
val mash_suggested_facts : Proof.context -> params -> int -> term list -> term -> raw_fact list ->
fact list * fact list
val mash_learn_proof : Proof.context -> params -> term -> ('a * thm) list -> thm list -> unit
@@ -320,10 +318,10 @@
structure MaSh_SML =
struct
-exception BOTTOM of int
-
fun heap cmp bnd al a =
let
+ exception BOTTOM of int
+
fun maxson l i =
let val i31 = i + i + i + 1 in
if i31 + 2 < l then
@@ -395,10 +393,10 @@
Array.update (recommends, at, (j, big_number + ov))
end)
-exception EXIT of unit
-
fun k_nearest_neighbors dffreq num_facts depss feat_facts max_suggs visible_facts goal_feats =
let
+ exception EXIT of unit
+
val ln_afreq = Math.ln (Real.fromInt num_facts)
fun tfidf feat = ln_afreq - Math.ln (Real.fromInt (Vector.sub (dffreq, feat)))
@@ -968,7 +966,7 @@
val max_pat_breadth = 10 (* FUDGE *)
-fun term_features_of ctxt thy_name num_facts const_tab term_max_depth type_max_depth ts =
+fun term_features_of ctxt thy_name term_max_depth type_max_depth ts =
let
val thy = Proof_Context.theory_of ctxt
@@ -1060,10 +1058,10 @@
val type_max_depth = 1
(* TODO: Generate type classes for types? *)
-fun features_of ctxt thy num_facts const_tab (scope, _) ts =
+fun features_of ctxt thy (scope, _) ts =
let val thy_name = Context.theory_name thy in
thy_feature_of thy_name ::
- term_features_of ctxt thy_name num_facts const_tab term_max_depth type_max_depth ts
+ term_features_of ctxt thy_name term_max_depth type_max_depth ts
|> scope <> Global ? cons local_feature
end
@@ -1291,9 +1289,6 @@
(mesh_facts (eq_snd (gen_eq_thm ctxt)) max_facts mess, unknown)
end
-fun add_const_counts t =
- fold (fn s => Symtab.map_default (s, 0) (Integer.add 1)) (Term.add_const_names t [])
-
fun mash_suggested_facts ctxt ({debug, overlord, ...} : params) max_suggs hyp_ts concl_t facts =
let
val thy = Proof_Context.theory_of ctxt
@@ -1302,26 +1297,20 @@
val facts = facts |> sort (crude_thm_ord o pairself snd o swap)
val chained = facts |> filter (fn ((_, (scope, _)), _) => scope = Chained)
- val num_facts = length facts
-
- (* Weights appear to hurt kNN more than they help. *)
- val const_tab = Symtab.empty |> engine <> MaSh_SML_kNN
- ? fold (add_const_counts o prop_of o snd) facts
fun fact_has_right_theory (_, th) =
thy_name = Context.theory_name (theory_of_thm th)
fun chained_or_extra_features_of factor (((_, stature), th), weight) =
[prop_of th]
- |> features_of ctxt (theory_of_thm th) num_facts const_tab stature
+ |> features_of ctxt (theory_of_thm th) stature
|> map (rpair (weight * factor))
fun query_args access_G =
let
val parents = maximal_wrt_access_graph access_G facts
- val goal_feats =
- features_of ctxt thy num_facts const_tab (Local, General) (concl_t :: hyp_ts)
+ val goal_feats = features_of ctxt thy (Local, General) (concl_t :: hyp_ts)
val chained_feats = chained
|> map (rpair 1.0)
|> map (chained_or_extra_features_of chained_feature_factor)
@@ -1435,7 +1424,7 @@
launch_thread timeout (fn () =>
let
val thy = Proof_Context.theory_of ctxt
- val feats = features_of ctxt thy 0 Symtab.empty (Local, General) [t]
+ val feats = features_of ctxt thy (Local, General) [t]
in
map_state ctxt overlord
(fn state as {access_G, xtabs as ((num_facts0, _), _), ffds, freqs, dirty_facts} =>
@@ -1554,7 +1543,7 @@
(learns, (num_nontrivial, next_commit, _)) =
let
val name = nickname_of_thm th
- val feats = features_of ctxt (theory_of_thm th) 0 Symtab.empty stature [prop_of th]
+ val feats = features_of ctxt (theory_of_thm th) stature [prop_of th]
val deps = deps_of status th |> these
val num_nontrivial = num_nontrivial |> not (null deps) ? Integer.add 1
val learns = (name, parents, feats, deps) :: learns