diff --git a/src/HOL/TPTP/MaSh_Export_Base.thy b/src/HOL/TPTP/MaSh_Export_Base.thy --- a/src/HOL/TPTP/MaSh_Export_Base.thy +++ b/src/HOL/TPTP/MaSh_Export_Base.thy @@ -1,42 +1,41 @@ (* Title: HOL/TPTP/MaSh_Export_Base.thy Author: Jasmin Blanchette, TU Muenchen *) section \MaSh Exporter Base\ theory MaSh_Export_Base imports Main begin ML_file \mash_export.ML\ sledgehammer_params [provers = spass, max_facts = 32, strict, dont_slice, type_enc = mono_native, lam_trans = lifting, timeout = 2, dont_preplay, minimize] declare [[sledgehammer_fact_duplicates = true]] -declare [[sledgehammer_instantiate_inducts = false]] hide_fact (open) HOL.ext ML \ Multithreading.max_threads () \ ML \ open MaSh_Export \ ML \ val do_it = false (* switch to "true" to generate the files *) val thys = [\<^theory>\List\] val params as {provers, ...} = Sledgehammer_Commands.default_params \<^theory> [] val prover = hd provers val range = (1, NONE) val step = 1 val max_suggestions = 1024 val dir = "List" val prefix = "/tmp/" ^ dir ^ "/" \ end diff --git a/src/HOL/TPTP/atp_theory_export.ML b/src/HOL/TPTP/atp_theory_export.ML --- a/src/HOL/TPTP/atp_theory_export.ML +++ b/src/HOL/TPTP/atp_theory_export.ML @@ -1,365 +1,365 @@ (* Title: HOL/TPTP/atp_theory_export.ML Author: Jasmin Blanchette, TU Muenchen Copyright 2011 Export Isabelle theories as first-order TPTP inferences. *) signature ATP_THEORY_EXPORT = sig type atp_format = ATP_Problem.atp_format datatype inference_policy = No_Inferences | Unchecked_Inferences | Checked_Inferences val generate_atp_inference_file_for_theory : Proof.context -> theory -> atp_format -> inference_policy -> string -> string -> unit val generate_casc_lbt_isa_files_for_theory : Proof.context -> theory -> atp_format -> inference_policy -> string -> string -> unit end; structure ATP_Theory_Export : ATP_THEORY_EXPORT = struct open ATP_Problem open ATP_Proof open ATP_Problem_Generate open Sledgehammer_ATP_Systems val max_dependencies = 100 val max_facts = 512 val atp_timeout = seconds 0.5 datatype inference_policy = No_Inferences | Unchecked_Inferences | Checked_Inferences val prefix = Library.prefix val fact_name_of = prefix fact_prefix o ascii_of fun atp_of_format (THF (_, Polymorphic, _)) = leo3N | atp_of_format (THF (_, Monomorphic, _)) = satallaxN | atp_of_format (DFG Polymorphic) = pirateN | atp_of_format (DFG Monomorphic) = spassN | atp_of_format (TFF (_, Polymorphic)) = alt_ergoN | atp_of_format (TFF (_, Monomorphic)) = vampireN | atp_of_format FOF = eN (* FIXME? *) | atp_of_format CNF_UEQ = waldmeisterN | atp_of_format CNF = eN (* FIXME? *) fun run_atp ctxt format problem = let val thy = Proof_Context.theory_of ctxt val prob_file = File.tmp_path (Path.explode "prob") val atp = atp_of_format format val {exec, arguments, proof_delims, known_failures, ...} = get_atp thy atp () val ord = effective_term_order ctxt atp val _ = problem |> lines_of_atp_problem format ord (K []) |> File.write_list prob_file val path = getenv (List.last (fst exec)) ^ "/" ^ List.last (snd exec) val command = space_implode " " (File.bash_path (Path.explode path) :: arguments ctxt false "" atp_timeout prob_file (ord, K [], K [])) val outcome = Timeout.apply atp_timeout Isabelle_System.bash_output command |> fst |> extract_tstplike_proof_and_outcome false proof_delims known_failures |> snd handle Timeout.TIMEOUT _ => SOME TimedOut val _ = tracing ("Ran ATP: " ^ (case outcome of NONE => "Success" | SOME failure => string_of_atp_failure failure)) in outcome end fun is_problem_line_reprovable ctxt format prelude axioms deps (Formula (ident', _, phi, _, _)) = is_none (run_atp ctxt format ((factsN, Formula (ident', Conjecture, phi, NONE, []) :: map_filter (Symtab.lookup axioms) deps) :: prelude)) | is_problem_line_reprovable _ _ _ _ _ _ = false fun inference_term _ [] = NONE | inference_term check_infs ss = ATerm (("inference", []), [ATerm (("checked_isabelle" |> not check_infs ? prefix "un", []), []), ATerm ((tptp_empty_list, []), []), ATerm ((tptp_empty_list, []), map (fn s => ATerm ((s, []), [])) ss)]) |> SOME fun add_inferences_to_problem_line ctxt format check_infs prelude axioms infers (line as Formula ((ident, alt), Axiom, phi, NONE, info)) = let val deps = case these (AList.lookup (op =) infers ident) of [] => [] | deps => if check_infs andalso not (is_problem_line_reprovable ctxt format prelude axioms deps line) then [] else deps in Formula ((ident, alt), Lemma, phi, inference_term check_infs deps, info) end | add_inferences_to_problem_line _ _ _ _ _ _ line = line fun add_inferences_to_problem ctxt format check_infs prelude infers problem = let fun add_if_axiom (axiom as Formula ((ident, _), Axiom, _, _, _)) = Symtab.default (ident, axiom) | add_if_axiom _ = I val add_axioms_of_problem = fold (fold add_if_axiom o snd) val axioms = Symtab.empty |> check_infs ? add_axioms_of_problem problem in map (apsnd (map (add_inferences_to_problem_line ctxt format check_infs prelude axioms infers))) problem end fun ident_of_problem_line (Class_Decl (ident, _, _)) = ident | ident_of_problem_line (Type_Decl (ident, _, _)) = ident | ident_of_problem_line (Sym_Decl (ident, _, _)) = ident | ident_of_problem_line (Class_Memb (ident, _, _, _)) = ident | ident_of_problem_line (Formula ((ident, _), _, _, _, _)) = ident fun order_facts ord = sort (ord o apply2 ident_of_problem_line) fun order_problem_facts _ [] = [] | order_problem_facts ord ((heading, lines) :: problem) = if heading = factsN then (heading, order_facts ord lines) :: problem else (heading, lines) :: order_problem_facts ord problem (* A fairly random selection of types used for monomorphizing. *) val ground_types = [\<^typ>\nat\, HOLogic.intT, HOLogic.realT, \<^typ>\nat => bool\, \<^typ>\bool\, \<^typ>\unit\] fun ground_type_of_tvar _ [] tvar = raise TYPE ("ground_type_of_tvar", [TVar tvar], []) | ground_type_of_tvar thy (T :: Ts) tvar = if can (Sign.typ_match thy (TVar tvar, T)) Vartab.empty then T else ground_type_of_tvar thy Ts tvar fun monomorphize_term ctxt t = let val thy = Proof_Context.theory_of ctxt in t |> map_types (map_type_tvar (ground_type_of_tvar thy ground_types)) handle TYPE _ => \<^prop>\True\ end fun heading_sort_key heading = if String.isPrefix factsN heading then "_" ^ heading else heading fun problem_of_theory ctxt thy format infer_policy type_enc = let val css_table = Sledgehammer_Fact.clasimpset_rule_table_of ctxt val type_enc = type_enc |> type_enc_of_string Non_Strict |> adjust_type_enc format val mono = not (is_type_enc_polymorphic type_enc) val facts = - Sledgehammer_Fact.all_facts (Proof_Context.init_global thy) true false - Keyword.empty_keywords [] [] css_table + Sledgehammer_Fact.all_facts (Proof_Context.init_global thy) true Keyword.empty_keywords [] [] + css_table |> sort (Sledgehammer_MaSh.crude_thm_ord ctxt o apply2 snd) val problem = facts |> map (fn ((_, loc), th) => ((Thm.get_name_hint th, loc), th |> Thm.prop_of |> mono ? monomorphize_term ctxt)) |> generate_atp_problem ctxt true format Axiom type_enc Exporter combsN false false true [] \<^prop>\False\ |> #1 |> sort_by (heading_sort_key o fst) val prelude = fst (split_last problem) val name_tabs = Sledgehammer_Fact.build_name_tables Thm.get_name_hint facts val infers = if infer_policy = No_Inferences then [] else facts |> map (fn (_, th) => (fact_name_of (Thm.get_name_hint th), th |> Sledgehammer_Util.thms_in_proof max_dependencies (SOME name_tabs) |> these |> map fact_name_of)) val all_problem_names = problem |> maps (map ident_of_problem_line o snd) |> distinct (op =) val all_problem_name_set = Symtab.make (map (rpair ()) all_problem_names) val infers = infers |> filter (Symtab.defined all_problem_name_set o fst) |> map (apsnd (filter (Symtab.defined all_problem_name_set))) val maybe_add_edge = perhaps o try o String_Graph.add_edge_acyclic val ordered_names = String_Graph.empty |> fold (String_Graph.new_node o rpair ()) all_problem_names |> fold (fn (to, froms) => fold (fn from => maybe_add_edge (from, to)) froms) infers |> fold (fn (to, from) => maybe_add_edge (from, to)) (tl all_problem_names ~~ fst (split_last all_problem_names)) |> String_Graph.topological_order val order_tab = Symtab.empty |> fold (Symtab.insert (op =)) (ordered_names ~~ (1 upto length ordered_names)) val name_ord = int_ord o apply2 (the o Symtab.lookup order_tab) in (facts, problem |> (case format of DFG _ => I | _ => add_inferences_to_problem ctxt format (infer_policy = Checked_Inferences) prelude infers) |> order_problem_facts name_ord) end fun lines_of_problem ctxt format = lines_of_atp_problem format (effective_term_order ctxt eN (* dummy *)) (K []) fun write_lines path ss = let val _ = File.write path "" val _ = app (File.append path) ss in () end fun generate_atp_inference_file_for_theory ctxt thy format infer_policy type_enc file_name = let val (_, problem) = problem_of_theory ctxt thy format infer_policy type_enc val ss = lines_of_problem ctxt format problem in write_lines (Path.explode file_name) ss end fun ap dir = Path.append dir o Path.explode fun chop_maximal_groups eq xs = let val rev_xs = rev xs fun chop_group _ [] = [] | chop_group n (xs as x :: _) = let val n' = find_index (curry eq x) rev_xs val (ws', xs') = chop (n - n') xs in ws' :: chop_group n' xs' end in chop_group (length xs) xs end fun theory_name_of_fact (Formula ((_, alt), _, _, _, _)) = (case first_field Long_Name.separator alt of NONE => alt | SOME (thy, _) => thy) | theory_name_of_fact _ = "" val problem_suffix = ".p" val suggestion_suffix = ".sugg" val include_suffix = ".ax" val file_order_name = "FilesInProcessingOrder" val problem_order_name = "ProblemsInProcessingOrder" val problem_name = "problems" val suggestion_name = "suggestions" val include_name = "incl" val prelude_base_name = "prelude" val prelude_name = prelude_base_name ^ include_suffix val encode_meta = Sledgehammer_MaSh.encode_str fun include_base_name_of_fact x = encode_meta (theory_name_of_fact x) fun include_line base_name = "include('" ^ include_name ^ "/" ^ base_name ^ include_suffix ^ "').\n" val hol_base_name = encode_meta "HOL" fun should_generate_problem thy base_name (Formula ((_, alt), _, _, _, _)) = (case try (Global_Theory.get_thm thy) alt of SOME th => (* This is a crude hack to detect theorems stated and proved by the user (as opposed to those derived by various packages). In addition, we leave out everything in "HOL" as too basic to be interesting. *) Thm.legacy_get_kind th <> "" andalso base_name <> hol_base_name | NONE => false) (* Convention: theoryname__goalname *) fun problem_name_of base_name n alt = base_name ^ "__" ^ string_of_int n ^ "_" ^ perhaps (try (unprefix (base_name ^ "_"))) alt ^ problem_suffix fun suggestion_name_of base_name n alt = base_name ^ "__" ^ string_of_int n ^ "_" ^ perhaps (try (unprefix (base_name ^ "_"))) alt ^ suggestion_suffix fun generate_casc_lbt_isa_files_for_theory ctxt thy format infer_policy type_enc dir_name = let val dir = Isabelle_System.make_directory (Path.explode dir_name) val file_order_path = ap dir file_order_name val _ = File.write file_order_path "" val problem_order_path = ap dir problem_order_name val _ = File.write problem_order_path "" val problem_dir = Isabelle_System.make_directory (ap dir problem_name) val suggestion_dir = Isabelle_System.make_directory (ap dir suggestion_name) val include_dir = Isabelle_System.make_directory (ap problem_dir include_name) val (facts, (prelude, groups)) = problem_of_theory ctxt thy format infer_policy type_enc ||> split_last ||> apsnd (snd #> chop_maximal_groups (op = o apply2 theory_name_of_fact) #> map (`(include_base_name_of_fact o hd))) val fact_tab = Symtab.make (map (fn fact as (_, th) => (Thm.get_name_hint th, fact)) facts) fun write_prelude () = let val ss = lines_of_problem ctxt format prelude in File.append file_order_path (prelude_base_name ^ "\n"); write_lines (ap include_dir prelude_name) ss end fun write_include_file (base_name, fact_lines) = let val name = base_name ^ include_suffix val ss = lines_of_problem ctxt format [(factsN, fact_lines)] in File.append file_order_path (base_name ^ "\n"); write_lines (ap include_dir name) ss end fun select_facts_for_fact facts fact = let val (hyp_ts, conj_t) = Logic.strip_horn (Thm.prop_of (snd fact)) val mepo = Sledgehammer_MePo.mepo_suggested_facts ctxt (Sledgehammer_Commands.default_params thy []) max_facts NONE hyp_ts conj_t facts in map (suffix "\n" o fact_name_of o Thm.get_name_hint o snd) mepo end fun write_problem_files _ _ _ _ [] = () | write_problem_files _ seen_facts includes [] groups = write_problem_files 1 seen_facts includes includes groups | write_problem_files n seen_facts includes _ ((base_name, []) :: groups) = write_problem_files n seen_facts (includes @ [include_line base_name]) [] groups | write_problem_files n seen_facts includes seen_ss ((base_name, fact_line :: fact_lines) :: groups) = let val (alt, pname, sname, conj) = (case fact_line of Formula ((ident, alt), _, phi, _, _) => (alt, problem_name_of base_name n (encode_meta alt), suggestion_name_of base_name n (encode_meta alt), Formula ((ident, alt), Conjecture, phi, NONE, []))) val fact = the (Symtab.lookup fact_tab alt) val fact_s = tptp_string_of_line format fact_line in (if should_generate_problem thy base_name fact_line then let val conj_s = tptp_string_of_line format conj in File.append problem_order_path (pname ^ "\n"); write_lines (ap problem_dir pname) (seen_ss @ [conj_s]); write_lines (ap suggestion_dir sname) (select_facts_for_fact facts fact) end else (); write_problem_files (n + 1) (fact :: seen_facts) includes (seen_ss @ [fact_s]) ((base_name, fact_lines) :: groups)) end val _ = write_prelude () val _ = app write_include_file groups val _ = write_problem_files 1 [] [include_line prelude_base_name] [] groups in () end end; diff --git a/src/HOL/TPTP/mash_eval.ML b/src/HOL/TPTP/mash_eval.ML --- a/src/HOL/TPTP/mash_eval.ML +++ b/src/HOL/TPTP/mash_eval.ML @@ -1,169 +1,170 @@ (* Title: HOL/TPTP/mash_eval.ML Author: Jasmin Blanchette, TU Muenchen Copyright 2012 Evaluate proof suggestions from MaSh (Machine-learning for Sledgehammer). *) signature MASH_EVAL = sig type params = Sledgehammer_Prover.params val evaluate_mash_suggestions : Proof.context -> params -> int * int option -> string option -> string list -> string -> unit end; structure MaSh_Eval : MASH_EVAL = struct open Sledgehammer_Util open Sledgehammer_Fact open Sledgehammer_MePo open Sledgehammer_MaSh open Sledgehammer_Prover open Sledgehammer_Prover_ATP open Sledgehammer_Commands open MaSh_Export val prefix = Library.prefix fun evaluate_mash_suggestions ctxt params range prob_dir_name file_names report_file_name = let val thy = Proof_Context.theory_of ctxt val zeros = [0, 0, 0, 0, 0, 0] val report_path = report_file_name |> Path.explode val _ = File.write report_path "" fun print s = File.append report_path (s ^ "\n") - val {provers, max_facts, slice, type_enc, lam_trans, timeout, ...} = default_params thy [] + val {provers, max_facts, slice, type_enc, lam_trans, timeout, induction_rules, ...} = + default_params thy [] val prover = hd provers val max_suggs = generous_max_suggestions (the max_facts) + val inst_inducts = induction_rules = SOME Instantiate val method_of_file_name = perhaps (try (unsuffix "_suggestions")) o List.last o space_explode "/" val methods = "isar" :: map method_of_file_name file_names val lines_of = Path.explode #> try File.read_lines #> these val liness0 = map lines_of file_names val num_lines = fold (Integer.max o length) liness0 0 fun pad lines = lines @ replicate (num_lines - length lines) "" val liness' = Ctr_Sugar_Util.transpose (map pad liness0) val css = clasimpset_rule_table_of ctxt - val facts = all_facts ctxt true false Keyword.empty_keywords [] [] css + val facts = all_facts ctxt true Keyword.empty_keywords [] [] css val name_tabs = build_name_tables nickname_of_thm facts fun with_index facts s = (find_index (curry (op =) s) facts + 1, s) fun index_str (j, s) = s ^ "@" ^ string_of_int j val str_of_method = enclose " " ": " fun str_of_result method facts ({outcome, run_time, used_facts, ...} : prover_result) = let val facts = facts |> map (fst o fst) in str_of_method method ^ (if is_none outcome then "Success (" ^ ATP_Util.string_of_time run_time ^ "): " ^ (used_facts |> map (with_index facts o fst) |> sort (int_ord o apply2 fst) |> map index_str |> space_implode " ") ^ (if length facts < the max_facts then " (of " ^ string_of_int (length facts) ^ ")" else "") else "Failure: " ^ (facts |> take (the max_facts) |> tag_list 1 |> map index_str |> space_implode " ")) end fun solve_goal (j, lines) = if in_range range j andalso exists (curry (op <>) "") lines then let val get_suggs = extract_suggestions ##> (take max_suggs #> map fst) val (names, suggss0) = split_list (map get_suggs lines) val name = (case names |> filter (curry (op <>) "") |> distinct (op =) of [name] => name | names => error ("Input files out of sync: facts " ^ commas (map quote names))) val th = case find_first (fn (_, th) => nickname_of_thm th = name) facts of SOME (_, th) => th | NONE => error ("No fact called \"" ^ name) val goal = goal_of_thm (Proof_Context.theory_of ctxt) th val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal goal 1 ctxt val isar_deps = these (isar_dependencies_of name_tabs th) val suggss = isar_deps :: suggss0 val facts = facts |> filter (fn (_, th') => thm_less (th', th)) (* adapted from "mirabelle_sledgehammer.ML" *) fun set_file_name method (SOME dir) = let val prob_prefix = "goal_" ^ string_of_int j ^ "__" ^ encode_str name ^ "__" ^ method in Config.put atp_dest_dir dir #> Config.put atp_problem_prefix (prob_prefix ^ "__") #> Config.put SMT_Config.debug_files (dir ^ "/" ^ prob_prefix) end | set_file_name _ NONE = I fun prove method suggs = if null facts then (str_of_method method ^ "Skipped", 0) else let fun nickify ((_, stature), th) = ((K (encode_str (nickname_of_thm th)), stature), th) val facts = suggs |> find_suggested_facts ctxt facts |> map (fact_of_raw_fact #> nickify) - |> maybe_instantiate_inducts ctxt hyp_ts concl_t + |> inst_inducts ? instantiate_inducts ctxt hyp_ts concl_t |> take (the max_facts) |> map fact_of_raw_fact val ctxt = ctxt |> set_file_name method prob_dir_name val res as {outcome, ...} = run_prover_for_mash ctxt params prover name facts goal val ok = if is_none outcome then 1 else 0 in (str_of_result method facts res, ok) end val ress = map2 prove methods suggss in "Goal " ^ string_of_int j ^ ": " ^ name :: map fst ress |> cat_lines |> print; map snd ress end else zeros - val inst_inducts = Config.get ctxt instantiate_inducts val options = ["prover = " ^ prover, "max_facts = " ^ string_of_int (the max_facts), "slice" |> not slice ? prefix "dont_", "type_enc = " ^ the_default "smart" type_enc, "lam_trans = " ^ the_default "smart" lam_trans, "timeout = " ^ ATP_Util.string_of_time timeout, "instantiate_inducts" |> not inst_inducts ? prefix "dont_"] val _ = print " * * *"; val _ = print ("Options: " ^ commas options); val oks = Par_List.map solve_goal (tag_list 1 liness') val n = length oks fun total_of method ok = str_of_method method ^ string_of_int ok ^ " (" ^ Real.fmt (StringCvt.FIX (SOME 1)) (100.0 * Real.fromInt ok / Real.fromInt (Int.max (1, n))) ^ "%)" val oks' = if n = 0 then zeros else map Integer.sum (map_transpose I oks) in "Successes (of " ^ string_of_int n ^ " goals)" :: map2 total_of methods oks' |> cat_lines |> print end end; diff --git a/src/HOL/TPTP/mash_export.ML b/src/HOL/TPTP/mash_export.ML --- a/src/HOL/TPTP/mash_export.ML +++ b/src/HOL/TPTP/mash_export.ML @@ -1,328 +1,328 @@ (* Title: HOL/TPTP/mash_export.ML Author: Jasmin Blanchette, TU Muenchen Copyright 2012 Export Isabelle theory information for MaSh (Machine-learning for Sledgehammer). *) signature MASH_EXPORT = sig type params = Sledgehammer_Prover.params val in_range : int * int option -> int -> bool val extract_suggestions : string -> string * (string * real) list val generate_accessibility : Proof.context -> theory list -> string -> unit val generate_features : Proof.context -> theory list -> string -> unit val generate_isar_dependencies : Proof.context -> int * int option -> theory list -> string -> unit val generate_prover_dependencies : Proof.context -> params -> int * int option -> theory list -> string -> unit val generate_isar_commands : Proof.context -> string -> (int * int option) * int -> theory list -> int -> string -> unit val generate_prover_commands : Proof.context -> params -> (int * int option) * int -> theory list -> int -> string -> unit val generate_mepo_suggestions : Proof.context -> params -> (int * int option) * int -> theory list -> int -> string -> unit val generate_mash_suggestions : string -> Proof.context -> params -> (int * int option) * int -> theory list -> int -> string -> unit val generate_mesh_suggestions : int -> string -> string -> string -> unit end; structure MaSh_Export : MASH_EXPORT = struct open Sledgehammer_Fact open Sledgehammer_Prover_ATP open Sledgehammer_MePo open Sledgehammer_MaSh fun in_range (from, to) j = j >= from andalso (to = NONE orelse j <= the to) fun encode_feature (names, weight) = encode_str names ^ (if Real.== (weight, 1.0) then "" else "=" ^ Real.toString weight) val encode_features = map encode_feature #> space_implode " " (* The suggested weights do not make much sense. *) fun extract_suggestion sugg = (case space_explode "=" sugg of [name, weight] => SOME (decode_str name, Real.fromString weight |> the_default 1.0) | [name] => SOME (decode_str name, 1.0) | _ => NONE) fun extract_suggestions line = (case space_explode ":" line of [goal, suggs] => (decode_str goal, map_filter extract_suggestion (space_explode " " suggs)) | _ => ("", [])) fun has_thm_thy th thy = Context.theory_name thy = Thm.theory_name th fun has_thys thys th = exists (has_thm_thy th) thys fun all_facts ctxt = let val css = Sledgehammer_Fact.clasimpset_rule_table_of ctxt in - Sledgehammer_Fact.all_facts ctxt true false Keyword.empty_keywords [] [] css + Sledgehammer_Fact.all_facts ctxt true Keyword.empty_keywords [] [] css |> sort (crude_thm_ord ctxt o apply2 snd) end fun filter_accessible_from th = filter (fn (_, th') => thm_less (th', th)) fun generate_accessibility ctxt thys file_name = let val path = Path.explode file_name fun do_fact (parents, fact) = let val s = encode_str fact ^ ": " ^ encode_strs parents ^ "\n" in File.append path s end val facts = all_facts ctxt |> filter_out (has_thys thys o snd) |> attach_parents_to_facts [] |> map (apsnd (nickname_of_thm o snd)) in File.write path ""; List.app do_fact facts end fun generate_features ctxt thys file_name = let val path = Path.explode file_name val _ = File.write path "" val facts = all_facts ctxt |> filter_out (has_thys thys o snd) fun do_fact ((_, stature), th) = let val name = nickname_of_thm th val feats = features_of ctxt (Thm.theory_name th) stature [Thm.prop_of th] val s = encode_str name ^ ": " ^ encode_strs (sort string_ord feats) ^ "\n" in File.append path s end in List.app do_fact facts end val prover_marker = "$a" val isar_marker = "$i" val omitted_marker = "$o" val unprovable_marker = "$u" (* axiom or definition or characteristic theorem *) val prover_failed_marker = "$x" fun smart_dependencies_of ctxt params_opt facts name_tabs th isar_deps_opt = let val (marker, deps) = (case params_opt of SOME (params as {provers = prover :: _, ...}) => prover_dependencies_of ctxt params prover 0 facts name_tabs th |>> (fn true => prover_marker | false => prover_failed_marker) | NONE => let val deps = (case isar_deps_opt of NONE => isar_dependencies_of name_tabs th | deps => deps) in (case deps of NONE => (omitted_marker, []) | SOME [] => (unprovable_marker, []) | SOME deps => (isar_marker, deps)) end) in (case trim_dependencies deps of SOME deps => (marker, deps) | NONE => (omitted_marker, [])) end fun generate_isar_or_prover_dependencies ctxt params_opt range thys file_name = let val path = Path.explode file_name val facts = filter_out (has_thys thys o snd) (all_facts ctxt) val name_tabs = build_name_tables nickname_of_thm facts fun do_fact (j, (_, th)) = if in_range range j then let val name = nickname_of_thm th val _ = tracing ("Fact " ^ string_of_int j ^ ": " ^ name) val access_facts = filter_accessible_from th facts val (marker, deps) = smart_dependencies_of ctxt params_opt access_facts name_tabs th NONE in encode_str name ^ ": " ^ marker ^ " " ^ encode_strs deps ^ "\n" end else "" val lines = map do_fact (tag_list 1 facts) in File.write_list path lines end fun generate_isar_dependencies ctxt = generate_isar_or_prover_dependencies ctxt NONE fun generate_prover_dependencies ctxt params = generate_isar_or_prover_dependencies ctxt (SOME params) fun is_bad_query ctxt ho_atp step j th isar_deps = j mod step <> 0 orelse Thm.legacy_get_kind th = "" orelse null (the_list isar_deps) orelse - is_blacklisted_or_something ctxt ho_atp (Thm.get_name_hint th) + is_blacklisted_or_something (Thm.get_name_hint th) fun generate_isar_or_prover_commands ctxt prover params_opt (range, step) thys max_suggs file_name = let val ho_atp = is_ho_atp ctxt prover val path = Path.explode file_name val facts = all_facts ctxt val (new_facts, old_facts) = facts |> List.partition (has_thys thys o snd) val name_tabs = build_name_tables nickname_of_thm facts fun do_fact (j, (name, (parents, ((_, stature), th)))) = if in_range range j then let val _ = tracing ("Fact " ^ string_of_int j ^ ": " ^ name) val isar_deps = isar_dependencies_of name_tabs th val do_query = not (is_bad_query ctxt ho_atp step j th isar_deps) val goal_feats = features_of ctxt (Thm.theory_name th) stature [Thm.prop_of th] val access_facts = filter_accessible_from th new_facts @ old_facts val (marker, deps) = smart_dependencies_of ctxt params_opt access_facts name_tabs th isar_deps fun extra_features_of (((_, stature), th), weight) = [Thm.prop_of th] |> features_of ctxt (Thm.theory_name th) stature |> map (rpair (weight * extra_feature_factor)) val query = if do_query then let val query_feats = new_facts |> drop (j - num_extra_feature_facts) |> take num_extra_feature_facts |> rev |> weight_facts_steeply |> map extra_features_of |> rpair (map (rpair 1.0) goal_feats) |-> fold (union (eq_fst (op =))) in "? " ^ string_of_int max_suggs ^ " # " ^ encode_str name ^ ": " ^ encode_strs parents ^ "; " ^ encode_features query_feats ^ "\n" end else "" val update = "! " ^ encode_str name ^ ": " ^ encode_strs parents ^ "; " ^ encode_strs goal_feats ^ "; " ^ marker ^ " " ^ encode_strs deps ^ "\n" in query ^ update end else "" val new_facts = new_facts |> attach_parents_to_facts old_facts |> map (`(nickname_of_thm o snd o snd)) val lines = map do_fact (tag_list 1 new_facts) in File.write_list path lines end fun generate_isar_commands ctxt prover = generate_isar_or_prover_commands ctxt prover NONE fun generate_prover_commands ctxt (params as {provers = prover :: _, ...}) = generate_isar_or_prover_commands ctxt prover (SOME params) fun generate_mepo_or_mash_suggestions mepo_or_mash_suggested_facts ctxt (params as {provers = prover :: _, ...}) (range, step) thys max_suggs file_name = let val ho_atp = is_ho_atp ctxt prover val path = Path.explode file_name val facts = all_facts ctxt val (new_facts, old_facts) = facts |> List.partition (has_thys thys o snd) val name_tabs = build_name_tables nickname_of_thm facts fun do_fact (j, ((_, th), old_facts)) = if in_range range j then let val name = nickname_of_thm th val _ = tracing ("Fact " ^ string_of_int j ^ ": " ^ name) val goal = goal_of_thm (Proof_Context.theory_of ctxt) th val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal goal 1 ctxt val isar_deps = isar_dependencies_of name_tabs th in if is_bad_query ctxt ho_atp step j th isar_deps then "" else let val suggs = old_facts |> filter_accessible_from th |> mepo_or_mash_suggested_facts ctxt (Thm.theory_name th) params max_suggs hyp_ts concl_t |> map (nickname_of_thm o snd) in encode_str name ^ ": " ^ encode_strs suggs ^ "\n" end end else "" fun accum x (yss as ys :: _) = (x :: ys) :: yss val old_factss = tl (fold accum new_facts [rev old_facts]) val lines = map do_fact (tag_list 1 (new_facts ~~ rev (map rev old_factss))) in File.write_list path lines end val generate_mepo_suggestions = generate_mepo_or_mash_suggestions (fn ctxt => fn _ => fn params => fn max_suggs => fn hyp_ts => fn concl_t => not (Config.get ctxt Sledgehammer_MaSh.duplicates) ? Sledgehammer_Fact.drop_duplicate_facts #> Sledgehammer_MePo.mepo_suggested_facts ctxt params max_suggs NONE hyp_ts concl_t) fun generate_mash_suggestions algorithm ctxt = (Options.put_default \<^system_option>\MaSh\ algorithm; Sledgehammer_MaSh.mash_unlearn ctxt; generate_mepo_or_mash_suggestions (fn ctxt => fn thy_name => fn params as {provers = prover :: _, ...} => fn max_suggs => fn hyp_ts => fn concl_t => tap (Sledgehammer_MaSh.mash_learn_facts ctxt params prover 2 false Sledgehammer_Util.one_year) #> Sledgehammer_MaSh.mash_suggested_facts ctxt thy_name params max_suggs hyp_ts concl_t #> fst) ctxt) fun generate_mesh_suggestions max_suggs mash_file_name mepo_file_name mesh_file_name = let val mesh_path = Path.explode mesh_file_name val _ = File.write mesh_path "" fun do_fact (mash_line, mepo_line) = let val (name, mash_suggs) = extract_suggestions mash_line ||> (map fst #> weight_facts_steeply) val (name', mepo_suggs) = extract_suggestions mepo_line ||> (map fst #> weight_facts_steeply) val _ = if name = name' then () else error "Input files out of sync" val mess = [(mepo_weight, (mepo_suggs, [])), (mash_weight, (mash_suggs, []))] val mesh_suggs = mesh_facts I (op =) max_suggs mess val mesh_line = encode_str name ^ ": " ^ encode_strs mesh_suggs ^ "\n" in File.append mesh_path mesh_line end val mash_lines = Path.explode mash_file_name |> File.read_lines val mepo_lines = Path.explode mepo_file_name |> File.read_lines in if length mash_lines = length mepo_lines then List.app do_fact (mash_lines ~~ mepo_lines) else warning "Skipped: MaSh file missing or out of sync with MePo file" end end;