--- a/src/HOL/Tools/Sledgehammer/sledgehammer_preplay.ML Mon Dec 16 09:48:26 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_preplay.ML Mon Dec 16 12:02:28 2013 +0100
@@ -104,17 +104,17 @@
fun tac_of_method method type_enc lam_trans ctxt facts =
(case method of
- MetisM => Metis_Tactic.metis_tac [type_enc] lam_trans ctxt facts
- | MesonM => Meson.meson_tac ctxt facts
+ 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
- SimpM => Simplifier.asm_full_simp_tac ctxt
- | AutoM => K (Clasimp.auto_tac ctxt)
- | FastforceM => Clasimp.fast_force_tac ctxt
- | ForceM => Clasimp.force_tac ctxt
- | ArithM => Arith_Data.arith_tac ctxt
- | BlastM => blast_tac ctxt
+ Simp_Method => Simplifier.asm_full_simp_tac 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
| _ => raise Fail "Sledgehammer_Preplay: tac_of_method"))
(* main function for preplaying Isar steps; may throw exceptions *)
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_print.ML Mon Dec 16 09:48:26 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_print.ML Mon Dec 16 12:02:28 2013 +0100
@@ -174,20 +174,20 @@
fun by_method meth = "by " ^
(case meth of
- SimpM => "simp"
- | AutoM => "auto"
- | FastforceM => "fastforce"
- | ForceM => "force"
- | ArithM => "arith"
- | BlastM => "blast"
- | MesonM => "meson"
+ Simp_Method => "simp"
+ | Auto_Method => "auto"
+ | Fastforce_Method => "fastforce"
+ | Force_Method => "force"
+ | Arith_Method => "arith"
+ | Blast_Method => "blast"
+ | Meson_Method => "meson"
| _ => raise Fail "Sledgehammer_Print: by_method")
fun using_facts [] [] = ""
| using_facts ls ss =
"using " ^ space_implode " " (map string_of_label ls @ ss) ^ " "
- fun of_method ls ss MetisM =
+ fun of_method ls ss Metis_Method =
reconstructor_command (Metis (type_enc, lam_trans)) 1 1 [] 0 (ls, ss)
| of_method ls ss meth = using_facts ls ss ^ by_method meth
@@ -254,21 +254,16 @@
| 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_step_post ind l t facts meth ""
+ add_step_pre ind qs subproofs
+ #> add_suffix (of_prove qs (length subproofs) ^ " ")
+ #> add_step_post ind l t facts meth ""
| _ => (* obtain *)
- add_step_pre ind qs subproofs
- #> add_suffix (of_obtain qs (length subproofs) ^ " ")
- #> add_frees xs
- #> add_suffix " where "
- (* The new skolemizer puts the arguments in the same order as the ATPs (E and Vampire --
- but see also "atp_proof_reconstruct.ML" regarding Vampire). *)
- #> add_step_post ind l t facts meth
- (if use_metis_new_skolem step then
- "using [[metis_new_skolem]] "
- else
- ""))
+ add_step_pre ind qs subproofs
+ #> add_suffix (of_obtain qs (length subproofs) ^ " ")
+ #> 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 ""))
and add_steps ind = fold (add_step ind)
@@ -278,7 +273,7 @@
(* 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 (_, [], _, _, [], (_, MetisM))]) => ""
+ | 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 09:48:26 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof.ML Mon Dec 16 12:02:28 2013 +0100
@@ -20,14 +20,8 @@
Prove of isar_qualifier list * (string * typ) list * label * term * isar_proof list *
(facts * proof_method)
and proof_method =
- MetisM |
- SimpM |
- AutoM |
- FastforceM |
- ForceM |
- ArithM |
- BlastM |
- MesonM
+ Metis_Method | Simp_Method | Auto_Method | Fastforce_Method | Force_Method | Arith_Method |
+ Blast_Method | Meson_Method
val no_label : label
val no_facts : facts
@@ -49,8 +43,7 @@
val use_metis_new_skolem : isar_step -> bool
val fold_isar_step : (isar_step -> 'a -> 'a) -> isar_step -> 'a -> 'a
- val fold_isar_steps :
- (isar_step -> 'a -> 'a) -> isar_step list -> 'a -> 'a
+ val fold_isar_steps : (isar_step -> 'a -> 'a) -> isar_step list -> 'a -> 'a
val map_isar_steps : (isar_step -> isar_step) -> isar_proof -> isar_proof
@@ -78,14 +71,8 @@
Prove of isar_qualifier list * (string * typ) list * label * term * isar_proof list *
(facts * proof_method)
and proof_method =
- MetisM |
- SimpM |
- AutoM |
- FastforceM |
- ForceM |
- ArithM |
- BlastM |
- MesonM
+ Metis_Method | Simp_Method | Auto_Method | Fastforce_Method | Force_Method | Arith_Method |
+ Blast_Method | Meson_Method
val no_label = ("", ~1)
val no_facts = ([],[])
@@ -112,24 +99,25 @@
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))) =
- meth = MetisM andalso exists (fn (_, T) => length (binder_types T) > 1) xs
+ meth = Metis_Method andalso exists (fn (_, T) => length (binder_types T) > 1) xs
| use_metis_new_skolem _ = false
fun fold_isar_steps f = fold (fold_isar_step f)
-and fold_isar_step f step s =
- fold (steps_of_proof #> fold_isar_steps f)
- (these (subproofs_of_step step)) s
- |> f step
+and fold_isar_step f step =
+ fold (steps_of_proof #> fold_isar_steps f) (these (subproofs_of_step step))
+ #> f step
-fun map_isar_steps f proof =
+fun map_isar_steps f =
let
fun do_proof (Proof (fix, assms, steps)) = Proof (fix, assms, map do_step steps)
and do_step (step as Let _) = f step
| do_step (Prove (qs, xs, l, t, subproofs, by)) =
f (Prove (qs, xs, l, t, map do_proof subproofs, by))
in
- do_proof proof
+ do_proof
end
val add_proof_steps = fold_isar_steps (fn Prove _ => Integer.add 1 | _ => I)
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Mon Dec 16 09:48:26 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Mon Dec 16 12:02:28 2013 +0100
@@ -288,9 +288,9 @@
|> map (fn ((l, t), rule) =>
let
val (skos, meth) =
- if is_skolemize_rule rule then (skolems_of t, MetisM)
- else if is_arith_rule rule then ([], ArithM)
- else ([], AutoM)
+ if is_skolemize_rule rule then (skolems_of t, Metis_Method)
+ else if is_arith_rule rule then ([], Arith_Method)
+ else ([], Auto_Method)
in
Prove ([], skos, l, t, [], (([], []), meth))
end)
@@ -340,7 +340,7 @@
accum
|> (if tainted = [] then
cons (Prove (if outer then [Show] else [], [], no_label, concl_t, [],
- ((the_list predecessor, []), MetisM)))
+ ((the_list predecessor, []), Metis_Method)))
else
I)
|> rev
@@ -355,7 +355,7 @@
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 ArithM else MetisM
+ val meth = if is_arith_rule rule then Arith_Method else Metis_Method
val by = (deps, meth)
in
if is_clause_tainted c then
@@ -363,15 +363,13 @@
[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, MetisM)] []
+ isar_steps outer (SOME l) [prove [subproof] (no_facts, Metis_Method)] []
end
else
do_rest l (prove [] by)
| _ => do_rest l (prove [] by))
else
- (if skolem then Prove ([], skolems_of t, l, t, [], by)
- else prove [] by)
- |> do_rest l
+ do_rest l (if skolem then Prove ([], skolems_of t, l, t, [], by) else prove [] by)
end
| isar_steps outer predecessor accum (Cases cases :: infs) =
let
@@ -383,14 +381,14 @@
val step =
Prove (maybe_show outer c [], [], l, t,
map isar_case (filter_out (null o snd) cases),
- ((the_list predecessor, []), MetisM))
+ ((the_list predecessor, []), Metis_Method))
in
isar_steps outer (SOME l) (step :: accum) infs
end
and isar_proof outer fix assms lems infs =
Proof (fix, assms, lems @ isar_steps outer NONE [] infs)
- (* 60 seconds seems like a good interpreation of "no timeout" *)
+ (* 60 seconds seems like a reasonable interpreation of "no timeout" *)
val preplay_timeout = preplay_timeout |> the_default (seconds 60.0)
val (preplay_interface as {overall_preplay_stats, ...}, isar_proof) =
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_try0.ML Mon Dec 16 09:48:26 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_try0.ML Mon Dec 16 12:02:28 2013 +0100
@@ -21,7 +21,9 @@
open Sledgehammer_Proof
open Sledgehammer_Preplay
-val variant_methods = [SimpM, AutoM, ArithM, FastforceM, BlastM, ForceM, MetisM, MesonM]
+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))) =