store all MaSh data on the Isabelle side, in preparation for replacing 'mash.py' with ML solution
authorblanchet
Mon May 19 23:43:53 2014 +0200 (2014-05-19)
changeset 5700533f3d2ea803d
parent 57004 c8288ce9676a
child 57006 20e5b110d19b
store all MaSh data on the Isabelle side, in preparation for replacing 'mash.py' with ML solution
src/HOL/TPTP/mash_export.ML
src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
     1.1 --- a/src/HOL/TPTP/mash_export.ML	Mon May 19 19:17:15 2014 +0200
     1.2 +++ b/src/HOL/TPTP/mash_export.ML	Mon May 19 23:43:53 2014 +0200
     1.3 @@ -75,7 +75,7 @@
     1.4          val name = nickname_of_thm th
     1.5          val feats =
     1.6            features_of ctxt (theory_of_thm th) 0 Symtab.empty stature false [prop_of th] |> map fst
     1.7 -        val s = encode_str name ^ ": " ^ encode_plain_features (sort_wrt hd feats) ^ "\n"
     1.8 +        val s = encode_str name ^ ": " ^ encode_unweighted_features (sort_wrt hd feats) ^ "\n"
     1.9        in File.append path s end
    1.10    in List.app do_fact facts end
    1.11  
    1.12 @@ -194,8 +194,7 @@
    1.13              |> map fst |> sort_wrt hd
    1.14            val update =
    1.15              "! " ^ encode_str name ^ ": " ^ encode_strs parents ^ "; " ^
    1.16 -            encode_plain_features nongoal_feats ^ "; " ^ marker ^ " " ^
    1.17 -            encode_strs deps ^ "\n"
    1.18 +            encode_unweighted_features nongoal_feats ^ "; " ^ marker ^ " " ^ encode_strs deps ^ "\n"
    1.19          in query ^ update end
    1.20        else
    1.21          ""
     2.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Mon May 19 19:17:15 2014 +0200
     2.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Mon May 19 23:43:53 2014 +0200
     2.3 @@ -28,9 +28,9 @@
     2.4    val fact_filters : string list
     2.5    val encode_str : string -> string
     2.6    val encode_strs : string list -> string
     2.7 -  val unencode_str : string -> string
     2.8 -  val unencode_strs : string -> string list
     2.9 -  val encode_plain_features : string list list -> string
    2.10 +  val decode_str : string -> string
    2.11 +  val decode_strs : string -> string list
    2.12 +  val encode_unweighted_features : string list list -> string
    2.13    val encode_features : (string list * real) list -> string
    2.14    val extract_suggestions : string -> string * string list
    2.15  
    2.16 @@ -110,8 +110,7 @@
    2.17  open Sledgehammer_Prover_Minimize
    2.18  open Sledgehammer_MePo
    2.19  
    2.20 -val trace =
    2.21 -  Attrib.setup_config_bool @{binding sledgehammer_mash_trace} (K false)
    2.22 +val trace = Attrib.setup_config_bool @{binding sledgehammer_mash_trace} (K false)
    2.23  
    2.24  fun trace_msg ctxt msg = if Config.get ctxt trace then tracing (msg ()) else ()
    2.25  
    2.26 @@ -172,8 +171,7 @@
    2.27        \ --log " ^ log_file ^
    2.28        " --inputFile " ^ cmd_file ^
    2.29        " --predictions " ^ sugg_file ^
    2.30 -      (if extra_args = [] then "" else " " ^ space_implode " " extra_args) ^
    2.31 -      " >& " ^ err_file ^
    2.32 +      (if extra_args = [] then "" else " " ^ space_implode " " extra_args) ^ " >& " ^ err_file ^
    2.33        (if background then " &" else "")
    2.34      fun run_on () =
    2.35        (Isabelle_System.bash command
    2.36 @@ -183,8 +181,7 @@
    2.37              | s => warning ("MaSh error: " ^ elide_string 1000 s)));
    2.38         read_suggs (fn () => try File.read_lines sugg_path |> these))
    2.39      fun clean_up () =
    2.40 -      if overlord then ()
    2.41 -      else List.app wipe_out_file [err_file, sugg_file, cmd_file]
    2.42 +      if overlord then () else List.app wipe_out_file [err_file, sugg_file, cmd_file]
    2.43    in
    2.44      write_file (SOME "") ([], K "") sugg_path;
    2.45      write_file (SOME "") write_cmds cmd_path;
    2.46 @@ -203,16 +200,16 @@
    2.47  fun unmeta_chars accum [] = String.implode (rev accum)
    2.48    | unmeta_chars accum (#"%" :: d1 :: d2 :: d3 :: cs) =
    2.49      (case Int.fromString (String.implode [d1, d2, d3]) of
    2.50 -       SOME n => unmeta_chars (Char.chr n :: accum) cs
    2.51 -     | NONE => "" (* error *))
    2.52 +      SOME n => unmeta_chars (Char.chr n :: accum) cs
    2.53 +    | NONE => "" (* error *))
    2.54    | unmeta_chars _ (#"%" :: _) = "" (* error *)
    2.55    | unmeta_chars accum (c :: cs) = unmeta_chars (c :: accum) cs
    2.56  
    2.57  val encode_str = String.translate meta_char
    2.58 +val decode_str = String.explode #> unmeta_chars []
    2.59 +
    2.60  val encode_strs = map encode_str #> space_implode " "
    2.61 -val unencode_str = String.explode #> unmeta_chars []
    2.62 -val unencode_strs =
    2.63 -  space_explode " " #> filter_out (curry (op =) "") #> map unencode_str
    2.64 +val decode_strs = space_explode " " #> filter_out (curry (op =) "") #> map decode_str
    2.65  
    2.66  (* Avoid scientific notation *)
    2.67  fun safe_str_of_real r =
    2.68 @@ -220,38 +217,38 @@
    2.69    else if r >= 1000000.0 then "1000000"
    2.70    else Markup.print_real r
    2.71  
    2.72 -val encode_plain_feature = space_implode "|" o map encode_str
    2.73 +val encode_unweighted_feature = map encode_str #> space_implode "|"
    2.74 +val decode_unweighted_feature = space_explode "|" #> map decode_str
    2.75  
    2.76  fun encode_feature (names, weight) =
    2.77 -  encode_plain_feature names ^ (if Real.== (weight, 1.0) then "" else "=" ^ safe_str_of_real weight)
    2.78 +  encode_unweighted_feature names ^ (if Real.== (weight, 1.0) then "" else "=" ^ safe_str_of_real weight)
    2.79  
    2.80 -val encode_plain_features = map encode_plain_feature #> space_implode " "
    2.81 +val encode_unweighted_features = map encode_unweighted_feature #> space_implode " "
    2.82 +val decode_unweighted_features = space_explode " " #> map decode_unweighted_feature
    2.83 +
    2.84  val encode_features = map encode_feature #> space_implode " "
    2.85  
    2.86 -fun str_of_learn (name, parents, feats : string list list, deps) =
    2.87 +fun str_of_learn (name, parents, feats, deps) =
    2.88    "! " ^ encode_str name ^ ": " ^ encode_strs parents ^ "; " ^
    2.89 -  encode_plain_features feats ^ "; " ^ encode_strs deps ^ "\n"
    2.90 +  encode_unweighted_features feats ^ "; " ^ encode_strs deps ^ "\n"
    2.91  
    2.92 -fun str_of_relearn (name, deps) =
    2.93 -  "p " ^ encode_str name ^ ": " ^ encode_strs deps ^ "\n"
    2.94 +fun str_of_relearn (name, deps) = "p " ^ encode_str name ^ ": " ^ encode_strs deps ^ "\n"
    2.95  
    2.96  fun str_of_query max_suggs (learns, hints, parents, feats) =
    2.97    implode (map str_of_learn learns) ^
    2.98 -  "? " ^ string_of_int max_suggs ^ " # " ^ encode_strs parents ^ "; " ^
    2.99 -  encode_features feats ^
   2.100 +  "? " ^ string_of_int max_suggs ^ " # " ^ encode_strs parents ^ "; " ^ encode_features feats ^
   2.101    (if null hints then "" else "; " ^ encode_strs hints) ^ "\n"
   2.102  
   2.103 -(* The suggested weights don't make much sense. *)
   2.104 +(* The suggested weights do not make much sense. *)
   2.105  fun extract_suggestion sugg =
   2.106    (case space_explode "=" sugg of
   2.107 -    [name, _ (* weight *)] =>
   2.108 -    SOME (unencode_str name (* , Real.fromString weight |> the_default 1.0 *))
   2.109 -  | [name] => SOME (unencode_str name (* , 1.0 *))
   2.110 +    [name, _ (* weight *)] => SOME (decode_str name)
   2.111 +  | [name] => SOME (decode_str name)
   2.112    | _ => NONE)
   2.113  
   2.114  fun extract_suggestions line =
   2.115    (case space_explode ":" line of
   2.116 -    [goal, suggs] => (unencode_str goal, map_filter extract_suggestion (space_explode " " suggs))
   2.117 +    [goal, suggs] => (decode_str goal, map_filter extract_suggestion (space_explode " " suggs))
   2.118    | _ => ("", []))
   2.119  
   2.120  structure MaSh =
   2.121 @@ -304,40 +301,31 @@
   2.122  
   2.123  (*** Middle-level communication with MaSh ***)
   2.124  
   2.125 -datatype proof_kind =
   2.126 -  Isar_Proof | Automatic_Proof | Isar_Proof_wegen_Prover_Flop
   2.127 +datatype proof_kind = Isar_Proof | Automatic_Proof | Isar_Proof_wegen_Prover_Flop
   2.128  
   2.129  fun str_of_proof_kind Isar_Proof = "i"
   2.130    | str_of_proof_kind Automatic_Proof = "a"
   2.131    | str_of_proof_kind Isar_Proof_wegen_Prover_Flop = "x"
   2.132  
   2.133 -fun proof_kind_of_str "i" = Isar_Proof
   2.134 -  | proof_kind_of_str "a" = Automatic_Proof
   2.135 +fun proof_kind_of_str "a" = Automatic_Proof
   2.136    | proof_kind_of_str "x" = Isar_Proof_wegen_Prover_Flop
   2.137 -
   2.138 -(* FIXME: Here a "Graph.update_node" function would be useful *)
   2.139 -fun update_access_graph_node (name, kind) =
   2.140 -  Graph.default_node (name, Isar_Proof)
   2.141 -  #> kind <> Isar_Proof ? Graph.map_node name (K kind)
   2.142 +  | proof_kind_of_str _ (* "i" *) = Isar_Proof
   2.143  
   2.144  fun try_graph ctxt when def f =
   2.145    f ()
   2.146 -  handle Graph.CYCLES (cycle :: _) =>
   2.147 -         (trace_msg ctxt (fn () =>
   2.148 -              "Cycle involving " ^ commas cycle ^ " when " ^ when); def)
   2.149 -       | Graph.DUP name =>
   2.150 -         (trace_msg ctxt (fn () =>
   2.151 -              "Duplicate fact " ^ quote name ^ " when " ^ when); def)
   2.152 -       | Graph.UNDEF name =>
   2.153 -         (trace_msg ctxt (fn () =>
   2.154 -              "Unknown fact " ^ quote name ^ " when " ^ when); def)
   2.155 -       | exn =>
   2.156 -         if Exn.is_interrupt exn then
   2.157 -           reraise exn
   2.158 -         else
   2.159 -           (trace_msg ctxt (fn () =>
   2.160 -                "Internal error when " ^ when ^ ":\n" ^
   2.161 -                Runtime.exn_message exn); def)
   2.162 +  handle
   2.163 +    Graph.CYCLES (cycle :: _) =>
   2.164 +    (trace_msg ctxt (fn () => "Cycle involving " ^ commas cycle ^ " when " ^ when); def)
   2.165 +  | Graph.DUP name =>
   2.166 +    (trace_msg ctxt (fn () => "Duplicate fact " ^ quote name ^ " when " ^ when); def)
   2.167 +  | Graph.UNDEF name =>
   2.168 +    (trace_msg ctxt (fn () => "Unknown fact " ^ quote name ^ " when " ^ when); def)
   2.169 +  | exn =>
   2.170 +    if Exn.is_interrupt exn then
   2.171 +      reraise exn
   2.172 +    else
   2.173 +      (trace_msg ctxt (fn () => "Internal error when " ^ when ^ ":\n" ^ Runtime.exn_message exn);
   2.174 +       def)
   2.175  
   2.176  fun graph_info G =
   2.177    string_of_int (length (Graph.keys G)) ^ " node(s), " ^
   2.178 @@ -347,25 +335,25 @@
   2.179    string_of_int (length (Graph.maximals G)) ^ " maximal"
   2.180  
   2.181  type mash_state =
   2.182 -  {access_G : unit Graph.T,
   2.183 +  {access_G : (proof_kind * string list list * string list) Graph.T,
   2.184     num_known_facts : int,
   2.185     dirty : string list option}
   2.186  
   2.187 -val empty_state = {access_G = Graph.empty, num_known_facts = 0, dirty = SOME []}
   2.188 +val empty_state = {access_G = Graph.empty, num_known_facts = 0, dirty = SOME []} : mash_state
   2.189  
   2.190  local
   2.191  
   2.192 -val version = "*** MaSh version 20131206 ***"
   2.193 +val version = "*** MaSh version 20140516 ***"
   2.194  
   2.195  exception FILE_VERSION_TOO_NEW of unit
   2.196  
   2.197  fun extract_node line =
   2.198    (case space_explode ":" line of
   2.199 -    [head, parents] =>
   2.200 -    (case space_explode " " head of
   2.201 -      [kind, name] =>
   2.202 -      SOME (unencode_str name, unencode_strs parents,
   2.203 -        try proof_kind_of_str kind |> the_default Isar_Proof)
   2.204 +    [head, tail] =>
   2.205 +    (case (space_explode " " head, map (unprefix " ") (space_explode ";" tail)) of
   2.206 +      ([kind, name], [parents, feats, deps]) =>
   2.207 +      SOME (proof_kind_of_str kind, decode_str name, decode_strs parents,
   2.208 +        decode_unweighted_features feats, decode_strs deps)
   2.209      | _ => NONE)
   2.210    | _ => NONE)
   2.211  
   2.212 @@ -377,40 +365,40 @@
   2.213           SOME (version' :: node_lines) =>
   2.214           let
   2.215             fun add_edge_to name parent =
   2.216 -             Graph.default_node (parent, Isar_Proof)
   2.217 +             Graph.default_node (parent, (Isar_Proof, [], []))
   2.218               #> Graph.add_edge (parent, name)
   2.219             fun add_node line =
   2.220               (case extract_node line of
   2.221 -               NONE => I (* shouldn't happen *)
   2.222 -             | SOME (name, parents, kind) =>
   2.223 -               update_access_graph_node (name, kind) #> fold (add_edge_to name) parents)
   2.224 +               NONE => I (* should not happen *)
   2.225 +             | SOME (kind, name, parents, feats, deps) =>
   2.226 +               Graph.default_node (name, (kind, feats, deps))
   2.227 +               #> Graph.map_node name (K (kind, feats, deps))
   2.228 +               #> fold (add_edge_to name) parents)
   2.229             val (access_G, num_known_facts) =
   2.230               (case string_ord (version', version) of
   2.231                 EQUAL =>
   2.232                 (try_graph ctxt "loading state" Graph.empty (fn () =>
   2.233                    fold add_node node_lines Graph.empty),
   2.234                  length node_lines)
   2.235 -             | LESS =>
   2.236 -               (* can't parse old file *)
   2.237 -               (MaSh.unlearn ctxt overlord; (Graph.empty, 0))
   2.238 +             | LESS => (MaSh.unlearn ctxt overlord; (Graph.empty, 0)) (* cannot parse old file *)
   2.239               | GREATER => raise FILE_VERSION_TOO_NEW ())
   2.240           in
   2.241 -           trace_msg ctxt (fn () =>
   2.242 -               "Loaded fact graph (" ^ graph_info access_G ^ ")");
   2.243 -           {access_G = access_G, num_known_facts = num_known_facts,
   2.244 -            dirty = SOME []}
   2.245 +           trace_msg ctxt (fn () => "Loaded fact graph (" ^ graph_info access_G ^ ")");
   2.246 +           {access_G = access_G, num_known_facts = num_known_facts, dirty = SOME []}
   2.247           end
   2.248         | _ => empty_state))
   2.249      end
   2.250  
   2.251 +fun str_of_entry (kind, name, parents, feats, deps) =
   2.252 +  str_of_proof_kind kind ^ " " ^ encode_str name ^ ": " ^ encode_strs parents ^ "; " ^
   2.253 +  encode_unweighted_features feats ^ "; " ^ encode_strs deps ^ "\n"
   2.254 +
   2.255  fun save_state _ (state as {dirty = SOME [], ...}) = state
   2.256    | save_state ctxt {access_G, num_known_facts, dirty} =
   2.257      let
   2.258 -      fun str_of_entry (name, parents, kind) =
   2.259 -        str_of_proof_kind kind ^ " " ^ encode_str name ^ ": " ^
   2.260 -        encode_strs parents ^ "\n"
   2.261 -      fun append_entry (name, (kind, (parents, _))) =
   2.262 -        cons (name, Graph.Keys.dest parents, kind)
   2.263 +      fun append_entry (name, ((kind, feats, deps), (parents, _))) =
   2.264 +        cons (kind, name, Graph.Keys.dest parents, feats, deps)
   2.265 +
   2.266        val (banner, entries) =
   2.267          (case dirty of
   2.268            SOME names => (NONE, fold (append_entry o Graph.get_entry access_G) names [])
   2.269 @@ -418,11 +406,10 @@
   2.270      in
   2.271        write_file banner (entries, str_of_entry) (mash_state_file ());
   2.272        trace_msg ctxt (fn () =>
   2.273 -          "Saved fact graph (" ^ graph_info access_G ^
   2.274 -          (case dirty of
   2.275 -             SOME dirty =>
   2.276 -             "; " ^ string_of_int (length dirty) ^ " dirty fact(s)"
   2.277 -           | _ => "") ^  ")");
   2.278 +        "Saved fact graph (" ^ graph_info access_G ^
   2.279 +        (case dirty of
   2.280 +          SOME dirty => "; " ^ string_of_int (length dirty) ^ " dirty fact(s)"
   2.281 +        | _ => "") ^  ")");
   2.282        {access_G = access_G, num_known_facts = num_known_facts, dirty = SOME []}
   2.283      end
   2.284  
   2.285 @@ -432,18 +419,15 @@
   2.286  in
   2.287  
   2.288  fun map_state ctxt overlord f =
   2.289 -  Synchronized.change global_state
   2.290 -                      (load_state ctxt overlord ##> (f #> save_state ctxt))
   2.291 +  Synchronized.change global_state (load_state ctxt overlord ##> (f #> save_state ctxt))
   2.292    handle FILE_VERSION_TOO_NEW () => ()
   2.293  
   2.294  fun peek_state ctxt overlord f =
   2.295 -  Synchronized.change_result global_state
   2.296 -      (perhaps (try (load_state ctxt overlord)) #> `snd #>> f)
   2.297 +  Synchronized.change_result global_state (perhaps (try (load_state ctxt overlord)) #> `snd #>> f)
   2.298  
   2.299  fun clear_state ctxt overlord =
   2.300 -  Synchronized.change global_state (fn _ =>
   2.301 -      (MaSh.unlearn ctxt overlord; (* also removes the state file *)
   2.302 -       (false, empty_state)))
   2.303 +  (* "unlearn" also removes the state file *)
   2.304 +  Synchronized.change global_state (fn _ => (MaSh.unlearn ctxt overlord; (false, empty_state)))
   2.305  
   2.306  end
   2.307  
   2.308 @@ -747,7 +731,7 @@
   2.309    end
   2.310  
   2.311  (* Too many dependencies is a sign that a decision procedure is at work. There
   2.312 -   isn't much to learn from such proofs. *)
   2.313 +   is not much to learn from such proofs. *)
   2.314  val max_dependencies = 20
   2.315  
   2.316  val prover_default_max_facts = 25
   2.317 @@ -819,7 +803,7 @@
   2.318          else
   2.319            (case find_first (is_dep dep) facts of
   2.320              SOME ((_, status), th) => accum @ [(("", status), th)]
   2.321 -          | NONE => accum (* shouldn't happen *))
   2.322 +          | NONE => accum (* should not happen *))
   2.323        val mepo_facts =
   2.324          facts
   2.325          |> mepo_suggested_facts ctxt params (max_facts |> the_default prover_default_max_facts) NONE
   2.326 @@ -1006,30 +990,26 @@
   2.327                val parents = maximal_wrt_access_graph access_G facts
   2.328                val goal_feats =
   2.329                  features_of ctxt thy num_facts const_tab (Local, General) true (concl_t :: hyp_ts)
   2.330 -              val chained_feats =
   2.331 -                chained
   2.332 +              val chained_feats = chained
   2.333                  |> map (rpair 1.0)
   2.334                  |> map (chained_or_extra_features_of chained_feature_factor)
   2.335                  |> rpair [] |-> fold (union (eq_fst (op =)))
   2.336 -              val extra_feats =
   2.337 -                facts
   2.338 +              val extra_feats = facts
   2.339                  |> take (Int.max (0, num_extra_feature_facts - length chained))
   2.340                  |> filter fact_has_right_theory
   2.341                  |> weight_facts_steeply
   2.342                  |> map (chained_or_extra_features_of extra_feature_factor)
   2.343                  |> rpair [] |-> fold (union (eq_fst (op =)))
   2.344                val feats =
   2.345 -                fold (union (eq_fst (op =))) [chained_feats, extra_feats]
   2.346 -                     goal_feats
   2.347 +                fold (union (eq_fst (op =))) [chained_feats, extra_feats] goal_feats
   2.348                  |> debug ? sort (Real.compare o swap o pairself snd)
   2.349 -              val hints =
   2.350 -                chained |> filter (is_fact_in_graph access_G o snd)
   2.351 -                        |> map (nickname_of_thm o snd)
   2.352 +              val hints = chained
   2.353 +                |> filter (is_fact_in_graph access_G o snd)
   2.354 +                |> map (nickname_of_thm o snd)
   2.355              in
   2.356 -              (access_G, MaSh.query ctxt overlord max_facts
   2.357 -                                    ([], hints, parents, feats))
   2.358 +              (access_G, MaSh.query ctxt overlord max_facts ([], hints, parents, feats))
   2.359              end)
   2.360 -    val unknown = facts |> filter_out (is_fact_in_graph access_G o snd)
   2.361 +    val unknown = filter_out (is_fact_in_graph access_G o snd) facts
   2.362    in
   2.363      find_mash_suggestions ctxt max_facts suggs facts chained unknown
   2.364      |> pairself (map fact_of_raw_fact)
   2.365 @@ -1039,8 +1019,8 @@
   2.366    let
   2.367      fun maybe_learn_from from (accum as (parents, graph)) =
   2.368        try_graph ctxt "updating graph" accum (fn () =>
   2.369 -          (from :: parents, Graph.add_edge_acyclic (from, name) graph))
   2.370 -    val graph = graph |> Graph.default_node (name, Isar_Proof)
   2.371 +        (from :: parents, Graph.add_edge_acyclic (from, name) graph))
   2.372 +    val graph = graph |> Graph.default_node (name, (Isar_Proof, feats, deps))
   2.373      val (parents, graph) = ([], graph) |> fold maybe_learn_from parents
   2.374      val (deps, _) = ([], graph) |> fold maybe_learn_from deps
   2.375    in ((name, parents, feats, deps) :: learns, graph) end
   2.376 @@ -1049,13 +1029,13 @@
   2.377    let
   2.378      fun maybe_relearn_from from (accum as (parents, graph)) =
   2.379        try_graph ctxt "updating graph" accum (fn () =>
   2.380 -          (from :: parents, Graph.add_edge_acyclic (from, name) graph))
   2.381 -    val graph = graph |> update_access_graph_node (name, Automatic_Proof)
   2.382 +        (from :: parents, Graph.add_edge_acyclic (from, name) graph))
   2.383 +    val graph = graph |> Graph.map_node name (fn (_, feats, _) => (Automatic_Proof, feats, deps))
   2.384      val (deps, _) = ([], graph) |> fold maybe_relearn_from deps
   2.385    in ((name, deps) :: relearns, graph) end
   2.386  
   2.387  fun flop_wrt_access_graph name =
   2.388 -  update_access_graph_node (name, Isar_Proof_wegen_Prover_Flop)
   2.389 +  Graph.map_node name (fn (_, feats, deps) => (Isar_Proof_wegen_Prover_Flop, feats, deps))
   2.390  
   2.391  val learn_timeout_slack = 2.0
   2.392  
   2.393 @@ -1099,17 +1079,16 @@
   2.394    let
   2.395      val timer = Timer.startRealTimer ()
   2.396      fun next_commit_time () = Time.+ (Timer.checkRealTimer timer, commit_timeout)
   2.397 +
   2.398      val {access_G, ...} = peek_state ctxt overlord I
   2.399      val is_in_access_G = is_fact_in_graph access_G o snd
   2.400      val no_new_facts = forall is_in_access_G facts
   2.401    in
   2.402      if no_new_facts andalso not run_prover then
   2.403        if auto_level < 2 then
   2.404 -        "No new " ^ (if run_prover then "automatic" else "Isar") ^
   2.405 -        " proofs to learn." ^
   2.406 +        "No new " ^ (if run_prover then "automatic" else "Isar") ^ " proofs to learn." ^
   2.407          (if auto_level = 0 andalso not run_prover then
   2.408 -           "\n\nHint: Try " ^ sendback learn_proverN ^
   2.409 -           " to learn from an automatic prover."
   2.410 +           "\n\nHint: Try " ^ sendback learn_proverN ^ " to learn from an automatic prover."
   2.411           else
   2.412             "")
   2.413        else
   2.414 @@ -1117,23 +1096,22 @@
   2.415      else
   2.416        let
   2.417          val name_tabs = build_name_tables nickname_of_thm facts
   2.418 +
   2.419          fun deps_of status th =
   2.420            if no_dependencies_for_status status then
   2.421              SOME []
   2.422            else if run_prover then
   2.423 -            prover_dependencies_of ctxt params prover auto_level facts name_tabs
   2.424 -                                   th
   2.425 -            |> (fn (false, _) => NONE
   2.426 -                 | (true, deps) => trim_dependencies deps)
   2.427 +            prover_dependencies_of ctxt params prover auto_level facts name_tabs th
   2.428 +            |> (fn (false, _) => NONE | (true, deps) => trim_dependencies deps)
   2.429            else
   2.430              isar_dependencies_of name_tabs th
   2.431              |> trim_dependencies
   2.432 +
   2.433          fun do_commit [] [] [] state = state
   2.434            | do_commit learns relearns flops {access_G, num_known_facts, dirty} =
   2.435              let
   2.436                val was_empty = Graph.is_empty access_G
   2.437 -              val (learns, access_G) =
   2.438 -                ([], access_G) |> fold (learn_wrt_access_graph ctxt) learns
   2.439 +              val (learns, access_G) = ([], access_G) |> fold (learn_wrt_access_graph ctxt) learns
   2.440                val (relearns, access_G) =
   2.441                  ([], access_G) |> fold (relearn_wrt_access_graph ctxt) relearns
   2.442                val access_G = access_G |> fold flop_wrt_access_graph flops
   2.443 @@ -1145,9 +1123,9 @@
   2.444              in
   2.445                MaSh.learn ctxt overlord (save andalso null relearns) (rev learns);
   2.446                MaSh.relearn ctxt overlord save relearns;
   2.447 -              {access_G = access_G, num_known_facts = num_known_facts,
   2.448 -               dirty = dirty}
   2.449 +              {access_G = access_G, num_known_facts = num_known_facts, dirty = dirty}
   2.450              end
   2.451 +
   2.452          fun commit last learns relearns flops =
   2.453            (if debug andalso auto_level = 0 then
   2.454               Output.urgent_message "Committing..."
   2.455 @@ -1164,9 +1142,10 @@
   2.456               end
   2.457             else
   2.458               ())
   2.459 +
   2.460          fun learn_new_fact _ (accum as (_, (_, _, true))) = accum
   2.461            | learn_new_fact (parents, ((_, stature as (_, status)), th))
   2.462 -                           (learns, (n, next_commit, _)) =
   2.463 +              (learns, (n, next_commit, _)) =
   2.464              let
   2.465                val name = nickname_of_thm th
   2.466                val feats =
   2.467 @@ -1181,23 +1160,28 @@
   2.468                  else
   2.469                    (learns, next_commit)
   2.470                val timed_out = Time.> (Timer.checkRealTimer timer, learn_timeout)
   2.471 -            in (learns, (n, next_commit, timed_out)) end
   2.472 +            in
   2.473 +              (learns, (n, next_commit, timed_out))
   2.474 +            end
   2.475 +
   2.476          val n =
   2.477            if no_new_facts then
   2.478              0
   2.479            else
   2.480              let
   2.481 -              val new_facts =
   2.482 -                facts |> sort (crude_thm_ord o pairself snd)
   2.483 -                      |> attach_parents_to_facts []
   2.484 -                      |> filter_out (is_in_access_G o snd)
   2.485 +              val new_facts = facts
   2.486 +                |> sort (crude_thm_ord o pairself snd)
   2.487 +                |> attach_parents_to_facts []
   2.488 +                |> filter_out (is_in_access_G o snd)
   2.489                val (learns, (n, _, _)) =
   2.490                  ([], (0, next_commit_time (), false))
   2.491                  |> fold learn_new_fact new_facts
   2.492 -            in commit true learns [] []; n end
   2.493 +            in
   2.494 +              commit true learns [] []; n
   2.495 +            end
   2.496 +
   2.497          fun relearn_old_fact _ (accum as (_, (_, _, true))) = accum
   2.498 -          | relearn_old_fact ((_, (_, status)), th)
   2.499 -                             ((relearns, flops), (n, next_commit, _)) =
   2.500 +          | relearn_old_fact ((_, (_, status)), th) ((relearns, flops), (n, next_commit, _)) =
   2.501              let
   2.502                val name = nickname_of_thm th
   2.503                val (n, relearns, flops) =
   2.504 @@ -1206,37 +1190,43 @@
   2.505                  | NONE => (n, relearns, name :: flops))
   2.506                val (relearns, flops, next_commit) =
   2.507                  if Time.> (Timer.checkRealTimer timer, next_commit) then
   2.508 -                  (commit false [] relearns flops;
   2.509 -                   ([], [], next_commit_time ()))
   2.510 +                  (commit false [] relearns flops; ([], [], next_commit_time ()))
   2.511                  else
   2.512                    (relearns, flops, next_commit)
   2.513                val timed_out = Time.> (Timer.checkRealTimer timer, learn_timeout)
   2.514 -            in ((relearns, flops), (n, next_commit, timed_out)) end
   2.515 +            in
   2.516 +              ((relearns, flops), (n, next_commit, timed_out))
   2.517 +            end
   2.518 +
   2.519          val n =
   2.520            if not run_prover then
   2.521              n
   2.522            else
   2.523              let
   2.524                val max_isar = 1000 * max_dependencies
   2.525 -              fun kind_of_proof th =
   2.526 -                try (Graph.get_node access_G) (nickname_of_thm th)
   2.527 -                |> the_default Isar_Proof
   2.528 -              fun priority_of (_, th) =
   2.529 +
   2.530 +              val kind_of_proof =
   2.531 +                nickname_of_thm #> try (#1 o Graph.get_node access_G) #> the_default Isar_Proof
   2.532 +
   2.533 +              fun priority_of th =
   2.534                  random_range 0 max_isar
   2.535                  + (case kind_of_proof th of
   2.536                       Isar_Proof => 0
   2.537                     | Automatic_Proof => 2 * max_isar
   2.538                     | Isar_Proof_wegen_Prover_Flop => max_isar)
   2.539                  - 100 * length (isar_dependencies_of name_tabs th)
   2.540 -              val old_facts =
   2.541 -                facts |> filter is_in_access_G
   2.542 -                      |> map (`priority_of)
   2.543 -                      |> sort (int_ord o pairself fst)
   2.544 -                      |> map snd
   2.545 +
   2.546 +              val old_facts = facts
   2.547 +                |> filter is_in_access_G
   2.548 +                |> map (`(priority_of o snd))
   2.549 +                |> sort (int_ord o pairself fst)
   2.550 +                |> map snd
   2.551                val ((relearns, flops), (n, _, _)) =
   2.552                  (([], []), (n, next_commit_time (), false))
   2.553                  |> fold relearn_old_fact old_facts
   2.554 -            in commit true [] relearns flops; n end
   2.555 +            in
   2.556 +              commit true [] relearns flops; n
   2.557 +            end
   2.558        in
   2.559          if verbose orelse auto_level < 2 then
   2.560            "Learned " ^ string_of_int n ^ " nontrivial " ^
   2.561 @@ -1291,8 +1281,8 @@
   2.562  
   2.563  val max_facts_to_learn_before_query = 100
   2.564  
   2.565 -(* The threshold should be large enough so that MaSh doesn't kick in for Auto
   2.566 -   Sledgehammer and Try. *)
   2.567 +(* The threshold should be large enough so that MaSh does not get activated for Auto Sledgehammer
   2.568 +   and Try. *)
   2.569  val min_secs_for_learning = 15
   2.570  
   2.571  fun relevant_facts ctxt (params as {overlord, blocking, learn, fact_filter, timeout, ...}) prover
   2.572 @@ -1381,6 +1371,7 @@
   2.573  
   2.574  fun kill_learners ctxt ({overlord, ...} : params) =
   2.575    (Async_Manager.kill_threads MaShN "learner"; MaSh.shutdown ctxt overlord)
   2.576 +
   2.577  fun running_learners () = Async_Manager.running_threads MaShN "learner"
   2.578  
   2.579  end;