# HG changeset patch
# User blanchet
# Date 1401445671 -7200
# Node ID f8112c4b9cb86b95987dfea0a2b15fa715f23fe6
# Parent  f6d1f88021be9a1d8dba23e8191448c6e6807604
extend exporter with new versions of MaSh

diff -r f6d1f88021be -r f8112c4b9cb8 src/HOL/TPTP/MaSh_Export.thy
--- 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
   ()
 *}
diff -r f6d1f88021be -r f8112c4b9cb8 src/HOL/TPTP/mash_export.ML
--- 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
diff -r f6d1f88021be -r f8112c4b9cb8 src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
--- 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