5 Export Isabelle theory information for MaSh (Machine-learning for Sledgehammer). |
5 Export Isabelle theory information for MaSh (Machine-learning for Sledgehammer). |
6 *) |
6 *) |
7 |
7 |
8 signature MASH_EXPORT = |
8 signature MASH_EXPORT = |
9 sig |
9 sig |
10 type stature = ATP_Problem_Generate.stature |
10 type params = Sledgehammer_Provers.params |
11 type prover_result = Sledgehammer_Provers.prover_result |
|
12 |
11 |
13 val non_tautological_facts_of : |
|
14 theory -> (((unit -> string) * stature) * thm) list |
|
15 val theory_ord : theory * theory -> order |
|
16 val thm_ord : thm * thm -> order |
|
17 val dependencies_of : string list -> thm -> string list |
|
18 val goal_of_thm : theory -> thm -> thm |
|
19 val meng_paulson_facts : |
|
20 Proof.context -> int -> thm -> (((unit -> string) * stature) * thm) list |
|
21 -> ((string * stature) * thm) list |
|
22 val run_sledgehammer : |
|
23 Proof.context -> ((string * stature) * thm) list -> thm -> prover_result |
|
24 val generate_accessibility : theory -> bool -> string -> unit |
|
25 val generate_features : theory -> bool -> string -> unit |
|
26 val generate_isa_dependencies : theory -> bool -> string -> unit |
|
27 val generate_atp_dependencies : |
|
28 Proof.context -> theory -> bool -> string -> unit |
|
29 val generate_commands : theory -> string -> unit |
12 val generate_commands : theory -> string -> unit |
30 val generate_meng_paulson_suggestions : |
13 val generate_iter_suggestions : |
31 Proof.context -> theory -> int -> string -> unit |
14 Proof.context -> params -> theory -> int -> string -> unit |
32 end; |
15 end; |
33 |
16 |
34 structure MaSh_Export : MASH_EXPORT = |
17 structure MaSh_Export : MASH_EXPORT = |
35 struct |
18 struct |
36 |
19 |
37 open ATP_Util |
20 open Sledgehammer_Filter_MaSh |
38 open ATP_Problem_Generate |
|
39 open ATP_Theory_Export |
|
40 |
|
41 type prover_result = Sledgehammer_Provers.prover_result |
|
42 |
|
43 fun stringN_of_int 0 _ = "" |
|
44 | stringN_of_int k n = |
|
45 stringN_of_int (k - 1) (n div 10) ^ string_of_int (n mod 10) |
|
46 |
|
47 fun escape_meta_char c = |
|
48 if Char.isAlphaNum c orelse c = #"_" orelse c = #"." orelse c = #"(" orelse |
|
49 c = #")" orelse c = #"," then |
|
50 String.str c |
|
51 else |
|
52 (* fixed width, in case more digits follow *) |
|
53 "\\" ^ stringN_of_int 3 (Char.ord c) |
|
54 |
|
55 val escape_meta = String.translate escape_meta_char |
|
56 |
|
57 val thy_prefix = "y_" |
|
58 |
|
59 val fact_name_of = escape_meta |
|
60 val thy_name_of = prefix thy_prefix o escape_meta |
|
61 val const_name_of = prefix const_prefix o escape_meta |
|
62 val type_name_of = prefix type_const_prefix o escape_meta |
|
63 val class_name_of = prefix class_prefix o escape_meta |
|
64 |
|
65 val thy_name_of_thm = theory_of_thm #> Context.theory_name |
|
66 |
|
67 local |
|
68 |
|
69 fun has_bool @{typ bool} = true |
|
70 | has_bool (Type (_, Ts)) = exists has_bool Ts |
|
71 | has_bool _ = false |
|
72 |
|
73 fun has_fun (Type (@{type_name fun}, _)) = true |
|
74 | has_fun (Type (_, Ts)) = exists has_fun Ts |
|
75 | has_fun _ = false |
|
76 |
|
77 val is_conn = member (op =) |
|
78 [@{const_name Trueprop}, @{const_name HOL.conj}, @{const_name HOL.disj}, |
|
79 @{const_name HOL.implies}, @{const_name Not}, |
|
80 @{const_name All}, @{const_name Ex}, @{const_name Ball}, @{const_name Bex}, |
|
81 @{const_name HOL.eq}] |
|
82 |
|
83 val has_bool_arg_const = |
|
84 exists_Const (fn (c, T) => |
|
85 not (is_conn c) andalso exists has_bool (binder_types T)) |
|
86 |
|
87 fun higher_inst_const thy (c, T) = |
|
88 case binder_types T of |
|
89 [] => false |
|
90 | Ts => length (binder_types (Sign.the_const_type thy c)) <> length Ts |
|
91 |
|
92 val binders = [@{const_name All}, @{const_name Ex}] |
|
93 |
|
94 in |
|
95 |
|
96 fun is_fo_term thy t = |
|
97 let |
|
98 val t = |
|
99 t |> Envir.beta_eta_contract |
|
100 |> transform_elim_prop |
|
101 |> Object_Logic.atomize_term thy |
|
102 in |
|
103 Term.is_first_order binders t andalso |
|
104 not (exists_subterm (fn Var (_, T) => has_bool T orelse has_fun T |
|
105 | _ => false) t orelse |
|
106 has_bool_arg_const t orelse exists_Const (higher_inst_const thy) t) |
|
107 end |
|
108 |
|
109 end |
|
110 |
|
111 fun interesting_terms_types_and_classes term_max_depth type_max_depth t = |
|
112 let |
|
113 val bad_types = [@{type_name prop}, @{type_name bool}, @{type_name fun}] |
|
114 val bad_consts = atp_widely_irrelevant_consts |
|
115 fun do_add_type (Type (s, Ts)) = |
|
116 (not (member (op =) bad_types s) ? insert (op =) (type_name_of s)) |
|
117 #> fold do_add_type Ts |
|
118 | do_add_type (TFree (_, S)) = union (op =) (map class_name_of S) |
|
119 | do_add_type (TVar (_, S)) = union (op =) (map class_name_of S) |
|
120 fun add_type T = type_max_depth >= 0 ? do_add_type T |
|
121 fun mk_app s args = |
|
122 if member (op <>) args "" then s ^ "(" ^ space_implode "," args ^ ")" |
|
123 else s |
|
124 fun patternify ~1 _ = "" |
|
125 | patternify depth t = |
|
126 case strip_comb t of |
|
127 (Const (s, _), args) => |
|
128 mk_app (const_name_of s) (map (patternify (depth - 1)) args) |
|
129 | _ => "" |
|
130 fun add_term_patterns ~1 _ = I |
|
131 | add_term_patterns depth t = |
|
132 insert (op =) (patternify depth t) |
|
133 #> add_term_patterns (depth - 1) t |
|
134 val add_term = add_term_patterns term_max_depth |
|
135 fun add_patterns t = |
|
136 let val (head, args) = strip_comb t in |
|
137 (case head of |
|
138 Const (s, T) => |
|
139 not (member (op =) bad_consts s) ? (add_term t #> add_type T) |
|
140 | Free (_, T) => add_type T |
|
141 | Var (_, T) => add_type T |
|
142 | Abs (_, T, body) => add_type T #> add_patterns body |
|
143 | _ => I) |
|
144 #> fold add_patterns args |
|
145 end |
|
146 in [] |> add_patterns t |> sort string_ord end |
|
147 |
|
148 fun is_likely_tautology th = |
|
149 null (interesting_terms_types_and_classes 0 ~1 (prop_of th)) andalso |
|
150 not (Thm.eq_thm_prop (@{thm ext}, th)) |
|
151 |
|
152 fun is_too_meta thy th = |
|
153 fastype_of (Object_Logic.atomize_term thy (prop_of th)) <> @{typ bool} |
|
154 |
|
155 fun non_tautological_facts_of thy = |
|
156 all_facts_of_theory thy |
|
157 |> filter_out ((is_likely_tautology orf is_too_meta thy) o snd) |
|
158 |
|
159 fun theory_ord p = |
|
160 if Theory.eq_thy p then EQUAL |
|
161 else if Theory.subthy p then LESS |
|
162 else if Theory.subthy (swap p) then GREATER |
|
163 else EQUAL |
|
164 |
|
165 val thm_ord = theory_ord o pairself theory_of_thm |
|
166 |
|
167 fun thms_by_thy ths = |
|
168 ths |> map (snd #> `thy_name_of_thm) |
|
169 |> AList.group (op =) |
|
170 |> sort (int_ord o pairself (length o Theory.ancestors_of o theory_of_thm |
|
171 o hd o snd)) |
|
172 |> map (apsnd (sort thm_ord)) |
|
173 |
|
174 fun has_thy thy th = (Context.theory_name thy = thy_name_of_thm th) |
|
175 |
|
176 fun parent_thms thy_ths thy = |
|
177 Theory.parents_of thy |
|
178 |> map Context.theory_name |
|
179 |> map_filter (AList.lookup (op =) thy_ths) |
|
180 |> map List.last |
|
181 |> map (fact_name_of o Thm.get_name_hint) |
|
182 |
|
183 fun is_exists (s, _) = (s = @{const_name Ex} orelse s = @{const_name Ex1}) |
|
184 |
|
185 val max_depth = 1 |
|
186 |
|
187 (* TODO: Generate type classes for types? *) |
|
188 fun features_of thy (status, th) = |
|
189 let val t = Thm.prop_of th in |
|
190 thy_name_of (thy_name_of_thm th) :: |
|
191 interesting_terms_types_and_classes max_depth max_depth t |
|
192 |> not (has_no_lambdas t) ? cons "lambdas" |
|
193 |> exists_Const is_exists t ? cons "skolems" |
|
194 |> not (is_fo_term thy t) ? cons "ho" |
|
195 |> (case status of |
|
196 General => I |
|
197 | Induction => cons "induction" |
|
198 | Intro => cons "intro" |
|
199 | Inductive => cons "inductive" |
|
200 | Elim => cons "elim" |
|
201 | Simp => cons "simp" |
|
202 | Def => cons "def") |
|
203 end |
|
204 |
|
205 fun dependencies_of all_facts = |
|
206 theorems_mentioned_in_proof_term (SOME all_facts) |
|
207 #> map fact_name_of |
|
208 #> sort string_ord |
|
209 |
|
210 val freezeT = Type.legacy_freeze_type |
|
211 |
|
212 fun freeze (t $ u) = freeze t $ freeze u |
|
213 | freeze (Abs (s, T, t)) = Abs (s, freezeT T, freeze t) |
|
214 | freeze (Var ((s, _), T)) = Free (s, freezeT T) |
|
215 | freeze (Const (s, T)) = Const (s, freezeT T) |
|
216 | freeze (Free (s, T)) = Free (s, freezeT T) |
|
217 | freeze t = t |
|
218 |
|
219 fun goal_of_thm thy = prop_of #> freeze #> cterm_of thy #> Goal.init |
|
220 |
|
221 fun meng_paulson_facts ctxt max_relevant goal = |
|
222 let |
|
223 val {provers, relevance_thresholds, ...} = |
|
224 Sledgehammer_Isar.default_params ctxt [] |
|
225 val prover_name = hd provers |
|
226 val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal 1 |
|
227 val is_built_in_const = |
|
228 Sledgehammer_Provers.is_built_in_const_for_prover ctxt prover_name |
|
229 val relevance_fudge = |
|
230 Sledgehammer_Provers.relevance_fudge_for_prover ctxt prover_name |
|
231 val relevance_override = {add = [], del = [], only = false} |
|
232 in |
|
233 Sledgehammer_Filter.relevant_facts ctxt relevance_thresholds |
|
234 max_relevant is_built_in_const relevance_fudge relevance_override [] |
|
235 hyp_ts concl_t |
|
236 end |
|
237 |
|
238 fun run_sledgehammer ctxt facts goal = |
|
239 let |
|
240 val params as {provers, ...} = Sledgehammer_Isar.default_params ctxt [] |
|
241 val problem = |
|
242 {state = Proof.init ctxt, goal = goal, subgoal = 1, subgoal_count = 1, |
|
243 facts = facts |> map Sledgehammer_Provers.Untranslated_Fact} |
|
244 val prover = |
|
245 Sledgehammer_Minimize.get_minimizing_prover ctxt |
|
246 Sledgehammer_Provers.Normal (hd provers) |
|
247 in prover params (K (K (K ""))) problem end |
|
248 |
|
249 fun generate_accessibility thy include_thy file_name = |
|
250 let |
|
251 val path = file_name |> Path.explode |
|
252 val _ = File.write path "" |
|
253 fun do_thm th prevs = |
|
254 let |
|
255 val s = th ^ ": " ^ space_implode " " prevs ^ "\n" |
|
256 val _ = File.append path s |
|
257 in [th] end |
|
258 val thy_ths = |
|
259 non_tautological_facts_of thy |
|
260 |> not include_thy ? filter_out (has_thy thy o snd) |
|
261 |> thms_by_thy |
|
262 fun do_thy ths = |
|
263 let |
|
264 val thy = theory_of_thm (hd ths) |
|
265 val parents = parent_thms thy_ths thy |
|
266 val ths = ths |> map (fact_name_of o Thm.get_name_hint) |
|
267 in fold do_thm ths parents; () end |
|
268 in List.app (do_thy o snd) thy_ths end |
|
269 |
|
270 fun generate_features thy include_thy file_name = |
|
271 let |
|
272 val path = file_name |> Path.explode |
|
273 val _ = File.write path "" |
|
274 val facts = |
|
275 non_tautological_facts_of thy |
|
276 |> not include_thy ? filter_out (has_thy thy o snd) |
|
277 fun do_fact ((_, (_, status)), th) = |
|
278 let |
|
279 val name = Thm.get_name_hint th |
|
280 val feats = features_of thy (status, th) |
|
281 val s = fact_name_of name ^ ": " ^ space_implode " " feats ^ "\n" |
|
282 in File.append path s end |
|
283 in List.app do_fact facts end |
|
284 |
|
285 fun generate_isa_dependencies thy include_thy file_name = |
|
286 let |
|
287 val path = file_name |> Path.explode |
|
288 val _ = File.write path "" |
|
289 val ths = |
|
290 non_tautological_facts_of thy |
|
291 |> not include_thy ? filter_out (has_thy thy o snd) |
|
292 |> map snd |
|
293 val all_names = ths |> map Thm.get_name_hint |
|
294 fun do_thm th = |
|
295 let |
|
296 val name = Thm.get_name_hint th |
|
297 val deps = dependencies_of all_names th |
|
298 val s = fact_name_of name ^ ": " ^ space_implode " " deps ^ "\n" |
|
299 in File.append path s end |
|
300 in List.app do_thm ths end |
|
301 |
|
302 fun generate_atp_dependencies ctxt thy include_thy file_name = |
|
303 let |
|
304 val {max_relevant, ...} = Sledgehammer_Isar.default_params ctxt [] |
|
305 val path = file_name |> Path.explode |
|
306 val _ = File.write path "" |
|
307 val facts = |
|
308 non_tautological_facts_of thy |
|
309 |> not include_thy ? filter_out (has_thy thy o snd) |
|
310 val ths = facts |> map snd |
|
311 val all_names = ths |> map Thm.get_name_hint |
|
312 fun is_dep dep (_, th) = fact_name_of (Thm.get_name_hint th) = dep |
|
313 fun add_isa_dep facts dep accum = |
|
314 if exists (is_dep dep) accum then |
|
315 accum |
|
316 else case find_first (is_dep dep) facts of |
|
317 SOME ((name, status), th) => accum @ [((name (), status), th)] |
|
318 | NONE => accum (* shouldn't happen *) |
|
319 fun fix_name ((_, stature), th) = |
|
320 ((th |> Thm.get_name_hint |> fact_name_of, stature), th) |
|
321 fun do_thm th = |
|
322 let |
|
323 val name = Thm.get_name_hint th |
|
324 val goal = goal_of_thm thy th |
|
325 val deps = |
|
326 case dependencies_of all_names th of |
|
327 [] => [] |
|
328 | isa_dep as [_] => isa_dep (* can hardly beat that *) |
|
329 | isa_deps => |
|
330 let |
|
331 val facts = |
|
332 facts |> filter (fn (_, th') => thm_ord (th', th) = LESS) |
|
333 val facts = |
|
334 facts |> meng_paulson_facts ctxt (the max_relevant) goal |
|
335 |> fold (add_isa_dep facts) isa_deps |
|
336 |> map fix_name |
|
337 in |
|
338 case run_sledgehammer ctxt facts goal of |
|
339 {outcome = NONE, used_facts, ...} => |
|
340 used_facts |> map fst |> sort string_ord |
|
341 | _ => isa_deps |
|
342 end |
|
343 val s = fact_name_of name ^ ": " ^ space_implode " " deps ^ "\n" |
|
344 in File.append path s end |
|
345 in List.app do_thm ths end |
|
346 |
21 |
347 fun generate_commands thy file_name = |
22 fun generate_commands thy file_name = |
348 let |
23 let |
349 val path = file_name |> Path.explode |
24 val path = file_name |> Path.explode |
350 val _ = File.write path "" |
25 val _ = File.write path "" |
351 val facts = non_tautological_facts_of thy |
26 val facts = all_non_tautological_facts_of thy |
352 val (new_facts, old_facts) = |
27 val (new_facts, old_facts) = |
353 facts |> List.partition (has_thy thy o snd) |
28 facts |> List.partition (has_thy thy o snd) |
354 |>> sort (thm_ord o pairself snd) |
29 |>> sort (thm_ord o pairself snd) |
355 val ths = facts |> map snd |
30 val ths = facts |> map snd |
356 val all_names = ths |> map Thm.get_name_hint |
31 val all_names = ths |> map Thm.get_name_hint |
357 fun do_fact ((_, (_, status)), th) prevs = |
32 fun do_fact ((_, (_, status)), th) prevs = |
358 let |
33 let |
359 val name = Thm.get_name_hint th |
34 val name = Thm.get_name_hint th |
360 val feats = features_of thy (status, th) |
35 val feats = features_of thy (status, th) |
361 val deps = dependencies_of all_names th |
36 val deps = isabelle_dependencies_of all_names th |
362 val kind = Thm.legacy_get_kind th |
37 val kind = Thm.legacy_get_kind th |
363 val name = fact_name_of name |
38 val name = fact_name_of name |
364 val core = |
39 val core = |
365 name ^ ": " ^ space_implode " " prevs ^ "; " ^ space_implode " " feats |
40 name ^ ": " ^ space_implode " " prevs ^ "; " ^ space_implode " " feats |
366 val query = if kind <> "" then "? " ^ core ^ "\n" else "" |
41 val query = if kind <> "" then "? " ^ core ^ "\n" else "" |