src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML

   val encode_features : (string * real) list -> string
   val extract_suggestions : string -> string * string list
 
   structure MaSh:
   sig
-    val unlearn : Proof.context -> unit
+    val unlearn : Proof.context -> bool -> unit
     val learn :
       Proof.context -> bool
       -> (string * string list * string list * string list) list -> unit
     val relearn :
       Proof.context -> bool -> (string * string list) list -> unit

       -> (string * string list * string list * string list) list
          * string list * string list * (string * real) list
       -> string list
   end
 
-  val mash_unlearn : Proof.context -> unit
+  val mash_unlearn : Proof.context -> params -> unit
   val nickname_of_thm : thm -> string
   val find_suggested_facts :
     Proof.context -> ('b * thm) list -> string list -> ('b * thm) list
   val mesh_facts :
     ('a * 'a -> bool) -> int -> (real * (('a * real) list * 'a list)) list

     Proof.context -> params -> string -> term -> ('a * thm) list -> thm list
     -> unit
   val mash_learn :
     Proof.context -> params -> fact_override -> thm list -> bool -> unit
   val is_mash_enabled : unit -> bool
-  val mash_can_suggest_facts : Proof.context -> bool
+  val mash_can_suggest_facts : Proof.context -> bool -> bool
   val generous_max_facts : int -> int
   val mepo_weight : real
   val mash_weight : real
   val relevant_facts :
     Proof.context -> params -> string -> int -> fact_override -> term list
     -> term -> raw_fact list -> (string * fact list) list
-  val kill_learners : Proof.context -> unit
+  val kill_learners : Proof.context -> params -> unit
   val running_learners : unit -> unit
 end;
 
 structure Sledgehammer_MaSh : SLEDGEHAMMER_MASH =
 struct

   | _ => ("", [])
 
 structure MaSh =
 struct
 
-fun shutdown ctxt =
-  run_mash_tool ctxt false [shutdown_server_arg] ([], K "") (K ())
-
-fun unlearn ctxt =
+fun shutdown ctxt overlord =
+  run_mash_tool ctxt overlord [shutdown_server_arg] ([], K "") (K ())
+
+fun unlearn ctxt overlord =
   let val path = mash_model_dir () in
     trace_msg ctxt (K "MaSh unlearn");
-    shutdown ctxt;
+    shutdown ctxt overlord;
     try (File.fold_dir (fn file => fn _ =>
                            try File.rm (Path.append path (Path.basic file)))
                        path) NONE;
     ()
   end

        SOME (unencode_str name, unencode_strs parents,
              try proof_kind_of_str kind |> the_default Isar_Proof)
      | _ => NONE)
   | _ => NONE
 
-fun load _ (state as (true, _)) = state
-  | load ctxt _ =
+fun load _ _ (state as (true, _)) = state
+  | load ctxt overlord _ =
     let val path = mash_state_file () in
       (true,
        case try File.read_lines path of
          SOME (version' :: node_lines) =>
          let

                (try_graph ctxt "loading state" Graph.empty (fn () =>
                     fold add_node node_lines Graph.empty),
                 length node_lines)
              | LESS =>
                (* can't parse old file *)
-               (MaSh.unlearn ctxt; (Graph.empty, 0))
+               (MaSh.unlearn ctxt overlord; (Graph.empty, 0))
              | GREATER => raise FILE_VERSION_TOO_NEW ()
          in
            trace_msg ctxt (fn () =>
                "Loaded fact graph (" ^ graph_info access_G ^ ")");
            {access_G = access_G, num_known_facts = num_known_facts,

 val global_state =
   Synchronized.var "Sledgehammer_MaSh.global_state" (false, empty_state)
 
 in
 
-fun map_state ctxt f =
-  Synchronized.change global_state (load ctxt ##> (f #> save ctxt))
+fun map_state ctxt overlord f =
+  Synchronized.change global_state (load ctxt overlord ##> (f #> save ctxt))
   handle FILE_VERSION_TOO_NEW () => ()
 
-fun peek_state ctxt f =
+fun peek_state ctxt overlord f =
   Synchronized.change_result global_state
-      (perhaps (try (load ctxt)) #> `snd #>> f)
-
-fun clear_state ctxt =
+      (perhaps (try (load ctxt overlord)) #> `snd #>> f)
+
+fun clear_state ctxt overlord =
   Synchronized.change global_state (fn _ =>
-      (MaSh.unlearn ctxt; (* also removes the state file *)
+      (MaSh.unlearn ctxt overlord; (* also removes the state file *)
        (false, empty_state)))
 
 end
 
-val mash_unlearn = clear_state
+fun mash_unlearn ctxt ({overlord, ...} : params) = clear_state ctxt overlord
 
 
 (*** Isabelle helpers ***)
 
 val local_prefix = "local" ^ Long_Name.separator

   | crude_str_of_typ (TVar (_, S)) = crude_str_of_sort S
 
 fun maybe_singleton_str _ "" = []
   | maybe_singleton_str pref s = [pref ^ s]
 
-val max_pat_breadth = 10
+val max_pat_breadth = 10 (* FUDGE *)
 
 fun term_features_of ctxt prover thy_name num_facts const_tab term_max_depth
                      type_max_depth ts =
   let
     val thy = Proof_Context.theory_of ctxt

       16.0 +
       (if num_facts = 0 then
          0.0
        else
          let val count = Symtab.lookup const_tab s |> the_default 1 in
-           (Real.fromInt num_facts / Real.fromInt count) (* FUDGE *)
+           Real.fromInt num_facts / Real.fromInt count (* FUDGE *)
          end)
     fun pattify_term _ _ 0 _ = []
       | pattify_term _ args _ (Const (x as (s, _))) =
         if fst (is_built_in x args) then []
         else [(massage_long_name s, weight_of_const s)]

 
 fun is_fact_in_graph access_G = can (Graph.get_node access_G) o nickname_of_thm
 
 val chained_feature_factor = 0.5
 val extra_feature_factor = 0.1
-val num_extra_feature_facts = 10 (* FUDGE *)
+val num_extra_feature_facts = 0 (* FUDGE *)
 
 (* FUDGE *)
 fun weight_of_proximity_fact rank =
   Math.pow (1.3, 15.5 - 0.2 * Real.fromInt rank) + 15.0
 

     fun chained_or_extra_features_of factor (((_, stature), th), weight) =
       [prop_of th]
       |> features_of ctxt prover (theory_of_thm th) num_facts const_tab stature
       |> map (apsnd (fn r => weight * factor * r))
     val (access_G, suggs) =
-      peek_state ctxt (fn {access_G, ...} =>
+      peek_state ctxt overlord (fn {access_G, ...} =>
           if Graph.is_empty access_G then
             (access_G, [])
           else
             let
               val parents = maximal_wrt_access_graph access_G facts

                 |> map (rpair 1.0)
                 |> map (chained_or_extra_features_of chained_feature_factor)
                 |> rpair [] |-> fold (union (op = o pairself fst))
               val extra_feats =
                 facts
-                |> take (num_extra_feature_facts - length chained)
+                |> take (Int.max (0, num_extra_feature_facts - length chained))
                 |> weight_facts_steeply
                 |> map (chained_or_extra_features_of extra_feature_factor)
                 |> rpair [] |-> fold (union (op = o pairself fst))
               val feats =
                 fold (union (op = o pairself fst)) [chained_feats, extra_feats]

         val name = freshish_name ()
         val feats =
           features_of ctxt prover thy 0 Symtab.empty (Local, General) [t]
           |> map fst
       in
-        peek_state ctxt (fn {access_G, ...} =>
+        peek_state ctxt overlord (fn {access_G, ...} =>
             let
               val parents = maximal_wrt_access_graph access_G facts
               val deps =
                 used_ths |> filter (is_fact_in_graph access_G)
                          |> map nickname_of_thm

                      auto_level run_prover learn_timeout facts =
   let
     val timer = Timer.startRealTimer ()
     fun next_commit_time () =
       Time.+ (Timer.checkRealTimer timer, commit_timeout)
-    val {access_G, ...} = peek_state ctxt I
+    val {access_G, ...} = peek_state ctxt overlord I
     val is_in_access_G = is_fact_in_graph access_G o snd
     val no_new_facts = forall is_in_access_G facts
   in
     if no_new_facts andalso not run_prover then
       if auto_level < 2 then

         fun commit last learns relearns flops =
           (if debug andalso auto_level = 0 then
              Output.urgent_message "Committing..."
            else
              ();
-           map_state ctxt (do_commit (rev learns) relearns flops);
+           map_state ctxt overlord (do_commit (rev learns) relearns flops);
            if not last andalso auto_level = 0 then
              let val num_proofs = length learns + length relearns in
                "Learned " ^ string_of_int num_proofs ^ " " ^
                (if run_prover then "automatic" else "Isar") ^ " proof" ^
                plural_s num_proofs ^ " in the last " ^

        |> Output.urgent_message;
        learn 0 false)
   end
 
 fun is_mash_enabled () = (getenv "MASH" = "yes")
-fun mash_can_suggest_facts ctxt =
-  not (Graph.is_empty (#access_G (peek_state ctxt I)))
+fun mash_can_suggest_facts ctxt overlord =
+  not (Graph.is_empty (#access_G (peek_state ctxt overlord I)))
 
 (* Generate more suggestions than requested, because some might be thrown out
    later for various reasons. *)
 fun generous_max_facts max_facts = max_facts + Int.min (50, max_facts)
 

 
 (* The threshold should be large enough so that MaSh doesn't kick in for Auto
    Sledgehammer and Try. *)
 val min_secs_for_learning = 15
 
-fun relevant_facts ctxt (params as {learn, fact_filter, timeout, ...}) prover
-        max_facts ({add, only, ...} : fact_override) hyp_ts concl_t facts =
+fun relevant_facts ctxt (params as {overlord, learn, fact_filter, timeout, ...})
+        prover max_facts ({add, only, ...} : fact_override) hyp_ts concl_t
+        facts =
   if not (subset (op =) (the_list fact_filter, fact_filters)) then
     error ("Unknown fact filter: " ^ quote (the fact_filter) ^ ".")
   else if only then
     let val facts = facts |> map fact_of_raw_fact in
       [("", facts)]

         case fact_filter of
           SOME ff => (() |> ff <> mepoN ? maybe_learn; ff)
         | NONE =>
           if is_mash_enabled () then
             (maybe_learn ();
-             if mash_can_suggest_facts ctxt then meshN else mepoN)
+             if mash_can_suggest_facts ctxt overlord then meshN else mepoN)
           else
             mepoN
       val add_ths = Attrib.eval_thms ctxt add
       fun in_add (_, th) = member Thm.eq_thm_prop add_ths th
       fun add_and_take accepts =

         [(meshN, mesh), (mepoN, mepo |> map fst |> add_and_take),
          (mashN, mash |> map fst |> add_and_take)]
       | _ => [("", mesh)]
     end
 
-fun kill_learners ctxt =
-  (Async_Manager.kill_threads MaShN "learner"; MaSh.shutdown ctxt)
+fun kill_learners ctxt ({overlord, ...} : params) =
+  (Async_Manager.kill_threads MaShN "learner"; MaSh.shutdown ctxt overlord)
 fun running_learners () = Async_Manager.running_threads MaShN "learner"
 
 end;