# HG changeset patch # User blanchet # Date 1387191748 -3600 # Node ID b05b0ea063061c03dbc6d449d4871b3a54645fe8 # Parent 1c9ef5c834e8e933037079c68e6b732af475325f tuning diff -r 1c9ef5c834e8 -r b05b0ea06306 src/HOL/Tools/Sledgehammer/sledgehammer_preplay.ML --- 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 *) diff -r 1c9ef5c834e8 -r b05b0ea06306 src/HOL/Tools/Sledgehammer/sledgehammer_print.ML --- 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 ^ diff -r 1c9ef5c834e8 -r b05b0ea06306 src/HOL/Tools/Sledgehammer/sledgehammer_proof.ML --- 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) diff -r 1c9ef5c834e8 -r b05b0ea06306 src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML --- 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) = diff -r 1c9ef5c834e8 -r b05b0ea06306 src/HOL/Tools/Sledgehammer/sledgehammer_try0.ML --- 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))) =