diff --git a/src/HOL/Tools/Sledgehammer/sledgehammer.ML b/src/HOL/Tools/Sledgehammer/sledgehammer.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML +++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML @@ -1,334 +1,336 @@ (* Title: HOL/Tools/Sledgehammer/sledgehammer.ML Author: Fabian Immler, TU Muenchen Author: Makarius Author: Jasmin Blanchette, TU Muenchen Sledgehammer's heart. *) signature SLEDGEHAMMER = sig type stature = ATP_Problem_Generate.stature type fact = Sledgehammer_Fact.fact type fact_override = Sledgehammer_Fact.fact_override type proof_method = Sledgehammer_Proof_Methods.proof_method type play_outcome = Sledgehammer_Proof_Methods.play_outcome type mode = Sledgehammer_Prover.mode type params = Sledgehammer_Prover.params val someN : string val noneN : string val timeoutN : string val unknownN : string val play_one_line_proof : bool -> Time.time -> (string * stature) list -> Proof.state -> int -> proof_method * proof_method list list -> (string * stature) list * (proof_method * play_outcome) val string_of_factss : (string * fact list) list -> string val run_sledgehammer : params -> mode -> (string -> unit) option -> int -> fact_override -> Proof.state -> bool * (string * string list) end; structure Sledgehammer : SLEDGEHAMMER = struct open ATP_Util open ATP_Proof open ATP_Problem_Generate open Sledgehammer_Util open Sledgehammer_Fact open Sledgehammer_Proof_Methods open Sledgehammer_Isar_Proof open Sledgehammer_Isar_Preplay open Sledgehammer_Isar_Minimize open Sledgehammer_Prover open Sledgehammer_Prover_ATP open Sledgehammer_Prover_Minimize open Sledgehammer_MaSh val someN = "some" val noneN = "none" val timeoutN = "timeout" val unknownN = "unknown" val ordered_outcome_codes = [someN, unknownN, timeoutN, noneN] fun max_outcome_code codes = NONE |> fold (fn candidate => fn accum as SOME _ => accum | NONE => if member (op =) codes candidate then SOME candidate else NONE) ordered_outcome_codes |> the_default unknownN fun is_metis_method (Metis_Method _) = true | is_metis_method _ = false fun play_one_line_proof minimize timeout used_facts state i (preferred_meth, methss) = (if timeout = Time.zeroTime then (used_facts, (preferred_meth, Play_Timed_Out Time.zeroTime)) else let val ctxt = Proof.context_of state val fact_names = map fst used_facts val {facts = chained, goal, ...} = Proof.goal state val goal_t = Logic.get_goal (Thm.prop_of goal) i fun try_methss [] [] = (used_facts, (preferred_meth, Play_Timed_Out Time.zeroTime)) | try_methss ress [] = (used_facts, (case AList.lookup (op =) ress preferred_meth of SOME play => (preferred_meth, play) | NONE => hd (sort (play_outcome_ord o apply2 snd) (rev ress)))) | try_methss ress (meths :: methss) = let fun mk_step fact_names meths = Prove { qualifiers = [], obtains = [], label = ("", 0), goal = goal_t, subproofs = [], facts = ([], fact_names), proof_methods = meths, comment = ""} in (case preplay_isar_step ctxt [] timeout [] (mk_step fact_names meths) of (res as (meth, Played time)) :: _ => (* if a fact is needed by an ATP, it will be needed by "metis" *) if not minimize orelse is_metis_method meth then (used_facts, res) else let val (time', used_names') = minimized_isar_step ctxt chained time (mk_step fact_names [meth]) ||> (facts_of_isar_step #> snd) val used_facts' = filter (member (op =) used_names' o fst) used_facts in (used_facts', (meth, Played time')) end | ress' => try_methss (ress' @ ress) methss) end in try_methss [] methss end) |> (fn (used_facts, (meth, play)) => (used_facts |> not (proof_method_distinguishes_chained_and_direct meth) ? filter_out (fn (_, (sc, _)) => sc = Chained), (meth, play))) fun launch_prover (params as {debug, verbose, spy, max_facts, minimize, timeout, preplay_timeout, expect, ...}) mode writeln_result only learn {comment, state, goal, subgoal, subgoal_count, factss as (_, facts) :: _, found_proof} name = let val ctxt = Proof.context_of state val hard_timeout = Time.scale 5.0 timeout val _ = spying spy (fn () => (state, subgoal, name, "Launched")); val max_facts = max_facts |> the_default (default_max_facts_of_prover ctxt name) val num_facts = length facts |> not only ? Integer.min max_facts val problem = {comment = comment, state = state, goal = goal, subgoal = subgoal, subgoal_count = subgoal_count, factss = factss |> map (apsnd ((not (is_ho_atp ctxt name) ? filter_out (fn ((_, (_, Induction)), _) => true | _ => false)) #> take num_facts)), found_proof = found_proof} fun print_used_facts used_facts used_from = tag_list 1 used_from |> map (fn (j, fact) => fact |> apsnd (K j)) |> filter_used_facts false used_facts |> map (fn ((name, _), j) => name ^ "@" ^ string_of_int j) |> commas |> prefix ("Fact" ^ plural_s (length facts) ^ " in " ^ quote name ^ " proof (of " ^ string_of_int (length facts) ^ "): ") |> writeln fun spying_str_of_res ({outcome = NONE, used_facts, used_from, ...} : prover_result) = let val num_used_facts = length used_facts fun find_indices facts = tag_list 1 facts |> map (fn (j, fact) => fact |> apsnd (K j)) |> filter_used_facts false used_facts |> distinct (eq_fst (op =)) |> map (prefix "@" o string_of_int o snd) fun filter_info (fact_filter, facts) = let val indices = find_indices facts (* "Int.max" is there for robustness -- it shouldn't be necessary *) val unknowns = replicate (Int.max (0, num_used_facts - length indices)) "?" in (commas (indices @ unknowns), fact_filter) end val filter_infos = map filter_info (("actual", used_from) :: factss) |> AList.group (op =) |> map (fn (indices, fact_filters) => commas fact_filters ^ ": " ^ indices) in "Success: Found proof with " ^ string_of_int num_used_facts ^ " of " ^ string_of_int num_facts ^ " fact" ^ plural_s num_facts ^ (if num_used_facts = 0 then "" else ": " ^ commas filter_infos) end | spying_str_of_res {outcome = SOME failure, ...} = "Failure: " ^ string_of_atp_failure failure fun really_go () = problem |> get_minimizing_prover ctxt mode learn name params |> verbose ? tap (fn {outcome = NONE, used_facts as _ :: _, used_from, ...} => print_used_facts used_facts used_from | _ => ()) |> spy ? tap (fn res => spying spy (fn () => (state, subgoal, name, spying_str_of_res res))) |> (fn {outcome, used_facts, preferred_methss, message, ...} => (if outcome = SOME ATP_Proof.TimedOut then timeoutN else if is_some outcome then noneN else someN, fn () => message (fn () => play_one_line_proof minimize preplay_timeout used_facts state subgoal preferred_methss))) fun go () = let val (outcome_code, message) = if debug then really_go () else (really_go () handle ERROR msg => (unknownN, fn () => "Error: " ^ msg ^ "\n") | exn => if Exn.is_interrupt exn then Exn.reraise exn else (unknownN, fn () => "Internal error:\n" ^ Runtime.exn_message exn ^ "\n")) val _ = (* The "expect" argument is deliberately ignored if the prover is missing so that the "Metis_Examples" can be processed on any machine. *) if expect = "" orelse outcome_code = expect orelse not (is_prover_installed ctxt name) then () else error ("Unexpected outcome: " ^ quote outcome_code) in (outcome_code, message) end in if mode = Auto_Try then let val (outcome_code, message) = Timeout.apply timeout go () in (outcome_code, if outcome_code = someN then [message ()] else []) end else let val (outcome_code, message) = Timeout.apply hard_timeout go () val outcome = if outcome_code = someN orelse mode = Normal then quote name ^ ": " ^ message () else "" val _ = if outcome <> "" andalso is_some writeln_result then the writeln_result outcome else writeln outcome in (outcome_code, []) end end val auto_try_max_facts_divisor = 2 (* FUDGE *) fun string_of_facts facts = "Including " ^ string_of_int (length facts) ^ " relevant fact" ^ plural_s (length facts) ^ ": " ^ (facts |> map (fst o fst) |> space_implode " ") fun string_of_factss factss = if forall (null o snd) factss then "Found no relevant facts" else cat_lines (map (fn (filter, facts) => (if filter = "" then "" else quote filter ^ ": ") ^ string_of_facts facts) factss) -fun run_sledgehammer (params as {verbose, spy, provers, max_facts, ...}) mode writeln_result i - (fact_override as {only, ...}) state = +fun run_sledgehammer (params as {verbose, spy, provers, induction_rules, max_facts, ...}) mode + writeln_result i (fact_override as {only, ...}) state = if null provers then error "No prover is set" else (case subgoal_count state of 0 => (error "No subgoal!"; (false, (noneN, []))) | n => let val _ = Proof.assert_backward state val print = if mode = Normal andalso is_none writeln_result then writeln else K () val found_proof = if mode = Normal then let val proof_found = Synchronized.var "proof_found" false in fn () => if Synchronized.change_result proof_found (rpair true) then () else (writeln_result |> the_default writeln) "Proof found..." end else I val ctxt = Proof.context_of state val keywords = Thy_Header.get_keywords' ctxt val {facts = chained, goal, ...} = Proof.goal state val (_, hyp_ts, concl_t) = strip_subgoal goal i ctxt val ho_atp = exists (is_ho_atp ctxt) provers + val induction_rules = the_default (if ho_atp then Instantiate else Exclude) induction_rules val css = clasimpset_rule_table_of ctxt val all_facts = - nearly_all_facts ctxt ho_atp fact_override keywords css chained hyp_ts concl_t + nearly_all_facts ctxt induction_rules fact_override keywords css chained hyp_ts + concl_t val _ = (case find_first (not o is_prover_supported ctxt) provers of SOME name => error ("No such prover: " ^ name) | NONE => ()) val _ = print "Sledgehammering..." val _ = spying spy (fn () => (state, i, "***", "Starting " ^ str_of_mode mode ^ " mode")) val spying_str_of_factss = commas o map (fn (filter, facts) => filter ^ ": " ^ string_of_int (length facts)) fun get_factss provers = let val max_max_facts = (case max_facts of SOME n => n | NONE => 0 |> fold (Integer.max o default_max_facts_of_prover ctxt) provers |> mode = Auto_Try ? (fn n => n div auto_try_max_facts_divisor)) val _ = spying spy (fn () => (state, i, "All", "Filtering " ^ string_of_int (length all_facts) ^ " facts (MaSh algorithm: " ^ str_of_mash_algorithm (the_mash_algorithm ()) ^ ")")); in all_facts |> relevant_facts ctxt params (hd provers) max_max_facts fact_override hyp_ts concl_t |> tap (fn factss => if verbose then print (string_of_factss factss) else ()) |> spy ? tap (fn factss => spying spy (fn () => (state, i, "All", "Selected facts: " ^ spying_str_of_factss factss))) end fun launch_provers () = let val factss = get_factss provers val problem = {comment = "", state = state, goal = goal, subgoal = i, subgoal_count = n, factss = factss, found_proof = found_proof} val learn = mash_learn_proof ctxt params (Thm.prop_of goal) val launch = launch_prover params mode writeln_result only learn in if mode = Auto_Try then (unknownN, []) |> fold (fn prover => fn accum as (outcome_code, _) => if outcome_code = someN then accum else launch problem prover) provers else (learn chained; provers |> Par_List.map (launch problem #> fst) |> max_outcome_code |> rpair []) end in launch_provers () handle Timeout.TIMEOUT _ => (print "Sledgehammer ran out of time"; (unknownN, [])) end |> `(fn (outcome_code, _) => outcome_code = someN)) end; diff --git a/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML b/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML @@ -1,414 +1,416 @@ (* Title: HOL/Tools/Sledgehammer/sledgehammer_commands.ML Author: Jasmin Blanchette, TU Muenchen Adds "sledgehammer" and related commands to Isabelle/Isar's outer syntax. *) signature SLEDGEHAMMER_COMMANDS = sig type params = Sledgehammer_Prover.params val provers : string Unsynchronized.ref val default_params : theory -> (string * string) list -> params val parse_params: (string * string) list parser end; structure Sledgehammer_Commands : SLEDGEHAMMER_COMMANDS = struct open ATP_Util open ATP_Problem_Generate open ATP_Proof open ATP_Proof_Reconstruct open Sledgehammer_Util open Sledgehammer_Fact open Sledgehammer_ATP_Systems open Sledgehammer_Prover open Sledgehammer_Prover_Minimize open Sledgehammer_MaSh open Sledgehammer val cvc4N = "cvc4" val veritN = "verit" val z3N = "z3" val runN = "run" val supported_proversN = "supported_provers" val refresh_tptpN = "refresh_tptp" (** Sledgehammer commands **) fun add_fact_override ns : fact_override = {add = ns, del = [], only = false} fun del_fact_override ns : fact_override = {add = [], del = ns, only = false} fun only_fact_override ns : fact_override = {add = ns, del = [], only = true} fun merge_fact_override_pairwise (r1 : fact_override) (r2 : fact_override) = {add = #add r1 @ #add r2, del = #del r1 @ #del r2, only = #only r1 andalso #only r2} fun merge_fact_overrides rs = fold merge_fact_override_pairwise rs (only_fact_override []) (*** parameters ***) val provers = Unsynchronized.ref "" type raw_param = string * string list val default_default_params = [("debug", "false"), ("verbose", "false"), ("overlord", "false"), ("spy", "false"), ("type_enc", "smart"), ("strict", "false"), ("lam_trans", "smart"), ("uncurried_aliases", "smart"), ("learn", "true"), ("fact_filter", "smart"), ("max_facts", "smart"), ("fact_thresholds", "0.45 0.85"), ("max_mono_iters", "smart"), ("max_new_mono_instances", "smart"), ("isar_proofs", "smart"), ("compress", "smart"), ("try0", "true"), ("smt_proofs", "true"), ("slice", "true"), ("minimize", "true"), ("preplay_timeout", "1")] val alias_params = [("prover", ("provers", [])), (* undocumented *) ("dont_preplay", ("preplay_timeout", ["0"])), ("dont_compress", ("compress", ["1"])), ("isar_proof", ("isar_proofs", [])) (* legacy *)] val negated_alias_params = [("no_debug", "debug"), ("quiet", "verbose"), ("no_overlord", "overlord"), ("dont_spy", "spy"), ("non_strict", "strict"), ("no_uncurried_aliases", "uncurried_aliases"), ("dont_learn", "learn"), ("no_isar_proofs", "isar_proofs"), ("dont_slice", "slice"), ("dont_minimize", "minimize"), ("dont_try0", "try0"), ("no_smt_proofs", "smt_proofs")] val property_dependent_params = ["provers", "timeout"] fun is_known_raw_param s = AList.defined (op =) default_default_params s orelse AList.defined (op =) alias_params s orelse AList.defined (op =) negated_alias_params s orelse member (op =) property_dependent_params s orelse s = "expect" fun is_prover_list ctxt s = (case space_explode " " s of ss as _ :: _ => forall (is_prover_supported ctxt) ss | _ => false) fun unalias_raw_param (name, value) = (case AList.lookup (op =) alias_params name of SOME (name', []) => (name', value) | SOME (param' as (name', _)) => if value <> ["false"] then param' else error ("Parameter " ^ quote name ^ " cannot be set to \"false\" (cf. " ^ quote name' ^ ")") | NONE => (case AList.lookup (op =) negated_alias_params name of SOME name' => (name', (case value of ["false"] => ["true"] | ["true"] => ["false"] | [] => ["false"] | _ => value)) | NONE => (name, value))) val any_type_enc = type_enc_of_string Strict "erased" (* "provers =", "type_enc =", "lam_trans =", "fact_filter =", and "max_facts =" can be omitted. For the last four, this is a secret feature. *) fun normalize_raw_param ctxt = unalias_raw_param #> (fn (name, value) => if is_known_raw_param name then (name, value) else if null value then if is_prover_list ctxt name then ("provers", [name]) else if can (type_enc_of_string Strict) name then ("type_enc", [name]) else if can (trans_lams_of_string ctxt any_type_enc) name then ("lam_trans", [name]) else if member (op =) fact_filters name then ("fact_filter", [name]) else if is_some (Int.fromString name) then ("max_facts", [name]) else error ("Unknown parameter: " ^ quote name) else error ("Unknown parameter: " ^ quote name)) (* Ensures that type encodings such as "mono_native?" and "poly_guards!!" are read correctly. *) val implode_param = strip_spaces_except_between_idents o space_implode " " (* FIXME: use "Generic_Data" *) structure Data = Theory_Data ( type T = raw_param list val empty = default_default_params |> map (apsnd single) val extend = I fun merge data : T = AList.merge (op =) (K true) data ) fun remotify_prover_if_supported_and_not_already_remote ctxt name = if String.isPrefix remote_prefix name then SOME name else let val remote_name = remote_prefix ^ name in if is_prover_supported ctxt remote_name then SOME remote_name else NONE end fun remotify_prover_if_not_installed ctxt name = if is_prover_supported ctxt name andalso is_prover_installed ctxt name then SOME name else remotify_prover_if_supported_and_not_already_remote ctxt name (* The first ATP of the list is used by Auto Sledgehammer. *) fun default_provers_param_value mode ctxt = [cvc4N] @ (if is_vampire_noncommercial_license_accepted () = SOME false then [] else [vampireN]) @ [z3N, eN, spassN, veritN] |> map_filter (remotify_prover_if_not_installed ctxt) (* In "try" mode, leave at least one thread to another slow tool (e.g. Nitpick) *) |> take (Multithreading.max_threads () - (if mode = Try then 1 else 0)) |> implode_param fun set_default_raw_param param thy = let val ctxt = Proof_Context.init_global thy in thy |> Data.map (AList.update (op =) (normalize_raw_param ctxt param)) end fun default_raw_params mode thy = let val ctxt = Proof_Context.init_global thy in Data.get thy |> fold (AList.default (op =)) [("provers", [(case !provers of "" => default_provers_param_value mode ctxt | s => s)]), ("timeout", let val timeout = Options.default_int \<^system_option>\sledgehammer_timeout\ in [if timeout <= 0 then "none" else string_of_int timeout] end)] end fun extract_params mode default_params override_params = let val raw_params = rev override_params @ rev default_params val lookup = Option.map implode_param o AList.lookup (op =) raw_params val lookup_string = the_default "" o lookup fun general_lookup_bool option default_value name = (case lookup name of SOME s => parse_bool_option option name s | NONE => default_value) val lookup_bool = the o general_lookup_bool false (SOME false) fun lookup_time name = (case lookup name of SOME s => parse_time name s | NONE => Time.zeroTime) fun lookup_int name = (case lookup name of NONE => 0 | SOME s => (case Int.fromString s of SOME n => n | NONE => error ("Parameter " ^ quote name ^ " must be assigned an integer value"))) fun lookup_real name = (case lookup name of NONE => 0.0 | SOME s => (case Real.fromString s of SOME n => n | NONE => error ("Parameter " ^ quote name ^ " must be assigned a real value"))) fun lookup_real_pair name = (case lookup name of NONE => (0.0, 0.0) | SOME s => (case s |> space_explode " " |> map Real.fromString of [SOME r1, SOME r2] => (r1, r2) | _ => error ("Parameter " ^ quote name ^ " must be assigned a pair of floating-point \ \values (e.g., \"0.6 0.95\")"))) fun lookup_option lookup' name = (case lookup name of SOME "smart" => NONE | _ => SOME (lookup' name)) val debug = mode <> Auto_Try andalso lookup_bool "debug" val verbose = debug orelse (mode <> Auto_Try andalso lookup_bool "verbose") val overlord = lookup_bool "overlord" val spy = getenv "SLEDGEHAMMER_SPY" = "yes" orelse lookup_bool "spy" val provers = lookup_string "provers" |> space_explode " " |> mode = Auto_Try ? single o hd val type_enc = if mode = Auto_Try then NONE else (case lookup_string "type_enc" of "smart" => NONE | s => (type_enc_of_string Strict s; SOME s)) val strict = mode = Auto_Try orelse lookup_bool "strict" val lam_trans = lookup_option lookup_string "lam_trans" val uncurried_aliases = lookup_option lookup_bool "uncurried_aliases" val learn = lookup_bool "learn" val fact_filter = lookup_option lookup_string "fact_filter" |> mode = Auto_Try ? (fn NONE => SOME mepoN | sf => sf) + val induction_rules = lookup_option (the o induction_rules_of_string) "induction_rules" val max_facts = lookup_option lookup_int "max_facts" val fact_thresholds = lookup_real_pair "fact_thresholds" val max_mono_iters = lookup_option lookup_int "max_mono_iters" val max_new_mono_instances = lookup_option lookup_int "max_new_mono_instances" val isar_proofs = lookup_option lookup_bool "isar_proofs" val compress = Option.map (curry Real.max 1.0) (lookup_option lookup_real "compress") val try0 = lookup_bool "try0" val smt_proofs = lookup_bool "smt_proofs" val slice = mode <> Auto_Try andalso lookup_bool "slice" val minimize = lookup_bool "minimize" val timeout = lookup_time "timeout" val preplay_timeout = lookup_time "preplay_timeout" val expect = lookup_string "expect" in {debug = debug, verbose = verbose, overlord = overlord, spy = spy, provers = provers, type_enc = type_enc, strict = strict, lam_trans = lam_trans, uncurried_aliases = uncurried_aliases, learn = learn, fact_filter = fact_filter, - max_facts = max_facts, fact_thresholds = fact_thresholds, max_mono_iters = max_mono_iters, - max_new_mono_instances = max_new_mono_instances, isar_proofs = isar_proofs, - compress = compress, try0 = try0, smt_proofs = smt_proofs, slice = slice, minimize = minimize, - timeout = timeout, preplay_timeout = preplay_timeout, expect = expect} + induction_rules = induction_rules, max_facts = max_facts, fact_thresholds = fact_thresholds, + max_mono_iters = max_mono_iters, max_new_mono_instances = max_new_mono_instances, + isar_proofs = isar_proofs, compress = compress, try0 = try0, smt_proofs = smt_proofs, + slice = slice, minimize = minimize, timeout = timeout, preplay_timeout = preplay_timeout, + expect = expect} end fun get_params mode = extract_params mode o default_raw_params mode fun default_params thy = get_params Normal thy o map (apsnd single) val silence_state = Proof.map_contexts (Try0.silence_methods false #> Config.put SMT_Config.verbose false) (* Sledgehammer the given subgoal *) val default_learn_prover_timeout = 2.0 fun hammer_away override_params writeln_result subcommand opt_i fact_override state0 = let (* We generally want chained facts to be picked up by the relevance filter, because it can then give it a proper name, which is useful for a variety of reasons (minimization, Isar proofs, verbose output, machine learning). However, if the fact is available by no other means (not even backticks), as "f" would be in "using f unfolding f'" after unfolding, we have no choice but to insert it into the state as an additional hypothesis. *) val {facts = chained0, ...} = Proof.goal state0 val (inserts, keep_chained) = if null chained0 orelse #only fact_override then (chained0, []) else let val ctxt0 = Proof.context_of state0 in List.partition (is_useful_unnamed_local_fact ctxt0) chained0 end val state = state0 |> (if null inserts then I else Proof.refine_insert inserts #> Proof.set_facts keep_chained) |> silence_state val thy = Proof.theory_of state val ctxt = Proof.context_of state val override_params = override_params |> map (normalize_raw_param ctxt) in if subcommand = runN then let val i = the_default 1 opt_i in ignore (run_sledgehammer (get_params Normal thy override_params) Normal writeln_result i fact_override state) end else if subcommand = supported_proversN then supported_provers ctxt else if subcommand = unlearnN then mash_unlearn ctxt else if subcommand = learn_isarN orelse subcommand = learn_proverN orelse subcommand = relearn_isarN orelse subcommand = relearn_proverN then (if subcommand = relearn_isarN orelse subcommand = relearn_proverN then mash_unlearn ctxt else (); mash_learn ctxt (* TODO: Use MaSh mode instead and have the special defaults hardcoded in "get_params" *) (get_params Normal thy ([("timeout", [string_of_real default_learn_prover_timeout]), ("slice", ["false"])] @ override_params @ [("preplay_timeout", ["0"])])) fact_override (#facts (Proof.goal state)) (subcommand = learn_proverN orelse subcommand = relearn_proverN)) else if subcommand = refresh_tptpN then refresh_systems_on_tptp () else error ("Unknown subcommand: " ^ quote subcommand) end fun string_of_raw_param (key, values) = key ^ (case implode_param values of "" => "" | value => " = " ^ value) val parse_query_bang = \<^keyword>\?\ || \<^keyword>\!\ || \<^keyword>\!!\ val parse_key = Scan.repeat1 (Parse.embedded || parse_query_bang) >> implode_param val parse_value = Scan.repeat1 (Parse.name || Parse.float_number || parse_query_bang) val parse_param = parse_key -- Scan.optional (\<^keyword>\=\ |-- parse_value) [] val parse_raw_params = Scan.optional (Args.bracks (Parse.list parse_param)) [] val parse_params = parse_raw_params >> map (apsnd implode_param) val parse_fact_refs = Scan.repeat1 (Scan.unless (Parse.name -- Args.colon) Parse.thm) val parse_fact_override_chunk = (Args.add |-- Args.colon |-- parse_fact_refs >> add_fact_override) || (Args.del |-- Args.colon |-- parse_fact_refs >> del_fact_override) || (parse_fact_refs >> only_fact_override) val parse_fact_override = Scan.optional (Args.parens (Scan.repeat parse_fact_override_chunk >> merge_fact_overrides)) no_fact_override val _ = Outer_Syntax.command \<^command_keyword>\sledgehammer\ "search for first-order proof using automatic theorem provers" (Scan.optional Parse.name runN -- parse_raw_params -- parse_fact_override -- Scan.option Parse.nat >> (fn (((subcommand, params), fact_override), opt_i) => Toplevel.keep_proof (hammer_away params NONE subcommand opt_i fact_override o Toplevel.proof_of))) val _ = Outer_Syntax.command \<^command_keyword>\sledgehammer_params\ "set and display the default parameters for Sledgehammer" (parse_raw_params >> (fn params => Toplevel.theory (fold set_default_raw_param params #> tap (fn thy => writeln ("Default parameters for Sledgehammer:\n" ^ (case rev (default_raw_params Normal thy) of [] => "none" | params => params |> map string_of_raw_param |> sort_strings |> cat_lines)))))) fun try_sledgehammer auto state = let val thy = Proof.theory_of state val mode = if auto then Auto_Try else Try val i = 1 in run_sledgehammer (get_params mode thy []) mode NONE i no_fact_override (silence_state state) end val _ = Try.tool_setup (sledgehammerN, (40, \<^system_option>\auto_sledgehammer\, try_sledgehammer)) val _ = Query_Operation.register {name = sledgehammerN, pri = 0} (fn {state = st, args, writeln_result, ...} => (case try Toplevel.proof_of st of SOME state => let val [provers_arg, isar_proofs_arg, try0_arg] = args val override_params = ((if provers_arg = "" then [] else [("provers", space_explode " " provers_arg)]) @ [("isar_proofs", [if isar_proofs_arg = "true" then "true" else "smart"]), ("try0", [try0_arg]), ("debug", ["false"]), ("verbose", ["false"]), ("overlord", ["false"])]); in hammer_away override_params (SOME writeln_result) runN NONE no_fact_override state end | NONE => error "Unknown proof context")) end; diff --git a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML @@ -1,567 +1,574 @@ (* Title: HOL/Tools/Sledgehammer/sledgehammer_fact.ML Author: Jia Meng, Cambridge University Computer Laboratory and NICTA Author: Jasmin Blanchette, TU Muenchen Sledgehammer fact handling. *) signature SLEDGEHAMMER_FACT = sig type status = ATP_Problem_Generate.status type stature = ATP_Problem_Generate.stature type raw_fact = ((unit -> string) * stature) * thm (* TODO: rename to lazy_fact *) type fact = (string * stature) * thm type fact_override = {add : (Facts.ref * Token.src list) list, del : (Facts.ref * Token.src list) list, only : bool} - val instantiate_inducts : bool Config.T + datatype induction_rules = Include | Exclude | Instantiate + val induction_rules_of_string : string -> induction_rules option + val no_fact_override : fact_override val fact_of_ref : Proof.context -> Keyword.keywords -> thm list -> status Termtab.table -> Facts.ref * Token.src list -> ((string * stature) * thm) list val cartouche_thm : Proof.context -> thm -> string - val is_blacklisted_or_something : Proof.context -> bool -> string -> bool + val is_blacklisted_or_something : induction_rules -> string -> bool val clasimpset_rule_table_of : Proof.context -> status Termtab.table val build_name_tables : (thm -> string) -> ('a * thm) list -> string Symtab.table * string Symtab.table val fact_distinct : (term * term -> bool) -> ('a * thm) list -> ('a * thm) list - val maybe_instantiate_inducts : Proof.context -> term list -> term -> + val maybe_instantiate_inducts : Proof.context -> induction_rules -> term list -> term -> (((unit -> string) * 'a) * thm) list -> (((unit -> string) * 'a) * thm) list val fact_of_raw_fact : raw_fact -> fact val is_useful_unnamed_local_fact : Proof.context -> thm -> bool - val all_facts : Proof.context -> bool -> bool -> Keyword.keywords -> thm list -> thm list -> - status Termtab.table -> raw_fact list - val nearly_all_facts : Proof.context -> bool -> fact_override -> Keyword.keywords -> - status Termtab.table -> thm list -> term list -> term -> raw_fact list + val all_facts : Proof.context -> bool -> induction_rules -> Keyword.keywords -> + thm list -> thm list -> status Termtab.table -> raw_fact list + val nearly_all_facts : Proof.context -> induction_rules -> fact_override -> + Keyword.keywords -> status Termtab.table -> thm list -> term list -> term -> raw_fact list val drop_duplicate_facts : raw_fact list -> raw_fact list + end; structure Sledgehammer_Fact : SLEDGEHAMMER_FACT = struct open ATP_Util open ATP_Problem_Generate open Sledgehammer_Util type raw_fact = ((unit -> string) * stature) * thm type fact = (string * stature) * thm type fact_override = {add : (Facts.ref * Token.src list) list, del : (Facts.ref * Token.src list) list, only : bool} val local_thisN = Long_Name.localN ^ Long_Name.separator ^ Auto_Bind.thisN (* gracefully handle huge background theories *) val max_facts_for_duplicates = 50000 val max_facts_for_complex_check = 25000 val max_simps_for_clasimpset = 10000 -(* experimental feature *) -val instantiate_inducts = - Attrib.setup_config_bool \<^binding>\sledgehammer_instantiate_inducts\ (K false) +datatype induction_rules = Include | Exclude | Instantiate + +fun induction_rules_of_string "include" = SOME Include + | induction_rules_of_string "exclude" = SOME Exclude + | induction_rules_of_string "instantiate" = SOME Instantiate + | induction_rules_of_string _ = NONE val no_fact_override = {add = [], del = [], only = false} fun needs_quoting keywords s = Keyword.is_literal keywords s orelse exists (not o Symbol_Pos.is_identifier) (Long_Name.explode s) fun make_name keywords multi j name = (name |> needs_quoting keywords name ? quote) ^ (if multi then "(" ^ string_of_int j ^ ")" else "") fun explode_interval _ (Facts.FromTo (i, j)) = i upto j | explode_interval max (Facts.From i) = i upto i + max - 1 | explode_interval _ (Facts.Single i) = [i] fun is_rec_eq lhs = Term.exists_subterm (curry (op =) (head_of lhs)) fun is_rec_def (\<^const>\Trueprop\ $ t) = is_rec_def t | is_rec_def (\<^const>\Pure.imp\ $ _ $ t2) = is_rec_def t2 | is_rec_def (Const (\<^const_name>\Pure.eq\, _) $ t1 $ t2) = is_rec_eq t1 t2 | is_rec_def (Const (\<^const_name>\HOL.eq\, _) $ t1 $ t2) = is_rec_eq t1 t2 | is_rec_def _ = false fun is_assum assms th = exists (fn ct => Thm.prop_of th aconv Thm.term_of ct) assms fun is_chained chained = member Thm.eq_thm_prop chained fun scope_of_thm global assms chained th = if is_chained chained th then Chained else if global then Global else if is_assum assms th then Assum else Local val may_be_induction = exists_subterm (fn Var (_, Type (\<^type_name>\fun\, [_, T])) => body_type T = \<^typ>\bool\ | _ => false) (* TODO: get rid of *) fun normalize_vars t = let fun normT (Type (s, Ts)) = fold_map normT Ts #>> curry Type s | normT (TVar (z as (_, S))) = (fn ((knownT, nT), accum) => (case find_index (equal z) knownT of ~1 => (TVar ((Name.uu, nT), S), ((z :: knownT, nT + 1), accum)) | j => (TVar ((Name.uu, nT - j - 1), S), ((knownT, nT), accum)))) | normT (T as TFree _) = pair T fun norm (t $ u) = norm t ##>> norm u #>> op $ | norm (Const (s, T)) = normT T #>> curry Const s | norm (Var (z as (_, T))) = normT T #> (fn (T, (accumT, (known, n))) => (case find_index (equal z) known of ~1 => (Var ((Name.uu, n), T), (accumT, (z :: known, n + 1))) | j => (Var ((Name.uu, n - j - 1), T), (accumT, (known, n))))) | norm (Abs (_, T, t)) = norm t ##>> normT T #>> (fn (t, T) => Abs (Name.uu, T, t)) | norm (Bound j) = pair (Bound j) | norm (Free (s, T)) = normT T #>> curry Free s in fst (norm t (([], 0), ([], 0))) end fun status_of_thm css name th = if Termtab.is_empty css then General else let val t = Thm.prop_of th in (* FIXME: use structured name *) if String.isSubstring ".induct" name andalso may_be_induction t then Induction else let val t = normalize_vars t in (case Termtab.lookup css t of SOME status => status | NONE => let val concl = Logic.strip_imp_concl t in (case try (HOLogic.dest_eq o HOLogic.dest_Trueprop) concl of SOME lrhss => let val prems = Logic.strip_imp_prems t val t' = Logic.list_implies (prems, Logic.mk_equals lrhss) in Termtab.lookup css t' |> the_default General end | NONE => General) end) end end fun stature_of_thm global assms chained css name th = (scope_of_thm global assms chained th, status_of_thm css name th) fun fact_of_ref ctxt keywords chained css (xthm as (xref, args)) = let val ths = Attrib.eval_thms ctxt [xthm] val bracket = implode (map (enclose "[" "]" o Pretty.unformatted_string_of o Token.pretty_src ctxt) args) fun nth_name j = (case xref of Facts.Fact s => cartouche (simplify_spaces (YXML.content_of s)) ^ bracket | Facts.Named (("", _), _) => "[" ^ bracket ^ "]" | Facts.Named ((name, _), NONE) => make_name keywords (length ths > 1) (j + 1) name ^ bracket | Facts.Named ((name, _), SOME intervals) => make_name keywords true (nth (maps (explode_interval (length ths)) intervals) j) name ^ bracket) fun add_nth th (j, rest) = let val name = nth_name j in (j + 1, ((name, stature_of_thm false [] chained css name th), th) :: rest) end in (0, []) |> fold add_nth ths |> snd end (* Reject theorems with names like "List.filter.filter_list_def" or "Accessible_Part.acc.defs", as these are definitions arising from packages. *) fun is_package_def s = let val ss = Long_Name.explode s in length ss > 2 andalso not (hd ss = "local") andalso exists (fn suf => String.isSuffix suf s) ["_case_def", "_rec_def", "_size_def", "_size_overloaded_def"] end (* FIXME: put other record thms here, or declare as "no_atp" *) -fun multi_base_blacklist ctxt ho_atp = +fun multi_base_blacklist induction_rules = ["defs", "select_defs", "update_defs", "split", "splits", "split_asm", "ext_cases", "eq.simps", "eq.refl", "nchotomy", "case_cong", "case_cong_weak", "nat_of_char_simps", "nibble.simps", "nibble.distinct"] - |> not (ho_atp orelse Config.get ctxt instantiate_inducts) ? append ["induct", "inducts"] + |> induction_rules = Exclude ? append ["induct", "inducts"] |> map (prefix Long_Name.separator) (* The maximum apply depth of any "metis" call in "Metis_Examples" (back in 2007) was 11. *) val max_apply_depth = 18 fun apply_depth (f $ t) = Int.max (apply_depth f, apply_depth t + 1) | apply_depth (Abs (_, _, t)) = apply_depth t | apply_depth _ = 0 fun is_too_complex t = apply_depth t > max_apply_depth (* FIXME: Ad hoc list *) val technical_prefixes = ["ATP", "Code_Evaluation", "Datatype", "Enum", "Lazy_Sequence", "Limited_Sequence", "Meson", "Metis", "Nitpick", "Quickcheck_Random", "Quickcheck_Exhaustive", "Quickcheck_Narrowing", "Random_Sequence", "Sledgehammer", "SMT"] |> map (suffix Long_Name.separator) fun is_technical_const s = exists (fn pref => String.isPrefix pref s) technical_prefixes (* FIXME: make more reliable *) val sep_class_sep = Long_Name.separator ^ "class" ^ Long_Name.separator fun is_low_level_class_const s = s = \<^const_name>\equal_class.equal\ orelse String.isSubstring sep_class_sep s val sep_that = Long_Name.separator ^ Auto_Bind.thatN val skolem_thesis = Name.skolem Auto_Bind.thesisN fun is_that_fact th = exists_subterm (fn Free (s, _) => s = skolem_thesis | _ => false) (Thm.prop_of th) andalso String.isSuffix sep_that (Thm.get_name_hint th) datatype interest = Deal_Breaker | Interesting | Boring fun combine_interests Deal_Breaker _ = Deal_Breaker | combine_interests _ Deal_Breaker = Deal_Breaker | combine_interests Interesting _ = Interesting | combine_interests _ Interesting = Interesting | combine_interests Boring Boring = Boring val type_has_top_sort = exists_subtype (fn TFree (_, []) => true | TVar (_, []) => true | _ => false) fun is_likely_tautology_too_meta_or_too_technical th = let fun is_interesting_subterm (Const (s, _)) = not (member (op =) atp_widely_irrelevant_consts s) | is_interesting_subterm (Free _) = true | is_interesting_subterm _ = false fun interest_of_bool t = if exists_Const ((is_technical_const o fst) orf (is_low_level_class_const o fst) orf type_has_top_sort o snd) t then Deal_Breaker else if exists_type (exists_subtype (curry (op =) \<^typ>\prop\)) t orelse not (exists_subterm is_interesting_subterm t) then Boring else Interesting fun interest_of_prop _ (\<^const>\Trueprop\ $ t) = interest_of_bool t | interest_of_prop Ts (\<^const>\Pure.imp\ $ t $ u) = combine_interests (interest_of_prop Ts t) (interest_of_prop Ts u) | interest_of_prop Ts (Const (\<^const_name>\Pure.all\, _) $ Abs (_, T, t)) = if type_has_top_sort T then Deal_Breaker else interest_of_prop (T :: Ts) t | interest_of_prop Ts ((t as Const (\<^const_name>\Pure.all\, _)) $ u) = interest_of_prop Ts (t $ eta_expand Ts u 1) | interest_of_prop _ (Const (\<^const_name>\Pure.eq\, _) $ t $ u) = combine_interests (interest_of_bool t) (interest_of_bool u) | interest_of_prop _ _ = Deal_Breaker val t = Thm.prop_of th in (interest_of_prop [] t <> Interesting andalso not (Thm.eq_thm_prop (@{thm ext}, th))) orelse is_that_fact th end -fun is_blacklisted_or_something ctxt ho_atp = - let val blist = multi_base_blacklist ctxt ho_atp in +fun is_blacklisted_or_something induction_rules = + let val blist = multi_base_blacklist induction_rules in fn name => is_package_def name orelse exists (fn s => String.isSuffix s name) blist end (* This is a terrible hack. Free variables are sometimes coded as "M__" when they are displayed as "M" and we want to avoid clashes with these. But sometimes it's even worse: "Ma__" encodes "M". So we simply reserve all prefixes of all free variables. In the worse case scenario, where the fact won't be resolved correctly, the user can fix it manually, e.g., by giving a name to the offending fact. *) fun all_prefixes_of s = map (fn i => String.extract (s, 0, SOME i)) (1 upto size s - 1) fun close_form t = (t, [] |> Term.add_free_names t |> maps all_prefixes_of) |> fold (fn ((s, i), T) => fn (t', taken) => let val s' = singleton (Name.variant_list taken) s in ((if fastype_of t' = HOLogic.boolT then HOLogic.all_const else Logic.all_const) T $ Abs (s', T, abstract_over (Var ((s, i), T), t')), s' :: taken) end) (Term.add_vars t [] |> sort_by (fst o fst)) |> fst fun cartouche_term ctxt = close_form #> hackish_string_of_term ctxt #> cartouche fun cartouche_thm ctxt = cartouche_term ctxt o Thm.prop_of (* TODO: rewrite to use nets and/or to reuse existing data structures *) fun clasimpset_rule_table_of ctxt = let val simps = ctxt |> simpset_of |> dest_ss |> #simps in if length simps >= max_simps_for_clasimpset then Termtab.empty else let fun add stature th = Termtab.update (normalize_vars (Thm.prop_of th), stature) val {safeIs, (* safeEs, *) unsafeIs, (* unsafeEs, *) ...} = ctxt |> claset_of |> Classical.rep_cs val intros = map #1 (Item_Net.content safeIs @ Item_Net.content unsafeIs) (* Add once it is used: val elims = Item_Net.content safeEs @ Item_Net.content unsafeEs |> map Classical.classical_rule *) val specs = Spec_Rules.get ctxt val (rec_defs, nonrec_defs) = specs |> filter (Spec_Rules.is_equational o #rough_classification) |> maps #rules |> List.partition (is_rec_def o Thm.prop_of) val spec_intros = specs |> filter (Spec_Rules.is_relational o #rough_classification) |> maps #rules in Termtab.empty |> fold (add Simp o snd) simps |> fold (add Rec_Def) rec_defs |> fold (add Non_Rec_Def) nonrec_defs (* Add once it is used: |> fold (add Elim) elims *) |> fold (add Intro) intros |> fold (add Inductive) spec_intros end end fun normalize_eq (\<^const>\Trueprop\ $ (t as (t0 as Const (\<^const_name>\HOL.eq\, _)) $ t1 $ t2)) = if is_less_equal (Term_Ord.fast_term_ord (t1, t2)) then t else t0 $ t2 $ t1 | normalize_eq (\<^const>\Trueprop\ $ (t as \<^const>\Not\ $ ((t0 as Const (\<^const_name>\HOL.eq\, _)) $ t1 $ t2))) = if is_less_equal (Term_Ord.fast_term_ord (t1, t2)) then t else HOLogic.mk_not (t0 $ t2 $ t1) | normalize_eq (Const (\<^const_name>\Pure.eq\, Type (_, [T, _])) $ t1 $ t2) = (if is_less_equal (Term_Ord.fast_term_ord (t1, t2)) then (t1, t2) else (t2, t1)) |> (fn (t1, t2) => HOLogic.eq_const T $ t1 $ t2) | normalize_eq t = t fun if_thm_before th th' = if Context.subthy_id (apply2 Thm.theory_id (th, th')) then th else th' (* Hack: Conflate the facts about a class as seen from the outside with the corresponding low-level facts, so that MaSh can learn from the low-level proofs. *) fun un_class_ify s = (case first_field "_class" s of SOME (pref, suf) => [s, pref ^ suf] | NONE => [s]) fun build_name_tables name_of facts = let fun cons_thm (_, th) = Termtab.cons_list (normalize_vars (normalize_eq (Thm.prop_of th)), th) fun add_plain canon alias = Symtab.update (Thm.get_name_hint alias, name_of (if_thm_before canon alias)) fun add_plains (_, aliases as canon :: _) = fold (add_plain canon) aliases fun add_inclass (name, target) = fold (fn s => Symtab.update (s, target)) (un_class_ify name) val prop_tab = fold cons_thm facts Termtab.empty val plain_name_tab = Termtab.fold add_plains prop_tab Symtab.empty val inclass_name_tab = Symtab.fold add_inclass plain_name_tab Symtab.empty in (plain_name_tab, inclass_name_tab) end fun fact_distinct eq facts = fold (fn (i, fact as (_, th)) => Net.insert_term_safe (eq o apply2 (normalize_eq o Thm.prop_of o snd o snd)) (normalize_eq (Thm.prop_of th), (i, fact))) (tag_list 0 facts) Net.empty |> Net.entries |> sort (int_ord o apply2 fst) |> map snd fun struct_induct_rule_on th = (case Logic.strip_horn (Thm.prop_of th) of (prems, \<^const>\Trueprop\ $ ((p as Var ((p_name, 0), _)) $ (a as Var (_, ind_T)))) => if not (is_TVar ind_T) andalso length prems > 1 andalso exists (exists_subterm (curry (op aconv) p)) prems andalso not (exists (exists_subterm (curry (op aconv) a)) prems) then SOME (p_name, ind_T) else NONE | _ => NONE) val instantiate_induct_timeout = seconds 0.01 fun instantiate_induct_rule ctxt concl_prop p_name ((name, stature), th) ind_x = let fun varify_noninducts (t as Free (s, T)) = if (s, T) = ind_x orelse can dest_funT T then t else Var ((s, 0), T) | varify_noninducts t = t val p_inst = concl_prop |> map_aterms varify_noninducts |> close_form |> lambda (Free ind_x) |> hackish_string_of_term ctxt in ((fn () => name () ^ "[where " ^ p_name ^ " = " ^ quote p_inst ^ "]", stature), th |> Rule_Insts.read_instantiate ctxt [(((p_name, 0), Position.none), p_inst)] []) end fun type_match thy (T1, T2) = (Sign.typ_match thy (T2, T1) Vartab.empty; true) handle Type.TYPE_MATCH => false fun instantiate_if_induct_rule ctxt stmt stmt_xs (ax as (_, th)) = (case struct_induct_rule_on th of SOME (p_name, ind_T) => let val thy = Proof_Context.theory_of ctxt in stmt_xs |> filter (fn (_, T) => type_match thy (T, ind_T)) |> map_filter (try (Timeout.apply instantiate_induct_timeout (instantiate_induct_rule ctxt stmt p_name ax))) end | NONE => [ax]) fun external_frees t = [] |> Term.add_frees t |> filter_out (Name.is_internal o fst) -fun maybe_instantiate_inducts ctxt hyp_ts concl_t = - if Config.get ctxt instantiate_inducts then +fun maybe_instantiate_inducts ctxt induction_rules hyp_ts concl_t = + if induction_rules = Instantiate then let val ind_stmt = (hyp_ts |> filter_out (null o external_frees), concl_t) |> Logic.list_implies |> Object_Logic.atomize_term ctxt val ind_stmt_xs = external_frees ind_stmt in maps (instantiate_if_induct_rule ctxt ind_stmt ind_stmt_xs) end else I fun fact_of_raw_fact ((name, stature), th) = ((name (), stature), th) fun fact_count facts = Facts.fold_static (K (Integer.add 1)) facts 0 fun is_useful_unnamed_local_fact ctxt = let val thy = Proof_Context.theory_of ctxt val global_facts = Global_Theory.facts_of thy val local_facts = Proof_Context.facts_of ctxt val named_locals = Facts.dest_static true [global_facts] local_facts |> maps (map (normalize_eq o Thm.prop_of) o snd) in fn th => not (Thm.has_name_hint th) andalso not (member (op aconv) named_locals (normalize_eq (Thm.prop_of th))) end -fun all_facts ctxt generous ho_atp keywords add_ths chained css = +fun all_facts ctxt generous induction_rules keywords add_ths chained css = let val thy = Proof_Context.theory_of ctxt val transfer = Global_Theory.transfer_theories thy val global_facts = Global_Theory.facts_of thy val is_too_complex = if generous orelse fact_count global_facts >= max_facts_for_complex_check then K false else is_too_complex val local_facts = Proof_Context.facts_of ctxt val assms = Assumption.all_assms_of ctxt val named_locals = Facts.dest_static true [global_facts] local_facts val unnamed_locals = Facts.props local_facts |> map #1 |> filter (is_useful_unnamed_local_fact ctxt) |> map (pair "" o single) val full_space = Name_Space.merge (Facts.space_of global_facts, Facts.space_of local_facts) - val is_blacklisted_or_something = is_blacklisted_or_something ctxt ho_atp + val is_blacklisted_or_something = is_blacklisted_or_something induction_rules fun add_facts global foldx facts = foldx (fn (name0, ths) => fn accum => if name0 <> "" andalso (Long_Name.is_hidden (Facts.intern facts name0) orelse ((Facts.is_concealed facts name0 orelse (not generous andalso is_blacklisted_or_something name0)) andalso forall (not o member Thm.eq_thm_prop add_ths) ths)) then accum else let val n = length ths val multi = n > 1 fun check_thms a = (case try (Proof_Context.get_thms ctxt) a of NONE => false | SOME ths' => eq_list Thm.eq_thm_prop (ths, ths')) in snd (fold_rev (fn th0 => fn (j, accum) => let val th = transfer th0 in (j - 1, if not (member Thm.eq_thm_prop add_ths th) andalso (is_likely_tautology_too_meta_or_too_technical th orelse is_too_complex (Thm.prop_of th)) then accum else let fun get_name () = if name0 = "" orelse name0 = local_thisN then cartouche_thm ctxt th else let val short_name = Facts.extern ctxt facts name0 in if check_thms short_name then short_name else let val long_name = Name_Space.extern ctxt full_space name0 in if check_thms long_name then long_name else name0 end end |> make_name keywords multi j val stature = stature_of_thm global assms chained css name0 th val new = ((get_name, stature), th) in (if multi then apsnd else apfst) (cons new) accum end) end) ths (n, accum)) end) in (* The single-theorem names go before the multiple-theorem ones (e.g., "xxx" vs. "xxx(3)"), so that single names are preferred when both are available. *) ([], []) |> add_facts false fold local_facts (unnamed_locals @ named_locals) |> add_facts true Facts.fold_static global_facts global_facts |> op @ end -fun nearly_all_facts ctxt ho_atp {add, del, only} keywords css chained hyp_ts concl_t = +fun nearly_all_facts ctxt induction_rules {add, del, only} keywords css chained hyp_ts + concl_t = if only andalso null add then [] else let val chained = chained |> maps (fn th => insert Thm.eq_thm_prop (zero_var_indexes th) [th]) in (if only then maps (map (fn ((name, stature), th) => ((K name, stature), th)) o fact_of_ref ctxt keywords chained css) add else let val (add, del) = apply2 (Attrib.eval_thms ctxt) (add, del) val facts = - all_facts ctxt false ho_atp keywords add chained css + all_facts ctxt false induction_rules keywords add chained css |> filter_out ((member Thm.eq_thm_prop del orf (Named_Theorems.member ctxt \<^named_theorems>\no_atp\ andf not o member Thm.eq_thm_prop add)) o snd) in facts end) - |> maybe_instantiate_inducts ctxt hyp_ts concl_t + |> maybe_instantiate_inducts ctxt induction_rules hyp_ts concl_t end fun drop_duplicate_facts facts = let val num_facts = length facts in facts |> num_facts <= max_facts_for_duplicates ? fact_distinct (op aconv) end end; diff --git a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML @@ -1,1635 +1,1636 @@ (* Title: HOL/Tools/Sledgehammer/sledgehammer_mash.ML Author: Jasmin Blanchette, TU Muenchen Author: Cezary Kaliszyk, University of Innsbruck Sledgehammer's machine-learning-based relevance filter (MaSh). *) signature SLEDGEHAMMER_MASH = sig type stature = ATP_Problem_Generate.stature type raw_fact = Sledgehammer_Fact.raw_fact type fact = Sledgehammer_Fact.fact type fact_override = Sledgehammer_Fact.fact_override type params = Sledgehammer_Prover.params type prover_result = Sledgehammer_Prover.prover_result val trace : bool Config.T val duplicates : bool Config.T val MePoN : string val MaShN : string val MeShN : string val mepoN : string val mashN : string val meshN : string val unlearnN : string val learn_isarN : string val learn_proverN : string val relearn_isarN : string val relearn_proverN : string val fact_filters : string list val encode_str : string -> string val encode_strs : string list -> string val decode_str : string -> string val decode_strs : string -> string list datatype mash_algorithm = MaSh_NB | MaSh_kNN | MaSh_NB_kNN | MaSh_NB_Ext | MaSh_kNN_Ext val is_mash_enabled : unit -> bool val the_mash_algorithm : unit -> mash_algorithm val str_of_mash_algorithm : mash_algorithm -> string val mesh_facts : ('a list -> 'a list) -> ('a * 'a -> bool) -> int -> (real * (('a * real) list * 'a list)) list -> 'a list val nickname_of_thm : thm -> string val find_suggested_facts : Proof.context -> ('b * thm) list -> string list -> ('b * thm) list val crude_thm_ord : Proof.context -> thm ord val thm_less : thm * thm -> bool val goal_of_thm : theory -> thm -> thm val run_prover_for_mash : Proof.context -> params -> string -> string -> fact list -> thm -> prover_result val features_of : Proof.context -> string -> stature -> term list -> string list val trim_dependencies : string list -> string list option val isar_dependencies_of : string Symtab.table * string Symtab.table -> thm -> string list option val prover_dependencies_of : Proof.context -> params -> string -> int -> raw_fact list -> string Symtab.table * string Symtab.table -> thm -> bool * string list val attach_parents_to_facts : ('a * thm) list -> ('a * thm) list -> (string list * ('a * thm)) list val num_extra_feature_facts : int val extra_feature_factor : real val weight_facts_smoothly : 'a list -> ('a * real) list val weight_facts_steeply : 'a list -> ('a * real) list val find_mash_suggestions : Proof.context -> int -> string list -> ('a * thm) list -> ('a * thm) list -> ('a * thm) list -> ('a * thm) list * ('a * thm) list val mash_suggested_facts : Proof.context -> string -> params -> int -> term list -> term -> raw_fact list -> fact list * fact list val mash_unlearn : Proof.context -> unit val mash_learn_proof : Proof.context -> params -> term -> thm list -> unit val mash_learn_facts : Proof.context -> params -> string -> int -> bool -> Time.time -> raw_fact list -> string val mash_learn : Proof.context -> params -> fact_override -> thm list -> bool -> unit val mash_can_suggest_facts : Proof.context -> bool val mash_can_suggest_facts_fast : Proof.context -> bool val generous_max_suggestions : int -> int val mepo_weight : real val mash_weight : real val relevant_facts : Proof.context -> params -> string -> int -> fact_override -> term list -> term -> raw_fact list -> (string * fact list) list end; structure Sledgehammer_MaSh : SLEDGEHAMMER_MASH = struct open ATP_Util open ATP_Problem_Generate open Sledgehammer_Util open Sledgehammer_Fact open Sledgehammer_Prover open Sledgehammer_Prover_Minimize open Sledgehammer_MePo val anonymous_proof_prefix = "." val trace = Attrib.setup_config_bool \<^binding>\sledgehammer_mash_trace\ (K false) val duplicates = Attrib.setup_config_bool \<^binding>\sledgehammer_fact_duplicates\ (K false) fun trace_msg ctxt msg = if Config.get ctxt trace then tracing (msg ()) else () fun gen_eq_thm ctxt = if Config.get ctxt duplicates then Thm.eq_thm_strict else Thm.eq_thm_prop val MePoN = "MePo" val MaShN = "MaSh" val MeShN = "MeSh" val mepoN = "mepo" val mashN = "mash" val meshN = "mesh" val fact_filters = [meshN, mepoN, mashN] val unlearnN = "unlearn" val learn_isarN = "learn_isar" val learn_proverN = "learn_prover" val relearn_isarN = "relearn_isar" val relearn_proverN = "relearn_prover" fun map_array_at ary f i = Array.update (ary, i, f (Array.sub (ary, i))) type xtab = int * int Symtab.table val empty_xtab = (0, Symtab.empty) fun add_to_xtab key (next, tab) = (next + 1, Symtab.update_new (key, next) tab) fun maybe_add_to_xtab key = perhaps (try (add_to_xtab key)) fun state_file () = Path.expand (Path.explode "$ISABELLE_HOME_USER/mash_state") val remove_state_file = try File.rm o state_file datatype mash_algorithm = MaSh_NB | MaSh_kNN | MaSh_NB_kNN | MaSh_NB_Ext | MaSh_kNN_Ext fun mash_algorithm () = (case Options.default_string \<^system_option>\MaSh\ of "yes" => SOME MaSh_NB_kNN | "sml" => SOME MaSh_NB_kNN | "nb" => SOME MaSh_NB | "knn" => SOME MaSh_kNN | "nb_knn" => SOME MaSh_NB_kNN | "nb_ext" => SOME MaSh_NB_Ext | "knn_ext" => SOME MaSh_kNN_Ext | "none" => NONE | "" => NONE | algorithm => (warning ("Unknown MaSh algorithm: " ^ quote algorithm); NONE)) val is_mash_enabled = is_some o mash_algorithm val the_mash_algorithm = the_default MaSh_NB_kNN o mash_algorithm fun str_of_mash_algorithm MaSh_NB = "nb" | str_of_mash_algorithm MaSh_kNN = "knn" | str_of_mash_algorithm MaSh_NB_kNN = "nb_knn" | str_of_mash_algorithm MaSh_NB_Ext = "nb_ext" | str_of_mash_algorithm MaSh_kNN_Ext = "knn_ext" fun scaled_avg [] = 0 | scaled_avg xs = Real.ceil (100000000.0 * fold (curry (op +)) xs 0.0) div length xs fun avg [] = 0.0 | avg xs = fold (curry (op +)) xs 0.0 / Real.fromInt (length xs) fun normalize_scores _ [] = [] | normalize_scores max_facts xs = map (apsnd (curry (op *) (1.0 / avg (map snd (take max_facts xs))))) xs fun mesh_facts maybe_distinct _ max_facts [(_, (sels, unks))] = map fst (take max_facts sels) @ take (max_facts - length sels) unks |> maybe_distinct | mesh_facts _ fact_eq max_facts mess = let val mess = mess |> map (apsnd (apfst (normalize_scores max_facts))) fun score_in fact (global_weight, (sels, unks)) = let val score_at = try (nth sels) #> Option.map (fn (_, score) => global_weight * score) in (case find_index (curry fact_eq fact o fst) sels of ~1 => if member fact_eq unks fact then NONE else SOME 0.0 | rank => score_at rank) end fun weight_of fact = mess |> map_filter (score_in fact) |> scaled_avg in fold (union fact_eq o map fst o take max_facts o fst o snd) mess [] |> map (`weight_of) |> sort (int_ord o apply2 fst o swap) |> map snd |> take max_facts end fun smooth_weight_of_fact rank = Math.pow (1.3, 15.5 - 0.2 * Real.fromInt rank) + 15.0 (* FUDGE *) fun steep_weight_of_fact rank = Math.pow (0.62, log2 (Real.fromInt (rank + 1))) (* FUDGE *) fun weight_facts_smoothly facts = facts ~~ map smooth_weight_of_fact (0 upto length facts - 1) fun weight_facts_steeply facts = facts ~~ map steep_weight_of_fact (0 upto length facts - 1) fun sort_array_suffix cmp needed a = let exception BOTTOM of int val al = Array.length a fun maxson l i = let val i31 = i + i + i + 1 in if i31 + 2 < l then let val x = Unsynchronized.ref i31 in if is_less (cmp (Array.sub (a, i31), Array.sub (a, i31 + 1))) then x := i31 + 1 else (); if is_less (cmp (Array.sub (a, !x), Array.sub (a, i31 + 2))) then x := i31 + 2 else (); !x end else if i31 + 1 < l andalso is_less (cmp (Array.sub (a, i31), Array.sub (a, i31 + 1))) then i31 + 1 else if i31 < l then i31 else raise BOTTOM i end fun trickledown l i e = let val j = maxson l i in if is_greater (cmp (Array.sub (a, j), e)) then (Array.update (a, i, Array.sub (a, j)); trickledown l j e) else Array.update (a, i, e) end fun trickle l i e = trickledown l i e handle BOTTOM i => Array.update (a, i, e) fun bubbledown l i = let val j = maxson l i in Array.update (a, i, Array.sub (a, j)); bubbledown l j end fun bubble l i = bubbledown l i handle BOTTOM i => i fun trickleup i e = let val father = (i - 1) div 3 in if is_less (cmp (Array.sub (a, father), e)) then (Array.update (a, i, Array.sub (a, father)); if father > 0 then trickleup father e else Array.update (a, 0, e)) else Array.update (a, i, e) end fun for i = if i < 0 then () else (trickle al i (Array.sub (a, i)); for (i - 1)) fun for2 i = if i < Integer.max 2 (al - needed) then () else let val e = Array.sub (a, i) in Array.update (a, i, Array.sub (a, 0)); trickleup (bubble i 0) e; for2 (i - 1) end in for (((al + 1) div 3) - 1); for2 (al - 1); if al > 1 then let val e = Array.sub (a, 1) in Array.update (a, 1, Array.sub (a, 0)); Array.update (a, 0, e) end else () end fun rev_sort_list_prefix cmp needed xs = let val ary = Array.fromList xs in sort_array_suffix cmp needed ary; Array.foldl (op ::) [] ary end (*** Convenience functions for synchronized access ***) fun synchronized_timed_value var time_limit = Synchronized.timed_access var time_limit (fn value => SOME (value, value)) fun synchronized_timed_change_result var time_limit f = Synchronized.timed_access var time_limit (SOME o f) fun synchronized_timed_change var time_limit f = synchronized_timed_change_result var time_limit (fn x => ((), f x)) fun mash_time_limit _ = SOME (seconds 0.1) (*** Isabelle-agnostic machine learning ***) structure MaSh = struct fun select_fact_idxs (big_number : real) recommends = List.app (fn at => let val (j, ov) = Array.sub (recommends, at) in Array.update (recommends, at, (j, big_number + ov)) end) fun wider_array_of_vector init vec = let val ary = Array.array init in Array.copyVec {src = vec, dst = ary, di = 0}; ary end val nb_def_prior_weight = 1000 (* FUDGE *) fun learn_facts (tfreq0, sfreq0, dffreq0) num_facts0 num_facts num_feats depss featss = let val tfreq = wider_array_of_vector (num_facts, 0) tfreq0 val sfreq = wider_array_of_vector (num_facts, Inttab.empty) sfreq0 val dffreq = wider_array_of_vector (num_feats, 0) dffreq0 fun learn_one th feats deps = let fun add_th weight t = let val im = Array.sub (sfreq, t) fun fold_fn s = Inttab.map_default (s, 0) (Integer.add weight) in map_array_at tfreq (Integer.add weight) t; Array.update (sfreq, t, fold fold_fn feats im) end val add_sym = map_array_at dffreq (Integer.add 1) in add_th nb_def_prior_weight th; List.app (add_th 1) deps; List.app add_sym feats end fun for i = if i = num_facts then () else (learn_one i (Vector.sub (featss, i)) (Vector.sub (depss, i)); for (i + 1)) in for num_facts0; (Array.vector tfreq, Array.vector sfreq, Array.vector dffreq) end fun naive_bayes (tfreq, sfreq, dffreq) num_facts max_suggs fact_idxs goal_feats = let val tau = 0.2 (* FUDGE *) val pos_weight = 5.0 (* FUDGE *) val def_val = ~18.0 (* FUDGE *) val init_val = 30.0 (* FUDGE *) val ln_afreq = Math.ln (Real.fromInt num_facts) val idf = Vector.map (fn i => ln_afreq - Math.ln (Real.fromInt i)) dffreq fun tfidf feat = Vector.sub (idf, feat) fun log_posterior i = let val tfreq = Real.fromInt (Vector.sub (tfreq, i)) fun add_feat (f, fw0) (res, sfh) = (case Inttab.lookup sfh f of SOME sf => (res + fw0 * tfidf f * Math.ln (pos_weight * Real.fromInt sf / tfreq), Inttab.delete f sfh) | NONE => (res + fw0 * tfidf f * def_val, sfh)) val (res, sfh) = fold add_feat goal_feats (init_val * Math.ln tfreq, Vector.sub (sfreq, i)) fun fold_sfh (f, sf) sow = sow + tfidf f * Math.ln (1.0 - Real.fromInt (sf - 1) / tfreq) val sum_of_weights = Inttab.fold fold_sfh sfh 0.0 in res + tau * sum_of_weights end val posterior = Array.tabulate (num_facts, (fn j => (j, log_posterior j))) fun ret at acc = if at = num_facts then acc else ret (at + 1) (Array.sub (posterior, at) :: acc) in select_fact_idxs 100000.0 posterior fact_idxs; sort_array_suffix (Real.compare o apply2 snd) max_suggs posterior; ret (Integer.max 0 (num_facts - max_suggs)) [] end val initial_k = 0 fun k_nearest_neighbors dffreq num_facts num_feats depss featss max_suggs fact_idxs goal_feats = let exception EXIT of unit val ln_afreq = Math.ln (Real.fromInt num_facts) fun tfidf feat = ln_afreq - Math.ln (Real.fromInt (Vector.sub (dffreq, feat))) val overlaps_sqr = Array.tabulate (num_facts, rpair 0.0) val feat_facts = Array.array (num_feats, []) val _ = Vector.foldl (fn (feats, fact) => (List.app (map_array_at feat_facts (cons fact)) feats; fact + 1)) 0 featss fun do_feat (s, sw0) = let val sw = sw0 * tfidf s val w6 = Math.pow (sw, 6.0 (* FUDGE *)) fun inc_overlap j = let val (_, ov) = Array.sub (overlaps_sqr, j) in Array.update (overlaps_sqr, j, (j, w6 + ov)) end in List.app inc_overlap (Array.sub (feat_facts, s)) end val _ = List.app do_feat goal_feats val _ = sort_array_suffix (Real.compare o apply2 snd) num_facts overlaps_sqr val no_recommends = Unsynchronized.ref 0 val recommends = Array.tabulate (num_facts, rpair 0.0) val age = Unsynchronized.ref 500000000.0 fun inc_recommend v j = let val (_, ov) = Array.sub (recommends, j) in if ov <= 0.0 then (no_recommends := !no_recommends + 1; Array.update (recommends, j, (j, !age + ov))) else Array.update (recommends, j, (j, v + ov)) end val k = Unsynchronized.ref 0 fun do_k k = if k >= num_facts then raise EXIT () else let val deps_factor = 2.7 (* FUDGE *) val (j, o2) = Array.sub (overlaps_sqr, num_facts - k - 1) val _ = inc_recommend o2 j val ds = Vector.sub (depss, j) val l = Real.fromInt (length ds) in List.app (inc_recommend (deps_factor * o2 / l)) ds end fun while1 () = if !k = initial_k + 1 then () else (do_k (!k); k := !k + 1; while1 ()) handle EXIT () => () fun while2 () = if !no_recommends >= max_suggs then () else (do_k (!k); k := !k + 1; age := !age - 10000.0; while2 ()) handle EXIT () => () fun ret acc at = if at = num_facts then acc else ret (Array.sub (recommends, at) :: acc) (at + 1) in while1 (); while2 (); select_fact_idxs 1000000000.0 recommends fact_idxs; sort_array_suffix (Real.compare o apply2 snd) max_suggs recommends; ret [] (Integer.max 0 (num_facts - max_suggs)) end (* experimental *) fun external_tool tool max_suggs learns goal_feats = let val ser = string_of_int (serial ()) (* poor person's attempt at thread-safety *) val ocs = TextIO.openOut ("adv_syms" ^ ser) val ocd = TextIO.openOut ("adv_deps" ^ ser) val ocq = TextIO.openOut ("adv_seq" ^ ser) val occ = TextIO.openOut ("adv_conj" ^ ser) fun os oc s = TextIO.output (oc, s) fun ol _ _ _ [] = () | ol _ f _ [e] = f e | ol oc f sep (h :: t) = (f h; os oc sep; ol oc f sep t) fun do_learn (name, feats, deps) = (os ocs name; os ocs ":"; ol ocs (os ocs o quote) ", " feats; os ocs "\n"; os ocd name; os ocd ":"; ol ocd (os ocd) " " deps; os ocd "\n"; os ocq name; os ocq "\n") fun forkexec no = let val cmd = "~/misc/" ^ tool ^ " adv_syms" ^ ser ^ " adv_deps" ^ ser ^ " " ^ string_of_int no ^ " adv_seq" ^ ser ^ " < adv_conj" ^ ser in fst (Isabelle_System.bash_output cmd) |> space_explode " " |> filter_out (curry (op =) "") end in (List.app do_learn learns; ol occ (os occ o quote) ", " (map fst goal_feats); TextIO.closeOut ocs; TextIO.closeOut ocd; TextIO.closeOut ocq; TextIO.closeOut occ; forkexec max_suggs) end fun k_nearest_neighbors_ext max_suggs = external_tool ("newknn/knn" ^ " " ^ string_of_int initial_k) max_suggs fun naive_bayes_ext max_suggs = external_tool "predict/nbayes" max_suggs fun query_external ctxt algorithm max_suggs learns goal_feats = (trace_msg ctxt (fn () => "MaSh query external " ^ commas (map fst goal_feats)); (case algorithm of MaSh_NB_Ext => naive_bayes_ext max_suggs learns goal_feats | MaSh_kNN_Ext => k_nearest_neighbors_ext max_suggs learns goal_feats)) fun query_internal ctxt algorithm num_facts num_feats (fact_names, featss, depss) (freqs as (_, _, dffreq)) fact_idxs max_suggs goal_feats int_goal_feats = let fun nb () = naive_bayes freqs num_facts max_suggs fact_idxs int_goal_feats |> map fst fun knn () = k_nearest_neighbors dffreq num_facts num_feats depss featss max_suggs fact_idxs int_goal_feats |> map fst in (trace_msg ctxt (fn () => "MaSh query internal " ^ commas (map fst goal_feats) ^ " from {" ^ elide_string 1000 (space_implode " " (Vector.foldr (op ::) [] fact_names)) ^ "}"); (case algorithm of MaSh_NB => nb () | MaSh_kNN => knn () | MaSh_NB_kNN => mesh_facts I (op =) max_suggs [(0.5 (* FUDGE *), (weight_facts_steeply (nb ()), [])), (0.5 (* FUDGE *), (weight_facts_steeply (knn ()), []))]) |> map (curry Vector.sub fact_names)) end end; (*** Persistent, stringly-typed state ***) fun meta_char c = if Char.isAlphaNum c orelse c = #"_" orelse c = #"." orelse c = #"(" orelse c = #")" orelse c = #"," orelse c = #"'" then String.str c else (* fixed width, in case more digits follow *) "%" ^ stringN_of_int 3 (Char.ord c) fun unmeta_chars accum [] = String.implode (rev accum) | unmeta_chars accum (#"%" :: d1 :: d2 :: d3 :: cs) = (case Int.fromString (String.implode [d1, d2, d3]) of SOME n => unmeta_chars (Char.chr n :: accum) cs | NONE => "" (* error *)) | unmeta_chars _ (#"%" :: _) = "" (* error *) | unmeta_chars accum (c :: cs) = unmeta_chars (c :: accum) cs val encode_str = String.translate meta_char val encode_strs = map encode_str #> space_implode " " fun decode_str s = if String.isSubstring "%" s then unmeta_chars [] (String.explode s) else s; fun decode_strs s = space_explode " " s |> String.isSubstring "%" s ? map decode_str; datatype proof_kind = Isar_Proof | Automatic_Proof | Isar_Proof_wegen_Prover_Flop fun str_of_proof_kind Isar_Proof = "i" | str_of_proof_kind Automatic_Proof = "a" | str_of_proof_kind Isar_Proof_wegen_Prover_Flop = "x" fun proof_kind_of_str "a" = Automatic_Proof | proof_kind_of_str "x" = Isar_Proof_wegen_Prover_Flop | proof_kind_of_str _ (* "i" *) = Isar_Proof fun add_edge_to name parent = Graph.default_node (parent, (Isar_Proof, [], [])) #> Graph.add_edge (parent, name) fun add_node kind name parents feats deps (accum as (access_G, (fact_xtab, feat_xtab), learns)) = let val fact_xtab' = add_to_xtab name fact_xtab in ((Graph.new_node (name, (kind, feats, deps)) access_G handle Graph.DUP _ => Graph.map_node name (K (kind, feats, deps)) access_G) |> fold (add_edge_to name) parents, (fact_xtab', fold maybe_add_to_xtab feats feat_xtab), (name, feats, deps) :: learns) end handle Symtab.DUP _ => accum (* robustness (in case the state file violates the invariant) *) fun try_graph ctxt when def f = f () handle Graph.CYCLES (cycle :: _) => (trace_msg ctxt (fn () => "Cycle involving " ^ commas cycle ^ " when " ^ when); def) | Graph.DUP name => (trace_msg ctxt (fn () => "Duplicate fact " ^ quote name ^ " when " ^ when); def) | Graph.UNDEF name => (trace_msg ctxt (fn () => "Unknown fact " ^ quote name ^ " when " ^ when); def) | exn => if Exn.is_interrupt exn then Exn.reraise exn else (trace_msg ctxt (fn () => "Internal error when " ^ when ^ ":\n" ^ Runtime.exn_message exn); def) fun graph_info G = string_of_int (length (Graph.keys G)) ^ " node(s), " ^ string_of_int (fold (Integer.add o length o snd) (Graph.dest G) 0) ^ " edge(s), " ^ string_of_int (length (Graph.maximals G)) ^ " maximal" type ffds = string vector * int list vector * int list vector type freqs = int vector * int Inttab.table vector * int vector type mash_state = {access_G : (proof_kind * string list * string list) Graph.T, xtabs : xtab * xtab, ffds : ffds, freqs : freqs, dirty_facts : string list option} val empty_xtabs = (empty_xtab, empty_xtab) val empty_ffds = (Vector.fromList [], Vector.fromList [], Vector.fromList []) : ffds val empty_freqs = (Vector.fromList [], Vector.fromList [], Vector.fromList []) : freqs val empty_state = {access_G = Graph.empty, xtabs = empty_xtabs, ffds = empty_ffds, freqs = empty_freqs, dirty_facts = SOME []} : mash_state fun recompute_ffds_freqs_from_learns (learns : (string * string list * string list) list) ((num_facts, fact_tab), (num_feats, feat_tab)) num_facts0 (fact_names0, featss0, depss0) freqs0 = let val fact_names = Vector.concat [fact_names0, Vector.fromList (map #1 learns)] val featss = Vector.concat [featss0, Vector.fromList (map (map_filter (Symtab.lookup feat_tab) o #2) learns)] val depss = Vector.concat [depss0, Vector.fromList (map (map_filter (Symtab.lookup fact_tab) o #3) learns)] in ((fact_names, featss, depss), MaSh.learn_facts freqs0 num_facts0 num_facts num_feats depss featss) end fun reorder_learns (num_facts, fact_tab) learns = let val ary = Array.array (num_facts, ("", [], [])) in List.app (fn learn as (fact, _, _) => Array.update (ary, the (Symtab.lookup fact_tab fact), learn)) learns; Array.foldr (op ::) [] ary end fun recompute_ffds_freqs_from_access_G access_G (xtabs as (fact_xtab, _)) = let val learns = Graph.schedule (fn _ => fn (fact, (_, feats, deps)) => (fact, feats, deps)) access_G |> reorder_learns fact_xtab in recompute_ffds_freqs_from_learns learns xtabs 0 empty_ffds empty_freqs end local val version = "*** MaSh version 20190121 ***" exception FILE_VERSION_TOO_NEW of unit fun extract_node line = (case space_explode ":" line of [head, tail] => (case (space_explode " " head, map (unprefix " ") (space_explode ";" tail)) of ([kind, name], [parents, feats, deps]) => SOME (proof_kind_of_str kind, decode_str name, decode_strs parents, decode_strs feats, decode_strs deps) | _ => NONE) | _ => NONE) fun would_load_state (memory_time, _) = let val path = state_file () in (case try OS.FileSys.modTime (File.platform_path path) of NONE => false | SOME disk_time => memory_time < disk_time) end; fun load_state ctxt (time_state as (memory_time, _)) = let val path = state_file () in (case try OS.FileSys.modTime (File.platform_path path) of NONE => time_state | SOME disk_time => if memory_time >= disk_time then time_state else (disk_time, (case try File.read_lines path of SOME (version' :: node_lines) => let fun extract_line_and_add_node line = (case extract_node line of NONE => I (* should not happen *) | SOME (kind, name, parents, feats, deps) => add_node kind name parents feats deps) val empty_G_etc = (Graph.empty, empty_xtabs, []) val (access_G, xtabs, rev_learns) = (case string_ord (version', version) of EQUAL => try_graph ctxt "loading state" empty_G_etc (fn () => fold extract_line_and_add_node node_lines empty_G_etc) | LESS => (remove_state_file (); empty_G_etc) (* cannot parse old file *) | GREATER => raise FILE_VERSION_TOO_NEW ()) val (ffds, freqs) = recompute_ffds_freqs_from_learns (rev rev_learns) xtabs 0 empty_ffds empty_freqs in trace_msg ctxt (fn () => "Loaded fact graph (" ^ graph_info access_G ^ ")"); {access_G = access_G, xtabs = xtabs, ffds = ffds, freqs = freqs, dirty_facts = SOME []} end | _ => empty_state))) end fun str_of_entry (kind, name, parents, feats, deps) = str_of_proof_kind kind ^ " " ^ encode_str name ^ ": " ^ encode_strs parents ^ "; " ^ encode_strs feats ^ "; " ^ encode_strs deps ^ "\n" fun save_state _ (time_state as (_, {dirty_facts = SOME [], ...})) = time_state | save_state ctxt (memory_time, {access_G, xtabs, ffds, freqs, dirty_facts}) = let fun append_entry (name, ((kind, feats, deps), (parents, _))) = cons (kind, name, Graph.Keys.dest parents, feats, deps) val path = state_file () val dirty_facts' = (case try OS.FileSys.modTime (File.platform_path path) of NONE => NONE | SOME disk_time => if disk_time <= memory_time then dirty_facts else NONE) val (banner, entries) = (case dirty_facts' of SOME names => (NONE, fold (append_entry o Graph.get_entry access_G) names []) | NONE => (SOME (version ^ "\n"), Graph.fold append_entry access_G [])) in (case banner of SOME s => File.write path s | NONE => (); entries |> chunk_list 500 |> List.app (File.append path o implode o map str_of_entry)) handle IO.Io _ => (); trace_msg ctxt (fn () => "Saved fact graph (" ^ graph_info access_G ^ (case dirty_facts of SOME dirty_facts => "; " ^ string_of_int (length dirty_facts) ^ " dirty fact(s)" | _ => "") ^ ")"); (Time.now (), {access_G = access_G, xtabs = xtabs, ffds = ffds, freqs = freqs, dirty_facts = SOME []}) end val global_state = Synchronized.var "Sledgehammer_MaSh.global_state" (Time.zeroTime, empty_state) in fun map_state ctxt f = (trace_msg ctxt (fn () => "Changing MaSh state"); synchronized_timed_change global_state mash_time_limit (load_state ctxt ##> f #> save_state ctxt)) |> ignore handle FILE_VERSION_TOO_NEW () => () fun peek_state ctxt = (trace_msg ctxt (fn () => "Peeking at MaSh state"); (case synchronized_timed_value global_state mash_time_limit of NONE => NONE | SOME state => if would_load_state state then NONE else SOME state)) fun get_state ctxt = (trace_msg ctxt (fn () => "Retrieving MaSh state"); synchronized_timed_change_result global_state mash_time_limit (perhaps (try (load_state ctxt)) #> `snd)) fun clear_state ctxt = (trace_msg ctxt (fn () => "Clearing MaSh state"); Synchronized.change global_state (fn _ => (remove_state_file (); (Time.zeroTime, empty_state)))) end (*** Isabelle helpers ***) fun crude_printed_term size t = let fun term _ (res, 0) = (res, 0) | term (t $ u) (res, size) = let val (res, size) = term t (res ^ "(", size) val (res, size) = term u (res ^ " ", size) in (res ^ ")", size) end | term (Abs (s, _, t)) (res, size) = term t (res ^ "%" ^ s ^ ".", size - 1) | term (Bound n) (res, size) = (res ^ "#" ^ string_of_int n, size - 1) | term (Const (s, _)) (res, size) = (res ^ Long_Name.base_name s, size - 1) | term (Free (s, _)) (res, size) = (res ^ s, size - 1) | term (Var ((s, _), _)) (res, size) = (res ^ s, size - 1) in fst (term t ("", size)) end fun nickname_of_thm th = if Thm.has_name_hint th then let val hint = Thm.get_name_hint th in (* There must be a better way to detect local facts. *) (case Long_Name.dest_local hint of SOME suf => Long_Name.implode [Thm.theory_name th, suf, crude_printed_term 25 (Thm.prop_of th)] | NONE => hint) end else crude_printed_term 50 (Thm.prop_of th) fun find_suggested_facts ctxt facts = let fun add (fact as (_, th)) = Symtab.default (nickname_of_thm th, fact) val tab = fold add facts Symtab.empty fun lookup nick = Symtab.lookup tab nick |> tap (fn NONE => trace_msg ctxt (fn () => "Cannot find " ^ quote nick) | _ => ()) in map_filter lookup end fun free_feature_of s = "f" ^ s fun thy_feature_of s = "y" ^ s fun type_feature_of s = "t" ^ s fun class_feature_of s = "s" ^ s val local_feature = "local" fun crude_thm_ord ctxt = let val ancestor_lengths = fold (fn thy => Symtab.update (Context.theory_name thy, length (Context.ancestors_of thy))) (Theory.nodes_of (Proof_Context.theory_of ctxt)) Symtab.empty val ancestor_length = Symtab.lookup ancestor_lengths o Context.theory_id_name fun crude_theory_ord p = if Context.eq_thy_id p then EQUAL else if Context.proper_subthy_id p then LESS else if Context.proper_subthy_id (swap p) then GREATER else (case apply2 ancestor_length p of (SOME m, SOME n) => (case int_ord (m, n) of EQUAL => string_ord (apply2 Context.theory_id_name p) | ord => ord) | _ => string_ord (apply2 Context.theory_id_name p)) in fn p => (case crude_theory_ord (apply2 Thm.theory_id p) of EQUAL => (* The hack below is necessary because of odd dependencies that are not reflected in the theory comparison. *) let val q = apply2 nickname_of_thm p in (* Hack to put "xxx_def" before "xxxI" and "xxxE" *) (case bool_ord (apply2 (String.isSuffix "_def") (swap q)) of EQUAL => string_ord q | ord => ord) end | ord => ord) end; val thm_less_eq = Context.subthy_id o apply2 Thm.theory_id fun thm_less p = thm_less_eq p andalso not (thm_less_eq (swap p)) val freezeT = Type.legacy_freeze_type fun freeze (t $ u) = freeze t $ freeze u | freeze (Abs (s, T, t)) = Abs (s, freezeT T, freeze t) | freeze (Var ((s, _), T)) = Free (s, freezeT T) | freeze (Const (s, T)) = Const (s, freezeT T) | freeze (Free (s, T)) = Free (s, freezeT T) | freeze t = t fun goal_of_thm thy = Thm.prop_of #> freeze #> Thm.global_cterm_of thy #> Goal.init fun run_prover_for_mash ctxt params prover goal_name facts goal = let val problem = {comment = "Goal: " ^ goal_name, state = Proof.init ctxt, goal = goal, subgoal = 1, subgoal_count = 1, factss = [("", facts)], found_proof = I} in get_minimizing_prover ctxt MaSh (K ()) prover params problem end val bad_types = [\<^type_name>\prop\, \<^type_name>\bool\, \<^type_name>\fun\] val crude_str_of_sort = space_implode "," o map Long_Name.base_name o subtract (op =) \<^sort>\type\ fun crude_str_of_typ (Type (s, [])) = Long_Name.base_name s | crude_str_of_typ (Type (s, Ts)) = Long_Name.base_name s ^ implode (map crude_str_of_typ Ts) | crude_str_of_typ (TFree (_, S)) = crude_str_of_sort S | crude_str_of_typ (TVar (_, S)) = crude_str_of_sort S fun maybe_singleton_str "" = [] | maybe_singleton_str s = [s] val max_pat_breadth = 5 (* FUDGE *) fun term_features_of ctxt thy_name term_max_depth type_max_depth ts = let val thy = Proof_Context.theory_of ctxt val fixes = map snd (Variable.dest_fixes ctxt) val classes = Sign.classes_of thy fun add_classes \<^sort>\type\ = I | add_classes S = fold (`(Sorts.super_classes classes) #> swap #> op :: #> subtract (op =) \<^sort>\type\ #> map class_feature_of #> union (op =)) S fun pattify_type 0 _ = [] | pattify_type _ (Type (s, [])) = if member (op =) bad_types s then [] else [s] | pattify_type depth (Type (s, U :: Ts)) = let val T = Type (s, Ts) val ps = take max_pat_breadth (pattify_type depth T) val qs = take max_pat_breadth ("" :: pattify_type (depth - 1) U) in map_product (fn p => fn "" => p | q => p ^ "(" ^ q ^ ")") ps qs end | pattify_type _ (TFree (_, S)) = maybe_singleton_str (crude_str_of_sort S) | pattify_type _ (TVar (_, S)) = maybe_singleton_str (crude_str_of_sort S) fun add_type_pat depth T = union (op =) (map type_feature_of (pattify_type depth T)) fun add_type_pats 0 _ = I | add_type_pats depth t = add_type_pat depth t #> add_type_pats (depth - 1) t fun add_type T = add_type_pats type_max_depth T #> fold_atyps_sorts (add_classes o snd) T fun add_subtypes (T as Type (_, Ts)) = add_type T #> fold add_subtypes Ts | add_subtypes T = add_type T fun pattify_term _ 0 _ = [] | pattify_term _ _ (Const (s, _)) = if is_widely_irrelevant_const s then [] else [s] | pattify_term _ _ (Free (s, T)) = maybe_singleton_str (crude_str_of_typ T) |> (if member (op =) fixes s then cons (free_feature_of (Long_Name.append thy_name s)) else I) | pattify_term _ _ (Var (_, T)) = maybe_singleton_str (crude_str_of_typ T) | pattify_term Ts _ (Bound j) = maybe_singleton_str (crude_str_of_typ (nth Ts j)) | pattify_term Ts depth (t $ u) = let val ps = take max_pat_breadth (pattify_term Ts depth t) val qs = take max_pat_breadth ("" :: pattify_term Ts (depth - 1) u) in map_product (fn p => fn "" => p | q => p ^ "(" ^ q ^ ")") ps qs end | pattify_term _ _ _ = [] fun add_term_pat Ts = union (op =) oo pattify_term Ts fun add_term_pats _ 0 _ = I | add_term_pats Ts depth t = add_term_pat Ts depth t #> add_term_pats Ts (depth - 1) t fun add_term Ts = add_term_pats Ts term_max_depth fun add_subterms Ts t = (case strip_comb t of (Const (s, T), args) => (not (is_widely_irrelevant_const s) ? add_term Ts t) #> add_subtypes T #> fold (add_subterms Ts) args | (head, args) => (case head of Free (_, T) => add_term Ts t #> add_subtypes T | Var (_, T) => add_subtypes T | Abs (_, T, body) => add_subtypes T #> add_subterms (T :: Ts) body | _ => I) #> fold (add_subterms Ts) args) in fold (add_subterms []) ts [] end val term_max_depth = 2 val type_max_depth = 1 (* TODO: Generate type classes for types? *) fun features_of ctxt thy_name (scope, _) ts = thy_feature_of thy_name :: term_features_of ctxt thy_name term_max_depth type_max_depth ts |> scope <> Global ? cons local_feature (* Too many dependencies is a sign that a decision procedure is at work. There is not much to learn from such proofs. *) val max_dependencies = 20 (* FUDGE *) val prover_default_max_facts = 25 (* FUDGE *) (* "type_definition_xxx" facts are characterized by their use of "CollectI". *) val typedef_dep = nickname_of_thm @{thm CollectI} (* Mysterious parts of the class machinery create lots of proofs that refer exclusively to "someI_ex" (and to some internal constructions). *) val class_some_dep = nickname_of_thm @{thm someI_ex} val fundef_ths = @{thms fundef_ex1_existence fundef_ex1_uniqueness fundef_ex1_iff fundef_default_value} |> map nickname_of_thm (* "Rep_xxx_inject", "Abs_xxx_inverse", etc., are derived using these facts. *) val typedef_ths = @{thms type_definition.Abs_inverse type_definition.Rep_inverse type_definition.Rep type_definition.Rep_inject type_definition.Abs_inject type_definition.Rep_cases type_definition.Abs_cases type_definition.Rep_induct type_definition.Abs_induct type_definition.Rep_range type_definition.Abs_image} |> map nickname_of_thm fun is_size_def [dep] th = (case first_field ".rec" dep of SOME (pref, _) => (case first_field ".size" (nickname_of_thm th) of SOME (pref', _) => pref = pref' | NONE => false) | NONE => false) | is_size_def _ _ = false fun trim_dependencies deps = if length deps > max_dependencies then NONE else SOME deps fun isar_dependencies_of name_tabs th = thms_in_proof max_dependencies (SOME name_tabs) th |> Option.map (fn deps => if deps = [typedef_dep] orelse deps = [class_some_dep] orelse exists (member (op =) fundef_ths) deps orelse exists (member (op =) typedef_ths) deps orelse is_size_def deps th then [] else deps) fun prover_dependencies_of ctxt (params as {verbose, max_facts, ...}) prover auto_level facts name_tabs th = (case isar_dependencies_of name_tabs th of SOME [] => (false, []) | isar_deps0 => let val isar_deps = these isar_deps0 val thy = Proof_Context.theory_of ctxt val goal = goal_of_thm thy th val name = nickname_of_thm th val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal goal 1 ctxt val facts = facts |> filter (fn (_, th') => thm_less (th', th)) fun nickify ((_, stature), th) = ((nickname_of_thm th, stature), th) fun is_dep dep (_, th) = (nickname_of_thm th = dep) fun add_isar_dep facts dep accum = if exists (is_dep dep) accum then accum else (case find_first (is_dep dep) facts of SOME ((_, status), th) => accum @ [(("", status), th)] | NONE => accum (* should not happen *)) val mepo_facts = facts |> mepo_suggested_facts ctxt params (max_facts |> the_default prover_default_max_facts) NONE hyp_ts concl_t val facts = mepo_facts |> fold (add_isar_dep facts) isar_deps |> map nickify val num_isar_deps = length isar_deps in if verbose andalso auto_level = 0 then writeln ("MaSh: " ^ quote prover ^ " on " ^ quote name ^ " with " ^ string_of_int num_isar_deps ^ " + " ^ string_of_int (length facts - num_isar_deps) ^ " facts") else (); (case run_prover_for_mash ctxt params prover name facts goal of {outcome = NONE, used_facts, ...} => (if verbose andalso auto_level = 0 then let val num_facts = length used_facts in writeln ("Found proof with " ^ string_of_int num_facts ^ " fact" ^ plural_s num_facts) end else (); (true, map fst used_facts)) | _ => (false, isar_deps)) end) (*** High-level communication with MaSh ***) (* In the following functions, chunks are risers w.r.t. "thm_less_eq". *) fun chunks_and_parents_for chunks th = let fun insert_parent new parents = let val parents = parents |> filter_out (fn p => thm_less_eq (p, new)) in parents |> forall (fn p => not (thm_less_eq (new, p))) parents ? cons new end fun rechunk seen (rest as th' :: ths) = if thm_less_eq (th', th) then (rev seen, rest) else rechunk (th' :: seen) ths fun do_chunk [] accum = accum | do_chunk (chunk as hd_chunk :: _) (chunks, parents) = if thm_less_eq (hd_chunk, th) then (chunk :: chunks, insert_parent hd_chunk parents) else if thm_less_eq (List.last chunk, th) then let val (front, back as hd_back :: _) = rechunk [] chunk in (front :: back :: chunks, insert_parent hd_back parents) end else (chunk :: chunks, parents) in fold_rev do_chunk chunks ([], []) |>> cons [] ||> map nickname_of_thm end fun attach_parents_to_facts _ [] = [] | attach_parents_to_facts old_facts (facts as (_, th) :: _) = let fun do_facts _ [] = [] | do_facts (_, parents) [fact] = [(parents, fact)] | do_facts (chunks, parents) ((fact as (_, th)) :: (facts as (_, th') :: _)) = let val chunks = app_hd (cons th) chunks val chunks_and_parents' = if thm_less_eq (th, th') andalso Thm.theory_name th = Thm.theory_name th' then (chunks, [nickname_of_thm th]) else chunks_and_parents_for chunks th' in (parents, fact) :: do_facts chunks_and_parents' facts end in old_facts @ facts |> do_facts (chunks_and_parents_for [[]] th) |> drop (length old_facts) end fun is_fact_in_graph access_G = can (Graph.get_node access_G) o nickname_of_thm val chained_feature_factor = 0.5 (* FUDGE *) val extra_feature_factor = 0.1 (* FUDGE *) val num_extra_feature_facts = 10 (* FUDGE *) val max_proximity_facts = 100 (* FUDGE *) fun find_mash_suggestions ctxt max_facts suggs facts chained raw_unknown = let val inter_fact = inter (eq_snd Thm.eq_thm_prop) val raw_mash = find_suggested_facts ctxt facts suggs val proximate = take max_proximity_facts facts val unknown_chained = inter_fact raw_unknown chained val unknown_proximate = inter_fact raw_unknown proximate val mess = [(0.9 (* FUDGE *), (map (rpair 1.0) unknown_chained, [])), (0.4 (* FUDGE *), (weight_facts_smoothly unknown_proximate, [])), (0.1 (* FUDGE *), (weight_facts_steeply raw_mash, raw_unknown))] val unknown = raw_unknown |> fold (subtract (eq_snd Thm.eq_thm_prop)) [unknown_chained, unknown_proximate] in (mesh_facts (fact_distinct (op aconv)) (eq_snd (gen_eq_thm ctxt)) max_facts mess, unknown) end fun mash_suggested_facts ctxt thy_name ({debug, ...} : params) max_suggs hyp_ts concl_t facts = let val algorithm = the_mash_algorithm () val facts = facts |> rev_sort_list_prefix (crude_thm_ord ctxt o apply2 snd) (Int.max (num_extra_feature_facts, max_proximity_facts)) val chained = filter (fn ((_, (scope, _)), _) => scope = Chained) facts fun fact_has_right_theory (_, th) = thy_name = Thm.theory_name th fun chained_or_extra_features_of factor (((_, stature), th), weight) = [Thm.prop_of th] |> features_of ctxt (Thm.theory_name th) stature |> map (rpair (weight * factor)) in (case get_state ctxt of NONE => ([], []) | SOME {access_G, xtabs = ((num_facts, fact_tab), (num_feats, feat_tab)), ffds, freqs, ...} => let val goal_feats0 = features_of ctxt thy_name (Local, General) (concl_t :: hyp_ts) val chained_feats = chained |> map (rpair 1.0) |> map (chained_or_extra_features_of chained_feature_factor) |> rpair [] |-> fold (union (eq_fst (op =))) val extra_feats = facts |> take (Int.max (0, num_extra_feature_facts - length chained)) |> filter fact_has_right_theory |> weight_facts_steeply |> map (chained_or_extra_features_of extra_feature_factor) |> rpair [] |-> fold (union (eq_fst (op =))) val goal_feats = fold (union (eq_fst (op =))) [chained_feats, extra_feats] (map (rpair 1.0) goal_feats0) |> debug ? sort (Real.compare o swap o apply2 snd) val fact_idxs = map_filter (Symtab.lookup fact_tab o nickname_of_thm o snd) facts val suggs = if algorithm = MaSh_NB_Ext orelse algorithm = MaSh_kNN_Ext then let val learns = Graph.schedule (fn _ => fn (fact, (_, feats, deps)) => (fact, feats, deps)) access_G in MaSh.query_external ctxt algorithm max_suggs learns goal_feats end else let val int_goal_feats = map_filter (fn (s, w) => Option.map (rpair w) (Symtab.lookup feat_tab s)) goal_feats in MaSh.query_internal ctxt algorithm num_facts num_feats ffds freqs fact_idxs max_suggs goal_feats int_goal_feats end val unknown = filter_out (is_fact_in_graph access_G o snd) facts in find_mash_suggestions ctxt max_suggs suggs facts chained unknown |> apply2 (map fact_of_raw_fact) end) end fun mash_unlearn ctxt = (clear_state ctxt; writeln "Reset MaSh") fun learn_wrt_access_graph ctxt (name, parents, feats, deps) (accum as (access_G, (fact_xtab, feat_xtab))) = let fun maybe_learn_from from (accum as (parents, access_G)) = try_graph ctxt "updating graph" accum (fn () => (from :: parents, Graph.add_edge_acyclic (from, name) access_G)) val access_G = access_G |> Graph.default_node (name, (Isar_Proof, feats, deps)) val (parents, access_G) = ([], access_G) |> fold maybe_learn_from parents val (deps, _) = ([], access_G) |> fold maybe_learn_from deps val fact_xtab = add_to_xtab name fact_xtab val feat_xtab = fold maybe_add_to_xtab feats feat_xtab in (SOME (name, parents, feats, deps), (access_G, (fact_xtab, feat_xtab))) end handle Symtab.DUP _ => (NONE, accum) (* facts sometimes have the same name, confusingly *) fun relearn_wrt_access_graph ctxt (name, deps) access_G = let fun maybe_relearn_from from (accum as (parents, access_G)) = try_graph ctxt "updating graph" accum (fn () => (from :: parents, Graph.add_edge_acyclic (from, name) access_G)) val access_G = access_G |> Graph.map_node name (fn (_, feats, _) => (Automatic_Proof, feats, deps)) val (deps, _) = ([], access_G) |> fold maybe_relearn_from deps in ((name, deps), access_G) end fun flop_wrt_access_graph name = Graph.map_node name (fn (_, feats, deps) => (Isar_Proof_wegen_Prover_Flop, feats, deps)) val learn_timeout_slack = 20.0 fun launch_thread timeout task = let val hard_timeout = Time.scale learn_timeout_slack timeout val birth_time = Time.now () val death_time = birth_time + Timeout.scale_time hard_timeout val desc = ("Machine learner for Sledgehammer", "") in Async_Manager_Legacy.thread MaShN birth_time death_time desc task end fun anonymous_proof_name () = Date.fmt (anonymous_proof_prefix ^ "%Y%m%d.%H%M%S.") (Date.fromTimeLocal (Time.now ())) ^ serial_string () fun mash_learn_proof ctxt ({timeout, ...} : params) t used_ths = if not (null used_ths) andalso is_mash_enabled () then launch_thread timeout (fn () => let val thy = Proof_Context.theory_of ctxt val feats = features_of ctxt (Context.theory_name thy) (Local, General) [t] in map_state ctxt (fn {access_G, xtabs as ((num_facts0, _), _), ffds, freqs, dirty_facts} => let val deps = used_ths |> filter (is_fact_in_graph access_G) |> map nickname_of_thm val name = anonymous_proof_name () val (access_G', xtabs', rev_learns) = add_node Automatic_Proof name [] (* ignore parents *) feats deps (access_G, xtabs, []) val (ffds', freqs') = recompute_ffds_freqs_from_learns (rev rev_learns) xtabs' num_facts0 ffds freqs in {access_G = access_G', xtabs = xtabs', ffds = ffds', freqs = freqs', dirty_facts = Option.map (cons name) dirty_facts} end); (true, "") end) else () fun sendback sub = Active.sendback_markup_command (sledgehammerN ^ " " ^ sub) val commit_timeout = seconds 30.0 (* The timeout is understood in a very relaxed fashion. *) fun mash_learn_facts ctxt (params as {debug, verbose, ...}) prover auto_level run_prover learn_timeout facts = let val timer = Timer.startRealTimer () fun next_commit_time () = Timer.checkRealTimer timer + commit_timeout in (case get_state ctxt of NONE => "MaSh is busy\nPlease try again later" | SOME {access_G, ...} => let val is_in_access_G = is_fact_in_graph access_G o snd val no_new_facts = forall is_in_access_G facts in if no_new_facts andalso not run_prover then if auto_level < 2 then "No new " ^ (if run_prover then "automatic" else "Isar") ^ " proofs to learn" ^ (if auto_level = 0 andalso not run_prover then "\n\nHint: Try " ^ sendback learn_proverN ^ " to learn from an automatic prover" else "") else "" else let val name_tabs = build_name_tables nickname_of_thm facts fun deps_of status th = if status = Non_Rec_Def orelse status = Rec_Def then SOME [] else if run_prover then prover_dependencies_of ctxt params prover auto_level facts name_tabs th |> (fn (false, _) => NONE | (true, deps) => trim_dependencies deps) else isar_dependencies_of name_tabs th fun do_commit [] [] [] state = state | do_commit learns relearns flops {access_G, xtabs as ((num_facts0, _), _), ffds, freqs, dirty_facts} = let val was_empty = Graph.is_empty access_G val (learns, (access_G', xtabs')) = fold_map (learn_wrt_access_graph ctxt) learns (access_G, xtabs) |>> map_filter I val (relearns, access_G'') = fold_map (relearn_wrt_access_graph ctxt) relearns access_G' val access_G''' = access_G'' |> fold flop_wrt_access_graph flops val dirty_facts' = (case (was_empty, dirty_facts) of (false, SOME names) => SOME (map #1 learns @ map #1 relearns @ names) | _ => NONE) val (ffds', freqs') = if null relearns then recompute_ffds_freqs_from_learns (map (fn (name, _, feats, deps) => (name, feats, deps)) learns) xtabs' num_facts0 ffds freqs else recompute_ffds_freqs_from_access_G access_G''' xtabs' in {access_G = access_G''', xtabs = xtabs', ffds = ffds', freqs = freqs', dirty_facts = dirty_facts'} end fun commit last learns relearns flops = (if debug andalso auto_level = 0 then writeln "Committing..." else (); map_state ctxt (do_commit (rev learns) relearns flops); if not last andalso auto_level = 0 then let val num_proofs = length learns + length relearns in writeln ("Learned " ^ string_of_int num_proofs ^ " " ^ (if run_prover then "automatic" else "Isar") ^ " proof" ^ plural_s num_proofs ^ " in the last " ^ string_of_time commit_timeout) end else ()) fun learn_new_fact _ (accum as (_, (_, _, true))) = accum | learn_new_fact (parents, ((_, stature as (_, status)), th)) (learns, (num_nontrivial, next_commit, _)) = let val name = nickname_of_thm th val feats = features_of ctxt (Thm.theory_name th) stature [Thm.prop_of th] val deps = these (deps_of status th) val num_nontrivial = num_nontrivial |> not (null deps) ? Integer.add 1 val learns = (name, parents, feats, deps) :: learns val (learns, next_commit) = if Timer.checkRealTimer timer > next_commit then (commit false learns [] []; ([], next_commit_time ())) else (learns, next_commit) val timed_out = Timer.checkRealTimer timer > learn_timeout in (learns, (num_nontrivial, next_commit, timed_out)) end val (num_new_facts, num_nontrivial) = if no_new_facts then (0, 0) else let val new_facts = facts |> sort (crude_thm_ord ctxt o apply2 snd) |> map (pair []) (* ignore parents *) |> filter_out (is_in_access_G o snd) val (learns, (num_nontrivial, _, _)) = ([], (0, next_commit_time (), false)) |> fold learn_new_fact new_facts in commit true learns [] []; (length new_facts, num_nontrivial) end fun relearn_old_fact _ (accum as (_, (_, _, true))) = accum | relearn_old_fact ((_, (_, status)), th) ((relearns, flops), (num_nontrivial, next_commit, _)) = let val name = nickname_of_thm th val (num_nontrivial, relearns, flops) = (case deps_of status th of SOME deps => (num_nontrivial + 1, (name, deps) :: relearns, flops) | NONE => (num_nontrivial, relearns, name :: flops)) val (relearns, flops, next_commit) = if Timer.checkRealTimer timer > next_commit then (commit false [] relearns flops; ([], [], next_commit_time ())) else (relearns, flops, next_commit) val timed_out = Timer.checkRealTimer timer > learn_timeout in ((relearns, flops), (num_nontrivial, next_commit, timed_out)) end val num_nontrivial = if not run_prover then num_nontrivial else let val max_isar = 1000 * max_dependencies fun priority_of th = Random.random_range 0 max_isar + (case try (Graph.get_node access_G) (nickname_of_thm th) of SOME (Isar_Proof, _, deps) => ~100 * length deps | SOME (Automatic_Proof, _, _) => 2 * max_isar | SOME (Isar_Proof_wegen_Prover_Flop, _, _) => max_isar | NONE => 0) val old_facts = facts |> filter is_in_access_G |> map (`(priority_of o snd)) |> sort (int_ord o apply2 fst) |> map snd val ((relearns, flops), (num_nontrivial, _, _)) = (([], []), (num_nontrivial, next_commit_time (), false)) |> fold relearn_old_fact old_facts in commit true [] relearns flops; num_nontrivial end in if verbose orelse auto_level < 2 then "Learned " ^ string_of_int num_new_facts ^ " fact" ^ plural_s num_new_facts ^ " and " ^ string_of_int num_nontrivial ^ " nontrivial " ^ (if run_prover then "automatic and " else "") ^ "Isar proof" ^ plural_s num_nontrivial ^ (if verbose then " in " ^ string_of_time (Timer.checkRealTimer timer) else "") else "" end end) end -fun mash_learn ctxt (params as {provers, timeout, ...}) fact_override chained run_prover = +fun mash_learn ctxt (params as {provers, timeout, induction_rules, ...}) fact_override chained run_prover = let val css = Sledgehammer_Fact.clasimpset_rule_table_of ctxt - val ctxt = ctxt |> Config.put instantiate_inducts false + val induction_rules = the_default Exclude induction_rules val facts = - nearly_all_facts ctxt false fact_override Keyword.empty_keywords css chained [] \<^prop>\True\ + nearly_all_facts ctxt induction_rules fact_override Keyword.empty_keywords css chained [] + \<^prop>\True\ |> sort (crude_thm_ord ctxt o apply2 snd o swap) val num_facts = length facts val prover = hd provers fun learn auto_level run_prover = mash_learn_facts ctxt params prover auto_level run_prover one_year facts |> writeln in if run_prover then (writeln ("MaShing through " ^ string_of_int num_facts ^ " fact" ^ plural_s num_facts ^ " for automatic proofs (" ^ quote prover ^ " timeout: " ^ string_of_time timeout ^ ").\n\nCollecting Isar proofs first..."); learn 1 false; writeln "Now collecting automatic proofs\n\ \This may take several hours; you can safely stop the learning process at any point"; learn 0 true) else (writeln ("MaShing through " ^ string_of_int num_facts ^ " fact" ^ plural_s num_facts ^ " for Isar proofs..."); learn 0 false) end fun mash_can_suggest_facts ctxt = (case get_state ctxt of NONE => false | SOME {access_G, ...} => not (Graph.is_empty access_G)) fun mash_can_suggest_facts_fast ctxt = (case peek_state ctxt of NONE => false | SOME (_, {access_G, ...}) => not (Graph.is_empty access_G)) (* Generate more suggestions than requested, because some might be thrown out later for various reasons (e.g., duplicates). *) fun generous_max_suggestions max_facts = 2 * max_facts + 25 (* FUDGE *) val mepo_weight = 0.5 (* FUDGE *) val mash_weight = 0.5 (* FUDGE *) val max_facts_to_learn_before_query = 100 (* FUDGE *) (* The threshold should be large enough so that MaSh does not get activated for Auto Sledgehammer. *) val min_secs_for_learning = 10 fun relevant_facts ctxt (params as {verbose, learn, fact_filter, timeout, ...}) prover max_facts ({add, only, ...} : fact_override) hyp_ts concl_t facts = if not (subset (op =) (the_list fact_filter, fact_filters)) then error ("Unknown fact filter: " ^ quote (the fact_filter)) else if only then [("", map fact_of_raw_fact facts)] else if max_facts <= 0 orelse null facts then [("", [])] else let val thy_name = Context.theory_name (Proof_Context.theory_of ctxt) fun maybe_launch_thread exact min_num_facts_to_learn = if not (Async_Manager_Legacy.has_running_threads MaShN) andalso Time.toSeconds timeout >= min_secs_for_learning then let val timeout = Time.scale learn_timeout_slack timeout in (if verbose then writeln ("Started MaShing through " ^ (if exact then "" else "up to ") ^ string_of_int min_num_facts_to_learn ^ " fact" ^ plural_s min_num_facts_to_learn ^ " in the background") else ()); launch_thread timeout (fn () => (true, mash_learn_facts ctxt params prover 2 false timeout facts)) end else () val mash_enabled = is_mash_enabled () val mash_fast = mash_can_suggest_facts_fast ctxt fun please_learn () = if mash_fast then (case get_state ctxt of NONE => maybe_launch_thread false (length facts) | SOME {access_G, xtabs = ((num_facts0, _), _), ...} => let val is_in_access_G = is_fact_in_graph access_G o snd val min_num_facts_to_learn = length facts - num_facts0 in if min_num_facts_to_learn <= max_facts_to_learn_before_query then (case length (filter_out is_in_access_G facts) of 0 => () | num_facts_to_learn => if num_facts_to_learn <= max_facts_to_learn_before_query then mash_learn_facts ctxt params prover 2 false timeout facts |> (fn "" => () | s => writeln (MaShN ^ ": " ^ s)) else maybe_launch_thread true num_facts_to_learn) else maybe_launch_thread false min_num_facts_to_learn end) else maybe_launch_thread false (length facts) val _ = if learn andalso mash_enabled andalso fact_filter <> SOME mepoN then please_learn () else () val effective_fact_filter = (case fact_filter of SOME ff => ff | NONE => if mash_enabled andalso mash_fast then meshN else mepoN) val unique_facts = drop_duplicate_facts facts val add_ths = Attrib.eval_thms ctxt add fun in_add (_, th) = member Thm.eq_thm_prop add_ths th fun add_and_take accepts = (case add_ths of [] => accepts | _ => (unique_facts |> filter in_add |> map fact_of_raw_fact) @ (accepts |> filter_out in_add)) |> take max_facts fun mepo () = (mepo_suggested_facts ctxt params max_facts NONE hyp_ts concl_t unique_facts |> weight_facts_steeply, []) fun mash () = mash_suggested_facts ctxt thy_name params (generous_max_suggestions max_facts) hyp_ts concl_t facts |>> weight_facts_steeply val mess = (* the order is important for the "case" expression below *) [] |> effective_fact_filter <> mepoN ? cons (mash_weight, mash) |> effective_fact_filter <> mashN ? cons (mepo_weight, mepo) |> Par_List.map (apsnd (fn f => f ())) val mesh = mesh_facts (fact_distinct (op aconv)) (eq_snd (gen_eq_thm ctxt)) max_facts mess |> add_and_take in (case (fact_filter, mess) of (NONE, [(_, (mepo, _)), (_, (mash, _))]) => [(meshN, mesh), (mepoN, mepo |> map fst |> add_and_take), (mashN, mash |> map fst |> add_and_take)] | _ => [(effective_fact_filter, mesh)]) end end; diff --git a/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML b/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML @@ -1,213 +1,216 @@ (* Title: HOL/Tools/Sledgehammer/sledgehammer_prover.ML Author: Fabian Immler, TU Muenchen Author: Makarius Author: Jasmin Blanchette, TU Muenchen Generic prover abstraction for Sledgehammer. *) signature SLEDGEHAMMER_PROVER = sig type atp_failure = ATP_Proof.atp_failure type stature = ATP_Problem_Generate.stature type type_enc = ATP_Problem_Generate.type_enc type fact = Sledgehammer_Fact.fact + type induction_rules = Sledgehammer_Fact.induction_rules type proof_method = Sledgehammer_Proof_Methods.proof_method type play_outcome = Sledgehammer_Proof_Methods.play_outcome datatype mode = Auto_Try | Try | Normal | Minimize | MaSh type params = {debug : bool, verbose : bool, overlord : bool, spy : bool, provers : string list, type_enc : string option, strict : bool, lam_trans : string option, uncurried_aliases : bool option, learn : bool, fact_filter : string option, + induction_rules : induction_rules option, max_facts : int option, fact_thresholds : real * real, max_mono_iters : int option, max_new_mono_instances : int option, isar_proofs : bool option, compress : real option, try0 : bool, smt_proofs : bool, slice : bool, minimize : bool, timeout : Time.time, preplay_timeout : Time.time, expect : string} type prover_problem = {comment : string, state : Proof.state, goal : thm, subgoal : int, subgoal_count : int, factss : (string * fact list) list, found_proof : unit -> unit} type prover_result = {outcome : atp_failure option, used_facts : (string * stature) list, used_from : fact list, preferred_methss : proof_method * proof_method list list, run_time : Time.time, message : (unit -> (string * stature) list * (proof_method * play_outcome)) -> string} type prover = params -> prover_problem -> prover_result val SledgehammerN : string val str_of_mode : mode -> string val overlord_file_location_of_prover : string -> string * string val proof_banner : mode -> string -> string val is_atp : theory -> string -> bool val bunches_of_proof_methods : Proof.context -> bool -> bool -> bool -> string -> proof_method list list val is_fact_chained : (('a * stature) * 'b) -> bool val filter_used_facts : bool -> (''a * stature) list -> ((''a * stature) * 'b) list -> ((''a * stature) * 'b) list val repair_monomorph_context : int option -> int -> int option -> int -> Proof.context -> Proof.context val supported_provers : Proof.context -> unit end; structure Sledgehammer_Prover : SLEDGEHAMMER_PROVER = struct open ATP_Proof open ATP_Util open ATP_Problem open ATP_Problem_Generate open ATP_Proof_Reconstruct open Metis_Tactic open Sledgehammer_Fact open Sledgehammer_Proof_Methods open Sledgehammer_ATP_Systems (* Identifier that distinguishes Sledgehammer from other tools that could use "Async_Manager". *) val SledgehammerN = "Sledgehammer" datatype mode = Auto_Try | Try | Normal | Minimize | MaSh fun str_of_mode Auto_Try = "Auto Try" | str_of_mode Try = "Try" | str_of_mode Normal = "Normal" | str_of_mode Minimize = "Minimize" | str_of_mode MaSh = "MaSh" val is_atp = member (op =) o supported_atps type params = {debug : bool, verbose : bool, overlord : bool, spy : bool, provers : string list, type_enc : string option, strict : bool, lam_trans : string option, uncurried_aliases : bool option, learn : bool, fact_filter : string option, + induction_rules : induction_rules option, max_facts : int option, fact_thresholds : real * real, max_mono_iters : int option, max_new_mono_instances : int option, isar_proofs : bool option, compress : real option, try0 : bool, smt_proofs : bool, slice : bool, minimize : bool, timeout : Time.time, preplay_timeout : Time.time, expect : string} type prover_problem = {comment : string, state : Proof.state, goal : thm, subgoal : int, subgoal_count : int, factss : (string * fact list) list, found_proof : unit -> unit} type prover_result = {outcome : atp_failure option, used_facts : (string * stature) list, used_from : fact list, preferred_methss : proof_method * proof_method list list, run_time : Time.time, message : (unit -> (string * stature) list * (proof_method * play_outcome)) -> string} type prover = params -> prover_problem -> prover_result fun overlord_file_location_of_prover prover = (getenv "ISABELLE_HOME_USER", "prob_" ^ prover) fun proof_banner mode name = (case mode of Auto_Try => "Auto Sledgehammer (" ^ quote name ^ ") found a proof" | Try => "Sledgehammer (" ^ quote name ^ ") found a proof" | _ => "Try this") fun bunches_of_proof_methods ctxt try0 smt_proofs needs_full_types desperate_lam_trans = let val try0_methodss = if try0 then [[Simp_Method, Auto_Method, Blast_Method, Linarith_Method, Meson_Method, Metis_Method (NONE, NONE), Fastforce_Method, Force_Method, Presburger_Method]] else [] val metis_methods = (if try0 then [] else [Metis_Method (NONE, NONE)]) @ Metis_Method (SOME full_typesN, NONE) :: Metis_Method (SOME really_full_type_enc, SOME desperate_lam_trans) :: (if needs_full_types then [Metis_Method (SOME really_full_type_enc, NONE), Metis_Method (SOME full_typesN, SOME desperate_lam_trans)] else [Metis_Method (SOME no_typesN, SOME desperate_lam_trans)]) val smt_methodss = if smt_proofs then [SMT_Method SMT_Z3 :: map (fn strategy => SMT_Method (SMT_Verit strategy)) (Verit_Proof.all_veriT_stgies (Context.Proof ctxt))] else [] in try0_methodss @ [metis_methods] @ smt_methodss end fun is_fact_chained ((_, (sc, _)), _) = sc = Chained fun filter_used_facts keep_chained used = filter ((member (eq_fst (op =)) used o fst) orf (if keep_chained then is_fact_chained else K false)) val max_fact_instances = 10 (* FUDGE *) fun repair_monomorph_context max_iters best_max_iters max_new_instances best_max_new_instances = Config.put Monomorph.max_rounds (max_iters |> the_default best_max_iters) #> Config.put Monomorph.max_new_instances (max_new_instances |> the_default best_max_new_instances) #> Config.put Monomorph.max_thm_instances max_fact_instances fun supported_provers ctxt = let val thy = Proof_Context.theory_of ctxt val (remote_provers, local_provers) = sort_strings (supported_atps thy) @ sort_strings (SMT_Config.available_solvers_of ctxt) |> List.partition (String.isPrefix remote_prefix) in writeln ("Supported provers: " ^ commas (local_provers @ remote_provers)) end end; diff --git a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML @@ -1,265 +1,265 @@ (* Title: HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML Author: Philipp Meyer, TU Muenchen Author: Jasmin Blanchette, TU Muenchen Minimization of fact list for Metis using external provers. *) signature SLEDGEHAMMER_PROVER_MINIMIZE = sig type stature = ATP_Problem_Generate.stature type proof_method = Sledgehammer_Proof_Methods.proof_method type play_outcome = Sledgehammer_Proof_Methods.play_outcome type mode = Sledgehammer_Prover.mode type params = Sledgehammer_Prover.params type prover = Sledgehammer_Prover.prover val is_prover_supported : Proof.context -> string -> bool val is_prover_installed : Proof.context -> string -> bool val default_max_facts_of_prover : Proof.context -> string -> int val get_prover : Proof.context -> mode -> string -> prover val binary_min_facts : int Config.T val minimize_facts : (thm list -> unit) -> string -> params -> bool -> int -> int -> Proof.state -> thm -> ((string * stature) * thm list) list -> ((string * stature) * thm list) list option * ((unit -> (string * stature) list * (proof_method * play_outcome)) -> string) val get_minimizing_prover : Proof.context -> mode -> (thm list -> unit) -> string -> prover end; structure Sledgehammer_Prover_Minimize : SLEDGEHAMMER_PROVER_MINIMIZE = struct open ATP_Util open ATP_Proof open ATP_Problem_Generate open ATP_Proof_Reconstruct open Sledgehammer_Util open Sledgehammer_Fact open Sledgehammer_Proof_Methods open Sledgehammer_Isar open Sledgehammer_ATP_Systems open Sledgehammer_Prover open Sledgehammer_Prover_ATP open Sledgehammer_Prover_SMT fun is_prover_supported ctxt = let val thy = Proof_Context.theory_of ctxt in is_atp thy orf is_smt_prover ctxt end fun is_prover_installed ctxt = is_smt_prover ctxt orf is_atp_installed (Proof_Context.theory_of ctxt) fun default_max_facts_of_prover ctxt name = let val thy = Proof_Context.theory_of ctxt in if is_atp thy name then fold (Integer.max o fst o #1 o fst o snd) (#best_slices (get_atp thy name ()) ctxt) 0 else if is_smt_prover ctxt name then SMT_Solver.default_max_relevant ctxt name else error ("No such prover: " ^ name) end fun get_prover ctxt mode name = let val thy = Proof_Context.theory_of ctxt in if is_atp thy name then run_atp mode name else if is_smt_prover ctxt name then run_smt_solver mode name else error ("No such prover: " ^ name) end (* wrapper for calling external prover *) fun n_facts names = let val n = length names in string_of_int n ^ " fact" ^ plural_s n ^ (if n > 0 then ": " ^ (names |> map fst |> sort string_ord |> space_implode " ") else "") end fun print silent f = if silent then () else writeln (f ()) fun test_facts ({debug, verbose, overlord, spy, provers, max_mono_iters, max_new_mono_instances, type_enc, strict, lam_trans, uncurried_aliases, isar_proofs, compress, try0, smt_proofs, - minimize, preplay_timeout, ...} : params) + minimize, preplay_timeout, induction_rules, ...} : params) silent (prover : prover) timeout i n state goal facts = let val _ = print silent (fn () => "Testing " ^ n_facts (map fst facts) ^ (if verbose then " (timeout: " ^ string_of_time timeout ^ ")" else "") ^ "...") val facts = facts |> maps (fn (n, ths) => map (pair n) ths) val params = {debug = debug, verbose = verbose, overlord = overlord, spy = spy, provers = provers, type_enc = type_enc, strict = strict, lam_trans = lam_trans, uncurried_aliases = uncurried_aliases, learn = false, fact_filter = NONE, - max_facts = SOME (length facts), fact_thresholds = (1.01, 1.01), - max_mono_iters = max_mono_iters, max_new_mono_instances = max_new_mono_instances, - isar_proofs = isar_proofs, compress = compress, try0 = try0, smt_proofs = smt_proofs, - slice = false, minimize = minimize, timeout = timeout, preplay_timeout = preplay_timeout, - expect = ""} + induction_rules = induction_rules, max_facts = SOME (length facts), + fact_thresholds = (1.01, 1.01), max_mono_iters = max_mono_iters, + max_new_mono_instances = max_new_mono_instances, isar_proofs = isar_proofs, + compress = compress, try0 = try0, smt_proofs = smt_proofs, slice = false, + minimize = minimize, timeout = timeout, preplay_timeout = preplay_timeout, expect = ""} val problem = {comment = "", state = state, goal = goal, subgoal = i, subgoal_count = n, factss = [("", facts)], found_proof = I} val result0 as {outcome = outcome0, used_facts, used_from, preferred_methss, run_time, message} = prover params problem val result as {outcome, ...} = if is_none outcome0 andalso forall (member (fn ((s, _), ((s', _), _)) => s = s') used_from) used_facts then result0 else {outcome = SOME MaybeUnprovable, used_facts = [], used_from = used_from, preferred_methss = preferred_methss, run_time = run_time, message = message} in print silent (fn () => (case outcome of SOME failure => string_of_atp_failure failure | NONE => "Found proof" ^ (if length used_facts = length facts then "" else " with " ^ n_facts used_facts) ^ " (" ^ string_of_time run_time ^ ")")); result end (* minimalization of facts *) (* Give the external prover some slack. The ATP gets further slack because the Sledgehammer preprocessing time is included in the estimate below but isn't part of the timeout. *) val slack_msecs = 200 fun new_timeout timeout run_time = Int.min (Time.toMilliseconds timeout, Time.toMilliseconds run_time + slack_msecs) |> Time.fromMilliseconds (* The linear algorithm usually outperforms the binary algorithm when over 60% of the facts are actually needed. The binary algorithm is much more appropriate for provers that cannot return the list of used facts and hence returns all facts as used. Since we cannot know in advance how many facts are actually needed, we heuristically set the threshold to 10 facts. *) val binary_min_facts = Attrib.setup_config_int \<^binding>\sledgehammer_minimize_binary_min_facts\ (K 20) fun linear_minimize test timeout result xs = let fun min _ [] p = p | min timeout (x :: xs) (seen, result) = (case test timeout (xs @ seen) of result as {outcome = NONE, used_facts, run_time, ...} : prover_result => min (new_timeout timeout run_time) (filter_used_facts true used_facts xs) (filter_used_facts false used_facts seen, result) | _ => min timeout xs (x :: seen, result)) in min timeout xs ([], result) end fun binary_minimize test timeout result xs = let fun min depth (result as {run_time, ...} : prover_result) sup (xs as _ :: _ :: _) = let val (l0, r0) = chop (length xs div 2) xs (* val _ = warning (replicate_string depth " " ^ "{ " ^ "sup: " ^ n_facts (map fst sup)) val _ = warning (replicate_string depth " " ^ " " ^ "xs: " ^ n_facts (map fst xs)) val _ = warning (replicate_string depth " " ^ " " ^ "l0: " ^ n_facts (map fst l0)) val _ = warning (replicate_string depth " " ^ " " ^ "r0: " ^ n_facts (map fst r0)) *) val depth = depth + 1 val timeout = new_timeout timeout run_time in (case test timeout (sup @ l0) of result as {outcome = NONE, used_facts, ...} => min depth result (filter_used_facts true used_facts sup) (filter_used_facts true used_facts l0) | _ => (case test timeout (sup @ r0) of result as {outcome = NONE, used_facts, ...} => min depth result (filter_used_facts true used_facts sup) (filter_used_facts true used_facts r0) | _ => let val (sup_r0, (l, result)) = min depth result (sup @ r0) l0 val (sup, r0) = (sup, r0) |> apply2 (filter_used_facts true (map fst sup_r0)) val (sup_l, (r, result)) = min depth result (sup @ l) r0 val sup = sup |> filter_used_facts true (map fst sup_l) in (sup, (l @ r, result)) end)) end (* |> tap (fn _ => warning (replicate_string depth " " ^ "}")) *) | min _ result sup xs = (sup, (xs, result)) in (case snd (min 0 result [] xs) of ([x], result as {run_time, ...}) => (case test (new_timeout timeout run_time) [] of result as {outcome = NONE, ...} => ([], result) | _ => ([x], result)) | p => p) end fun minimize_facts do_learn prover_name (params as {learn, timeout, ...}) silent i n state goal facts = let val ctxt = Proof.context_of state val prover = get_prover ctxt Minimize prover_name val (chained, non_chained) = List.partition is_fact_chained facts fun test timeout non_chained = test_facts params silent prover timeout i n state goal (chained @ non_chained) in (print silent (fn () => "Sledgehammer minimizer: " ^ quote prover_name); (case test timeout non_chained of result as {outcome = NONE, used_facts, run_time, ...} => let val non_chained = filter_used_facts true used_facts non_chained val min = if length non_chained >= Config.get ctxt binary_min_facts then binary_minimize else linear_minimize val (min_facts, {message, ...}) = min test (new_timeout timeout run_time) result non_chained val min_facts_and_chained = chained @ min_facts in print silent (fn () => cat_lines ["Minimized to " ^ n_facts (map fst min_facts)] ^ (case length chained of 0 => "" | n => " (plus " ^ string_of_int n ^ " chained)")); (if learn then do_learn (maps snd min_facts_and_chained) else ()); (SOME min_facts_and_chained, message) end | {outcome = SOME TimedOut, ...} => (NONE, fn _ => "Timeout: You can increase the time limit using the \"timeout\" option (e.g., \ \timeout = " ^ string_of_int (10 + Time.toMilliseconds timeout div 1000) ^ "\")") | {message, ...} => (NONE, (prefix "Prover error: " o message)))) handle ERROR msg => (NONE, fn _ => "Error: " ^ msg) end fun maybe_minimize mode do_learn name (params as {verbose, minimize, ...}) ({state, goal, subgoal, subgoal_count, ...} : prover_problem) (result as {outcome, used_facts, used_from, preferred_methss, run_time, message} : prover_result) = if is_some outcome then result else let val (used_facts, message) = if minimize then minimize_facts do_learn name params (not verbose orelse (mode <> Normal andalso mode <> MaSh)) subgoal subgoal_count state goal (filter_used_facts true used_facts (map (apsnd single) used_from)) |>> Option.map (map fst) else (SOME used_facts, message) in (case used_facts of SOME used_facts => {outcome = NONE, used_facts = sort_by fst used_facts, used_from = used_from, preferred_methss = preferred_methss, run_time = run_time, message = message} | NONE => result) end fun get_minimizing_prover ctxt mode do_learn name params problem = get_prover ctxt mode name params problem |> maybe_minimize mode do_learn name params problem end; diff --git a/src/HOL/Tools/Sledgehammer/sledgehammer_tactics.ML b/src/HOL/Tools/Sledgehammer/sledgehammer_tactics.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_tactics.ML +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_tactics.ML @@ -1,76 +1,77 @@ (* Title: HOL/Tools/Sledgehammer/sledgehammer_tactics.ML Author: Jasmin Blanchette, TU Muenchen Copyright 2010, 2011 Sledgehammer as a tactic. *) signature SLEDGEHAMMER_TACTICS = sig type fact_override = Sledgehammer_Fact.fact_override val sledgehammer_with_metis_tac : Proof.context -> (string * string) list -> fact_override -> thm list -> int -> tactic val sledgehammer_as_oracle_tac : Proof.context -> (string * string) list -> fact_override -> thm list -> int -> tactic end; structure Sledgehammer_Tactics : SLEDGEHAMMER_TACTICS = struct open Sledgehammer_Util open Sledgehammer_Fact open Sledgehammer_Prover open Sledgehammer_Prover_ATP open Sledgehammer_Prover_Minimize open Sledgehammer_MaSh open Sledgehammer_Commands fun run_prover override_params fact_override chained i n ctxt goal = let val thy = Proof_Context.theory_of ctxt val mode = Normal - val params as {provers, max_facts, ...} = default_params thy override_params + val params as {provers, induction_rules, max_facts, ...} = default_params thy override_params val name = hd provers val prover = get_prover ctxt mode name val default_max_facts = default_max_facts_of_prover ctxt name val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal goal i ctxt val ho_atp = exists (is_ho_atp ctxt) provers val keywords = Thy_Header.get_keywords' ctxt val css_table = clasimpset_rule_table_of ctxt + val induction_rules = the_default (if ho_atp then Instantiate else Exclude) induction_rules val facts = - nearly_all_facts ctxt ho_atp fact_override keywords css_table chained hyp_ts concl_t + nearly_all_facts ctxt induction_rules fact_override keywords css_table chained hyp_ts concl_t |> relevant_facts ctxt params name (the_default default_max_facts max_facts) fact_override hyp_ts concl_t |> hd |> snd val problem = {comment = "", state = Proof.init ctxt, goal = goal, subgoal = i, subgoal_count = n, factss = [("", facts)], found_proof = I} in (case prover params problem of {outcome = NONE, used_facts, ...} => used_facts |> map fst |> SOME | _ => NONE) handle ERROR message => (warning ("Error: " ^ message ^ "\n"); NONE) end fun sledgehammer_with_metis_tac ctxt override_params fact_override chained i th = let val override_params = override_params @ [("preplay_timeout", "0")] in (case run_prover override_params fact_override chained i i ctxt th of SOME facts => Metis_Tactic.metis_tac [] ATP_Problem_Generate.combs_or_liftingN ctxt (maps (thms_of_name ctxt) facts) i th | NONE => Seq.empty) end fun sledgehammer_as_oracle_tac ctxt override_params fact_override chained i th = let val override_params = override_params @ [("preplay_timeout", "0"), ("minimize", "false")] val xs = run_prover override_params fact_override chained i i ctxt th in if is_some xs then ALLGOALS (Skip_Proof.cheat_tac ctxt) th else Seq.empty end end;