1.1 --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Fri Apr 23 16:21:47 2010 +0200
1.2 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Fri Apr 23 16:55:51 2010 +0200
1.3 @@ -475,7 +475,7 @@
1.4
1.5 fun invoke args =
1.6 let
1.7 - val _ = ATP_Manager.full_types := AList.defined (op =) args full_typesK
1.8 + val _ = Sledgehammer_Isar.full_types := AList.defined (op =) args full_typesK
1.9 in Mirabelle.register (init, sledgehammer_action args, done) end
1.10
1.11 end
2.1 --- a/src/HOL/Tools/ATP_Manager/atp_manager.ML Fri Apr 23 16:21:47 2010 +0200
2.2 +++ b/src/HOL/Tools/ATP_Manager/atp_manager.ML Fri Apr 23 16:55:51 2010 +0200
2.3 @@ -55,9 +55,9 @@
2.4 val add_prover: string * prover -> theory -> theory
2.5 val get_prover: theory -> string -> prover option
2.6 val available_atps: theory -> unit
2.7 - val sledgehammer:
2.8 - params -> int -> relevance_override -> (string -> minimize_command)
2.9 - -> Proof.state -> unit
2.10 + val start_prover_thread:
2.11 + params -> Time.time -> Time.time -> int -> relevance_override
2.12 + -> (string -> minimize_command) -> Proof.state -> string -> unit
2.13 end;
2.14
2.15 structure ATP_Manager : ATP_MANAGER =
2.16 @@ -331,8 +331,8 @@
2.17
2.18 (* start prover thread *)
2.19
2.20 -fun start_prover (params as {timeout, ...}) birth_time death_time i
2.21 - relevance_override minimize_command proof_state name =
2.22 +fun start_prover_thread (params as {timeout, ...}) birth_time death_time i
2.23 + relevance_override minimize_command proof_state name =
2.24 (case get_prover (Proof.theory_of proof_state) name of
2.25 NONE => error ("Unknown ATP: " ^ quote name ^ ".")
2.26 | SOME prover =>
2.27 @@ -358,20 +358,4 @@
2.28 in () end);
2.29 in () end);
2.30
2.31 -
2.32 -(* Sledgehammer the given subgoal *)
2.33 -
2.34 -fun sledgehammer {atps = [], ...} _ _ _ _ = error "No ATP is set."
2.35 - | sledgehammer (params as {atps, timeout, ...}) i relevance_override
2.36 - minimize_command proof_state =
2.37 - let
2.38 - val birth_time = Time.now ()
2.39 - val death_time = Time.+ (birth_time, timeout)
2.40 - val _ = kill_atps () (* Race w.r.t. other invocations of Sledgehammer *)
2.41 - val _ = priority "Sledgehammering..."
2.42 - val _ = List.app (start_prover params birth_time death_time i
2.43 - relevance_override minimize_command
2.44 - proof_state) atps
2.45 - in () end
2.46 -
2.47 end;
3.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Fri Apr 23 16:21:47 2010 +0200
3.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Fri Apr 23 16:55:51 2010 +0200
3.3 @@ -53,13 +53,13 @@
3.4 val _ =
3.5 ProofGeneralPgip.add_preference Preferences.category_proof
3.6 (Preferences.int_pref timeout
3.7 - "Sledgehammer: Time limit"
3.8 + "Sledgehammer: Time Limit"
3.9 "ATPs will be interrupted after this time (in seconds)")
3.10
3.11 val _ =
3.12 ProofGeneralPgip.add_preference Preferences.category_proof
3.13 (Preferences.bool_pref full_types
3.14 - "Sledgehammer: Full types" "ATPs will use full type information")
3.15 + "Sledgehammer: Full Types" "ATPs will use full type information")
3.16
3.17 type raw_param = string * string list
3.18
3.19 @@ -196,6 +196,21 @@
3.20 fun get_params thy = extract_params thy (default_raw_params thy)
3.21 fun default_params thy = get_params thy o map (apsnd single)
3.22
3.23 +(* Sledgehammer the given subgoal *)
3.24 +
3.25 +fun run {atps = [], ...} _ _ _ _ = error "No ATP is set."
3.26 + | run (params as {atps, timeout, ...}) i relevance_override minimize_command
3.27 + proof_state =
3.28 + let
3.29 + val birth_time = Time.now ()
3.30 + val death_time = Time.+ (birth_time, timeout)
3.31 + val _ = kill_atps () (* race w.r.t. other invocations of Sledgehammer *)
3.32 + val _ = priority "Sledgehammering..."
3.33 + val _ = List.app (start_prover_thread params birth_time death_time i
3.34 + relevance_override minimize_command
3.35 + proof_state) atps
3.36 + in () end
3.37 +
3.38 fun minimize override_params old_style_args i fact_refs state =
3.39 let
3.40 val thy = Proof.theory_of state
3.41 @@ -232,6 +247,9 @@
3.42 priority (#2 (minimize_theorems params prover atp i state name_thms_pairs))
3.43 end
3.44
3.45 +val sledgehammerN = "sledgehammer"
3.46 +val sledgehammer_paramsN = "sledgehammer_params"
3.47 +
3.48 val runN = "run"
3.49 val minimizeN = "minimize"
3.50 val messagesN = "messages"
3.51 @@ -252,7 +270,7 @@
3.52 | value => " = " ^ value)
3.53
3.54 fun minimize_command override_params i atp_name facts =
3.55 - "sledgehammer minimize [atp = " ^ atp_name ^
3.56 + sledgehammerN ^ " " ^ minimizeN ^ " [atp = " ^ atp_name ^
3.57 (override_params |> filter is_raw_param_relevant_for_minimize
3.58 |> implode o map (prefix ", " o string_for_raw_param)) ^
3.59 "] (" ^ space_implode " " facts ^ ")" ^
3.60 @@ -265,8 +283,8 @@
3.61 in
3.62 if subcommand = runN then
3.63 let val i = the_default 1 opt_i in
3.64 - sledgehammer (get_params thy override_params) i relevance_override
3.65 - (minimize_command override_params i) state
3.66 + run (get_params thy override_params) i relevance_override
3.67 + (minimize_command override_params i) state
3.68 end
3.69 else if subcommand = minimizeN then
3.70 minimize (map (apfst minimizize_raw_param_name) override_params) []
3.71 @@ -355,11 +373,11 @@
3.72 Toplevel.keep (minimize [] args 1 fact_refs o Toplevel.proof_of)))
3.73
3.74 val _ =
3.75 - OuterSyntax.improper_command "sledgehammer"
3.76 + OuterSyntax.improper_command sledgehammerN
3.77 "search for first-order proof using automatic theorem provers" K.diag
3.78 parse_sledgehammer_command
3.79 val _ =
3.80 - OuterSyntax.command "sledgehammer_params"
3.81 + OuterSyntax.command sledgehammer_paramsN
3.82 "set and display the default parameters for Sledgehammer" K.thy_decl
3.83 parse_sledgehammer_params_command
3.84