--- a/src/HOL/Tools/Sledgehammer/sledgehammer_preplay.ML Mon Dec 16 12:02:28 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_preplay.ML Mon Dec 16 12:26:18 2013 +0100
@@ -102,13 +102,13 @@
|> Skip_Proof.make_thm thy
end
-fun tac_of_method method type_enc lam_trans ctxt facts =
- (case method of
+fun tac_of_method meth type_enc lam_trans ctxt facts =
+ (case meth of
Metis_Method => Metis_Tactic.metis_tac [type_enc] lam_trans ctxt facts
| Meson_Method => Meson.meson_tac ctxt facts
| _ =>
Method.insert_tac facts THEN'
- (case method of
+ (case meth of
Simp_Method => Simplifier.asm_full_simp_tac ctxt
| Auto_Method => K (Clasimp.auto_tac ctxt)
| Fastforce_Method => Clasimp.fast_force_tac ctxt
@@ -120,7 +120,7 @@
(* main function for preplaying Isar steps; may throw exceptions *)
fun preplay_raw _ _ _ _ _ (Let _) = zero_preplay_time
| preplay_raw debug type_enc lam_trans ctxt timeout
- (step as Prove (_, xs, _, t, subproofs, (fact_names, meth))) =
+ (step as Prove (_, xs, _, t, subproofs, (fact_names, meth :: _))) =
let
val goal =
(case xs of
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_print.ML Mon Dec 16 12:02:28 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_print.ML Mon Dec 16 12:26:18 2013 +0100
@@ -155,7 +155,7 @@
fun of_thus_hence qs = if member (op =) qs Show then "thus" else "hence"
- fun of_prove qs nr =
+ fun of_have qs nr =
if nr > 1 orelse (nr = 1 andalso member (op =) qs Then) then
"ultimately " ^ of_show_have qs
else if nr=1 orelse member (op =) qs Then then
@@ -184,8 +184,7 @@
| _ => raise Fail "Sledgehammer_Print: by_method")
fun using_facts [] [] = ""
- | using_facts ls ss =
- "using " ^ space_implode " " (map string_of_label ls @ ss) ^ " "
+ | using_facts ls ss = "using " ^ space_implode " " (map string_of_label ls @ ss) ^ " "
fun of_method ls ss Metis_Method =
reconstructor_command (Metis (type_enc, lam_trans)) 1 1 [] 0 (ls, ss)
@@ -236,26 +235,23 @@
SOME (size s - ind * indent_size - 1)) ^
suffix ^ "\n"
end
-
and of_subproofs _ _ _ [] = ""
| of_subproofs ind ctxt qs subproofs =
(if member (op =) qs Then then of_moreover ind else "") ^
space_implode (of_moreover ind) (map (of_subproof ind ctxt) subproofs)
-
and add_step_pre ind qs subproofs (s, ctxt) =
(s ^ of_subproofs ind ctxt qs subproofs ^ of_indent ind, ctxt)
-
and add_step ind (Let (t1, t2)) =
add_suffix (of_indent ind ^ "let ")
#> add_term t1
#> add_suffix " = "
#> add_term t2
#> add_suffix "\n"
- | add_step ind (step as Prove (qs, xs, l, t, subproofs, (facts, meth))) =
+ | add_step ind (step as Prove (qs, xs, l, t, subproofs, (facts, meth :: _))) =
(case xs of
[] => (* have *)
add_step_pre ind qs subproofs
- #> add_suffix (of_prove qs (length subproofs) ^ " ")
+ #> add_suffix (of_have qs (length subproofs) ^ " ")
#> add_step_post ind l t facts meth ""
| _ => (* obtain *)
add_step_pre ind qs subproofs
@@ -263,17 +259,15 @@
#> add_frees xs
#> add_suffix " where "
#> add_step_post ind l t facts meth
- (if use_metis_new_skolem step then "using [[metis_new_skolem]] " else ""))
-
+ (if use_metis_new_skolem step then "using [[metis_new_skolem]] " else ""))
and add_steps ind = fold (add_step ind)
-
and of_proof ind ctxt (Proof (xs, assms, steps)) =
("", ctxt) |> add_fix ind xs |> add_assms ind assms |> add_steps ind steps |> fst
in
(* One-step Metis proofs are pointless; better use the one-liner directly. *)
(case proof of
Proof ([], [], []) => "" (* degenerate case: the conjecture is "True" with Z3 *)
- | Proof ([], [], [Prove (_, [], _, _, [], (_, Metis_Method))]) => ""
+ | Proof ([], [], [Prove (_, [], _, _, [], (_, Metis_Method :: _))]) => ""
| _ =>
(if i <> 1 then "prefer " ^ string_of_int i ^ "\n" else "") ^
of_indent 0 ^ "proof -\n" ^ of_proof 1 ctxt proof ^
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof.ML Mon Dec 16 12:02:28 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof.ML Mon Dec 16 12:26:18 2013 +0100
@@ -18,7 +18,7 @@
and isar_step =
Let of term * term |
Prove of isar_qualifier list * (string * typ) list * label * term * isar_proof list *
- (facts * proof_method)
+ (facts * proof_method list)
and proof_method =
Metis_Method | Simp_Method | Auto_Method | Fastforce_Method | Force_Method | Arith_Method |
Blast_Method | Meson_Method
@@ -38,8 +38,7 @@
val label_of_step : isar_step -> label option
val subproofs_of_step : isar_step -> isar_proof list option
- val byline_of_step : isar_step -> (facts * proof_method) option
- val proof_method_of_step : isar_step -> proof_method option
+ val byline_of_step : isar_step -> (facts * proof_method list) option
val use_metis_new_skolem : isar_step -> bool
val fold_isar_step : (isar_step -> 'a -> 'a) -> isar_step -> 'a -> 'a
@@ -69,7 +68,7 @@
and isar_step =
Let of term * term |
Prove of isar_qualifier list * (string * typ) list * label * term * isar_proof list *
- (facts * proof_method)
+ (facts * proof_method list)
and proof_method =
Metis_Method | Simp_Method | Auto_Method | Fastforce_Method | Force_Method | Arith_Method |
Blast_Method | Meson_Method
@@ -96,12 +95,9 @@
fun byline_of_step (Prove (_, _, _, _, _, byline)) = SOME byline
| byline_of_step _ = NONE
-fun proof_method_of_step (Prove (_, _, _, _, _, (_, method))) = SOME method
- | proof_method_of_step _ = NONE
-
(* The new skolemizer puts the arguments in the same order as the ATPs (E and Vampire -- but see
also "atp_proof_reconstruct.ML" concerning Vampire). *)
-fun use_metis_new_skolem (Prove (_, xs, _, _, _, (_, meth))) =
+fun use_metis_new_skolem (Prove (_, xs, _, _, _, (_, meth :: _))) =
meth = Metis_Method andalso exists (fn (_, T) => length (binder_types T) > 1) xs
| use_metis_new_skolem _ = false
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Mon Dec 16 12:02:28 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Mon Dec 16 12:26:18 2013 +0100
@@ -230,9 +230,9 @@
fun chain_qs_lfs NONE lfs = ([], lfs)
| chain_qs_lfs (SOME l0) lfs =
if member (op =) lfs l0 then ([Then], lfs |> remove (op =) l0) else ([], lfs)
- fun chain_step lbl (Prove (qs, xs, l, t, subproofs, ((lfs, gfs), method))) =
+ fun chain_step lbl (Prove (qs, xs, l, t, subproofs, ((lfs, gfs), meths))) =
let val (qs', lfs) = chain_qs_lfs lbl lfs in
- Prove (qs' @ qs, xs, l, t, chain_proofs subproofs, ((lfs, gfs), method))
+ Prove (qs' @ qs, xs, l, t, chain_proofs subproofs, ((lfs, gfs), meths))
end
| chain_step _ step = step
and chain_steps _ [] = []
@@ -248,6 +248,15 @@
bool * bool * string * string * Time.time option * real * bool * (term, string) atp_step list *
thm
+val arith_methods =
+ [Arith_Method, Simp_Method, Auto_Method, Fastforce_Method, Blast_Method, Force_Method,
+ Metis_Method]
+val metislike_methods =
+ [Metis_Method, Simp_Method, Auto_Method, Arith_Method, Blast_Method, Fastforce_Method,
+ Force_Method, Meson_Method]
+val rewrite_methods = [Simp_Method, Auto_Method, Fastforce_Method, Force_Method, Metis_Method]
+val skolem_methods = [Metis_Method, Meson_Method]
+
fun isar_proof_text ctxt isar_proofs
(debug, verbose, metis_type_enc, metis_lam_trans, preplay_timeout, isar_compress, isar_try0,
atp_proof, goal)
@@ -287,12 +296,12 @@
map_filter (get_role (curry (op =) Lemma)) atp_proof
|> map (fn ((l, t), rule) =>
let
- val (skos, meth) =
- if is_skolemize_rule rule then (skolems_of t, Metis_Method)
- else if is_arith_rule rule then ([], Arith_Method)
- else ([], Auto_Method)
+ val (skos, meths) =
+ if is_skolemize_rule rule then (skolems_of t, skolem_methods)
+ else if is_arith_rule rule then ([], arith_methods)
+ else ([], rewrite_methods)
in
- Prove ([], skos, l, t, [], (([], []), meth))
+ Prove ([], skos, l, t, [], (([], []), meths))
end)
val bot = atp_proof |> List.last |> #1
@@ -340,7 +349,7 @@
accum
|> (if tainted = [] then
cons (Prove (if outer then [Show] else [], [], no_label, concl_t, [],
- ((the_list predecessor, []), Metis_Method)))
+ ((the_list predecessor, []), metislike_methods)))
else
I)
|> rev
@@ -355,15 +364,15 @@
fun do_rest l step = isar_steps outer (SOME l) (step :: accum) infs
val deps = fold add_fact_of_dependencies gamma no_facts
- val meth = if is_arith_rule rule then Arith_Method else Metis_Method
- val by = (deps, meth)
+ val meths = if is_arith_rule rule then arith_methods else metislike_methods
+ val by = (deps, meths)
in
if is_clause_tainted c then
(case gamma of
[g] =>
if skolem andalso is_clause_tainted g then
let val subproof = Proof (skolems_of (prop_of_clause g), [], rev accum) in
- isar_steps outer (SOME l) [prove [subproof] (no_facts, Metis_Method)] []
+ isar_steps outer (SOME l) [prove [subproof] (no_facts, skolem_methods)] []
end
else
do_rest l (prove [] by)
@@ -381,7 +390,7 @@
val step =
Prove (maybe_show outer c [], [], l, t,
map isar_case (filter_out (null o snd) cases),
- ((the_list predecessor, []), Metis_Method))
+ ((the_list predecessor, []), metislike_methods))
in
isar_steps outer (SOME l) (step :: accum) infs
end
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_try0.ML Mon Dec 16 12:02:28 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_try0.ML Mon Dec 16 12:26:18 2013 +0100
@@ -1,9 +1,9 @@
(* Title: HOL/Tools/Sledgehammer/sledgehammer_try0.ML
- Author: Jasmin Blanchette, TU Muenchen
Author: Steffen Juilf Smolka, TU Muenchen
+ Author: Jasmin Blanchette, TU Muenchen
-Try replacing calls to metis with calls to other proof methods in order to
-speed up proofs, eliminate dependencies, and repair broken proof steps.
+Try replacing calls to metis with calls to other proof methods to speed up proofs, eliminate
+dependencies, and repair broken proof steps.
*)
signature SLEDGEHAMMER_TRY0 =
@@ -21,15 +21,9 @@
open Sledgehammer_Proof
open Sledgehammer_Preplay
-val variant_methods =
- [Simp_Method, Auto_Method, Arith_Method, Fastforce_Method, Blast_Method, Force_Method,
- Metis_Method, Meson_Method]
-
-fun variants_of_step (Let _) = raise Fail "Sledgehammer_Try0: variants_of_step"
- | variants_of_step (Prove (qs, xs, l, t, subproofs, (facts, meth))) =
- variant_methods
- |> remove (op =) meth
- |> map (fn meth' => Prove (qs, xs, l, t, subproofs, (facts, meth')))
+fun variants_of_step (Prove (qs, xs, l, t, subproofs, (facts, _ :: meths))) =
+ map (fn meth => Prove (qs, xs, l, t, subproofs, (facts, [meth]))) meths
+ | variants_of_step _ = raise Fail "Sledgehammer_Try0: variants_of_step"
val slack = seconds 0.05