1 (* Title: HOL/TPTP/atp_theory_export.ML |
1 (* Title: HOL/TPTP/atp_theory_export.ML |
2 Author: Jasmin Blanchette, TU Muenchen |
2 Author: Jasmin Blanchette, TU Muenchen |
3 Copyright 2011 |
3 Copyright 2011 |
4 |
4 |
5 Export Isabelle theories as MaSh (Machine-learning for Sledgehammer) or as |
5 Export Isabelle theories as first-order TPTP inferences. |
6 first-order TPTP inferences. |
|
7 *) |
6 *) |
8 |
7 |
9 signature ATP_THEORY_EXPORT = |
8 signature ATP_THEORY_EXPORT = |
10 sig |
9 sig |
11 type atp_format = ATP_Problem.atp_format |
10 type atp_format = ATP_Problem.atp_format |
|
11 type stature = Sledgehammer_Filter.stature |
12 |
12 |
13 val theorems_mentioned_in_proof_term : |
13 val theorems_mentioned_in_proof_term : |
14 string list option -> thm -> string list |
14 string list option -> thm -> string list |
15 val generate_mash_accessibility_file_for_theory : |
15 val all_facts_of_theory : theory -> (((unit -> string) * stature) * thm) list |
16 theory -> bool -> string -> unit |
16 val generate_atp_inference_file_for_theory : |
17 val generate_mash_feature_file_for_theory : theory -> bool -> string -> unit |
|
18 val generate_mash_dependency_file_for_theory : |
|
19 theory -> bool -> string -> unit |
|
20 val generate_mash_problem_file_for_theory : theory -> string -> unit |
|
21 val generate_tptp_inference_file_for_theory : |
|
22 Proof.context -> theory -> atp_format -> string -> string -> unit |
17 Proof.context -> theory -> atp_format -> string -> string -> unit |
23 end; |
18 end; |
24 |
19 |
25 structure ATP_Theory_Export (* ### : ATP_THEORY_EXPORT *) = |
20 structure ATP_Theory_Export : ATP_THEORY_EXPORT = |
26 struct |
21 struct |
27 |
22 |
28 open ATP_Problem |
23 open ATP_Problem |
29 open ATP_Proof |
24 open ATP_Proof |
30 open ATP_Problem_Generate |
25 open ATP_Problem_Generate |
31 open ATP_Systems |
26 open ATP_Systems |
32 open ATP_Util |
27 |
33 |
28 val fact_name_of = prefix fact_prefix o ascii_of |
34 fun stringN_of_int 0 _ = "" |
|
35 | stringN_of_int k n = |
|
36 stringN_of_int (k - 1) (n div 10) ^ string_of_int (n mod 10) |
|
37 |
|
38 fun escape_meta_char c = |
|
39 if Char.isAlphaNum c orelse c = #"_" orelse c = #"." orelse c = #"(" orelse |
|
40 c = #")" orelse c = #"," then |
|
41 String.str c |
|
42 else if c = #"'" then |
|
43 "~" |
|
44 else |
|
45 (* fixed width, in case more digits follow *) |
|
46 "\\" ^ stringN_of_int 3 (Char.ord c) |
|
47 val escape_meta = String.translate escape_meta_char |
|
48 |
|
49 val thy_prefix = "y_" |
|
50 |
|
51 val fact_name_of = escape_meta |
|
52 val thy_name_of = prefix thy_prefix o escape_meta |
|
53 val const_name_of = prefix const_prefix o escape_meta |
|
54 val type_name_of = prefix type_const_prefix o escape_meta |
|
55 val class_name_of = prefix class_prefix o escape_meta |
|
56 |
|
57 val thy_name_of_thm = theory_of_thm #> Context.theory_name |
|
58 |
|
59 fun has_thy thy th = (Context.theory_name thy = thy_name_of_thm th) |
|
60 |
29 |
61 (* FIXME: Similar yet different code in "mirabelle.ML". The code here has a few |
30 (* FIXME: Similar yet different code in "mirabelle.ML". The code here has a few |
62 fixes that seem to be missing over there; or maybe the two code portions are |
31 fixes that seem to be missing over there; or maybe the two code portions are |
63 not doing the same? *) |
32 not doing the same? *) |
64 fun fold_body_thms thm_name f = |
33 fun fold_body_thms thm_name f = |
86 SOME names => member (op =) names |
55 SOME names => member (op =) names |
87 | NONE => (fn s => s <> "" andalso not (String.isPrefix "Pure." s)) |
56 | NONE => (fn s => s <> "" andalso not (String.isPrefix "Pure." s)) |
88 fun collect (s, _, _) = is_name_ok s ? insert (op =) s |
57 fun collect (s, _, _) = is_name_ok s ? insert (op =) s |
89 val names = |
58 val names = |
90 [] |> fold_body_thms (Thm.get_name_hint th) collect [Thm.proof_body_of th] |
59 [] |> fold_body_thms (Thm.get_name_hint th) collect [Thm.proof_body_of th] |
91 |> map fact_name_of |
|
92 in names end |
60 in names end |
93 |
61 |
94 fun interesting_terms_types_and_classes term_max_depth type_max_depth t = |
62 fun all_facts_of_theory thy = |
95 let |
|
96 val bad_types = [@{type_name prop}, @{type_name bool}, @{type_name fun}] |
|
97 val bad_consts = atp_widely_irrelevant_consts |
|
98 val add_classes = |
|
99 subtract (op =) @{sort type} #> map class_name_of #> union (op =) |
|
100 fun do_add_type (Type (s, Ts)) = |
|
101 (not (member (op =) bad_types s) ? insert (op =) (type_name_of s)) |
|
102 #> fold do_add_type Ts |
|
103 | do_add_type (TFree (_, S)) = add_classes S |
|
104 | do_add_type (TVar (_, S)) = add_classes S |
|
105 fun add_type T = type_max_depth >= 0 ? do_add_type T |
|
106 fun mk_app s args = |
|
107 if member (op <>) args "" then s ^ "(" ^ space_implode "," args ^ ")" |
|
108 else s |
|
109 fun patternify ~1 _ = "" |
|
110 | patternify depth t = |
|
111 case strip_comb t of |
|
112 (Const (s, _), args) => |
|
113 mk_app (const_name_of s) (map (patternify (depth - 1)) args) |
|
114 | _ => "" |
|
115 fun add_term_patterns ~1 _ = I |
|
116 | add_term_patterns depth t = |
|
117 insert (op =) (patternify depth t) |
|
118 #> add_term_patterns (depth - 1) t |
|
119 val add_term = add_term_patterns term_max_depth |
|
120 fun add_patterns t = |
|
121 let val (head, args) = strip_comb t in |
|
122 (case head of |
|
123 Const (s, T) => |
|
124 not (member (op =) bad_consts s) ? (add_term t #> add_type T) |
|
125 | Free (_, T) => add_type T |
|
126 | Var (_, T) => add_type T |
|
127 | Abs (_, T, body) => add_type T #> add_patterns body |
|
128 | _ => I) |
|
129 #> fold add_patterns args |
|
130 end |
|
131 in [] |> add_patterns t |> sort string_ord end |
|
132 |
|
133 fun is_likely_tautology th = |
|
134 null (interesting_terms_types_and_classes 0 ~1 (prop_of th)) andalso |
|
135 not (Thm.eq_thm_prop (@{thm ext}, th)) |
|
136 |
|
137 fun is_too_meta thy th = |
|
138 fastype_of (Object_Logic.atomize_term thy (prop_of th)) <> @{typ bool} |
|
139 |
|
140 fun facts_of thy = |
|
141 let val ctxt = Proof_Context.init_global thy in |
63 let val ctxt = Proof_Context.init_global thy in |
142 Sledgehammer_Filter.all_facts ctxt false Symtab.empty true [] [] |
64 Sledgehammer_Filter.all_facts ctxt false Symtab.empty true [] [] |
143 (Sledgehammer_Filter.clasimpset_rule_table_of ctxt) |
65 (Sledgehammer_Filter.clasimpset_rule_table_of ctxt) |
144 |> filter_out ((is_likely_tautology orf is_too_meta thy) o snd) |
|
145 |> rev |
|
146 end |
66 end |
147 |
|
148 fun theory_ord p = |
|
149 if Theory.eq_thy p then EQUAL |
|
150 else if Theory.subthy p then LESS |
|
151 else if Theory.subthy (swap p) then GREATER |
|
152 else EQUAL |
|
153 |
|
154 val thm_ord = theory_ord o pairself theory_of_thm |
|
155 |
|
156 fun parent_thms thy_ths thy = |
|
157 Theory.parents_of thy |
|
158 |> map Context.theory_name |
|
159 |> map_filter (AList.lookup (op =) thy_ths) |
|
160 |> map List.last |
|
161 |> map (fact_name_of o Thm.get_name_hint) |
|
162 |
|
163 val thms_by_thy = |
|
164 map (snd #> `thy_name_of_thm) |
|
165 #> AList.group (op =) |
|
166 #> sort (int_ord |
|
167 o pairself (length o Theory.ancestors_of o theory_of_thm o hd o snd)) |
|
168 #> map (apsnd (sort thm_ord)) |
|
169 |
|
170 fun generate_mash_accessibility_file_for_theory thy include_thy file_name = |
|
171 let |
|
172 val path = file_name |> Path.explode |
|
173 val _ = File.write path "" |
|
174 fun do_thm th prevs = |
|
175 let |
|
176 val s = th ^ ": " ^ space_implode " " prevs ^ "\n" |
|
177 val _ = File.append path s |
|
178 in [th] end |
|
179 val thy_ths = |
|
180 facts_of thy |
|
181 |> not include_thy ? filter_out (has_thy thy o snd) |
|
182 |> thms_by_thy |
|
183 fun do_thy ths = |
|
184 let |
|
185 val thy = theory_of_thm (hd ths) |
|
186 val parents = parent_thms thy_ths thy |
|
187 val ths = ths |> map (fact_name_of o Thm.get_name_hint) |
|
188 val _ = fold do_thm ths parents |
|
189 in () end |
|
190 val _ = List.app (do_thy o snd) thy_ths |
|
191 in () end |
|
192 |
|
193 fun has_bool @{typ bool} = true |
|
194 | has_bool (Type (_, Ts)) = exists has_bool Ts |
|
195 | has_bool _ = false |
|
196 |
|
197 fun has_fun (Type (@{type_name fun}, _)) = true |
|
198 | has_fun (Type (_, Ts)) = exists has_fun Ts |
|
199 | has_fun _ = false |
|
200 |
|
201 val is_conn = member (op =) |
|
202 [@{const_name Trueprop}, @{const_name HOL.conj}, @{const_name HOL.disj}, |
|
203 @{const_name HOL.implies}, @{const_name Not}, |
|
204 @{const_name All}, @{const_name Ex}, @{const_name Ball}, @{const_name Bex}, |
|
205 @{const_name HOL.eq}] |
|
206 |
|
207 val has_bool_arg_const = |
|
208 exists_Const (fn (c, T) => |
|
209 not (is_conn c) andalso exists has_bool (binder_types T)) |
|
210 |
|
211 fun higher_inst_const thy (c, T) = |
|
212 case binder_types T of |
|
213 [] => false |
|
214 | Ts => length (binder_types (Sign.the_const_type thy c)) <> length Ts |
|
215 |
|
216 val binders = [@{const_name All}, @{const_name Ex}] |
|
217 |
|
218 fun is_fo_term thy t = |
|
219 let |
|
220 val t = |
|
221 t |> Envir.beta_eta_contract |
|
222 |> transform_elim_prop |
|
223 |> Object_Logic.atomize_term thy |
|
224 in |
|
225 Term.is_first_order binders t andalso |
|
226 not (exists_subterm (fn Var (_, T) => has_bool T orelse has_fun T |
|
227 | _ => false) t orelse |
|
228 has_bool_arg_const t orelse exists_Const (higher_inst_const thy) t) |
|
229 end |
|
230 |
|
231 fun is_exists (s, _) = (s = @{const_name Ex} orelse s = @{const_name Ex1}) |
|
232 |
|
233 val max_depth = 1 |
|
234 |
|
235 fun features_of thy (status, th) = |
|
236 let val t = Thm.prop_of th in |
|
237 thy_name_of (thy_name_of_thm th) :: |
|
238 interesting_terms_types_and_classes max_depth max_depth t |
|
239 |> not (has_no_lambdas t) ? cons "lambdas" |
|
240 |> exists_Const is_exists t ? cons "skolems" |
|
241 |> not (is_fo_term thy t) ? cons "ho" |
|
242 |> (case status of |
|
243 General => I |
|
244 | Induction => cons "induction" |
|
245 | Intro => cons "intro" |
|
246 | Inductive => cons "inductive" |
|
247 | Elim => cons "elim" |
|
248 | Simp => cons "simp" |
|
249 | Def => cons "def") |
|
250 end |
|
251 |
|
252 fun generate_mash_feature_file_for_theory thy include_thy file_name = |
|
253 let |
|
254 val path = file_name |> Path.explode |
|
255 val _ = File.write path "" |
|
256 val facts = facts_of thy |> not include_thy ? filter_out (has_thy thy o snd) |
|
257 fun do_fact ((_, (_, status)), th) = |
|
258 let |
|
259 val name = Thm.get_name_hint th |
|
260 val feats = features_of thy (status, th) |
|
261 val s = fact_name_of name ^ ": " ^ space_implode " " feats ^ "\n" |
|
262 in File.append path s end |
|
263 val _ = List.app do_fact facts |
|
264 in () end |
|
265 |
|
266 val dependencies_of = theorems_mentioned_in_proof_term o SOME |
|
267 |
|
268 fun generate_mash_dependency_file_for_theory thy include_thy file_name = |
|
269 let |
|
270 val path = file_name |> Path.explode |
|
271 val _ = File.write path "" |
|
272 val ths = |
|
273 facts_of thy |> not include_thy ? filter_out (has_thy thy o snd) |
|
274 |> map snd |
|
275 val all_names = ths |> map Thm.get_name_hint |
|
276 fun do_thm th = |
|
277 let |
|
278 val name = Thm.get_name_hint th |
|
279 val deps = dependencies_of all_names th |
|
280 val s = fact_name_of name ^ ": " ^ space_implode " " deps ^ "\n" |
|
281 in File.append path s end |
|
282 val _ = List.app do_thm ths |
|
283 in () end |
|
284 |
|
285 fun generate_mash_problem_file_for_theory thy file_name = |
|
286 let |
|
287 val path = file_name |> Path.explode |
|
288 val _ = File.write path "" |
|
289 val facts = facts_of thy |
|
290 val (new_facts, old_facts) = |
|
291 facts |> List.partition (has_thy thy o snd) |
|
292 |>> sort (thm_ord o pairself snd) |
|
293 val ths = facts |> map snd |
|
294 val all_names = ths |> map Thm.get_name_hint |
|
295 fun do_fact ((_, (_, status)), th) prevs = |
|
296 let |
|
297 val name = Thm.get_name_hint th |
|
298 val feats = features_of thy (status, th) |
|
299 val deps = dependencies_of all_names th |
|
300 val kind = Thm.legacy_get_kind th |
|
301 val name = fact_name_of name |
|
302 val core = |
|
303 name ^ ": " ^ space_implode " " prevs ^ "; " ^ space_implode " " feats |
|
304 val query = if kind <> "" then "? " ^ core ^ "\n" else "" |
|
305 val update = "! " ^ core ^ "; " ^ space_implode " " deps ^ "\n" |
|
306 val _ = File.append path (query ^ update) |
|
307 in [name] end |
|
308 val thy_ths = old_facts |> thms_by_thy |
|
309 val parents = parent_thms thy_ths thy |
|
310 val _ = fold do_fact new_facts parents |
|
311 in () end |
|
312 |
67 |
313 fun inference_term [] = NONE |
68 fun inference_term [] = NONE |
314 | inference_term ss = |
69 | inference_term ss = |
315 ATerm (("inference", []), |
70 ATerm (("inference", []), |
316 [ATerm (("isabelle", []), []), |
71 [ATerm (("isabelle", []), []), |