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