val unescape_meta : string -> string

   val unescape_meta : string -> string

   val unescape_metas : string -> string list

   val unescape_metas : string -> string list

   val extract_query : string -> string * string list

   val extract_query : string -> string * string list

   val suggested_facts : string list -> fact list -> fact list

   val suggested_facts : string list -> fact list -> fact list

   val mesh_facts : int -> (fact list * int option) list -> fact list

   val mesh_facts : int -> (fact list * int option) list -> fact list

   val is_too_meta : thm -> bool

   val is_too_meta : thm -> bool

   val theory_ord : theory * theory -> order

   val theory_ord : theory * theory -> order

   val thm_ord : thm * thm -> order

   val thm_ord : thm * thm -> order

   val isabelle_dependencies_of : unit Symtab.table -> thm -> string list

   val isabelle_dependencies_of : unit Symtab.table -> thm -> string list

   val goal_of_thm : theory -> thm -> thm

   val goal_of_thm : theory -> thm -> thm

   val mash_RESET : Proof.context -> unit

   val mash_RESET : Proof.context -> unit

   val mash_INIT :

   val mash_INIT :

     Proof.context -> bool

     Proof.context -> bool

     -> (string * string list * string list * string list) list -> unit

     -> (string * string list * string list * string list) list -> unit

   val mash_ADD :

   val mash_ADD :

     Proof.context -> bool

     Proof.context -> bool

     -> (string * string list * string list * string list) list -> unit

     -> (string * string list * string list * string list) list -> unit

   val mash_QUERY :

   val mash_QUERY :

   val mash_reset : Proof.context -> unit

   val mash_reset : Proof.context -> unit

   val mash_suggest_facts :

   val mash_suggest_facts :

     -> fact list

     -> fact list

   val mash_learn_proof :

   val mash_learn_proof :

     Proof.context -> params -> term -> thm list -> fact list -> unit

     Proof.context -> params -> term -> thm list -> fact list -> unit

   val relevant_facts :

   val relevant_facts :

     Proof.context -> params -> string -> int -> fact_override -> term list

     Proof.context -> params -> string -> int -> fact_override -> term list

     -> term -> fact list -> fact list

     -> term -> fact list -> fact list

 open ATP_Problem_Generate

 open ATP_Problem_Generate

 open Sledgehammer_Util

 open Sledgehammer_Util

 open Sledgehammer_Fact

 open Sledgehammer_Fact

 open Sledgehammer_Filter_Iter

 open Sledgehammer_Filter_Iter

 open Sledgehammer_Provers

 open Sledgehammer_Provers

 val trace =

 val trace =

   Attrib.setup_config_bool @{binding sledgehammer_filter_mash_trace} (K false)

   Attrib.setup_config_bool @{binding sledgehammer_filter_mash_trace} (K false)

 fun trace_msg ctxt msg = if Config.get ctxt trace then tracing (msg ()) else ()

 fun trace_msg ctxt msg = if Config.get ctxt trace then tracing (msg ()) else ()

          has_bool_arg_const t orelse exists_Const (higher_inst_const thy) t)

          has_bool_arg_const t orelse exists_Const (higher_inst_const thy) t)

   end

   end

 end

 end

   let

   let

     val bad_types = [@{type_name prop}, @{type_name bool}, @{type_name fun}]

     val bad_types = [@{type_name prop}, @{type_name bool}, @{type_name fun}]

     fun add_classes @{sort type} = I

     fun add_classes @{sort type} = I

       | add_classes S = union (op =) (map class_name_of S)

       | add_classes S = union (op =) (map class_name_of S)

     fun do_add_type (Type (s, Ts)) =

     fun do_add_type (Type (s, Ts)) =

         (not (member (op =) bad_types s) ? insert (op =) (type_name_of s))

         (not (member (op =) bad_types s) ? insert (op =) (type_name_of s))

         #> fold do_add_type Ts

         #> fold do_add_type Ts

         #> add_term_patterns (depth - 1) t

         #> add_term_patterns (depth - 1) t

     val add_term = add_term_patterns term_max_depth

     val add_term = add_term_patterns term_max_depth

     fun add_patterns t =

     fun add_patterns t =

       let val (head, args) = strip_comb t in

       let val (head, args) = strip_comb t in

         (case head of

         (case head of

          | Free (_, T) => add_type T

          | Free (_, T) => add_type T

          | Var (_, T) => add_type T

          | Var (_, T) => add_type T

          | Abs (_, T, body) => add_type T #> add_patterns body

          | Abs (_, T, body) => add_type T #> add_patterns body

          | _ => I)

          | _ => I)

         #> fold add_patterns args

         #> fold add_patterns args

       end

       end

   in [] |> fold add_patterns ts |> sort string_ord end

   in [] |> fold add_patterns ts |> sort string_ord end

 (* ### FIXME: optimize *)

 (* ### FIXME: optimize *)

 fun is_too_meta th =

 fun is_too_meta th =

   fastype_of (Object_Logic.atomize_term (theory_of_thm th) (prop_of th))

   fastype_of (Object_Logic.atomize_term (theory_of_thm th) (prop_of th))

   <> @{typ bool}

   <> @{typ bool}

 val term_max_depth = 1

 val term_max_depth = 1

 val type_max_depth = 1

 val type_max_depth = 1

 (* TODO: Generate type classes for types? *)

 (* TODO: Generate type classes for types? *)

   thy_feature_name_of (Context.theory_name thy) ::

   thy_feature_name_of (Context.theory_name thy) ::

   |> exists (not o is_lambda_free) ts ? cons "lambdas"

   |> exists (not o is_lambda_free) ts ? cons "lambdas"

   |> exists (exists_Const is_exists) ts ? cons "skolems"

   |> exists (exists_Const is_exists) ts ? cons "skolems"

   |> exists (not o is_fo_term thy) ts ? cons "ho"

   |> exists (not o is_fo_term thy) ts ? cons "ho"

   |> (case status of

   |> (case status of

         General => I

         General => I

   | freeze (Free (s, T)) = Free (s, freezeT T)

   | freeze (Free (s, T)) = Free (s, freezeT T)

   | freeze t = t

   | freeze t = t

 fun goal_of_thm thy = prop_of #> freeze #> cterm_of thy #> Goal.init

 fun goal_of_thm thy = prop_of #> freeze #> cterm_of thy #> Goal.init

   let

   let

     val problem =

     val problem =

       {state = Proof.init ctxt, goal = goal, subgoal = 1, subgoal_count = 1,

       {state = Proof.init ctxt, goal = goal, subgoal = 1, subgoal_count = 1,

        facts = facts |> map (apfst (apfst (fn name => name ())))

        facts = facts |> map (apfst (apfst (fn name => name ())))

   in prover params (K (K (K ""))) problem end

   in prover params (K (K (K ""))) problem end

 (*** Low-level communication with MaSh ***)

 (*** Low-level communication with MaSh ***)

 fun mash_info overlord =

 fun mash_info overlord =

   if overlord then (getenv "ISABELLE_HOME_USER", "")

   if overlord then (getenv "ISABELLE_HOME_USER", "")

   else (getenv "ISABELLE_TMP", serial_string ())

   else (getenv "ISABELLE_TMP", serial_string ())

     val command =

     val command =

       mash_home () ^ "/mash.py --quiet --outputDir " ^ mash_state_dir () ^

       mash_home () ^ "/mash.py --quiet --outputDir " ^ mash_state_dir () ^

       " --log " ^ log_file ^ " " ^ core ^ " 2>&1 > " ^ err_file

       " --log " ^ log_file ^ " " ^ core ^ " 2>&1 > " ^ err_file

   in

   in

     trace_msg ctxt (fn () => "Running " ^ command);

     trace_msg ctxt (fn () => "Running " ^ command);

     Isabelle_System.bash command; ()

     Isabelle_System.bash command; ()

   end

   end

 fun run_mash_init ctxt overlord write_access write_feats write_deps =

 fun run_mash_init ctxt overlord write_access write_feats write_deps =

   let

   let

     val info as (temp_dir, serial) = mash_info overlord

     val info as (temp_dir, serial) = mash_info overlord

     write_file write_feats (in_dir ^ "/mash_features");

     write_file write_feats (in_dir ^ "/mash_features");

     write_file write_deps (in_dir ^ "/mash_dependencies");

     write_file write_deps (in_dir ^ "/mash_dependencies");

     run_mash ctxt info ("--init --inputDir " ^ in_dir)

     run_mash ctxt info ("--init --inputDir " ^ in_dir)

   end

   end

   let

   let

     val info as (temp_dir, serial) = mash_info overlord

     val info as (temp_dir, serial) = mash_info overlord

     val cmd_file = temp_dir ^ "/mash_commands" ^ serial

     val cmd_file = temp_dir ^ "/mash_commands" ^ serial

   in

   in

     write_file write_cmds cmd_file;

     write_file write_cmds cmd_file;

     run_mash ctxt info

     run_mash ctxt info

               (if save then " --saveModel" else ""));

               (if save then " --saveModel" else ""));

   end

   end

 fun str_of_update (name, parents, feats, deps) =

 fun str_of_update (name, parents, feats, deps) =

   "! " ^ escape_meta name ^ ": " ^ escape_metas parents ^ "; " ^

   "! " ^ escape_meta name ^ ": " ^ escape_metas parents ^ "; " ^

   escape_metas feats ^ "; " ^ escape_metas deps ^ "\n"

   escape_metas feats ^ "; " ^ escape_metas deps ^ "\n"

 fun mash_ADD _ _ [] = ()

 fun mash_ADD _ _ [] = ()

   | mash_ADD ctxt overlord upds =

   | mash_ADD ctxt overlord upds =

     (trace_msg ctxt (fn () => "MaSh ADD " ^

     (trace_msg ctxt (fn () => "MaSh ADD " ^

          elide_string 1000 (space_implode " " (map #1 upds)));

          elide_string 1000 (space_implode " " (map #1 upds)));

          (fn append => List.app (append o str_of_update) upds) (K ()))

          (fn append => List.app (append o str_of_update) upds) (K ()))

   (trace_msg ctxt (fn () => "MaSh QUERY " ^ space_implode " " feats);

   (trace_msg ctxt (fn () => "MaSh QUERY " ^ space_implode " " feats);

        (fn append => append (str_of_query query))

        (fn append => append (str_of_query query))

    handle List.Empty => [])

    handle List.Empty => [])

 (*** High-level communication with MaSh ***)

 (*** High-level communication with MaSh ***)

 fun mash_save ({thys, fact_graph, ...} : mash_state) =

 fun mash_save ({thys, fact_graph, ...} : mash_state) =

   let

   let

     val path = mash_state_path ()

     val path = mash_state_path ()

     val thys = Symtab.dest thys

     val thys = Symtab.dest thys

     val append_fact = File.append path o suffix "\n" oo fact_line_for

     val append_fact = File.append path o suffix "\n" oo fact_line_for

   in

   in

     File.write path (line_for_thys true ^ "\n" ^ line_for_thys false ^ "\n");

     File.write path (line_for_thys true ^ "\n" ^ line_for_thys false ^ "\n");

     Graph.fold (fn (name, ((), (parents, _))) => fn () =>

     Graph.fold (fn (name, ((), (parents, _))) => fn () =>

                    append_fact name (Graph.Keys.dest parents))

                    append_fact name (Graph.Keys.dest parents))

       (mash_RESET ctxt; File.write (mash_state_path ()) "";

       (mash_RESET ctxt; File.write (mash_state_path ()) "";

        (true, empty_state)))

        (true, empty_state)))

 end

 end

     val facts =

     val facts =

   in fact_graph |> Graph.restrict (Symtab.defined facts) |> Graph.maximals end

   in fact_graph |> Graph.restrict (Symtab.defined facts) |> Graph.maximals end

   let

   let

     val thy = Proof_Context.theory_of ctxt

     val thy = Proof_Context.theory_of ctxt

     val fact_graph = #fact_graph (mash_get ())

     val fact_graph = #fact_graph (mash_get ())

   in suggested_facts suggs facts end

   in suggested_facts suggs facts end

 fun add_thys_for thy =

 fun add_thys_for thy =

   let fun add comp thy = Symtab.update (Context.theory_name thy, comp) in

   let fun add comp thy = Symtab.update (Context.theory_name thy, comp) in

     add false thy #> fold (add true) (Theory.ancestors_of thy)

     add false thy #> fold (add true) (Theory.ancestors_of thy)

     val graph = graph |> Graph.new_node (name, ())

     val graph = graph |> Graph.new_node (name, ())

     val (parents, graph) = ([], graph) |> fold maybe_add_from parents

     val (parents, graph) = ([], graph) |> fold maybe_add_from parents

     val (deps, graph) = ([], graph) |> fold maybe_add_from deps

     val (deps, graph) = ([], graph) |> fold maybe_add_from deps

   in ((name, parents, feats, deps) :: upds, graph) end

   in ((name, parents, feats, deps) :: upds, graph) end

     val facts = all_facts_of thy css_table

     val facts = all_facts_of thy css_table

     val {fact_graph, ...} = mash_get ()

     val {fact_graph, ...} = mash_get ()

     fun is_old (_, th) = can (Graph.get_node fact_graph) (Thm.get_name_hint th)

     fun is_old (_, th) = can (Graph.get_node fact_graph) (Thm.get_name_hint th)

     val new_facts = facts |> filter_out is_old |> sort (thm_ord o pairself snd)

     val new_facts = facts |> filter_out is_old |> sort (thm_ord o pairself snd)

   in

   in

     if null new_facts then

     if null new_facts then

       ()

       ()

     else

     else

       let

       let

         val ths = facts |> map snd

         val ths = facts |> map snd

         val all_names =

         val all_names =

               |> map (rpair () o Thm.get_name_hint)

               |> map (rpair () o Thm.get_name_hint)

               |> Symtab.make

               |> Symtab.make

         fun trans {thys, fact_graph} =

         fun trans {thys, fact_graph} =

           let

           let

             val mash_INIT_or_ADD =

             val mash_INIT_or_ADD =

               if Graph.is_empty fact_graph then mash_INIT else mash_ADD

               if Graph.is_empty fact_graph then mash_INIT else mash_ADD

             val (upds, fact_graph) =

             val (upds, fact_graph) =

           in

           in

             (mash_INIT_or_ADD ctxt overlord (rev upds);

             (mash_INIT_or_ADD ctxt overlord (rev upds);

              {thys = thys |> add_thys_for thy,

              {thys = thys |> add_thys_for thy,

               fact_graph = fact_graph})

               fact_graph = fact_graph})

           end

           end

   let

   let

     val thy = Proof_Context.theory_of ctxt

     val thy = Proof_Context.theory_of ctxt

     val deps = used_ths |> map Thm.get_name_hint

     val deps = used_ths |> map Thm.get_name_hint

   in

   in

     mash_map (fn {thys, fact_graph} =>

     mash_map (fn {thys, fact_graph} =>

         let

         let

           val upds = [(name, parents, feats, deps)]

           val upds = [(name, parents, feats, deps)]

           val (upds, fact_graph) =

           val (upds, fact_graph) =

             ([], fact_graph) |> fold (update_fact_graph ctxt) upds

             ([], fact_graph) |> fold (update_fact_graph ctxt) upds

         in

         in

           mash_ADD ctxt overlord upds;

           mash_ADD ctxt overlord upds;

           {thys = thys, fact_graph = fact_graph}

           {thys = thys, fact_graph = fact_graph}

         end)

         end)

   end

   end

         ({add, only, ...} : fact_override) hyp_ts concl_t facts =

         ({add, only, ...} : fact_override) hyp_ts concl_t facts =

   if not (subset (op =) (the_list fact_filter, fact_filters)) then

   if not (subset (op =) (the_list fact_filter, fact_filters)) then

     error ("Unknown fact filter: " ^ quote (the fact_filter) ^ ".")

     error ("Unknown fact filter: " ^ quote (the fact_filter) ^ ".")

   else if only then

   else if only then

     facts

     facts

   else if max_facts <= 0 then

   else if max_facts <= 0 then

     []

     []

   else

   else

     let

     let

       val fact_filter =

       val fact_filter =

         case fact_filter of

         case fact_filter of

       val add_ths = Attrib.eval_thms ctxt add

       val add_ths = Attrib.eval_thms ctxt add

       fun prepend_facts ths accepts =

       fun prepend_facts ths accepts =

         ((facts |> filter (member Thm.eq_thm_prop ths o snd)) @

         ((facts |> filter (member Thm.eq_thm_prop ths o snd)) @

          (accepts |> filter_out (member Thm.eq_thm_prop ths o snd)))

          (accepts |> filter_out (member Thm.eq_thm_prop ths o snd)))

         |> take max_facts

         |> take max_facts

       fun iter () =

       fun iter () =

         iterative_relevant_facts ctxt params prover max_facts NONE hyp_ts

         iterative_relevant_facts ctxt params prover max_facts NONE hyp_ts

                                  concl_t facts

                                  concl_t facts

         |> (fn facts => (facts, SOME (length facts)))

         |> (fn facts => (facts, SOME (length facts)))

       fun mash () =

       fun mash () =

       val mess =

       val mess =

         [] |> (if fact_filter <> mashN then cons (iter ()) else I)

         [] |> (if fact_filter <> mashN then cons (iter ()) else I)

            |> (if fact_filter <> iterN then cons (mash ()) else I)

            |> (if fact_filter <> iterN then cons (mash ()) else I)

     in

     in

       mesh_facts max_facts mess

       mesh_facts max_facts mess