# HG changeset patch
# User blanchet
# Date 1342815586 -7200
# Node ID 4147f2bc444262cf1fe52137c6384f33ad2a71de
# Parent  65679f12df4c0e086ad99132085cf9e99e304899
add versioning to MaSh state + cleanup dead code

diff -r 65679f12df4c -r 4147f2bc4442 doc-src/Sledgehammer/sledgehammer.tex
--- a/doc-src/Sledgehammer/sledgehammer.tex	Fri Jul 20 22:19:46 2012 +0200
+++ b/doc-src/Sledgehammer/sledgehammer.tex	Fri Jul 20 22:19:46 2012 +0200
@@ -1009,8 +1009,8 @@
 Specifies whether Sledgehammer should put its temporary files in
 \texttt{\$ISA\-BELLE\_\allowbreak HOME\_\allowbreak USER}, which is useful for
 debugging Sledgehammer but also unsafe if several instances of the tool are run
-simultaneously. The files are identified by the prefix \texttt{prob\_}; you may
-safely remove them after Sledgehammer has run.
+simultaneously. The files are identified by the prefixes \texttt{prob\_} and
+\texttt{mash\_}; you may safely remove them after Sledgehammer has run.
 
 \nopagebreak
 {\small See also \textit{debug} (\S\ref{output-format}).}
@@ -1032,6 +1032,7 @@
 \texttt{mash}, which can be obtained from the author at \authoremail. To install
 it, set the environment variable \texttt{MASH\_HOME} to the directory that
 contains the \texttt{mash} executable.
+Persistent data is stored in the \texttt{\$ISABELLE\_HOME\_USER/mash} directory.
 
 \item[\labelitemi] \textbf{\textit{mesh}:} A combination of MePo and MaSh.
 
