src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
author blanchet
Mon May 26 14:15:48 2014 +0200 (2014-05-26)
changeset 57089 353652f47974
parent 57076 3d4b172d2209
child 57095 001ec97c3e59
permissions -rw-r--r--
renamed 'MaSh' option
     1 (*  Title:      HOL/Tools/Sledgehammer/sledgehammer_mash.ML
     2     Author:     Jasmin Blanchette, TU Muenchen
     3     Author:     Cezary Kaliszyk, University of Innsbruck
     4 
     5 Sledgehammer's machine-learning-based relevance filter (MaSh).
     6 *)
     7 
     8 signature SLEDGEHAMMER_MASH =
     9 sig
    10   type stature = ATP_Problem_Generate.stature
    11   type raw_fact = Sledgehammer_Fact.raw_fact
    12   type fact = Sledgehammer_Fact.fact
    13   type fact_override = Sledgehammer_Fact.fact_override
    14   type params = Sledgehammer_Prover.params
    15   type prover_result = Sledgehammer_Prover.prover_result
    16 
    17   val trace : bool Config.T
    18   val MePoN : string
    19   val MaShN : string
    20   val MeShN : string
    21   val mepoN : string
    22   val mashN : string
    23   val meshN : string
    24   val unlearnN : string
    25   val learn_isarN : string
    26   val learn_proverN : string
    27   val relearn_isarN : string
    28   val relearn_proverN : string
    29   val fact_filters : string list
    30   val encode_str : string -> string
    31   val encode_strs : string list -> string
    32   val decode_str : string -> string
    33   val decode_strs : string -> string list
    34   val encode_features : (string * real) list -> string
    35   val extract_suggestions : string -> string * string list
    36 
    37   val mash_unlearn : Proof.context -> params -> unit
    38   val nickname_of_thm : thm -> string
    39   val find_suggested_facts : Proof.context -> ('b * thm) list -> string list -> ('b * thm) list
    40   val mesh_facts : ('a * 'a -> bool) -> int -> (real * (('a * real) list * 'a list)) list -> 'a list
    41   val crude_thm_ord : thm * thm -> order
    42   val thm_less : thm * thm -> bool
    43   val goal_of_thm : theory -> thm -> thm
    44   val run_prover_for_mash : Proof.context -> params -> string -> string -> fact list -> thm ->
    45     prover_result
    46   val features_of : Proof.context -> theory -> int -> int Symtab.table -> stature -> term list ->
    47     (string * real) list
    48   val trim_dependencies : string list -> string list option
    49   val isar_dependencies_of : string Symtab.table * string Symtab.table -> thm -> string list
    50   val prover_dependencies_of : Proof.context -> params -> string -> int -> raw_fact list ->
    51     string Symtab.table * string Symtab.table -> thm -> bool * string list
    52   val attach_parents_to_facts : ('a * thm) list -> ('a * thm) list ->
    53     (string list * ('a * thm)) list
    54   val num_extra_feature_facts : int
    55   val extra_feature_factor : real
    56   val weight_facts_smoothly : 'a list -> ('a * real) list
    57   val weight_facts_steeply : 'a list -> ('a * real) list
    58   val find_mash_suggestions : Proof.context -> int -> string list -> ('b * thm) list ->
    59     ('b * thm) list -> ('b * thm) list -> ('b * thm) list * ('b * thm) list
    60   val add_const_counts : term -> int Symtab.table -> int Symtab.table
    61   val mash_suggested_facts : Proof.context -> params -> int -> term list -> term -> raw_fact list ->
    62     fact list * fact list
    63   val mash_learn_proof : Proof.context -> params -> term -> ('a * thm) list -> thm list -> unit
    64   val mash_learn : Proof.context -> params -> fact_override -> thm list -> bool -> unit
    65 
    66   val mash_can_suggest_facts : Proof.context -> bool -> bool
    67   val generous_max_facts : int -> int
    68   val mepo_weight : real
    69   val mash_weight : real
    70   val relevant_facts : Proof.context -> params -> string -> int -> fact_override -> term list ->
    71     term -> raw_fact list -> (string * fact list) list
    72   val kill_learners : Proof.context -> params -> unit
    73   val running_learners : unit -> unit
    74 end;
    75 
    76 structure Sledgehammer_MaSh : SLEDGEHAMMER_MASH =
    77 struct
    78 
    79 open ATP_Util
    80 open ATP_Problem_Generate
    81 open Sledgehammer_Util
    82 open Sledgehammer_Fact
    83 open Sledgehammer_Prover
    84 open Sledgehammer_Prover_Minimize
    85 open Sledgehammer_MePo
    86 
    87 val trace = Attrib.setup_config_bool @{binding sledgehammer_mash_trace} (K false)
    88 
    89 fun trace_msg ctxt msg = if Config.get ctxt trace then tracing (msg ()) else ()
    90 
    91 val MePoN = "MePo"
    92 val MaShN = "MaSh"
    93 val MeShN = "MeSh"
    94 
    95 val mepoN = "mepo"
    96 val mashN = "mash"
    97 val meshN = "mesh"
    98 
    99 val fact_filters = [meshN, mepoN, mashN]
   100 
   101 val unlearnN = "unlearn"
   102 val learn_isarN = "learn_isar"
   103 val learn_proverN = "learn_prover"
   104 val relearn_isarN = "relearn_isar"
   105 val relearn_proverN = "relearn_prover"
   106 
   107 fun mash_state_dir () = Path.explode "$ISABELLE_HOME_USER/mash" |> tap Isabelle_System.mkdir
   108 fun mash_state_file () = Path.append (mash_state_dir ()) (Path.explode "state")
   109 
   110 fun wipe_out_mash_state_dir () =
   111   let val path = mash_state_dir () in
   112     try (File.fold_dir (fn file => fn _ => try File.rm (Path.append path (Path.basic file))) path)
   113       NONE;
   114     ()
   115   end
   116 
   117 datatype mash_engine = MaSh_Py | MaSh_SML_kNN | MaSh_SML_NB
   118 
   119 fun mash_engine () =
   120   let val flag1 = Options.default_string @{system_option MaSh} in
   121     (case if flag1 <> "none" (* default *) then flag1 else getenv "MASH" of
   122       "yes" => SOME MaSh_Py
   123     | "py" => SOME MaSh_Py
   124     | "sml" => SOME MaSh_SML_kNN
   125     | "sml_knn" => SOME MaSh_SML_kNN
   126     | "sml_nb" => SOME MaSh_SML_NB
   127     | _ => NONE)
   128   end
   129 
   130 val is_mash_enabled = is_some o mash_engine
   131 val the_mash_engine = the_default MaSh_Py o mash_engine
   132 
   133 
   134 (*** Low-level communication with Python version of MaSh ***)
   135 
   136 val save_models_arg = "--saveModels"
   137 val shutdown_server_arg = "--shutdownServer"
   138 
   139 fun wipe_out_file file = (try (File.rm o Path.explode) file; ())
   140 
   141 fun write_file banner (xs, f) path =
   142   (case banner of SOME s => File.write path s | NONE => ();
   143    xs |> chunk_list 500 |> List.app (File.append path o implode o map f))
   144   handle IO.Io _ => ()
   145 
   146 fun run_mash_tool ctxt overlord extra_args background write_cmds read_suggs =
   147   let
   148     val (temp_dir, serial) =
   149       if overlord then (getenv "ISABELLE_HOME_USER", "")
   150       else (getenv "ISABELLE_TMP", serial_string ())
   151     val log_file = temp_dir ^ "/mash_log" ^ serial
   152     val err_file = temp_dir ^ "/mash_err" ^ serial
   153     val sugg_file = temp_dir ^ "/mash_suggs" ^ serial
   154     val sugg_path = Path.explode sugg_file
   155     val cmd_file = temp_dir ^ "/mash_commands" ^ serial
   156     val cmd_path = Path.explode cmd_file
   157     val model_dir = File.shell_path (mash_state_dir ())
   158     val command =
   159       "cd \"$ISABELLE_SLEDGEHAMMER_MASH\"/src; \
   160       \PYTHONDONTWRITEBYTECODE=y ./mash.py\
   161       \ --quiet\
   162       \ --port=$MASH_PORT\
   163       \ --outputDir " ^ model_dir ^
   164       " --modelFile=" ^ model_dir ^ "/model.pickle\
   165       \ --dictsFile=" ^ model_dir ^ "/dict.pickle\
   166       \ --log " ^ log_file ^
   167       " --inputFile " ^ cmd_file ^
   168       " --predictions " ^ sugg_file ^
   169       (if extra_args = [] then "" else " " ^ space_implode " " extra_args) ^ " >& " ^ err_file ^
   170       (if background then " &" else "")
   171     fun run_on () =
   172       (Isabelle_System.bash command
   173        |> tap (fn _ =>
   174          (case try File.read (Path.explode err_file) |> the_default "" of
   175            "" => trace_msg ctxt (K "Done")
   176          | s => warning ("MaSh error: " ^ elide_string 1000 s)));
   177        read_suggs (fn () => try File.read_lines sugg_path |> these))
   178     fun clean_up () =
   179       if overlord then () else List.app wipe_out_file [err_file, sugg_file, cmd_file]
   180   in
   181     write_file (SOME "") ([], K "") sugg_path;
   182     write_file (SOME "") write_cmds cmd_path;
   183     trace_msg ctxt (fn () => "Running " ^ command);
   184     with_cleanup clean_up run_on ()
   185   end
   186 
   187 fun meta_char c =
   188   if Char.isAlphaNum c orelse c = #"_" orelse c = #"." orelse c = #"(" orelse c = #")" orelse
   189      c = #"," then
   190     String.str c
   191   else
   192     (* fixed width, in case more digits follow *)
   193     "%" ^ stringN_of_int 3 (Char.ord c)
   194 
   195 fun unmeta_chars accum [] = String.implode (rev accum)
   196   | unmeta_chars accum (#"%" :: d1 :: d2 :: d3 :: cs) =
   197     (case Int.fromString (String.implode [d1, d2, d3]) of
   198       SOME n => unmeta_chars (Char.chr n :: accum) cs
   199     | NONE => "" (* error *))
   200   | unmeta_chars _ (#"%" :: _) = "" (* error *)
   201   | unmeta_chars accum (c :: cs) = unmeta_chars (c :: accum) cs
   202 
   203 val encode_str = String.translate meta_char
   204 val decode_str = String.explode #> unmeta_chars []
   205 
   206 val encode_strs = map encode_str #> space_implode " "
   207 val decode_strs = space_explode " " #> filter_out (curry (op =) "") #> map decode_str
   208 
   209 (* Avoid scientific notation *)
   210 fun safe_str_of_real r =
   211   if r < 0.00001 then "0.00001"
   212   else if r >= 1000000.0 then "1000000"
   213   else Markup.print_real r
   214 
   215 fun encode_feature (names, weight) =
   216   encode_str names ^ (if Real.== (weight, 1.0) then "" else "=" ^ safe_str_of_real weight)
   217 
   218 fun decode_feature s =
   219   (case space_explode "=" s of
   220     [feat, weight] => (decode_str feat, Real.fromString weight |> the_default 1.0)
   221   | _ => (decode_str s, 1.0))
   222 
   223 val encode_features = map encode_feature #> space_implode " "
   224 val decode_features = space_explode " " #> map decode_feature
   225 
   226 fun str_of_learn (name, parents, feats, deps) =
   227   "! " ^ encode_str name ^ ": " ^ encode_strs parents ^ "; " ^ encode_strs feats ^ "; " ^
   228   encode_strs deps ^ "\n"
   229 
   230 fun str_of_relearn (name, deps) = "p " ^ encode_str name ^ ": " ^ encode_strs deps ^ "\n"
   231 
   232 fun str_of_query max_suggs (learns, hints, parents, feats) =
   233   implode (map str_of_learn learns) ^
   234   "? " ^ string_of_int max_suggs ^ " # " ^ encode_strs parents ^ "; " ^ encode_features feats ^
   235   (if null hints then "" else "; " ^ encode_strs hints) ^ "\n"
   236 
   237 (* The suggested weights do not make much sense. *)
   238 fun extract_suggestion sugg =
   239   (case space_explode "=" sugg of
   240     [name, _ (* weight *)] => SOME (decode_str name)
   241   | [name] => SOME (decode_str name)
   242   | _ => NONE)
   243 
   244 fun extract_suggestions line =
   245   (case space_explode ":" line of
   246     [goal, suggs] => (decode_str goal, map_filter extract_suggestion (space_explode " " suggs))
   247   | _ => ("", []))
   248 
   249 structure MaSh_Py =
   250 struct
   251 
   252 fun shutdown ctxt overlord =
   253   (trace_msg ctxt (K "MaSh_Py shutdown");
   254    run_mash_tool ctxt overlord [shutdown_server_arg] false ([], K "") (K ()))
   255 
   256 fun save ctxt overlord =
   257   (trace_msg ctxt (K "MaSh_Py save");
   258    run_mash_tool ctxt overlord [save_models_arg] true ([], K "") (K ()))
   259 
   260 fun unlearn ctxt overlord =
   261   (trace_msg ctxt (K "MaSh_Py unlearn");
   262    shutdown ctxt overlord;
   263    wipe_out_mash_state_dir ())
   264 
   265 fun learn _ _ _ [] = ()
   266   | learn ctxt overlord save learns =
   267     (trace_msg ctxt (fn () =>
   268        "MaSh_Py learn {" ^ elide_string 1000 (space_implode " " (map #1 learns)) ^ "}");
   269      run_mash_tool ctxt overlord ([] |> save ? cons save_models_arg) false (learns, str_of_learn)
   270        (K ()))
   271 
   272 fun relearn _ _ _ [] = ()
   273   | relearn ctxt overlord save relearns =
   274     (trace_msg ctxt (fn () => "MaSh_Py relearn " ^
   275        elide_string 1000 (space_implode " " (map #1 relearns)));
   276      run_mash_tool ctxt overlord ([] |> save ? cons save_models_arg) false
   277        (relearns, str_of_relearn) (K ()))
   278 
   279 fun query ctxt overlord max_suggs (query as (_, _, _, feats)) =
   280   (trace_msg ctxt (fn () => "MaSh_Py query " ^ encode_features feats);
   281    run_mash_tool ctxt overlord [] false ([query], str_of_query max_suggs) (fn suggs =>
   282      (case suggs () of [] => [] | suggs => snd (extract_suggestions (List.last suggs))))
   283    handle List.Empty => [])
   284 
   285 end;
   286 
   287 
   288 (*** Standard ML version of MaSh ***)
   289 
   290 structure MaSh_SML =
   291 struct
   292 
   293 exception BOTTOM of int
   294 
   295 fun heap cmp bnd a =
   296   let
   297     fun maxson l i =
   298       let val i31 = i + i + i + 1 in
   299         if i31 + 2 < l then
   300           let val x = Unsynchronized.ref i31 in
   301             if cmp (Array.sub (a, i31), Array.sub (a, i31 + 1)) = LESS then x := i31 + 1 else ();
   302             if cmp (Array.sub (a, !x), Array.sub (a, i31 + 2)) = LESS then x := i31 + 2 else ();
   303             !x
   304           end
   305         else
   306           if i31 + 1 < l andalso cmp (Array.sub (a, i31), Array.sub (a, i31 + 1)) = LESS
   307           then i31 + 1 else if i31 < l then i31 else raise BOTTOM i
   308       end
   309 
   310     fun trickledown l i e =
   311       let val j = maxson l i in
   312         if cmp (Array.sub (a, j), e) = GREATER then
   313           (Array.update (a, i, Array.sub (a, j)); trickledown l j e)
   314         else
   315           Array.update (a, i, e)
   316       end
   317 
   318     fun trickle l i e = trickledown l i e handle BOTTOM i => Array.update (a, i, e)
   319 
   320     fun bubbledown l i =
   321       let val j = maxson l i in
   322         Array.update (a, i, Array.sub (a, j));
   323         bubbledown l j
   324       end
   325 
   326     fun bubble l i = bubbledown l i handle BOTTOM i => i
   327 
   328     fun trickleup i e =
   329       let val father = (i - 1) div 3 in
   330         if cmp (Array.sub (a, father), e) = LESS then
   331           (Array.update (a, i, Array.sub (a, father));
   332            if father > 0 then trickleup father e else Array.update (a, 0, e))
   333         else
   334           Array.update (a, i, e)
   335       end
   336 
   337     val l = Array.length a
   338 
   339     fun for i = if i < 0 then () else (trickle l i (Array.sub (a, i)); for (i - 1))
   340 
   341     fun for2 i =
   342       if i < Integer.max 2 (l - bnd) then
   343         ()
   344       else
   345         let val e = Array.sub (a, i) in
   346           Array.update (a, i, Array.sub (a, 0));
   347           trickleup (bubble i 0) e;
   348           for2 (i - 1)
   349         end
   350   in
   351     for (((l + 1) div 3) - 1);
   352     for2 (l - 1);
   353     if l > 1 then
   354       let val e = Array.sub (a, 1) in
   355         Array.update (a, 1, Array.sub (a, 0));
   356         Array.update (a, 0, e)
   357       end
   358     else
   359       ()
   360   end
   361 
   362 (*
   363   avail_num = maximum number of theorems to check dependencies and symbols
   364   adv_max = do not return theorems over or equal to this number. Must satisfy: adv_max <= avail_num
   365   get_deps = returns dependencies of a theorem
   366   get_sym_ths = get theorems that have this feature
   367   knns = number of nearest neighbours
   368   advno = number of predictions to return
   369   syms = symbols of the conjecture
   370 *)
   371 fun k_nearest_neighbors avail_num adv_max get_deps get_sym_ths knns advno syms =
   372   let
   373     (* Can be later used for TFIDF *)
   374     fun sym_wght _ = 1.0
   375 
   376     val overlaps_sqr = Array.tabulate (avail_num, (fn i => (i, 0.0)))
   377 
   378     fun inc_overlap j v =
   379       let
   380         val ov = snd (Array.sub (overlaps_sqr, j))
   381       in
   382         Array.update (overlaps_sqr, j, (j, v + ov))
   383       end
   384 
   385     fun do_sym (s, con_wght) =
   386       let
   387         val sw = sym_wght s
   388         val w2 = sw * sw * con_wght
   389 
   390         fun do_th (j, prem_wght) = if j < avail_num then inc_overlap j (w2 * prem_wght) else ()
   391       in
   392         List.app do_th (get_sym_ths s)
   393       end
   394 
   395     val _ = List.app do_sym syms
   396     val _ = heap (Real.compare o pairself snd) knns overlaps_sqr
   397     val recommends = Array.tabulate (adv_max, rpair 0.0)
   398 
   399     fun inc_recommend j v =
   400       if j >= adv_max then ()
   401       else Array.update (recommends, j, (j, v + snd (Array.sub (recommends, j))))
   402 
   403     fun for k =
   404       if k = knns orelse k >= adv_max then
   405         ()
   406       else
   407         let
   408           val (j, o2) = Array.sub (overlaps_sqr, avail_num - k - 1)
   409           val o1 = Math.sqrt o2
   410           val _ = inc_recommend j o1
   411           val ds = get_deps j
   412           val l = Real.fromInt (length ds)
   413         in
   414           List.app (fn d => inc_recommend d (o1 / l)) ds; for (k + 1)
   415         end
   416 
   417     fun ret acc at =
   418       if at = Array.length recommends then acc else ret (Array.sub (recommends, at) :: acc) (at + 1)
   419   in
   420     for 0;
   421     heap (Real.compare o pairself snd) advno recommends;
   422     ret [] (Integer.max 0 (adv_max - advno))
   423   end
   424 
   425 (* Two arguments control the behaviour of naive Bayes: prior and ess. Prior expresses our belief in
   426    usefulness of unknown features, and ess (equivalent sample size) expresses our confidence in the
   427    prior. *)
   428 fun naive_bayes avail_num adv_max get_deps get_th_syms sym_num ess prior advno syms =
   429   let
   430     val afreq = Unsynchronized.ref 0
   431     val tfreq = Array.array (avail_num, 0)
   432     val sfreq = Array.array (avail_num, Inttab.empty)
   433 
   434     fun nb_learn syms ts =
   435       let
   436         fun add_sym hpis sym =
   437           let
   438             val im = Array.sub (sfreq, hpis)
   439             val v = the_default 0 (Inttab.lookup im sym)
   440           in
   441             Array.update (sfreq, hpis, Inttab.update (sym, v + 1) im)
   442           end
   443 
   444         fun add_th t =
   445           (Array.update (tfreq, t, Array.sub (tfreq, t) + 1); List.app (add_sym t) syms)
   446       in
   447         afreq := !afreq + 1; List.app add_th ts
   448       end
   449 
   450     fun nb_eval syms =
   451       let
   452         fun log_posterior i =
   453           let
   454             val symh = fold (Inttab.update o rpair ()) syms Inttab.empty
   455             val n = Real.fromInt (Array.sub (tfreq, i))
   456             val sfreqh = Array.sub (sfreq, i)
   457             val p = if prior > 0.0 then prior else ess / Real.fromInt (!afreq)
   458             val mp = ess * p
   459             val logmp = Math.ln mp
   460             val lognmp = Math.ln (n + mp)
   461 
   462             fun in_sfreqh (s, sfreqv) (sofar, sfsymh) =
   463               let val sfreqv = Real.fromInt sfreqv in
   464                 if Inttab.defined sfsymh s then
   465                   (sofar + Math.ln (sfreqv + mp), Inttab.delete s sfsymh)
   466                 else
   467                   (sofar + Math.ln (n - sfreqv + mp), sfsymh)
   468               end
   469 
   470             val (postsfreqh, symh) = Inttab.fold in_sfreqh sfreqh (Math.ln n, symh)
   471             val len_mem = length (Inttab.keys symh)
   472             val len_nomem = sym_num - len_mem - length (Inttab.keys sfreqh)
   473           in
   474             postsfreqh + Real.fromInt len_mem * logmp + Real.fromInt len_nomem * lognmp -
   475               Real.fromInt sym_num * Math.ln (n + ess)
   476           end
   477 
   478         val posterior = Array.tabulate (adv_max, swap o `log_posterior)
   479 
   480         fun ret acc at =
   481           if at = Array.length posterior then acc
   482           else ret (Array.sub (posterior, at) :: acc) (at + 1)
   483       in
   484         heap (Real.compare o pairself snd) advno posterior;
   485         ret [] (Integer.max 0 (adv_max - advno))
   486       end
   487 
   488     fun for i =
   489       if i = avail_num then () else (nb_learn (get_th_syms i) (i :: get_deps i); for (i + 1))
   490   in
   491     for 0; nb_eval syms
   492   end
   493 
   494 val knns = 40 (* FUDGE *)
   495 val ess = 0.00001 (* FUDGE *)
   496 val prior = 0.001 (* FUDGE *)
   497 
   498 fun add_to_xtab key (next, tab, keys) = (next + 1, Symtab.update_new (key, next) tab, key :: keys)
   499 
   500 fun map_array_at ary f i = Array.update (ary, i, f (Array.sub (ary, i)))
   501 
   502 fun query ctxt engine parents access_G max_suggs hints feats =
   503   let
   504     val visible_facts = Graph.all_preds access_G parents
   505     val visible_fact_set = Symtab.make_set visible_facts
   506 
   507     val all_nodes =
   508       (Graph.schedule (fn _ => fn (fact, (_, feats, deps)) => (fact, feats, deps)) access_G
   509        |> List.partition (Symtab.defined visible_fact_set o #1) |> op @) @
   510       (if null hints then [] else [(".goal", feats, hints)])
   511 
   512     val (rev_depss, rev_featss, (num_facts, _, rev_facts), (num_feats, feat_tab, _)) =
   513       fold (fn (fact, feats, deps) =>
   514             fn (rev_depss, rev_featss, fact_xtab as (_, fact_tab, _), feat_xtab) =>
   515           let
   516             fun add_feat (feat, weight) (xtab as (n, tab, _)) =
   517               (case Symtab.lookup tab feat of
   518                 SOME i => ((i, weight), xtab)
   519               | NONE => ((n, weight), add_to_xtab feat xtab))
   520 
   521             val (feats', feat_xtab') = fold_map add_feat feats feat_xtab
   522           in
   523             (map_filter (Symtab.lookup fact_tab) deps :: rev_depss, feats' :: rev_featss,
   524              add_to_xtab fact fact_xtab, feat_xtab')
   525           end)
   526         all_nodes ([], [], (0, Symtab.empty, []), (0, Symtab.empty, []))
   527 
   528     val facts = rev rev_facts
   529     val fact_vec = Vector.fromList facts
   530 
   531     val deps_vec = Vector.fromList (rev rev_depss)
   532 
   533     val num_visible_facts = length visible_facts
   534     val get_deps = curry Vector.sub deps_vec
   535   in
   536     trace_msg ctxt (fn () => "MaSh_SML " ^ (if engine = MaSh_SML_kNN then "kNN" else "NB") ^
   537       " query " ^ encode_features feats ^ " from {" ^
   538       elide_string 1000 (space_implode " " (take num_visible_facts facts)) ^ "}");
   539     (if engine = MaSh_SML_kNN then
   540        let
   541          val facts_ary = Array.array (num_feats, [])
   542          val _ =
   543            fold (fn feats => fn fact =>
   544                let val fact' = fact - 1 in
   545                  List.app (fn (feat, weight) => map_array_at facts_ary (cons (fact', weight)) feat)
   546                    feats;
   547                  fact'
   548                end)
   549              rev_featss num_facts
   550          val get_facts = curry Array.sub facts_ary
   551          val syms = map_filter (fn (feat, weight) =>
   552            Option.map (rpair weight) (Symtab.lookup feat_tab feat)) feats
   553        in
   554          k_nearest_neighbors num_facts num_visible_facts get_deps get_facts knns max_suggs syms
   555        end
   556      else
   557        let
   558          val unweighted_feats_ary = Vector.fromList (map (map fst) (rev rev_featss))
   559          val get_unweighted_feats = curry Vector.sub unweighted_feats_ary
   560          val unweighted_syms = map_filter (Symtab.lookup feat_tab o fst) feats
   561        in
   562          naive_bayes num_facts num_visible_facts get_deps get_unweighted_feats num_feats ess prior
   563            max_suggs unweighted_syms
   564        end)
   565     |> map (curry Vector.sub fact_vec o fst)
   566   end
   567 
   568 end;
   569 
   570 
   571 (*** Middle-level communication with MaSh ***)
   572 
   573 datatype proof_kind = Isar_Proof | Automatic_Proof | Isar_Proof_wegen_Prover_Flop
   574 
   575 fun str_of_proof_kind Isar_Proof = "i"
   576   | str_of_proof_kind Automatic_Proof = "a"
   577   | str_of_proof_kind Isar_Proof_wegen_Prover_Flop = "x"
   578 
   579 fun proof_kind_of_str "a" = Automatic_Proof
   580   | proof_kind_of_str "x" = Isar_Proof_wegen_Prover_Flop
   581   | proof_kind_of_str _ (* "i" *) = Isar_Proof
   582 
   583 fun add_edge_to name parent =
   584   Graph.default_node (parent, (Isar_Proof, [], []))
   585   #> Graph.add_edge (parent, name)
   586 
   587 fun add_node kind name parents feats deps G =
   588   (Graph.new_node (name, (kind, feats, deps)) G
   589    handle Graph.DUP _ => Graph.map_node name (K (kind, feats, deps)) G)
   590   |> fold (add_edge_to name) parents
   591 
   592 fun try_graph ctxt when def f =
   593   f ()
   594   handle
   595     Graph.CYCLES (cycle :: _) =>
   596     (trace_msg ctxt (fn () => "Cycle involving " ^ commas cycle ^ " when " ^ when); def)
   597   | Graph.DUP name =>
   598     (trace_msg ctxt (fn () => "Duplicate fact " ^ quote name ^ " when " ^ when); def)
   599   | Graph.UNDEF name =>
   600     (trace_msg ctxt (fn () => "Unknown fact " ^ quote name ^ " when " ^ when); def)
   601   | exn =>
   602     if Exn.is_interrupt exn then
   603       reraise exn
   604     else
   605       (trace_msg ctxt (fn () => "Internal error when " ^ when ^ ":\n" ^ Runtime.exn_message exn);
   606        def)
   607 
   608 fun graph_info G =
   609   string_of_int (length (Graph.keys G)) ^ " node(s), " ^
   610   string_of_int (fold (Integer.add o length o snd) (Graph.dest G) 0) ^ " edge(s), " ^
   611   string_of_int (length (Graph.maximals G)) ^ " maximal"
   612 
   613 type mash_state =
   614   {access_G : (proof_kind * (string * real) list * string list) Graph.T,
   615    num_known_facts : int,
   616    dirty : string list option}
   617 
   618 val empty_state = {access_G = Graph.empty, num_known_facts = 0, dirty = SOME []} : mash_state
   619 
   620 local
   621 
   622 val version = "*** MaSh version 20140519 ***"
   623 
   624 exception FILE_VERSION_TOO_NEW of unit
   625 
   626 fun extract_node line =
   627   (case space_explode ":" line of
   628     [head, tail] =>
   629     (case (space_explode " " head, map (unprefix " ") (space_explode ";" tail)) of
   630       ([kind, name], [parents, feats, deps]) =>
   631       SOME (proof_kind_of_str kind, decode_str name, decode_strs parents, decode_features feats,
   632         decode_strs deps)
   633     | _ => NONE)
   634   | _ => NONE)
   635 
   636 fun load_state ctxt overlord (time_state as (memory_time, _)) =
   637   let val path = mash_state_file () in
   638     (case try OS.FileSys.modTime (Path.implode (Path.expand path)) of
   639       NONE => time_state
   640     | SOME disk_time =>
   641       if Time.>= (memory_time, disk_time) then
   642         time_state
   643       else
   644         (disk_time,
   645          (case try File.read_lines path of
   646            SOME (version' :: node_lines) =>
   647            let
   648              fun extract_line_and_add_node line =
   649                (case extract_node line of
   650                  NONE => I (* should not happen *)
   651                | SOME (kind, name, parents, feats, deps) => add_node kind name parents feats deps)
   652 
   653              val (access_G, num_known_facts) =
   654                (case string_ord (version', version) of
   655                  EQUAL =>
   656                  (try_graph ctxt "loading state" Graph.empty (fn () =>
   657                     fold extract_line_and_add_node node_lines Graph.empty),
   658                   length node_lines)
   659                | LESS =>
   660                  (* cannot parse old file *)
   661                  (if the_mash_engine () = MaSh_Py then MaSh_Py.unlearn ctxt overlord
   662                   else wipe_out_mash_state_dir ();
   663                   (Graph.empty, 0))
   664                | GREATER => raise FILE_VERSION_TOO_NEW ())
   665            in
   666              trace_msg ctxt (fn () => "Loaded fact graph (" ^ graph_info access_G ^ ")");
   667              {access_G = access_G, num_known_facts = num_known_facts, dirty = SOME []}
   668            end
   669          | _ => empty_state)))
   670   end
   671 
   672 fun str_of_entry (kind, name, parents, feats, deps) =
   673   str_of_proof_kind kind ^ " " ^ encode_str name ^ ": " ^ encode_strs parents ^ "; " ^
   674   encode_features feats ^ "; " ^ encode_strs deps ^ "\n"
   675 
   676 fun save_state _ (time_state as (_, {dirty = SOME [], ...})) = time_state
   677   | save_state ctxt (memory_time, {access_G, num_known_facts, dirty}) =
   678     let
   679       fun append_entry (name, ((kind, feats, deps), (parents, _))) =
   680         cons (kind, name, Graph.Keys.dest parents, feats, deps)
   681 
   682       val path = mash_state_file ()
   683       val dirty' =
   684         (case try OS.FileSys.modTime (Path.implode path) of
   685           NONE => NONE
   686         | SOME disk_time => if Time.< (disk_time, memory_time) then dirty else NONE)
   687       val (banner, entries) =
   688         (case dirty' of
   689           SOME names => (NONE, fold (append_entry o Graph.get_entry access_G) names [])
   690         | NONE => (SOME (version ^ "\n"), Graph.fold append_entry access_G []))
   691     in
   692       write_file banner (entries, str_of_entry) path;
   693       trace_msg ctxt (fn () =>
   694         "Saved fact graph (" ^ graph_info access_G ^
   695         (case dirty of
   696           SOME dirty => "; " ^ string_of_int (length dirty) ^ " dirty fact(s)"
   697         | _ => "") ^  ")");
   698       (Time.now (), {access_G = access_G, num_known_facts = num_known_facts, dirty = SOME []})
   699     end
   700 
   701 val global_state =
   702   Synchronized.var "Sledgehammer_MaSh.global_state" (Time.zeroTime, empty_state)
   703 
   704 in
   705 
   706 fun map_state ctxt overlord f =
   707   Synchronized.change global_state (load_state ctxt overlord ##> f #> save_state ctxt)
   708   handle FILE_VERSION_TOO_NEW () => ()
   709 
   710 fun peek_state ctxt overlord f =
   711   Synchronized.change_result global_state (perhaps (try (load_state ctxt overlord)) #> `snd #>> f)
   712 
   713 fun clear_state ctxt overlord =
   714   (* "MaSh_Py.unlearn" also removes the state file *)
   715   Synchronized.change global_state (fn _ =>
   716     (if the_mash_engine () = MaSh_Py then MaSh_Py.unlearn ctxt overlord
   717      else wipe_out_mash_state_dir ();
   718      (Time.zeroTime, empty_state)))
   719 
   720 end
   721 
   722 fun mash_unlearn ctxt ({overlord, ...} : params) =
   723   (clear_state ctxt overlord; Output.urgent_message "Reset MaSh.")
   724 
   725 
   726 (*** Isabelle helpers ***)
   727 
   728 val local_prefix = "local" ^ Long_Name.separator
   729 
   730 fun elided_backquote_thm threshold th =
   731   elide_string threshold (backquote_thm (Proof_Context.init_global (Thm.theory_of_thm th)) th)
   732 
   733 val thy_name_of_thm = Context.theory_name o Thm.theory_of_thm
   734 
   735 fun nickname_of_thm th =
   736   if Thm.has_name_hint th then
   737     let val hint = Thm.get_name_hint th in
   738       (* There must be a better way to detect local facts. *)
   739       (case try (unprefix local_prefix) hint of
   740         SOME suf =>
   741         thy_name_of_thm th ^ Long_Name.separator ^ suf ^ Long_Name.separator ^
   742         elided_backquote_thm 50 th
   743       | NONE => hint)
   744     end
   745   else
   746     elided_backquote_thm 200 th
   747 
   748 fun find_suggested_facts ctxt facts =
   749   let
   750     fun add (fact as (_, th)) = Symtab.default (nickname_of_thm th, fact)
   751     val tab = fold add facts Symtab.empty
   752     fun lookup nick =
   753       Symtab.lookup tab nick
   754       |> tap (fn NONE => trace_msg ctxt (fn () => "Cannot find " ^ quote nick) | _ => ())
   755   in map_filter lookup end
   756 
   757 fun scaled_avg [] = 0
   758   | scaled_avg xs = Real.ceil (100000000.0 * fold (curry (op +)) xs 0.0) div length xs
   759 
   760 fun avg [] = 0.0
   761   | avg xs = fold (curry (op +)) xs 0.0 / Real.fromInt (length xs)
   762 
   763 fun normalize_scores _ [] = []
   764   | normalize_scores max_facts xs =
   765     map (apsnd (curry Real.* (1.0 / avg (map snd (take max_facts xs))))) xs
   766 
   767 fun mesh_facts _ max_facts [(_, (sels, unks))] =
   768     map fst (take max_facts sels) @ take (max_facts - length sels) unks
   769   | mesh_facts fact_eq max_facts mess =
   770     let
   771       val mess = mess |> map (apsnd (apfst (normalize_scores max_facts)))
   772 
   773       fun score_in fact (global_weight, (sels, unks)) =
   774         let val score_at = try (nth sels) #> Option.map (fn (_, score) => global_weight * score) in
   775           (case find_index (curry fact_eq fact o fst) sels of
   776             ~1 => if member fact_eq unks fact then NONE else SOME 0.0
   777           | rank => score_at rank)
   778         end
   779 
   780       fun weight_of fact = mess |> map_filter (score_in fact) |> scaled_avg
   781     in
   782       fold (union fact_eq o map fst o take max_facts o fst o snd) mess []
   783       |> map (`weight_of) |> sort (int_ord o swap o pairself fst)
   784       |> map snd |> take max_facts
   785     end
   786 
   787 val default_weight = 1.0
   788 fun free_feature_of s = ("f" ^ s, 40.0 (* FUDGE *))
   789 fun thy_feature_of s = ("y" ^ s, 8.0 (* FUDGE *))
   790 fun type_feature_of s = ("t" ^ s, 4.0 (* FUDGE *))
   791 fun class_feature_of s = ("s" ^ s, 1.0 (* FUDGE *))
   792 val local_feature = ("local", 16.0 (* FUDGE *))
   793 
   794 fun crude_theory_ord p =
   795   if Theory.subthy p then
   796     if Theory.eq_thy p then EQUAL else LESS
   797   else if Theory.subthy (swap p) then
   798     GREATER
   799   else
   800     (case int_ord (pairself (length o Theory.ancestors_of) p) of
   801       EQUAL => string_ord (pairself Context.theory_name p)
   802     | order => order)
   803 
   804 fun crude_thm_ord p =
   805   (case crude_theory_ord (pairself theory_of_thm p) of
   806     EQUAL =>
   807     (* The hack below is necessary because of odd dependencies that are not reflected in the theory
   808        comparison. *)
   809     let val q = pairself nickname_of_thm p in
   810       (* Hack to put "xxx_def" before "xxxI" and "xxxE" *)
   811       (case bool_ord (pairself (String.isSuffix "_def") (swap q)) of
   812         EQUAL => string_ord q
   813       | ord => ord)
   814     end
   815   | ord => ord)
   816 
   817 val thm_less_eq = Theory.subthy o pairself theory_of_thm
   818 fun thm_less p = thm_less_eq p andalso not (thm_less_eq (swap p))
   819 
   820 val freezeT = Type.legacy_freeze_type
   821 
   822 fun freeze (t $ u) = freeze t $ freeze u
   823   | freeze (Abs (s, T, t)) = Abs (s, freezeT T, freeze t)
   824   | freeze (Var ((s, _), T)) = Free (s, freezeT T)
   825   | freeze (Const (s, T)) = Const (s, freezeT T)
   826   | freeze (Free (s, T)) = Free (s, freezeT T)
   827   | freeze t = t
   828 
   829 fun goal_of_thm thy = prop_of #> freeze #> cterm_of thy #> Goal.init
   830 
   831 fun run_prover_for_mash ctxt params prover goal_name facts goal =
   832   let
   833     val problem =
   834       {comment = "Goal: " ^ goal_name, state = Proof.init ctxt, goal = goal, subgoal = 1,
   835        subgoal_count = 1, factss = [("", facts)]}
   836   in
   837     get_minimizing_prover ctxt MaSh (K ()) prover params (K (K (K ""))) problem
   838   end
   839 
   840 val bad_types = [@{type_name prop}, @{type_name bool}, @{type_name fun}]
   841 
   842 val pat_tvar_prefix = "_"
   843 val pat_var_prefix = "_"
   844 
   845 (* try "Long_Name.base_name" for shorter names *)
   846 fun massage_long_name s = s
   847 
   848 val crude_str_of_sort = space_implode ":" o map massage_long_name o subtract (op =) @{sort type}
   849 
   850 fun crude_str_of_typ (Type (s, [])) = massage_long_name s
   851   | crude_str_of_typ (Type (s, Ts)) = massage_long_name s ^ implode (map crude_str_of_typ Ts)
   852   | crude_str_of_typ (TFree (_, S)) = crude_str_of_sort S
   853   | crude_str_of_typ (TVar (_, S)) = crude_str_of_sort S
   854 
   855 fun maybe_singleton_str _ "" = []
   856   | maybe_singleton_str pref s = [pref ^ s]
   857 
   858 val max_pat_breadth = 10 (* FUDGE *)
   859 
   860 fun term_features_of ctxt thy_name num_facts const_tab term_max_depth type_max_depth ts =
   861   let
   862     val thy = Proof_Context.theory_of ctxt
   863 
   864     val fixes = map snd (Variable.dest_fixes ctxt)
   865     val classes = Sign.classes_of thy
   866 
   867     fun add_classes @{sort type} = I
   868       | add_classes S =
   869         fold (`(Sorts.super_classes classes)
   870           #> swap #> op ::
   871           #> subtract (op =) @{sort type} #> map massage_long_name
   872           #> map class_feature_of
   873           #> union (eq_fst (op =))) S
   874 
   875     fun pattify_type 0 _ = []
   876       | pattify_type _ (Type (s, [])) =
   877         if member (op =) bad_types s then [] else [massage_long_name s]
   878       | pattify_type depth (Type (s, U :: Ts)) =
   879         let
   880           val T = Type (s, Ts)
   881           val ps = take max_pat_breadth (pattify_type depth T)
   882           val qs = take max_pat_breadth ("" :: pattify_type (depth - 1) U)
   883         in
   884           map_product (fn p => fn "" => p | q => p ^ "(" ^ q ^ ")") ps qs
   885         end
   886       | pattify_type _ (TFree (_, S)) =
   887         maybe_singleton_str pat_tvar_prefix (crude_str_of_sort S)
   888       | pattify_type _ (TVar (_, S)) =
   889         maybe_singleton_str pat_tvar_prefix (crude_str_of_sort S)
   890 
   891     fun add_type_pat depth T =
   892       union (eq_fst (op =)) (map type_feature_of (pattify_type depth T))
   893 
   894     fun add_type_pats 0 _ = I
   895       | add_type_pats depth t =
   896         add_type_pat depth t #> add_type_pats (depth - 1) t
   897 
   898     fun add_type T =
   899       add_type_pats type_max_depth T
   900       #> fold_atyps_sorts (add_classes o snd) T
   901 
   902     fun add_subtypes (T as Type (_, Ts)) = add_type T #> fold add_subtypes Ts
   903       | add_subtypes T = add_type T
   904 
   905     fun weight_of_const s =
   906       16.0 +
   907       (if num_facts = 0 then
   908          0.0
   909        else
   910          let val count = Symtab.lookup const_tab s |> the_default 1 in
   911            Real.fromInt num_facts / Real.fromInt count (* FUDGE *)
   912          end)
   913 
   914     fun pattify_term _ 0 _ = []
   915       | pattify_term _ _ (Const (s, _)) =
   916         if is_widely_irrelevant_const s then [] else [(massage_long_name s, weight_of_const s)]
   917       | pattify_term _ _ (Free (s, T)) =
   918         maybe_singleton_str pat_var_prefix (crude_str_of_typ T)
   919         |> map (rpair 1.0)
   920         |> (if member (op =) fixes s then
   921               cons (free_feature_of (massage_long_name
   922                   (thy_name ^ Long_Name.separator ^ s)))
   923             else
   924               I)
   925       | pattify_term _ _ (Var (_, T)) =
   926         maybe_singleton_str pat_var_prefix (crude_str_of_typ T) |> map (rpair default_weight)
   927       | pattify_term Ts _ (Bound j) =
   928         maybe_singleton_str pat_var_prefix (crude_str_of_typ (nth Ts j))
   929         |> map (rpair default_weight)
   930       | pattify_term Ts depth (t $ u) =
   931         let
   932           val ps = take max_pat_breadth (pattify_term Ts depth t)
   933           val qs = take max_pat_breadth (("", default_weight) :: pattify_term Ts (depth - 1) u)
   934         in
   935           map_product (fn ppw as (p, pw) =>
   936             fn ("", _) => ppw
   937              | (q, qw) => (p ^ "(" ^ q ^ ")", pw + qw)) ps qs
   938         end
   939       | pattify_term _ _ _ = []
   940 
   941     fun add_term_pat Ts = union (eq_fst (op =)) oo pattify_term Ts
   942 
   943     fun add_term_pats _ 0 _ = I
   944       | add_term_pats Ts depth t = add_term_pat Ts depth t #> add_term_pats Ts (depth - 1) t
   945 
   946     fun add_term Ts = add_term_pats Ts term_max_depth
   947 
   948     fun add_subterms Ts t =
   949       (case strip_comb t of
   950         (Const (s, T), args) =>
   951         (not (is_widely_irrelevant_const s) ? add_term Ts t)
   952         #> add_subtypes T
   953         #> fold (add_subterms Ts) args
   954       | (head, args) =>
   955         (case head of
   956            Free (_, T) => add_term Ts t #> add_subtypes T
   957          | Var (_, T) => add_subtypes T
   958          | Abs (_, T, body) => add_subtypes T #> add_subterms (T :: Ts) body
   959          | _ => I)
   960         #> fold (add_subterms Ts) args)
   961   in
   962     fold (add_subterms []) ts []
   963   end
   964 
   965 val term_max_depth = 2
   966 val type_max_depth = 1
   967 
   968 (* TODO: Generate type classes for types? *)
   969 fun features_of ctxt thy num_facts const_tab (scope, _) ts =
   970   let val thy_name = Context.theory_name thy in
   971     thy_feature_of thy_name ::
   972     term_features_of ctxt thy_name num_facts const_tab term_max_depth type_max_depth ts
   973     |> scope <> Global ? cons local_feature
   974   end
   975 
   976 (* Too many dependencies is a sign that a decision procedure is at work. There is not much to learn
   977    from such proofs. *)
   978 val max_dependencies = 20
   979 
   980 val prover_default_max_facts = 25
   981 
   982 (* "type_definition_xxx" facts are characterized by their use of "CollectI". *)
   983 val typedef_dep = nickname_of_thm @{thm CollectI}
   984 (* Mysterious parts of the class machinery create lots of proofs that refer exclusively to
   985    "someI_ex" (and to some internal constructions). *)
   986 val class_some_dep = nickname_of_thm @{thm someI_ex}
   987 
   988 val fundef_ths =
   989   @{thms fundef_ex1_existence fundef_ex1_uniqueness fundef_ex1_iff fundef_default_value}
   990   |> map nickname_of_thm
   991 
   992 (* "Rep_xxx_inject", "Abs_xxx_inverse", etc., are derived using these facts. *)
   993 val typedef_ths =
   994   @{thms type_definition.Abs_inverse type_definition.Rep_inverse type_definition.Rep
   995       type_definition.Rep_inject type_definition.Abs_inject type_definition.Rep_cases
   996       type_definition.Abs_cases type_definition.Rep_induct type_definition.Abs_induct
   997       type_definition.Rep_range type_definition.Abs_image}
   998   |> map nickname_of_thm
   999 
  1000 fun is_size_def [dep] th =
  1001     (case first_field ".rec" dep of
  1002       SOME (pref, _) =>
  1003       (case first_field ".size" (nickname_of_thm th) of
  1004         SOME (pref', _) => pref = pref'
  1005       | NONE => false)
  1006     | NONE => false)
  1007   | is_size_def _ _ = false
  1008 
  1009 fun trim_dependencies deps =
  1010   if length deps > max_dependencies then NONE else SOME deps
  1011 
  1012 fun isar_dependencies_of name_tabs th =
  1013   let val deps = thms_in_proof (SOME name_tabs) th in
  1014     if deps = [typedef_dep] orelse deps = [class_some_dep] orelse
  1015        exists (member (op =) fundef_ths) deps orelse exists (member (op =) typedef_ths) deps orelse
  1016        is_size_def deps th then
  1017       []
  1018     else
  1019       deps
  1020   end
  1021 
  1022 fun prover_dependencies_of ctxt (params as {verbose, max_facts, ...}) prover auto_level facts
  1023     name_tabs th =
  1024   (case isar_dependencies_of name_tabs th of
  1025     [] => (false, [])
  1026   | isar_deps =>
  1027     let
  1028       val thy = Proof_Context.theory_of ctxt
  1029       val goal = goal_of_thm thy th
  1030       val name = nickname_of_thm th
  1031       val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal goal 1 ctxt
  1032       val facts = facts |> filter (fn (_, th') => thm_less (th', th))
  1033 
  1034       fun nickify ((_, stature), th) = ((nickname_of_thm th, stature), th)
  1035 
  1036       fun is_dep dep (_, th) = nickname_of_thm th = dep
  1037 
  1038       fun add_isar_dep facts dep accum =
  1039         if exists (is_dep dep) accum then
  1040           accum
  1041         else
  1042           (case find_first (is_dep dep) facts of
  1043             SOME ((_, status), th) => accum @ [(("", status), th)]
  1044           | NONE => accum (* should not happen *))
  1045 
  1046       val mepo_facts =
  1047         facts
  1048         |> mepo_suggested_facts ctxt params (max_facts |> the_default prover_default_max_facts) NONE
  1049              hyp_ts concl_t
  1050       val facts =
  1051         mepo_facts
  1052         |> fold (add_isar_dep facts) isar_deps
  1053         |> map nickify
  1054       val num_isar_deps = length isar_deps
  1055     in
  1056       if verbose andalso auto_level = 0 then
  1057         Output.urgent_message ("MaSh: " ^ quote prover ^ " on " ^ quote name ^ " with " ^
  1058           string_of_int num_isar_deps ^ " + " ^ string_of_int (length facts - num_isar_deps) ^
  1059           " facts.")
  1060       else
  1061         ();
  1062       (case run_prover_for_mash ctxt params prover name facts goal of
  1063         {outcome = NONE, used_facts, ...} =>
  1064         (if verbose andalso auto_level = 0 then
  1065            let val num_facts = length used_facts in
  1066              Output.urgent_message ("Found proof with " ^ string_of_int num_facts ^ " fact" ^
  1067                plural_s num_facts ^ ".")
  1068            end
  1069          else
  1070            ();
  1071          (true, map fst used_facts))
  1072       | _ => (false, isar_deps))
  1073     end)
  1074 
  1075 
  1076 (*** High-level communication with MaSh ***)
  1077 
  1078 (* In the following functions, chunks are risers w.r.t. "thm_less_eq". *)
  1079 
  1080 fun chunks_and_parents_for chunks th =
  1081   let
  1082     fun insert_parent new parents =
  1083       let val parents = parents |> filter_out (fn p => thm_less_eq (p, new)) in
  1084         parents |> forall (fn p => not (thm_less_eq (new, p))) parents
  1085                    ? cons new
  1086       end
  1087 
  1088     fun rechunk seen (rest as th' :: ths) =
  1089       if thm_less_eq (th', th) then (rev seen, rest)
  1090       else rechunk (th' :: seen) ths
  1091 
  1092     fun do_chunk [] accum = accum
  1093       | do_chunk (chunk as hd_chunk :: _) (chunks, parents) =
  1094         if thm_less_eq (hd_chunk, th) then
  1095           (chunk :: chunks, insert_parent hd_chunk parents)
  1096         else if thm_less_eq (List.last chunk, th) then
  1097           let val (front, back as hd_back :: _) = rechunk [] chunk in
  1098             (front :: back :: chunks, insert_parent hd_back parents)
  1099           end
  1100         else
  1101           (chunk :: chunks, parents)
  1102   in
  1103     fold_rev do_chunk chunks ([], [])
  1104     |>> cons []
  1105     ||> map nickname_of_thm
  1106   end
  1107 
  1108 fun attach_parents_to_facts _ [] = []
  1109   | attach_parents_to_facts old_facts (facts as (_, th) :: _) =
  1110     let
  1111       fun do_facts _ [] = []
  1112         | do_facts (_, parents) [fact] = [(parents, fact)]
  1113         | do_facts (chunks, parents)
  1114                    ((fact as (_, th)) :: (facts as (_, th') :: _)) =
  1115           let
  1116             val chunks = app_hd (cons th) chunks
  1117             val chunks_and_parents' =
  1118               if thm_less_eq (th, th') andalso
  1119                  thy_name_of_thm th = thy_name_of_thm th' then
  1120                 (chunks, [nickname_of_thm th])
  1121               else
  1122                 chunks_and_parents_for chunks th'
  1123           in
  1124             (parents, fact) :: do_facts chunks_and_parents' facts
  1125           end
  1126     in
  1127       old_facts @ facts
  1128       |> do_facts (chunks_and_parents_for [[]] th)
  1129       |> drop (length old_facts)
  1130     end
  1131 
  1132 fun maximal_wrt_graph G keys =
  1133   let
  1134     val tab = Symtab.empty |> fold (fn name => Symtab.default (name, ())) keys
  1135 
  1136     fun insert_new seen name = not (Symtab.defined seen name) ? insert (op =) name
  1137 
  1138     fun num_keys keys = Graph.Keys.fold (K (Integer.add 1)) keys 0
  1139 
  1140     fun find_maxes _ (maxs, []) = map snd maxs
  1141       | find_maxes seen (maxs, new :: news) =
  1142         find_maxes (seen |> num_keys (Graph.imm_succs G new) > 1 ? Symtab.default (new, ()))
  1143           (if Symtab.defined tab new then
  1144              let
  1145                val newp = Graph.all_preds G [new]
  1146                fun is_ancestor x yp = member (op =) yp x
  1147                val maxs = maxs |> filter (fn (_, max) => not (is_ancestor max newp))
  1148              in
  1149                if exists (is_ancestor new o fst) maxs then (maxs, news)
  1150                else ((newp, new) :: filter_out (fn (_, max) => is_ancestor max newp) maxs, news)
  1151              end
  1152            else
  1153              (maxs, Graph.Keys.fold (insert_new seen) (Graph.imm_preds G new) news))
  1154   in
  1155     find_maxes Symtab.empty ([], Graph.maximals G)
  1156   end
  1157 
  1158 fun maximal_wrt_access_graph access_G facts =
  1159   map (nickname_of_thm o snd) facts
  1160   |> maximal_wrt_graph access_G
  1161 
  1162 fun is_fact_in_graph access_G = can (Graph.get_node access_G) o nickname_of_thm
  1163 
  1164 val chained_feature_factor = 0.5 (* FUDGE *)
  1165 val extra_feature_factor = 0.1 (* FUDGE *)
  1166 val num_extra_feature_facts = 10 (* FUDGE *)
  1167 
  1168 (* FUDGE *)
  1169 fun weight_of_proximity_fact rank =
  1170   Math.pow (1.3, 15.5 - 0.2 * Real.fromInt rank) + 15.0
  1171 
  1172 fun weight_facts_smoothly facts =
  1173   facts ~~ map weight_of_proximity_fact (0 upto length facts - 1)
  1174 
  1175 (* FUDGE *)
  1176 fun steep_weight_of_fact rank =
  1177   Math.pow (0.62, log2 (Real.fromInt (rank + 1)))
  1178 
  1179 fun weight_facts_steeply facts =
  1180   facts ~~ map steep_weight_of_fact (0 upto length facts - 1)
  1181 
  1182 val max_proximity_facts = 100
  1183 
  1184 fun find_mash_suggestions ctxt max_facts suggs facts chained raw_unknown =
  1185   let
  1186     val inter_fact = inter (eq_snd Thm.eq_thm_prop)
  1187     val raw_mash = find_suggested_facts ctxt facts suggs
  1188     val proximate = take max_proximity_facts facts
  1189     val unknown_chained = inter_fact raw_unknown chained
  1190     val unknown_proximate = inter_fact raw_unknown proximate
  1191     val mess =
  1192       [(0.9 (* FUDGE *), (map (rpair 1.0) unknown_chained, [])),
  1193        (0.4 (* FUDGE *), (weight_facts_smoothly unknown_proximate, [])),
  1194        (0.1 (* FUDGE *), (weight_facts_steeply raw_mash, raw_unknown))]
  1195     val unknown = raw_unknown
  1196       |> fold (subtract (eq_snd Thm.eq_thm_prop)) [unknown_chained, unknown_proximate]
  1197   in
  1198     (mesh_facts (eq_snd Thm.eq_thm_prop) max_facts mess, unknown)
  1199   end
  1200 
  1201 fun add_const_counts t =
  1202   fold (fn s => Symtab.map_default (s, 0) (Integer.add 1)) (Term.add_const_names t [])
  1203 
  1204 fun mash_suggested_facts ctxt ({debug, overlord, ...} : params) max_facts hyp_ts concl_t facts =
  1205   let
  1206     val thy = Proof_Context.theory_of ctxt
  1207     val thy_name = Context.theory_name thy
  1208     val engine = the_mash_engine ()
  1209 
  1210     val facts = facts |> sort (crude_thm_ord o pairself snd o swap)
  1211     val chained = facts |> filter (fn ((_, (scope, _)), _) => scope = Chained)
  1212     val num_facts = length facts
  1213 
  1214     (* Weights are currently ignored by SML naive Bayes and appear to hurt kNN more than they
  1215        help. *)
  1216     val const_tab = Symtab.empty |> engine = MaSh_Py ? fold (add_const_counts o prop_of o snd) facts
  1217 
  1218     fun fact_has_right_theory (_, th) =
  1219       thy_name = Context.theory_name (theory_of_thm th)
  1220 
  1221     fun chained_or_extra_features_of factor (((_, stature), th), weight) =
  1222       [prop_of th]
  1223       |> features_of ctxt (theory_of_thm th) num_facts const_tab stature
  1224       |> map (apsnd (fn r => weight * factor * r))
  1225 
  1226     fun query_args access_G =
  1227       let
  1228         val parents = maximal_wrt_access_graph access_G facts
  1229         val hints = chained
  1230           |> filter (is_fact_in_graph access_G o snd)
  1231           |> map (nickname_of_thm o snd)
  1232 
  1233         val goal_feats =
  1234           features_of ctxt thy num_facts const_tab (Local, General) (concl_t :: hyp_ts)
  1235         val chained_feats = chained
  1236           |> map (rpair 1.0)
  1237           |> map (chained_or_extra_features_of chained_feature_factor)
  1238           |> rpair [] |-> fold (union (eq_fst (op =)))
  1239         val extra_feats =
  1240           (* As long as SML NB does not support weights, it makes little sense to include these
  1241              extra features. *)
  1242           if engine = MaSh_SML_NB then
  1243             []
  1244           else
  1245             facts
  1246             |> take (Int.max (0, num_extra_feature_facts - length chained))
  1247             |> filter fact_has_right_theory
  1248             |> weight_facts_steeply
  1249             |> map (chained_or_extra_features_of extra_feature_factor)
  1250             |> rpair [] |-> fold (union (eq_fst (op =)))
  1251         val feats = fold (union (eq_fst (op =))) [chained_feats, extra_feats] goal_feats
  1252           |> debug ? sort (Real.compare o swap o pairself snd)
  1253       in
  1254         (parents, hints, feats)
  1255       end
  1256 
  1257     val (access_G, py_suggs) =
  1258       peek_state ctxt overlord (fn {access_G, ...} =>
  1259         if Graph.is_empty access_G then
  1260           (trace_msg ctxt (K "Nothing has been learned yet"); (access_G, []))
  1261         else
  1262           (access_G,
  1263            if engine = MaSh_Py then
  1264              let val (parents, hints, feats) = query_args access_G in
  1265                MaSh_Py.query ctxt overlord max_facts ([], hints, parents, feats)
  1266              end
  1267            else
  1268              []))
  1269 
  1270     val sml_suggs =
  1271       if engine = MaSh_Py then
  1272         []
  1273       else
  1274         let val (parents, hints, feats) = query_args access_G in
  1275           MaSh_SML.query ctxt engine parents access_G max_facts hints feats
  1276         end
  1277 
  1278     val unknown = filter_out (is_fact_in_graph access_G o snd) facts
  1279   in
  1280     find_mash_suggestions ctxt max_facts (py_suggs @ sml_suggs) facts chained unknown
  1281     |> pairself (map fact_of_raw_fact)
  1282   end
  1283 
  1284 fun learn_wrt_access_graph ctxt (name, parents, feats, deps) (learns, G) =
  1285   let
  1286     fun maybe_learn_from from (accum as (parents, G)) =
  1287       try_graph ctxt "updating graph" accum (fn () =>
  1288         (from :: parents, Graph.add_edge_acyclic (from, name) G))
  1289     val G = G |> Graph.default_node (name, (Isar_Proof, feats, deps))
  1290     val (parents, G) = ([], G) |> fold maybe_learn_from parents
  1291     val (deps, _) = ([], G) |> fold maybe_learn_from deps
  1292   in
  1293     ((name, parents, map fst feats, deps) :: learns, G)
  1294   end
  1295 
  1296 fun relearn_wrt_access_graph ctxt (name, deps) (relearns, G) =
  1297   let
  1298     fun maybe_relearn_from from (accum as (parents, G)) =
  1299       try_graph ctxt "updating graph" accum (fn () =>
  1300         (from :: parents, Graph.add_edge_acyclic (from, name) G))
  1301     val G = G |> Graph.map_node name (fn (_, feats, _) => (Automatic_Proof, feats, deps))
  1302     val (deps, _) = ([], G) |> fold maybe_relearn_from deps
  1303   in
  1304     ((name, deps) :: relearns, G)
  1305   end
  1306 
  1307 fun flop_wrt_access_graph name =
  1308   Graph.map_node name (fn (_, feats, deps) => (Isar_Proof_wegen_Prover_Flop, feats, deps))
  1309 
  1310 val learn_timeout_slack = 2.0
  1311 
  1312 fun launch_thread timeout task =
  1313   let
  1314     val hard_timeout = time_mult learn_timeout_slack timeout
  1315     val birth_time = Time.now ()
  1316     val death_time = Time.+ (birth_time, hard_timeout)
  1317     val desc = ("Machine learner for Sledgehammer", "")
  1318   in
  1319     Async_Manager.thread MaShN birth_time death_time desc task
  1320   end
  1321 
  1322 fun learned_proof_name () =
  1323   Date.fmt ".%Y%m%d.%H%M%S." (Date.fromTimeLocal (Time.now ())) ^ serial_string ()
  1324 
  1325 fun mash_learn_proof ctxt ({overlord, timeout, ...} : params) t facts used_ths =
  1326   if is_mash_enabled () then
  1327     launch_thread timeout (fn () =>
  1328       let
  1329         val thy = Proof_Context.theory_of ctxt
  1330         val feats = features_of ctxt thy 0 Symtab.empty (Local, General) [t]
  1331       in
  1332         map_state ctxt overlord (fn state as {access_G, num_known_facts, dirty} =>
  1333           let
  1334             val name = learned_proof_name ()
  1335             val parents = maximal_wrt_access_graph access_G facts
  1336             val deps = used_ths
  1337               |> filter (is_fact_in_graph access_G)
  1338               |> map nickname_of_thm
  1339           in
  1340             if the_mash_engine () = MaSh_Py then
  1341               (MaSh_Py.learn ctxt overlord true [("", parents, map fst feats, deps)]; state)
  1342             else
  1343               let val access_G = access_G |> add_node Automatic_Proof name parents feats deps in
  1344                 {access_G = access_G, num_known_facts = num_known_facts + 1,
  1345                  dirty = Option.map (cons name) dirty}
  1346               end
  1347           end);
  1348         (true, "")
  1349       end)
  1350   else
  1351     ()
  1352 
  1353 fun sendback sub =
  1354   Active.sendback_markup [Markup.padding_command] (sledgehammerN ^ " " ^ sub)
  1355 
  1356 val commit_timeout = seconds 30.0
  1357 
  1358 (* The timeout is understood in a very relaxed fashion. *)
  1359 fun mash_learn_facts ctxt (params as {debug, verbose, overlord, ...}) prover save auto_level
  1360     run_prover learn_timeout facts =
  1361   let
  1362     val timer = Timer.startRealTimer ()
  1363     fun next_commit_time () = Time.+ (Timer.checkRealTimer timer, commit_timeout)
  1364 
  1365     val engine = the_mash_engine ()
  1366     val {access_G, ...} = peek_state ctxt overlord I
  1367     val is_in_access_G = is_fact_in_graph access_G o snd
  1368     val no_new_facts = forall is_in_access_G facts
  1369   in
  1370     if no_new_facts andalso not run_prover then
  1371       if auto_level < 2 then
  1372         "No new " ^ (if run_prover then "automatic" else "Isar") ^ " proofs to learn." ^
  1373         (if auto_level = 0 andalso not run_prover then
  1374            "\n\nHint: Try " ^ sendback learn_proverN ^ " to learn from an automatic prover."
  1375          else
  1376            "")
  1377       else
  1378         ""
  1379     else
  1380       let
  1381         val name_tabs = build_name_tables nickname_of_thm facts
  1382 
  1383         fun deps_of status th =
  1384           if status = Non_Rec_Def orelse status = Rec_Def then
  1385             SOME []
  1386           else if run_prover then
  1387             prover_dependencies_of ctxt params prover auto_level facts name_tabs th
  1388             |> (fn (false, _) => NONE | (true, deps) => trim_dependencies deps)
  1389           else
  1390             isar_dependencies_of name_tabs th
  1391             |> trim_dependencies
  1392 
  1393         fun do_commit [] [] [] state = state
  1394           | do_commit learns relearns flops {access_G, num_known_facts, dirty} =
  1395             let
  1396               val was_empty = Graph.is_empty access_G
  1397               val (learns, access_G) = ([], access_G) |> fold (learn_wrt_access_graph ctxt) learns
  1398               val (relearns, access_G) =
  1399                 ([], access_G) |> fold (relearn_wrt_access_graph ctxt) relearns
  1400               val access_G = access_G |> fold flop_wrt_access_graph flops
  1401               val num_known_facts = num_known_facts + length learns
  1402               val dirty =
  1403                 (case (was_empty, dirty) of
  1404                   (false, SOME names) => SOME (map #1 learns @ map #1 relearns @ names)
  1405                 | _ => NONE)
  1406             in
  1407               if engine = MaSh_Py then
  1408                 (MaSh_Py.learn ctxt overlord (save andalso null relearns) (rev learns);
  1409                  MaSh_Py.relearn ctxt overlord save relearns)
  1410               else
  1411                 ();
  1412               {access_G = access_G, num_known_facts = num_known_facts, dirty = dirty}
  1413             end
  1414 
  1415         fun commit last learns relearns flops =
  1416           (if debug andalso auto_level = 0 then Output.urgent_message "Committing..." else ();
  1417            map_state ctxt overlord (do_commit (rev learns) relearns flops);
  1418            if not last andalso auto_level = 0 then
  1419              let val num_proofs = length learns + length relearns in
  1420                Output.urgent_message ("Learned " ^ string_of_int num_proofs ^ " " ^
  1421                  (if run_prover then "automatic" else "Isar") ^ " proof" ^
  1422                  plural_s num_proofs ^ " in the last " ^ string_of_time commit_timeout ^ ".")
  1423              end
  1424            else
  1425              ())
  1426 
  1427         fun learn_new_fact _ (accum as (_, (_, _, true))) = accum
  1428           | learn_new_fact (parents, ((_, stature as (_, status)), th))
  1429               (learns, (n, next_commit, _)) =
  1430             let
  1431               val name = nickname_of_thm th
  1432               val feats = features_of ctxt (theory_of_thm th) 0 Symtab.empty stature [prop_of th]
  1433               val deps = deps_of status th |> these
  1434               val n = n |> not (null deps) ? Integer.add 1
  1435               val learns = (name, parents, feats, deps) :: learns
  1436               val (learns, next_commit) =
  1437                 if Time.> (Timer.checkRealTimer timer, next_commit) then
  1438                   (commit false learns [] []; ([], next_commit_time ()))
  1439                 else
  1440                   (learns, next_commit)
  1441               val timed_out = Time.> (Timer.checkRealTimer timer, learn_timeout)
  1442             in
  1443               (learns, (n, next_commit, timed_out))
  1444             end
  1445 
  1446         val n =
  1447           if no_new_facts then
  1448             0
  1449           else
  1450             let
  1451               val new_facts = facts
  1452                 |> sort (crude_thm_ord o pairself snd)
  1453                 |> attach_parents_to_facts []
  1454                 |> filter_out (is_in_access_G o snd)
  1455               val (learns, (n, _, _)) =
  1456                 ([], (0, next_commit_time (), false))
  1457                 |> fold learn_new_fact new_facts
  1458             in
  1459               commit true learns [] []; n
  1460             end
  1461 
  1462         fun relearn_old_fact _ (accum as (_, (_, _, true))) = accum
  1463           | relearn_old_fact ((_, (_, status)), th) ((relearns, flops), (n, next_commit, _)) =
  1464             let
  1465               val name = nickname_of_thm th
  1466               val (n, relearns, flops) =
  1467                 (case deps_of status th of
  1468                   SOME deps => (n + 1, (name, deps) :: relearns, flops)
  1469                 | NONE => (n, relearns, name :: flops))
  1470               val (relearns, flops, next_commit) =
  1471                 if Time.> (Timer.checkRealTimer timer, next_commit) then
  1472                   (commit false [] relearns flops; ([], [], next_commit_time ()))
  1473                 else
  1474                   (relearns, flops, next_commit)
  1475               val timed_out = Time.> (Timer.checkRealTimer timer, learn_timeout)
  1476             in
  1477               ((relearns, flops), (n, next_commit, timed_out))
  1478             end
  1479 
  1480         val n =
  1481           if not run_prover then
  1482             n
  1483           else
  1484             let
  1485               val max_isar = 1000 * max_dependencies
  1486 
  1487               fun priority_of th =
  1488                 random_range 0 max_isar +
  1489                 (case try (Graph.get_node access_G) (nickname_of_thm th) of
  1490                   SOME (Isar_Proof, _, deps) => ~100 * length deps
  1491                 | SOME (Automatic_Proof, _, _) => 2 * max_isar
  1492                 | SOME (Isar_Proof_wegen_Prover_Flop, _, _) => max_isar
  1493                 | NONE => 0)
  1494 
  1495               val old_facts = facts
  1496                 |> filter is_in_access_G
  1497                 |> map (`(priority_of o snd))
  1498                 |> sort (int_ord o pairself fst)
  1499                 |> map snd
  1500               val ((relearns, flops), (n, _, _)) =
  1501                 (([], []), (n, next_commit_time (), false))
  1502                 |> fold relearn_old_fact old_facts
  1503             in
  1504               commit true [] relearns flops; n
  1505             end
  1506       in
  1507         if verbose orelse auto_level < 2 then
  1508           "Learned " ^ string_of_int n ^ " nontrivial " ^
  1509           (if run_prover then "automatic and " else "") ^ "Isar proof" ^ plural_s n ^
  1510           (if verbose then " in " ^ string_of_time (Timer.checkRealTimer timer) else "") ^ "."
  1511         else
  1512           ""
  1513       end
  1514   end
  1515 
  1516 fun mash_learn ctxt (params as {provers, timeout, ...}) fact_override chained run_prover =
  1517   let
  1518     val css = Sledgehammer_Fact.clasimpset_rule_table_of ctxt
  1519     val ctxt = ctxt |> Config.put instantiate_inducts false
  1520     val facts = nearly_all_facts ctxt false fact_override Symtab.empty css chained [] @{prop True}
  1521       |> sort (crude_thm_ord o pairself snd o swap)
  1522     val num_facts = length facts
  1523     val prover = hd provers
  1524 
  1525     fun learn auto_level run_prover =
  1526       mash_learn_facts ctxt params prover true auto_level run_prover one_year facts
  1527       |> Output.urgent_message
  1528   in
  1529     if run_prover then
  1530       (Output.urgent_message ("MaShing through " ^ string_of_int num_facts ^ " fact" ^
  1531          plural_s num_facts ^ " for automatic proofs (" ^ quote prover ^ " timeout: " ^
  1532          string_of_time timeout ^ ").\n\nCollecting Isar proofs first...");
  1533        learn 1 false;
  1534        Output.urgent_message "Now collecting automatic proofs. This may take several hours. You \
  1535          \can safely stop the learning process at any point.";
  1536        learn 0 true)
  1537     else
  1538       (Output.urgent_message ("MaShing through " ^ string_of_int num_facts ^ " fact" ^
  1539          plural_s num_facts ^ " for Isar proofs...");
  1540        learn 0 false)
  1541   end
  1542 
  1543 fun mash_can_suggest_facts ctxt overlord =
  1544   not (Graph.is_empty (#access_G (peek_state ctxt overlord I)))
  1545 
  1546 (* Generate more suggestions than requested, because some might be thrown out
  1547    later for various reasons. *)
  1548 fun generous_max_facts max_facts = max_facts + Int.min (50, max_facts)
  1549 
  1550 val mepo_weight = 0.5
  1551 val mash_weight = 0.5
  1552 
  1553 val max_facts_to_learn_before_query = 100
  1554 
  1555 (* The threshold should be large enough so that MaSh does not get activated for Auto Sledgehammer
  1556    and Try. *)
  1557 val min_secs_for_learning = 15
  1558 
  1559 fun relevant_facts ctxt (params as {overlord, blocking, learn, fact_filter, timeout, ...}) prover
  1560     max_facts ({add, only, ...} : fact_override) hyp_ts concl_t facts =
  1561   if not (subset (op =) (the_list fact_filter, fact_filters)) then
  1562     error ("Unknown fact filter: " ^ quote (the fact_filter) ^ ".")
  1563   else if only then
  1564     let val facts = facts |> map fact_of_raw_fact in
  1565       [("", facts)]
  1566     end
  1567   else if max_facts <= 0 orelse null facts then
  1568     [("", [])]
  1569   else
  1570     let
  1571       fun maybe_launch_thread () =
  1572         if not blocking andalso not (Async_Manager.has_running_threads MaShN) andalso
  1573            Time.toSeconds timeout >= min_secs_for_learning then
  1574           let val timeout = time_mult learn_timeout_slack timeout in
  1575             launch_thread timeout
  1576               (fn () => (true, mash_learn_facts ctxt params prover true 2 false timeout facts))
  1577           end
  1578         else
  1579           ()
  1580 
  1581       fun maybe_learn () =
  1582         if is_mash_enabled () andalso learn then
  1583           let
  1584             val {access_G, num_known_facts, ...} = peek_state ctxt overlord I
  1585             val is_in_access_G = is_fact_in_graph access_G o snd
  1586           in
  1587             if length facts - num_known_facts <= max_facts_to_learn_before_query then
  1588               (case length (filter_out is_in_access_G facts) of
  1589                 0 => false
  1590               | num_facts_to_learn =>
  1591                 if num_facts_to_learn <= max_facts_to_learn_before_query then
  1592                   (mash_learn_facts ctxt params prover false 2 false timeout facts
  1593                    |> (fn "" => () | s => Output.urgent_message (MaShN ^ ": " ^ s));
  1594                    true)
  1595                 else
  1596                   (maybe_launch_thread (); false))
  1597             else
  1598               (maybe_launch_thread (); false)
  1599           end
  1600         else
  1601           false
  1602 
  1603       val (save, effective_fact_filter) =
  1604         (case fact_filter of
  1605           SOME ff => (ff <> mepoN andalso maybe_learn (), ff)
  1606         | NONE =>
  1607           if is_mash_enabled () then
  1608             (maybe_learn (),
  1609              if mash_can_suggest_facts ctxt overlord then meshN else mepoN)
  1610           else
  1611             (false, mepoN))
  1612 
  1613       val unique_facts = drop_duplicate_facts facts
  1614       val add_ths = Attrib.eval_thms ctxt add
  1615 
  1616       fun in_add (_, th) = member Thm.eq_thm_prop add_ths th
  1617 
  1618       fun add_and_take accepts =
  1619         (case add_ths of
  1620            [] => accepts
  1621          | _ => (unique_facts |> filter in_add |> map fact_of_raw_fact) @
  1622                 (accepts |> filter_out in_add))
  1623         |> take max_facts
  1624 
  1625       fun mepo () =
  1626         (mepo_suggested_facts ctxt params max_facts NONE hyp_ts concl_t unique_facts
  1627          |> weight_facts_steeply, [])
  1628 
  1629       fun mash () =
  1630         mash_suggested_facts ctxt params (generous_max_facts max_facts) hyp_ts concl_t facts
  1631         |>> weight_facts_steeply
  1632 
  1633       val mess =
  1634         (* the order is important for the "case" expression below *)
  1635         [] |> effective_fact_filter <> mepoN ? cons (mash_weight, mash)
  1636            |> effective_fact_filter <> mashN ? cons (mepo_weight, mepo)
  1637            |> Par_List.map (apsnd (fn f => f ()))
  1638       val mesh = mesh_facts (eq_snd Thm.eq_thm_prop) max_facts mess |> add_and_take
  1639     in
  1640       if the_mash_engine () = MaSh_Py andalso save then MaSh_Py.save ctxt overlord else ();
  1641       (case (fact_filter, mess) of
  1642         (NONE, [(_, (mepo, _)), (_, (mash, _))]) =>
  1643         [(meshN, mesh), (mepoN, mepo |> map fst |> add_and_take),
  1644          (mashN, mash |> map fst |> add_and_take)]
  1645       | _ => [(effective_fact_filter, mesh)])
  1646     end
  1647 
  1648 fun kill_learners ctxt ({overlord, ...} : params) =
  1649   (Async_Manager.kill_threads MaShN "learner";
  1650    if the_mash_engine () = MaSh_Py then MaSh_Py.shutdown ctxt overlord else ())
  1651 
  1652 fun running_learners () = Async_Manager.running_threads MaShN "learner"
  1653 
  1654 end;