--- 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
--- 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 =
--- 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
--- 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 =
--- 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 =
--- 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
--- 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}