diff -r 65679f12df4c -r 4147f2bc4442 src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Fri Jul 20 22:19:46 2012 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Fri Jul 20 22:19:46 2012 +0200
@@ -52,8 +52,8 @@
   val mash_learn_proof :
     Proof.context -> params -> string -> term -> ('a * thm) list -> thm list
     -> unit
-  val mash_learn_thy :
-    Proof.context -> params -> theory -> Time.time -> fact list -> string
+  val mash_learn_facts :
+    Proof.context -> params -> Time.time -> fact list -> string
   val mash_learn : Proof.context -> params -> unit
   val relevant_facts :
     Proof.context -> params -> string -> int -> fact_override -> term list
@@ -394,22 +394,21 @@
          (trace_msg ctxt (fn () =>
               "Unknown fact " ^ quote name ^ " when " ^ when); def)
 
-type mash_state =
-  {thys : bool Symtab.table,
-   fact_graph : unit Graph.T}
+type mash_state = {fact_graph : unit Graph.T}
 
-val empty_state = {thys = Symtab.empty, fact_graph = Graph.empty}
+val empty_state = {fact_graph = Graph.empty}
 
 local
 
-fun mash_load _ (state as (true, _)) = state
-  | mash_load ctxt _ =
+val version = "*** MaSh 0.0 ***"
+
+fun load _ (state as (true, _)) = state
+  | load ctxt _ =
     let val path = mash_state_path () in
       (true,
        case try File.read_lines path of
-         SOME (comp_thys :: incomp_thys :: fact_lines) =>
+         SOME (version' :: fact_lines) =>
          let
-           fun add_thy comp thy = Symtab.update (thy, comp)
            fun add_edge_to name parent =
              Graph.default_node (parent, ())
              #> Graph.add_edge (parent, name)
@@ -419,26 +418,22 @@
              | (name, parents) =>
                Graph.default_node (name, ())
                #> fold (add_edge_to name) parents
-           val thys =
-             Symtab.empty |> fold (add_thy true) (unescape_metas comp_thys)
-                          |> fold (add_thy false) (unescape_metas incomp_thys)
            val fact_graph =
              try_graph ctxt "loading state" Graph.empty (fn () =>
-                 Graph.empty |> fold add_fact_line fact_lines)
-         in {thys = thys, fact_graph = fact_graph} end
+                 Graph.empty |> version' = version
+                                ? fold add_fact_line fact_lines)
+         in {fact_graph = fact_graph} end
        | _ => empty_state)
     end
 
-fun mash_save ({thys, fact_graph, ...} : mash_state) =
+fun save {fact_graph} =
   let
     val path = mash_state_path ()
-    val thys = Symtab.dest thys
-    val line_for_thys = escape_metas o AList.find (op =) thys
     fun fact_line_for name parents =
       escape_meta name ^ ": " ^ escape_metas parents
     val append_fact = File.append path o suffix "\n" oo fact_line_for
   in
-    File.write path (line_for_thys true ^ "\n" ^ line_for_thys false ^ "\n");
+    File.write path (version ^ "\n");
     Graph.fold (fn (name, ((), (parents, _))) => fn () =>
                    append_fact name (Graph.Keys.dest parents))
         fact_graph ()
@@ -450,10 +445,10 @@
 in
 
 fun mash_map ctxt f =
-  Synchronized.change global_state (mash_load ctxt ##> (f #> tap mash_save))
+  Synchronized.change global_state (load ctxt ##> (f #> tap save))
 
 fun mash_get ctxt =
-  Synchronized.change_result global_state (mash_load ctxt #> `snd)
+  Synchronized.change_result global_state (load ctxt #> `snd)
 
 fun mash_unlearn ctxt =
   Synchronized.change global_state (fn _ =>
@@ -504,11 +499,6 @@
     val unknown = facts |> filter_out (is_fact_in_graph fact_graph)
   in (selected, unknown) end
 
-fun add_thys_for thy =
-  let fun add comp thy = Symtab.update (Context.theory_name thy, comp) in
-    add false thy #> fold (add true) (Theory.ancestors_of thy)
-  end
-
 fun update_fact_graph ctxt (name, parents, feats, deps) (upds, graph) =
   let
     fun maybe_add_from from (accum as (parents, graph)) =
@@ -542,15 +532,14 @@
               val feats = features_of ctxt prover thy (Local, General) [t]
               val deps = used_ths |> map nickname_of
             in
-              mash_map ctxt (fn {thys, fact_graph} =>
+              mash_map ctxt (fn {fact_graph} =>
                   let
                     val parents = parents_wrt_facts facts fact_graph
                     val upds = [(name, parents, feats, deps)]
                     val (upds, fact_graph) =
                       ([], fact_graph) |> fold (update_fact_graph ctxt) upds
                   in
-                    mash_ADD ctxt overlord upds;
-                    {thys = thys, fact_graph = fact_graph}
+                    mash_ADD ctxt overlord upds; {fact_graph = fact_graph}
                   end);
               (true, "")
             end)
@@ -561,14 +550,14 @@
 val pass1_learn_timeout_factor = 0.75
 
 (* The timeout is understood in a very slack fashion. *)
-fun mash_learn_thy ctxt ({provers, verbose, overlord, ...} : params) thy timeout
-                   facts =
+fun mash_learn_facts ctxt ({provers, verbose, overlord, ...} : params) timeout
+                     facts =
   let
     val timer = Timer.startRealTimer ()
     val prover = hd provers
     fun timed_out frac =
       Time.> (Timer.checkRealTimer timer, time_mult frac timeout)
-    val {fact_graph, ...} = mash_get ctxt
+    val {fact_graph} = mash_get ctxt
     val new_facts =
       facts |> filter_out (is_fact_in_graph fact_graph)
             |> sort (thm_ord o pairself snd)
@@ -596,14 +585,11 @@
         val ((_, upds), _) =
           ((parents, []), false) |> fold do_fact new_facts |>> apsnd rev
         val n = length upds
-        fun trans {thys, fact_graph} =
+        fun trans {fact_graph} =
           let
             val (upds, fact_graph) =
               ([], fact_graph) |> fold (update_fact_graph ctxt) upds
-          in
-            (mash_ADD ctxt overlord (rev upds);
-             {thys = thys |> add_thys_for thy, fact_graph = fact_graph})
-          end
+          in (mash_ADD ctxt overlord (rev upds); {fact_graph = fact_graph}) end
       in
         mash_map ctxt trans;
         if verbose then
@@ -624,7 +610,7 @@
     val css_table = Sledgehammer_Fact.clasimpset_rule_table_of ctxt
     val facts = all_facts_of thy css_table
   in
-     mash_learn_thy ctxt params thy infinite_timeout facts
+     mash_learn_facts ctxt params infinite_timeout facts
      |> (fn "" => "Learned nothing." | msg => msg)
      |> Output.urgent_message
   end
@@ -643,13 +629,12 @@
     []
   else
     let
-      val thy = Proof_Context.theory_of ctxt
       fun maybe_learn () =
         if learn andalso not (Async_Manager.has_running_threads MaShN) andalso
            Time.toSeconds timeout >= min_secs_for_learning then
           let val timeout = time_mult learn_timeout_slack timeout in
             launch_thread timeout
-                (fn () => (true, mash_learn_thy ctxt params thy timeout facts))
+                (fn () => (true, mash_learn_facts ctxt params timeout facts))
           end
         else
           ()