# HG changeset patch # User blanchet # Date 1391370831 -3600 # Node ID 12e1a5d8ee48811d003e495b371d13ba22e26304 # Parent 66709d41601e52d1101ea0c36ffc930b3d07b7ee simplified data structure -- eliminated distinction between 'first-class' and 'second-class' proof methods diff -r 66709d41601e -r 12e1a5d8ee48 src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML --- 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 diff -r 66709d41601e -r 12e1a5d8ee48 src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML --- 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) diff -r 66709d41601e -r 12e1a5d8ee48 src/HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML --- 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) diff -r 66709d41601e -r 12e1a5d8ee48 src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML --- 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 diff -r 66709d41601e -r 12e1a5d8ee48 src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML --- 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 ^ diff -r 66709d41601e -r 12e1a5d8ee48 src/HOL/Tools/Sledgehammer/sledgehammer_isar_try0.ML --- 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