# HG changeset patch # User blanchet # Date 1387193178 -3600 # Node ID 6ac273f176cde7fc5618533e25143c3c8fe0d811 # Parent b05b0ea063061c03dbc6d449d4871b3a54645fe8 store alternative proof methods in Isar data structure diff -r b05b0ea06306 -r 6ac273f176cd src/HOL/Tools/Sledgehammer/sledgehammer_preplay.ML --- 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 diff -r b05b0ea06306 -r 6ac273f176cd src/HOL/Tools/Sledgehammer/sledgehammer_print.ML --- 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 ^ diff -r b05b0ea06306 -r 6ac273f176cd src/HOL/Tools/Sledgehammer/sledgehammer_proof.ML --- 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 diff -r b05b0ea06306 -r 6ac273f176cd src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML --- 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 diff -r b05b0ea06306 -r 6ac273f176cd src/HOL/Tools/Sledgehammer/sledgehammer_try0.ML --- 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