--- a/src/HOL/TPTP/MaSh_Export.thy Fri May 30 08:23:08 2014 +0200
+++ b/src/HOL/TPTP/MaSh_Export.thy Fri May 30 12:27:51 2014 +0200
@@ -8,6 +8,7 @@
imports Main
begin
+ML_file "~~/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML" (*###*)
ML_file "mash_export.ML"
sledgehammer_params
@@ -27,11 +28,11 @@
*}
ML {*
-val do_it = false (* switch to "true" to generate the files *)
+val do_it = true (*###*) (* 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)
+val range = (1, (* ### NONE *) SOME 100)
val step = 1
val linearize = false
val max_suggestions = 1024
@@ -46,10 +47,39 @@
()
*}
+ML {* Options.put_default @{system_option MaSh} "sml_knn" *}
+
+ML {*
+if do_it then
+ generate_mash_suggestions @{context} params (range, step) thys linearize max_suggestions
+ (prefix ^ "mash_sml_knn_suggestions")
+else
+ ()
+*}
+
+ML {* Options.put_default @{system_option MaSh} "sml_nb" *}
+
ML {*
if do_it then
- generate_accessibility @{context} thys linearize
- (prefix ^ "mash_accessibility")
+ generate_mepo_suggestions @{context} params (range, step) thys linearize max_suggestions
+ (prefix ^ "mash_sml_nb_suggestions")
+else
+ ()
+*}
+
+ML {* Options.put_default @{system_option MaSh} "py" *}
+
+ML {*
+if do_it then
+ generate_mepo_suggestions @{context} params (range, step) thys linearize max_suggestions
+ (prefix ^ "mepo_suggestions")
+else
+ ()
+*}
+
+ML {*
+if do_it then
+ generate_accessibility @{context} thys linearize (prefix ^ "mash_accessibility")
else
()
*}
@@ -63,24 +93,23 @@
ML {*
if do_it then
- generate_isar_dependencies @{context} range thys linearize
- (prefix ^ "mash_dependencies")
+ generate_isar_dependencies @{context} range thys linearize (prefix ^ "mash_dependencies")
else
()
*}
ML {*
if do_it then
- generate_isar_commands @{context} prover (range, step) thys linearize
- max_suggestions (prefix ^ "mash_commands")
+ generate_isar_commands @{context} prover (range, step) thys linearize max_suggestions
+ (prefix ^ "mash_commands")
else
()
*}
ML {*
if do_it then
- generate_mepo_suggestions @{context} params (range, step) thys linearize
- max_suggestions (prefix ^ "mepo_suggestions")
+ generate_mepo_suggestions @{context} params (range, step) thys linearize max_suggestions
+ (prefix ^ "mepo_suggestions")
else
()
*}
@@ -88,7 +117,7 @@
ML {*
if do_it then
generate_mesh_suggestions max_suggestions (prefix ^ "mash_suggestions")
- (prefix ^ "mepo_suggestions") (prefix ^ "mesh_suggestions")
+ (prefix ^ "mepo_suggestions") (prefix ^ "mesh_suggestions")
else
()
*}
@@ -96,15 +125,15 @@
ML {*
if do_it then
generate_prover_dependencies @{context} params range thys linearize
- (prefix ^ "mash_prover_dependencies")
+ (prefix ^ "mash_prover_dependencies")
else
()
*}
ML {*
if do_it then
- generate_prover_commands @{context} params (range, step) thys linearize
- max_suggestions (prefix ^ "mash_prover_commands")
+ generate_prover_commands @{context} params (range, step) thys linearize max_suggestions
+ (prefix ^ "mash_prover_commands")
else
()
*}
@@ -112,7 +141,7 @@
ML {*
if do_it then
generate_mesh_suggestions max_suggestions (prefix ^ "mash_prover_suggestions")
- (prefix ^ "mepo_suggestions") (prefix ^ "mesh_prover_suggestions")
+ (prefix ^ "mepo_suggestions") (prefix ^ "mesh_prover_suggestions")
else
()
*}
--- a/src/HOL/TPTP/mash_export.ML Fri May 30 08:23:08 2014 +0200
+++ b/src/HOL/TPTP/mash_export.ML Fri May 30 12:27:51 2014 +0200
@@ -21,6 +21,8 @@
theory list -> bool -> int -> string -> unit
val generate_mepo_suggestions : Proof.context -> params -> (int * int option) * int ->
theory list -> bool -> int -> string -> unit
+ val generate_mash_suggestions : Proof.context -> params -> (int * int option) * int ->
+ theory list -> bool -> int -> string -> unit
val generate_mesh_suggestions : int -> string -> string -> string -> unit
end;
@@ -220,8 +222,8 @@
fun generate_prover_commands ctxt (params as {provers = prover :: _, ...}) =
generate_isar_or_prover_commands ctxt prover (SOME params)
-fun generate_mepo_suggestions ctxt (params as {provers = prover :: _, ...}) (range, step) thys
- linearize max_suggs file_name =
+fun generate_mepo_or_mash_suggestions mepo_or_mash_suggested_facts ctxt
+ (params as {provers = prover :: _, ...}) (range, step) thys linearize max_suggs file_name =
let
val ho_atp = is_ho_atp ctxt prover
val path = file_name |> Path.explode
@@ -245,10 +247,11 @@
val suggs =
old_facts
|> not linearize ? filter_accessible_from th
- |> Sledgehammer_Fact.drop_duplicate_facts
- |> Sledgehammer_MePo.mepo_suggested_facts ctxt params max_suggs NONE hyp_ts concl_t
+ |> mepo_or_mash_suggested_facts ctxt params max_suggs hyp_ts concl_t
|> map (nickname_of_thm o snd)
- in encode_str name ^ ": " ^ encode_strs suggs ^ "\n" end
+ in
+ encode_str name ^ ": " ^ encode_strs suggs ^ "\n"
+ end
end
else
""
@@ -260,6 +263,22 @@
File.write_list path lines
end
+val generate_mepo_suggestions =
+ generate_mepo_or_mash_suggestions
+ (fn ctxt => fn params => fn max_suggs => fn hyp_ts => fn concl_t =>
+ Sledgehammer_Fact.drop_duplicate_facts
+ #> Sledgehammer_MePo.mepo_suggested_facts ctxt params max_suggs NONE hyp_ts concl_t)
+
+fun generate_mash_suggestions ctxt params =
+ (Sledgehammer_MaSh.mash_unlearn ctxt params;
+ 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
+ Sledgehammer_Util.one_year)
+ #> Sledgehammer_MaSh.mash_suggested_facts ctxt params max_suggs hyp_ts concl_t
+ #> fst) ctxt params)
+
fun generate_mesh_suggestions max_suggs mash_file_name mepo_file_name mesh_file_name =
let
val mesh_path = Path.explode mesh_file_name
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Fri May 30 08:23:08 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Fri May 30 12:27:51 2014 +0200
@@ -36,6 +36,9 @@
datatype mash_engine = MaSh_Py | MaSh_SML_kNN | MaSh_SML_NB
+ val is_mash_enabled : unit -> bool
+ val the_mash_engine : unit -> mash_engine
+
structure MaSh_Py :
sig
val unlearn : Proof.context -> bool -> unit
@@ -82,6 +85,8 @@
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
+ val mash_learn_facts : Proof.context -> params -> string -> bool -> int -> bool -> Time.time ->
+ raw_fact list -> string
val mash_learn : Proof.context -> params -> fact_override -> thm list -> bool -> unit
val mash_can_suggest_facts : Proof.context -> bool -> bool