14 structure Sledgehammer_Isar : sig end = |
14 structure Sledgehammer_Isar : sig end = |
15 struct |
15 struct |
16 |
16 |
17 open ATP_Manager |
17 open ATP_Manager |
18 open ATP_Minimal |
18 open ATP_Minimal |
|
19 open ATP_Wrapper |
19 open Sledgehammer_Util |
20 open Sledgehammer_Util |
20 |
21 |
21 structure K = OuterKeyword and P = OuterParse |
22 structure K = OuterKeyword and P = OuterParse |
|
23 |
|
24 datatype facta = Facta of {add: Facts.ref list, del: Facts.ref list, only: bool} |
|
25 |
|
26 fun add_to_facta ns = Facta {add = ns, del = [], only = false}; |
|
27 fun del_from_facta ns = Facta {add = [], del = ns, only = false}; |
|
28 fun only_facta ns = Facta {add = ns, del = [], only = true}; |
|
29 val default_facta = add_to_facta [] |
|
30 fun merge_facta_pairwise (Facta f1) (Facta f2) = |
|
31 Facta {add = #add f1 @ #add f2, del = #del f1 @ #del f2, |
|
32 only = #only f1 orelse #only f2} |
|
33 fun merge_facta fs = fold merge_facta_pairwise fs default_facta |
22 |
34 |
23 type raw_param = string * string list |
35 type raw_param = string * string list |
24 |
36 |
25 val default_default_params = |
37 val default_default_params = |
26 [("debug", "false"), |
38 [("debug", "false"), |
114 respect_no_atp = respect_no_atp, follow_defs = follow_defs, |
126 respect_no_atp = respect_no_atp, follow_defs = follow_defs, |
115 isar_proof = isar_proof, timeout = timeout, |
127 isar_proof = isar_proof, timeout = timeout, |
116 minimize_timeout = minimize_timeout} |
128 minimize_timeout = minimize_timeout} |
117 end |
129 end |
118 |
130 |
119 fun default_params thy = |
131 fun get_params thy = extract_params thy (default_raw_params thy) |
120 extract_params thy (default_raw_params thy) o map (apsnd single) |
132 fun default_params thy = get_params thy o map (apsnd single) |
121 |
133 |
122 fun atp_minimize_command args thm_names state = |
134 fun atp_minimize_command override_params old_style_args fact_refs state = |
123 let |
135 let |
124 val thy = Proof.theory_of state |
136 val thy = Proof.theory_of state |
125 val ctxt = Proof.context_of state |
137 val ctxt = Proof.context_of state |
126 fun theorems_from_names ctxt = |
138 fun theorems_from_refs ctxt = |
127 map (fn (name, interval) => |
139 map (fn fact_ref => |
128 let |
140 let |
129 val thmref = Facts.Named ((name, Position.none), interval) |
141 val ths = ProofContext.get_fact ctxt fact_ref |
130 val ths = ProofContext.get_fact ctxt thmref |
142 val name' = Facts.string_of_ref fact_ref |
131 val name' = Facts.string_of_ref thmref |
|
132 in (name', ths) end) |
143 in (name', ths) end) |
133 fun get_time_limit_arg s = |
144 fun get_time_limit_arg s = |
134 (case Int.fromString s of |
145 (case Int.fromString s of |
135 SOME t => Time.fromSeconds t |
146 SOME t => Time.fromSeconds t |
136 | NONE => error ("Invalid time limit: " ^ quote s)) |
147 | NONE => error ("Invalid time limit: " ^ quote s)) |
137 fun get_opt (name, a) (p, t) = |
148 fun get_opt (name, a) (p, t) = |
138 (case name of |
149 (case name of |
139 "time" => (p, get_time_limit_arg a) |
150 "time" => (p, get_time_limit_arg a) |
140 | "atp" => (a, t) |
151 | "atp" => (a, t) |
141 | n => error ("Invalid argument: " ^ n)) |
152 | n => error ("Invalid argument: " ^ n)) |
142 val {atps, minimize_timeout, ...} = default_params thy [] |
153 val {atps, minimize_timeout, ...} = get_params thy override_params |
143 fun get_options args = fold get_opt args (hd atps, minimize_timeout) |
154 val (atp, timeout) = fold get_opt old_style_args (hd atps, minimize_timeout) |
144 val (atp, timeout) = get_options args |
|
145 val params = |
155 val params = |
146 default_params thy |
156 get_params thy |
147 [("atps", atp), |
157 [("atps", [atp]), |
148 ("minimize_timeout", string_of_int (Time.toSeconds timeout) ^ " s")] |
158 ("minimize_timeout", |
|
159 [string_of_int (Time.toSeconds timeout) ^ " s"])] |
149 val prover = |
160 val prover = |
150 (case get_prover thy atp of |
161 (case get_prover thy atp of |
151 SOME prover => prover |
162 SOME prover => prover |
152 | NONE => error ("Unknown ATP: " ^ quote atp)) |
163 | NONE => error ("Unknown ATP: " ^ quote atp)) |
153 val name_thms_pairs = theorems_from_names ctxt thm_names |
164 val name_thms_pairs = theorems_from_refs ctxt fact_refs |
154 in |
165 in |
155 writeln (#2 (minimize_theorems params linear_minimize prover atp state |
166 writeln (#2 (minimize_theorems params linear_minimize prover atp state |
156 name_thms_pairs)) |
167 name_thms_pairs)) |
157 end |
168 end |
158 |
169 |
159 val parse_args = |
170 val runN = "run" |
160 Scan.optional (Args.bracks (P.list (P.xname --| P.$$$ "=" -- P.xname))) [] |
171 val minimizeN = "minimize" |
161 val parse_thm_names = Scan.repeat (P.xname -- Scan.option Attrib.thm_sel) |
172 val messagesN = "messages" |
162 val _ = |
173 val available_atpsN = "available_atps" |
163 OuterSyntax.improper_command "atp_minimize" |
174 val running_atpsN = "running_atps" |
164 "minimize theorem list with external prover" K.diag |
175 val kill_atpsN = "kill_atps" |
165 (parse_args -- parse_thm_names >> (fn (args, thm_names) => |
176 val refresh_tptpN = "refresh_tptp" |
166 Toplevel.no_timing o Toplevel.unknown_proof o |
177 val helpN = "help" |
167 Toplevel.keep (atp_minimize_command args thm_names o Toplevel.proof_of))) |
178 |
168 |
179 val addN = "add" |
169 fun hammer_away override_params i state = |
180 val delN = "del" |
|
181 val onlyN = "only" |
|
182 |
|
183 fun hammer_away override_params subcommand opt_i (Facta f) state = |
170 let |
184 let |
171 val thy = Proof.theory_of state |
185 val thy = Proof.theory_of state |
172 val _ = List.app check_raw_param override_params |
186 val _ = List.app check_raw_param override_params |
173 val params = extract_params thy (default_raw_params thy) override_params |
187 in |
174 in sledgehammer params i state end |
188 if subcommand = runN then |
175 |
189 sledgehammer (get_params thy override_params) (the_default 1 opt_i) state |
176 fun sledgehammer_trans (opt_params, opt_i) = |
190 else if subcommand = minimizeN then |
177 Toplevel.keep (hammer_away (these opt_params) (the_default 1 opt_i) |
191 atp_minimize_command override_params [] (#add f) state |
178 o Toplevel.proof_of) |
192 else if subcommand = messagesN then |
|
193 messages opt_i |
|
194 else if subcommand = available_atpsN then |
|
195 available_atps thy |
|
196 else if subcommand = running_atpsN then |
|
197 running_atps () |
|
198 else if subcommand = kill_atpsN then |
|
199 kill_atps () |
|
200 else if subcommand = refresh_tptpN then |
|
201 refresh_systems_on_tptp () |
|
202 else |
|
203 error ("Unknown subcommand: " ^ quote subcommand ^ ".") |
|
204 end |
|
205 |
|
206 fun sledgehammer_trans (((params, subcommand), opt_i), facta) = |
|
207 Toplevel.keep (hammer_away params subcommand opt_i facta o Toplevel.proof_of) |
179 |
208 |
180 fun string_for_raw_param (name, value) = name ^ " = " ^ space_implode " " value |
209 fun string_for_raw_param (name, value) = name ^ " = " ^ space_implode " " value |
181 |
210 |
182 fun sledgehammer_params_trans opt_params = |
211 fun sledgehammer_params_trans params = |
183 Toplevel.theory |
212 Toplevel.theory |
184 (fold set_default_raw_param (these opt_params) |
213 (fold set_default_raw_param params |
185 #> tap (fn thy => |
214 #> tap (fn thy => |
186 writeln ("Default parameters for Sledgehammer:\n" ^ |
215 writeln ("Default parameters for Sledgehammer:\n" ^ |
187 (case rev (default_raw_params thy) of |
216 (case rev (default_raw_params thy) of |
188 [] => "none" |
217 [] => "none" |
189 | params => |
218 | params => |
193 |
222 |
194 val parse_key = Scan.repeat1 P.typ_group >> space_implode " " |
223 val parse_key = Scan.repeat1 P.typ_group >> space_implode " " |
195 val parse_value = |
224 val parse_value = |
196 Scan.repeat1 (P.minus >> single |
225 Scan.repeat1 (P.minus >> single |
197 || Scan.repeat1 (Scan.unless P.minus P.name)) >> flat |
226 || Scan.repeat1 (Scan.unless P.minus P.name)) >> flat |
198 val parse_param = |
227 val parse_param = parse_key -- Scan.optional (P.$$$ "=" |-- parse_value) [] |
199 parse_key -- (Scan.option (P.$$$ "=" |-- parse_value) >> these) |
228 val parse_params = Scan.optional (Args.bracks (P.list parse_param)) [] |
200 val parse_params = |
229 val parse_fact_refs = |
201 Scan.option (P.$$$ "[" |-- P.list parse_param --| P.$$$ "]") |
230 Scan.repeat (P.xname -- Scan.option Attrib.thm_sel |
|
231 >> (fn (name, interval) => |
|
232 Facts.Named ((name, Position.none), interval))) |
|
233 val parse_slew = |
|
234 (Args.add |-- Args.colon |-- parse_fact_refs >> add_to_facta) |
|
235 || (Args.del |-- Args.colon |-- parse_fact_refs >> del_from_facta) |
|
236 || (P.$$$ onlyN |-- Args.colon |-- parse_fact_refs >> only_facta) |
|
237 val parse_facta = |
|
238 Args.parens (Scan.optional (parse_fact_refs >> only_facta) default_facta |
|
239 -- Scan.repeat parse_slew) >> op :: >> merge_facta |
202 val parse_sledgehammer_command = |
240 val parse_sledgehammer_command = |
203 (parse_params -- Scan.option P.nat) #>> sledgehammer_trans |
241 (parse_params -- Scan.optional P.name runN -- Scan.option P.nat |
|
242 -- parse_facta) |
|
243 #>> sledgehammer_trans |
204 val parse_sledgehammer_params_command = |
244 val parse_sledgehammer_params_command = |
205 parse_params #>> sledgehammer_params_trans |
245 parse_params #>> sledgehammer_params_trans |
206 |
246 |
|
247 val parse_minimize_args = |
|
248 Scan.optional (Args.bracks (P.list (P.xname --| P.$$$ "=" -- P.xname))) [] |
|
249 |
207 val _ = |
250 val _ = |
208 OuterSyntax.improper_command "atp_kill" "kill all managed provers" K.diag |
251 OuterSyntax.improper_command "atp_kill" "kill all managed provers" K.diag |
209 (Scan.succeed (Toplevel.no_timing o Toplevel.imperative kill)) |
252 (Scan.succeed (Toplevel.no_timing o Toplevel.imperative kill_atps)) |
210 val _ = |
253 val _ = |
211 OuterSyntax.improper_command "atp_info" |
254 OuterSyntax.improper_command "atp_info" |
212 "print information about managed provers" K.diag |
255 "print information about managed provers" K.diag |
213 (Scan.succeed (Toplevel.no_timing o Toplevel.imperative info)) |
256 (Scan.succeed (Toplevel.no_timing o Toplevel.imperative running_atps)) |
214 val _ = |
257 val _ = |
215 OuterSyntax.improper_command "atp_messages" |
258 OuterSyntax.improper_command "atp_messages" |
216 "print recent messages issued by managed provers" K.diag |
259 "print recent messages issued by managed provers" K.diag |
217 (Scan.option (P.$$$ "(" |-- P.nat --| P.$$$ ")") >> |
260 (Scan.option (P.$$$ "(" |-- P.nat --| P.$$$ ")") >> |
218 (fn limit => Toplevel.no_timing |
261 (fn limit => Toplevel.no_timing |
219 o Toplevel.imperative (fn () => messages limit))) |
262 o Toplevel.imperative (fn () => messages limit))) |
220 val _ = |
263 val _ = |
221 OuterSyntax.improper_command "print_atps" "print external provers" K.diag |
264 OuterSyntax.improper_command "print_atps" "print external provers" K.diag |
222 (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_theory o |
265 (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_theory o |
223 Toplevel.keep (print_provers o Toplevel.theory_of))) |
266 Toplevel.keep (available_atps o Toplevel.theory_of))) |
|
267 val _ = |
|
268 OuterSyntax.improper_command "atp_minimize" |
|
269 "minimize theorem list with external prover" K.diag |
|
270 (parse_minimize_args -- parse_fact_refs >> (fn (args, fact_refs) => |
|
271 Toplevel.no_timing o Toplevel.unknown_proof o |
|
272 Toplevel.keep (atp_minimize_command [] args fact_refs |
|
273 o Toplevel.proof_of))) |
|
274 |
224 val _ = |
275 val _ = |
225 OuterSyntax.improper_command "sledgehammer" |
276 OuterSyntax.improper_command "sledgehammer" |
226 "search for first-order proof using automatic theorem provers" K.diag |
277 "search for first-order proof using automatic theorem provers" K.diag |
227 parse_sledgehammer_command |
278 parse_sledgehammer_command |
228 val _ = |
279 val _ = |