|
1 (* Title: HOL/TPTP/?/tptp_interpret.ML |
|
2 Author: Nik Sultana, Cambridge University Computer Laboratory |
|
3 |
|
4 Interprets TPTP problems in Isabelle/HOL. |
|
5 *) |
|
6 |
|
7 signature TPTP_INTERPRET = |
|
8 sig |
|
9 (*signature extension: typing information for variables and constants |
|
10 (note that the former isn't really part of the signature, but it's bundled |
|
11 along for more configurability -- though it's probably useless and could be |
|
12 dropped in the future.*) |
|
13 type const_map = (string * term) list |
|
14 type var_types = (string * typ option) list |
|
15 |
|
16 (*mapping from THF types to Isabelle/HOL types. This map works over all |
|
17 base types (i.e. THF functions must be interpreted as Isabelle/HOL functions). |
|
18 The map must be total wrt THF types. Later on there could be a configuration |
|
19 option to make a map extensible.*) |
|
20 type type_map = (TPTP_Syntax.tptp_type * typ) list |
|
21 |
|
22 (*inference info, when available, consists of the name of the inference rule |
|
23 and the names of the inferences involved in the reasoning step.*) |
|
24 type inference_info = (string * string list) option |
|
25 |
|
26 (*a parsed annotated formula is represented as a triple consisting of |
|
27 the formula's label, its role, and a constant function to its Isabelle/HOL |
|
28 term meaning*) |
|
29 type tptp_formula_meaning = |
|
30 string * TPTP_Syntax.role * TPTP_Syntax.tptp_formula * term * inference_info |
|
31 |
|
32 (*In general, the meaning of a TPTP statement (which, through the Include |
|
33 directive, may include the meaning of an entire TPTP file, is an extended |
|
34 Isabelle/HOL theory, an explicit map from constants to their Isabelle/HOL |
|
35 counterparts and their types, the meaning of any TPTP formulas encountered |
|
36 while interpreting that statement, and a map from THF to Isabelle/HOL types |
|
37 (these types would have been added to the theory returned in the first position |
|
38 of the tuple). The last value is NONE when the function which produced the |
|
39 whole tptp_general_meaning value was given a type_map argument -- since |
|
40 this means that the type_map is already known, and it has not been changed.*) |
|
41 type tptp_general_meaning = |
|
42 (type_map * const_map * tptp_formula_meaning list) |
|
43 |
|
44 (*if problem_name is given then it is used to qualify types & constants*) |
|
45 type config = |
|
46 {(*init_type_map : type_map with_origin, |
|
47 init_const_map : type_map with_origin,*) |
|
48 cautious : bool, |
|
49 problem_name : TPTP_Problem_Name.problem_name option |
|
50 (*dont_build_maps : bool, |
|
51 extend_given_type_map : bool, |
|
52 extend_given_const_map : bool, |
|
53 generative_type_interpretation : bool, |
|
54 generative_const_interpretation : bool*)} |
|
55 |
|
56 (*map types form THF to Isabelle/HOL*) |
|
57 val interpret_type : config -> theory -> type_map -> |
|
58 TPTP_Syntax.tptp_type -> typ |
|
59 |
|
60 (*interpret a TPTP line: return an updated theory including the |
|
61 types & constants which were specified in that formula, a map from |
|
62 constant names to their types, and a map from constant names to Isabelle/HOL |
|
63 constants; and a list possible formulas resulting from that line. |
|
64 Note that type/constant declarations do not result in any formulas being |
|
65 returned. A typical TPTP line might update the theory, or return a single |
|
66 formula. The sole exception is the "include" directive which may update the |
|
67 theory and also return a list of formulas from the included file. |
|
68 Arguments: |
|
69 cautious = indicates whether additional checks are made to check |
|
70 that all used types have been declared. |
|
71 type_map = mapping of THF-types to Isabelle/HOL types. This argument may be |
|
72 given to force a specific mapping: this is usually done for using an |
|
73 imported THF problem in Isar. |
|
74 const_map = as previous, but for constants. |
|
75 path_prefix = path where THF problems etc are located (to help the "include" |
|
76 directive find the files. |
|
77 thy = theory where interpreted info will be stored. |
|
78 *) |
|
79 |
|
80 (*map terms form TPTP to Isabelle/HOL*) |
|
81 val interpret_term : bool -> config -> TPTP_Syntax.language -> theory -> |
|
82 const_map -> var_types -> type_map -> TPTP_Syntax.tptp_term -> |
|
83 term * theory |
|
84 |
|
85 val interpret_formula : config -> TPTP_Syntax.language -> const_map -> |
|
86 var_types -> type_map -> TPTP_Syntax.tptp_formula -> theory -> |
|
87 term * theory |
|
88 |
|
89 val interpret_line : config -> type_map -> const_map -> |
|
90 Path.T -> TPTP_Syntax.tptp_line -> theory -> tptp_general_meaning * theory |
|
91 |
|
92 (*Like "interpret_line" above, but works over a whole parsed problem. |
|
93 Arguments: |
|
94 new_basic_types = indicates whether interpretations of $i and $o |
|
95 types are to be added to the type map (unless it is Given). |
|
96 This is "true" if we are running this over a fresh THF problem, but |
|
97 "false" if we are calling this _during_ the interpretation of a THF file |
|
98 (i.e. when interpreting an "include" directive. |
|
99 config = config |
|
100 path_prefix = " " |
|
101 contents = parsed TPTP syntax |
|
102 type_map = see "interpret_line" |
|
103 const_map = " " |
|
104 thy = " " |
|
105 *) |
|
106 val interpret_problem : bool -> config -> Path.T -> |
|
107 TPTP_Syntax.tptp_line list -> type_map -> const_map -> theory -> |
|
108 tptp_general_meaning * theory |
|
109 |
|
110 (*Like "interpret_problem" above, but it's given a filename rather than |
|
111 a parsed problem.*) |
|
112 val interpret_file : bool -> Path.T -> Path.T -> type_map -> const_map -> |
|
113 theory -> tptp_general_meaning * theory |
|
114 |
|
115 (*General exception for this signature.*) |
|
116 exception MISINTERPRET_FORMULA of string * TPTP_Syntax.tptp_formula |
|
117 exception MISINTERPRET_SYMBOL of string * TPTP_Syntax.symbol |
|
118 exception MISINTERPRET_TERM of string * TPTP_Syntax.tptp_term |
|
119 exception MISINTERPRET_TYPE of string * TPTP_Syntax.tptp_type |
|
120 |
|
121 (*Generates a fresh Isabelle/HOL type for interpreting a THF type in a theory.*) |
|
122 val declare_type : config -> (TPTP_Syntax.tptp_type * string) -> type_map -> |
|
123 theory -> type_map * theory |
|
124 |
|
125 (*Returns the list of all files included in a directory and its |
|
126 subdirectories. This is only used for testing the parser/interpreter against |
|
127 all THF problems.*) |
|
128 val get_file_list : Path.T -> Path.T list |
|
129 |
|
130 type manifest = TPTP_Problem_Name.problem_name * tptp_general_meaning |
|
131 |
|
132 val get_manifests : theory -> manifest list |
|
133 |
|
134 val import_file : bool -> Path.T -> Path.T -> type_map -> const_map -> |
|
135 theory -> theory |
|
136 |
|
137 val extract_inference_info : (TPTP_Syntax.general_term * 'a list) option -> |
|
138 (string * string list) option |
|
139 end |
|
140 |
|
141 structure TPTP_Interpret : TPTP_INTERPRET = |
|
142 struct |
|
143 |
|
144 open TPTP_Syntax |
|
145 exception MISINTERPRET_FORMULA of string * TPTP_Syntax.tptp_formula |
|
146 exception MISINTERPRET_SYMBOL of string * TPTP_Syntax.symbol |
|
147 exception MISINTERPRET_TERM of string * TPTP_Syntax.tptp_term |
|
148 exception MISINTERPRET_TYPE of string * TPTP_Syntax.tptp_type |
|
149 |
|
150 (* General stuff *) |
|
151 |
|
152 type config = |
|
153 {(*init_type_map : type_map with_origin, |
|
154 init_const_map : type_map with_origin,*) |
|
155 cautious : bool, |
|
156 problem_name : TPTP_Problem_Name.problem_name option |
|
157 (*dont_build_maps : bool, |
|
158 extend_given_type_map : bool, |
|
159 extend_given_const_map : bool, |
|
160 generative_type_interpretation : bool, |
|
161 generative_const_interpretation : bool*)} |
|
162 |
|
163 (* Interpretation *) |
|
164 |
|
165 (** Signatures and other type abbrevations **) |
|
166 |
|
167 type const_map = (string * term) list |
|
168 type var_types = (string * typ option) list |
|
169 type type_map = (TPTP_Syntax.tptp_type * typ) list |
|
170 type inference_info = (string * string list) option |
|
171 type tptp_formula_meaning = |
|
172 string * TPTP_Syntax.role * TPTP_Syntax.tptp_formula * term * inference_info |
|
173 type tptp_general_meaning = |
|
174 (type_map * const_map * tptp_formula_meaning list) |
|
175 |
|
176 type manifest = TPTP_Problem_Name.problem_name * tptp_general_meaning |
|
177 structure TPTP_Data = Theory_Data |
|
178 (type T = manifest list |
|
179 val empty = [] |
|
180 val extend = I |
|
181 val merge = Library.merge (op =)) |
|
182 val get_manifests = TPTP_Data.get |
|
183 |
|
184 |
|
185 (** Adding types to a signature **) |
|
186 |
|
187 fun type_exists thy ty_name = |
|
188 Sign.declared_tyname thy (Sign.full_bname thy ty_name) |
|
189 |
|
190 val IND_TYPE = "ind" |
|
191 |
|
192 fun mk_binding config ident = |
|
193 let |
|
194 val pre_binding = Binding.name ident |
|
195 in |
|
196 case #problem_name config of |
|
197 NONE => pre_binding |
|
198 | SOME prob => |
|
199 Binding.qualify |
|
200 false |
|
201 (TPTP_Problem_Name.mangle_problem_name prob) |
|
202 pre_binding |
|
203 end |
|
204 |
|
205 (*Returns updated theory and the name of the final type's name -- i.e. if the |
|
206 original name is already taken then the function looks for an available |
|
207 alternative. It also returns an updated type_map if one has been passed to it.*) |
|
208 fun declare_type (config : config) (thf_type, type_name) ty_map thy = |
|
209 if type_exists thy type_name then |
|
210 raise MISINTERPRET_TYPE ("Type already exists", Atom_type type_name) |
|
211 else |
|
212 let |
|
213 val binding = mk_binding config type_name |
|
214 val final_fqn = Sign.full_name thy binding |
|
215 val thy' = Typedecl.typedecl_global (mk_binding config type_name, [], NoSyn) thy |> snd |
|
216 val typ_map_entry = (thf_type, (Type (final_fqn, []))) |
|
217 val ty_map' = typ_map_entry :: ty_map |
|
218 in (ty_map', thy') end |
|
219 |
|
220 |
|
221 (** Adding constants to signature **) |
|
222 |
|
223 fun full_name thy config const_name = |
|
224 Sign.full_name thy (mk_binding config const_name) |
|
225 |
|
226 fun const_exists config thy const_name = |
|
227 Sign.declared_const thy (full_name thy config const_name) |
|
228 |
|
229 fun declare_constant config const_name ty thy = |
|
230 if const_exists config thy const_name then |
|
231 raise MISINTERPRET_TERM |
|
232 ("Const already declared", Term_Func (Uninterpreted const_name, [])) |
|
233 else |
|
234 Theory.specify_const |
|
235 ((mk_binding config const_name, ty), NoSyn) thy |
|
236 |
|
237 |
|
238 (** Interpretation **) |
|
239 |
|
240 (*Types in THF are encoded as formulas. This function translates them to type form.*) |
|
241 (*FIXME possibly incomplete hack*) |
|
242 fun fmlatype_to_type (Atom (THF_Atom_term (Term_Func (TypeSymbol typ, [])))) = |
|
243 Defined_type typ |
|
244 | fmlatype_to_type (Atom (THF_Atom_term (Term_Func (Uninterpreted str, [])))) = |
|
245 Atom_type str |
|
246 | fmlatype_to_type (THF_type (Fn_type (ty1, ty2))) = |
|
247 let |
|
248 val ty1' = case ty1 of |
|
249 Fn_type _ => fmlatype_to_type (THF_type ty1) |
|
250 | Fmla_type ty1 => fmlatype_to_type ty1 |
|
251 val ty2' = case ty2 of |
|
252 Fn_type _ => fmlatype_to_type (THF_type ty2) |
|
253 | Fmla_type ty2 => fmlatype_to_type ty2 |
|
254 in Fn_type (ty1', ty2') end |
|
255 |
|
256 fun interpret_type config thy type_map thf_ty = |
|
257 let |
|
258 fun lookup_type ty_map thf_ty = |
|
259 (case AList.lookup (op =) ty_map thf_ty of |
|
260 NONE => |
|
261 raise MISINTERPRET_TYPE |
|
262 ("Could not find the interpretation of this TPTP type in the " ^ |
|
263 "mapping to Isabelle/HOL", thf_ty) |
|
264 | SOME ty => ty) |
|
265 in |
|
266 case thf_ty of (*FIXME make tail*) |
|
267 Prod_type (thf_ty1, thf_ty2) => |
|
268 Type ("Product_Type.prod", |
|
269 [interpret_type config thy type_map thf_ty1, |
|
270 interpret_type config thy type_map thf_ty2]) |
|
271 | Fn_type (thf_ty1, thf_ty2) => |
|
272 Type ("fun", |
|
273 [interpret_type config thy type_map thf_ty1, |
|
274 interpret_type config thy type_map thf_ty2]) |
|
275 | Atom_type _ => |
|
276 lookup_type type_map thf_ty |
|
277 | Defined_type tptp_base_type => |
|
278 (case tptp_base_type of |
|
279 Type_Ind => |
|
280 lookup_type type_map thf_ty |
|
281 | Type_Bool => HOLogic.boolT |
|
282 | Type_Type => |
|
283 raise MISINTERPRET_TYPE |
|
284 ("No type interpretation", thf_ty) |
|
285 | Type_Int => Type ("Int.int", []) |
|
286 (*FIXME these types are currently unsupported, so they're treated as |
|
287 individuals*) |
|
288 | Type_Rat => |
|
289 interpret_type config thy type_map (Defined_type Type_Ind) |
|
290 | Type_Real => |
|
291 interpret_type config thy type_map (Defined_type Type_Ind) |
|
292 ) |
|
293 | Sum_type _ => |
|
294 raise MISINTERPRET_TYPE (*FIXME*) |
|
295 ("No type interpretation (sum type)", thf_ty) |
|
296 | Fmla_type tptp_ty => |
|
297 fmlatype_to_type tptp_ty |
|
298 |> interpret_type config thy type_map |
|
299 | Subtype _ => |
|
300 raise MISINTERPRET_TYPE (*FIXME*) |
|
301 ("No type interpretation (subtype)", thf_ty) |
|
302 end |
|
303 |
|
304 fun the_const config thy language const_map_payload str = |
|
305 if language = THF then |
|
306 (case AList.lookup (op =) const_map_payload str of |
|
307 NONE => raise MISINTERPRET_TERM |
|
308 ("Could not find the interpretation of this constant in the " ^ |
|
309 "mapping to Isabelle/HOL", Term_Func (Uninterpreted str, [])) |
|
310 | SOME t => t) |
|
311 else |
|
312 if const_exists config thy str then |
|
313 Sign.mk_const thy ((Sign.full_name thy (mk_binding config str)), []) |
|
314 else raise MISINTERPRET_TERM |
|
315 ("Could not find the interpretation of this constant in the " ^ |
|
316 "mapping to Isabelle/HOL: ", Term_Func (Uninterpreted str, [])) |
|
317 |
|
318 (*Eta-expands Isabelle/HOL binary function. |
|
319 "str" is the name of a polymorphic constant in Isabelle/HOL*) |
|
320 fun mk_fun str = |
|
321 (Const (str, Term.dummyT) $ Bound 1 $ Bound 0) |
|
322 |> (Term.absdummy Term.dummyT #> Term.absdummy Term.dummyT) |
|
323 (*As above, but swaps the function's arguments*) |
|
324 fun mk_swapped_fun str = |
|
325 (Const (str, Term.dummyT) $ Bound 0 $ Bound 1) |
|
326 |> (Term.absdummy Term.dummyT #> Term.absdummy Term.dummyT) |
|
327 |
|
328 fun dummy_THF () = |
|
329 HOLogic.choice_const Term.dummyT $ Term.absdummy Term.dummyT @{term "True"} |
|
330 |
|
331 fun interpret_symbol config thy language const_map symb = |
|
332 case symb of |
|
333 Uninterpreted n => |
|
334 (*Constant would have been added to the map at the time of |
|
335 declaration*) |
|
336 the_const config thy language const_map n |
|
337 | Interpreted_ExtraLogic interpreted_symbol => |
|
338 (case interpreted_symbol of (*FIXME incomplete, |
|
339 and doesn't work with $i*) |
|
340 Sum => mk_fun @{const_name Groups.plus} |
|
341 | UMinus => |
|
342 (Const (@{const_name Groups.uminus}, Term.dummyT) $ Bound 0) |
|
343 |> Term.absdummy Term.dummyT |
|
344 | Difference => mk_fun @{const_name Groups.minus} |
|
345 | Product => mk_fun @{const_name Groups.times} |
|
346 | Quotient => mk_fun @{const_name Fields.divide} |
|
347 | Less => mk_fun @{const_name Orderings.less} |
|
348 | LessEq => mk_fun @{const_name Orderings.less_eq} |
|
349 | Greater => mk_swapped_fun @{const_name Orderings.less} |
|
350 (*FIXME would be nicer to expand "greater" |
|
351 and "greater_eq" abbreviations*) |
|
352 | GreaterEq => mk_swapped_fun @{const_name Orderings.less_eq} |
|
353 (* FIXME todo |
|
354 | Quotient_E | Quotient_T | Quotient_F | Remainder_E | Remainder_T |
|
355 | Remainder_F | Floor | Ceiling | Truncate | Round | To_Int | To_Rat |
|
356 | To_Real | EvalEq | Is_Int | Is_Rat*) |
|
357 | Apply => raise MISINTERPRET_SYMBOL ("Malformed term?", symb) |
|
358 | _ => dummy_THF () |
|
359 ) |
|
360 | Interpreted_Logic logic_symbol => |
|
361 (case logic_symbol of |
|
362 Equals => HOLogic.eq_const Term.dummyT |
|
363 | NEquals => |
|
364 HOLogic.mk_not (HOLogic.eq_const Term.dummyT $ Bound 1 $ Bound 0) |
|
365 |> (Term.absdummy Term.dummyT #> Term.absdummy Term.dummyT) |
|
366 | Or => HOLogic.disj |
|
367 | And => HOLogic.conj |
|
368 | Iff => HOLogic.eq_const HOLogic.boolT |
|
369 | If => HOLogic.imp |
|
370 | Fi => @{term "\<lambda> x. \<lambda> y. y \<longrightarrow> x"} |
|
371 | Xor => |
|
372 @{term |
|
373 "\<lambda> x. \<lambda> y. \<not> (x \<longleftrightarrow> y)"} |
|
374 | Nor => @{term "\<lambda> x. \<lambda> y. \<not> (x \<or> y)"} |
|
375 | Nand => @{term "\<lambda> x. \<lambda> y. \<not> (x \<and> y)"} |
|
376 | Not => HOLogic.Not |
|
377 | Op_Forall => HOLogic.all_const Term.dummyT |
|
378 | Op_Exists => HOLogic.exists_const Term.dummyT |
|
379 | True => @{term "True"} |
|
380 | False => @{term "False"} |
|
381 ) |
|
382 | TypeSymbol _ => |
|
383 raise MISINTERPRET_SYMBOL |
|
384 ("Cannot have TypeSymbol in term", symb) |
|
385 | System str => |
|
386 raise MISINTERPRET_SYMBOL |
|
387 ("How to interpret system terms?", symb) |
|
388 |
|
389 (*Apply a function to a list of arguments*) |
|
390 val mapply = fold (fn x => fn y => y $ x) |
|
391 (*As above, but for products*) |
|
392 fun mtimes thy = |
|
393 fold (fn x => fn y => |
|
394 Sign.mk_const thy |
|
395 ("Product_Type.Pair",[Term.dummyT, Term.dummyT]) $ y $ x) |
|
396 |
|
397 (*Adds constants to signature in FOL. "formula_level" means that the constants |
|
398 are to be interpreted as predicates, otherwise as functions over individuals.*) |
|
399 fun FO_const_types config formula_level type_map tptp_t thy = |
|
400 let |
|
401 val ind_type = interpret_type config thy type_map (Defined_type Type_Ind) |
|
402 val value_type = |
|
403 if formula_level then |
|
404 interpret_type config thy type_map (Defined_type Type_Bool) |
|
405 else ind_type |
|
406 in case tptp_t of |
|
407 Term_Func (symb, tptp_ts) => |
|
408 let |
|
409 val thy' = fold (FO_const_types config false type_map) tptp_ts thy |
|
410 val ty = fold (fn ty1 => fn ty2 => Type ("fun", [ty1, ty2])) |
|
411 (map (fn _ => ind_type) tptp_ts) value_type |
|
412 in |
|
413 case symb of |
|
414 Uninterpreted const_name => |
|
415 if const_exists config thy' const_name then thy' |
|
416 else snd (declare_constant config const_name ty thy') |
|
417 | _ => thy' |
|
418 end |
|
419 | _ => thy |
|
420 end |
|
421 |
|
422 (*like FO_const_types but works over symbols*) |
|
423 fun symb_const_types config type_map formula_level const_name n_args thy = |
|
424 let |
|
425 val ind_type = interpret_type config thy type_map (Defined_type Type_Ind) |
|
426 val value_type = |
|
427 if formula_level then |
|
428 interpret_type config thy type_map (Defined_type Type_Bool) |
|
429 else interpret_type config thy type_map (Defined_type Type_Ind) |
|
430 fun mk_i_fun b n acc = |
|
431 if n = 0 then acc b |
|
432 else |
|
433 mk_i_fun b (n - 1) (fn ty => Type ("fun", [ind_type, acc ty])) |
|
434 in |
|
435 if const_exists config thy const_name then thy |
|
436 else |
|
437 snd (declare_constant config const_name |
|
438 (mk_i_fun value_type n_args I) thy) |
|
439 end |
|
440 |
|
441 (*Next batch of functions give info about Isabelle/HOL types*) |
|
442 fun is_fun (Type ("fun", _)) = true |
|
443 | is_fun _ = false |
|
444 fun is_prod (Type ("Product_Type.prod", _)) = true |
|
445 | is_prod _ = false |
|
446 fun dom_type (Type ("fun", [ty1, _])) = ty1 |
|
447 fun is_prod_typed thy config symb = |
|
448 let |
|
449 fun symb_type const_name = |
|
450 Sign.the_const_type thy (full_name thy config const_name) |
|
451 in |
|
452 case symb of |
|
453 Uninterpreted const_name => |
|
454 if is_fun (symb_type const_name) then |
|
455 symb_type const_name |> dom_type |> is_prod |
|
456 else false |
|
457 | _ => false |
|
458 end |
|
459 |
|
460 |
|
461 (* |
|
462 Information needed to be carried around: |
|
463 - constant mapping: maps constant names to Isabelle terms with fully-qualified |
|
464 names. This is fixed, and it is determined by declaration lines earlier |
|
465 in the script (i.e. constants must be declared before appearing in terms. |
|
466 - type context: maps bound variables to their Isabelle type. This is discarded |
|
467 after each call of interpret_term since variables' can't be bound across |
|
468 terms. |
|
469 *) |
|
470 fun interpret_term formula_level config language thy const_map var_types type_map tptp_t = |
|
471 case tptp_t of |
|
472 Term_Func (symb, tptp_ts) => |
|
473 let |
|
474 val thy' = FO_const_types config formula_level type_map tptp_t thy |
|
475 fun typeof_const const_name = Sign.the_const_type thy' |
|
476 (Sign.full_name thy' (mk_binding config const_name)) |
|
477 in |
|
478 case symb of |
|
479 Interpreted_ExtraLogic Apply => |
|
480 (*apply the head of the argument list to the tail*) |
|
481 (mapply |
|
482 (map (interpret_term false config language thy' const_map |
|
483 var_types type_map #> fst) (tl tptp_ts)) |
|
484 (interpret_term formula_level config language thy' const_map |
|
485 var_types type_map (hd tptp_ts) |> fst), |
|
486 thy') |
|
487 | _ => |
|
488 (*apply symb to tptp_ts*) |
|
489 if is_prod_typed thy' config symb then |
|
490 (interpret_symbol config thy' language const_map symb $ |
|
491 mtimes thy' |
|
492 (map (interpret_term false config language thy' const_map |
|
493 var_types type_map #> fst) (tl tptp_ts)) |
|
494 ((interpret_term false config language thy' const_map |
|
495 var_types type_map #> fst) (hd tptp_ts)), |
|
496 thy') |
|
497 else |
|
498 (mapply |
|
499 (map (interpret_term false config language thy' const_map |
|
500 var_types type_map #> fst) tptp_ts) |
|
501 (interpret_symbol config thy' language const_map symb), |
|
502 thy') |
|
503 end |
|
504 | Term_Var n => |
|
505 (if language = THF orelse language = TFF then |
|
506 (case AList.lookup (op =) var_types n of |
|
507 SOME ty => |
|
508 (case ty of |
|
509 SOME ty => Free (n, ty) |
|
510 | NONE => Free (n, Term.dummyT) (*to infer the variable's type*) |
|
511 ) |
|
512 | NONE => |
|
513 raise MISINTERPRET_TERM ("Could not type variable", tptp_t)) |
|
514 else (*variables range over individuals*) |
|
515 Free (n, interpret_type config thy type_map (Defined_type Type_Ind)), |
|
516 thy) |
|
517 | Term_Conditional (tptp_formula, tptp_t1, tptp_t2) => |
|
518 (mk_fun @{const_name If}, thy) |
|
519 | Term_Num (number_kind, num) => |
|
520 let |
|
521 val num_term = |
|
522 if number_kind = Int_num then |
|
523 HOLogic.mk_number @{typ "int"} (the (Int.fromString num)) |
|
524 else dummy_THF () (*FIXME: not yet supporting rationals and reals*) |
|
525 in (num_term, thy) end |
|
526 | Term_Distinct_Object str => |
|
527 let |
|
528 fun alphanumerate c = |
|
529 let |
|
530 val c' = ord c |
|
531 val out_of_range = |
|
532 ((c' > 64) andalso (c' < 91)) orelse ((c' > 96) |
|
533 andalso (c' < 123)) orelse ((c' > 47) andalso (c' < 58)) |
|
534 in |
|
535 if (not out_of_range) andalso (not (c = "_")) then |
|
536 "_nom_" ^ Int.toString (ord c) ^ "_" |
|
537 else c |
|
538 end |
|
539 val mangle_name = raw_explode #> map alphanumerate #> implode |
|
540 in declare_constant config (mangle_name str) |
|
541 (interpret_type config thy type_map (Defined_type Type_Ind)) thy |
|
542 end |
|
543 |
|
544 (*Given a list of "'a option", then applies a function to each element if that |
|
545 element is SOME value, otherwise it leaves it as NONE.*) |
|
546 fun map_opt f xs = |
|
547 fold |
|
548 (fn x => fn y => |
|
549 (if Option.isSome x then |
|
550 SOME (f (Option.valOf x)) |
|
551 else NONE) :: y |
|
552 ) xs [] |
|
553 |
|
554 fun interpret_formula config language const_map var_types type_map tptp_fmla thy = |
|
555 case tptp_fmla of |
|
556 Pred app => |
|
557 interpret_term true config language thy const_map |
|
558 var_types type_map (Term_Func app) |
|
559 | Fmla (symbol, tptp_formulas) => |
|
560 (case symbol of |
|
561 Interpreted_ExtraLogic Apply => |
|
562 let |
|
563 val (args, thy') = (fold_map (interpret_formula config language |
|
564 const_map var_types type_map) (tl tptp_formulas) thy) |
|
565 val (func, thy') = interpret_formula config language const_map |
|
566 var_types type_map (hd tptp_formulas) thy' |
|
567 in (mapply args func, thy') end |
|
568 | Uninterpreted const_name => |
|
569 let |
|
570 val (args, thy') = (fold_map (interpret_formula config language |
|
571 const_map var_types type_map) tptp_formulas thy) |
|
572 val thy' = symb_const_types config type_map true const_name |
|
573 (length tptp_formulas) thy' |
|
574 in |
|
575 (if is_prod_typed thy' config symbol then |
|
576 mtimes thy' args (interpret_symbol config thy' language |
|
577 const_map symbol) |
|
578 else |
|
579 mapply args |
|
580 (interpret_symbol config thy' language const_map symbol), |
|
581 thy') |
|
582 end |
|
583 | _ => |
|
584 let |
|
585 val (args, thy') = |
|
586 fold_map |
|
587 (interpret_formula config language |
|
588 const_map var_types type_map) |
|
589 tptp_formulas thy |
|
590 in |
|
591 (if is_prod_typed thy' config symbol then |
|
592 mtimes thy' args (interpret_symbol config thy' language |
|
593 const_map symbol) |
|
594 else |
|
595 mapply args |
|
596 (interpret_symbol config thy' language const_map symbol), |
|
597 thy') |
|
598 end) |
|
599 | Sequent _ => |
|
600 raise MISINTERPRET_FORMULA ("Sequent", tptp_fmla) (*FIXME unsupported*) |
|
601 | Quant (quantifier, bindings, tptp_formula) => |
|
602 let |
|
603 val (bound_vars, bound_var_types) = ListPair.unzip bindings |
|
604 val bound_var_types' : typ option list = |
|
605 (map_opt : (tptp_type -> typ) -> (tptp_type option list) -> typ option list) |
|
606 (interpret_type config thy type_map) bound_var_types |
|
607 val var_types' = |
|
608 ListPair.zip (bound_vars, List.rev bound_var_types') |
|
609 |> List.rev |
|
610 fun fold_bind f = |
|
611 fold |
|
612 (fn (n, ty) => fn t => |
|
613 case ty of |
|
614 NONE => |
|
615 f (n, |
|
616 if language = THF then Term.dummyT |
|
617 else |
|
618 interpret_type config thy type_map |
|
619 (Defined_type Type_Ind), |
|
620 t) |
|
621 | SOME ty => f (n, ty, t) |
|
622 ) |
|
623 var_types' |
|
624 in case quantifier of |
|
625 Forall => |
|
626 interpret_formula config language const_map (var_types' @ var_types) |
|
627 type_map tptp_formula thy |
|
628 |>> fold_bind HOLogic.mk_all |
|
629 | Exists => |
|
630 interpret_formula config language const_map (var_types' @ var_types) |
|
631 type_map tptp_formula thy |
|
632 |>> fold_bind HOLogic.mk_exists |
|
633 | Lambda => |
|
634 interpret_formula config language const_map (var_types' @ var_types) |
|
635 type_map tptp_formula thy |
|
636 |>> fold_bind (fn (n, ty, rest) => lambda (Free (n, ty)) rest) |
|
637 | Epsilon => |
|
638 let val (t, thy') = |
|
639 interpret_formula config language const_map var_types type_map |
|
640 (Quant (Lambda, bindings, tptp_formula)) thy |
|
641 in ((HOLogic.choice_const Term.dummyT) $ t, thy') end |
|
642 | Iota => |
|
643 let val (t, thy') = |
|
644 interpret_formula config language const_map var_types type_map |
|
645 (Quant (Lambda, bindings, tptp_formula)) thy |
|
646 in (Const (@{const_name The}, Term.dummyT) $ t, thy') end |
|
647 | Dep_Prod => |
|
648 raise MISINTERPRET_FORMULA ("Unsupported", tptp_fmla) |
|
649 | Dep_Sum => |
|
650 raise MISINTERPRET_FORMULA ("Unsupported", tptp_fmla) |
|
651 end |
|
652 (*FIXME unsupported |
|
653 | Conditional of tptp_formula * tptp_formula * tptp_formula |
|
654 | Let of tptp_let list * tptp_formula |
|
655 |
|
656 and tptp_let = |
|
657 Let_fmla of (string * tptp_type option) * tptp_formula (*both TFF and THF*) |
|
658 | Let_term of (string * tptp_type option) * tptp_term (*only TFF*) |
|
659 *) |
|
660 | Atom tptp_atom => |
|
661 (case tptp_atom of |
|
662 TFF_Typed_Atom (symbol, tptp_type_opt) => |
|
663 (*FIXME ignoring type info*) |
|
664 (interpret_symbol config thy language const_map symbol, thy) |
|
665 | THF_Atom_term tptp_term => |
|
666 interpret_term true config language thy const_map var_types |
|
667 type_map tptp_term |
|
668 | THF_Atom_conn_term symbol => |
|
669 (interpret_symbol config thy language const_map symbol, thy)) |
|
670 | THF_type _ => (*FIXME unsupported*) |
|
671 raise MISINTERPRET_FORMULA |
|
672 ("Cannot interpret types as formulas", tptp_fmla) |
|
673 | THF_typing (tptp_formula, _) => (*FIXME ignoring type info*) |
|
674 interpret_formula config language |
|
675 const_map var_types type_map tptp_formula thy |
|
676 |
|
677 |
|
678 (*Extract name of inference rule, and the inferences it relies on*) |
|
679 (*This is tuned to work with LEO-II, and is brittle to upstream |
|
680 changes of the proof protocol.*) |
|
681 fun extract_inference_info annot = |
|
682 let |
|
683 fun get_line_id (General_Data (Number (Int_num, num))) = [num] |
|
684 | get_line_id (General_Data (Atomic_Word name)) = [name] |
|
685 | get_line_id (General_Term (Number (Int_num, num), _ (*e.g. a bind*))) = [num] |
|
686 | get_line_id _ = [] |
|
687 (*e.g. General_Data (Application ("theory", [General_Data |
|
688 (Atomic_Word "equality")])) -- which would come from E through LEO-II*) |
|
689 in |
|
690 case annot of |
|
691 NONE => NONE |
|
692 | SOME annot => |
|
693 (case annot of |
|
694 (General_Data (Application ("inference", |
|
695 [General_Data (Atomic_Word inference_name), |
|
696 _, |
|
697 General_List related_lines])), _) => |
|
698 (SOME (inference_name, map get_line_id related_lines |> List.concat)) |
|
699 | _ => NONE) |
|
700 end |
|
701 |
|
702 |
|
703 (*Extract the type from a typing*) |
|
704 local |
|
705 fun extract_type tptp_type = |
|
706 case tptp_type of |
|
707 Fmla_type typ => fmlatype_to_type typ |
|
708 | _ => tptp_type |
|
709 in |
|
710 fun typeof_typing (THF_typing (_, tptp_type)) = extract_type tptp_type |
|
711 fun typeof_tff_typing (Atom (TFF_Typed_Atom (_, SOME tptp_type))) = |
|
712 extract_type tptp_type |
|
713 end |
|
714 fun nameof_typing |
|
715 (THF_typing |
|
716 ((Atom (THF_Atom_term (Term_Func (Uninterpreted str, [])))), _)) = str |
|
717 fun nameof_tff_typing (Atom (TFF_Typed_Atom (Uninterpreted str, _))) = str |
|
718 |
|
719 fun interpret_line config type_map const_map path_prefix line thy = |
|
720 case line of |
|
721 Include (quoted_path, _) => (*FIXME currently everything is imported*) |
|
722 interpret_file' |
|
723 false |
|
724 config |
|
725 path_prefix |
|
726 (Path.append |
|
727 path_prefix |
|
728 (quoted_path |
|
729 |> unenclose |
|
730 |> Path.explode)) |
|
731 type_map |
|
732 const_map |
|
733 thy |
|
734 | Annotated_Formula (pos, lang, label, role, tptp_formula, annotation_opt) => |
|
735 case role of |
|
736 Role_Type => |
|
737 let |
|
738 val thy_name = Context.theory_name thy |
|
739 val (tptp_ty, name) = |
|
740 if lang = THF then |
|
741 (typeof_typing tptp_formula (*assuming tptp_formula is a typing*), |
|
742 nameof_typing tptp_formula (*and that the LHS is a (atom) name*)) |
|
743 else |
|
744 (typeof_tff_typing tptp_formula, |
|
745 nameof_tff_typing tptp_formula) |
|
746 in |
|
747 case tptp_ty of |
|
748 Defined_type Type_Type => (*add new type*) |
|
749 (*generate an Isabelle/HOL type to interpret this THF type, |
|
750 and add it to both the Isabelle/HOL theory and to the type_map*) |
|
751 let |
|
752 val (type_map', thy') = |
|
753 declare_type |
|
754 config |
|
755 (Atom_type name, name) |
|
756 type_map |
|
757 thy |
|
758 in ((type_map', |
|
759 const_map, |
|
760 []), |
|
761 thy') |
|
762 end |
|
763 |
|
764 | _ => (*declaration of constant*) |
|
765 (*Here we populate the map from constants to the Isabelle/HOL |
|
766 terms they map to (which in turn contain their types).*) |
|
767 let |
|
768 val ty = interpret_type config thy type_map tptp_ty |
|
769 (*make sure that the theory contains all the types appearing |
|
770 in this constant's signature. Exception is thrown if encounter |
|
771 an undeclared types.*) |
|
772 val (t, thy') = |
|
773 let |
|
774 fun analyse_type thy thf_ty = |
|
775 if #cautious config then |
|
776 case thf_ty of |
|
777 Fn_type (thf_ty1, thf_ty2) => |
|
778 (analyse_type thy thf_ty1; |
|
779 analyse_type thy thf_ty2) |
|
780 | Atom_type ty_name => |
|
781 if type_exists thy ty_name then () |
|
782 else |
|
783 raise MISINTERPRET_TYPE |
|
784 ("This type, in signature of " ^ |
|
785 name ^ " has not been declared.", |
|
786 Atom_type ty_name) |
|
787 | _ => () |
|
788 else () (*skip test if we're not being cautious.*) |
|
789 in |
|
790 analyse_type thy tptp_ty; |
|
791 declare_constant config name ty thy |
|
792 end |
|
793 (*register a mapping from name to t. Constants' type |
|
794 declarations should occur at most once, so it's justified to |
|
795 use "::". Note that here we use a constant's name rather |
|
796 than the possibly- new one, since all references in the |
|
797 theory will be to this name.*) |
|
798 val const_map' = ((name, t) :: const_map) |
|
799 in ((type_map,(*type_map unchanged, since a constant's |
|
800 declaration shouldn't include any new types.*) |
|
801 const_map',(*typing table of constant was extended*) |
|
802 []),(*no formulas were interpreted*) |
|
803 thy')(*theory was extended with new constant*) |
|
804 end |
|
805 end |
|
806 |
|
807 | _ => (*i.e. the AF is not a type declaration*) |
|
808 let |
|
809 (*gather interpreted term, and the map of types occurring in that term*) |
|
810 val (t, thy') = |
|
811 interpret_formula config lang |
|
812 const_map [] type_map tptp_formula thy |
|
813 |>> HOLogic.mk_Trueprop |
|
814 (*type_maps grow monotonically, so return the newest value (type_mapped); |
|
815 there's no need to unify it with the type_map parameter.*) |
|
816 in |
|
817 ((type_map, const_map, |
|
818 [(label, role, tptp_formula, |
|
819 Syntax.check_term (Proof_Context.init_global thy') t, |
|
820 extract_inference_info annotation_opt)]), thy') |
|
821 end |
|
822 |
|
823 and interpret_problem new_basic_types config path_prefix lines type_map const_map thy = |
|
824 let |
|
825 val thy_name = Context.theory_name thy |
|
826 (*Add interpretation of $o and generate an Isabelle/HOL type to |
|
827 interpret $i, unless we've been given a mapping of types.*) |
|
828 val (thy', type_map') = |
|
829 if not new_basic_types then (thy, type_map) |
|
830 else |
|
831 let |
|
832 val (type_map', thy') = |
|
833 declare_type config |
|
834 (Defined_type Type_Ind, IND_TYPE) type_map thy |
|
835 in |
|
836 (thy', type_map') |
|
837 end |
|
838 in |
|
839 fold (fn line => |
|
840 fn ((type_map, const_map, lines), thy) => |
|
841 let |
|
842 (*process the line, ignoring the type-context for variables*) |
|
843 val ((type_map', const_map', l'), thy') = |
|
844 interpret_line config type_map const_map path_prefix line thy |
|
845 in |
|
846 ((type_map', |
|
847 const_map', |
|
848 l' @ lines),(*append is sufficient, union would be overkill*) |
|
849 thy') |
|
850 end) |
|
851 lines (*lines of the problem file*) |
|
852 ((type_map', const_map, []), thy') (*initial values*) |
|
853 end |
|
854 |
|
855 and interpret_file' new_basic_types config path_prefix file_name = |
|
856 let |
|
857 val file_name' = Path.expand file_name |
|
858 in |
|
859 if Path.is_absolute file_name' then |
|
860 Path.implode file_name |
|
861 |> TPTP_Parser.parse_file |
|
862 |> interpret_problem new_basic_types config path_prefix |
|
863 else error "Could not determine absolute path to file." |
|
864 end |
|
865 |
|
866 and interpret_file cautious path_prefix file_name = |
|
867 let |
|
868 val config = |
|
869 {cautious = cautious, |
|
870 problem_name = |
|
871 SOME (TPTP_Problem_Name.parse_problem_name ((Path.base #> Path.implode) |
|
872 file_name)) |
|
873 } |
|
874 handle _(*FIXME*) => |
|
875 {cautious = cautious, |
|
876 problem_name = NONE |
|
877 } |
|
878 in interpret_file' true config path_prefix file_name end |
|
879 |
|
880 fun import_file cautious path_prefix file_name type_map const_map thy = |
|
881 let |
|
882 val prob_name = |
|
883 TPTP_Problem_Name.parse_problem_name (Path.implode (Path.base file_name)) |
|
884 handle _(*FIXME*) => TPTP_Problem_Name.Nonstandard (Path.implode file_name) |
|
885 val (result, thy') = |
|
886 interpret_file cautious path_prefix file_name type_map const_map thy |
|
887 in TPTP_Data.map (cons ((prob_name, result))) thy' end |
|
888 |
|
889 val _ = |
|
890 Outer_Syntax.improper_command "import_tptp" "import TPTP problem" |
|
891 Keyword.diag (*FIXME why diag?*) |
|
892 (Parse.string >> |
|
893 (fn file_name => |
|
894 Toplevel.theory (fn thy => |
|
895 import_file true (Path.explode file_name |> Path.dir) |
|
896 (Path.explode file_name) [] [] thy |
|
897 ))) |
|
898 |
|
899 |
|
900 (*Used for debugging. Returns all files contained within a directory or its |
|
901 subdirectories. Follows symbolic links, filters away directories.*) |
|
902 fun get_file_list path = |
|
903 let |
|
904 fun check_file_entry f rest = |
|
905 let |
|
906 (*NOTE needed since don't have File.is_link and File.read_link*) |
|
907 val f_str = Path.implode f |
|
908 in |
|
909 if File.is_dir f then |
|
910 rest (*filter out directories*) |
|
911 else if OS.FileSys.isLink f_str then |
|
912 (*follow links -- NOTE this breaks if links are relative paths*) |
|
913 check_file_entry (Path.explode (OS.FileSys.readLink f_str)) rest |
|
914 else f :: rest |
|
915 end |
|
916 in |
|
917 File.read_dir path |
|
918 |> map |
|
919 (Path.explode |
|
920 #> Path.append path) |
|
921 |> (fn l => fold check_file_entry l []) |
|
922 end |
|
923 |
|
924 end |