--- a/src/HOL/TPTP/MaSh_Export.thy Fri May 30 12:27:51 2014 +0200
+++ b/src/HOL/TPTP/MaSh_Export.thy Fri May 30 12:27:51 2014 +0200
@@ -8,7 +8,6 @@
imports Main
begin
-ML_file "~~/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML" (*###*)
ML_file "mash_export.ML"
sledgehammer_params
@@ -28,11 +27,11 @@
*}
ML {*
-val do_it = true (*###*) (* switch to "true" to generate the files *)
+val do_it = false (* switch to "true" to generate the files *)
val thys = [@{theory List}]
val params as {provers, ...} = Sledgehammer_Commands.default_params @{theory} []
val prover = hd provers
-val range = (1, (* ### NONE *) SOME 100)
+val range = (1, NONE)
val step = 1
val max_suggestions = 1024
val dir = "List"
@@ -51,7 +50,7 @@
ML {*
if do_it then
generate_mash_suggestions @{context} params (range, step) thys max_suggestions
- (prefix ^ "mash_sml_knn_suggestions")
+ (prefix ^ "mash_sml_nb_suggestions")
else
()
*}
@@ -60,8 +59,8 @@
ML {*
if do_it then
- generate_mepo_suggestions @{context} params (range, step) thys max_suggestions
- (prefix ^ "mash_sml_nb_suggestions")
+ generate_mash_suggestions @{context} params (range, step) thys max_suggestions
+ (prefix ^ "mash_sml_knn_suggestions")
else
()
*}
@@ -70,8 +69,8 @@
ML {*
if do_it then
- generate_mepo_suggestions @{context} params (range, step) thys max_suggestions
- (prefix ^ "mepo_suggestions")
+ generate_mash_suggestions @{context} params (range, step) thys max_suggestions
+ (prefix ^ "mash_py_suggestions")
else
()
*}
--- a/src/HOL/TPTP/mash_export.ML Fri May 30 12:27:51 2014 +0200
+++ b/src/HOL/TPTP/mash_export.ML Fri May 30 12:27:51 2014 +0200
@@ -53,13 +53,11 @@
fun generate_accessibility ctxt thys file_name =
let
val path = Path.explode file_name
- val _ = File.write path ""
fun do_fact (parents, fact) prevs =
- let
- val s = encode_str fact ^ ": " ^ encode_strs parents ^ "\n"
- val _ = File.append path s
- in [fact] end
+ let val s = encode_str fact ^ ": " ^ encode_strs parents ^ "\n" in
+ File.append path s; [fact]
+ end
val facts =
all_facts ctxt
@@ -67,7 +65,8 @@
|> attach_parents_to_facts []
|> map (apsnd (nickname_of_thm o snd))
in
- fold do_fact facts []; ()
+ File.write path "";
+ ignore (fold do_fact facts [])
end
fun generate_features ctxt thys file_name =
@@ -75,13 +74,16 @@
val path = file_name |> Path.explode
val _ = File.write path ""
val facts = all_facts ctxt |> filter_out (has_thys thys o snd)
+
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 s = encode_str name ^ ": " ^ encode_strs (sort string_ord feats) ^ "\n"
- in File.append path s end
+ in
+ File.append path s
+ end
in
List.app do_fact facts
end
@@ -169,11 +171,12 @@
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 (SOME isar_deps)
- val parents = parents
+
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))
+
val query =
if do_query then
let
@@ -186,9 +189,8 @@
|> map extra_features_of
|> rpair goal_feats |-> fold (union (eq_fst (op =)))
in
- "? " ^ string_of_int max_suggs ^ " # " ^
- encode_str name ^ ": " ^ encode_strs parents ^ "; " ^
- encode_features query_feats ^ "\n"
+ "? " ^ string_of_int max_suggs ^ " # " ^ encode_str name ^ ": " ^
+ encode_strs parents ^ "; " ^ encode_features query_feats ^ "\n"
end
else
""
@@ -198,9 +200,9 @@
in query ^ update end
else
""
+
val new_facts =
- new_facts |> attach_parents_to_facts old_facts
- |> map (`(nickname_of_thm o snd o snd))
+ 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
@@ -269,7 +271,7 @@
generate_mepo_or_mash_suggestions
(fn ctxt => fn params as {provers = prover :: _, ...} => fn max_suggs => fn hyp_ts =>
fn concl_t =>
- tap (Sledgehammer_MaSh.mash_learn_facts ctxt params prover false 2 false
+ tap (Sledgehammer_MaSh.mash_learn_facts ctxt params prover true 2 false
Sledgehammer_Util.one_year)
#> Sledgehammer_MaSh.mash_suggested_facts ctxt params max_suggs hyp_ts concl_t
#> fst) ctxt params)
@@ -298,10 +300,8 @@
val mash_lines = Path.explode mash_file_name |> File.read_lines
val mepo_lines = Path.explode mepo_file_name |> File.read_lines
in
- if length mash_lines = length mepo_lines then
- List.app do_fact (mash_lines ~~ mepo_lines)
- else
- warning "Skipped: MaSh file missing or out of sync with MePo file."
+ if length mash_lines = length mepo_lines then List.app do_fact (mash_lines ~~ mepo_lines)
+ else warning "Skipped: MaSh file missing or out of sync with MePo file."
end
end;
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Fri May 30 12:27:51 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Fri May 30 12:27:51 2014 +0200
@@ -162,7 +162,7 @@
val save_models_arg = "--saveModels"
val shutdown_server_arg = "--shutdownServer"
-fun wipe_out_file file = (try (File.rm o Path.explode) file; ())
+fun wipe_out_file file = ignore (try (File.rm o Path.explode) file)
fun write_file banner (xs, f) path =
(case banner of SOME s => File.write path s | NONE => ();
@@ -1579,7 +1579,7 @@
(* Generate more suggestions than requested, because some might be thrown out
later for various reasons. *)
-fun generous_max_suggestions max_facts = max_facts (*### 11 * max_facts div 10 + 20 *)
+fun generous_max_suggestions max_facts = 11 * max_facts div 10 + 20
val mepo_weight = 0.5
val mash_weight = 0.5