# HG changeset patch # User blanchet # Date 1269881064 -7200 # Node ID cdc6855a63871aa692973d69413d8b016dbd44b9 # Parent 194cb6e3c13f560063d7957eb7616ef4c7dc2109 make Sledgehammer output "by" vs. "apply", "qed" vs. "next", and any necessary "prefer" diff -r 194cb6e3c13f -r cdc6855a6387 src/HOL/Tools/ATP_Manager/atp_manager.ML --- a/src/HOL/Tools/ATP_Manager/atp_manager.ML Mon Mar 29 15:50:18 2010 +0200 +++ b/src/HOL/Tools/ATP_Manager/atp_manager.ML Mon Mar 29 18:44:24 2010 +0200 @@ -54,7 +54,8 @@ structure ATP_Manager : ATP_MANAGER = struct -type relevance_override = Sledgehammer_Fact_Filter.relevance_override +open Sledgehammer_Fact_Filter +open Sledgehammer_Proof_Reconstruct (** parameters, problems, results, and provers **) @@ -322,6 +323,7 @@ | SOME prover => let val {context = ctxt, facts, goal} = Proof.goal proof_state; + val n = Logic.count_prems (prop_of goal) val desc = "ATP " ^ quote name ^ " for subgoal " ^ string_of_int i ^ ":\n" ^ Syntax.string_of_term ctxt (Thm.term_of (Thm.cprem_of goal i)); @@ -334,9 +336,8 @@ relevance_override = relevance_override, axiom_clauses = NONE, filtered_clauses = NONE} val message = #message (prover params timeout problem) - handle Sledgehammer_HOL_Clause.TRIVIAL => (* FIXME !? *) - "Try this command: " ^ - Markup.markup Markup.sendback "by metis" ^ "." + handle Sledgehammer_HOL_Clause.TRIVIAL => + metis_line i n [] | ERROR msg => ("Error: " ^ msg); val _ = unregister message (Thread.self ()); in () end); diff -r 194cb6e3c13f -r cdc6855a6387 src/HOL/Tools/ATP_Manager/atp_minimal.ML --- a/src/HOL/Tools/ATP_Manager/atp_minimal.ML Mon Mar 29 15:50:18 2010 +0200 +++ b/src/HOL/Tools/ATP_Manager/atp_minimal.ML Mon Mar 29 18:44:24 2010 +0200 @@ -14,7 +14,7 @@ val linear_minimize : 'a minimize_fun val binary_minimize : 'a minimize_fun val minimize_theorems : - params -> (string * thm list) minimize_fun -> prover -> string + params -> (string * thm list) minimize_fun -> prover -> string -> int -> Proof.state -> (string * thm list) list -> (string * thm list) list option * string end; @@ -23,6 +23,7 @@ struct open Sledgehammer_Fact_Preprocessor +open Sledgehammer_Proof_Reconstruct open ATP_Manager type 'a minimize_fun = ('a list -> bool) -> 'a list -> 'a list @@ -111,7 +112,7 @@ (* wrapper for calling external prover *) fun sledgehammer_test_theorems (params as {full_types, ...} : params) prover - timeout subgoalno state filtered name_thms_pairs = + timeout subgoal state filtered name_thms_pairs = let val _ = priority ("Testing " ^ string_of_int (length name_thms_pairs) ^ " theorems... ") @@ -119,7 +120,7 @@ val axclauses = cnf_rules_pairs (Proof.theory_of state) name_thm_pairs val {context = ctxt, facts, goal} = Proof.goal state val problem = - {subgoal = subgoalno, goal = (ctxt, (facts, goal)), + {subgoal = subgoal, goal = (ctxt, (facts, goal)), relevance_override = {add = [], del = [], only = false}, axiom_clauses = SOME axclauses, filtered_clauses = filtered} val (result, proof) = produce_answer (prover params timeout problem) @@ -130,7 +131,7 @@ (* minimalization of thms *) fun minimize_theorems (params as {minimize_timeout, ...}) gen_min prover - prover_name state name_thms_pairs = + prover_name i state name_thms_pairs = let val msecs = Time.toMilliseconds minimize_timeout val _ = @@ -138,9 +139,10 @@ " theorems, ATP: " ^ prover_name ^ ", time limit: " ^ string_of_int msecs ^ " ms") val test_thms_fun = - sledgehammer_test_theorems params prover minimize_timeout 1 state + sledgehammer_test_theorems params prover minimize_timeout i state fun test_thms filtered thms = case test_thms_fun filtered thms of (Success _, _) => true | _ => false + val n = state |> Proof.raw_goal |> #goal |> prop_of |> Logic.count_prems in (* try prove first to check result and get used theorems *) (case test_thms_fun NONE name_thms_pairs of @@ -157,13 +159,7 @@ val min_names = sort_distinct string_ord (map fst min_thms) val _ = priority (cat_lines ["Minimal " ^ string_of_int (length min_thms) ^ " theorems"]) - in - (SOME min_thms, - "Try this command: " ^ - Markup.markup Markup.sendback - ("by (metis " ^ space_implode " " min_names ^ ")") - ^ ".") - end + in (SOME min_thms, metis_line i n min_names) end | (Timeout, _) => (NONE, "Timeout: You may need to increase the time limit of " ^ string_of_int msecs ^ " ms. Invoke \"atp_minimize [time=...]\".") @@ -172,8 +168,7 @@ | (Failure, _) => (NONE, "Failure: No proof with the theorems supplied")) handle Sledgehammer_HOL_Clause.TRIVIAL => - (SOME [], "Trivial: Try this command: " ^ - Markup.markup Markup.sendback "by metis" ^ ".") + (SOME [], metis_line i n []) | ERROR msg => (NONE, "Error: " ^ msg) end diff -r 194cb6e3c13f -r cdc6855a6387 src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML Mon Mar 29 15:50:18 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML Mon Mar 29 18:44:24 2010 +0200 @@ -80,6 +80,8 @@ structure Sledgehammer_FOL_Clause : SLEDGEHAMMER_FOL_CLAUSE = struct +open Sledgehammer_Util + val schematic_var_prefix = "V_"; val fixed_var_prefix = "v_"; @@ -184,8 +186,7 @@ solved in 3.7 and perhaps in earlier versions too.) *) (* 32-bit hash, so we expect no collisions. *) fun controlled_length dfg s = - if dfg andalso size s > 60 then Word.toString (hashw_string (s, 0w0)) - else s; + if dfg andalso size s > 60 then Word.toString (hashw_string (s, 0w0)) else s; fun lookup_const dfg c = case Symtab.lookup const_trans_table c of diff -r 194cb6e3c13f -r cdc6855a6387 src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Mon Mar 29 15:50:18 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Mon Mar 29 18:44:24 2010 +0200 @@ -144,7 +144,7 @@ fun get_params thy = extract_params thy (default_raw_params thy) fun default_params thy = get_params thy o map (apsnd single) -fun atp_minimize_command override_params old_style_args fact_refs state = +fun atp_minimize_command override_params old_style_args i fact_refs state = let val thy = Proof.theory_of state val ctxt = Proof.context_of state @@ -176,7 +176,7 @@ | NONE => error ("Unknown ATP: " ^ quote atp)) val name_thms_pairs = theorems_from_refs ctxt fact_refs in - writeln (#2 (minimize_theorems params linear_minimize prover atp state + writeln (#2 (minimize_theorems params linear_minimize prover atp i state name_thms_pairs)) end @@ -202,7 +202,8 @@ sledgehammer (get_params thy override_params) (the_default 1 opt_i) relevance_override state else if subcommand = minimizeN then - atp_minimize_command override_params [] (#add relevance_override) state + atp_minimize_command override_params [] (the_default 1 opt_i) + (#add relevance_override) state else if subcommand = messagesN then messages opt_i else if subcommand = available_atpsN then @@ -287,7 +288,7 @@ "minimize theorem list with external prover" K.diag (parse_minimize_args -- parse_fact_refs >> (fn (args, fact_refs) => Toplevel.no_timing o Toplevel.unknown_proof o - Toplevel.keep (atp_minimize_command [] args fact_refs + Toplevel.keep (atp_minimize_command [] args 1 fact_refs o Toplevel.proof_of))) val _ = diff -r 194cb6e3c13f -r cdc6855a6387 src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Mon Mar 29 15:50:18 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Mon Mar 29 18:44:24 2010 +0200 @@ -14,6 +14,7 @@ val strip_prefix: string -> string -> string option val setup: theory -> theory val is_proof_well_formed: string -> bool + val metis_line: int -> int -> string list -> string val metis_lemma_list: bool -> string -> string * string vector * (int * int) * Proof.context * thm * int -> string * string list val structured_isar_proof: string -> @@ -427,12 +428,15 @@ stringify_deps thm_names ((lno,lname)::deps_map) lines end; -val proofstart = "proof (neg_clausify)\n"; +fun isar_proof_start i = + (if i = 1 then "" else "prefer " ^ string_of_int i ^ "\n") ^ + "proof (neg_clausify)\n"; +fun isar_fixes [] = "" + | isar_fixes ts = " fix " ^ space_implode " " ts ^ "\n"; +fun isar_proof_end 1 = "qed" + | isar_proof_end _ = "next" -fun isar_header [] = proofstart - | isar_header ts = proofstart ^ "fix " ^ space_implode " " ts ^ "\n"; - -fun isar_proof_from_tstp_file cnfs ctxt th sgno thm_names = +fun isar_proof_from_tstp_file cnfs ctxt goal i thm_names = let val _ = trace_proof_msg (K "\nisar_proof_from_tstp_file: start\n") val tuples = map (dest_tstp o tstp_line o explode) cnfs @@ -448,7 +452,7 @@ val (_, lines) = List.foldr (add_wanted_prfline ctxt) (0,[]) nonnull_lines val _ = trace_proof_msg (fn () => Int.toString (length lines) ^ " lines extracted\n") - val (ccls, fixes) = neg_conjecture_clauses ctxt th sgno + val (ccls, fixes) = neg_conjecture_clauses ctxt goal i val _ = trace_proof_msg (fn () => Int.toString (length ccls) ^ " conjecture clauses\n") val ccls = map forall_intr_vars ccls @@ -456,8 +460,12 @@ (fn () => "\nccl: " ^ string_of_thm ctxt th)) ccls val body = isar_proof_body ctxt (map prop_of ccls) (stringify_deps thm_names [] lines) + val n = Logic.count_prems (prop_of goal) val _ = trace_proof_msg (K "\nisar_proof_from_tstp_file: finishing\n") - in isar_header (map #1 fixes) ^ implode body ^ "qed\n" end + in + isar_proof_start i ^ isar_fixes (map #1 fixes) ^ implode body ^ + isar_proof_end n ^ "\n" + end handle STREE _ => error "Could not extract proof (ATP output malformed?)"; @@ -534,22 +542,30 @@ val chained_hint = "CHAINED"; val kill_chained = filter_out (curry (op =) chained_hint) -(* metis-command *) -fun metis_line [] = "by metis" - | metis_line xs = "by (metis " ^ space_implode " " xs ^ ")" - +fun apply_command _ 1 = "by " + | apply_command 1 _ = "apply " + | apply_command i _ = "prefer " ^ string_of_int i ^ " apply " +fun metis_command i n [] = + apply_command i n ^ "metis" + | metis_command i n xs = + apply_command i n ^ "(metis " ^ space_implode " " xs ^ ")" +fun metis_line i n xs = + "Try this command: " ^ + Markup.markup Markup.sendback (metis_command i n xs) ^ ".\n" fun minimize_line _ [] = "" - | minimize_line name lemmas = + | minimize_line name xs = "To minimize the number of lemmas, try this command:\n" ^ Markup.markup Markup.sendback ("sledgehammer minimize [atps = " ^ name ^ "] (" ^ - space_implode " " (kill_chained lemmas) ^ ")") ^ "." + space_implode " " xs ^ ")") ^ "." -fun metis_lemma_list dfg name result = - let val (lemmas, used_conj) = extract_lemmas (get_step_nums dfg) result in - ("Try this command: " ^ - Markup.markup Markup.sendback (metis_line (kill_chained lemmas)) ^ ".\n" ^ - minimize_line name lemmas ^ +fun metis_lemma_list dfg name (result as (_, _, _, _, goal, subgoalno)) = + let + val (lemmas, used_conj) = extract_lemmas (get_step_nums dfg) result + val n = Logic.count_prems (prop_of goal) + val xs = kill_chained lemmas + in + (metis_line subgoalno n xs ^ minimize_line name xs ^ (if used_conj then "" else @@ -572,11 +588,8 @@ if member (op =) tokens chained_hint then "" else isar_proof_from_tstp_file cnfs ctxt goal subgoalno thm_names in - (* Hack: The " \n" shouldn't be part of the markup. This is a workaround - for a strange ProofGeneral bug, whereby the first two letters of the word - "proof" are not highlighted. *) - (one_line_proof ^ "\n\nStructured proof:" ^ - Markup.markup Markup.sendback (" \n" ^ isar_proof), lemma_names) + (one_line_proof ^ "\nStructured proof:\n" ^ + Markup.markup Markup.sendback isar_proof, lemma_names) end end;