src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
author blanchet
Thu Jan 31 17:54:05 2013 +0100 (2013-01-31)
changeset 51003 198cb05fb35b
parent 51001 461fdbbdb912
child 51004 5f2788c38127
permissions -rw-r--r--
report (MeSh, MePo, MaSh) triple, to be able to use different filters in different slices
     1 (*  Title:      HOL/Tools/Sledgehammer/sledgehammer_mash.ML
     2     Author:     Jasmin Blanchette, TU Muenchen
     3 
     4 Sledgehammer's machine-learning-based relevance filter (MaSh).
     5 *)
     6 
     7 signature SLEDGEHAMMER_MASH =
     8 sig
     9   type stature = ATP_Problem_Generate.stature
    10   type fact = Sledgehammer_Fact.fact
    11   type fact_override = Sledgehammer_Fact.fact_override
    12   type params = Sledgehammer_Provers.params
    13   type relevance_fudge = Sledgehammer_Provers.relevance_fudge
    14   type prover_result = Sledgehammer_Provers.prover_result
    15 
    16   val trace : bool Config.T
    17   val MaShN : string
    18   val mepoN : string
    19   val mashN : string
    20   val meshN : string
    21   val unlearnN : string
    22   val learn_isarN : string
    23   val learn_proverN : string
    24   val relearn_isarN : string
    25   val relearn_proverN : string
    26   val fact_filters : string list
    27   val encode_str : string -> string
    28   val encode_strs : string list -> string
    29   val unencode_str : string -> string
    30   val unencode_strs : string -> string list
    31   val encode_features : (string * real) list -> string
    32   val extract_suggestions : string -> string * string list
    33 
    34   structure MaSh:
    35   sig
    36     val unlearn : Proof.context -> unit
    37     val learn :
    38       Proof.context -> bool
    39       -> (string * string list * (string * real) list * string list) list -> unit
    40     val relearn :
    41       Proof.context -> bool -> (string * string list) list -> unit
    42     val query :
    43       Proof.context -> bool -> bool -> int
    44       -> string list * (string * real) list * string list -> string list
    45   end
    46 
    47   val mash_unlearn : Proof.context -> unit
    48   val nickname_of_thm : thm -> string
    49   val find_suggested_facts : ('b * thm) list -> string list -> ('b * thm) list
    50   val mesh_facts :
    51     ('a * 'a -> bool) -> int -> (real * (('a * real) list * 'a list)) list
    52     -> 'a list
    53   val theory_ord : theory * theory -> order
    54   val thm_ord : thm * thm -> order
    55   val goal_of_thm : theory -> thm -> thm
    56   val run_prover_for_mash :
    57     Proof.context -> params -> string -> fact list -> thm -> prover_result
    58   val features_of :
    59     Proof.context -> string -> theory -> stature -> term list
    60     -> (string * real) list
    61   val trim_dependencies : thm -> string list -> string list option
    62   val isar_dependencies_of :
    63     string Symtab.table * string Symtab.table -> thm -> string list
    64   val prover_dependencies_of :
    65     Proof.context -> params -> string -> int -> fact list
    66     -> string Symtab.table * string Symtab.table -> thm
    67     -> bool * string list
    68   val weight_mepo_facts : 'a list -> ('a * real) list
    69   val weight_mash_facts : 'a list -> ('a * real) list
    70   val find_mash_suggestions :
    71     int -> string list -> ('b * thm) list -> ('b * thm) list -> ('b * thm) list
    72     -> ('b * thm) list * ('b * thm) list
    73   val mash_suggested_facts :
    74     Proof.context -> params -> string -> int -> term list -> term -> fact list
    75     -> fact list * fact list
    76   val mash_learn_proof :
    77     Proof.context -> params -> string -> term -> ('a * thm) list -> thm list
    78     -> unit
    79   val mash_learn :
    80     Proof.context -> params -> fact_override -> thm list -> bool -> unit
    81   val is_mash_enabled : unit -> bool
    82   val mash_can_suggest_facts : Proof.context -> bool
    83   val generous_max_facts : int -> int
    84   val mepo_weight : real
    85   val mash_weight : real
    86   val relevant_facts :
    87     Proof.context -> params -> string -> int -> fact_override -> term list
    88     -> term -> fact list -> fact list * fact list * fact list
    89   val kill_learners : unit -> unit
    90   val running_learners : unit -> unit
    91 end;
    92 
    93 structure Sledgehammer_MaSh : SLEDGEHAMMER_MASH =
    94 struct
    95 
    96 open ATP_Util
    97 open ATP_Problem_Generate
    98 open Sledgehammer_Util
    99 open Sledgehammer_Fact
   100 open Sledgehammer_Provers
   101 open Sledgehammer_Minimize
   102 open Sledgehammer_MePo
   103 
   104 val trace =
   105   Attrib.setup_config_bool @{binding sledgehammer_mash_trace} (K false)
   106 fun trace_msg ctxt msg = if Config.get ctxt trace then tracing (msg ()) else ()
   107 
   108 val MaShN = "MaSh"
   109 
   110 val mepoN = "mepo"
   111 val mashN = "mash"
   112 val meshN = "mesh"
   113 
   114 val fact_filters = [meshN, mepoN, mashN]
   115 
   116 val unlearnN = "unlearn"
   117 val learn_isarN = "learn_isar"
   118 val learn_proverN = "learn_prover"
   119 val relearn_isarN = "relearn_isar"
   120 val relearn_proverN = "relearn_prover"
   121 
   122 fun mash_model_dir () =
   123   Path.explode "$ISABELLE_HOME_USER/mash" |> tap Isabelle_System.mkdir
   124 val mash_state_dir = mash_model_dir
   125 fun mash_state_file () = Path.append (mash_state_dir ()) (Path.explode "state")
   126 
   127 
   128 (*** Low-level communication with MaSh ***)
   129 
   130 fun wipe_out_file file = (try (File.rm o Path.explode) file; ())
   131 
   132 fun write_file banner (xs, f) path =
   133   (case banner of SOME s => File.write path s | NONE => ();
   134    xs |> chunk_list 500
   135       |> List.app (File.append path o space_implode "" o map f))
   136   handle IO.Io _ => ()
   137 
   138 fun run_mash_tool ctxt overlord save max_suggs write_cmds read_suggs =
   139   let
   140     val (temp_dir, serial) =
   141       if overlord then (getenv "ISABELLE_HOME_USER", "")
   142       else (getenv "ISABELLE_TMP", serial_string ())
   143     val log_file = if overlord then temp_dir ^ "/mash_log" else "/dev/null"
   144     val err_file = temp_dir ^ "/mash_err" ^ serial
   145     val sugg_file = temp_dir ^ "/mash_suggs" ^ serial
   146     val sugg_path = Path.explode sugg_file
   147     val cmd_file = temp_dir ^ "/mash_commands" ^ serial
   148     val cmd_path = Path.explode cmd_file
   149     val model_dir = File.shell_path (mash_model_dir ())
   150     val core =
   151       "--inputFile " ^ cmd_file ^ " --predictions " ^ sugg_file ^
   152       " --numberOfPredictions " ^ string_of_int max_suggs ^
   153       (* " --learnTheories" ^ *) (if save then " --saveModel" else "")
   154     val command =
   155       "\"$ISABELLE_SLEDGEHAMMER_MASH/src/mash.py\" --quiet" ^
   156       " --outputDir " ^ model_dir ^
   157       " --modelFile=" ^ model_dir ^ "/model.pickle" ^
   158       " --dictsFile=" ^ model_dir ^ "/dict.pickle" ^
   159       " --theoryFile=" ^ model_dir ^ "/theory.pickle" ^
   160       " --log " ^ log_file ^ " " ^ core ^
   161       " >& " ^ err_file
   162     fun run_on () =
   163       (Isabelle_System.bash command
   164        |> tap (fn _ => trace_msg ctxt (fn () =>
   165               case try File.read (Path.explode err_file) of
   166                 NONE => "Done"
   167               | SOME "" => "Done"
   168               | SOME s => "Error: " ^ elide_string 1000 s));
   169        read_suggs (fn () => try File.read_lines sugg_path |> these))
   170     fun clean_up () =
   171       if overlord then ()
   172       else List.app wipe_out_file [err_file, sugg_file, cmd_file]
   173   in
   174     write_file (SOME "") ([], K "") sugg_path;
   175     write_file (SOME "") write_cmds cmd_path;
   176     trace_msg ctxt (fn () => "Running " ^ command);
   177     with_cleanup clean_up run_on ()
   178   end
   179 
   180 fun meta_char c =
   181   if Char.isAlphaNum c orelse c = #"_" orelse c = #"." orelse c = #"(" orelse
   182      c = #")" orelse c = #"," then
   183     String.str c
   184   else
   185     (* fixed width, in case more digits follow *)
   186     "%" ^ stringN_of_int 3 (Char.ord c)
   187 
   188 fun unmeta_chars accum [] = String.implode (rev accum)
   189   | unmeta_chars accum (#"%" :: d1 :: d2 :: d3 :: cs) =
   190     (case Int.fromString (String.implode [d1, d2, d3]) of
   191        SOME n => unmeta_chars (Char.chr n :: accum) cs
   192      | NONE => "" (* error *))
   193   | unmeta_chars _ (#"%" :: _) = "" (* error *)
   194   | unmeta_chars accum (c :: cs) = unmeta_chars (c :: accum) cs
   195 
   196 val encode_str = String.translate meta_char
   197 val encode_strs = map encode_str #> space_implode " "
   198 val unencode_str = String.explode #> unmeta_chars []
   199 val unencode_strs =
   200   space_explode " " #> filter_out (curry (op =) "") #> map unencode_str
   201 
   202 fun freshish_name () =
   203   Date.fmt ".%Y%m%d_%H%M%S__" (Date.fromTimeLocal (Time.now ())) ^
   204   serial_string ()
   205 
   206 fun encode_feature (name, weight) =
   207   encode_str name ^
   208   (if Real.== (weight, 1.0) then "" else "=" ^ Real.toString weight)
   209 
   210 val encode_features = map encode_feature #> space_implode " "
   211 
   212 fun str_of_learn (name, parents, feats, deps) =
   213   "! " ^ encode_str name ^ ": " ^ encode_strs parents ^ "; " ^
   214   encode_features feats ^ "; " ^ encode_strs deps ^ "\n"
   215 
   216 fun str_of_relearn (name, deps) =
   217   "p " ^ encode_str name ^ ": " ^ encode_strs deps ^ "\n"
   218 
   219 fun str_of_query learn_hints (parents, feats, hints) =
   220   (if not learn_hints orelse null hints then ""
   221    else str_of_learn (freshish_name (), parents, feats, hints)) ^
   222   "? " ^ encode_strs parents ^ "; " ^ encode_features feats ^
   223   (if learn_hints orelse null hints then "" else "; " ^ encode_strs hints) ^
   224   "\n"
   225 
   226 (* The weights currently returned by "mash.py" are too spaced out to make any
   227    sense. *)
   228 fun extract_suggestion sugg =
   229   case space_explode "=" sugg of
   230     [name, weight] =>
   231     SOME (unencode_str name (* , Real.fromString weight |> the_default 1.0 *))
   232   | [name] => SOME (unencode_str name (* , 1.0 *))
   233   | _ => NONE
   234 
   235 fun extract_suggestions line =
   236   case space_explode ":" line of
   237     [goal, suggs] =>
   238     (unencode_str goal, map_filter extract_suggestion (space_explode " " suggs))
   239   | _ => ("", [])
   240 
   241 structure MaSh =
   242 struct
   243 
   244 fun unlearn ctxt =
   245   let val path = mash_model_dir () in
   246     trace_msg ctxt (K "MaSh unlearn");
   247     try (File.fold_dir (fn file => fn _ =>
   248                            try File.rm (Path.append path (Path.basic file)))
   249                        path) NONE;
   250     ()
   251   end
   252 
   253 fun learn _ _ [] = ()
   254   | learn ctxt overlord learns =
   255     (trace_msg ctxt (fn () => "MaSh learn " ^
   256          elide_string 1000 (space_implode " " (map #1 learns)));
   257      run_mash_tool ctxt overlord true 0 (learns, str_of_learn) (K ()))
   258 
   259 fun relearn _ _ [] = ()
   260   | relearn ctxt overlord relearns =
   261     (trace_msg ctxt (fn () => "MaSh relearn " ^
   262          elide_string 1000 (space_implode " " (map #1 relearns)));
   263      run_mash_tool ctxt overlord true 0 (relearns, str_of_relearn) (K ()))
   264 
   265 fun query ctxt overlord learn_hints max_suggs (query as (_, feats, hints)) =
   266   (trace_msg ctxt (fn () => "MaSh query " ^ encode_features feats);
   267    run_mash_tool ctxt overlord (learn_hints andalso not (null hints))
   268        max_suggs ([query], str_of_query learn_hints)
   269        (fn suggs =>
   270            case suggs () of
   271              [] => []
   272            | suggs => snd (extract_suggestions (List.last suggs)))
   273    handle List.Empty => [])
   274 
   275 end;
   276 
   277 
   278 (*** Middle-level communication with MaSh ***)
   279 
   280 datatype proof_kind =
   281   Isar_Proof | Automatic_Proof | Isar_Proof_wegen_Prover_Flop
   282 
   283 fun str_of_proof_kind Isar_Proof = "i"
   284   | str_of_proof_kind Automatic_Proof = "a"
   285   | str_of_proof_kind Isar_Proof_wegen_Prover_Flop = "x"
   286 
   287 fun proof_kind_of_str "i" = Isar_Proof
   288   | proof_kind_of_str "a" = Automatic_Proof
   289   | proof_kind_of_str "x" = Isar_Proof_wegen_Prover_Flop
   290 
   291 (* FIXME: Here a "Graph.update_node" function would be useful *)
   292 fun update_access_graph_node (name, kind) =
   293   Graph.default_node (name, Isar_Proof)
   294   #> kind <> Isar_Proof ? Graph.map_node name (K kind)
   295 
   296 fun try_graph ctxt when def f =
   297   f ()
   298   handle Graph.CYCLES (cycle :: _) =>
   299          (trace_msg ctxt (fn () =>
   300               "Cycle involving " ^ commas cycle ^ " when " ^ when); def)
   301        | Graph.DUP name =>
   302          (trace_msg ctxt (fn () =>
   303               "Duplicate fact " ^ quote name ^ " when " ^ when); def)
   304        | Graph.UNDEF name =>
   305          (trace_msg ctxt (fn () =>
   306               "Unknown fact " ^ quote name ^ " when " ^ when); def)
   307        | exn =>
   308          if Exn.is_interrupt exn then
   309            reraise exn
   310          else
   311            (trace_msg ctxt (fn () =>
   312                 "Internal error when " ^ when ^ ":\n" ^
   313                 ML_Compiler.exn_message exn); def)
   314 
   315 fun graph_info G =
   316   string_of_int (length (Graph.keys G)) ^ " node(s), " ^
   317   string_of_int (fold (Integer.add o length o snd) (Graph.dest G) 0) ^
   318   " edge(s), " ^
   319   string_of_int (length (Graph.minimals G)) ^ " minimal, " ^
   320   string_of_int (length (Graph.maximals G)) ^ " maximal"
   321 
   322 type mash_state = {access_G : unit Graph.T, dirty : string list option}
   323 
   324 val empty_state = {access_G = Graph.empty, dirty = SOME []}
   325 
   326 local
   327 
   328 val version = "*** MaSh version 20130113a ***"
   329 
   330 exception Too_New of unit
   331 
   332 fun extract_node line =
   333   case space_explode ":" line of
   334     [head, parents] =>
   335     (case space_explode " " head of
   336        [kind, name] =>
   337        SOME (unencode_str name, unencode_strs parents,
   338              try proof_kind_of_str kind |> the_default Isar_Proof)
   339      | _ => NONE)
   340   | _ => NONE
   341 
   342 fun load _ (state as (true, _)) = state
   343   | load ctxt _ =
   344     let val path = mash_state_file () in
   345       (true,
   346        case try File.read_lines path of
   347          SOME (version' :: node_lines) =>
   348          let
   349            fun add_edge_to name parent =
   350              Graph.default_node (parent, Isar_Proof)
   351              #> Graph.add_edge (parent, name)
   352            fun add_node line =
   353              case extract_node line of
   354                NONE => I (* shouldn't happen *)
   355              | SOME (name, parents, kind) =>
   356                update_access_graph_node (name, kind)
   357                #> fold (add_edge_to name) parents
   358            val access_G =
   359              case string_ord (version', version) of
   360                EQUAL =>
   361                try_graph ctxt "loading state" Graph.empty (fn () =>
   362                    fold add_node node_lines Graph.empty)
   363              | LESS =>
   364                (MaSh.unlearn ctxt; Graph.empty) (* can't parse old file *)
   365              | GREATER => raise Too_New ()
   366          in
   367            trace_msg ctxt (fn () =>
   368                "Loaded fact graph (" ^ graph_info access_G ^ ")");
   369            {access_G = access_G, dirty = SOME []}
   370          end
   371        | _ => empty_state)
   372     end
   373 
   374 fun save _ (state as {dirty = SOME [], ...}) = state
   375   | save ctxt {access_G, dirty} =
   376     let
   377       fun str_of_entry (name, parents, kind) =
   378         str_of_proof_kind kind ^ " " ^ encode_str name ^ ": " ^
   379         encode_strs parents ^ "\n"
   380       fun append_entry (name, (kind, (parents, _))) =
   381         cons (name, Graph.Keys.dest parents, kind)
   382       val (banner, entries) =
   383         case dirty of
   384           SOME names =>
   385           (NONE, fold (append_entry o Graph.get_entry access_G) names [])
   386         | NONE => (SOME (version ^ "\n"), Graph.fold append_entry access_G [])
   387     in
   388       write_file banner (entries, str_of_entry) (mash_state_file ());
   389       trace_msg ctxt (fn () =>
   390           "Saved fact graph (" ^ graph_info access_G ^
   391           (case dirty of
   392              SOME dirty =>
   393              "; " ^ string_of_int (length dirty) ^ " dirty fact(s)"
   394            | _ => "") ^  ")");
   395       {access_G = access_G, dirty = SOME []}
   396     end
   397 
   398 val global_state =
   399   Synchronized.var "Sledgehammer_MaSh.global_state" (false, empty_state)
   400 
   401 in
   402 
   403 fun map_state ctxt f =
   404   Synchronized.change global_state (load ctxt ##> (f #> save ctxt))
   405   handle Too_New () => ()
   406 
   407 fun peek_state ctxt f =
   408   Synchronized.change_result global_state
   409       (perhaps (try (load ctxt)) #> `snd #>> f)
   410 
   411 fun clear_state ctxt =
   412   Synchronized.change global_state (fn _ =>
   413       (MaSh.unlearn ctxt; (* also removes the state file *)
   414        (true, empty_state)))
   415 
   416 end
   417 
   418 val mash_unlearn = clear_state
   419 
   420 
   421 (*** Isabelle helpers ***)
   422 
   423 val local_prefix = "local" ^ Long_Name.separator
   424 
   425 fun elided_backquote_thm threshold th =
   426   elide_string threshold
   427     (backquote_thm (Proof_Context.init_global (Thm.theory_of_thm th)) th)
   428 
   429 fun nickname_of_thm th =
   430   if Thm.has_name_hint th then
   431     let val hint = Thm.get_name_hint th in
   432       (* There must be a better way to detect local facts. *)
   433       case try (unprefix local_prefix) hint of
   434         SOME suf =>
   435         Context.theory_name (Thm.theory_of_thm th) ^ Long_Name.separator ^ suf ^
   436         Long_Name.separator ^ elided_backquote_thm 50 th
   437       | NONE => hint
   438     end
   439   else
   440     elided_backquote_thm 200 th
   441 
   442 fun find_suggested_facts facts =
   443   let
   444     fun add_fact (fact as (_, th)) = Symtab.default (nickname_of_thm th, fact)
   445     val tab = fold add_fact facts Symtab.empty
   446   in map_filter (Symtab.lookup tab) end
   447 
   448 fun scaled_avg [] = 0
   449   | scaled_avg xs =
   450     Real.ceil (100000000.0 * fold (curry (op +)) xs 0.0) div length xs
   451 
   452 fun avg [] = 0.0
   453   | avg xs = fold (curry (op +)) xs 0.0 / Real.fromInt (length xs)
   454 
   455 fun normalize_scores _ [] = []
   456   | normalize_scores max_facts xs =
   457     let val avg = avg (map snd (take max_facts xs)) in
   458       map (apsnd (curry Real.* (1.0 / avg))) xs
   459     end
   460 
   461 fun mesh_facts _ max_facts [(_, (sels, unks))] =
   462     map fst (take max_facts sels) @ take (max_facts - length sels) unks
   463   | mesh_facts fact_eq max_facts mess =
   464     let
   465       val mess =
   466         mess |> map (apsnd (apfst (normalize_scores max_facts #> `length)))
   467       fun score_in fact (global_weight, ((sel_len, sels), unks)) =
   468         let
   469           fun score_at j =
   470             case try (nth sels) j of
   471               SOME (_, score) => SOME (global_weight * score)
   472             | NONE => NONE
   473         in
   474           case find_index (curry fact_eq fact o fst) sels of
   475             ~1 => (case find_index (curry fact_eq fact) unks of
   476                      ~1 => SOME 0.0
   477                    | _ => NONE)
   478           | rank => score_at rank
   479         end
   480       fun weight_of fact = mess |> map_filter (score_in fact) |> scaled_avg
   481       val facts =
   482         fold (union fact_eq o map fst o take max_facts o snd o fst o snd) mess
   483              []
   484     in
   485       facts |> map (`weight_of) |> sort (int_ord o swap o pairself fst)
   486             |> map snd |> take max_facts
   487     end
   488 
   489 fun thy_feature_of s = ("y" ^ s, 8.0 (* FUDGE *))
   490 fun const_feature_of s = ("c" ^ s, 32.0 (* FUDGE *))
   491 fun free_feature_of s = ("f" ^ s, 40.0 (* FUDGE *))
   492 fun type_feature_of s = ("t" ^ s, 4.0 (* FUDGE *))
   493 fun class_feature_of s = ("s" ^ s, 1.0 (* FUDGE *))
   494 fun status_feature_of status = (string_of_status status, 2.0 (* FUDGE *))
   495 val local_feature = ("local", 8.0 (* FUDGE *))
   496 val lams_feature = ("lams", 2.0 (* FUDGE *))
   497 val skos_feature = ("skos", 2.0 (* FUDGE *))
   498 
   499 fun theory_ord p =
   500   if Theory.subthy p then
   501     if Theory.eq_thy p then EQUAL else LESS
   502   else if Theory.subthy (swap p) then
   503     GREATER
   504   else case int_ord (pairself (length o Theory.ancestors_of) p) of
   505     EQUAL => string_ord (pairself Context.theory_name p)
   506   | order => order
   507 
   508 fun thm_ord p =
   509   case theory_ord (pairself theory_of_thm p) of
   510     EQUAL =>
   511     let val q = pairself nickname_of_thm p in
   512       (* Hack to put "xxx_def" before "xxxI" and "xxxE" *)
   513       case bool_ord (pairself (String.isSuffix "_def") (swap q)) of
   514         EQUAL => string_ord q
   515       | ord => ord
   516     end
   517   | ord => ord
   518 
   519 val freezeT = Type.legacy_freeze_type
   520 
   521 fun freeze (t $ u) = freeze t $ freeze u
   522   | freeze (Abs (s, T, t)) = Abs (s, freezeT T, freeze t)
   523   | freeze (Var ((s, _), T)) = Free (s, freezeT T)
   524   | freeze (Const (s, T)) = Const (s, freezeT T)
   525   | freeze (Free (s, T)) = Free (s, freezeT T)
   526   | freeze t = t
   527 
   528 fun goal_of_thm thy = prop_of #> freeze #> cterm_of thy #> Goal.init
   529 
   530 fun run_prover_for_mash ctxt params prover facts goal =
   531   let
   532     val problem =
   533       {state = Proof.init ctxt, goal = goal, subgoal = 1, subgoal_count = 1,
   534        facts = facts |> map (apfst (apfst (fn name => name ())))
   535                      |> map Untranslated_Fact}
   536   in
   537     get_minimizing_isar_prover ctxt MaSh (K (K ())) prover params (K (K (K "")))
   538                                problem
   539   end
   540 
   541 val bad_types = [@{type_name prop}, @{type_name bool}, @{type_name fun}]
   542 
   543 val logical_consts =
   544   [@{const_name prop}, @{const_name Pure.conjunction}] @ atp_logical_consts
   545 
   546 val max_pattern_breadth = 10
   547 
   548 fun term_features_of ctxt prover thy_name term_max_depth type_max_depth ts =
   549   let
   550     val thy = Proof_Context.theory_of ctxt
   551     fun is_built_in (x as (s, _)) args =
   552       if member (op =) logical_consts s then (true, args)
   553       else is_built_in_const_for_prover ctxt prover x args
   554     val fixes = map snd (Variable.dest_fixes ctxt)
   555     val classes = Sign.classes_of thy
   556     fun add_classes @{sort type} = I
   557       | add_classes S =
   558         fold (`(Sorts.super_classes classes)
   559               #> swap #> op ::
   560               #> subtract (op =) @{sort type}
   561               #> map class_feature_of
   562               #> union (op = o pairself fst)) S
   563     fun do_add_type (Type (s, Ts)) =
   564         (not (member (op =) bad_types s)
   565          ? insert (op = o pairself fst) (type_feature_of s))
   566         #> fold do_add_type Ts
   567       | do_add_type (TFree (_, S)) = add_classes S
   568       | do_add_type (TVar (_, S)) = add_classes S
   569     fun add_type T = type_max_depth >= 0 ? do_add_type T
   570     fun patternify_term _ 0 _ = []
   571       | patternify_term args _ (Const (x as (s, _))) =
   572         if fst (is_built_in x args) then [] else [s]
   573       | patternify_term _ depth (Free (s, _)) =
   574         if depth = term_max_depth andalso member (op =) fixes s then
   575           [thy_name ^ Long_Name.separator ^ s]
   576         else
   577           []
   578       | patternify_term args depth (t $ u) =
   579         let
   580           val ps =
   581             take max_pattern_breadth (patternify_term (u :: args) depth t)
   582           val qs =
   583             take max_pattern_breadth ("" :: patternify_term [] (depth - 1) u)
   584         in map_product (fn p => fn "" => p | q => p ^ "(" ^ q ^ ")") ps qs end
   585       | patternify_term _ _ _ = []
   586     fun add_term_pattern feature_of =
   587       union (op = o pairself fst) o map feature_of oo patternify_term []
   588     fun add_term_patterns _ 0 _ = I
   589       | add_term_patterns feature_of depth t =
   590         add_term_pattern feature_of depth t
   591         #> add_term_patterns feature_of (depth - 1) t
   592     fun add_term feature_of = add_term_patterns feature_of term_max_depth
   593     fun add_patterns t =
   594       case strip_comb t of
   595         (Const (x as (_, T)), args) =>
   596         let val (built_in, args) = is_built_in x args in
   597           (not built_in ? add_term const_feature_of t)
   598           #> add_type T
   599           #> fold add_patterns args
   600         end
   601       | (head, args) =>
   602         (case head of
   603            Const (_, T) => add_term const_feature_of t #> add_type T
   604          | Free (_, T) => add_term free_feature_of t #> add_type T
   605          | Var (_, T) => add_type T
   606          | Abs (_, T, body) => add_type T #> add_patterns body
   607          | _ => I)
   608         #> fold add_patterns args
   609   in [] |> fold add_patterns ts end
   610 
   611 fun is_exists (s, _) = (s = @{const_name Ex} orelse s = @{const_name Ex1})
   612 
   613 val term_max_depth = 2
   614 val type_max_depth = 2
   615 
   616 (* TODO: Generate type classes for types? *)
   617 fun features_of ctxt prover thy (scope, status) ts =
   618   let val thy_name = Context.theory_name thy in
   619     thy_feature_of thy_name ::
   620     term_features_of ctxt prover thy_name term_max_depth type_max_depth ts
   621     |> status <> General ? cons (status_feature_of status)
   622     |> scope <> Global ? cons local_feature
   623     |> exists (not o is_lambda_free) ts ? cons lams_feature
   624     |> exists (exists_Const is_exists) ts ? cons skos_feature
   625   end
   626 
   627 (* Too many dependencies is a sign that a decision procedure is at work. There
   628    isn't much to learn from such proofs. *)
   629 val max_dependencies = 20
   630 
   631 val prover_dependency_default_max_facts = 50
   632 
   633 (* "type_definition_xxx" facts are characterized by their use of "CollectI". *)
   634 val typedef_dep = nickname_of_thm @{thm CollectI}
   635 (* Mysterious parts of the class machinery create lots of proofs that refer
   636    exclusively to "someI_e" (and to some internal constructions). *)
   637 val class_some_dep = nickname_of_thm @{thm someI_ex}
   638 
   639 val fundef_ths =
   640   @{thms fundef_ex1_existence fundef_ex1_uniqueness fundef_ex1_iff
   641          fundef_default_value}
   642   |> map nickname_of_thm
   643 
   644 (* "Rep_xxx_inject", "Abs_xxx_inverse", etc., are derived using these facts. *)
   645 val typedef_ths =
   646   @{thms type_definition.Abs_inverse type_definition.Rep_inverse
   647          type_definition.Rep type_definition.Rep_inject
   648          type_definition.Abs_inject type_definition.Rep_cases
   649          type_definition.Abs_cases type_definition.Rep_induct
   650          type_definition.Abs_induct type_definition.Rep_range
   651          type_definition.Abs_image}
   652   |> map nickname_of_thm
   653 
   654 fun is_size_def [dep] th =
   655     (case first_field ".recs" dep of
   656        SOME (pref, _) =>
   657        (case first_field ".size" (nickname_of_thm th) of
   658           SOME (pref', _) => pref = pref'
   659         | NONE => false)
   660      | NONE => false)
   661   | is_size_def _ _ = false
   662 
   663 fun trim_dependencies th deps =
   664   if length deps > max_dependencies then NONE else SOME deps
   665 
   666 fun isar_dependencies_of name_tabs th =
   667   let
   668     val deps = thms_in_proof (SOME name_tabs) th
   669   in
   670     if deps = [typedef_dep] orelse
   671        deps = [class_some_dep] orelse
   672        exists (member (op =) fundef_ths) deps orelse
   673        exists (member (op =) typedef_ths) deps orelse
   674        is_size_def deps th then
   675       []
   676     else
   677       deps
   678   end
   679 
   680 fun prover_dependencies_of ctxt (params as {verbose, max_facts, ...}) prover
   681                            auto_level facts name_tabs th =
   682   case isar_dependencies_of name_tabs th of
   683     [] => (false, [])
   684   | isar_deps =>
   685     let
   686       val thy = Proof_Context.theory_of ctxt
   687       val goal = goal_of_thm thy th
   688       val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal 1
   689       val facts = facts |> filter (fn (_, th') => thm_ord (th', th) = LESS)
   690       fun nickify ((_, stature), th) =
   691         ((fn () => nickname_of_thm th, stature), th)
   692       fun is_dep dep (_, th) = nickname_of_thm th = dep
   693       fun add_isar_dep facts dep accum =
   694         if exists (is_dep dep) accum then
   695           accum
   696         else case find_first (is_dep dep) facts of
   697           SOME ((name, status), th) => accum @ [((name, status), th)]
   698         | NONE => accum (* shouldn't happen *)
   699       val facts =
   700         facts
   701         |> mepo_suggested_facts ctxt params prover
   702                (max_facts |> the_default prover_dependency_default_max_facts)
   703                NONE hyp_ts concl_t
   704         |> fold (add_isar_dep facts) isar_deps
   705         |> map nickify
   706     in
   707       if verbose andalso auto_level = 0 then
   708         let val num_facts = length facts in
   709           "MaSh: " ^ quote prover ^ " on " ^ quote (nickname_of_thm th) ^
   710           " with " ^ string_of_int num_facts ^ " fact" ^ plural_s num_facts ^
   711           "."
   712           |> Output.urgent_message
   713         end
   714       else
   715         ();
   716       case run_prover_for_mash ctxt params prover facts goal of
   717         {outcome = NONE, used_facts, ...} =>
   718         (if verbose andalso auto_level = 0 then
   719            let val num_facts = length used_facts in
   720              "Found proof with " ^ string_of_int num_facts ^ " fact" ^
   721              plural_s num_facts ^ "."
   722              |> Output.urgent_message
   723            end
   724          else
   725            ();
   726          (true, map fst used_facts))
   727       | _ => (false, isar_deps)
   728     end
   729 
   730 
   731 (*** High-level communication with MaSh ***)
   732 
   733 fun num_keys keys = Graph.Keys.fold (K (Integer.add 1)) keys 0
   734 
   735 fun maximal_in_graph access_G facts =
   736   let
   737     val facts = [] |> fold (cons o nickname_of_thm o snd) facts
   738     val tab = Symtab.empty |> fold (fn name => Symtab.default (name, ())) facts
   739     fun insert_new seen name =
   740       not (Symtab.defined seen name) ? insert (op =) name
   741     fun find_maxes _ (maxs, []) = map snd maxs
   742       | find_maxes seen (maxs, new :: news) =
   743         find_maxes
   744             (seen |> num_keys (Graph.imm_succs access_G new) > 1
   745                      ? Symtab.default (new, ()))
   746             (if Symtab.defined tab new then
   747                let
   748                  val newp = Graph.all_preds access_G [new]
   749                  fun is_ancestor x yp = member (op =) yp x
   750                  val maxs =
   751                    maxs |> filter (fn (_, max) => not (is_ancestor max newp))
   752                in
   753                  if exists (is_ancestor new o fst) maxs then
   754                    (maxs, news)
   755                  else
   756                    ((newp, new)
   757                     :: filter_out (fn (_, max) => is_ancestor max newp) maxs,
   758                     news)
   759                end
   760              else
   761                (maxs, Graph.Keys.fold (insert_new seen)
   762                                       (Graph.imm_preds access_G new) news))
   763   in find_maxes Symtab.empty ([], Graph.maximals access_G) end
   764 
   765 fun is_fact_in_graph access_G get_th fact =
   766   can (Graph.get_node access_G) (nickname_of_thm (get_th fact))
   767 
   768 (* FUDGE *)
   769 fun weight_of_mepo_fact rank =
   770   Math.pow (0.62, log2 (Real.fromInt (rank + 1)))
   771 
   772 fun weight_mepo_facts facts =
   773   facts ~~ map weight_of_mepo_fact (0 upto length facts - 1)
   774 
   775 val weight_raw_mash_facts = weight_mepo_facts
   776 val weight_mash_facts = weight_raw_mash_facts
   777 
   778 (* FUDGE *)
   779 fun weight_of_proximity_fact rank =
   780   Math.pow (1.3, 15.5 - 0.2 * Real.fromInt rank) + 15.0
   781 
   782 fun weight_proximity_facts facts =
   783   facts ~~ map weight_of_proximity_fact (0 upto length facts - 1)
   784 
   785 val max_proximity_facts = 100
   786 
   787 fun find_mash_suggestions _ [] _ _ raw_unknown = ([], raw_unknown)
   788   | find_mash_suggestions max_facts suggs facts chained raw_unknown =
   789     let
   790       val raw_mash = find_suggested_facts facts suggs
   791       val unknown_chained =
   792         inter (Thm.eq_thm_prop o pairself snd) chained raw_unknown
   793       val proximity =
   794         facts |> sort (thm_ord o pairself snd o swap)
   795               |> take max_proximity_facts
   796       val mess =
   797         [(0.90 (* FUDGE *), (map (rpair 1.0) unknown_chained, [])),
   798          (0.08 (* FUDGE *), (weight_raw_mash_facts raw_mash, raw_unknown)),
   799          (0.02 (* FUDGE *), (weight_proximity_facts proximity, []))]
   800       val unknown =
   801         raw_unknown
   802         |> fold (subtract (Thm.eq_thm_prop o pairself snd))
   803                 [unknown_chained, proximity]
   804     in (mesh_facts (Thm.eq_thm_prop o pairself snd) max_facts mess, unknown) end
   805 
   806 fun mash_suggested_facts ctxt ({overlord, learn, ...} : params) prover max_facts
   807                          hyp_ts concl_t facts =
   808   let
   809     val thy = Proof_Context.theory_of ctxt
   810     val chained = facts |> filter (fn ((_, (scope, _)), _) => scope = Chained)
   811     val (access_G, suggs) =
   812       peek_state ctxt (fn {access_G, ...} =>
   813           if Graph.is_empty access_G then
   814             (access_G, [])
   815           else
   816             let
   817               val parents = maximal_in_graph access_G facts
   818               val feats =
   819                 features_of ctxt prover thy (Local, General) (concl_t :: hyp_ts)
   820               val hints =
   821                 chained |> filter (is_fact_in_graph access_G snd)
   822                         |> map (nickname_of_thm o snd)
   823             in
   824               (access_G, MaSh.query ctxt overlord learn max_facts
   825                                     (parents, feats, hints))
   826             end)
   827     val unknown = facts |> filter_out (is_fact_in_graph access_G snd)
   828   in find_mash_suggestions max_facts suggs facts chained unknown end
   829 
   830 fun learn_wrt_access_graph ctxt (name, parents, feats, deps) (learns, graph) =
   831   let
   832     fun maybe_learn_from from (accum as (parents, graph)) =
   833       try_graph ctxt "updating graph" accum (fn () =>
   834           (from :: parents, Graph.add_edge_acyclic (from, name) graph))
   835     val graph = graph |> Graph.default_node (name, Isar_Proof)
   836     val (parents, graph) = ([], graph) |> fold maybe_learn_from parents
   837     val (deps, _) = ([], graph) |> fold maybe_learn_from deps
   838   in ((name, parents, feats, deps) :: learns, graph) end
   839 
   840 fun relearn_wrt_access_graph ctxt (name, deps) (relearns, graph) =
   841   let
   842     fun maybe_relearn_from from (accum as (parents, graph)) =
   843       try_graph ctxt "updating graph" accum (fn () =>
   844           (from :: parents, Graph.add_edge_acyclic (from, name) graph))
   845     val graph = graph |> update_access_graph_node (name, Automatic_Proof)
   846     val (deps, _) = ([], graph) |> fold maybe_relearn_from deps
   847   in ((name, deps) :: relearns, graph) end
   848 
   849 fun flop_wrt_access_graph name =
   850   update_access_graph_node (name, Isar_Proof_wegen_Prover_Flop)
   851 
   852 val learn_timeout_slack = 2.0
   853 
   854 fun launch_thread timeout task =
   855   let
   856     val hard_timeout = time_mult learn_timeout_slack timeout
   857     val birth_time = Time.now ()
   858     val death_time = Time.+ (birth_time, hard_timeout)
   859     val desc = ("Machine learner for Sledgehammer", "")
   860   in Async_Manager.launch MaShN birth_time death_time desc task end
   861 
   862 fun mash_learn_proof ctxt ({overlord, timeout, ...} : params) prover t facts
   863                      used_ths =
   864   launch_thread (timeout |> the_default one_day) (fn () =>
   865       let
   866         val thy = Proof_Context.theory_of ctxt
   867         val name = freshish_name ()
   868         val feats = features_of ctxt prover thy (Local, General) [t]
   869       in
   870         peek_state ctxt (fn {access_G, ...} =>
   871             let
   872               val parents = maximal_in_graph access_G facts
   873               val deps =
   874                 used_ths |> filter (is_fact_in_graph access_G I)
   875                          |> map nickname_of_thm
   876             in
   877               MaSh.learn ctxt overlord [(name, parents, feats, deps)]
   878             end);
   879         (true, "")
   880       end)
   881 
   882 fun sendback sub = Active.sendback_markup (sledgehammerN ^ " " ^ sub)
   883 
   884 val commit_timeout = seconds 30.0
   885 
   886 (* The timeout is understood in a very relaxed fashion. *)
   887 fun mash_learn_facts ctxt (params as {debug, verbose, overlord, ...}) prover
   888                      auto_level run_prover learn_timeout facts =
   889   let
   890     val timer = Timer.startRealTimer ()
   891     fun next_commit_time () =
   892       Time.+ (Timer.checkRealTimer timer, commit_timeout)
   893     val {access_G, ...} = peek_state ctxt I
   894     val facts = facts |> sort (thm_ord o pairself snd)
   895     val (old_facts, new_facts) =
   896       facts |> List.partition (is_fact_in_graph access_G snd)
   897   in
   898     if null new_facts andalso (not run_prover orelse null old_facts) then
   899       if auto_level < 2 then
   900         "No new " ^ (if run_prover then "automatic" else "Isar") ^
   901         " proofs to learn." ^
   902         (if auto_level = 0 andalso not run_prover then
   903            "\n\nHint: Try " ^ sendback learn_proverN ^
   904            " to learn from an automatic prover."
   905          else
   906            "")
   907       else
   908         ""
   909     else
   910       let
   911         val name_tabs = build_name_tables nickname_of_thm facts
   912         fun deps_of status th =
   913           if status = Non_Rec_Def orelse status = Rec_Def then
   914             SOME []
   915           else if run_prover then
   916             prover_dependencies_of ctxt params prover auto_level facts name_tabs
   917                                    th
   918             |> (fn (false, _) => NONE
   919                  | (true, deps) => trim_dependencies th deps)
   920           else
   921             isar_dependencies_of name_tabs th
   922             |> trim_dependencies th
   923         fun do_commit [] [] [] state = state
   924           | do_commit learns relearns flops {access_G, dirty} =
   925             let
   926               val was_empty = Graph.is_empty access_G
   927               val (learns, access_G) =
   928                 ([], access_G) |> fold (learn_wrt_access_graph ctxt) learns
   929               val (relearns, access_G) =
   930                 ([], access_G) |> fold (relearn_wrt_access_graph ctxt) relearns
   931               val access_G = access_G |> fold flop_wrt_access_graph flops
   932               val dirty =
   933                 case (was_empty, dirty, relearns) of
   934                   (false, SOME names, []) => SOME (map #1 learns @ names)
   935                 | _ => NONE
   936             in
   937               MaSh.learn ctxt overlord (rev learns);
   938               MaSh.relearn ctxt overlord relearns;
   939               {access_G = access_G, dirty = dirty}
   940             end
   941         fun commit last learns relearns flops =
   942           (if debug andalso auto_level = 0 then
   943              Output.urgent_message "Committing..."
   944            else
   945              ();
   946            map_state ctxt (do_commit (rev learns) relearns flops);
   947            if not last andalso auto_level = 0 then
   948              let val num_proofs = length learns + length relearns in
   949                "Learned " ^ string_of_int num_proofs ^ " " ^
   950                (if run_prover then "automatic" else "Isar") ^ " proof" ^
   951                plural_s num_proofs ^ " in the last " ^
   952                string_from_time commit_timeout ^ "."
   953                |> Output.urgent_message
   954              end
   955            else
   956              ())
   957         fun learn_new_fact _ (accum as (_, (_, _, _, true))) = accum
   958           | learn_new_fact ((_, stature as (_, status)), th)
   959                            (learns, (parents, n, next_commit, _)) =
   960             let
   961               val name = nickname_of_thm th
   962               val feats =
   963                 features_of ctxt prover (theory_of_thm th) stature [prop_of th]
   964               val deps = deps_of status th |> these
   965               val n = n |> not (null deps) ? Integer.add 1
   966               val learns = (name, parents, feats, deps) :: learns
   967               val (learns, next_commit) =
   968                 if Time.> (Timer.checkRealTimer timer, next_commit) then
   969                   (commit false learns [] []; ([], next_commit_time ()))
   970                 else
   971                   (learns, next_commit)
   972               val timed_out =
   973                 case learn_timeout of
   974                   SOME timeout => Time.> (Timer.checkRealTimer timer, timeout)
   975                 | NONE => false
   976             in (learns, ([name], n, next_commit, timed_out)) end
   977         val n =
   978           if null new_facts then
   979             0
   980           else
   981             let
   982               val last_th = new_facts |> List.last |> snd
   983               (* crude approximation *)
   984               val ancestors =
   985                 old_facts
   986                 |> filter (fn (_, th) => thm_ord (th, last_th) <> GREATER)
   987               val parents = maximal_in_graph access_G ancestors
   988               val (learns, (_, n, _, _)) =
   989                 ([], (parents, 0, next_commit_time (), false))
   990                 |> fold learn_new_fact new_facts
   991             in commit true learns [] []; n end
   992         fun relearn_old_fact _ (accum as (_, (_, _, true))) = accum
   993           | relearn_old_fact ((_, (_, status)), th)
   994                              ((relearns, flops), (n, next_commit, _)) =
   995             let
   996               val name = nickname_of_thm th
   997               val (n, relearns, flops) =
   998                 case deps_of status th of
   999                   SOME deps => (n + 1, (name, deps) :: relearns, flops)
  1000                 | NONE => (n, relearns, name :: flops)
  1001               val (relearns, flops, next_commit) =
  1002                 if Time.> (Timer.checkRealTimer timer, next_commit) then
  1003                   (commit false [] relearns flops;
  1004                    ([], [], next_commit_time ()))
  1005                 else
  1006                   (relearns, flops, next_commit)
  1007               val timed_out =
  1008                 case learn_timeout of
  1009                   SOME timeout => Time.> (Timer.checkRealTimer timer, timeout)
  1010                 | NONE => false
  1011             in ((relearns, flops), (n, next_commit, timed_out)) end
  1012         val n =
  1013           if not run_prover orelse null old_facts then
  1014             n
  1015           else
  1016             let
  1017               val max_isar = 1000 * max_dependencies
  1018               fun kind_of_proof th =
  1019                 try (Graph.get_node access_G) (nickname_of_thm th)
  1020                 |> the_default Isar_Proof
  1021               fun priority_of (_, th) =
  1022                 random_range 0 max_isar
  1023                 + (case kind_of_proof th of
  1024                      Isar_Proof => 0
  1025                    | Automatic_Proof => 2 * max_isar
  1026                    | Isar_Proof_wegen_Prover_Flop => max_isar)
  1027                 - 500 * length (isar_dependencies_of name_tabs th)
  1028               val old_facts =
  1029                 old_facts |> map (`priority_of)
  1030                           |> sort (int_ord o pairself fst)
  1031                           |> map snd
  1032               val ((relearns, flops), (n, _, _)) =
  1033                 (([], []), (n, next_commit_time (), false))
  1034                 |> fold relearn_old_fact old_facts
  1035             in commit true [] relearns flops; n end
  1036       in
  1037         if verbose orelse auto_level < 2 then
  1038           "Learned " ^ string_of_int n ^ " nontrivial " ^
  1039           (if run_prover then "automatic" else "Isar") ^ " proof" ^ plural_s n ^
  1040           (if verbose then
  1041              " in " ^ string_from_time (Timer.checkRealTimer timer)
  1042            else
  1043              "") ^ "."
  1044         else
  1045           ""
  1046       end
  1047   end
  1048 
  1049 fun mash_learn ctxt (params as {provers, timeout, ...}) fact_override chained
  1050                run_prover =
  1051   let
  1052     val css = Sledgehammer_Fact.clasimpset_rule_table_of ctxt
  1053     val ctxt = ctxt |> Config.put instantiate_inducts false
  1054     val facts =
  1055       nearly_all_facts ctxt false fact_override Symtab.empty css chained []
  1056                        @{prop True}
  1057     val num_facts = length facts
  1058     val prover = hd provers
  1059     fun learn auto_level run_prover =
  1060       mash_learn_facts ctxt params prover auto_level run_prover NONE facts
  1061       |> Output.urgent_message
  1062   in
  1063     if run_prover then
  1064       ("MaShing through " ^ string_of_int num_facts ^ " fact" ^
  1065        plural_s num_facts ^ " for automatic proofs (" ^ quote prover ^
  1066        (case timeout of
  1067           SOME timeout => " timeout: " ^ string_from_time timeout
  1068         | NONE => "") ^ ").\n\nCollecting Isar proofs first..."
  1069        |> Output.urgent_message;
  1070        learn 1 false;
  1071        "Now collecting automatic proofs. This may take several hours. You can \
  1072        \safely stop the learning process at any point."
  1073        |> Output.urgent_message;
  1074        learn 0 true)
  1075     else
  1076       ("MaShing through " ^ string_of_int num_facts ^ " fact" ^
  1077        plural_s num_facts ^ " for Isar proofs..."
  1078        |> Output.urgent_message;
  1079        learn 0 false)
  1080   end
  1081 
  1082 fun is_mash_enabled () = (getenv "MASH" = "yes")
  1083 fun mash_can_suggest_facts ctxt =
  1084   not (Graph.is_empty (#access_G (peek_state ctxt I)))
  1085 
  1086 (* Generate more suggestions than requested, because some might be thrown out
  1087    later for various reasons. *)
  1088 fun generous_max_facts max_facts = max_facts + Int.min (50, max_facts)
  1089 
  1090 val mepo_weight = 0.5
  1091 val mash_weight = 0.5
  1092 
  1093 (* The threshold should be large enough so that MaSh doesn't kick in for Auto
  1094    Sledgehammer and Try. *)
  1095 val min_secs_for_learning = 15
  1096 
  1097 fun relevant_facts ctxt (params as {learn, fact_filter, timeout, ...}) prover
  1098         max_facts ({add, only, ...} : fact_override) hyp_ts concl_t facts =
  1099   if not (subset (op =) (the_list fact_filter, fact_filters)) then
  1100     error ("Unknown fact filter: " ^ quote (the fact_filter) ^ ".")
  1101   else if only then
  1102     (facts, facts, facts)
  1103   else if max_facts <= 0 orelse null facts then
  1104     ([], [], [])
  1105   else
  1106     let
  1107       fun maybe_learn () =
  1108         if learn andalso not (Async_Manager.has_running_threads MaShN) andalso
  1109            (timeout = NONE orelse
  1110             Time.toSeconds (the timeout) >= min_secs_for_learning) then
  1111           let
  1112             val timeout = Option.map (time_mult learn_timeout_slack) timeout
  1113           in
  1114             launch_thread (timeout |> the_default one_day)
  1115                 (fn () => (true, mash_learn_facts ctxt params prover 2 false
  1116                                                   timeout facts))
  1117           end
  1118         else
  1119           ()
  1120       val fact_filter =
  1121         case fact_filter of
  1122           SOME ff => (() |> ff <> mepoN ? maybe_learn; ff)
  1123         | NONE =>
  1124           if is_smt_prover ctxt prover then
  1125             mepoN
  1126           else if is_mash_enabled () then
  1127             (maybe_learn ();
  1128              if mash_can_suggest_facts ctxt then meshN else mepoN)
  1129           else
  1130             mepoN
  1131       val add_ths = Attrib.eval_thms ctxt add
  1132       val in_add = member Thm.eq_thm_prop add_ths o snd
  1133       fun add_and_take accepts =
  1134         (case add_ths of
  1135            [] => accepts
  1136          | _ => (facts |> filter in_add) @ (accepts |> filter_out in_add))
  1137         |> take max_facts
  1138       fun mepo () =
  1139         mepo_suggested_facts ctxt params prover max_facts NONE hyp_ts concl_t
  1140                              facts
  1141         |> weight_mepo_facts
  1142       fun mash () =
  1143         mash_suggested_facts ctxt params prover (generous_max_facts max_facts)
  1144             hyp_ts concl_t facts
  1145         |>> weight_mash_facts
  1146       val mess =
  1147         (* the order is important for the "case" expression below *)
  1148         [] |> (if fact_filter <> mepoN then cons (mash_weight, (mash ()))
  1149                else I)
  1150            |> (if fact_filter <> mashN then cons (mepo_weight, (mepo (), []))
  1151                else I)
  1152       val mesh =
  1153         mesh_facts (Thm.eq_thm_prop o pairself snd) max_facts mess
  1154         |> add_and_take
  1155     in
  1156       case mess of
  1157         [(_, (mepo, _)), (_, (mash, _))] =>
  1158         (mesh, mepo |> map fst |> add_and_take, mash |> map fst |> add_and_take)
  1159       | _ => (mesh, mesh, mesh)
  1160     end
  1161 
  1162 fun kill_learners () = Async_Manager.kill_threads MaShN "learner"
  1163 fun running_learners () = Async_Manager.running_threads MaShN "learner"
  1164 
  1165 end;