1.1 --- a/doc-src/Sledgehammer/sledgehammer.tex	Fri Jul 20 22:19:46 2012 +0200
     1.2 +++ b/doc-src/Sledgehammer/sledgehammer.tex	Fri Jul 20 22:19:46 2012 +0200
     1.3 @@ -1009,8 +1009,8 @@
     1.4  Specifies whether Sledgehammer should put its temporary files in
     1.5  \texttt{\$ISA\-BELLE\_\allowbreak HOME\_\allowbreak USER}, which is useful for
     1.6  debugging Sledgehammer but also unsafe if several instances of the tool are run
     1.7 -simultaneously. The files are identified by the prefix \texttt{prob\_}; you may
     1.8 -safely remove them after Sledgehammer has run.
     1.9 +simultaneously. The files are identified by the prefixes \texttt{prob\_} and
    1.10 +\texttt{mash\_}; you may safely remove them after Sledgehammer has run.
    1.11  
    1.12  \nopagebreak
    1.13  {\small See also \textit{debug} (\S\ref{output-format}).}
    1.14 @@ -1032,6 +1032,7 @@
    1.15  \texttt{mash}, which can be obtained from the author at \authoremail. To install
    1.16  it, set the environment variable \texttt{MASH\_HOME} to the directory that
    1.17  contains the \texttt{mash} executable.
    1.18 +Persistent data is stored in the \texttt{\$ISABELLE\_HOME\_USER/mash} directory.
    1.19  
    1.20  \item[\labelitemi] \textbf{\textit{mesh}:} A combination of MePo and MaSh.
    1.21  

     2.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Fri Jul 20 22:19:46 2012 +0200
     2.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Fri Jul 20 22:19:46 2012 +0200
     2.3 @@ -52,8 +52,8 @@
     2.4    val mash_learn_proof :
     2.5      Proof.context -> params -> string -> term -> ('a * thm) list -> thm list
     2.6      -> unit
     2.7 -  val mash_learn_thy :
     2.8 -    Proof.context -> params -> theory -> Time.time -> fact list -> string
     2.9 +  val mash_learn_facts :
    2.10 +    Proof.context -> params -> Time.time -> fact list -> string
    2.11    val mash_learn : Proof.context -> params -> unit
    2.12    val relevant_facts :
    2.13      Proof.context -> params -> string -> int -> fact_override -> term list
    2.14 @@ -394,22 +394,21 @@
    2.15           (trace_msg ctxt (fn () =>
    2.16                "Unknown fact " ^ quote name ^ " when " ^ when); def)
    2.17  
    2.18 -type mash_state =
    2.19 -  {thys : bool Symtab.table,
    2.20 -   fact_graph : unit Graph.T}
    2.21 +type mash_state = {fact_graph : unit Graph.T}
    2.22  
    2.23 -val empty_state = {thys = Symtab.empty, fact_graph = Graph.empty}
    2.24 +val empty_state = {fact_graph = Graph.empty}
    2.25  
    2.26  local
    2.27  
    2.28 -fun mash_load _ (state as (true, _)) = state
    2.29 -  | mash_load ctxt _ =
    2.30 +val version = "*** MaSh 0.0 ***"
    2.31 +
    2.32 +fun load _ (state as (true, _)) = state
    2.33 +  | load ctxt _ =
    2.34      let val path = mash_state_path () in
    2.35        (true,
    2.36         case try File.read_lines path of
    2.37 -         SOME (comp_thys :: incomp_thys :: fact_lines) =>
    2.38 +         SOME (version' :: fact_lines) =>
    2.39           let
    2.40 -           fun add_thy comp thy = Symtab.update (thy, comp)
    2.41             fun add_edge_to name parent =
    2.42               Graph.default_node (parent, ())
    2.43               #> Graph.add_edge (parent, name)
    2.44 @@ -419,26 +418,22 @@
    2.45               | (name, parents) =>
    2.46                 Graph.default_node (name, ())
    2.47                 #> fold (add_edge_to name) parents
    2.48 -           val thys =
    2.49 -             Symtab.empty |> fold (add_thy true) (unescape_metas comp_thys)
    2.50 -                          |> fold (add_thy false) (unescape_metas incomp_thys)
    2.51             val fact_graph =
    2.52               try_graph ctxt "loading state" Graph.empty (fn () =>
    2.53 -                 Graph.empty |> fold add_fact_line fact_lines)
    2.54 -         in {thys = thys, fact_graph = fact_graph} end
    2.55 +                 Graph.empty |> version' = version
    2.56 +                                ? fold add_fact_line fact_lines)
    2.57 +         in {fact_graph = fact_graph} end
    2.58         | _ => empty_state)
    2.59      end
    2.60  
    2.61 -fun mash_save ({thys, fact_graph, ...} : mash_state) =
    2.62 +fun save {fact_graph} =
    2.63    let
    2.64      val path = mash_state_path ()
    2.65 -    val thys = Symtab.dest thys
    2.66 -    val line_for_thys = escape_metas o AList.find (op =) thys
    2.67      fun fact_line_for name parents =
    2.68        escape_meta name ^ ": " ^ escape_metas parents
    2.69      val append_fact = File.append path o suffix "\n" oo fact_line_for
    2.70    in
    2.71 -    File.write path (line_for_thys true ^ "\n" ^ line_for_thys false ^ "\n");
    2.72 +    File.write path (version ^ "\n");
    2.73      Graph.fold (fn (name, ((), (parents, _))) => fn () =>
    2.74                     append_fact name (Graph.Keys.dest parents))
    2.75          fact_graph ()
    2.76 @@ -450,10 +445,10 @@
    2.77  in
    2.78  
    2.79  fun mash_map ctxt f =
    2.80 -  Synchronized.change global_state (mash_load ctxt ##> (f #> tap mash_save))
    2.81 +  Synchronized.change global_state (load ctxt ##> (f #> tap save))
    2.82  
    2.83  fun mash_get ctxt =
    2.84 -  Synchronized.change_result global_state (mash_load ctxt #> `snd)
    2.85 +  Synchronized.change_result global_state (load ctxt #> `snd)
    2.86  
    2.87  fun mash_unlearn ctxt =
    2.88    Synchronized.change global_state (fn _ =>
    2.89 @@ -504,11 +499,6 @@
    2.90      val unknown = facts |> filter_out (is_fact_in_graph fact_graph)
    2.91    in (selected, unknown) end
    2.92  
    2.93 -fun add_thys_for thy =
    2.94 -  let fun add comp thy = Symtab.update (Context.theory_name thy, comp) in
    2.95 -    add false thy #> fold (add true) (Theory.ancestors_of thy)
    2.96 -  end
    2.97 -
    2.98  fun update_fact_graph ctxt (name, parents, feats, deps) (upds, graph) =
    2.99    let
   2.100      fun maybe_add_from from (accum as (parents, graph)) =
   2.101 @@ -542,15 +532,14 @@
   2.102                val feats = features_of ctxt prover thy (Local, General) [t]
   2.103                val deps = used_ths |> map nickname_of
   2.104              in
   2.105 -              mash_map ctxt (fn {thys, fact_graph} =>
   2.106 +              mash_map ctxt (fn {fact_graph} =>
   2.107                    let
   2.108                      val parents = parents_wrt_facts facts fact_graph
   2.109                      val upds = [(name, parents, feats, deps)]
   2.110                      val (upds, fact_graph) =
   2.111                        ([], fact_graph) |> fold (update_fact_graph ctxt) upds
   2.112                    in
   2.113 -                    mash_ADD ctxt overlord upds;
   2.114 -                    {thys = thys, fact_graph = fact_graph}
   2.115 +                    mash_ADD ctxt overlord upds; {fact_graph = fact_graph}
   2.116                    end);
   2.117                (true, "")
   2.118              end)
   2.119 @@ -561,14 +550,14 @@
   2.120  val pass1_learn_timeout_factor = 0.75
   2.121  
   2.122  (* The timeout is understood in a very slack fashion. *)
   2.123 -fun mash_learn_thy ctxt ({provers, verbose, overlord, ...} : params) thy timeout
   2.124 -                   facts =
   2.125 +fun mash_learn_facts ctxt ({provers, verbose, overlord, ...} : params) timeout
   2.126 +                     facts =
   2.127    let
   2.128      val timer = Timer.startRealTimer ()
   2.129      val prover = hd provers
   2.130      fun timed_out frac =
   2.131        Time.> (Timer.checkRealTimer timer, time_mult frac timeout)
   2.132 -    val {fact_graph, ...} = mash_get ctxt
   2.133 +    val {fact_graph} = mash_get ctxt
   2.134      val new_facts =
   2.135        facts |> filter_out (is_fact_in_graph fact_graph)
   2.136              |> sort (thm_ord o pairself snd)
   2.137 @@ -596,14 +585,11 @@
   2.138          val ((_, upds), _) =
   2.139            ((parents, []), false) |> fold do_fact new_facts |>> apsnd rev
   2.140          val n = length upds
   2.141 -        fun trans {thys, fact_graph} =
   2.142 +        fun trans {fact_graph} =
   2.143            let
   2.144              val (upds, fact_graph) =
   2.145                ([], fact_graph) |> fold (update_fact_graph ctxt) upds
   2.146 -          in
   2.147 -            (mash_ADD ctxt overlord (rev upds);
   2.148 -             {thys = thys |> add_thys_for thy, fact_graph = fact_graph})
   2.149 -          end
   2.150 +          in (mash_ADD ctxt overlord (rev upds); {fact_graph = fact_graph}) end
   2.151        in
   2.152          mash_map ctxt trans;
   2.153          if verbose then
   2.154 @@ -624,7 +610,7 @@
   2.155      val css_table = Sledgehammer_Fact.clasimpset_rule_table_of ctxt
   2.156      val facts = all_facts_of thy css_table
   2.157    in
   2.158 -     mash_learn_thy ctxt params thy infinite_timeout facts
   2.159 +     mash_learn_facts ctxt params infinite_timeout facts
   2.160       |> (fn "" => "Learned nothing." | msg => msg)
   2.161       |> Output.urgent_message
   2.162    end
   2.163 @@ -643,13 +629,12 @@
   2.164      []
   2.165    else
   2.166      let
   2.167 -      val thy = Proof_Context.theory_of ctxt
   2.168        fun maybe_learn () =
   2.169          if learn andalso not (Async_Manager.has_running_threads MaShN) andalso
   2.170             Time.toSeconds timeout >= min_secs_for_learning then
   2.171            let val timeout = time_mult learn_timeout_slack timeout in
   2.172              launch_thread timeout
   2.173 -                (fn () => (true, mash_learn_thy ctxt params thy timeout facts))
   2.174 +                (fn () => (true, mash_learn_facts ctxt params timeout facts))
   2.175            end
   2.176          else
   2.177            ()