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@49266:   val fact_name_of : string -> string
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@49266:   val thms_by_thy : ('a * thm) list -> (string * thm list) list
blanchet@49266:   val has_thy : theory -> thm -> bool
blanchet@49311:   val parent_facts : (string * thm list) list -> theory -> 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@49314:   val generate_accessibility : Proof.context -> theory -> bool -> string -> unit
blanchet@49314:   val generate_features : Proof.context -> theory -> bool -> string -> unit
blanchet@49314:   val generate_isa_dependencies :
blanchet@49314:     Proof.context -> theory -> bool -> string -> unit
blanchet@49266:   val generate_atp_dependencies :
blanchet@49266:     Proof.context -> params -> theory -> bool -> string -> unit
blanchet@49317:   val mash_RESET : unit -> unit
blanchet@49317:   val mash_ADD : string -> string list -> string list -> string list -> unit
blanchet@49317:   val mash_DEL : string list -> string list -> unit
blanchet@49317:   val mash_SUGGEST : string list -> string list -> string list
blanchet@49313:   val mash_reset : unit -> unit
blanchet@49313:   val mash_can_suggest_facts : unit -> bool
blanchet@49313:   val mash_suggest_facts :
blanchet@49317:     Proof.context -> params -> string -> int -> term list -> term -> fact list
blanchet@49313:     -> fact list * fact list
blanchet@49313:   val mash_can_learn_thy : theory -> bool
blanchet@49313:   val mash_learn_thy : theory -> real -> unit
blanchet@49313:   val mash_learn_proof : 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@49316: val mash_dir = "mash"
blanchet@49316: val model_file = "model"
blanchet@49316: val state_file = "state"
blanchet@49316: 
blanchet@49317: fun mk_path file =
blanchet@49317:   getenv "ISABELLE_HOME_USER" ^ "/" ^ mash_dir ^ "/" ^ file
blanchet@49317:   |> Path.explode
blanchet@49316: 
blanchet@49317: val fresh_fact_prefix = Long_Name.separator
blanchet@49266: 
blanchet@49266: (*** Isabelle helpers ***)
blanchet@49266: 
blanchet@49266: fun escape_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@49266: val escape_meta = String.translate escape_meta_char
blanchet@49266: 
blanchet@49266: val thy_prefix = "y_"
blanchet@49266: 
blanchet@49266: val fact_name_of = escape_meta
blanchet@49266: val thy_name_of = prefix thy_prefix o escape_meta
blanchet@49266: val const_name_of = prefix const_prefix o escape_meta
blanchet@49266: val type_name_of = prefix type_const_prefix o escape_meta
blanchet@49266: val class_name_of = prefix class_prefix o escape_meta
blanchet@49266: 
blanchet@49266: val thy_name_of_thm = theory_of_thm #> Context.theory_name
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@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@49266:       | do_add_type (TFree (_, S)) = union (op =) (map class_name_of S)
blanchet@49266:       | do_add_type (TVar (_, S)) = union (op =) (map class_name_of 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@49266: fun thms_by_thy ths =
blanchet@49266:   ths |> map (snd #> `thy_name_of_thm)
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@49266:       |> map (apsnd (sort thm_ord))
blanchet@49266: 
blanchet@49266: fun has_thy thy th = (Context.theory_name thy = thy_name_of_thm th)
blanchet@49266: 
blanchet@49311: fun add_last_thms thy_ths thy =
blanchet@49311:   case AList.lookup (op =) thy_ths (Context.theory_name thy) of
blanchet@49311:     SOME (ths as _ :: _) => insert Thm.eq_thm (List.last ths)
blanchet@49311:   | _ => add_parent_thms thy_ths thy
blanchet@49311: and add_parent_thms thy_ths thy =
blanchet@49311:   fold (add_last_thms thy_ths) (Theory.parents_of thy)
blanchet@49311: 
blanchet@49311: fun parent_facts thy_ths thy =
blanchet@49311:   add_parent_thms thy_ths thy []
blanchet@49266:   |> map (fact_name_of o Thm.get_name_hint)
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@49317:   thy_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@49266:   thms_in_proof (SOME all_facts)
blanchet@49266:   #> map fact_name_of #> 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@49314: fun generate_accessibility ctxt thy include_thy file_name =
blanchet@49266:   let
blanchet@49266:     val path = file_name |> Path.explode
blanchet@49266:     val _ = File.write path ""
blanchet@49314:     val css_table = clasimpset_rule_table_of ctxt
blanchet@49266:     fun do_thm th prevs =
blanchet@49266:       let
blanchet@49266:         val s = th ^ ": " ^ space_implode " " prevs ^ "\n"
blanchet@49266:         val _ = File.append path s
blanchet@49266:       in [th] end
blanchet@49266:     val thy_ths =
blanchet@49314:       all_non_tautological_facts_of thy css_table
blanchet@49266:       |> not include_thy ? filter_out (has_thy thy o snd)
blanchet@49266:       |> thms_by_thy
blanchet@49266:     fun do_thy ths =
blanchet@49266:       let
blanchet@49266:         val thy = theory_of_thm (hd ths)
blanchet@49311:         val parents = parent_facts thy_ths thy
blanchet@49266:         val ths = ths |> map (fact_name_of o Thm.get_name_hint)
blanchet@49266:       in fold do_thm ths parents; () end
blanchet@49266:   in List.app (do_thy o snd) thy_ths end
blanchet@49266: 
blanchet@49314: fun generate_features ctxt thy include_thy file_name =
blanchet@49266:   let
blanchet@49266:     val path = file_name |> Path.explode
blanchet@49266:     val _ = File.write path ""
blanchet@49314:     val css_table = clasimpset_rule_table_of ctxt
blanchet@49266:     val facts =
blanchet@49314:       all_non_tautological_facts_of thy css_table
blanchet@49266:       |> not include_thy ? filter_out (has_thy thy o snd)
blanchet@49266:     fun do_fact ((_, (_, status)), th) =
blanchet@49266:       let
blanchet@49266:         val name = Thm.get_name_hint th
blanchet@49317:         val feats = features_of (theory_of_thm th) status [prop_of th]
blanchet@49266:         val s = fact_name_of name ^ ": " ^ space_implode " " feats ^ "\n"
blanchet@49266:       in File.append path s end
blanchet@49266:   in List.app do_fact facts end
blanchet@49266: 
blanchet@49314: fun generate_isa_dependencies ctxt thy include_thy file_name =
blanchet@49266:   let
blanchet@49266:     val path = file_name |> Path.explode
blanchet@49266:     val _ = File.write path ""
blanchet@49314:     val css_table = clasimpset_rule_table_of ctxt
blanchet@49266:     val ths =
blanchet@49314:       all_non_tautological_facts_of thy css_table
blanchet@49266:       |> not include_thy ? filter_out (has_thy thy o snd)
blanchet@49266:       |> map snd
blanchet@49266:     val all_names = ths |> map Thm.get_name_hint
blanchet@49266:     fun do_thm th =
blanchet@49266:       let
blanchet@49266:         val name = Thm.get_name_hint th
blanchet@49266:         val deps = isabelle_dependencies_of all_names th
blanchet@49266:         val s = fact_name_of name ^ ": " ^ space_implode " " deps ^ "\n"
blanchet@49266:       in File.append path s end
blanchet@49266:   in List.app do_thm ths end
blanchet@49266: 
blanchet@49308: fun generate_atp_dependencies ctxt (params as {provers, max_facts, ...}) thy
blanchet@49266:                               include_thy file_name =
blanchet@49266:   let
blanchet@49266:     val path = file_name |> Path.explode
blanchet@49266:     val _ = File.write path ""
blanchet@49314:     val css_table = clasimpset_rule_table_of ctxt
blanchet@49266:     val facts =
blanchet@49314:       all_non_tautological_facts_of thy css_table
blanchet@49266:       |> not include_thy ? filter_out (has_thy thy o snd)
blanchet@49266:     val ths = facts |> map snd
blanchet@49266:     val all_names = ths |> map Thm.get_name_hint
blanchet@49266:     fun is_dep dep (_, th) = fact_name_of (Thm.get_name_hint th) = dep
blanchet@49266:     fun add_isa_dep facts dep accum =
blanchet@49266:       if exists (is_dep dep) accum then
blanchet@49266:         accum
blanchet@49266:       else case find_first (is_dep dep) facts of
blanchet@49304:         SOME ((name, status), th) => accum @ [((name, status), th)]
blanchet@49266:       | NONE => accum (* shouldn't happen *)
blanchet@49266:     fun fix_name ((_, stature), th) =
blanchet@49304:       ((fn () => th |> Thm.get_name_hint |> fact_name_of, stature), th)
blanchet@49266:     fun do_thm th =
blanchet@49266:       let
blanchet@49266:         val name = Thm.get_name_hint th
blanchet@49266:         val goal = goal_of_thm thy th
blanchet@49307:         val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal 1
blanchet@49266:         val deps =
blanchet@49266:           case isabelle_dependencies_of all_names th of
blanchet@49266:             [] => []
blanchet@49266:           | isa_dep as [_] => isa_dep (* can hardly beat that *)
blanchet@49266:           | isa_deps =>
blanchet@49266:             let
blanchet@49266:               val facts =
blanchet@49266:                 facts |> filter (fn (_, th') => thm_ord (th', th) = LESS)
blanchet@49266:               val facts =
blanchet@49307:                 facts |> iterative_relevant_facts ctxt params (hd provers)
blanchet@49308:                              (the max_facts) NONE hyp_ts concl_t
blanchet@49266:                       |> fold (add_isa_dep facts) isa_deps
blanchet@49266:                       |> map fix_name
blanchet@49266:             in
blanchet@49266:               case run_prover ctxt params facts goal of
blanchet@49266:                 {outcome = NONE, used_facts, ...} =>
blanchet@49266:                 used_facts |> map fst |> sort string_ord
blanchet@49266:               | _ => isa_deps
blanchet@49266:             end
blanchet@49266:         val s = fact_name_of name ^ ": " ^ space_implode " " deps ^ "\n"
blanchet@49266:       in File.append path s end
blanchet@49266:   in List.app do_thm ths end
blanchet@49266: 
blanchet@49266: 
blanchet@49317: (*** Low-level communication with MaSh ***)
blanchet@49317: 
blanchet@49317: fun mash_RESET () = (warning "MaSh RESET"; File.rm (mk_path model_file))
blanchet@49317: 
blanchet@49317: fun mash_ADD fact access feats deps =
blanchet@49317:   warning ("MaSh ADD " ^ fact ^ ": " ^ space_implode " " access ^ "; " ^
blanchet@49317:            space_implode " " feats ^ "; " ^ space_implode " " deps)
blanchet@49317: 
blanchet@49317: fun mash_DEL facts feats =
blanchet@49317:   warning ("MaSh DEL " ^ space_implode " " facts ^ "; " ^
blanchet@49317:            space_implode " " feats)
blanchet@49317: 
blanchet@49317: fun mash_SUGGEST access feats =
blanchet@49317:   (warning ("MaSh SUGGEST " ^ space_implode " " access ^ "; " ^
blanchet@49317:             space_implode " " feats);
blanchet@49317:    [])
blanchet@49317: 
blanchet@49317: 
blanchet@49266: (*** High-level communication with MaSh ***)
blanchet@49266: 
blanchet@49316: type mash_state =
blanchet@49317:   {fresh : int,
blanchet@49317:    completed_thys : unit Symtab.table,
blanchet@49316:    thy_facts : string list Symtab.table}
blanchet@49264: 
blanchet@49316: val mash_zero =
blanchet@49317:   {fresh = 0,
blanchet@49317:    completed_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@49317:     let
blanchet@49317:       val path = mk_path state_file
blanchet@49317:       val _ = Isabelle_System.mkdir (path |> Path.dir)
blanchet@49317:     in
blanchet@49317:       (true,
blanchet@49317:        case try File.read_lines path of
blanchet@49317:          SOME (fresh_line :: comp_line :: facts_lines) =>
blanchet@49317:          let
blanchet@49317:            fun comp_thys_of_line comp_line =
blanchet@49317:              Symtab.make (comp_line |> space_explode " " |> map (rpair ()))
blanchet@49317:            fun add_facts_line line =
blanchet@49317:              case space_explode " " line of
blanchet@49317:                thy :: facts => Symtab.update_new (thy, facts)
blanchet@49317:              | _ => I (* shouldn't happen *)
blanchet@49317:          in
blanchet@49317:            {fresh = Int.fromString fresh_line |> the_default 0,
blanchet@49317:             completed_thys = comp_thys_of_line comp_line,
blanchet@49317:             thy_facts = fold add_facts_line facts_lines Symtab.empty}
blanchet@49317:          end
blanchet@49317:        | _ => mash_zero)
blanchet@49317:     end
blanchet@49316: 
blanchet@49317: fun mash_save ({fresh, completed_thys, thy_facts} : mash_state) =
blanchet@49316:   let
blanchet@49317:     val path = mk_path state_file
blanchet@49316:     val comp_line = (completed_thys |> Symtab.keys |> space_implode " ") ^ "\n"
blanchet@49316:     fun fact_line_for (thy, facts) = space_implode " " (thy :: facts) ^ "\n"
blanchet@49316:   in
blanchet@49317:     File.write path (string_of_int fresh ^ "\n" ^ comp_line);
blanchet@49316:     Symtab.fold (fn thy_fact => fn () =>
blanchet@49316:                     File.append path (fact_line_for thy_fact)) thy_facts
blanchet@49316:   end
blanchet@49316: 
blanchet@49317: val global_state =
blanchet@49317:   Synchronized.var "Sledgehammer_Filter_MaSh.global_state" (false, mash_zero)
blanchet@49316: 
blanchet@49316: in
blanchet@49316: 
blanchet@49316: fun mash_change f =
blanchet@49317:   Synchronized.change global_state (mash_load ##> (f #> tap mash_save))
blanchet@49316: 
blanchet@49317: fun mash_peek f = Synchronized.change global_state (mash_load ##> tap f)
blanchet@49317: 
blanchet@49317: fun mash_value () = Synchronized.change_result global_state (mash_load #> `snd)
blanchet@49317: 
blanchet@49317: fun mash_reset () =
blanchet@49317:   Synchronized.change global_state (fn _ =>
blanchet@49317:       (mash_RESET (); File.rm (mk_path state_file); (true, mash_zero)))
blanchet@49316: 
blanchet@49316: end
blanchet@49316: 
blanchet@49316: fun mash_can_suggest_facts () =
blanchet@49316:   not (Symtab.is_empty (#thy_facts (mash_value ())))
blanchet@49264: 
blanchet@49317: fun accessibility_of thy thy_facts =
blanchet@49317:   let
blanchet@49317:     val _ = 0
blanchet@49317:   in
blanchet@49317:     [] (*###*)
blanchet@49317:   end
blanchet@49317: 
blanchet@49313: fun mash_suggest_facts ctxt params prover max_facts hyp_ts concl_t facts =
blanchet@49316:   let
blanchet@49317:     val thy = Proof_Context.theory_of ctxt
blanchet@49317:     val access = accessibility_of thy (#thy_facts (mash_value ()))
blanchet@49317:     val feats = features_of thy General (concl_t :: hyp_ts)
blanchet@49316:     val suggs = mash_SUGGEST access feats
blanchet@49316:   in (facts, []) end
blanchet@49264: 
blanchet@49316: fun mash_can_learn_thy thy =
blanchet@49316:   not (Symtab.defined (#completed_thys (mash_value ()))
blanchet@49316:                       (Context.theory_name thy))
blanchet@49264: 
blanchet@49313: fun mash_learn_thy thy timeout = ()
blanchet@49317: (* ### *)
blanchet@49313: 
blanchet@49317: fun mash_learn_proof thy t ths =
blanchet@49317:   mash_change (fn {fresh, completed_thys, thy_facts} =>
blanchet@49317:     let
blanchet@49317:       val fact = fresh_fact_prefix ^ string_of_int fresh
blanchet@49317:       val access = accessibility_of thy thy_facts
blanchet@49317:       val feats = features_of thy General [t]
blanchet@49317:       val deps = ths |> map (fact_name_of o Thm.get_name_hint)
blanchet@49317:     in
blanchet@49317:       mash_ADD fact access feats deps;
blanchet@49317:       {fresh = fresh + 1, completed_thys = completed_thys,
blanchet@49317:        thy_facts = thy_facts}
blanchet@49317:     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@49313:       val (mash_facts, mash_rejected) =
blanchet@49313:         mash_suggest_facts ctxt params prover max_facts hyp_ts concl_t 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;