started implementing MaSh client-side I/O

--- a/src/HOL/TPTP/ATP_Theory_Export.thy	Wed Jul 18 08:44:03 2012 +0200
+++ b/src/HOL/TPTP/ATP_Theory_Export.thy	Wed Jul 18 08:44:03 2012 +0200
@@ -5,7 +5,7 @@
 header {* ATP Theory Exporter *}
 
 theory ATP_Theory_Export
-imports Complex_Main
+imports (* ### Complex_Main *) "~~/src/HOL/Sledgehammer2d"
 uses "atp_theory_export.ML"
 begin
 
@@ -15,13 +15,22 @@
 *}
 
 ML {*
-val do_it = false; (* switch to "true" to generate the files *)
-val thy = @{theory};
+val do_it = true; (* switch to "true" to generate the files *)
+val thy = @{theory List};
 val ctxt = @{context}
 *}
 
 ML {*
 if do_it then
+  "/tmp/axs_tc_native.dfg"
+  |> generate_atp_inference_file_for_theory ctxt thy (DFG Polymorphic)
+         "tc_native"
+else
+  ()
+*}
+
+ML {*
+if do_it then
   "/tmp/infs_poly_guards_query_query.tptp"
   |> generate_atp_inference_file_for_theory ctxt thy FOF
          "poly_guards_query_query"
@@ -38,13 +47,4 @@
   ()
 *}
 
-ML {*
-if do_it then
-  "/tmp/axs_tc_native.dfg"
-  |> generate_atp_inference_file_for_theory ctxt thy (DFG Polymorphic)
-         "tc_native"
-else
-  ()
-*}
-
 end

--- a/src/HOL/TPTP/MaSh_Eval.thy	Wed Jul 18 08:44:03 2012 +0200
+++ b/src/HOL/TPTP/MaSh_Eval.thy	Wed Jul 18 08:44:03 2012 +0200
@@ -5,7 +5,7 @@
 header {* MaSh Evaluation Driver *}
 
 theory MaSh_Eval
-imports Complex_Main
+imports (* ### Complex_Main *) "~~/src/HOL/Sledgehammer2d"
 uses "mash_eval.ML"
 begin
 
@@ -20,14 +20,14 @@
 *}
 
 ML {*
-val do_it = false (* switch to "true" to generate the files *);
-val thy = @{theory List};
+val do_it = true (* switch to "true" to generate the files *);
+val thy = @{theory Nat};
 val params = Sledgehammer_Isar.default_params @{context} []
 *}
 
 ML {*
 if do_it then
-  evaluate_mash_suggestions @{context} params thy "/tmp/mash_suggestions_list"
+  evaluate_mash_suggestions @{context} params thy "/Users/blanchet/tum/mash/mash/results/natNB200ATP-15.pred"
 else
   ()
 *}

--- a/src/HOL/TPTP/MaSh_Export.thy	Wed Jul 18 08:44:03 2012 +0200
+++ b/src/HOL/TPTP/MaSh_Export.thy	Wed Jul 18 08:44:03 2012 +0200
@@ -5,7 +5,7 @@
 header {* MaSh Exporter *}
 
 theory MaSh_Export
