src/HOL/Tools/Sledgehammer/sledgehammer_filter_mash.ML

     Proof.context -> string -> theory -> status -> term list -> string list
   val isabelle_dependencies_of : unit Symtab.table -> thm -> string list
   val goal_of_thm : theory -> thm -> thm
   val run_prover_for_mash :
     Proof.context -> params -> string -> fact list -> thm -> prover_result
-  val mash_RESET : Proof.context -> unit
+  val mash_CLEAR : Proof.context -> unit
   val mash_INIT :
     Proof.context -> bool
     -> (string * string list * string list * string list) list -> unit
   val mash_ADD :
     Proof.context -> bool
     -> (string * string list * string list * string list) list -> unit
   val mash_QUERY :
     Proof.context -> bool -> int -> string list * string list -> string list
-  val mash_reset : Proof.context -> unit
+  val mash_unlearn : Proof.context -> unit
   val mash_could_suggest_facts : unit -> bool
   val mash_can_suggest_facts : Proof.context -> bool
   val mash_suggest_facts :
     Proof.context -> params -> string -> int -> term list -> term
     -> ('a * thm) list -> ('a * thm) list * ('a * thm) list

 (* TODO: Generate type classes for types? *)
 fun features_of ctxt prover thy status ts =
   thy_feature_name_of (Context.theory_name thy) ::
   interesting_terms_types_and_classes ctxt prover term_max_depth type_max_depth
                                       ts
-  |> exists (not o is_lambda_free) ts ? cons "lambdas"
-  |> exists (exists_Const is_exists) ts ? cons "skolems"
+  |> forall is_lambda_free ts ? cons "no_lams"
+  |> forall (not o exists_Const is_exists) ts ? cons "no_skos"
   |> (case status of
         General => I
       | Induction => cons "induction"
       | Intro => cons "intro"
       | Inductive => cons "inductive"

 
 fun mash_info overlord =
   if overlord then (getenv "ISABELLE_HOME_USER", "")
   else (getenv "ISABELLE_TMP", serial_string ())
 
-fun run_mash ctxt (temp_dir, serial) core =
+fun run_mash ctxt overlord (temp_dir, serial) core =
   let
     val log_file = temp_dir ^ "/mash_log" ^ serial
     val err_file = temp_dir ^ "/mash_err" ^ serial
     val command =
       mash_home () ^ "/mash.py --quiet --outputDir " ^ mash_state_dir () ^
       " --log " ^ log_file ^ " " ^ core ^ " 2>&1 > " ^ err_file
   in
     trace_msg ctxt (fn () => "Running " ^ command);
     write_file ([], K "") log_file;
     write_file ([], K "") err_file;
-    Isabelle_System.bash command; ()
-  end
-
+    Isabelle_System.bash command;
+    if overlord then ()
+    else (map (File.rm o Path.explode) [log_file, err_file]; ());
+    trace_msg ctxt (K "Done")
+  end
+
+(* TODO: Eliminate code once "mash.py" handles sequences of ADD commands as fast
+   as a single INIT. *)
 fun run_mash_init ctxt overlord write_access write_feats write_deps =
   let
     val info as (temp_dir, serial) = mash_info overlord
     val in_dir = temp_dir ^ "/mash_init" ^ serial
-                 |> tap (Isabelle_System.mkdir o Path.explode)
+    val in_dir_path = in_dir |> Path.explode |> tap Isabelle_System.mkdir
   in
     write_file write_access (in_dir ^ "/mash_accessibility");
     write_file write_feats (in_dir ^ "/mash_features");
     write_file write_deps (in_dir ^ "/mash_dependencies");
-    run_mash ctxt info ("--init --inputDir " ^ in_dir)
+    run_mash ctxt overlord info ("--init --inputDir " ^ in_dir);
+    (* FIXME: temporary hack *)
+    if overlord then ()
+    else (Isabelle_System.bash ("rm -r -f " ^ File.shell_path in_dir_path); ())
   end
 
 fun run_mash_commands ctxt overlord save max_suggs write_cmds read_suggs =
   let
     val info as (temp_dir, serial) = mash_info overlord
     val sugg_file = temp_dir ^ "/mash_suggs" ^ serial
     val cmd_file = temp_dir ^ "/mash_commands" ^ serial
   in
     write_file ([], K "") sugg_file;
     write_file write_cmds cmd_file;
-    run_mash ctxt info
+    run_mash ctxt overlord info
              ("--inputFile " ^ cmd_file ^ " --predictions " ^ sugg_file ^
               " --numberOfPredictions " ^ string_of_int max_suggs ^
               (if save then " --saveModel" else ""));
     read_suggs (fn () => File.read_lines (Path.explode sugg_file))
+    |> tap (fn _ =>
+               if overlord then ()
+               else (map (File.rm o Path.explode) [sugg_file, cmd_file]; ()))
   end
 
 fun str_of_update (name, parents, feats, deps) =
   "! " ^ escape_meta name ^ ": " ^ escape_metas parents ^ "; " ^
   escape_metas feats ^ "; " ^ escape_metas deps ^ "\n"

   "? " ^ escape_metas parents ^ "; " ^ escape_metas feats
 
 fun init_str_of_update get (upd as (name, _, _, _)) =
   escape_meta name ^ ": " ^ escape_metas (get upd) ^ "\n"
 
-fun mash_RESET ctxt =
+fun mash_CLEAR ctxt =
   let val path = mash_state_dir () |> Path.explode in
-    trace_msg ctxt (K "MaSh RESET");
+    trace_msg ctxt (K "MaSh CLEAR");
     File.fold_dir (fn file => fn () =>
                       File.rm (Path.append path (Path.basic file)))
                   path ()
   end
 
-fun mash_INIT ctxt _ [] = mash_RESET ctxt
+fun mash_INIT ctxt _ [] = mash_CLEAR ctxt
   | mash_INIT ctxt overlord upds =
     (trace_msg ctxt (fn () => "MaSh INIT " ^
          elide_string 1000 (space_implode " " (map #1 upds)));
      run_mash_init ctxt overlord (upds, init_str_of_update #2)
                    (upds, init_str_of_update #3) (upds, init_str_of_update #4))

   Synchronized.change global_state (mash_load ctxt ##> (f #> tap mash_save))
 
 fun mash_get ctxt =
   Synchronized.change_result global_state (mash_load ctxt #> `snd)
 
-fun mash_reset ctxt =
+fun mash_unlearn ctxt =
   Synchronized.change global_state (fn _ =>
-      (mash_RESET ctxt; File.write (mash_state_path ()) "";
+      (mash_CLEAR ctxt; File.write (mash_state_path ()) "";
        (true, empty_state)))
 
 end
 
 fun mash_could_suggest_facts () = mash_home () <> ""
 fun mash_can_suggest_facts ctxt =
   not (Graph.is_empty (#fact_graph (mash_get ctxt)))
 
-fun parents_wrt_facts ctxt facts fact_graph =
+fun parents_wrt_facts facts fact_graph =
   let
     val facts = [] |> fold (cons o Thm.get_name_hint o snd) facts
     val tab = Symtab.empty |> fold (fn name => Symtab.update (name, ())) facts
-    val maxs = Graph.maximals fact_graph
-  in
-    if forall (Symtab.defined tab) maxs then
-      maxs
-    else
-      let
-        val graph_facts = Symtab.make (map (rpair ()) (Graph.keys fact_graph))
-        val ancestors =
-          try_graph ctxt "when computing ancestor facts" [] (fn () =>
-              facts |> filter (Symtab.defined graph_facts)
-                    |> Graph.all_preds fact_graph)
-        val ancestors =
-          Symtab.empty |> fold (fn name => Symtab.update (name, ())) ancestors
-      in
-        try_graph ctxt "when computing parent facts" [] (fn () =>
-            fact_graph |> Graph.restrict (Symtab.defined ancestors)
-                       |> Graph.maximals)
-      end
-  end
+    fun insert_not_parent parents name =
+      not (member (op =) parents name) ? insert (op =) name
+    fun parents_of parents [] = parents
+      | parents_of parents (name :: names) =
+        if Symtab.defined tab name then
+          parents_of (name :: parents) names
+        else
+          parents_of parents (Graph.Keys.fold (insert_not_parent parents)
+                                  (Graph.imm_preds fact_graph name) names)
+  in parents_of [] (Graph.maximals fact_graph) end
 
 (* Generate more suggestions than requested, because some might be thrown out
    later for various reasons and "meshing" gives better results with some
    slack. *)
 fun max_suggs_of max_facts = max_facts + Int.min (200, max_facts)

   can (Graph.get_node fact_graph) (Thm.get_name_hint th)
 
 fun mash_suggest_facts ctxt ({overlord, ...} : params) prover max_facts hyp_ts
                        concl_t facts =
   let
-val timer = Timer.startRealTimer ()
     val thy = Proof_Context.theory_of ctxt
-val _ = tracing ("A1: " ^ PolyML.makestring (Timer.checkRealTimer timer)) (*###*)
     val fact_graph = #fact_graph (mash_get ctxt)
-val _ = tracing ("A2: " ^ PolyML.makestring (Timer.checkRealTimer timer)) (*###*)
-    val parents = parents_wrt_facts ctxt facts fact_graph
-val _ = tracing ("A3: " ^ PolyML.makestring (Timer.checkRealTimer timer)) (*###*)
+    val parents = parents_wrt_facts facts fact_graph
     val feats = features_of ctxt prover thy General (concl_t :: hyp_ts)
-val _ = tracing ("A4: " ^ PolyML.makestring (Timer.checkRealTimer timer)) (*###*)
     val suggs =
       if Graph.is_empty fact_graph then []
       else mash_QUERY ctxt overlord (max_suggs_of max_facts) (parents, feats)
-val _ = tracing ("A5: " ^ PolyML.makestring (Timer.checkRealTimer timer)) (*###*)
     val selected = facts |> suggested_facts suggs
-val _ = tracing ("A6: " ^ PolyML.makestring (Timer.checkRealTimer timer)) (*###*)
     val unknown = facts |> filter_out (is_fact_in_graph fact_graph)
-val _ = tracing ("END: " ^ PolyML.makestring (Timer.checkRealTimer timer)) (*###*)
   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)

     val (parents, graph) = ([], graph) |> fold maybe_add_from parents
     val (deps, graph) = ([], graph) |> fold maybe_add_from deps
   in ((name, parents, feats, deps) :: upds, graph) end
 
 val pass1_learn_timeout_factor = 0.5
+
+(* Too many dependencies is a sign that a decision procedure is at work. There
+   isn't much too learn from such proofs. *)
+val max_dependencies = 10
 
 (* The timeout is understood in a very slack fashion. *)
 fun mash_learn_thy ctxt ({provers, verbose, overlord, ...} : params) thy timeout
                    facts =
   let

         val ths = facts |> map snd
         val all_names =
           ths |> filter_out is_likely_tautology_or_too_meta
               |> map (rpair () o Thm.get_name_hint)
               |> Symtab.make
+        fun trim_deps deps = if length deps > max_dependencies then [] else deps
         fun do_fact _ (accum as (_, true)) = accum
           | do_fact ((_, (_, status)), th) ((parents, upds), false) =
             let
               val name = Thm.get_name_hint th
-              val feats = features_of ctxt prover thy status [prop_of th]
-              val deps = isabelle_dependencies_of all_names th
+              val feats =
+                features_of ctxt prover (theory_of_thm th) status [prop_of th]
+              val deps = isabelle_dependencies_of all_names th |> trim_deps
               val upd = (name, parents, feats, deps)
             in (([name], upd :: upds), timed_out pass1_learn_timeout_factor) end
-        val parents = parents_wrt_facts ctxt facts fact_graph
+        val parents = parents_wrt_facts facts fact_graph
         val ((_, upds), _) =
           ((parents, []), false) |> fold do_fact new_facts |>> apsnd rev
         val n = length upds
         fun trans {thys, fact_graph} =
           let

     val feats = features_of ctxt prover thy General [t]
     val deps = used_ths |> map Thm.get_name_hint
   in
     mash_map ctxt (fn {thys, fact_graph} =>
         let
-          val parents = parents_wrt_facts ctxt facts fact_graph
+          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;