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,170 +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, induction_rules, ...} = + val {provers, max_facts, slices, 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 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_problem_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_lazy_fact #> nickify) |> inst_inducts ? instantiate_inducts ctxt hyp_ts concl_t |> take (the max_facts) |> map fact_of_lazy_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 options = ["prover = " ^ prover, "max_facts = " ^ string_of_int (the max_facts), - "slice" |> not slice ? prefix "dont_", + "slices = " ^ string_of_int slices, "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,326 @@ (* 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 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 = +fun is_bad_query ctxt 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 (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 do_query = not (is_bad_query ctxt 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 + if is_bad_query ctxt 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;