# HG changeset patch # User blanchet # Date 1403590762 -7200 # Node ID 68aa585269acbad9d7d3eb4872e25adbd3953d6e # Parent 4868ec62f533baf1ac55ba11b300ce03f0c325a6 given two one-liners, only show the best of the two diff -r 4868ec62f533 -r 68aa585269ac src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Tue Jun 24 08:19:22 2014 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Tue Jun 24 08:19:22 2014 +0200 @@ -117,11 +117,12 @@ val skolem_methods = basic_systematic_methods fun isar_proof_text ctxt debug isar_proofs smt_proofs isar_params - (one_line_params as (_, _, _, _, subgoal, subgoal_count)) = + (one_line_params as ((_, one_line_play), banner, used_facts, minimize_command, subgoal, + subgoal_count)) = let val _ = if debug then Output.urgent_message "Constructing Isar proof..." else () - fun isar_proof_of () = + fun generate_proof_text () = let val (verbose, alt_metis_args, preplay_timeout, compress, try0, minimize, atp_proof, goal) = isar_params () @@ -329,32 +330,42 @@ #> chain_isar_proof #> kill_useless_labels_in_isar_proof #> relabel_isar_proof_nicely) - - val isar_text = string_of_isar_proof ctxt subgoal subgoal_count isar_proof - val msg = - (if verbose then - let val num_steps = add_isar_steps (steps_of_isar_proof isar_proof) 0 in - [string_of_int num_steps ^ " step" ^ plural_s num_steps] - end - else - []) @ - (if do_preplay then [string_of_play_outcome play_outcome] else []) in - "\n\nStructured proof" ^ (commas msg |> not (null msg) ? enclose " (" ")") ^ ":\n" ^ - Active.sendback_markup [Markup.padding_command] isar_text + (case add_isar_steps (steps_of_isar_proof isar_proof) 0 of + 1 => + one_line_proof_text ctxt 0 + (if play_outcome_ord (play_outcome, one_line_play) = LESS then + (case isar_proof of + Proof (_, _, [Prove (_, _, _, _, _, (_, gfs), meth :: _, _)]) => + let val used_facts' = filter (member (op =) gfs o fst) used_facts in + ((meth, play_outcome), banner, used_facts', minimize_command, subgoal, + subgoal_count) + end) + else + one_line_params) ^ + (if isar_proofs = SOME true then "\n(No structured proof available -- proof too simple.)" + else "") + | num_steps => + let + val msg = + (if verbose then [string_of_int num_steps ^ " step" ^ plural_s num_steps] else []) @ + (if do_preplay then [string_of_play_outcome play_outcome] else []) + in + one_line_proof_text ctxt 0 one_line_params ^ + "\n\nStructured proof" ^ (commas msg |> not (null msg) ? enclose " (" ")") ^ ":\n" ^ + Active.sendback_markup [Markup.padding_command] + (string_of_isar_proof ctxt subgoal subgoal_count isar_proof) + end) end - - val one_line_proof = one_line_proof_text ctxt 0 one_line_params - val isar_proof = - if debug then - isar_proof_of () - else - (case try isar_proof_of () of - SOME s => s - | NONE => - if isar_proofs = SOME true then "\nWarning: Isar proof construction failed." else "") in - one_line_proof ^ isar_proof + if debug then + generate_proof_text () + else + (case try generate_proof_text () of + SOME s => s + | NONE => + one_line_proof_text ctxt 0 one_line_params ^ + (if isar_proofs = SOME true then "\nWarning: Isar proof construction failed." else "")) end fun isar_proof_would_be_a_good_idea smt_proofs (meth, play) = diff -r 4868ec62f533 -r 68aa585269ac src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML Tue Jun 24 08:19:22 2014 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML Tue Jun 24 08:19:22 2014 +0200 @@ -251,20 +251,14 @@ fun using_facts [] [] = "" | using_facts ls ss = enclose "using " " " (space_implode " " (map string_of_label ls @ ss)) - fun is_direct_method (Metis_Method _) = true - | is_direct_method Meson_Method = true - | is_direct_method SMT2_Method = true - | is_direct_method Simp_Method = true - | is_direct_method _ = false - (* Local facts are always passed via "using", which affects "meson" and "metis". This is arguably stylistically superior, because it emphasises the structure of the proof. It is also more robust w.r.t. preplay: Preplay is performed before chaining of local facts with "hence" and "thus" is introduced. See also "tac_of_method" in "Sledgehammer_Isar_Preplay". *) - fun of_method command ls ss meth = - let val direct = is_direct_method meth in + fun of_method ls ss meth = + let val direct = is_proof_method_direct meth in using_facts ls (if direct then [] else ss) ^ - command ^ " " ^ string_of_proof_method ctxt (if direct then ss else []) meth + "by " ^ string_of_proof_method ctxt (if direct then ss else []) meth end fun of_free (s, T) = @@ -308,7 +302,7 @@ #> add_str (of_label l) #> add_term t #> add_str (" " ^ - of_method "by" (sort_distinct label_ord ls) (sort_distinct string_ord ss) meth ^ + of_method (sort_distinct label_ord ls) (sort_distinct string_ord ss) meth ^ (if comment = "" then "" else " (* " ^ comment ^ " *)") ^ "\n") and add_steps ind = fold (add_step ind) and of_proof ind ctxt (Proof (xs, assms, steps)) = @@ -319,12 +313,8 @@ |> fst in (if i <> 1 then "prefer " ^ string_of_int i ^ "\n" else "") ^ - (case proof of - Proof (_, _, [Prove (_, _, _, _, [], (_, gfs), meth :: _, _)]) => - of_method (if n = 1 then "by" else "apply") [] gfs meth - | _ => - of_indent 0 ^ "proof -\n" ^ of_proof 1 ctxt proof ^ - of_indent 0 ^ (if n = 1 then "qed" else "next")) + of_indent 0 ^ "proof -\n" ^ of_proof 1 ctxt proof ^ + of_indent 0 ^ (if n = 1 then "qed" else "next") end end; diff -r 4868ec62f533 -r 68aa585269ac src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML Tue Jun 24 08:19:22 2014 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML Tue Jun 24 08:19:22 2014 +0200 @@ -33,6 +33,7 @@ type one_line_params = (proof_method * play_outcome) * string * (string * stature) list * minimize_command * int * int + val is_proof_method_direct : proof_method -> bool val string_of_proof_method : Proof.context -> string list -> proof_method -> string val tac_of_proof_method : Proof.context -> thm list * thm list -> proof_method -> int -> tactic val string_of_play_outcome : play_outcome -> string @@ -71,6 +72,12 @@ type one_line_params = (proof_method * play_outcome) * string * (string * stature) list * minimize_command * int * int +fun is_proof_method_direct (Metis_Method _) = true + | is_proof_method_direct Meson_Method = true + | is_proof_method_direct SMT2_Method = true + | is_proof_method_direct Simp_Method = true + | is_proof_method_direct _ = false + fun maybe_paren s = s |> not (Symbol_Pos.is_identifier s) ? enclose "(" ")" fun string_of_proof_method ctxt ss meth = @@ -136,12 +143,14 @@ fun apply_on_subgoal _ 1 = "by " | apply_on_subgoal 1 _ = "apply " - | apply_on_subgoal i n = - "prefer " ^ string_of_int i ^ " " ^ apply_on_subgoal 1 n + | apply_on_subgoal i n = "prefer " ^ string_of_int i ^ " " ^ apply_on_subgoal 1 n (* FIXME *) fun proof_method_command ctxt meth i n _(*used_chaineds*) _(*num_chained*) ss = - apply_on_subgoal i n ^ string_of_proof_method ctxt ss meth + let val (indirect_ss, direct_ss) = if is_proof_method_direct meth then ([], ss) else (ss, []) in + (if null indirect_ss then "" else "using " ^ space_implode " " indirect_ss ^ " ") ^ + apply_on_subgoal i n ^ string_of_proof_method ctxt direct_ss meth + end fun try_command_line banner play command = let val s = string_of_play_outcome play in