--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Mon Feb 03 14:35:19 2014 +0100
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Mon Feb 03 15:19:07 2014 +0100
@@ -19,7 +19,7 @@
(*refers to minimization attempted by Mirabelle*)
val minimize_timeoutK = "minimize_timeout" (*=TIME: timeout for each minimization step (seconds of*)
-val reconstructorK = "reconstructor" (*=NAME: how to reconstruct proofs (ie. using metis/smt)*)
+val proof_methodK = "proof_method" (*=NAME: how to reconstruct proofs (ie. using metis/smt)*)
val metis_ftK = "metis_ft" (*: apply metis with fully-typed encoding to the theorems found by sledgehammer*)
val max_factsK = "max_facts" (*=NUM: max. relevant clauses to use*)
@@ -43,8 +43,7 @@
fun sh_tag id = "#" ^ string_of_int id ^ " sledgehammer: "
fun minimize_tag id = "#" ^ string_of_int id ^ " minimize (sledgehammer): "
-fun reconstructor_tag reconstructor id =
- "#" ^ string_of_int id ^ " " ^ (!reconstructor) ^ " (sledgehammer): "
+fun proof_method_tag meth id = "#" ^ string_of_int id ^ " " ^ (!meth) ^ " (sledgehammer): "
val separator = "-----"
@@ -130,16 +129,16 @@
proofs, time, timeout, lemmas, posns}) = (calls, success, nontriv_calls,
nontriv_success, proofs, time, timeout, lemmas, posns)
-datatype reconstructor_mode =
+datatype proof_method_mode =
Unminimized | Minimized | UnminimizedFT | MinimizedFT
datatype data = Data of {
sh: sh_data,
min: min_data,
- re_u: re_data, (* reconstructor with unminimized set of lemmas *)
- re_m: re_data, (* reconstructor with minimized set of lemmas *)
- re_uft: re_data, (* reconstructor with unminimized set of lemmas and fully-typed *)
- re_mft: re_data, (* reconstructor with minimized set of lemmas and fully-typed *)
+ re_u: re_data, (* proof method with unminimized set of lemmas *)
+ re_m: re_data, (* proof method with minimized set of lemmas *)
+ re_uft: re_data, (* proof method with unminimized set of lemmas and fully-typed *)
+ re_mft: re_data, (* proof method with minimized set of lemmas and fully-typed *)
mini: bool (* with minimization *)
}
@@ -218,39 +217,39 @@
fun inc_min_ab_ratios r = map_min_data
(fn (succs, ab_ratios) => (succs, ab_ratios+r))
-val inc_reconstructor_calls = map_re_data
+val inc_proof_method_calls = map_re_data
(fn (calls,success,nontriv_calls, nontriv_success, proofs,time,timeout,lemmas,posns)
=> (calls + 1, success, nontriv_calls, nontriv_success, proofs, time, timeout, lemmas,posns))
-val inc_reconstructor_success = map_re_data
+val inc_proof_method_success = map_re_data
(fn (calls,success,nontriv_calls, nontriv_success, proofs,time,timeout,lemmas,posns)
=> (calls, success + 1, nontriv_calls, nontriv_success, proofs, time, timeout, lemmas,posns))
-val inc_reconstructor_nontriv_calls = map_re_data
+val inc_proof_method_nontriv_calls = map_re_data
(fn (calls,success,nontriv_calls, nontriv_success, proofs,time,timeout,lemmas,posns)
=> (calls, success, nontriv_calls + 1, nontriv_success, proofs, time, timeout, lemmas,posns))
-val inc_reconstructor_nontriv_success = map_re_data
+val inc_proof_method_nontriv_success = map_re_data
(fn (calls,success,nontriv_calls, nontriv_success, proofs,time,timeout,lemmas,posns)
=> (calls, success, nontriv_calls, nontriv_success + 1, proofs, time, timeout, lemmas,posns))
-val inc_reconstructor_proofs = map_re_data
+val inc_proof_method_proofs = map_re_data
(fn (calls,success,nontriv_calls, nontriv_success, proofs,time,timeout,lemmas,posns)
=> (calls, success, nontriv_calls, nontriv_success, proofs + 1, time, timeout, lemmas,posns))
-fun inc_reconstructor_time m t = map_re_data
+fun inc_proof_method_time m t = map_re_data
(fn (calls,success,nontriv_calls, nontriv_success, proofs,time,timeout,lemmas,posns)
=> (calls, success, nontriv_calls, nontriv_success, proofs, time + t, timeout, lemmas,posns)) m
-val inc_reconstructor_timeout = map_re_data
+val inc_proof_method_timeout = map_re_data
(fn (calls,success,nontriv_calls, nontriv_success, proofs,time,timeout,lemmas,posns)
=> (calls, success, nontriv_calls, nontriv_success, proofs, time, timeout + 1, lemmas,posns))
-fun inc_reconstructor_lemmas m n = map_re_data
+fun inc_proof_method_lemmas m n = map_re_data
(fn (calls,success,nontriv_calls, nontriv_success, proofs,time,timeout,lemmas,posns)
=> (calls, success, nontriv_calls, nontriv_success, proofs, time, timeout, inc_max n lemmas, posns)) m
-fun inc_reconstructor_posns m pos = map_re_data
+fun inc_proof_method_posns m pos = map_re_data
(fn (calls,success,nontriv_calls, nontriv_success, proofs,time,timeout,lemmas,posns)
=> (calls, success, nontriv_calls, nontriv_success, proofs, time, timeout, lemmas, pos::posns)) m
@@ -292,19 +291,19 @@
fun log_re_data log tag sh_calls (re_calls, re_success, re_nontriv_calls,
re_nontriv_success, re_proofs, re_time, re_timeout,
(lemmas, lems_sos, lems_max), re_posns) =
- (log ("Total number of " ^ tag ^ "reconstructor calls: " ^ str re_calls);
- log ("Number of successful " ^ tag ^ "reconstructor calls: " ^ str re_success ^
+ (log ("Total number of " ^ tag ^ "proof method calls: " ^ str re_calls);
+ log ("Number of successful " ^ tag ^ "proof method calls: " ^ str re_success ^
" (proof: " ^ str re_proofs ^ ")");
- log ("Number of " ^ tag ^ "reconstructor timeouts: " ^ str re_timeout);
+ log ("Number of " ^ tag ^ "proof method timeouts: " ^ str re_timeout);
log ("Success rate: " ^ percentage re_success sh_calls ^ "%");
- log ("Total number of nontrivial " ^ tag ^ "reconstructor calls: " ^ str re_nontriv_calls);
- log ("Number of successful nontrivial " ^ tag ^ "reconstructor calls: " ^ str re_nontriv_success ^
+ log ("Total number of nontrivial " ^ tag ^ "proof method calls: " ^ str re_nontriv_calls);
+ log ("Number of successful nontrivial " ^ tag ^ "proof method calls: " ^ str re_nontriv_success ^
" (proof: " ^ str re_proofs ^ ")");
- log ("Number of successful " ^ tag ^ "reconstructor lemmas: " ^ str lemmas);
- log ("SOS of successful " ^ tag ^ "reconstructor lemmas: " ^ str lems_sos);
- log ("Max number of successful " ^ tag ^ "reconstructor lemmas: " ^ str lems_max);
- log ("Total time for successful " ^ tag ^ "reconstructor calls: " ^ str3 (time re_time));
- log ("Average time for successful " ^ tag ^ "reconstructor calls: " ^
+ log ("Number of successful " ^ tag ^ "proof method lemmas: " ^ str lemmas);
+ log ("SOS of successful " ^ tag ^ "proof method lemmas: " ^ str lems_sos);
+ log ("Max number of successful " ^ tag ^ "proof method lemmas: " ^ str lems_max);
+ log ("Total time for successful " ^ tag ^ "proof method calls: " ^ str3 (time re_time));
+ log ("Average time for successful " ^ tag ^ "proof method calls: " ^
str3 (avg_time re_time re_success));
if tag=""
then log ("Proved: " ^ space_implode " " (map str_of_pos re_posns))
@@ -325,7 +324,7 @@
fun app_if (ReData {calls, ...}) f = if calls > 0 then f () else ()
fun log_re tag m =
log_re_data log tag sh_calls (tuple_of_re_data m)
- fun log_reconstructor (tag1, m1) (tag2, m2) = app_if m1 (fn () =>
+ fun log_proof_method (tag1, m1) (tag2, m2) = app_if m1 (fn () =>
(log_re tag1 m1; log ""; app_if m2 (fn () => log_re tag2 m2)))
in
if sh_calls > 0
@@ -334,14 +333,14 @@
log_sh_data log (tuple_of_sh_data sh);
log "";
if not mini
- then log_reconstructor ("", re_u) ("fully-typed ", re_uft)
+ then log_proof_method ("", re_u) ("fully-typed ", re_uft)
else
app_if re_u (fn () =>
- (log_reconstructor ("unminimized ", re_u) ("unminimized fully-typed ", re_uft);
+ (log_proof_method ("unminimized ", re_u) ("unminimized fully-typed ", re_uft);
log "";
app_if re_m (fn () =>
(log_min_data log (tuple_of_min_data min); log "";
- log_reconstructor ("", re_m) ("fully-typed ", re_mft))))))
+ log_proof_method ("", re_m) ("fully-typed ", re_mft))))))
else ()
end
@@ -385,8 +384,8 @@
andalso not (String.isSubstring "may fail" s)
(* Fragile hack *)
-fun reconstructor_from_msg args msg =
- (case AList.lookup (op =) args reconstructorK of
+fun proof_method_from_msg args msg =
+ (case AList.lookup (op =) args proof_methodK of
SOME name => name
| NONE =>
if exists good_line (split_lines msg) then
@@ -460,7 +459,7 @@
fun failed failure =
({outcome = SOME failure, used_facts = [], used_from = [],
run_time = Time.zeroTime,
- preplay = Lazy.value (Sledgehammer_Prover.plain_metis,
+ preplay = Lazy.value (Sledgehammer_Reconstructor.Metis_Method (NONE, NONE),
Sledgehammer_Reconstructor.Play_Failed),
message = K "", message_tail = ""}, ~1)
val ({outcome, used_facts, run_time, preplay, message, message_tail, ...}
@@ -501,7 +500,7 @@
in
-fun run_sledgehammer trivial args reconstructor named_thms id
+fun run_sledgehammer trivial args proof_method named_thms id
({pre=st, log, pos, ...}: Mirabelle.run_args) =
let
val thy = Proof.theory_of st
@@ -557,7 +556,7 @@
change_data id (inc_sh_max_lems (length names));
change_data id (inc_sh_time_isa time_isa);
change_data id (inc_sh_time_prover time_prover);
- reconstructor := reconstructor_from_msg args msg;
+ proof_method := proof_method_from_msg args msg;
named_thms := SOME (map_filter get_thms names);
log (sh_tag id ^ triv_str ^ "succeeded (" ^ string_of_int time_isa ^ "+" ^
string_of_int time_prover ^ ") [" ^ prover_name ^ "]:\n" ^ msg)
@@ -572,7 +571,7 @@
end
-fun run_minimize args reconstructor named_thms id ({pre = st, log, ...} : Mirabelle.run_args) =
+fun run_minimize args meth named_thms id ({pre = st, log, ...} : Mirabelle.run_args) =
let
val thy = Proof.theory_of st
val {goal, ...} = Proof.goal st
@@ -614,7 +613,7 @@
change_data id (inc_min_ab_ratios ((100 * length named_thms') div n0));
if length named_thms' = n0
then log (minimize_tag id ^ "already minimal")
- else (reconstructor := reconstructor_from_msg args msg;
+ else (meth := proof_method_from_msg args msg;
named_thms := SOME named_thms';
log (minimize_tag id ^ "succeeded:\n" ^ msg))
)
@@ -629,10 +628,10 @@
("slice", "false"),
("timeout", timeout |> Time.toSeconds |> string_of_int)]
-fun run_reconstructor trivial full m name reconstructor named_thms id
+fun run_proof_method trivial full m name meth named_thms id
({pre=st, timeout, log, pos, ...}: Mirabelle.run_args) =
let
- fun do_reconstructor named_thms ctxt =
+ fun do_method named_thms ctxt =
let
val ref_of_str =
suffix ";" #> Outer_Syntax.scan Position.none #> Parse_Spec.xthm
@@ -646,56 +645,56 @@
Sledgehammer_Tactics.sledgehammer_as_oracle_tac ctxt
(override_params prover type_enc (my_timeout time_slice)) fact_override
in
- if !reconstructor = "sledgehammer_tac" then
+ if !meth = "sledgehammer_tac" then
sledge_tac 0.2 ATP_Systems.vampireN "mono_native"
ORELSE' sledge_tac 0.2 ATP_Systems.eN "poly_guards??"
ORELSE' sledge_tac 0.2 ATP_Systems.spassN "mono_native"
ORELSE' sledge_tac 0.2 ATP_Systems.z3_tptpN "poly_tags??"
ORELSE' SMT_Solver.smt_tac ctxt thms
- else if !reconstructor = "smt" then
+ else if !meth = "smt" then
SMT_Solver.smt_tac ctxt thms
else if full then
Metis_Tactic.metis_tac [ATP_Proof_Reconstruct.full_typesN]
ATP_Proof_Reconstruct.default_metis_lam_trans ctxt thms
- else if String.isPrefix "metis (" (!reconstructor) then
+ else if String.isPrefix "metis (" (!meth) then
let
val (type_encs, lam_trans) =
- !reconstructor
+ !meth
|> Outer_Syntax.scan Position.start
|> filter Token.is_proper |> tl
|> Metis_Tactic.parse_metis_options |> fst
|>> the_default [ATP_Proof_Reconstruct.partial_typesN]
||> the_default ATP_Proof_Reconstruct.default_metis_lam_trans
in Metis_Tactic.metis_tac type_encs lam_trans ctxt thms end
- else if !reconstructor = "metis" then
+ else if !meth = "metis" then
Metis_Tactic.metis_tac [] ATP_Proof_Reconstruct.default_metis_lam_trans ctxt thms
else
K all_tac
end
- fun apply_reconstructor named_thms =
- Mirabelle.can_apply timeout (do_reconstructor named_thms) st
+ fun apply_method named_thms =
+ Mirabelle.can_apply timeout (do_method named_thms) st
fun with_time (false, t) = "failed (" ^ string_of_int t ^ ")"
- | with_time (true, t) = (change_data id (inc_reconstructor_success m);
+ | with_time (true, t) = (change_data id (inc_proof_method_success m);
if trivial then ()
- else change_data id (inc_reconstructor_nontriv_success m);
- change_data id (inc_reconstructor_lemmas m (length named_thms));
- change_data id (inc_reconstructor_time m t);
- change_data id (inc_reconstructor_posns m (pos, trivial));
- if name = "proof" then change_data id (inc_reconstructor_proofs m) else ();
+ else change_data id (inc_proof_method_nontriv_success m);
+ change_data id (inc_proof_method_lemmas m (length named_thms));
+ change_data id (inc_proof_method_time m t);
+ change_data id (inc_proof_method_posns m (pos, trivial));
+ if name = "proof" then change_data id (inc_proof_method_proofs m) else ();
"succeeded (" ^ string_of_int t ^ ")")
- fun timed_reconstructor named_thms =
- (with_time (Mirabelle.cpu_time apply_reconstructor named_thms), true)
- handle TimeLimit.TimeOut => (change_data id (inc_reconstructor_timeout m); ("timeout", false))
+ fun timed_method named_thms =
+ (with_time (Mirabelle.cpu_time apply_method named_thms), true)
+ handle TimeLimit.TimeOut => (change_data id (inc_proof_method_timeout m); ("timeout", false))
| ERROR msg => ("error: " ^ msg, false)
val _ = log separator
- val _ = change_data id (inc_reconstructor_calls m)
- val _ = if trivial then () else change_data id (inc_reconstructor_nontriv_calls m)
+ val _ = change_data id (inc_proof_method_calls m)
+ val _ = if trivial then () else change_data id (inc_proof_method_nontriv_calls m)
in
named_thms
- |> timed_reconstructor
- |>> log o prefix (reconstructor_tag reconstructor id)
+ |> timed_method
+ |>> log o prefix (proof_method_tag meth id)
|> snd
end
@@ -717,7 +716,7 @@
if !num_sledgehammer_calls > max_calls then ()
else
let
- val reconstructor = Unsynchronized.ref ""
+ val meth = Unsynchronized.ref ""
val named_thms =
Unsynchronized.ref (NONE : ((string * stature) * thm list) list option)
val minimize = AList.defined (op =) args minimizeK
@@ -728,33 +727,28 @@
Try0.try0 (SOME try_timeout) ([], [], [], []) pre
handle TimeLimit.TimeOut => false
else false
- fun apply_reconstructor m1 m2 =
+ fun apply_method m1 m2 =
if metis_ft
then
- if not (Mirabelle.catch_result (reconstructor_tag reconstructor) false
- (run_reconstructor trivial false m1 name reconstructor
- (these (!named_thms))) id st)
+ if not (Mirabelle.catch_result (proof_method_tag meth) false
+ (run_proof_method trivial false m1 name meth (these (!named_thms))) id st)
then
- (Mirabelle.catch_result (reconstructor_tag reconstructor) false
- (run_reconstructor trivial true m2 name reconstructor
- (these (!named_thms))) id st; ())
+ (Mirabelle.catch_result (proof_method_tag meth) false
+ (run_proof_method trivial true m2 name meth (these (!named_thms))) id st; ())
else ()
else
- (Mirabelle.catch_result (reconstructor_tag reconstructor) false
- (run_reconstructor trivial false m1 name reconstructor
- (these (!named_thms))) id st; ())
+ (Mirabelle.catch_result (proof_method_tag meth) false
+ (run_proof_method trivial false m1 name meth (these (!named_thms))) id st; ())
in
change_data id (set_mini minimize);
- Mirabelle.catch sh_tag (run_sledgehammer trivial args reconstructor
- named_thms) id st;
+ Mirabelle.catch sh_tag (run_sledgehammer trivial args meth named_thms) id st;
if is_some (!named_thms)
then
- (apply_reconstructor Unminimized UnminimizedFT;
+ (apply_method Unminimized UnminimizedFT;
if minimize andalso not (null (these (!named_thms)))
then
- (Mirabelle.catch minimize_tag
- (run_minimize args reconstructor named_thms) id st;
- apply_reconstructor Minimized MinimizedFT)
+ (Mirabelle.catch minimize_tag (run_minimize args meth named_thms) id st;
+ apply_method Minimized MinimizedFT)
else ())
else ()
end
--- a/src/HOL/Tools/ATP/atp_proof_reconstruct.ML Mon Feb 03 14:35:19 2014 +0100
+++ b/src/HOL/Tools/ATP/atp_proof_reconstruct.ML Mon Feb 03 15:19:07 2014 +0100
@@ -28,9 +28,9 @@
val partial_type_encs : string list
val default_metis_lam_trans : string
- val metis_call : string -> string -> string
val forall_of : term -> term -> term
val exists_of : term -> term -> term
+ val type_enc_aliases : (string * string list) list
val unalias_type_enc : string -> string list
val term_of_atp : Proof.context -> bool -> int Symtab.table -> typ option ->
(string, string atp_type) atp_term -> term
@@ -84,17 +84,6 @@
val default_metis_lam_trans = combsN
-fun metis_call type_enc lam_trans =
- let
- val type_enc =
- (case AList.find (fn (enc, encs) => enc = hd encs) type_enc_aliases type_enc of
- [alias] => alias
- | _ => type_enc)
- val opts =
- [] |> type_enc <> partial_typesN ? cons type_enc
- |> lam_trans <> default_metis_lam_trans ? cons lam_trans
- in metisN ^ (if null opts then "" else " (" ^ commas opts ^ ")") end
-
fun term_name' (Var ((s, _), _)) = perhaps (try Name.dest_skolem) s
| term_name' _ = ""
--- a/src/HOL/Tools/Metis/metis_tactic.ML Mon Feb 03 14:35:19 2014 +0100
+++ b/src/HOL/Tools/Metis/metis_tactic.ML Mon Feb 03 15:19:07 2014 +0100
@@ -129,6 +129,17 @@
| ord => ord
in {weight = weight, precedence = precedence} end
+fun metis_call type_enc lam_trans =
+ let
+ val type_enc =
+ (case AList.find (fn (enc, encs) => enc = hd encs) type_enc_aliases type_enc of
+ [alias] => alias
+ | _ => type_enc)
+ val opts =
+ [] |> type_enc <> partial_typesN ? cons type_enc
+ |> lam_trans <> default_metis_lam_trans ? cons lam_trans
+ in metisN ^ (if null opts then "" else " (" ^ commas opts ^ ")") end
+
exception METIS_UNPROVABLE of unit
(* Main function to start Metis proof and reconstruction *)
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Mon Feb 03 14:35:19 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Mon Feb 03 15:19:07 2014 +0100
@@ -286,7 +286,7 @@
val ctxt = ctxt
|> enrich_context_with_local_facts canonical_isar_proof
- |> silence_reconstructors debug
+ |> silence_proof_methods debug
val preplay_data = Unsynchronized.ref Canonical_Label_Tab.empty
@@ -354,9 +354,9 @@
if isar_proofs = SOME true then "\nWarning: The Isar proof construction failed." else "")
in one_line_proof ^ isar_proof end
-fun isar_proof_would_be_a_good_idea (reconstr, play) =
+fun isar_proof_would_be_a_good_idea (meth, play) =
(case play of
- Played _ => reconstr = SMT
+ Played _ => meth = SMT_Method
| Play_Timed_Out _ => true
| Play_Failed => true
| Not_Played => false)
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML Mon Feb 03 14:35:19 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML Mon Feb 03 15:19:07 2014 +0100
@@ -100,27 +100,6 @@
|> Skip_Proof.make_thm thy
end
-fun tac_of_method ctxt (local_facts, global_facts) meth =
- Method.insert_tac local_facts THEN'
- (case meth of
- Metis_Method (type_enc_opt, lam_trans_opt) =>
- Metis_Tactic.metis_tac [type_enc_opt |> the_default partial_type_enc]
- (the_default default_metis_lam_trans lam_trans_opt) ctxt global_facts
- | SMT_Method => SMT_Solver.smt_tac ctxt global_facts
- | Meson_Method => Meson.meson_tac ctxt global_facts
- | _ =>
- Method.insert_tac global_facts THEN'
- (case meth of
- Simp_Method => Simplifier.asm_full_simp_tac ctxt
- | Simp_Size_Method =>
- Simplifier.asm_full_simp_tac (Simplifier.add_simp @{thm size_ne_size_imp_ne} ctxt)
- | Auto_Method => K (Clasimp.auto_tac ctxt)
- | Fastforce_Method => Clasimp.fast_force_tac ctxt
- | Force_Method => Clasimp.force_tac ctxt
- | Arith_Method => Arith_Data.arith_tac ctxt
- | Blast_Method => blast_tac ctxt
- | Algebra_Method => Groebner.algebra_tac [] [] ctxt))
-
(* main function for preplaying Isar steps; may throw exceptions *)
fun raw_preplay_step_for_method ctxt timeout meth (Prove (_, xs, _, t, subproofs, fact_names, _)) =
let
@@ -149,7 +128,7 @@
fun prove () =
Goal.prove ctxt [] [] goal (fn {context = ctxt, ...} =>
- HEADGOAL (tac_of_method ctxt facts meth))
+ HEADGOAL (tac_of_proof_method ctxt facts meth))
handle ERROR msg => error ("Preplay error: " ^ msg)
val play_outcome = take_time timeout prove ()
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML Mon Feb 03 14:35:19 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML Mon Feb 03 15:19:07 2014 +0100
@@ -8,24 +8,13 @@
signature SLEDGEHAMMER_ISAR_PROOF =
sig
+ type proof_method = Sledgehammer_Reconstructor.proof_method
+
type label = string * int
type facts = label list * string list (* local and global facts *)
datatype isar_qualifier = Show | Then
- datatype proof_method =
- Metis_Method of string option * string option |
- Meson_Method |
- SMT_Method |
- Simp_Method |
- Simp_Size_Method |
- Auto_Method |
- Fastforce_Method |
- Force_Method |
- Arith_Method |
- Blast_Method |
- Algebra_Method
-
datatype isar_proof =
Proof of (string * typ) list * (label * term) list * isar_step list
and isar_step =
@@ -38,8 +27,6 @@
val label_ord : label * label -> order
val string_of_label : label -> string
- val string_of_proof_method : proof_method -> string
-
val steps_of_isar_proof : isar_proof -> isar_step list
val label_of_isar_step : isar_step -> label option
@@ -79,19 +66,6 @@
datatype isar_qualifier = Show | Then
-datatype proof_method =
- Metis_Method of string option * string option |
- Meson_Method |
- SMT_Method |
- Simp_Method |
- Simp_Size_Method |
- Auto_Method |
- Fastforce_Method |
- Force_Method |
- Arith_Method |
- Blast_Method |
- Algebra_Method
-
datatype isar_proof =
Proof of (string * typ) list * (label * term) list * isar_step list
and isar_step =
@@ -105,22 +79,6 @@
fun string_of_label (s, num) = s ^ string_of_int num
-fun string_of_proof_method meth =
- (case meth of
- Metis_Method (NONE, NONE) => "metis"
- | Metis_Method (type_enc_opt, lam_trans_opt) =>
- "metis (" ^ commas (map_filter I [type_enc_opt, lam_trans_opt]) ^ ")"
- | Meson_Method => "meson"
- | SMT_Method => "smt"
- | Simp_Method => "simp"
- | Simp_Size_Method => "simp add: size_ne_size_imp_ne"
- | Auto_Method => "auto"
- | Fastforce_Method => "fastforce"
- | Force_Method => "force"
- | Arith_Method => "arith"
- | Blast_Method => "blast"
- | Algebra_Method => "algebra")
-
fun steps_of_isar_proof (Proof (_, _, steps)) = steps
fun label_of_isar_step (Prove (_, _, l, _, _, _, _)) = SOME l
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML Mon Feb 03 14:35:19 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML Mon Feb 03 15:19:07 2014 +0100
@@ -12,7 +12,7 @@
type stature = ATP_Problem_Generate.stature
type type_enc = ATP_Problem_Generate.type_enc
type fact = Sledgehammer_Fact.fact
- type reconstructor = Sledgehammer_Reconstructor.reconstructor
+ type proof_method = Sledgehammer_Reconstructor.proof_method
type play_outcome = Sledgehammer_Reconstructor.play_outcome
type minimize_command = Sledgehammer_Reconstructor.minimize_command
@@ -57,8 +57,8 @@
used_facts : (string * stature) list,
used_from : fact list,
run_time : Time.time,
- preplay : (reconstructor * play_outcome) Lazy.lazy,
- message : reconstructor * play_outcome -> string,
+ preplay : (proof_method * play_outcome) Lazy.lazy,
+ message : proof_method * play_outcome -> string,
message_tail : string}
type prover =
@@ -66,23 +66,22 @@
-> prover_problem -> prover_result
val SledgehammerN : string
- val plain_metis : reconstructor
val overlord_file_location_of_prover : string -> string * string
val proof_banner : mode -> string -> string
- val extract_reconstructor : params -> reconstructor -> string * (string * string list) list
- val is_reconstructor : string -> bool
+ val extract_proof_method : params -> proof_method -> string * (string * string list) list
+ val is_proof_method : string -> bool
val is_atp : theory -> string -> bool
- val bunch_of_reconstructors : bool -> (bool -> string) -> reconstructor list
+ val bunch_of_proof_methods : bool -> string -> proof_method 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 play_one_line_proof : mode -> bool -> bool -> Time.time -> ((string * 'a) * thm) list ->
- Proof.state -> int -> reconstructor -> reconstructor list -> reconstructor * play_outcome
+ Proof.state -> int -> proof_method -> proof_method list -> proof_method * play_outcome
val remotify_atp_if_not_installed : theory -> string -> string option
val isar_supported_prover_of : theory -> string -> string
val choose_minimize_command : theory -> params -> ((string * string list) list -> string -> 'a) ->
- string -> reconstructor * play_outcome -> 'a
+ string -> proof_method * play_outcome -> 'a
val repair_monomorph_context : int option -> int -> int option -> int -> Proof.context ->
Proof.context
@@ -110,9 +109,8 @@
"Async_Manager". *)
val SledgehammerN = "Sledgehammer"
-val reconstructor_names = [metisN, smtN]
-val plain_metis = Metis (hd partial_type_encs, combsN)
-val is_reconstructor = member (op =) reconstructor_names
+val proof_method_names = [metisN, smtN]
+val is_proof_method = member (op =) proof_method_names
val is_atp = member (op =) o supported_atps
@@ -167,8 +165,8 @@
used_facts : (string * stature) list,
used_from : fact list,
run_time : Time.time,
- preplay : (reconstructor * play_outcome) Lazy.lazy,
- message : reconstructor * play_outcome -> string,
+ preplay : (proof_method * play_outcome) Lazy.lazy,
+ message : proof_method * play_outcome -> string,
message_tail : string}
type prover =
@@ -183,29 +181,30 @@
| Try => "Sledgehammer (" ^ quote name ^ ") found a proof"
| _ => "Try this")
-fun bunch_of_reconstructors needs_full_types lam_trans =
+fun bunch_of_proof_methods needs_full_types desperate_lam_trans =
if needs_full_types then
- [Metis (full_type_enc, lam_trans false),
- Metis (really_full_type_enc, lam_trans false),
- Metis (full_type_enc, lam_trans true),
- Metis (really_full_type_enc, lam_trans true),
- SMT]
+ [Metis_Method (SOME full_type_enc, NONE),
+ Metis_Method (SOME really_full_type_enc, NONE),
+ Metis_Method (SOME full_type_enc, SOME desperate_lam_trans),
+ Metis_Method (SOME really_full_type_enc, SOME desperate_lam_trans),
+ SMT_Method]
else
- [Metis (partial_type_enc, lam_trans false),
- Metis (full_type_enc, lam_trans false),
- Metis (no_typesN, lam_trans true),
- Metis (really_full_type_enc, lam_trans true),
- SMT]
+ [Metis_Method (NONE, NONE),
+ Metis_Method (SOME full_type_enc, NONE),
+ Metis_Method (SOME no_typesN, SOME desperate_lam_trans),
+ Metis_Method (SOME really_full_type_enc, SOME desperate_lam_trans),
+ SMT_Method]
-fun extract_reconstructor ({type_enc, lam_trans, ...} : params) (Metis (type_enc', lam_trans')) =
+fun extract_proof_method ({type_enc, lam_trans, ...} : params)
+ (Metis_Method (type_enc', lam_trans')) =
let
val override_params =
- (if is_none type_enc andalso type_enc' = hd partial_type_encs then []
- else [("type_enc", [hd (unalias_type_enc type_enc')])]) @
- (if is_none lam_trans andalso lam_trans' = default_metis_lam_trans then []
- else [("lam_trans", [lam_trans'])])
+ (if is_none type_enc' andalso is_none type_enc then []
+ else [("type_enc", [hd (unalias_type_enc (type_enc' |> the_default partial_typesN))])]) @
+ (if is_none lam_trans' andalso is_none lam_trans then []
+ else [("lam_trans", [lam_trans' |> the_default default_metis_lam_trans])])
in (metisN, override_params) end
- | extract_reconstructor _ SMT = (smtN, [])
+ | extract_proof_method _ SMT_Method = (smtN, [])
(* based on "Mirabelle.can_apply" and generalized *)
fun timed_apply timeout tac state i =
@@ -216,49 +215,46 @@
TimeLimit.timeLimit timeout (try (Seq.pull o full_tac)) goal
end
-fun tac_of_reconstructor (Metis (type_enc, lam_trans)) = metis_tac [type_enc] lam_trans
- | tac_of_reconstructor SMT = SMT_Solver.smt_tac
-
-fun timed_reconstructor reconstr debug timeout ths =
- timed_apply timeout (silence_reconstructors debug
- #> (fn ctxt => tac_of_reconstructor reconstr ctxt ths))
+(* FIXME *)
+fun timed_proof_method meth debug timeout ths =
+ timed_apply timeout (silence_proof_methods debug
+ #> (fn ctxt => tac_of_proof_method ctxt ([], ths) meth))
fun is_fact_chained ((_, (sc, _)), _) = sc = Chained
fun filter_used_facts keep_chained used =
filter ((member (op =) used o fst) orf (if keep_chained then is_fact_chained else K false))
-fun play_one_line_proof mode debug verbose timeout pairs state i preferred reconstrs =
+fun play_one_line_proof mode debug verbose timeout pairs state i preferred meths =
let
- fun get_preferred reconstrs =
- if member (op =) reconstrs preferred then preferred
- else List.last reconstrs
+ fun get_preferred meths =
+ if member (op =) meths preferred then preferred else List.last meths
in
if timeout = Time.zeroTime then
- (get_preferred reconstrs, Not_Played)
+ (get_preferred meths, Not_Played)
else
let
val _ = if mode = Minimize then Output.urgent_message "Preplaying proof..." else ()
val ths = pairs |> sort_wrt (fst o fst) |> map snd
- fun play [] [] = (get_preferred reconstrs, Play_Failed)
+ fun play [] [] = (get_preferred meths, Play_Failed)
| play timed_outs [] = (get_preferred timed_outs, Play_Timed_Out timeout)
- | play timed_out (reconstr :: reconstrs) =
+ | play timed_out (meth :: meths) =
let
val _ =
if verbose then
- Output.urgent_message ("Trying \"" ^ string_of_reconstructor reconstr ^
+ Output.urgent_message ("Trying \"" ^ string_of_proof_method meth ^
"\" for " ^ string_of_time timeout ^ "...")
else
()
val timer = Timer.startRealTimer ()
in
- case timed_reconstructor reconstr debug timeout ths state i of
- SOME (SOME _) => (reconstr, Played (Timer.checkRealTimer timer))
- | _ => play timed_out reconstrs
+ case timed_proof_method meth debug timeout ths state i of
+ SOME (SOME _) => (meth, Played (Timer.checkRealTimer timer))
+ | _ => play timed_out meths
end
- handle TimeLimit.TimeOut => play (reconstr :: timed_out) reconstrs
+ handle TimeLimit.TimeOut => play (meth :: timed_out) meths
in
- play [] reconstrs
+ play [] meths
end
end
@@ -275,9 +271,8 @@
val maybe_isar_name = name |> isar_proofs = SOME true ? isar_supported_prover_of thy
val (min_name, override_params) =
(case preplay of
- (reconstr, Played _) =>
- if isar_proofs = SOME true then (maybe_isar_name, [])
- else extract_reconstructor params reconstr
+ (meth, Played _) =>
+ if isar_proofs = SOME true then (maybe_isar_name, []) else extract_proof_method params meth
| _ => (maybe_isar_name, []))
in minimize_command override_params min_name end
@@ -293,7 +288,7 @@
let
val thy = Proof_Context.theory_of ctxt
val (remote_provers, local_provers) =
- reconstructor_names @
+ proof_method_names @
sort_strings (supported_atps thy) @
sort_strings (SMT_Solver.available_solvers_of ctxt)
|> List.partition (String.isPrefix remote_prefix)
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML Mon Feb 03 14:35:19 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML Mon Feb 03 15:19:07 2014 +0100
@@ -346,18 +346,15 @@
let
val used_facts = used_facts_in_atp_proof ctxt fact_names atp_proof
val needs_full_types = is_typed_helper_used_in_atp_proof atp_proof
- val reconstrs =
- bunch_of_reconstructors needs_full_types (fn desperate =>
- if desperate then
- if atp_proof_prefers_lifting atp_proof then liftingN else hide_lamsN
- else
- default_metis_lam_trans)
+ val meths =
+ bunch_of_proof_methods needs_full_types
+ (if atp_proof_prefers_lifting atp_proof then liftingN else hide_lamsN)
in
(used_facts,
Lazy.lazy (fn () =>
let val used_pairs = used_from |> filter_used_facts false used_facts in
play_one_line_proof mode debug verbose preplay_timeout used_pairs state subgoal
- (hd reconstrs) reconstrs
+ (hd meths) meths
end),
fn preplay =>
let
@@ -392,7 +389,8 @@
""))
end
| SOME failure =>
- ([], Lazy.value (plain_metis, Play_Failed), fn _ => string_of_atp_failure failure, ""))
+ ([], Lazy.value (Metis_Method (NONE, NONE), Play_Failed),
+ fn _ => string_of_atp_failure failure, ""))
in
{outcome = outcome, used_facts = used_facts, used_from = used_from, run_time = run_time,
preplay = preplay, message = message, message_tail = message_tail}
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML Mon Feb 03 14:35:19 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML Mon Feb 03 15:19:07 2014 +0100
@@ -8,7 +8,7 @@
signature SLEDGEHAMMER_PROVER_MINIMIZE =
sig
type stature = ATP_Problem_Generate.stature
- type reconstructor = Sledgehammer_Reconstructor.reconstructor
+ type proof_method = Sledgehammer_Reconstructor.proof_method
type play_outcome = Sledgehammer_Reconstructor.play_outcome
type mode = Sledgehammer_Prover.mode
type params = Sledgehammer_Prover.params
@@ -23,11 +23,11 @@
val auto_minimize_min_facts : int Config.T
val auto_minimize_max_time : real Config.T
val minimize_facts : (thm list -> unit) -> string -> params -> bool -> int -> int ->
- Proof.state -> thm -> (reconstructor * play_outcome) Lazy.lazy option ->
+ Proof.state -> thm -> (proof_method * play_outcome) Lazy.lazy option ->
((string * stature) * thm list) list ->
((string * stature) * thm list) list option
- * ((reconstructor * play_outcome) Lazy.lazy * ((reconstructor * play_outcome) -> string)
- * string)
+ * ((proof_method * play_outcome) Lazy.lazy * ((proof_method * play_outcome) -> string)
+ * string)
val get_minimizing_prover : Proof.context -> mode -> (thm list -> unit) -> string -> prover
val run_minimize : params -> (thm list -> unit) -> int -> (Facts.ref * Attrib.src list) list ->
@@ -50,29 +50,25 @@
open Sledgehammer_Prover_ATP
open Sledgehammer_Prover_SMT
-fun run_reconstructor mode name (params as {debug, verbose, timeout, type_enc, lam_trans, ...})
+fun run_proof_method mode name (params as {debug, verbose, timeout, type_enc, lam_trans, ...})
minimize_command
({state, subgoal, subgoal_count, factss = (_, facts) :: _, ...} : prover_problem) =
let
- val reconstr =
- if name = metisN then
- Metis (type_enc |> the_default (hd partial_type_encs),
- lam_trans |> the_default default_metis_lam_trans)
- else if name = smtN then
- SMT
- else
- raise Fail ("unknown reconstructor: " ^ quote name)
+ val meth =
+ if name = metisN then Metis_Method (type_enc, lam_trans)
+ else if name = smtN then SMT_Method
+ else raise Fail ("unknown proof_method: " ^ quote name)
val used_facts = facts |> map fst
in
(case play_one_line_proof (if mode = Minimize then Normal else mode) debug verbose timeout facts
- state subgoal reconstr [reconstr] of
+ state subgoal meth [meth] of
play as (_, Played time) =>
{outcome = NONE, used_facts = used_facts, used_from = facts, run_time = time,
preplay = Lazy.value play,
message =
fn play =>
let
- val (_, override_params) = extract_reconstructor params reconstr
+ val (_, override_params) = extract_proof_method params meth
val one_line_params =
(play, proof_banner mode name, used_facts, minimize_command override_params name,
subgoal, subgoal_count)
@@ -93,18 +89,18 @@
fun is_prover_supported ctxt =
let val thy = Proof_Context.theory_of ctxt in
- is_reconstructor orf is_atp thy orf is_smt_prover ctxt
+ is_proof_method orf is_atp thy orf is_smt_prover ctxt
end
fun is_prover_installed ctxt =
- is_reconstructor orf is_smt_prover ctxt orf is_atp_installed (Proof_Context.theory_of ctxt)
+ is_proof_method orf is_smt_prover ctxt orf is_atp_installed (Proof_Context.theory_of ctxt)
-val reconstructor_default_max_facts = 20
+val proof_method_default_max_facts = 20
fun default_max_facts_of_prover ctxt name =
let val thy = Proof_Context.theory_of ctxt in
- if is_reconstructor name then
- reconstructor_default_max_facts
+ if is_proof_method name then
+ proof_method_default_max_facts
else 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 (* is_smt_prover ctxt name *)
@@ -113,7 +109,7 @@
fun get_prover ctxt mode name =
let val thy = Proof_Context.theory_of ctxt in
- if is_reconstructor name then run_reconstructor mode name
+ if is_proof_method name then run_proof_method mode name
else 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 ^ ".")
@@ -286,10 +282,11 @@
"Timeout: You can increase the time limit using the \"timeout\" option (e.g., \
\timeout = " ^ string_of_int (10 + Time.toMilliseconds timeout div 1000) ^ "\").", ""))
| {preplay, message, ...} => (NONE, (preplay, prefix "Prover error: " o message, ""))))
- handle ERROR msg => (NONE, (Lazy.value (plain_metis, Play_Failed), fn _ => "Error: " ^ msg, ""))
+ handle ERROR msg =>
+ (NONE, (Lazy.value (Metis_Method (NONE, NONE), Play_Failed), fn _ => "Error: " ^ msg, ""))
end
-fun adjust_reconstructor_params override_params
+fun adjust_proof_method_params override_params
({debug, verbose, overlord, spy, blocking, provers, type_enc, strict, lam_trans,
uncurried_aliases, learn, fact_filter, max_facts, fact_thresholds, max_mono_iters,
max_new_mono_instances, isar_proofs, compress_isar, try0_isar, slice, minimize, timeout,
@@ -299,7 +296,7 @@
(case AList.lookup (op =) override_params name of
SOME [s] => SOME s
| _ => default_value)
- (* Only those options that reconstructors are interested in are considered here. *)
+ (* Only those options that proof_methods are interested in are considered here. *)
val type_enc = lookup_override "type_enc" type_enc
val lam_trans = lookup_override "lam_trans" lam_trans
in
@@ -336,18 +333,18 @@
fun prover_fast_enough () = can_min_fast_enough run_time
in
(case Lazy.force preplay of
- (reconstr as Metis _, Played timeout) =>
+ (meth as Metis_Method _, Played timeout) =>
if isar_proofs = SOME true then
(* Cheat: Assume the selected ATP is as fast as "metis" for the goal it proved
itself. *)
(can_min_fast_enough timeout, (isar_supported_prover_of thy name, params))
else if can_min_fast_enough timeout then
- (true, extract_reconstructor params reconstr
+ (true, extract_proof_method params meth
||> (fn override_params =>
- adjust_reconstructor_params override_params params))
+ adjust_proof_method_params override_params params))
else
(prover_fast_enough (), (name, params))
- | (SMT, Played timeout) =>
+ | (SMT_Method, Played timeout) =>
(* Cheat: Assume the original prover is as fast as "smt" for the goal it proved
itself. *)
(can_min_fast_enough timeout, (name, params))
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML Mon Feb 03 14:35:19 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML Mon Feb 03 15:19:07 2014 +0100
@@ -233,9 +233,8 @@
(case outcome of
NONE =>
(Lazy.lazy (fn () =>
- play_one_line_proof mode debug verbose preplay_timeout used_pairs state subgoal SMT
- (bunch_of_reconstructors false (fn desperate =>
- if desperate then liftingN else default_metis_lam_trans))),
+ play_one_line_proof mode debug verbose preplay_timeout used_pairs state subgoal
+ SMT_Method (bunch_of_proof_methods false liftingN)),
fn preplay =>
let
val one_line_params =
@@ -248,7 +247,8 @@
end,
if verbose then "\nSMT solver real CPU time: " ^ string_of_time run_time ^ "." else "")
| SOME failure =>
- (Lazy.value (plain_metis, Play_Failed), fn _ => string_of_atp_failure failure, ""))
+ (Lazy.value (Metis_Method (NONE, NONE), Play_Failed),
+ fn _ => string_of_atp_failure failure, ""))
in
{outcome = outcome, used_facts = used_facts, used_from = used_from, run_time = run_time,
preplay = preplay, message = message, message_tail = message_tail}
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstructor.ML Mon Feb 03 14:35:19 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstructor.ML Mon Feb 03 15:19:07 2014 +0100
@@ -9,9 +9,18 @@
sig
type stature = ATP_Problem_Generate.stature
- datatype reconstructor =
- Metis of string * string |
- SMT
+ datatype proof_method =
+ Metis_Method of string option * string option |
+ Meson_Method |
+ SMT_Method |
+ Simp_Method |
+ Simp_Size_Method |
+ Auto_Method |
+ Fastforce_Method |
+ Force_Method |
+ Arith_Method |
+ Blast_Method |
+ Algebra_Method
datatype play_outcome =
Played of Time.time |
@@ -21,16 +30,17 @@
type minimize_command = string list -> string
type one_line_params =
- (reconstructor * play_outcome) * string * (string * stature) list * minimize_command * int * int
+ (proof_method * play_outcome) * string * (string * stature) list * minimize_command * int * int
val smtN : string
- val string_of_reconstructor : reconstructor -> string
+ val string_of_proof_method : proof_method -> string
+ val tac_of_proof_method : Proof.context -> thm list * thm list -> proof_method -> int -> tactic
val string_of_play_outcome : play_outcome -> string
val play_outcome_ord : play_outcome * play_outcome -> order
val one_line_proof_text : int -> one_line_params -> string
- val silence_reconstructors : bool -> Proof.context -> Proof.context
+ val silence_proof_methods : bool -> Proof.context -> Proof.context
end;
structure Sledgehammer_Reconstructor : SLEDGEHAMMER_RECONSTRUCTOR =
@@ -40,9 +50,18 @@
open ATP_Problem_Generate
open ATP_Proof_Reconstruct
-datatype reconstructor =
- Metis of string * string |
- SMT
+datatype proof_method =
+ Metis_Method of string option * string option |
+ Meson_Method |
+ SMT_Method |
+ Simp_Method |
+ Simp_Size_Method |
+ Auto_Method |
+ Fastforce_Method |
+ Force_Method |
+ Arith_Method |
+ Blast_Method |
+ Algebra_Method
datatype play_outcome =
Played of Time.time |
@@ -52,12 +71,46 @@
type minimize_command = string list -> string
type one_line_params =
- (reconstructor * play_outcome) * string * (string * stature) list * minimize_command * int * int
+ (proof_method * play_outcome) * string * (string * stature) list * minimize_command * int * int
val smtN = "smt"
-fun string_of_reconstructor (Metis (type_enc, lam_trans)) = metis_call type_enc lam_trans
- | string_of_reconstructor SMT = smtN
+fun string_of_proof_method meth =
+ (case meth of
+ Metis_Method (NONE, NONE) => "metis"
+ | Metis_Method (type_enc_opt, lam_trans_opt) =>
+ "metis (" ^ commas (map_filter I [type_enc_opt, lam_trans_opt]) ^ ")"
+ | Meson_Method => "meson"
+ | SMT_Method => "smt"
+ | Simp_Method => "simp"
+ | Simp_Size_Method => "simp add: size_ne_size_imp_ne"
+ | Auto_Method => "auto"
+ | Fastforce_Method => "fastforce"
+ | Force_Method => "force"
+ | Arith_Method => "arith"
+ | Blast_Method => "blast"
+ | Algebra_Method => "algebra")
+
+fun tac_of_proof_method ctxt (local_facts, global_facts) meth =
+ Method.insert_tac local_facts THEN'
+ (case meth of
+ Metis_Method (type_enc_opt, lam_trans_opt) =>
+ Metis_Tactic.metis_tac [type_enc_opt |> the_default partial_type_enc]
+ (the_default default_metis_lam_trans lam_trans_opt) ctxt global_facts
+ | SMT_Method => SMT_Solver.smt_tac ctxt global_facts
+ | Meson_Method => Meson.meson_tac ctxt global_facts
+ | _ =>
+ Method.insert_tac global_facts THEN'
+ (case meth of
+ Simp_Method => Simplifier.asm_full_simp_tac ctxt
+ | Simp_Size_Method =>
+ Simplifier.asm_full_simp_tac (Simplifier.add_simp @{thm size_ne_size_imp_ne} ctxt)
+ | Auto_Method => K (Clasimp.auto_tac ctxt)
+ | Fastforce_Method => Clasimp.fast_force_tac ctxt
+ | Force_Method => Clasimp.force_tac ctxt
+ | Arith_Method => Arith_Data.arith_tac ctxt
+ | Blast_Method => blast_tac ctxt
+ | Algebra_Method => Groebner.algebra_tac [] [] ctxt))
fun string_of_play_outcome (Played time) = string_of_ext_time (false, time)
| string_of_play_outcome (Play_Timed_Out time) = string_of_ext_time (true, time) ^ ", timed out"
@@ -94,9 +147,10 @@
name |> not (Symbol_Pos.is_identifier name) ? enclose "(" ")"
| command_call name args = "(" ^ name ^ " " ^ space_implode " " args ^ ")"
-fun reconstructor_command reconstr i n used_chaineds num_chained ss =
+(* FIXME *)
+fun proof_method_command meth i n used_chaineds num_chained ss =
(* unusing_chained_facts used_chaineds num_chained ^ *)
- apply_on_subgoal i n ^ command_call (string_of_reconstructor reconstr) ss
+ apply_on_subgoal i n ^ command_call (string_of_proof_method meth) ss
fun show_time NONE = ""
| show_time (SOME ext_time) = " (" ^ string_of_ext_time ext_time ^ ")"
@@ -116,7 +170,7 @@
|> pairself (sort_distinct (string_ord o pairself fst))
fun one_line_proof_text num_chained
- ((reconstr, play), banner, used_facts, minimize_command, subgoal, subgoal_count) =
+ ((meth, play), banner, used_facts, minimize_command, subgoal, subgoal_count) =
let
val (chained, extra) = split_used_facts used_facts
@@ -129,7 +183,7 @@
val try_line =
map fst extra
- |> reconstructor_command reconstr subgoal subgoal_count (map fst chained) num_chained
+ |> proof_method_command meth subgoal subgoal_count (map fst chained) num_chained
|> (if failed then
enclose "One-line proof reconstruction failed: "
".\n(Invoking \"sledgehammer\" with \"[strict]\" might solve this.)"
@@ -139,9 +193,9 @@
try_line ^ minimize_line minimize_command (map fst (extra @ chained))
end
-(* Makes reconstructor tools as silent as possible. The "set_visible" calls suppresses "Unification
- bound exceeded" warnings and the like. *)
-fun silence_reconstructors debug =
+(* Makes proof methods as silent as possible. The "set_visible" calls suppresses "Unification bound
+ exceeded" warnings and the like. *)
+fun silence_proof_methods debug =
Try0.silence_methods debug
#> Config.put SMT_Config.verbose debug
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Mon Feb 03 14:35:19 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Mon Feb 03 15:19:07 2014 +0100
@@ -69,10 +69,10 @@
| "" => SOME true
| _ => raise Option.Option)
handle Option.Option =>
- let val ss = map quote ((option ? cons "smart") ["true", "false"]) in
- error ("Parameter " ^ quote name ^ " must be assigned " ^
- space_implode " " (serial_commas "or" ss) ^ ".")
- end
+ let val ss = map quote ((option ? cons "smart") ["true", "false"]) in
+ error ("Parameter " ^ quote name ^ " must be assigned " ^
+ space_implode " " (serial_commas "or" ss) ^ ".")
+ end
val has_junk =
exists (fn s => not (Symbol.is_digit s) andalso s <> ".") o raw_explode (* FIXME Symbol.explode (?) *)
@@ -80,8 +80,8 @@
fun parse_time name s =
let val secs = if has_junk s then NONE else Real.fromString s in
if is_none secs orelse Real.< (the secs, 0.0) then
- error ("Parameter " ^ quote name ^ " must be assigned a nonnegative \
- \number of seconds (e.g., \"60\", \"0.5\") or \"none\".")
+ error ("Parameter " ^ quote name ^ " must be assigned a nonnegative \number of seconds \
+ \(e.g., \"60\", \"0.5\") or \"none\".")
else
seconds (the secs)
end