blanchet@49263: (*  Title:      HOL/Tools/Sledgehammer/sledgehammer_filter_mash.ML
blanchet@49263:     Author:     Jasmin Blanchette, TU Muenchen
blanchet@49263: 
blanchet@49263: Sledgehammer's machine-learning-based relevance filter (MaSh).
blanchet@49263: *)
blanchet@49263: 
blanchet@49263: signature SLEDGEHAMMER_FILTER_MASH =
blanchet@49263: sig
blanchet@49266:   type status = ATP_Problem_Generate.status
blanchet@49266:   type stature = ATP_Problem_Generate.stature
blanchet@49311:   type fact = Sledgehammer_Fact.fact
blanchet@49311:   type fact_override = Sledgehammer_Fact.fact_override
blanchet@49266:   type params = Sledgehammer_Provers.params
blanchet@49303:   type relevance_fudge = Sledgehammer_Provers.relevance_fudge
blanchet@49266:   type prover_result = Sledgehammer_Provers.prover_result
blanchet@49266: 
blanchet@49323:   val trace : bool Config.T
blanchet@49318:   val escape_meta : string -> string
blanchet@49318:   val escape_metas : string list -> string
blanchet@49323:   val unescape_meta : string -> string
blanchet@49323:   val unescape_metas : string -> string list
blanchet@49326:   val extract_query : string -> string * string list
blanchet@49326:   val suggested_facts : string list -> ('a * thm) list -> ('a * thm) list
blanchet@49314:   val all_non_tautological_facts_of :
blanchet@49314:     theory -> status Termtab.table -> fact list
blanchet@49266:   val theory_ord : theory * theory -> order
blanchet@49266:   val thm_ord : thm * thm -> order
blanchet@49318:   val thy_facts_from_thms : ('a * thm) list -> string list Symtab.table
blanchet@49266:   val has_thy : theory -> thm -> bool
blanchet@49318:   val parent_facts : theory -> string list Symtab.table -> string list
blanchet@49317:   val features_of : theory -> status -> term list -> string list
blanchet@49266:   val isabelle_dependencies_of : string list -> thm -> string list
blanchet@49266:   val goal_of_thm : theory -> thm -> thm
blanchet@49311:   val run_prover : Proof.context -> params -> fact list -> thm -> prover_result
blanchet@49319:   val thy_name_of_fact : string -> string
blanchet@49323:   val mash_RESET : Proof.context -> unit
blanchet@49323:   val mash_ADD :
blanchet@49323:     Proof.context -> (string * string list * string list * string list) list
blanchet@49323:     -> unit
blanchet@49323:   val mash_DEL : Proof.context -> string list -> string list -> unit
blanchet@49326:   val mash_QUERY : Proof.context -> string list * string list -> string list
blanchet@49323:   val mash_reset : Proof.context -> unit
blanchet@49323:   val mash_can_suggest_facts : Proof.context -> bool
blanchet@49313:   val mash_suggest_facts :
blanchet@49326:     Proof.context -> params -> string -> term list -> term -> fact list
blanchet@49326:     -> fact list
blanchet@49323:   val mash_can_learn_thy : Proof.context -> theory -> bool
blanchet@49323:   val mash_learn_thy : Proof.context -> theory -> real -> unit
blanchet@49324:   val mash_learn_proof : Proof.context -> theory -> term -> thm list -> unit
blanchet@49303:   val relevant_facts :
blanchet@49307:     Proof.context -> params -> string -> int -> fact_override -> term list
blanchet@49311:     -> term -> fact list -> fact list
blanchet@49263: end;
blanchet@49263: 
blanchet@49263: structure Sledgehammer_Filter_MaSh : SLEDGEHAMMER_FILTER_MASH =
blanchet@49263: struct
blanchet@49264: 
blanchet@49266: open ATP_Util
blanchet@49266: open ATP_Problem_Generate
blanchet@49266: open Sledgehammer_Util
blanchet@49266: open Sledgehammer_Fact
blanchet@49266: open Sledgehammer_Filter_Iter
blanchet@49266: open Sledgehammer_Provers
blanchet@49266: 
blanchet@49323: val trace =
blanchet@49323:   Attrib.setup_config_bool @{binding sledgehammer_filter_mash_trace} (K false)
blanchet@49323: fun trace_msg ctxt msg = if Config.get ctxt trace then tracing (msg ()) else ()
blanchet@49323: 
blanchet@49324: fun mash_dir () =
blanchet@49324:   getenv "ISABELLE_HOME_USER" ^ "/mash"
blanchet@49324:   |> tap (fn dir => Isabelle_System.mkdir (Path.explode dir))
blanchet@49324: fun mash_state_path () = mash_dir () ^ "/state" |> Path.explode
blanchet@49266: 
blanchet@49266: (*** Isabelle helpers ***)
blanchet@49266: 
blanchet@49323: fun meta_char c =
blanchet@49266:   if Char.isAlphaNum c orelse c = #"_" orelse c = #"." orelse c = #"(" orelse
blanchet@49266:      c = #")" orelse c = #"," then
blanchet@49266:     String.str c
blanchet@49266:   else
blanchet@49266:     (* fixed width, in case more digits follow *)
blanchet@49266:     "\\" ^ stringN_of_int 3 (Char.ord c)
blanchet@49266: 
blanchet@49323: fun unmeta_chars accum [] = String.implode (rev accum)
blanchet@49323:   | unmeta_chars accum (#"\\" :: d1 :: d2 :: d3 :: cs) =
blanchet@49323:     (case Int.fromString (String.implode [d1, d2, d3]) of
blanchet@49323:        SOME n => unmeta_chars (Char.chr n :: accum) cs
blanchet@49323:      | NONE => "" (* error *))
blanchet@49323:   | unmeta_chars _ (#"\\" :: _) = "" (* error *)
blanchet@49323:   | unmeta_chars accum (c :: cs) = unmeta_chars (c :: accum) cs
blanchet@49323: 
blanchet@49323: val escape_meta = String.translate meta_char
blanchet@49318: val escape_metas = map escape_meta #> space_implode " "
blanchet@49323: val unescape_meta = unmeta_chars [] o String.explode
blanchet@49323: val unescape_metas = map unescape_meta o space_explode " "
blanchet@49266: 
blanchet@49326: val explode_suggs =
blanchet@49326:   space_explode " " #> filter_out (curry (op =) "") #> map unescape_meta
blanchet@49326: fun extract_query line =
blanchet@49326:   case space_explode ":" line of
blanchet@49326:     [goal_name, suggs] => (unescape_meta goal_name, explode_suggs suggs)
blanchet@49326:   | _ => ("", explode_suggs line)
blanchet@49326: 
blanchet@49326: fun find_suggested facts sugg =
blanchet@49326:   find_first (fn (_, th) => Thm.get_name_hint th = sugg) facts
blanchet@49326: fun suggested_facts suggs facts = map_filter (find_suggested facts) suggs
blanchet@49326: 
blanchet@49318: val thy_feature_prefix = "y_"
blanchet@49266: 
blanchet@49318: val thy_feature_name_of = prefix thy_feature_prefix
blanchet@49318: val const_name_of = prefix const_prefix
blanchet@49318: val type_name_of = prefix type_const_prefix
blanchet@49318: val class_name_of = prefix class_prefix
blanchet@49266: 
blanchet@49266: local
blanchet@49266: 
blanchet@49266: fun has_bool @{typ bool} = true
blanchet@49266:   | has_bool (Type (_, Ts)) = exists has_bool Ts
blanchet@49266:   | has_bool _ = false
blanchet@49266: 
blanchet@49266: fun has_fun (Type (@{type_name fun}, _)) = true
blanchet@49266:   | has_fun (Type (_, Ts)) = exists has_fun Ts
blanchet@49266:   | has_fun _ = false
blanchet@49266: 
blanchet@49266: val is_conn = member (op =)
blanchet@49266:   [@{const_name Trueprop}, @{const_name HOL.conj}, @{const_name HOL.disj},
blanchet@49266:    @{const_name HOL.implies}, @{const_name Not},
blanchet@49266:    @{const_name All}, @{const_name Ex}, @{const_name Ball}, @{const_name Bex},
blanchet@49266:    @{const_name HOL.eq}]
blanchet@49266: 
blanchet@49266: val has_bool_arg_const =
blanchet@49266:   exists_Const (fn (c, T) =>
blanchet@49266:                    not (is_conn c) andalso exists has_bool (binder_types T))
blanchet@49266: 
blanchet@49266: fun higher_inst_const thy (c, T) =
blanchet@49266:   case binder_types T of
blanchet@49266:     [] => false
blanchet@49266:   | Ts => length (binder_types (Sign.the_const_type thy c)) <> length Ts
blanchet@49266: 
blanchet@49266: val binders = [@{const_name All}, @{const_name Ex}]
blanchet@49266: 
blanchet@49266: in
blanchet@49266: 
blanchet@49266: fun is_fo_term thy t =
blanchet@49266:   let
blanchet@49266:     val t =
blanchet@49266:       t |> Envir.beta_eta_contract
blanchet@49266:         |> transform_elim_prop
blanchet@49266:         |> Object_Logic.atomize_term thy
blanchet@49266:   in
blanchet@49266:     Term.is_first_order binders t andalso
blanchet@49266:     not (exists_subterm (fn Var (_, T) => has_bool T orelse has_fun T
blanchet@49266:                           | _ => false) t orelse
blanchet@49266:          has_bool_arg_const t orelse exists_Const (higher_inst_const thy) t)
blanchet@49266:   end
blanchet@49266: 
blanchet@49266: end
blanchet@49266: 
blanchet@49317: fun interesting_terms_types_and_classes term_max_depth type_max_depth ts =
blanchet@49266:   let
blanchet@49266:     val bad_types = [@{type_name prop}, @{type_name bool}, @{type_name fun}]
blanchet@49266:     val bad_consts = atp_widely_irrelevant_consts
blanchet@49319:     fun add_classes @{sort type} = I
blanchet@49319:       | add_classes S = union (op =) (map class_name_of S)
blanchet@49266:     fun do_add_type (Type (s, Ts)) =
blanchet@49266:         (not (member (op =) bad_types s) ? insert (op =) (type_name_of s))
blanchet@49266:         #> fold do_add_type Ts
blanchet@49319:       | do_add_type (TFree (_, S)) = add_classes S
blanchet@49319:       | do_add_type (TVar (_, S)) = add_classes S
blanchet@49266:     fun add_type T = type_max_depth >= 0 ? do_add_type T
blanchet@49266:     fun mk_app s args =
blanchet@49266:       if member (op <>) args "" then s ^ "(" ^ space_implode "," args ^ ")"
blanchet@49266:       else s
blanchet@49266:     fun patternify ~1 _ = ""
blanchet@49266:       | patternify depth t =
blanchet@49266:         case strip_comb t of
blanchet@49266:           (Const (s, _), args) =>
blanchet@49266:           mk_app (const_name_of s) (map (patternify (depth - 1)) args)
blanchet@49266:         | _ => ""
blanchet@49266:     fun add_term_patterns ~1 _ = I
blanchet@49266:       | add_term_patterns depth t =
blanchet@49266:         insert (op =) (patternify depth t)
blanchet@49266:         #> add_term_patterns (depth - 1) t
blanchet@49266:     val add_term = add_term_patterns term_max_depth
blanchet@49266:     fun add_patterns t =
blanchet@49266:       let val (head, args) = strip_comb t in
blanchet@49266:         (case head of
blanchet@49266:            Const (s, T) =>
blanchet@49266:            not (member (op =) bad_consts s) ? (add_term t #> add_type T)
blanchet@49266:          | Free (_, T) => add_type T
blanchet@49266:          | Var (_, T) => add_type T
blanchet@49266:          | Abs (_, T, body) => add_type T #> add_patterns body
blanchet@49266:          | _ => I)
blanchet@49266:         #> fold add_patterns args
blanchet@49266:       end
blanchet@49317:   in [] |> fold add_patterns ts |> sort string_ord end
blanchet@49266: 
blanchet@49266: fun is_likely_tautology th =
blanchet@49317:   null (interesting_terms_types_and_classes 0 ~1 [prop_of th]) andalso
blanchet@49266:   not (Thm.eq_thm_prop (@{thm ext}, th))
blanchet@49266: 
blanchet@49266: fun is_too_meta thy th =
blanchet@49266:   fastype_of (Object_Logic.atomize_term thy (prop_of th)) <> @{typ bool}
blanchet@49266: 
blanchet@49314: fun all_non_tautological_facts_of thy css_table =
blanchet@49314:   all_facts_of thy css_table
blanchet@49266:   |> filter_out ((is_likely_tautology orf is_too_meta thy) o snd)
blanchet@49266: 
blanchet@49266: fun theory_ord p =
blanchet@49266:   if Theory.eq_thy p then EQUAL
blanchet@49266:   else if Theory.subthy p then LESS
blanchet@49266:   else if Theory.subthy (swap p) then GREATER
blanchet@49266:   else EQUAL
blanchet@49266: 
blanchet@49266: val thm_ord = theory_ord o pairself theory_of_thm
blanchet@49266: 
blanchet@49318: (* ### FIXME: optimize *)
blanchet@49318: fun thy_facts_from_thms ths =
blanchet@49318:   ths |> map (snd #> `(theory_of_thm #> Context.theory_name))
blanchet@49266:       |> AList.group (op =)
blanchet@49266:       |> sort (int_ord o pairself (length o Theory.ancestors_of o theory_of_thm
blanchet@49266:                                    o hd o snd))
blanchet@49318:       |> map (apsnd (sort (rev_order o thm_ord) #> map Thm.get_name_hint))
blanchet@49318:       |> Symtab.make
blanchet@49266: 
blanchet@49318: fun has_thy thy th =
blanchet@49318:   Context.theory_name thy = Context.theory_name (theory_of_thm th)
blanchet@49266: 
blanchet@49318: fun parent_facts thy thy_facts =
blanchet@49318:   let
blanchet@49318:     fun add_last thy =
blanchet@49318:       case Symtab.lookup thy_facts (Context.theory_name thy) of
blanchet@49318:         SOME (last_fact :: _) => insert (op =) last_fact
blanchet@49318:       | _ => add_parent thy
blanchet@49318:     and add_parent thy = fold add_last (Theory.parents_of thy)
blanchet@49318:   in add_parent thy [] end
blanchet@49266: 
blanchet@49266: fun is_exists (s, _) = (s = @{const_name Ex} orelse s = @{const_name Ex1})
blanchet@49266: 
blanchet@49312: val term_max_depth = 1
blanchet@49312: val type_max_depth = 1
blanchet@49266: 
blanchet@49266: (* TODO: Generate type classes for types? *)
blanchet@49317: fun features_of thy status ts =
blanchet@49318:   thy_feature_name_of (Context.theory_name thy) ::
blanchet@49317:   interesting_terms_types_and_classes term_max_depth type_max_depth ts
blanchet@49317:   |> exists (not o is_lambda_free) ts ? cons "lambdas"
blanchet@49317:   |> exists (exists_Const is_exists) ts ? cons "skolems"
blanchet@49317:   |> exists (not o is_fo_term thy) ts ? cons "ho"
blanchet@49317:   |> (case status of
blanchet@49317:         General => I
blanchet@49317:       | Induction => cons "induction"
blanchet@49317:       | Intro => cons "intro"
blanchet@49317:       | Inductive => cons "inductive"
blanchet@49317:       | Elim => cons "elim"
blanchet@49317:       | Simp => cons "simp"
blanchet@49317:       | Def => cons "def")
blanchet@49266: 
blanchet@49266: fun isabelle_dependencies_of all_facts =
blanchet@49318:   thms_in_proof (SOME all_facts) #> sort string_ord
blanchet@49266: 
blanchet@49266: val freezeT = Type.legacy_freeze_type
blanchet@49266: 
blanchet@49266: fun freeze (t $ u) = freeze t $ freeze u
blanchet@49266:   | freeze (Abs (s, T, t)) = Abs (s, freezeT T, freeze t)
blanchet@49266:   | freeze (Var ((s, _), T)) = Free (s, freezeT T)
blanchet@49266:   | freeze (Const (s, T)) = Const (s, freezeT T)
blanchet@49266:   | freeze (Free (s, T)) = Free (s, freezeT T)
blanchet@49266:   | freeze t = t
blanchet@49266: 
blanchet@49266: fun goal_of_thm thy = prop_of #> freeze #> cterm_of thy #> Goal.init
blanchet@49266: 
blanchet@49266: fun run_prover ctxt (params as {provers, ...}) facts goal =
blanchet@49266:   let
blanchet@49266:     val problem =
blanchet@49266:       {state = Proof.init ctxt, goal = goal, subgoal = 1, subgoal_count = 1,
blanchet@49304:        facts = facts |> map (apfst (apfst (fn name => name ())))
blanchet@49304:                      |> map Sledgehammer_Provers.Untranslated_Fact}
blanchet@49266:     val prover =
blanchet@49266:       Sledgehammer_Minimize.get_minimizing_prover ctxt
blanchet@49266:           Sledgehammer_Provers.Normal (hd provers)
blanchet@49266:   in prover params (K (K (K ""))) problem end
blanchet@49266: 
blanchet@49318: fun accessibility_of thy thy_facts =
blanchet@49318:   case Symtab.lookup thy_facts (Context.theory_name thy) of
blanchet@49318:     SOME (fact :: _) => [fact]
blanchet@49318:   | _ => parent_facts thy thy_facts
blanchet@49318: 
blanchet@49319: val thy_name_of_fact = hd o Long_Name.explode
blanchet@49266: 
blanchet@49266: 
blanchet@49317: (*** Low-level communication with MaSh ***)
blanchet@49317: 
blanchet@49326: fun run_mash ctxt save write_cmds read_preds =
blanchet@49326:   let
blanchet@49326:     val temp_dir = getenv "ISABELLE_TMP"
blanchet@49326:     val serial = serial_string ()
blanchet@49326:     val cmd_file = temp_dir ^ "/mash_commands." ^ serial
blanchet@49326:     val cmd_path = Path.explode cmd_file
blanchet@49326:     val pred_file = temp_dir ^ "/mash_preds." ^ serial
blanchet@49326:     val log_file = temp_dir ^ "/mash_log." ^ serial
blanchet@49326:     val command =
blanchet@49326:       getenv "MASH_HOME" ^ "/mash.py --inputFile " ^ cmd_file ^
blanchet@49326:       " --outputDir " ^ mash_dir () ^ " --predictions " ^ pred_file ^
blanchet@49326:       " --log " ^ log_file ^ (if save then " --saveModel" else "") ^
blanchet@49326:       " > /dev/null"
blanchet@49326:     val _ = File.write cmd_path ""
blanchet@49326:     val _ = write_cmds (File.append cmd_path)
blanchet@49326:     val _ = trace_msg ctxt (fn () => "  running " ^ command)
blanchet@49326:     val _ = Isabelle_System.bash command
blanchet@49326:   in read_preds (fn () => File.read_lines (Path.explode pred_file)) end
blanchet@49326: 
blanchet@49326: fun str_of_update (fact, access, feats, deps) =
blanchet@49326:   "! " ^ escape_meta fact ^ ": " ^ escape_metas access ^ "; " ^
blanchet@49326:   escape_metas feats ^ "; " ^ escape_metas deps ^ "\n"
blanchet@49326: 
blanchet@49326: fun str_of_query (access, feats) =
blanchet@49326:   "? " ^ escape_metas access ^ "; " ^ escape_metas feats
blanchet@49326: 
blanchet@49323: fun mash_RESET ctxt =
blanchet@49324:   let val path = mash_dir () |> Path.explode in
blanchet@49324:     trace_msg ctxt (K "MaSh RESET");
blanchet@49324:     File.fold_dir (fn file => fn () =>
blanchet@49324:                       File.rm (Path.append path (Path.basic file)))
blanchet@49324:                   path ()
blanchet@49324:   end
blanchet@49317: 
blanchet@49324: fun mash_ADD _ [] = ()
blanchet@49326:   | mash_ADD ctxt upds =
blanchet@49326:     (trace_msg ctxt (fn () => "MaSh ADD " ^ space_implode " " (map #1 upds));
blanchet@49326:      run_mash ctxt true (fn append => List.app (append o str_of_update) upds)
blanchet@49326:               (K ()))
blanchet@49317: 
blanchet@49323: fun mash_DEL ctxt facts feats =
blanchet@49323:   trace_msg ctxt (fn () =>
blanchet@49323:       "MaSh DEL " ^ escape_metas facts ^ "; " ^ escape_metas feats)
blanchet@49317: 
blanchet@49326: fun mash_QUERY ctxt (query as (_, feats)) =
blanchet@49326:   (trace_msg ctxt (fn () => "MaSh SUGGEST " ^ space_implode " " feats);
blanchet@49326:    run_mash ctxt false (fn append => append (str_of_query query))
blanchet@49326:                  (fn preds => snd (extract_query (List.last (preds ()))))
blanchet@49326:    handle List.Empty => [])
blanchet@49317: 
blanchet@49317: 
blanchet@49266: (*** High-level communication with MaSh ***)
blanchet@49266: 
blanchet@49316: type mash_state =
blanchet@49323:   {dirty_thys : unit Symtab.table,
blanchet@49316:    thy_facts : string list Symtab.table}
blanchet@49264: 
blanchet@49319: val empty_state =
blanchet@49323:   {dirty_thys = Symtab.empty,
blanchet@49316:    thy_facts = Symtab.empty}
blanchet@49316: 
blanchet@49316: local
blanchet@49316: 
blanchet@49316: fun mash_load (state as (true, _)) = state
blanchet@49316:   | mash_load _ =
blanchet@49324:     let val path = mash_state_path () in
blanchet@49317:       (true,
blanchet@49317:        case try File.read_lines path of
blanchet@49323:          SOME (dirty_line :: facts_lines) =>
blanchet@49317:          let
blanchet@49321:            fun dirty_thys_of_line line =
blanchet@49323:              Symtab.make (line |> unescape_metas |> map (rpair ()))
blanchet@49317:            fun add_facts_line line =
blanchet@49323:              case unescape_metas line of
blanchet@49317:                thy :: facts => Symtab.update_new (thy, facts)
blanchet@49317:              | _ => I (* shouldn't happen *)
blanchet@49317:          in
blanchet@49323:            {dirty_thys = dirty_thys_of_line dirty_line,
blanchet@49317:             thy_facts = fold add_facts_line facts_lines Symtab.empty}
blanchet@49317:          end
blanchet@49319:        | _ => empty_state)
blanchet@49317:     end
blanchet@49316: 
blanchet@49323: fun mash_save ({dirty_thys, thy_facts} : mash_state) =
blanchet@49316:   let
blanchet@49324:     val path = mash_state_path ()
blanchet@49323:     val dirty_line = (escape_metas (Symtab.keys dirty_thys)) ^ "\n"
blanchet@49318:     fun fact_line_for (thy, facts) = escape_metas (thy :: facts) ^ "\n"
blanchet@49316:   in
blanchet@49323:     File.write path dirty_line;
blanchet@49316:     Symtab.fold (fn thy_fact => fn () =>
blanchet@49323:                     File.append path (fact_line_for thy_fact)) thy_facts ()
blanchet@49316:   end
blanchet@49316: 
blanchet@49317: val global_state =
blanchet@49319:   Synchronized.var "Sledgehammer_Filter_MaSh.global_state" (false, empty_state)
blanchet@49316: 
blanchet@49316: in
blanchet@49316: 
blanchet@49321: fun mash_map f =
blanchet@49317:   Synchronized.change global_state (mash_load ##> (f #> tap mash_save))
blanchet@49316: 
blanchet@49319: fun mash_get () = Synchronized.change_result global_state (mash_load #> `snd)
blanchet@49317: 
blanchet@49323: fun mash_reset ctxt =
blanchet@49317:   Synchronized.change global_state (fn _ =>
blanchet@49324:       (mash_RESET ctxt; File.write (mash_state_path ()) "";
blanchet@49323:        (true, empty_state)))
blanchet@49316: 
blanchet@49316: end
blanchet@49316: 
blanchet@49323: fun mash_can_suggest_facts (_ : Proof.context) =
blanchet@49323:   not (Symtab.is_empty (#thy_facts (mash_get ())))
blanchet@49264: 
blanchet@49326: fun mash_suggest_facts ctxt params prover hyp_ts concl_t facts =
blanchet@49316:   let
blanchet@49317:     val thy = Proof_Context.theory_of ctxt
blanchet@49326:     val thy_facts = #thy_facts (mash_get ())
blanchet@49326:     val access = accessibility_of thy thy_facts
blanchet@49317:     val feats = features_of thy General (concl_t :: hyp_ts)
blanchet@49326:     val suggs = mash_QUERY ctxt (access, feats)
blanchet@49326:   in suggested_facts suggs facts end
blanchet@49264: 
blanchet@49323: fun mash_can_learn_thy (_ : Proof.context) thy =
blanchet@49321:   not (Symtab.defined (#dirty_thys (mash_get ())) (Context.theory_name thy))
blanchet@49264: 
blanchet@49319: fun is_fact_in_thy_facts thy_facts fact =
blanchet@49319:   case Symtab.lookup thy_facts (thy_name_of_fact fact) of
blanchet@49319:     SOME facts => member (op =) facts fact
blanchet@49319:   | NONE => false
blanchet@49319: 
blanchet@49321: fun zip_facts news [] = news
blanchet@49321:   | zip_facts [] olds = olds
blanchet@49321:   | zip_facts (new :: news) (old :: olds) =
blanchet@49321:     if new = old then
blanchet@49321:       new :: zip_facts news olds
blanchet@49321:     else if member (op =) news old then
blanchet@49321:       old :: zip_facts (filter_out (curry (op =) old) news) olds
blanchet@49321:     else if member (op =) olds new then
blanchet@49321:       new :: zip_facts news (filter_out (curry (op =) new) olds)
blanchet@49321:     else
blanchet@49321:       new :: old :: zip_facts news olds
blanchet@49321: 
blanchet@49321: fun add_thy_facts_from_thys new old =
blanchet@49321:   let
blanchet@49321:     fun add_thy (thy, new_facts) =
blanchet@49321:       case Symtab.lookup old thy of
blanchet@49321:         SOME old_facts => Symtab.update (thy, zip_facts old_facts new_facts)
blanchet@49321:       | NONE => Symtab.update_new (thy, new_facts)
blanchet@49321:   in old |> Symtab.fold add_thy new end
blanchet@49321: 
blanchet@49323: fun mash_learn_thy ctxt thy timeout =
blanchet@49319:   let
blanchet@49319:     val css_table = Sledgehammer_Fact.clasimpset_rule_table_of ctxt
blanchet@49319:     val facts = all_non_tautological_facts_of thy css_table
blanchet@49321:     val {thy_facts, ...} = mash_get ()
blanchet@49319:     fun is_old (_, th) = is_fact_in_thy_facts thy_facts (Thm.get_name_hint th)
blanchet@49319:     val (old_facts, new_facts) =
blanchet@49319:       facts |> List.partition is_old ||> sort (thm_ord o pairself snd)
blanchet@49323:   in
blanchet@49323:     if null new_facts then
blanchet@49323:       ()
blanchet@49323:     else
blanchet@49319:       let
blanchet@49323:         val ths = facts |> map snd
blanchet@49323:         val all_names = ths |> map Thm.get_name_hint
blanchet@49326:         fun do_fact ((_, (_, status)), th) (prevs, upds) =
blanchet@49323:           let
blanchet@49323:             val name = Thm.get_name_hint th
blanchet@49323:             val feats = features_of thy status [prop_of th]
blanchet@49323:             val deps = isabelle_dependencies_of all_names th
blanchet@49326:             val upd = (name, prevs, feats, deps)
blanchet@49326:           in ([name], upd :: upds) end
blanchet@49323:         val parents = parent_facts thy thy_facts
blanchet@49326:         val (_, upds) = (parents, []) |> fold do_fact new_facts
blanchet@49323:         val new_thy_facts = new_facts |> thy_facts_from_thms
blanchet@49323:         fun trans {dirty_thys, thy_facts} =
blanchet@49326:           (mash_ADD ctxt (rev upds);
blanchet@49323:            {dirty_thys = dirty_thys,
blanchet@49323:             thy_facts = thy_facts |> add_thy_facts_from_thys new_thy_facts})
blanchet@49323:       in mash_map trans end
blanchet@49323:   end
blanchet@49319: 
blanchet@49324: fun mash_learn_proof ctxt thy t ths =
blanchet@49324:   mash_map (fn state as {dirty_thys, thy_facts} =>
blanchet@49324:     let val deps = ths |> map Thm.get_name_hint in
blanchet@49324:       if forall (is_fact_in_thy_facts thy_facts) deps then
blanchet@49324:         let
blanchet@49324:           val fact = ATP_Util.timestamp () (* should be fairly fresh *)
blanchet@49324:           val access = accessibility_of thy thy_facts
blanchet@49324:           val feats = features_of thy General [t]
blanchet@49324:         in
blanchet@49324:           mash_ADD ctxt [(fact, access, feats, deps)];
blanchet@49324:           {dirty_thys = dirty_thys, thy_facts = thy_facts}
blanchet@49324:         end
blanchet@49324:       else
blanchet@49324:         state
blanchet@49324:     end)
blanchet@49264: 
blanchet@49308: fun relevant_facts ctxt params prover max_facts
blanchet@49313:         ({add, only, ...} : fact_override) hyp_ts concl_t facts =
blanchet@49303:   if only then
blanchet@49304:     facts
blanchet@49308:   else if max_facts <= 0 then
blanchet@49303:     []
blanchet@49303:   else
blanchet@49303:     let
blanchet@49303:       val add_ths = Attrib.eval_thms ctxt add
blanchet@49307:       fun prepend_facts ths accepts =
blanchet@49303:         ((facts |> filter (member Thm.eq_thm_prop ths o snd)) @
blanchet@49307:          (accepts |> filter_out (member Thm.eq_thm_prop ths o snd)))
blanchet@49308:         |> take max_facts
blanchet@49313:       val iter_facts =
blanchet@49313:         iterative_relevant_facts ctxt params prover max_facts NONE hyp_ts
blanchet@49313:                                  concl_t facts
blanchet@49326:       val (mash_facts, mash_antifacts) =
blanchet@49326:         facts |> mash_suggest_facts ctxt params prover hyp_ts concl_t
blanchet@49326:               |> chop max_facts
blanchet@49317:       val mesh_facts = iter_facts (* ### *)
blanchet@49303:     in
blanchet@49313:       mesh_facts
blanchet@49303:       |> not (null add_ths) ? prepend_facts add_ths
blanchet@49303:     end
blanchet@49303: 
blanchet@49263: end;