# HG changeset patch
# User blanchet
# Date 1401445671 -7200
# Node ID 5f69b8c3af5a3b7fcef9a6f56a16177148397fb0
# Parent  426ab5fabcae0f6fd04bb325b7c258957feff85c
more work on exporter

diff -r 426ab5fabcae -r 5f69b8c3af5a src/HOL/TPTP/MaSh_Export.thy
--- 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
   ()
 *}
diff -r 426ab5fabcae -r 5f69b8c3af5a src/HOL/TPTP/mash_export.ML
--- 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;
diff -r 426ab5fabcae -r 5f69b8c3af5a src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
--- 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