-imports Complex_Main
+imports (* ### Complex_Main *) "~~/src/HOL/Sledgehammer2d"
 uses "mash_export.ML"
 begin
 

--- a/src/HOL/TPTP/atp_theory_export.ML	Wed Jul 18 08:44:03 2012 +0200
+++ b/src/HOL/TPTP/atp_theory_export.ML	Wed Jul 18 08:44:03 2012 +0200
@@ -50,7 +50,11 @@
   let
     val thy = Proof_Context.theory_of ctxt
     val prob_file = File.tmp_path (Path.explode "prob")
-    val atp = case format of DFG _ => spassN | _ => eN
+    val atp =
+      case format of
+        DFG Polymorphic => spass_polyN
+      | DFG Monomorphic => spassN
+      | _ => eN
     val {exec, arguments, proof_delims, known_failures, ...} =
       get_atp thy atp ()
     val ord = effective_term_order ctxt atp

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter_mash.ML	Wed Jul 18 08:44:03 2012 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter_mash.ML	Wed Jul 18 08:44:03 2012 +0200
@@ -55,21 +55,27 @@
 open Sledgehammer_Filter_Iter
 open Sledgehammer_Provers
 
+val mash_dir = "mash"
+val model_file = "model"
+val state_file = "state"
+
+fun mash_path file = getenv "ISABELLE_HOME_USER" ^ "/" ^ mash_dir ^ "/" ^ file
+
 
 (*** Low-level communication with MaSh ***)
 
 fun mash_RESET () =
-  tracing "MaSh RESET"
+  warning "MaSh RESET"
 
-fun mash_ADD fact (access, feats, deps) =
-  tracing ("MaSh ADD " ^ fact ^ ": " ^ space_implode " " access ^ "; " ^
+fun mash_ADD fact access feats deps =
+  warning ("MaSh ADD " ^ fact ^ ": " ^ space_implode " " access ^ "; " ^
            space_implode " " feats ^ "; " ^ space_implode " " deps)
 
 fun mash_DEL fact =
-  tracing ("MaSh DEL " ^ fact)
+  warning ("MaSh DEL " ^ fact)
 
-fun mash_SUGGEST fact (access, feats) =
-  tracing ("MaSh SUGGEST " ^ fact ^ ": " ^ space_implode " " access ^ "; " ^
+fun mash_SUGGEST access feats =
+  warning ("MaSh SUGGEST " ^ space_implode " " access ^ "; " ^
            space_implode " " feats)
 
 
@@ -371,18 +377,82 @@
 
 (*** High-level communication with MaSh ***)
 
-fun mash_reset () = ()
+type mash_state =
+  {completed_thys : unit Symtab.table,
+   thy_facts : string list Symtab.table}
+
+val mash_zero =
+  {completed_thys = Symtab.empty,
+   thy_facts = Symtab.empty}
+
+local
+
+fun mash_load (state as (true, _)) = state
+  | mash_load _ =
+    (true,
+     case mash_path state_file |> Path.explode |> File.read_lines of
+       [] => mash_zero
+     | comp_line :: facts_lines =>
+       let
+         fun comp_thys_of_line comp_line =
+           Symtab.make (comp_line |> space_explode " " |> map (rpair ()))
+         fun add_facts_line line =
+           case space_explode " " line of
+             thy :: facts => Symtab.update_new (thy, facts)
+           | _ => I (* shouldn't happen *)
+       in
+         {completed_thys = comp_thys_of_line comp_line,
+          thy_facts = fold add_facts_line facts_lines Symtab.empty}
+       end)
 
-fun mash_can_suggest_facts () = true
+fun mash_save ({completed_thys, thy_facts} : mash_state) =
+  let
+    val path = mash_path state_file |> Path.explode
+    val comp_line = (completed_thys |> Symtab.keys |> space_implode " ") ^ "\n"
+    fun fact_line_for (thy, facts) = space_implode " " (thy :: facts) ^ "\n"
+  in
+    File.write path comp_line;
+    Symtab.fold (fn thy_fact => fn () =>
+                    File.append path (fact_line_for thy_fact)) thy_facts
+  end
+
+val state =
+  Synchronized.var "Sledgehammer_Filter_MaSh.state" (false, mash_zero)
+
+in
+
+fun mash_change f =
+  Synchronized.change state (apsnd (tap mash_save o f) o mash_load)
+
+fun mash_value () = Synchronized.change_result state (`snd o mash_load)
+
+end
+
+fun mash_reset () = mash_change (fn _ => (mash_RESET (); mash_zero))
+
+fun mash_can_suggest_facts () =
+  not (Symtab.is_empty (#thy_facts (mash_value ())))
 
 fun mash_suggest_facts ctxt params prover max_facts hyp_ts concl_t facts =
-  (facts, [])
+  let
+    val access = []
+    val feats = []
+    val suggs = mash_SUGGEST access feats
+  in (facts, []) end
 
-fun mash_can_learn_thy thy = true
+fun mash_can_learn_thy thy =
+  not (Symtab.defined (#completed_thys (mash_value ()))
+                      (Context.theory_name thy))
 
 fun mash_learn_thy thy timeout = ()
 
 fun mash_learn_proof thy t ths = ()
+(*###
+  let
+  in
+    mash_ADD
+  end
+*)
 
 fun relevant_facts ctxt params prover max_facts
         ({add, only, ...} : fact_override) hyp_ts concl_t facts =

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Wed Jul 18 08:44:03 2012 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Wed Jul 18 08:44:03 2012 +0200
@@ -26,6 +26,7 @@
 open Sledgehammer_Fact
 open Sledgehammer_Provers
 open Sledgehammer_Minimize
+open Sledgehammer_Filter_MaSh
 open Sledgehammer_Run
 
 val runN = "run"
@@ -35,6 +36,14 @@
 val running_proversN = "running_provers"
 val kill_proversN = "kill_provers"
 val refresh_tptpN = "refresh_tptp"
+val mash_resetN = "mash_reset"
+val mash_learnN = "mash_learn"
+
+(* experimental *)
+val mash_RESET_N = "mash_RESET"
+val mash_ADD_N = "mash_ADD"
+val mash_DEL_N = "mash_DEL"
+val mash_SUGGEST_N = "mash_SUGGEST"
 
 val auto = Unsynchronized.ref false
 
@@ -374,6 +383,18 @@
       kill_provers ()
     else if subcommand = refresh_tptpN then
       refresh_systems_on_tptp ()
+    else if subcommand = mash_resetN then
+      mash_reset ()
+    else if subcommand = mash_learnN then
+      () (* TODO: implement *)
+    else if subcommand = mash_RESET_N then
+      () (* TODO: implement *)
+    else if subcommand = mash_ADD_N then
+      () (* TODO: implement *)
+    else if subcommand = mash_DEL_N then
+      () (* TODO: implement *)
+    else if subcommand = mash_SUGGEST_N then
+      () (* TODO: implement *)
     else
       error ("Unknown subcommand: " ^ quote subcommand ^ ".")
   end