simplified data structure -- eliminated distinction between 'first-class' and 'second-class' proof methods
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Sun Feb 02 20:53:51 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Sun Feb 02 20:53:51 2014 +0100
@@ -110,16 +110,16 @@
type isar_params =
bool * string * string * Time.time * real * bool * (term, string) atp_step list * thm
-val arith_methodss =
- [[Arith_Method, Simp_Method, Auto_Method, Fastforce_Method, Blast_Method, Force_Method,
- Algebra_Method], [Metis_Method], [Meson_Method]]
-val datatype_methodss = [[Simp_Method], [Simp_Size_Method]]
-val metislike_methodss =
- [[Metis_Method, Simp_Method, Auto_Method, Arith_Method, Blast_Method, Fastforce_Method,
- Force_Method, Algebra_Method], [Meson_Method]]
-val rewrite_methodss =
- [[Auto_Method, Simp_Method, Fastforce_Method, Force_Method, Metis_Method], [Meson_Method]]
-val skolem_methodss = [[Metis_Method, Blast_Method], [Meson_Method]]
+val arith_methods =
+ [Arith_Method, Simp_Method, Auto_Method, Fastforce_Method, Blast_Method, Force_Method,
+ Algebra_Method, Metis_Method, Meson_Method]
+val datatype_methods = [Simp_Method, Simp_Size_Method]
+val metislike_methods =
+ [Metis_Method, Simp_Method, Auto_Method, Arith_Method, Blast_Method, Fastforce_Method,
+ Force_Method, Algebra_Method, Meson_Method]
+val rewrite_methods =
+ [Auto_Method, Simp_Method, Fastforce_Method, Force_Method, Metis_Method, Meson_Method]
+val skolem_methods = [Metis_Method, Blast_Method, Meson_Method]
fun isar_proof_text ctxt debug isar_proofs isar_params
(one_line_params as (_, _, _, _, subgoal, subgoal_count)) =
@@ -158,12 +158,12 @@
map_filter (get_role (curry (op =) Lemma)) atp_proof
|> map (fn ((l, t), rule) =>
let
- val (skos, methss) =
- if is_skolemize_rule rule then (skolems_of t, skolem_methodss)
- else if is_arith_rule rule then ([], arith_methodss)
- else ([], rewrite_methodss)
+ 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, [], (([], []), methss))
+ Prove ([], skos, l, t, [], (([], []), meths))
end)
val bot = atp_proof |> List.last |> #1
@@ -212,7 +212,7 @@
accum
|> (if tainted = [] then
cons (Prove (if outer then [Show] else [], [], no_label, concl_t, [],
- ((the_list predecessor, []), metislike_methodss)))
+ ((the_list predecessor, []), metislike_methods)))
else
I)
|> rev
@@ -227,18 +227,18 @@
fun do_rest l step = isar_steps outer (SOME l) (step :: accum) infs
val deps = fold add_fact_of_dependencies gamma no_facts
- val methss =
- if is_arith_rule rule then arith_methodss
- else if is_datatype_rule rule then datatype_methodss
- else metislike_methodss
- val by = (deps, methss)
+ val meths =
+ if is_arith_rule rule then arith_methods
+ else if is_datatype_rule rule then datatype_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, skolem_methodss)] infs
+ isar_steps outer (SOME l) [prove [subproof] (no_facts, skolem_methods)] infs
end
else
do_rest l (prove [] by)
@@ -256,7 +256,7 @@
val step =
Prove (maybe_show outer c [], [], l, t,
map isar_case (filter_out (null o snd) cases),
- ((the_list predecessor, []), metislike_methodss))
+ ((the_list predecessor, []), metislike_methods))
in
isar_steps outer (SOME l) (step :: accum) infs
end
@@ -286,7 +286,7 @@
fun str_of_meth l meth =
string_of_proof_method meth ^ " " ^ str_of_preplay_outcome (preplay_outcome l meth)
- fun comment_of l = map (map (str_of_meth l)) #> map commas #> space_implode "; "
+ fun comment_of l = map (str_of_meth l) #> commas
fun trace_isar_proof label proof =
if trace then
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML Sun Feb 02 20:53:51 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML Sun Feb 02 20:53:51 2014 +0100
@@ -79,15 +79,14 @@
| _ => raise Fail "Sledgehammer_Isar_Compress: update_steps")
end
-(* Tries merging the first step into the second step.
- FIXME: Arbitrarily picks the second step's method. *)
-fun try_merge (Prove (_, [], lbl1, _, [], ((lfs1, gfs1), _)))
- (Prove (qs2, fix, lbl2, t, subproofs, ((lfs2, gfs2), methss2))) =
+(* Tries merging the first step into the second step. *)
+fun try_merge (Prove (_, [], lbl1, _, [], ((lfs1, gfs1), meths1)))
+ (Prove (qs2, fix, lbl2, t, subproofs, ((lfs2, gfs2), meths2))) =
let
val lfs = remove (op =) lbl1 lfs2 |> union (op =) lfs1
val gfs = union (op =) gfs1 gfs2
in
- SOME (Prove (qs2, fix, lbl2, t, subproofs, ((lfs, gfs), methss2)))
+ SOME (Prove (qs2, fix, lbl2, t, subproofs, ((lfs, gfs), meths2)))
end
| try_merge _ _ = NONE
@@ -136,16 +135,16 @@
end
(* elimination of trivial, one-step subproofs *)
- fun elim_subproofs' time qs fix l t lfs gfs (methss as (meth :: _) :: _) subs nontriv_subs =
+ fun elim_subproofs' time qs fix l t lfs gfs (meths as meth :: _) subs nontriv_subs =
if null subs orelse not (compress_further ()) then
(set_preplay_outcome l meth (Played time);
- Prove (qs, fix, l, t, List.revAppend (nontriv_subs, subs), ((lfs, gfs), methss)))
+ Prove (qs, fix, l, t, List.revAppend (nontriv_subs, subs), ((lfs, gfs), meths)))
else
(case subs of
(sub as Proof (_, assms, sub_steps)) :: subs =>
(let
(* trivial subproofs have exactly one "Prove" step *)
- val SOME (Prove (_, [], l', _, [], ((lfs', gfs'), (meth' :: _) :: _))) =
+ val SOME (Prove (_, [], l', _, [], ((lfs', gfs'), meth' :: _))) =
try the_single sub_steps
(* only touch proofs that can be preplayed sucessfully *)
@@ -155,7 +154,7 @@
val subs'' = subs @ nontriv_subs
val lfs'' = union (op =) lfs (subtract (op =) (map fst assms) lfs')
val gfs'' = union (op =) gfs' gfs
- val by = ((lfs'', gfs''), methss(*FIXME*))
+ val by = ((lfs'', gfs''), meths(*FIXME*))
val step'' = Prove (qs, fix, l, t, subs'', by)
(* check if the modified step can be preplayed fast enough *)
@@ -164,20 +163,20 @@
in
decrement_step_count (); (* l' successfully eliminated! *)
map (replace_successor l' [l]) lfs';
- elim_subproofs' time'' qs fix l t lfs'' gfs'' methss subs nontriv_subs
+ elim_subproofs' time'' qs fix l t lfs'' gfs'' meths subs nontriv_subs
end
handle Bind =>
- elim_subproofs' time qs fix l t lfs gfs methss subs (sub :: nontriv_subs))
+ elim_subproofs' time qs fix l t lfs gfs meths subs (sub :: nontriv_subs))
| _ => raise Fail "Sledgehammer_Isar_Compress: elim_subproofs'")
fun elim_subproofs (step as Let _) = step
| elim_subproofs (step as Prove (qs, fix, l, t, subproofs,
- ((lfs, gfs), methss as (meth :: _) :: _))) =
+ ((lfs, gfs), meths as meth :: _))) =
if subproofs = [] then
step
else
(case Lazy.force (preplay_outcome l meth) of
- Played time => elim_subproofs' time qs fix l t lfs gfs methss subproofs []
+ Played time => elim_subproofs' time qs fix l t lfs gfs meths subproofs []
| _ => step)
(** top_level compression: eliminate steps by merging them into their successors **)
@@ -211,11 +210,10 @@
fun try_eliminate (i, l, _) succ_lbls steps =
let
- val ((cand as Prove (_, _, l, _, _, ((lfs, _), (meth :: _) :: _))) :: steps') =
- drop i steps
+ val ((cand as Prove (_, _, l, _, _, ((lfs, _), meth :: _))) :: steps') = drop i steps
val succs = collect_successors steps' succ_lbls
- val succ_meths = map (hd o hd o snd o the o byline_of_isar_step) succs
+ val succ_meths = map (hd o snd o the o byline_of_isar_step) succs
(* only touch steps that can be preplayed successfully *)
val Played time = Lazy.force (preplay_outcome l meth)
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML Sun Feb 02 20:53:51 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML Sun Feb 02 20:53:51 2014 +0100
@@ -28,11 +28,11 @@
fun minimize_isar_step_dependencies (_ : isar_preplay_data) (step as Let _) = step
| minimize_isar_step_dependencies
{reset_preplay_outcomes, set_preplay_outcome, preplay_outcome, preplay_quietly, ...}
- (step as Prove (qs, xs, l, t, subproofs, ((lfs, gfs), methss as (meth :: _) :: _))) =
+ (step as Prove (qs, xs, l, t, subproofs, ((lfs, gfs), meths as meth :: _))) =
(case Lazy.force (preplay_outcome l meth) of
Played time =>
let
- fun mk_step_lfs_gfs lfs gfs = Prove (qs, xs, l, t, subproofs, ((lfs, gfs), methss))
+ fun mk_step_lfs_gfs lfs gfs = Prove (qs, xs, l, t, subproofs, ((lfs, gfs), meths))
val mk_step_gfs_lfs = curry (swap #> uncurry mk_step_lfs_gfs)
fun minimize_facts _ time min_facts [] = (time, min_facts)
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML Sun Feb 02 20:53:51 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML Sun Feb 02 20:53:51 2014 +0100
@@ -210,15 +210,15 @@
Play_Failed)
(* preplay steps treating exceptions like timeouts *)
- fun preplay_quietly timeout (step as Prove (_, _, _, _, _, (_, (meth :: _) :: _))) =
+ fun preplay_quietly timeout (step as Prove (_, _, _, _, _, (_, meth :: _))) =
preplay true timeout meth step
| preplay_quietly _ _ = Played Time.zeroTime
val preplay_tab = Unsynchronized.ref Canonical_Label_Tab.empty
- fun reset_preplay_outcomes (step as Prove (_, _, l, _, _, (_, methss))) =
- preplay_tab := Canonical_Label_Tab.update (l, maps (map (fn meth =>
- (meth, Lazy.lazy (fn () => preplay false preplay_timeout meth step)))) methss)
+ fun reset_preplay_outcomes (step as Prove (_, _, l, _, _, (_, meths))) =
+ preplay_tab := Canonical_Label_Tab.update (l, map (fn meth =>
+ (meth, Lazy.lazy (fn () => preplay false preplay_timeout meth step))) meths)
(!preplay_tab)
| reset_preplay_outcomes _ = ()
@@ -236,7 +236,7 @@
val _ = fold_isar_steps (K o reset_preplay_outcomes) (steps_of_proof proof) ()
- fun result_of_step (Prove (_, _, l, _, _, (_, (meth :: _) :: _))) =
+ fun result_of_step (Prove (_, _, l, _, _, (_, meth :: _))) =
Lazy.force (preplay_outcome l meth)
| result_of_step _ = Played Time.zeroTime
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML Sun Feb 02 20:53:51 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML Sun Feb 02 20:53:51 2014 +0100
@@ -22,7 +22,7 @@
and isar_step =
Let of term * term |
Prove of isar_qualifier list * (string * typ) list * label * term * isar_proof list *
- (facts * proof_method list list)
+ (facts * proof_method list)
val no_label : label
val no_facts : facts
@@ -35,7 +35,7 @@
val steps_of_proof : isar_proof -> isar_step list
val label_of_isar_step : isar_step -> label option
- val byline_of_isar_step : isar_step -> (facts * proof_method list list) option
+ val byline_of_isar_step : isar_step -> (facts * proof_method list) option
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
@@ -51,7 +51,7 @@
val relabel_isar_proof_finally : isar_proof -> isar_proof
val string_of_isar_proof : Proof.context -> string -> string -> int -> int ->
- (label -> proof_method list list -> string) -> isar_proof -> string
+ (label -> proof_method list -> string) -> isar_proof -> string
end;
structure Sledgehammer_Isar_Proof : SLEDGEHAMMER_ISAR_PROOF =
@@ -79,7 +79,7 @@
and isar_step =
Let of term * term |
Prove of isar_qualifier list * (string * typ) list * label * term * isar_proof list *
- (facts * proof_method list list)
+ (facts * proof_method list)
val no_label = ("", ~1)
val no_facts = ([],[])
@@ -136,9 +136,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_isar_step lbl (Prove (qs, xs, l, t, subproofs, ((lfs, gfs), methss))) =
+fun chain_isar_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, map chain_isar_proof subproofs, ((lfs, gfs), methss))
+ Prove (qs' @ qs, xs, l, t, map chain_isar_proof subproofs, ((lfs, gfs), meths))
end
| chain_isar_step _ step = step
and chain_isar_steps _ [] = []
@@ -340,7 +340,7 @@
add_str (of_indent ind ^ "let ")
#> add_term t1 #> add_str " = " #> add_term t2
#> add_str "\n"
- | add_step ind (Prove (qs, xs, l, t, subproofs, ((ls, ss), methss as (meth :: _) :: _))) =
+ | add_step ind (Prove (qs, xs, l, t, subproofs, ((ls, ss), meths as meth :: _))) =
add_step_pre ind qs subproofs
#> (case xs of
[] => add_str (of_have qs (length subproofs) ^ " ")
@@ -350,7 +350,7 @@
#> add_term t
#> add_str (" " ^
of_method (sort_distinct label_ord ls) (sort_distinct string_ord ss) meth ^
- (case comment_of l methss of
+ (case comment_of l meths of
"" => ""
| comment => " (* " ^ comment ^ " *)") ^ "\n")
and add_steps ind = fold (add_step ind)
@@ -360,7 +360,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 (_, [], _, _, [], (_, (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_isar_try0.ML Sun Feb 02 20:53:51 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_try0.ML Sun Feb 02 20:53:51 2014 +0100
@@ -22,8 +22,8 @@
open Sledgehammer_Isar_Proof
open Sledgehammer_Isar_Preplay
-fun variants_of_step (Prove (qs, xs, l, t, subproofs, (facts, methss))) =
- map (fn meth => Prove (qs, xs, l, t, subproofs, (facts, [[meth]]))) (tl (flat methss))
+fun variants_of_step (Prove (qs, xs, l, t, subproofs, (facts, meths))) =
+ map (fn meth => Prove (qs, xs, l, t, subproofs, (facts, [meth]))) (tl meths)
| variants_of_step _ = raise Fail "Sledgehammer_Isar_Try0: variants_of_step"
val slack = seconds 0.05
@@ -31,7 +31,7 @@
fun try0_step _ _ (step as Let _) = step
| try0_step preplay_timeout
({preplay_outcome, set_preplay_outcome, preplay_quietly, ...} : isar_preplay_data)
- (step as Prove (_, _, l, _, _, (_, (meth :: _) :: _))) =
+ (step as Prove (_, _, l, _, _, (_, meth :: _))) =
let
val timeout =
(case Lazy.force (preplay_outcome l meth) of
@@ -45,7 +45,7 @@
in
(* FIXME: create variant after success *)
(case Par_List.get_some try_variant (variants_of_step step) of
- SOME (step' as Prove (_, _, _, _, _, (_, (meth' :: _) :: _)), result) =>
+ SOME (step' as Prove (_, _, _, _, _, (_, meth' :: _)), result) =>
(set_preplay_outcome l meth' result; step')
| NONE => step)
end