# HG changeset patch # User blanchet # Date 1269884997 -7200 # Node ID 48aec67c284f7235801c320869a35d0a84649341 # Parent cdc6855a63871aa692973d69413d8b016dbd44b9 added "modulus" and "sorts" options to control Sledgehammer's Isar proof output diff -r cdc6855a6387 -r 48aec67c284f src/HOL/Sledgehammer.thy --- a/src/HOL/Sledgehammer.thy Mon Mar 29 18:44:24 2010 +0200 +++ b/src/HOL/Sledgehammer.thy Mon Mar 29 19:49:57 2010 +0200 @@ -99,7 +99,6 @@ setup Sledgehammer_Fact_Preprocessor.setup use "Tools/Sledgehammer/sledgehammer_hol_clause.ML" use "Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML" -setup Sledgehammer_Proof_Reconstruct.setup use "Tools/Sledgehammer/sledgehammer_fact_filter.ML" use "Tools/ATP_Manager/atp_manager.ML" use "Tools/ATP_Manager/atp_wrapper.ML" diff -r cdc6855a6387 -r 48aec67c284f src/HOL/Tools/ATP_Manager/atp_manager.ML --- a/src/HOL/Tools/ATP_Manager/atp_manager.ML Mon Mar 29 18:44:24 2010 +0200 +++ b/src/HOL/Tools/ATP_Manager/atp_manager.ML Mon Mar 29 19:49:57 2010 +0200 @@ -21,6 +21,8 @@ higher_order: bool option, follow_defs: bool, isar_proof: bool, + modulus: int, + sorts: bool, timeout: Time.time, minimize_timeout: Time.time} type problem = @@ -71,6 +73,8 @@ higher_order: bool option, follow_defs: bool, isar_proof: bool, + modulus: int, + sorts: bool, timeout: Time.time, minimize_timeout: Time.time} diff -r cdc6855a6387 -r 48aec67c284f src/HOL/Tools/ATP_Manager/atp_wrapper.ML --- a/src/HOL/Tools/ATP_Manager/atp_wrapper.ML Mon Mar 29 18:44:24 2010 +0200 +++ b/src/HOL/Tools/ATP_Manager/atp_wrapper.ML Mon Mar 29 19:49:57 2010 +0200 @@ -160,7 +160,8 @@ (name, {command, arguments, failure_strs, max_new_clauses, prefers_theory_const, supports_isar_proofs}) (params as {respect_no_atp, relevance_threshold, convergence, - theory_const, higher_order, follow_defs, isar_proof, ...}) + theory_const, higher_order, follow_defs, isar_proof, + modulus, sorts, ...}) timeout = generic_prover (get_relevant_facts respect_no_atp relevance_threshold convergence @@ -168,8 +169,10 @@ (the_default prefers_theory_const theory_const)) (prepare_clauses higher_order false) write_tptp_file command (arguments timeout) failure_strs - (if supports_isar_proofs andalso isar_proof then structured_isar_proof - else metis_lemma_list false) name params; + (if supports_isar_proofs andalso isar_proof then + structured_isar_proof modulus sorts + else + metis_lemma_list false) name params; fun tptp_prover name p = (name, generic_tptp_prover (name, p)); @@ -215,7 +218,7 @@ (name, ({command, arguments, failure_strs, max_new_clauses, prefers_theory_const, ...} : prover_config)) (params as {respect_no_atp, relevance_threshold, convergence, - theory_const, higher_order, follow_defs, isar_proof, ...}) + theory_const, higher_order, follow_defs, ...}) timeout = generic_prover (get_relevant_facts respect_no_atp relevance_threshold convergence diff -r cdc6855a6387 -r 48aec67c284f src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Mon Mar 29 18:44:24 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Mon Mar 29 19:49:57 2010 +0200 @@ -47,6 +47,8 @@ ("higher_order", "smart"), ("follow_defs", "false"), ("isar_proof", "false"), + ("modulus", "1"), + ("sorts", "false"), ("minimize_timeout", "5 s")] val negated_params = @@ -57,7 +59,8 @@ ("no_theory_const", "theory_const"), ("first_order", "higher_order"), ("dont_follow_defs", "follow_defs"), - ("metis_proof", "isar_proof")] + ("metis_proof", "isar_proof"), + ("no_sorts", "sorts")] val property_dependent_params = ["atps", "full_types", "timeout"] @@ -130,6 +133,8 @@ val higher_order = lookup_bool_option "higher_order" val follow_defs = lookup_bool "follow_defs" val isar_proof = lookup_bool "isar_proof" + val modulus = Int.max (1, lookup_int "modulus") + val sorts = lookup_bool "sorts" val timeout = lookup_time "timeout" val minimize_timeout = lookup_time "minimize_timeout" in @@ -137,8 +142,8 @@ respect_no_atp = respect_no_atp, relevance_threshold = relevance_threshold, convergence = convergence, theory_const = theory_const, higher_order = higher_order, follow_defs = follow_defs, - isar_proof = isar_proof, timeout = timeout, - minimize_timeout = minimize_timeout} + isar_proof = isar_proof, modulus = modulus, sorts = sorts, + timeout = timeout, minimize_timeout = minimize_timeout} end fun get_params thy = extract_params thy (default_raw_params thy) diff -r cdc6855a6387 -r 48aec67c284f src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Mon Mar 29 18:44:24 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Mon Mar 29 19:49:57 2010 +0200 @@ -12,12 +12,11 @@ val num_typargs: theory -> string -> int val make_tvar: string -> typ 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 -> + val structured_isar_proof: int -> bool -> string -> string * string vector * (int * int) * Proof.context * thm * int -> string * string list end; @@ -34,14 +33,6 @@ fun string_of_thm ctxt = PrintMode.setmp [] (Display.string_of_thm ctxt); -(*For generating structured proofs: keep every nth proof line*) -val (modulus, modulus_setup) = Attrib.config_int "sledgehammer_modulus" (K 1); - -(*Indicates whether to include sort information in generated proofs*) -val (recon_sorts, recon_sorts_setup) = Attrib.config_bool "sledgehammer_sorts" (K true); - -val setup = modulus_setup #> recon_sorts_setup; - (**** PARSING OF TSTP FORMAT ****) (*Syntax trees, either termlist or formulae*) @@ -336,10 +327,13 @@ (*ctms is a list of conjecture clauses as yielded by Isabelle. Those returned by the ATP may have their literals reordered.*) -fun isar_proof_body ctxt ctms = +fun isar_proof_body ctxt sorts ctms = let val _ = trace_proof_msg (K "\n\nisar_proof_body: start\n") - val string_of_term = PrintMode.setmp [] (Syntax.string_of_term ctxt) + val string_of_term = + PrintMode.setmp (filter (curry (op =) Symbol.xsymbolsN) + (print_mode_value ())) + (Syntax.string_of_term ctxt) fun have_or_show "show" _ = " show \"" | have_or_show have lname = " " ^ have ^ " " ^ lname ^ ": \"" fun do_line _ (lname, t, []) = @@ -355,7 +349,7 @@ fun do_lines [(lname, t, deps)] = [do_line "show" (lname, t, deps)] | do_lines ((lname, t, deps) :: lines) = do_line "have" (lname, t, deps) :: do_lines lines - in setmp_CRITICAL show_sorts (Config.get ctxt recon_sorts) do_lines end; + in setmp_CRITICAL show_sorts sorts do_lines end; fun unequal t (_, t', _) = not (t aconv t'); @@ -405,13 +399,13 @@ counts the number of proof lines processed so far. Deleted lines are replaced by their own dependencies. Note that the "add_nonnull_prfline" phase may delete some dependencies, hence this phase comes later.*) -fun add_wanted_prfline ctxt ((lno, t, []), (nlines, lines)) = +fun add_wanted_prfline ctxt _ ((lno, t, []), (nlines, lines)) = (nlines, (lno, t, []) :: lines) (*conjecture clauses must be kept*) - | add_wanted_prfline ctxt ((lno, t, deps), (nlines, lines)) = + | add_wanted_prfline ctxt modulus ((lno, t, deps), (nlines, lines)) = if eq_types t orelse not (null (Term.add_tvars t [])) orelse exists_subterm bad_free t orelse (not (null lines) andalso (*final line can't be deleted for these reasons*) - (length deps < 2 orelse nlines mod (Config.get ctxt modulus) <> 0)) + (length deps < 2 orelse nlines mod modulus <> 0)) then (nlines+1, map (replace_deps (lno, deps)) lines) (*Delete line*) else (nlines+1, (lno, t, deps) :: lines); @@ -436,7 +430,7 @@ fun isar_proof_end 1 = "qed" | isar_proof_end _ = "next" -fun isar_proof_from_tstp_file cnfs ctxt goal i thm_names = +fun isar_proof_from_tstp_file cnfs modulus sorts 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 @@ -449,7 +443,7 @@ val nonnull_lines = List.foldr add_nonnull_prfline [] raw_lines val _ = trace_proof_msg (fn () => Int.toString (length nonnull_lines) ^ " nonnull_lines extracted\n") - val (_, lines) = List.foldr (add_wanted_prfline ctxt) (0,[]) nonnull_lines + val (_, lines) = List.foldr (add_wanted_prfline ctxt modulus) (0,[]) nonnull_lines val _ = trace_proof_msg (fn () => Int.toString (length lines) ^ " lines extracted\n") val (ccls, fixes) = neg_conjecture_clauses ctxt goal i @@ -458,7 +452,7 @@ val ccls = map forall_intr_vars ccls val _ = app (fn th => trace_proof_msg (fn () => "\nccl: " ^ string_of_thm ctxt th)) ccls - val body = isar_proof_body ctxt (map prop_of ccls) + val body = isar_proof_body ctxt sorts (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") @@ -559,13 +553,13 @@ ("sledgehammer minimize [atps = " ^ name ^ "] (" ^ space_implode " " xs ^ ")") ^ "." -fun metis_lemma_list dfg name (result as (_, _, _, _, goal, subgoalno)) = +fun metis_lemma_list dfg name (result as (_, _, _, _, goal, i)) = 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 ^ + (metis_line i n xs ^ minimize_line name xs ^ (if used_conj then "" else @@ -573,10 +567,10 @@ kill_chained lemmas) end; -fun structured_isar_proof name (result as (proof, thm_names, conj_count, ctxt, - goal, subgoalno)) = +fun structured_isar_proof modulus sorts name + (result as (proof, thm_names, conj_count, ctxt, goal, i)) = let - (* Could use "split_lines", but it can return blank lines *) + (* We could use "split_lines", but it can return blank lines. *) val lines = String.tokens (equal #"\n"); val kill_spaces = String.translate (fn c => if Char.isSpace c then "" else str c) @@ -586,10 +580,12 @@ val tokens = String.tokens (fn c => c = #" ") one_line_proof val isar_proof = if member (op =) tokens chained_hint then "" - else isar_proof_from_tstp_file cnfs ctxt goal subgoalno thm_names + else isar_proof_from_tstp_file cnfs modulus sorts ctxt goal i thm_names in - (one_line_proof ^ "\nStructured proof:\n" ^ - Markup.markup Markup.sendback isar_proof, lemma_names) + (one_line_proof ^ + (if isar_proof = "" then "" + else "\nStructured proof:\n" ^ Markup.markup Markup.sendback isar_proof), + lemma_names) end end;