# HG changeset patch # User blanchet # Date 1287749432 -7200 # Node ID 6f7bf79b1506e56558885bbe11b4ed94aa5a8492 # Parent ed2869dd9bfadcad8ae7f2054590c56c2a59b429 fixed signature of "is_smt_solver_installed"; renaming diff -r ed2869dd9bfa -r 6f7bf79b1506 src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Fri Oct 22 13:57:54 2010 +0200 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Fri Oct 22 14:10:32 2010 +0200 @@ -314,10 +314,11 @@ fun change_data id f = (Unsynchronized.change data (AList.map_entry (op =) id f); ()) -fun get_prover thy args = +fun get_prover ctxt args = let + val thy = ProofContext.theory_of ctxt fun default_prover_name () = - hd (#provers (Sledgehammer_Isar.default_params thy [])) + hd (#provers (Sledgehammer_Isar.default_params ctxt [])) handle Empty => error "No ATP available." fun get_prover name = (name, Sledgehammer.get_prover thy false name) in @@ -347,7 +348,7 @@ (change_dir dir #> Config.put Sledgehammer.measure_run_time true) val params as {full_types, relevance_thresholds, max_relevant, ...} = - Sledgehammer_Isar.default_params thy + Sledgehammer_Isar.default_params ctxt [("timeout", Int.toString timeout ^ " s")] val relevance_override = {add = [], del = [], only = false} val default_max_relevant = @@ -397,7 +398,7 @@ val triv_str = if trivial then "[T] " else "" val _ = change_data id inc_sh_calls val _ = if trivial then () else change_data id inc_sh_nontriv_calls - val (prover_name, prover) = get_prover (Proof.theory_of st) args + val (prover_name, prover) = get_prover (Proof.context_of st) args val dir = AList.lookup (op =) args keepK val timeout = Mirabelle.get_int_setting args (prover_timeoutK, 30) val hard_timeout = AList.lookup (op =) args prover_hard_timeoutK @@ -434,14 +435,14 @@ fun run_minimize args named_thms id ({pre=st, log, ...}: Mirabelle.run_args) = let open Metis_Translate - val thy = Proof.theory_of st + val ctxt = Proof.context_of st val n0 = length (these (!named_thms)) - val (prover_name, _) = get_prover thy args + val (prover_name, _) = get_prover ctxt args val timeout = AList.lookup (op =) args minimize_timeoutK |> Option.map (fst o read_int o explode) |> the_default 5 - val params = Sledgehammer_Isar.default_params thy + val params = Sledgehammer_Isar.default_params ctxt [("provers", prover_name), ("timeout", Int.toString timeout ^ " s")] val minimize = Sledgehammer_Minimize.minimize_facts params 1 diff -r ed2869dd9bfa -r 6f7bf79b1506 src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML Fri Oct 22 13:57:54 2010 +0200 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML Fri Oct 22 14:10:32 2010 +0200 @@ -95,7 +95,6 @@ SOME proofs => let val {context = ctxt, facts, goal} = Proof.goal pre - val thy = ProofContext.theory_of ctxt val args = args |> filter (fn (key, value) => @@ -104,7 +103,7 @@ | NONE => true) val {relevance_thresholds, full_types, max_relevant, ...} = - Sledgehammer_Isar.default_params thy args + Sledgehammer_Isar.default_params ctxt args val subgoal = 1 val (_, hyp_ts, concl_t) = Sledgehammer_Util.strip_subgoal goal subgoal val facts = diff -r ed2869dd9bfa -r 6f7bf79b1506 src/HOL/Tools/Sledgehammer/sledgehammer.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML Fri Oct 22 13:57:54 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML Fri Oct 22 14:10:32 2010 +0200 @@ -11,7 +11,7 @@ type failure = ATP_Systems.failure type locality = Sledgehammer_Filter.locality type relevance_override = Sledgehammer_Filter.relevance_override - type fol_formula = Sledgehammer_ATP_Translate.fol_formula + type prepared_formula = Sledgehammer_ATP_Translate.prepared_formula type minimize_command = Sledgehammer_ATP_Reconstruct.minimize_command type params = @@ -31,7 +31,7 @@ datatype axiom = Unprepared of (string * locality) * thm | - Prepared of term * ((string * locality) * fol_formula) option + Prepared of term * ((string * locality) * prepared_formula) option type prover_problem = {state: Proof.state, @@ -127,7 +127,7 @@ datatype axiom = Unprepared of (string * locality) * thm | - Prepared of term * ((string * locality) * fol_formula) option + Prepared of term * ((string * locality) * prepared_formula) option type prover_problem = {state: Proof.state, @@ -424,8 +424,7 @@ end fun run_sledgehammer (params as {blocking, provers, full_types, - relevance_thresholds, max_relevant, timeout, - ...}) + relevance_thresholds, max_relevant, ...}) auto i (relevance_override as {only, ...}) minimize_command state = if null provers then diff -r ed2869dd9bfa -r 6f7bf79b1506 src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML Fri Oct 22 13:57:54 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML Fri Oct 22 14:10:32 2010 +0200 @@ -434,7 +434,8 @@ | AImplies => s_imp | AIf => s_imp o swap | AIff => s_iff - | ANotIff => s_not o s_iff) + | ANotIff => s_not o s_iff + | _ => raise Fail "unexpected connective") | AAtom tm => term_from_pred thy full_types tfrees pos tm | _ => raise FORMULA [phi] in repair_tvar_sorts (do_formula true phi Vartab.empty) end @@ -505,6 +506,7 @@ (_, []) => lines (* no repetition of proof line *) | (pre, Inference (name', _, _) :: post) => pre @ map (replace_dependencies_in_line (name', [name])) post + | _ => raise Fail "unexpected inference" else if is_conjecture conjecture_shape name then Inference (name, negate_term t, []) :: lines else @@ -521,6 +523,7 @@ | (pre, Inference (name', t', _) :: post) => Inference (name, t', deps) :: pre @ map (replace_dependencies_in_line (name', [name])) post + | _ => raise Fail "unexpected inference" (* Recursively delete empty lines (type information) from the proof. *) fun add_nontrivial_line (Inference (name, t, [])) lines = diff -r ed2869dd9bfa -r 6f7bf79b1506 src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML Fri Oct 22 13:57:54 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML Fri Oct 22 14:10:32 2010 +0200 @@ -9,16 +9,16 @@ signature SLEDGEHAMMER_ATP_TRANSLATE = sig type 'a problem = 'a ATP_Problem.problem - type fol_formula + type prepared_formula val axiom_prefix : string val conjecture_prefix : string val prepare_axiom : Proof.context -> (string * 'a) * thm - -> term * ((string * 'a) * fol_formula) option + -> term * ((string * 'a) * prepared_formula) option val prepare_atp_problem : Proof.context -> bool -> bool -> bool -> bool -> term list -> term - -> (term * ((string * 'a) * fol_formula) option) list + -> (term * ((string * 'a) * prepared_formula) option) list -> string problem * string Symtab.table * int * (string * 'a) list vector end; @@ -39,7 +39,7 @@ (* Freshness almost guaranteed! *) val sledgehammer_weak_prefix = "Sledgehammer:" -type fol_formula = +type prepared_formula = {name: string, kind: kind, combformula: (name, combterm) formula, @@ -214,7 +214,7 @@ fun count_combformula (AQuant (_, _, phi)) = count_combformula phi | count_combformula (AConn (_, phis)) = fold count_combformula phis | count_combformula (AAtom tm) = count_combterm tm -fun count_fol_formula ({combformula, ...} : fol_formula) = +fun count_prepared_formula ({combformula, ...} : prepared_formula) = count_combformula combformula val optional_helpers = @@ -234,7 +234,8 @@ fun get_helper_facts ctxt is_FO full_types conjectures axioms = let - val ct = fold (fold count_fol_formula) [conjectures, axioms] init_counters + val ct = + fold (fold count_prepared_formula) [conjectures, axioms] init_counters fun is_needed c = the (Symtab.lookup ct c) > 0 fun baptize th = ((Thm.get_name_hint th, false), th) in @@ -322,7 +323,7 @@ in aux end fun formula_for_axiom full_types - ({combformula, ctypes_sorts, ...} : fol_formula) = + ({combformula, ctypes_sorts, ...} : prepared_formula) = mk_ahorn (map (formula_for_fo_literal o fo_literal_for_type_literal) (type_literals_for_types ctypes_sorts)) (formula_for_combformula full_types combformula) @@ -352,11 +353,11 @@ (fo_literal_for_arity_literal conclLit))) fun problem_line_for_conjecture full_types - ({name, kind, combformula, ...} : fol_formula) = + ({name, kind, combformula, ...} : prepared_formula) = Fof (conjecture_prefix ^ name, kind, formula_for_combformula full_types combformula) -fun free_type_literals_for_conjecture ({ctypes_sorts, ...} : fol_formula) = +fun free_type_literals_for_conjecture ({ctypes_sorts, ...} : prepared_formula) = map fo_literal_for_type_literal (type_literals_for_types ctypes_sorts) fun problem_line_for_free_type j lit = diff -r ed2869dd9bfa -r 6f7bf79b1506 src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Fri Oct 22 13:57:54 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Fri Oct 22 14:10:32 2010 +0200 @@ -12,7 +12,7 @@ val provers : string Unsynchronized.ref val timeout : int Unsynchronized.ref val full_types : bool Unsynchronized.ref - val default_params : theory -> (string * string) list -> params + val default_params : Proof.context -> (string * string) list -> params val setup : theory -> theory end; @@ -131,36 +131,40 @@ fun merge p : T = AList.merge (op =) (K true) p) (* FIXME: dummy *) -fun is_smt_solver_installed () = true +fun is_smt_solver_installed ctxt = true fun maybe_remote_atp thy name = name |> not (is_atp_installed thy name) ? prefix remote_prefix -fun maybe_remote_smt_solver thy = - smtN |> not (is_smt_solver_installed ()) ? prefix remote_prefix +fun maybe_remote_smt_solver ctxt = + smtN |> not (is_smt_solver_installed ctxt) ? prefix remote_prefix (* The first ATP of the list is used by Auto Sledgehammer. Because of the low timeout, it makes sense to put SPASS first. *) -fun default_provers_param_value thy = - (filter (is_atp_installed thy) [spassN] @ - [maybe_remote_atp thy eN, - if forall (is_atp_installed thy) [spassN, eN] then remote_prefix ^ vampireN - else maybe_remote_atp thy vampireN, - remote_prefix ^ sine_eN (* FIXME: Introduce and document: , - maybe_remote_smt_solver thy *)]) - |> space_implode " " +fun default_provers_param_value ctxt = + let val thy = ProofContext.theory_of ctxt in + (filter (is_atp_installed thy) [spassN] @ + [maybe_remote_atp thy eN, + if forall (is_atp_installed thy) [spassN, eN] then remote_prefix ^ vampireN + else maybe_remote_atp thy vampireN, + remote_prefix ^ sine_eN (* FIXME: Introduce and document: , + maybe_remote_smt_solver ctxt *)]) + |> space_implode " " + end val set_default_raw_param = Data.map o AList.update (op =) o unalias_raw_param -fun default_raw_params thy = - Data.get thy - |> fold (AList.default (op =)) - [("provers", [case !provers of - "" => default_provers_param_value thy - | s => s]), - ("full_types", [if !full_types then "true" else "false"]), - ("timeout", let val timeout = !timeout in - [if timeout <= 0 then "none" - else string_of_int timeout ^ " s"] - end)] +fun default_raw_params ctxt = + let val thy = ProofContext.theory_of ctxt in + Data.get thy + |> fold (AList.default (op =)) + [("provers", [case !provers of + "" => default_provers_param_value ctxt + | s => s]), + ("full_types", [if !full_types then "true" else "false"]), + ("timeout", let val timeout = !timeout in + [if timeout <= 0 then "none" + else string_of_int timeout ^ " s"] + end)] + end val infinity_time_in_secs = 60 * 60 * 24 * 365 val the_timeout = the_default (Time.fromSeconds infinity_time_in_secs) @@ -224,7 +228,7 @@ timeout = timeout, expect = expect} end -fun get_params auto thy = extract_params auto (default_raw_params thy) +fun get_params auto ctxt = extract_params auto (default_raw_params ctxt) fun default_params thy = get_params false thy o map (apsnd single) (* Sledgehammer the given subgoal *) @@ -254,18 +258,19 @@ fun hammer_away override_params subcommand opt_i relevance_override state = let + val ctxt = Proof.context_of state val thy = Proof.theory_of state val _ = app check_raw_param override_params in if subcommand = runN then let val i = the_default 1 opt_i in - run_sledgehammer (get_params false thy override_params) false i + run_sledgehammer (get_params false ctxt override_params) false i relevance_override (minimize_command override_params i) state |> K () end else if subcommand = minimizeN then - run_minimize (get_params false thy override_params) (the_default 1 opt_i) + run_minimize (get_params false ctxt override_params) (the_default 1 opt_i) (#add relevance_override) state else if subcommand = messagesN then messages opt_i @@ -291,13 +296,15 @@ Toplevel.theory (fold set_default_raw_param params #> tap (fn thy => - writeln ("Default parameters for Sledgehammer:\n" ^ - (case rev (default_raw_params thy) of - [] => "none" - | params => - (map check_raw_param params; - params |> map string_for_raw_param - |> sort_strings |> cat_lines))))) + let val ctxt = ProofContext.init_global thy in + writeln ("Default parameters for Sledgehammer:\n" ^ + (case default_raw_params ctxt |> rev of + [] => "none" + | params => + (map check_raw_param params; + params |> map string_for_raw_param + |> sort_strings |> cat_lines))) + end)) val parse_key = Scan.repeat1 Parse.typ_group >> space_implode " " val parse_value = Scan.repeat1 Parse.xname @@ -332,8 +339,8 @@ if not (!auto) then (false, state) else - let val thy = Proof.theory_of state in - run_sledgehammer (get_params true thy []) true 1 no_relevance_override + let val ctxt = Proof.context_of state in + run_sledgehammer (get_params true ctxt []) true 1 no_relevance_override (minimize_command [] 1) state end diff -r ed2869dd9bfa -r 6f7bf79b1506 src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Fri Oct 22 13:57:54 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Fri Oct 22 14:10:32 2010 +0200 @@ -56,7 +56,7 @@ isar_shrink_factor = isar_shrink_factor, timeout = timeout, expect = ""} val axioms = axioms |> maps (fn (n, ths) => ths |> map (Unprepared o pair n)) - val {context = ctxt, goal, ...} = Proof.goal state + val {goal, ...} = Proof.goal state val problem = {state = state, goal = goal, subgoal = i, subgoal_count = n, axioms = axioms, only = true}