1.1 --- a/src/HOL/Tools/ATP_Manager/atp_manager.ML Wed Apr 21 14:46:29 2010 +0200
1.2 +++ b/src/HOL/Tools/ATP_Manager/atp_manager.ML Wed Apr 21 16:21:19 2010 +0200
1.3 @@ -9,6 +9,7 @@
1.4 signature ATP_MANAGER =
1.5 sig
1.6 type relevance_override = Sledgehammer_Fact_Filter.relevance_override
1.7 + type minimize_command = Sledgehammer_Proof_Reconstruct.minimize_command
1.8 type params =
1.9 {debug: bool,
1.10 verbose: bool,
1.11 @@ -41,7 +42,8 @@
1.12 proof: string,
1.13 internal_thm_names: string Vector.vector,
1.14 filtered_clauses: (thm * (string * int)) list}
1.15 - type prover = params -> Time.time -> problem -> prover_result
1.16 + type prover =
1.17 + params -> minimize_command -> Time.time -> problem -> prover_result
1.18
1.19 val atps: string Unsynchronized.ref
1.20 val timeout: int Unsynchronized.ref
1.21 @@ -52,7 +54,9 @@
1.22 val add_prover: string * prover -> theory -> theory
1.23 val get_prover: theory -> string -> prover option
1.24 val available_atps: theory -> unit
1.25 - val sledgehammer: params -> int -> relevance_override -> Proof.state -> unit
1.26 + val sledgehammer:
1.27 + params -> int -> relevance_override -> (string -> minimize_command)
1.28 + -> Proof.state -> unit
1.29 end;
1.30
1.31 structure ATP_Manager : ATP_MANAGER =
1.32 @@ -62,7 +66,7 @@
1.33 open Sledgehammer_Fact_Filter
1.34 open Sledgehammer_Proof_Reconstruct
1.35
1.36 -(** parameters, problems, results, and provers **)
1.37 +(** problems, results, provers, etc. **)
1.38
1.39 type params =
1.40 {debug: bool,
1.41 @@ -99,7 +103,8 @@
1.42 internal_thm_names: string Vector.vector,
1.43 filtered_clauses: (thm * (string * int)) list};
1.44
1.45 -type prover = params -> Time.time -> problem -> prover_result;
1.46 +type prover =
1.47 + params -> minimize_command -> Time.time -> problem -> prover_result
1.48
1.49
1.50 (** preferences **)
1.51 @@ -323,12 +328,12 @@
1.52 val empty = Symtab.empty;
1.53 val extend = I;
1.54 fun merge data : T = Symtab.merge (eq_snd op =) data
1.55 - handle Symtab.DUP dup => err_dup_prover dup;
1.56 + handle Symtab.DUP name => err_dup_prover name;
1.57 );
1.58
1.59 fun add_prover (name, prover) thy =
1.60 Provers.map (Symtab.update_new (name, (prover, stamp ()))) thy
1.61 - handle Symtab.DUP dup => err_dup_prover dup;
1.62 + handle Symtab.DUP name => err_dup_prover name;
1.63
1.64 fun get_prover thy name =
1.65 Option.map #1 (Symtab.lookup (Provers.get thy) name);
1.66 @@ -341,7 +346,7 @@
1.67 (* start prover thread *)
1.68
1.69 fun start_prover (params as {timeout, ...}) birth_time death_time i
1.70 - relevance_override proof_state name =
1.71 + relevance_override minimize_command proof_state name =
1.72 (case get_prover (Proof.theory_of proof_state) name of
1.73 NONE => warning ("Unknown ATP: " ^ quote name ^ ".")
1.74 | SOME prover =>
1.75 @@ -359,7 +364,8 @@
1.76 {subgoal = i, goal = (ctxt, (facts, goal)),
1.77 relevance_override = relevance_override, axiom_clauses = NONE,
1.78 filtered_clauses = NONE}
1.79 - val message = #message (prover params timeout problem)
1.80 + val message =
1.81 + #message (prover params (minimize_command name) timeout problem)
1.82 handle Sledgehammer_HOL_Clause.TRIVIAL =>
1.83 metis_line i n []
1.84 | ERROR msg => "Error: " ^ msg ^ ".\n";
1.85 @@ -371,14 +377,15 @@
1.86 (* Sledgehammer the given subgoal *)
1.87
1.88 fun sledgehammer (params as {atps, timeout, ...}) i relevance_override
1.89 - proof_state =
1.90 + minimize_command proof_state =
1.91 let
1.92 val birth_time = Time.now ()
1.93 val death_time = Time.+ (birth_time, timeout)
1.94 val _ = kill_atps () (* RACE w.r.t. other invocations of Sledgehammer *)
1.95 val _ = priority "Sledgehammering..."
1.96 val _ = List.app (start_prover params birth_time death_time i
1.97 - relevance_override proof_state) atps
1.98 + relevance_override minimize_command
1.99 + proof_state) atps
1.100 in () end
1.101
1.102 end;
2.1 --- a/src/HOL/Tools/ATP_Manager/atp_minimal.ML Wed Apr 21 14:46:29 2010 +0200
2.2 +++ b/src/HOL/Tools/ATP_Manager/atp_minimal.ML Wed Apr 21 16:21:19 2010 +0200
2.3 @@ -78,7 +78,7 @@
2.4 axiom_clauses = SOME axclauses,
2.5 filtered_clauses = SOME (the_default axclauses filtered_clauses)}
2.6 in
2.7 - `outcome_of_result (prover params timeout problem)
2.8 + `outcome_of_result (prover params (K "") timeout problem)
2.9 |>> tap (priority o string_of_outcome)
2.10 end
2.11
2.12 @@ -122,8 +122,8 @@
2.13 ["Minimized: " ^ string_of_int n ^ " theorem" ^ plural_s n] ^ ".")
2.14 in
2.15 (SOME min_thms,
2.16 - proof_text isar_proof true modulus sorts atp_name proof
2.17 - internal_thm_names ctxt goal i |> fst)
2.18 + proof_text isar_proof modulus sorts ctxt (K "") proof
2.19 + internal_thm_names goal i |> fst)
2.20 end
2.21 | (Timeout, _) =>
2.22 (NONE, "Timeout: You can increase the time limit using the \"timeout\" \
3.1 --- a/src/HOL/Tools/ATP_Manager/atp_wrapper.ML Wed Apr 21 14:46:29 2010 +0200
3.2 +++ b/src/HOL/Tools/ATP_Manager/atp_wrapper.ML Wed Apr 21 16:21:19 2010 +0200
3.3 @@ -73,6 +73,7 @@
3.4
3.5 fun generic_prover overlord get_facts prepare write_file cmd args known_failures
3.6 proof_text name ({debug, full_types, explicit_apply, ...} : params)
3.7 + minimize_command
3.8 ({subgoal, goal, relevance_override, axiom_clauses, filtered_clauses}
3.9 : problem) =
3.10 let
3.11 @@ -105,7 +106,7 @@
3.12 in
3.13 if destdir' = "" then File.tmp_path probfile
3.14 else if File.exists (Path.explode destdir')
3.15 - then Path.append (Path.explode destdir') probfile
3.16 + then Path.append (Path.explode destdir') probfile
3.17 else error ("No such directory: " ^ destdir' ^ ".")
3.18 end;
3.19
3.20 @@ -154,7 +155,7 @@
3.21 val success = rc = 0 andalso failure = "";
3.22 val (message, relevant_thm_names) =
3.23 if success then
3.24 - proof_text name proof internal_thm_names ctxt th subgoal
3.25 + proof_text ctxt minimize_command proof internal_thm_names th subgoal
3.26 else if failure <> "" then
3.27 (failure, [])
3.28 else
3.29 @@ -176,7 +177,7 @@
3.30 (params as {debug, overlord, respect_no_atp, relevance_threshold,
3.31 convergence, theory_relevant, higher_order, follow_defs,
3.32 isar_proof, modulus, sorts, ...})
3.33 - timeout =
3.34 + minimize_command timeout =
3.35 generic_prover overlord
3.36 (get_relevant_facts respect_no_atp relevance_threshold convergence
3.37 higher_order follow_defs max_new_clauses
3.38 @@ -184,8 +185,8 @@
3.39 (prepare_clauses higher_order false)
3.40 (write_tptp_file (debug andalso overlord andalso not isar_proof)) command
3.41 (arguments timeout) known_failures
3.42 - (proof_text (supports_isar_proofs andalso isar_proof) false modulus sorts)
3.43 - name params
3.44 + (proof_text (supports_isar_proofs andalso isar_proof) modulus sorts)
3.45 + name params minimize_command
3.46
3.47 fun tptp_prover name p = (name, generic_tptp_prover (name, p));
3.48
3.49 @@ -240,14 +241,14 @@
3.50 prefers_theory_relevant, ...} : prover_config))
3.51 (params as {overlord, respect_no_atp, relevance_threshold, convergence,
3.52 theory_relevant, higher_order, follow_defs, ...})
3.53 - timeout =
3.54 + minimize_command timeout =
3.55 generic_prover overlord
3.56 (get_relevant_facts respect_no_atp relevance_threshold convergence
3.57 higher_order follow_defs max_new_clauses
3.58 (the_default prefers_theory_relevant theory_relevant))
3.59 (prepare_clauses higher_order true) write_dfg_file command
3.60 - (arguments timeout) known_failures (metis_proof_text false false)
3.61 - name params
3.62 + (arguments timeout) known_failures (K metis_proof_text)
3.63 + name params minimize_command
3.64
3.65 fun dfg_prover name p = (name, generic_dfg_prover (name, p))
3.66
4.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Wed Apr 21 14:46:29 2010 +0200
4.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Wed Apr 21 16:21:19 2010 +0200
4.3 @@ -68,6 +68,10 @@
4.4 ("metis_proof", "isar_proof"),
4.5 ("no_sorts", "sorts")]
4.6
4.7 +val params_for_minimize =
4.8 + ["full_types", "explicit_apply", "higher_order", "isar_proof", "modulus",
4.9 + "sorts", "minimize_timeout"]
4.10 +
4.11 val property_dependent_params = ["atps", "full_types", "timeout"]
4.12
4.13 fun is_known_raw_param s =
4.14 @@ -219,18 +223,33 @@
4.15 val refresh_tptpN = "refresh_tptp"
4.16 val helpN = "help"
4.17
4.18 -
4.19 fun minimizize_raw_param_name "timeout" = "minimize_timeout"
4.20 | minimizize_raw_param_name name = name
4.21
4.22 +val is_raw_param_relevant_for_minimize =
4.23 + member (op =) params_for_minimize o fst o unalias_raw_param
4.24 +fun string_for_raw_param (key, values) =
4.25 + key ^ (case space_implode " " values of
4.26 + "" => ""
4.27 + | value => " = " ^ value)
4.28 +
4.29 +fun minimize_command override_params i atp_name facts =
4.30 + "sledgehammer minimize [atp = " ^ atp_name ^
4.31 + (override_params |> filter is_raw_param_relevant_for_minimize
4.32 + |> implode o map (prefix ", " o string_for_raw_param)) ^
4.33 + "] (" ^ space_implode " " facts ^ ")" ^
4.34 + (if i = 1 then "" else " " ^ string_of_int i)
4.35 +
4.36 fun hammer_away override_params subcommand opt_i relevance_override state =
4.37 let
4.38 val thy = Proof.theory_of state
4.39 val _ = List.app check_raw_param override_params
4.40 in
4.41 if subcommand = runN then
4.42 - sledgehammer (get_params thy override_params) (the_default 1 opt_i)
4.43 - relevance_override state
4.44 + let val i = the_default 1 opt_i in
4.45 + sledgehammer (get_params thy override_params) i relevance_override
4.46 + (minimize_command override_params i) state
4.47 + end
4.48 else if subcommand = minimizeN then
4.49 minimize (map (apfst minimizize_raw_param_name) override_params) []
4.50 (the_default 1 opt_i) (#add relevance_override) state
5.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Wed Apr 21 14:46:29 2010 +0200
5.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Wed Apr 21 16:21:19 2010 +0200
5.3 @@ -6,6 +6,8 @@
5.4
5.5 signature SLEDGEHAMMER_PROOF_RECONSTRUCT =
5.6 sig
5.7 + type minimize_command = string list -> string
5.8 +
5.9 val chained_hint: string
5.10 val invert_const: string -> string
5.11 val invert_type_const: string -> string
5.12 @@ -15,14 +17,14 @@
5.13 val is_proof_well_formed: string -> bool
5.14 val metis_line: int -> int -> string list -> string
5.15 val metis_proof_text:
5.16 - bool -> bool -> string -> string -> string vector -> Proof.context -> thm
5.17 - -> int -> string * string list
5.18 + minimize_command -> string -> string vector -> thm -> int
5.19 + -> string * string list
5.20 val isar_proof_text:
5.21 - bool -> int -> bool -> string -> string -> string vector -> Proof.context
5.22 + int -> bool -> Proof.context -> minimize_command -> string -> string vector
5.23 -> thm -> int -> string * string list
5.24 val proof_text:
5.25 - bool -> bool -> int -> bool -> string -> string -> string vector
5.26 - -> Proof.context -> thm -> int -> string * string list
5.27 + bool -> int -> bool -> Proof.context -> minimize_command -> string
5.28 + -> string vector -> thm -> int -> string * string list
5.29 end;
5.30
5.31 structure Sledgehammer_Proof_Reconstruct : SLEDGEHAMMER_PROOF_RECONSTRUCT =
5.32 @@ -31,6 +33,8 @@
5.33 open Sledgehammer_FOL_Clause
5.34 open Sledgehammer_Fact_Preprocessor
5.35
5.36 +type minimize_command = string list -> string
5.37 +
5.38 val trace_proof_path = Path.basic "atp_trace";
5.39
5.40 fun trace_proof_msg f =
5.41 @@ -528,16 +532,15 @@
5.42 fun metis_line i n xs =
5.43 "Try this command: " ^
5.44 Markup.markup Markup.sendback (metis_command i n xs) ^ ".\n"
5.45 -fun minimize_line _ _ [] = ""
5.46 - | minimize_line isar_proof atp_name xs =
5.47 +fun minimize_line _ [] = ""
5.48 + | minimize_line minimize_command facts =
5.49 + case minimize_command facts of
5.50 + "" => ""
5.51 + | command =>
5.52 "To minimize the number of lemmas, try this command: " ^
5.53 - Markup.markup Markup.sendback
5.54 - ("sledgehammer minimize [atp = " ^ atp_name ^
5.55 - (if isar_proof then ", isar_proof" else "") ^ "] (" ^
5.56 - space_implode " " xs ^ ")") ^ ".\n"
5.57 + Markup.markup Markup.sendback command ^ ".\n"
5.58
5.59 -fun metis_proof_text isar_proof minimal atp_name proof thm_names
5.60 - (_ : Proof.context) goal i =
5.61 +fun metis_proof_text minimize_command proof thm_names goal i =
5.62 let
5.63 val lemmas =
5.64 proof |> get_proof_extract
5.65 @@ -549,12 +552,10 @@
5.66 val n = Logic.count_prems (prop_of goal)
5.67 val xs = kill_chained lemmas
5.68 in
5.69 - (metis_line i n xs ^
5.70 - (if minimal then "" else minimize_line isar_proof atp_name xs),
5.71 - kill_chained lemmas)
5.72 + (metis_line i n xs ^ minimize_line minimize_command xs, kill_chained lemmas)
5.73 end
5.74
5.75 -fun isar_proof_text minimal modulus sorts atp_name proof thm_names ctxt goal i =
5.76 +fun isar_proof_text modulus sorts ctxt minimize_command proof thm_names goal i =
5.77 let
5.78 (* We could use "split_lines", but it can return blank lines. *)
5.79 val lines = String.tokens (equal #"\n");
5.80 @@ -563,7 +564,7 @@
5.81 val extract = get_proof_extract proof
5.82 val cnfs = filter (String.isPrefix "cnf(") (map kill_spaces (lines extract))
5.83 val (one_line_proof, lemma_names) =
5.84 - metis_proof_text true minimal atp_name proof thm_names ctxt goal i
5.85 + metis_proof_text minimize_command proof thm_names goal i
5.86 val tokens = String.tokens (fn c => c = #" ") one_line_proof
5.87 val isar_proof =
5.88 if member (op =) tokens chained_hint then ""
5.89 @@ -575,8 +576,7 @@
5.90 lemma_names)
5.91 end
5.92
5.93 -fun proof_text isar_proof minimal modulus sorts =
5.94 - if isar_proof then isar_proof_text minimal modulus sorts
5.95 - else metis_proof_text isar_proof minimal
5.96 +fun proof_text isar_proof modulus sorts ctxt =
5.97 + if isar_proof then isar_proof_text modulus sorts ctxt else metis_proof_text
5.98
5.99 end;