# HG changeset patch # User blanchet # Date 1271859679 -7200 # Node ID dbbf4d5d584d217561aec0e99cb3dbf918fe52b0 # Parent 65aabc2c89aeff186b76f431489ea2718af97bc8 pass relevant options from "sledgehammer" to "sledgehammer minimize"; one nice side effect of this change is that the "sledgehammer minimize" syntax now only occurs in "sledgehammer_isar.ML", instead of being spread across two files diff -r 65aabc2c89ae -r dbbf4d5d584d src/HOL/Tools/ATP_Manager/atp_manager.ML --- a/src/HOL/Tools/ATP_Manager/atp_manager.ML Wed Apr 21 14:46:29 2010 +0200 +++ b/src/HOL/Tools/ATP_Manager/atp_manager.ML Wed Apr 21 16:21:19 2010 +0200 @@ -9,6 +9,7 @@ signature ATP_MANAGER = sig type relevance_override = Sledgehammer_Fact_Filter.relevance_override + type minimize_command = Sledgehammer_Proof_Reconstruct.minimize_command type params = {debug: bool, verbose: bool, @@ -41,7 +42,8 @@ proof: string, internal_thm_names: string Vector.vector, filtered_clauses: (thm * (string * int)) list} - type prover = params -> Time.time -> problem -> prover_result + type prover = + params -> minimize_command -> Time.time -> problem -> prover_result val atps: string Unsynchronized.ref val timeout: int Unsynchronized.ref @@ -52,7 +54,9 @@ val add_prover: string * prover -> theory -> theory val get_prover: theory -> string -> prover option val available_atps: theory -> unit - val sledgehammer: params -> int -> relevance_override -> Proof.state -> unit + val sledgehammer: + params -> int -> relevance_override -> (string -> minimize_command) + -> Proof.state -> unit end; structure ATP_Manager : ATP_MANAGER = @@ -62,7 +66,7 @@ open Sledgehammer_Fact_Filter open Sledgehammer_Proof_Reconstruct -(** parameters, problems, results, and provers **) +(** problems, results, provers, etc. **) type params = {debug: bool, @@ -99,7 +103,8 @@ internal_thm_names: string Vector.vector, filtered_clauses: (thm * (string * int)) list}; -type prover = params -> Time.time -> problem -> prover_result; +type prover = + params -> minimize_command -> Time.time -> problem -> prover_result (** preferences **) @@ -323,12 +328,12 @@ val empty = Symtab.empty; val extend = I; fun merge data : T = Symtab.merge (eq_snd op =) data - handle Symtab.DUP dup => err_dup_prover dup; + handle Symtab.DUP name => err_dup_prover name; ); fun add_prover (name, prover) thy = Provers.map (Symtab.update_new (name, (prover, stamp ()))) thy - handle Symtab.DUP dup => err_dup_prover dup; + handle Symtab.DUP name => err_dup_prover name; fun get_prover thy name = Option.map #1 (Symtab.lookup (Provers.get thy) name); @@ -341,7 +346,7 @@ (* start prover thread *) fun start_prover (params as {timeout, ...}) birth_time death_time i - relevance_override proof_state name = + relevance_override minimize_command proof_state name = (case get_prover (Proof.theory_of proof_state) name of NONE => warning ("Unknown ATP: " ^ quote name ^ ".") | SOME prover => @@ -359,7 +364,8 @@ {subgoal = i, goal = (ctxt, (facts, goal)), relevance_override = relevance_override, axiom_clauses = NONE, filtered_clauses = NONE} - val message = #message (prover params timeout problem) + val message = + #message (prover params (minimize_command name) timeout problem) handle Sledgehammer_HOL_Clause.TRIVIAL => metis_line i n [] | ERROR msg => "Error: " ^ msg ^ ".\n"; @@ -371,14 +377,15 @@ (* Sledgehammer the given subgoal *) fun sledgehammer (params as {atps, timeout, ...}) i relevance_override - proof_state = + minimize_command proof_state = let val birth_time = Time.now () val death_time = Time.+ (birth_time, timeout) val _ = kill_atps () (* RACE w.r.t. other invocations of Sledgehammer *) val _ = priority "Sledgehammering..." val _ = List.app (start_prover params birth_time death_time i - relevance_override proof_state) atps + relevance_override minimize_command + proof_state) atps in () end end; diff -r 65aabc2c89ae -r dbbf4d5d584d src/HOL/Tools/ATP_Manager/atp_minimal.ML --- a/src/HOL/Tools/ATP_Manager/atp_minimal.ML Wed Apr 21 14:46:29 2010 +0200 +++ b/src/HOL/Tools/ATP_Manager/atp_minimal.ML Wed Apr 21 16:21:19 2010 +0200 @@ -78,7 +78,7 @@ axiom_clauses = SOME axclauses, filtered_clauses = SOME (the_default axclauses filtered_clauses)} in - `outcome_of_result (prover params timeout problem) + `outcome_of_result (prover params (K "") timeout problem) |>> tap (priority o string_of_outcome) end @@ -122,8 +122,8 @@ ["Minimized: " ^ string_of_int n ^ " theorem" ^ plural_s n] ^ ".") in (SOME min_thms, - proof_text isar_proof true modulus sorts atp_name proof - internal_thm_names ctxt goal i |> fst) + proof_text isar_proof modulus sorts ctxt (K "") proof + internal_thm_names goal i |> fst) end | (Timeout, _) => (NONE, "Timeout: You can increase the time limit using the \"timeout\" \ diff -r 65aabc2c89ae -r dbbf4d5d584d src/HOL/Tools/ATP_Manager/atp_wrapper.ML --- a/src/HOL/Tools/ATP_Manager/atp_wrapper.ML Wed Apr 21 14:46:29 2010 +0200 +++ b/src/HOL/Tools/ATP_Manager/atp_wrapper.ML Wed Apr 21 16:21:19 2010 +0200 @@ -73,6 +73,7 @@ fun generic_prover overlord get_facts prepare write_file cmd args known_failures proof_text name ({debug, full_types, explicit_apply, ...} : params) + minimize_command ({subgoal, goal, relevance_override, axiom_clauses, filtered_clauses} : problem) = let @@ -105,7 +106,7 @@ in if destdir' = "" then File.tmp_path probfile else if File.exists (Path.explode destdir') - then Path.append (Path.explode destdir') probfile + then Path.append (Path.explode destdir') probfile else error ("No such directory: " ^ destdir' ^ ".") end; @@ -154,7 +155,7 @@ val success = rc = 0 andalso failure = ""; val (message, relevant_thm_names) = if success then - proof_text name proof internal_thm_names ctxt th subgoal + proof_text ctxt minimize_command proof internal_thm_names th subgoal else if failure <> "" then (failure, []) else @@ -176,7 +177,7 @@ (params as {debug, overlord, respect_no_atp, relevance_threshold, convergence, theory_relevant, higher_order, follow_defs, isar_proof, modulus, sorts, ...}) - timeout = + minimize_command timeout = generic_prover overlord (get_relevant_facts respect_no_atp relevance_threshold convergence higher_order follow_defs max_new_clauses @@ -184,8 +185,8 @@ (prepare_clauses higher_order false) (write_tptp_file (debug andalso overlord andalso not isar_proof)) command (arguments timeout) known_failures - (proof_text (supports_isar_proofs andalso isar_proof) false modulus sorts) - name params + (proof_text (supports_isar_proofs andalso isar_proof) modulus sorts) + name params minimize_command fun tptp_prover name p = (name, generic_tptp_prover (name, p)); @@ -240,14 +241,14 @@ prefers_theory_relevant, ...} : prover_config)) (params as {overlord, respect_no_atp, relevance_threshold, convergence, theory_relevant, higher_order, follow_defs, ...}) - timeout = + minimize_command timeout = generic_prover overlord (get_relevant_facts respect_no_atp relevance_threshold convergence higher_order follow_defs max_new_clauses (the_default prefers_theory_relevant theory_relevant)) (prepare_clauses higher_order true) write_dfg_file command - (arguments timeout) known_failures (metis_proof_text false false) - name params + (arguments timeout) known_failures (K metis_proof_text) + name params minimize_command fun dfg_prover name p = (name, generic_dfg_prover (name, p)) diff -r 65aabc2c89ae -r dbbf4d5d584d src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Wed Apr 21 14:46:29 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Wed Apr 21 16:21:19 2010 +0200 @@ -68,6 +68,10 @@ ("metis_proof", "isar_proof"), ("no_sorts", "sorts")] +val params_for_minimize = + ["full_types", "explicit_apply", "higher_order", "isar_proof", "modulus", + "sorts", "minimize_timeout"] + val property_dependent_params = ["atps", "full_types", "timeout"] fun is_known_raw_param s = @@ -219,18 +223,33 @@ val refresh_tptpN = "refresh_tptp" val helpN = "help" - fun minimizize_raw_param_name "timeout" = "minimize_timeout" | minimizize_raw_param_name name = name +val is_raw_param_relevant_for_minimize = + member (op =) params_for_minimize o fst o unalias_raw_param +fun string_for_raw_param (key, values) = + key ^ (case space_implode " " values of + "" => "" + | value => " = " ^ value) + +fun minimize_command override_params i atp_name facts = + "sledgehammer minimize [atp = " ^ atp_name ^ + (override_params |> filter is_raw_param_relevant_for_minimize + |> implode o map (prefix ", " o string_for_raw_param)) ^ + "] (" ^ space_implode " " facts ^ ")" ^ + (if i = 1 then "" else " " ^ string_of_int i) + fun hammer_away override_params subcommand opt_i relevance_override state = let val thy = Proof.theory_of state val _ = List.app check_raw_param override_params in if subcommand = runN then - sledgehammer (get_params thy override_params) (the_default 1 opt_i) - relevance_override state + let val i = the_default 1 opt_i in + sledgehammer (get_params thy override_params) i relevance_override + (minimize_command override_params i) state + end else if subcommand = minimizeN then minimize (map (apfst minimizize_raw_param_name) override_params) [] (the_default 1 opt_i) (#add relevance_override) state diff -r 65aabc2c89ae -r dbbf4d5d584d src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Wed Apr 21 14:46:29 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Wed Apr 21 16:21:19 2010 +0200 @@ -6,6 +6,8 @@ signature SLEDGEHAMMER_PROOF_RECONSTRUCT = sig + type minimize_command = string list -> string + val chained_hint: string val invert_const: string -> string val invert_type_const: string -> string @@ -15,14 +17,14 @@ val is_proof_well_formed: string -> bool val metis_line: int -> int -> string list -> string val metis_proof_text: - bool -> bool -> string -> string -> string vector -> Proof.context -> thm - -> int -> string * string list + minimize_command -> string -> string vector -> thm -> int + -> string * string list val isar_proof_text: - bool -> int -> bool -> string -> string -> string vector -> Proof.context + int -> bool -> Proof.context -> minimize_command -> string -> string vector -> thm -> int -> string * string list val proof_text: - bool -> bool -> int -> bool -> string -> string -> string vector - -> Proof.context -> thm -> int -> string * string list + bool -> int -> bool -> Proof.context -> minimize_command -> string + -> string vector -> thm -> int -> string * string list end; structure Sledgehammer_Proof_Reconstruct : SLEDGEHAMMER_PROOF_RECONSTRUCT = @@ -31,6 +33,8 @@ open Sledgehammer_FOL_Clause open Sledgehammer_Fact_Preprocessor +type minimize_command = string list -> string + val trace_proof_path = Path.basic "atp_trace"; fun trace_proof_msg f = @@ -528,16 +532,15 @@ fun metis_line i n xs = "Try this command: " ^ Markup.markup Markup.sendback (metis_command i n xs) ^ ".\n" -fun minimize_line _ _ [] = "" - | minimize_line isar_proof atp_name xs = +fun minimize_line _ [] = "" + | minimize_line minimize_command facts = + case minimize_command facts of + "" => "" + | command => "To minimize the number of lemmas, try this command: " ^ - Markup.markup Markup.sendback - ("sledgehammer minimize [atp = " ^ atp_name ^ - (if isar_proof then ", isar_proof" else "") ^ "] (" ^ - space_implode " " xs ^ ")") ^ ".\n" + Markup.markup Markup.sendback command ^ ".\n" -fun metis_proof_text isar_proof minimal atp_name proof thm_names - (_ : Proof.context) goal i = +fun metis_proof_text minimize_command proof thm_names goal i = let val lemmas = proof |> get_proof_extract @@ -549,12 +552,10 @@ val n = Logic.count_prems (prop_of goal) val xs = kill_chained lemmas in - (metis_line i n xs ^ - (if minimal then "" else minimize_line isar_proof atp_name xs), - kill_chained lemmas) + (metis_line i n xs ^ minimize_line minimize_command xs, kill_chained lemmas) end -fun isar_proof_text minimal modulus sorts atp_name proof thm_names ctxt goal i = +fun isar_proof_text modulus sorts ctxt minimize_command proof thm_names goal i = let (* We could use "split_lines", but it can return blank lines. *) val lines = String.tokens (equal #"\n"); @@ -563,7 +564,7 @@ val extract = get_proof_extract proof val cnfs = filter (String.isPrefix "cnf(") (map kill_spaces (lines extract)) val (one_line_proof, lemma_names) = - metis_proof_text true minimal atp_name proof thm_names ctxt goal i + metis_proof_text minimize_command proof thm_names goal i val tokens = String.tokens (fn c => c = #" ") one_line_proof val isar_proof = if member (op =) tokens chained_hint then "" @@ -575,8 +576,7 @@ lemma_names) end -fun proof_text isar_proof minimal modulus sorts = - if isar_proof then isar_proof_text minimal modulus sorts - else metis_proof_text isar_proof minimal +fun proof_text isar_proof modulus sorts ctxt = + if isar_proof then isar_proof_text modulus sorts ctxt else metis_proof_text end;