author | blanchet |
Thu, 16 Aug 2012 15:41:36 +0200 | |
changeset 48829 | 6ed588c4f963 |
parent 47729 | 44d1f4e0a46e |
child 48881 | 46e053eda5dd |
permissions | -rw-r--r-- |
46879 | 1 |
(* Title: HOL/TPTP/TPTP_Parser/tptp_interpret.ML |
46844 | 2 |
Author: Nik Sultana, Cambridge University Computer Laboratory |
3 |
||
4 |
Interprets TPTP problems in Isabelle/HOL. |
|
5 |
*) |
|
6 |
||
7 |
signature TPTP_INTERPRET = |
|
8 |
sig |
|
47515 | 9 |
(*Signature extension: typing information for variables and constants*) |
46844 | 10 |
type var_types = (string * typ option) list |
47515 | 11 |
type const_map = (string * term) list |
46844 | 12 |
|
47515 | 13 |
(*Mapping from TPTP types to Isabelle/HOL types. This map works over all |
14 |
base types. The map must be total wrt TPTP types.*) |
|
46844 | 15 |
type type_map = (TPTP_Syntax.tptp_type * typ) list |
16 |
||
47515 | 17 |
(*Inference info, when available, consists of the name of the inference rule |
46844 | 18 |
and the names of the inferences involved in the reasoning step.*) |
19 |
type inference_info = (string * string list) option |
|
20 |
||
47515 | 21 |
(*A parsed annotated formula is represented as a 5-tuple consisting of |
22 |
the formula's label, its role, the TPTP formula, its Isabelle/HOL meaning, and |
|
23 |
inference info*) |
|
46844 | 24 |
type tptp_formula_meaning = |
47548 | 25 |
string * TPTP_Syntax.role * term * inference_info |
46844 | 26 |
|
27 |
(*In general, the meaning of a TPTP statement (which, through the Include |
|
47515 | 28 |
directive, may include the meaning of an entire TPTP file, is a map from |
29 |
TPTP to Isabelle/HOL types, a map from TPTP constants to their Isabelle/HOL |
|
30 |
counterparts and their types, and a list of interpreted annotated formulas.*) |
|
46844 | 31 |
type tptp_general_meaning = |
32 |
(type_map * const_map * tptp_formula_meaning list) |
|
33 |
||
47515 | 34 |
(*cautious = indicates whether additional checks are made to check |
35 |
that all used types have been declared. |
|
36 |
problem_name = if given then it is used to qualify types & constants*) |
|
46844 | 37 |
type config = |
47515 | 38 |
{cautious : bool, |
47548 | 39 |
problem_name : TPTP_Problem_Name.problem_name option} |
46844 | 40 |
|
47515 | 41 |
(*Generates a fresh Isabelle/HOL type for interpreting a TPTP type in a theory.*) |
42 |
val declare_type : config -> (TPTP_Syntax.tptp_type * string) -> type_map -> |
|
43 |
theory -> type_map * theory |
|
44 |
||
45 |
(*Map TPTP types to Isabelle/HOL types*) |
|
46844 | 46 |
val interpret_type : config -> theory -> type_map -> |
47 |
TPTP_Syntax.tptp_type -> typ |
|
48 |
||
47515 | 49 |
(*Map TPTP terms to Isabelle/HOL terms*) |
47570
df3c9aa6c9dc
improved threading of thy-values through interpret functions;
sultana
parents:
47569
diff
changeset
|
50 |
val interpret_term : bool -> config -> TPTP_Syntax.language -> |
df3c9aa6c9dc
improved threading of thy-values through interpret functions;
sultana
parents:
47569
diff
changeset
|
51 |
const_map -> var_types -> type_map -> TPTP_Syntax.tptp_term -> theory -> |
47511 | 52 |
term * theory |
53 |
||
54 |
val interpret_formula : config -> TPTP_Syntax.language -> const_map -> |
|
55 |
var_types -> type_map -> TPTP_Syntax.tptp_formula -> theory -> |
|
56 |
term * theory |
|
57 |
||
47515 | 58 |
(*Interpret a TPTP line: return a "tptp_general_meaning" for that line, |
59 |
as well as an updated Isabelle theory including any types & constants |
|
60 |
which were specified in that line. |
|
46844 | 61 |
Note that type/constant declarations do not result in any formulas being |
47515 | 62 |
returned. A typical TPTP line might update the theory, and/or return one or |
63 |
more formulas. For instance, the "include" directive may update the theory |
|
64 |
and also return a list of formulas from the included file. |
|
46844 | 65 |
Arguments: |
47515 | 66 |
config = (see above) |
67 |
inclusion list = names of annotated formulas to interpret (since "include" |
|
68 |
directive can be selective wrt to such names) |
|
47360 | 69 |
type_map = mapping of TPTP-types to Isabelle/HOL types. This argument may be |
46844 | 70 |
given to force a specific mapping: this is usually done for using an |
47360 | 71 |
imported TPTP problem in Isar. |
46844 | 72 |
const_map = as previous, but for constants. |
48829
6ed588c4f963
look in current directory first before looking up includes in the TPTP directory, as required by Geoff
blanchet
parents:
47729
diff
changeset
|
73 |
path_prefixes = paths where TPTP problems etc are located (to help the |
6ed588c4f963
look in current directory first before looking up includes in the TPTP directory, as required by Geoff
blanchet
parents:
47729
diff
changeset
|
74 |
"include" directive find the files. |
47515 | 75 |
line = parsed TPTP line |
46844 | 76 |
thy = theory where interpreted info will be stored. |
77 |
*) |
|
47511 | 78 |
val interpret_line : config -> string list -> type_map -> const_map -> |
48829
6ed588c4f963
look in current directory first before looking up includes in the TPTP directory, as required by Geoff
blanchet
parents:
47729
diff
changeset
|
79 |
Path.T list -> TPTP_Syntax.tptp_line -> theory -> |
6ed588c4f963
look in current directory first before looking up includes in the TPTP directory, as required by Geoff
blanchet
parents:
47729
diff
changeset
|
80 |
tptp_general_meaning * theory |
46844 | 81 |
|
82 |
(*Like "interpret_line" above, but works over a whole parsed problem. |
|
83 |
Arguments: |
|
47515 | 84 |
config = as previously |
85 |
inclusion list = as previously |
|
48829
6ed588c4f963
look in current directory first before looking up includes in the TPTP directory, as required by Geoff
blanchet
parents:
47729
diff
changeset
|
86 |
path_prefixes = as previously |
47515 | 87 |
lines = parsed TPTP syntax |
88 |
type_map = as previously |
|
89 |
const_map = as previously |
|
90 |
thy = as previously |
|
46844 | 91 |
*) |
48829
6ed588c4f963
look in current directory first before looking up includes in the TPTP directory, as required by Geoff
blanchet
parents:
47729
diff
changeset
|
92 |
val interpret_problem : config -> string list -> Path.T list -> |
46844 | 93 |
TPTP_Syntax.tptp_line list -> type_map -> const_map -> theory -> |
94 |
tptp_general_meaning * theory |
|
95 |
||
47515 | 96 |
(*Like "interpret_problem" above, but it is given a filename rather than |
46844 | 97 |
a parsed problem.*) |
48829
6ed588c4f963
look in current directory first before looking up includes in the TPTP directory, as required by Geoff
blanchet
parents:
47729
diff
changeset
|
98 |
val interpret_file : bool -> Path.T list -> Path.T -> type_map -> const_map -> |
46844 | 99 |
theory -> tptp_general_meaning * theory |
100 |
||
47569
fce9d97a3258
exceptions related to interpreting tptp problems now mention the relevant position in the tptp file;
sultana
parents:
47558
diff
changeset
|
101 |
type position = string * int * int |
fce9d97a3258
exceptions related to interpreting tptp problems now mention the relevant position in the tptp file;
sultana
parents:
47558
diff
changeset
|
102 |
exception MISINTERPRET of position list * exn |
46844 | 103 |
exception MISINTERPRET_FORMULA of string * TPTP_Syntax.tptp_formula |
104 |
exception MISINTERPRET_SYMBOL of string * TPTP_Syntax.symbol |
|
105 |
exception MISINTERPRET_TERM of string * TPTP_Syntax.tptp_term |
|
106 |
exception MISINTERPRET_TYPE of string * TPTP_Syntax.tptp_type |
|
107 |
||
48829
6ed588c4f963
look in current directory first before looking up includes in the TPTP directory, as required by Geoff
blanchet
parents:
47729
diff
changeset
|
108 |
val import_file : bool -> Path.T list -> Path.T -> type_map -> const_map -> |
47515 | 109 |
theory -> theory |
110 |
||
111 |
(*Imported TPTP files are stored as "manifests" in the theory.*) |
|
112 |
type manifest = TPTP_Problem_Name.problem_name * tptp_general_meaning |
|
113 |
val get_manifests : theory -> manifest list |
|
46844 | 114 |
end |
115 |
||
116 |
structure TPTP_Interpret : TPTP_INTERPRET = |
|
117 |
struct |
|
118 |
||
119 |
open TPTP_Syntax |
|
47569
fce9d97a3258
exceptions related to interpreting tptp problems now mention the relevant position in the tptp file;
sultana
parents:
47558
diff
changeset
|
120 |
type position = string * int * int |
fce9d97a3258
exceptions related to interpreting tptp problems now mention the relevant position in the tptp file;
sultana
parents:
47558
diff
changeset
|
121 |
exception MISINTERPRET of position list * exn |
46844 | 122 |
exception MISINTERPRET_FORMULA of string * TPTP_Syntax.tptp_formula |
123 |
exception MISINTERPRET_SYMBOL of string * TPTP_Syntax.symbol |
|
124 |
exception MISINTERPRET_TERM of string * TPTP_Syntax.tptp_term |
|
125 |
exception MISINTERPRET_TYPE of string * TPTP_Syntax.tptp_type |
|
126 |
||
47515 | 127 |
|
46844 | 128 |
(* General stuff *) |
129 |
||
130 |
type config = |
|
47515 | 131 |
{cautious : bool, |
132 |
problem_name : TPTP_Problem_Name.problem_name option} |
|
133 |
||
46844 | 134 |
|
135 |
(* Interpretation *) |
|
136 |
||
137 |
(** Signatures and other type abbrevations **) |
|
138 |
||
139 |
type const_map = (string * term) list |
|
140 |
type var_types = (string * typ option) list |
|
141 |
type type_map = (TPTP_Syntax.tptp_type * typ) list |
|
142 |
type inference_info = (string * string list) option |
|
143 |
type tptp_formula_meaning = |
|
47548 | 144 |
string * TPTP_Syntax.role * term * inference_info |
46844 | 145 |
type tptp_general_meaning = |
146 |
(type_map * const_map * tptp_formula_meaning list) |
|
147 |
||
148 |
type manifest = TPTP_Problem_Name.problem_name * tptp_general_meaning |
|
47639 | 149 |
|
46844 | 150 |
structure TPTP_Data = Theory_Data |
47639 | 151 |
( |
152 |
type T = manifest list |
|
153 |
val empty = [] |
|
154 |
val extend = I |
|
155 |
fun merge data : T = Library.merge (op =) data |
|
156 |
) |
|
46844 | 157 |
val get_manifests = TPTP_Data.get |
158 |
||
159 |
||
160 |
(** Adding types to a signature **) |
|
161 |
||
47514 | 162 |
(*transform quoted names into acceptable ASCII strings*) |
163 |
fun alphanumerate c = |
|
164 |
let |
|
165 |
val c' = ord c |
|
166 |
val out_of_range = |
|
167 |
((c' > 64) andalso (c' < 91)) orelse ((c' > 96) |
|
168 |
andalso (c' < 123)) orelse ((c' > 47) andalso (c' < 58)) |
|
169 |
in |
|
170 |
if (not out_of_range) andalso (not (c = "_")) then |
|
171 |
"_nom_" ^ Int.toString (ord c) ^ "_" |
|
172 |
else c |
|
173 |
end |
|
174 |
fun alphanumerated_name prefix name = |
|
175 |
prefix ^ (raw_explode #> map alphanumerate #> implode) name |
|
176 |
||
47332
360e080fd13e
dealing with SMLNJ errors 'value type in structure doesn't match signature spec' (which originated from lack of type generalisation) and 'unresolved flex record' wrt tptp_interpret
sultana
parents:
46961
diff
changeset
|
177 |
(*SMLNJ complains if type annotation not used below*) |
360e080fd13e
dealing with SMLNJ errors 'value type in structure doesn't match signature spec' (which originated from lack of type generalisation) and 'unresolved flex record' wrt tptp_interpret
sultana
parents:
46961
diff
changeset
|
178 |
fun mk_binding (config : config) ident = |
46844 | 179 |
let |
47514 | 180 |
val pre_binding = Binding.name (alphanumerated_name "bnd_" ident) |
46844 | 181 |
in |
182 |
case #problem_name config of |
|
183 |
NONE => pre_binding |
|
184 |
| SOME prob => |
|
185 |
Binding.qualify |
|
186 |
false |
|
187 |
(TPTP_Problem_Name.mangle_problem_name prob) |
|
188 |
pre_binding |
|
189 |
end |
|
190 |
||
47548 | 191 |
fun type_exists config thy ty_name = |
192 |
Sign.declared_tyname thy (Sign.full_name thy (mk_binding config ty_name)) |
|
193 |
||
46844 | 194 |
(*Returns updated theory and the name of the final type's name -- i.e. if the |
195 |
original name is already taken then the function looks for an available |
|
196 |
alternative. It also returns an updated type_map if one has been passed to it.*) |
|
197 |
fun declare_type (config : config) (thf_type, type_name) ty_map thy = |
|
47548 | 198 |
if type_exists config thy type_name then |
46844 | 199 |
raise MISINTERPRET_TYPE ("Type already exists", Atom_type type_name) |
200 |
else |
|
201 |
let |
|
202 |
val binding = mk_binding config type_name |
|
203 |
val final_fqn = Sign.full_name thy binding |
|
47510 | 204 |
val thy' = |
205 |
Typedecl.typedecl_global (mk_binding config type_name, [], NoSyn) thy |
|
206 |
|> snd |
|
46844 | 207 |
val typ_map_entry = (thf_type, (Type (final_fqn, []))) |
208 |
val ty_map' = typ_map_entry :: ty_map |
|
209 |
in (ty_map', thy') end |
|
210 |
||
211 |
||
212 |
(** Adding constants to signature **) |
|
213 |
||
214 |
fun full_name thy config const_name = |
|
215 |
Sign.full_name thy (mk_binding config const_name) |
|
216 |
||
217 |
fun const_exists config thy const_name = |
|
218 |
Sign.declared_const thy (full_name thy config const_name) |
|
219 |
||
220 |
fun declare_constant config const_name ty thy = |
|
221 |
if const_exists config thy const_name then |
|
222 |
raise MISINTERPRET_TERM |
|
223 |
("Const already declared", Term_Func (Uninterpreted const_name, [])) |
|
224 |
else |
|
225 |
Theory.specify_const |
|
226 |
((mk_binding config const_name, ty), NoSyn) thy |
|
227 |
||
47692
3d76c81b5ed2
improved non-interpretation of constants and numbers;
sultana
parents:
47691
diff
changeset
|
228 |
fun declare_const_ifnot config const_name ty thy = |
3d76c81b5ed2
improved non-interpretation of constants and numbers;
sultana
parents:
47691
diff
changeset
|
229 |
if const_exists config thy const_name then |
3d76c81b5ed2
improved non-interpretation of constants and numbers;
sultana
parents:
47691
diff
changeset
|
230 |
(Sign.mk_const thy ((Sign.full_name thy (mk_binding config const_name)), []), thy) |
3d76c81b5ed2
improved non-interpretation of constants and numbers;
sultana
parents:
47691
diff
changeset
|
231 |
else declare_constant config const_name ty thy |
3d76c81b5ed2
improved non-interpretation of constants and numbers;
sultana
parents:
47691
diff
changeset
|
232 |
|
46844 | 233 |
|
47515 | 234 |
(** Interpretation functions **) |
46844 | 235 |
|
236 |
(*Types in THF are encoded as formulas. This function translates them to type form.*) |
|
237 |
(*FIXME possibly incomplete hack*) |
|
238 |
fun fmlatype_to_type (Atom (THF_Atom_term (Term_Func (TypeSymbol typ, [])))) = |
|
239 |
Defined_type typ |
|
240 |
| fmlatype_to_type (Atom (THF_Atom_term (Term_Func (Uninterpreted str, [])))) = |
|
241 |
Atom_type str |
|
47360 | 242 |
| fmlatype_to_type (Type_fmla (Fn_type (ty1, ty2))) = |
46844 | 243 |
let |
244 |
val ty1' = case ty1 of |
|
47360 | 245 |
Fn_type _ => fmlatype_to_type (Type_fmla ty1) |
46844 | 246 |
| Fmla_type ty1 => fmlatype_to_type ty1 |
247 |
val ty2' = case ty2 of |
|
47360 | 248 |
Fn_type _ => fmlatype_to_type (Type_fmla ty2) |
46844 | 249 |
| Fmla_type ty2 => fmlatype_to_type ty2 |
250 |
in Fn_type (ty1', ty2') end |
|
251 |
||
252 |
fun interpret_type config thy type_map thf_ty = |
|
253 |
let |
|
254 |
fun lookup_type ty_map thf_ty = |
|
255 |
(case AList.lookup (op =) ty_map thf_ty of |
|
256 |
NONE => |
|
257 |
raise MISINTERPRET_TYPE |
|
47510 | 258 |
("Could not find the interpretation of this TPTP type in the \ |
259 |
\mapping to Isabelle/HOL", thf_ty) |
|
46844 | 260 |
| SOME ty => ty) |
261 |
in |
|
47548 | 262 |
case thf_ty of |
46844 | 263 |
Prod_type (thf_ty1, thf_ty2) => |
264 |
Type ("Product_Type.prod", |
|
265 |
[interpret_type config thy type_map thf_ty1, |
|
266 |
interpret_type config thy type_map thf_ty2]) |
|
267 |
| Fn_type (thf_ty1, thf_ty2) => |
|
268 |
Type ("fun", |
|
269 |
[interpret_type config thy type_map thf_ty1, |
|
270 |
interpret_type config thy type_map thf_ty2]) |
|
271 |
| Atom_type _ => |
|
272 |
lookup_type type_map thf_ty |
|
273 |
| Defined_type tptp_base_type => |
|
274 |
(case tptp_base_type of |
|
47519 | 275 |
Type_Ind => @{typ ind} |
46844 | 276 |
| Type_Bool => HOLogic.boolT |
47510 | 277 |
| Type_Type => raise MISINTERPRET_TYPE ("No type interpretation", thf_ty) |
46844 | 278 |
(*FIXME these types are currently unsupported, so they're treated as |
279 |
individuals*) |
|
47690 | 280 |
| Type_Int => |
281 |
interpret_type config thy type_map (Defined_type Type_Ind) |
|
46844 | 282 |
| Type_Rat => |
283 |
interpret_type config thy type_map (Defined_type Type_Ind) |
|
284 |
| Type_Real => |
|
285 |
interpret_type config thy type_map (Defined_type Type_Ind) |
|
286 |
) |
|
287 |
| Sum_type _ => |
|
288 |
raise MISINTERPRET_TYPE (*FIXME*) |
|
289 |
("No type interpretation (sum type)", thf_ty) |
|
290 |
| Fmla_type tptp_ty => |
|
291 |
fmlatype_to_type tptp_ty |
|
292 |
|> interpret_type config thy type_map |
|
293 |
| Subtype _ => |
|
294 |
raise MISINTERPRET_TYPE (*FIXME*) |
|
295 |
("No type interpretation (subtype)", thf_ty) |
|
296 |
end |
|
297 |
||
298 |
fun the_const config thy language const_map_payload str = |
|
299 |
if language = THF then |
|
300 |
(case AList.lookup (op =) const_map_payload str of |
|
301 |
NONE => raise MISINTERPRET_TERM |
|
47510 | 302 |
("Could not find the interpretation of this constant in the \ |
303 |
\mapping to Isabelle/HOL", Term_Func (Uninterpreted str, [])) |
|
46844 | 304 |
| SOME t => t) |
305 |
else |
|
306 |
if const_exists config thy str then |
|
307 |
Sign.mk_const thy ((Sign.full_name thy (mk_binding config str)), []) |
|
308 |
else raise MISINTERPRET_TERM |
|
47510 | 309 |
("Could not find the interpretation of this constant in the \ |
310 |
\mapping to Isabelle/HOL", Term_Func (Uninterpreted str, [])) |
|
46844 | 311 |
|
47692
3d76c81b5ed2
improved non-interpretation of constants and numbers;
sultana
parents:
47691
diff
changeset
|
312 |
(*Eta-expands n-ary function. |
3d76c81b5ed2
improved non-interpretation of constants and numbers;
sultana
parents:
47691
diff
changeset
|
313 |
"str" is the name of an Isabelle/HOL constant*) |
3d76c81b5ed2
improved non-interpretation of constants and numbers;
sultana
parents:
47691
diff
changeset
|
314 |
fun mk_n_fun n str = |
3d76c81b5ed2
improved non-interpretation of constants and numbers;
sultana
parents:
47691
diff
changeset
|
315 |
let |
3d76c81b5ed2
improved non-interpretation of constants and numbers;
sultana
parents:
47691
diff
changeset
|
316 |
fun body 0 t = t |
3d76c81b5ed2
improved non-interpretation of constants and numbers;
sultana
parents:
47691
diff
changeset
|
317 |
| body n t = body (n - 1) (t $ (Bound (n - 1))) |
3d76c81b5ed2
improved non-interpretation of constants and numbers;
sultana
parents:
47691
diff
changeset
|
318 |
in |
3d76c81b5ed2
improved non-interpretation of constants and numbers;
sultana
parents:
47691
diff
changeset
|
319 |
body n (Const (str, Term.dummyT)) |
3d76c81b5ed2
improved non-interpretation of constants and numbers;
sultana
parents:
47691
diff
changeset
|
320 |
|> funpow n (Term.absdummy Term.dummyT) |
3d76c81b5ed2
improved non-interpretation of constants and numbers;
sultana
parents:
47691
diff
changeset
|
321 |
end |
3d76c81b5ed2
improved non-interpretation of constants and numbers;
sultana
parents:
47691
diff
changeset
|
322 |
fun mk_fun_type [] b acc = acc b |
3d76c81b5ed2
improved non-interpretation of constants and numbers;
sultana
parents:
47691
diff
changeset
|
323 |
| mk_fun_type (ty :: tys) b acc = |
3d76c81b5ed2
improved non-interpretation of constants and numbers;
sultana
parents:
47691
diff
changeset
|
324 |
mk_fun_type tys b (fn ty_rest => Type ("fun", [ty, acc ty_rest])) |
46844 | 325 |
|
47692
3d76c81b5ed2
improved non-interpretation of constants and numbers;
sultana
parents:
47691
diff
changeset
|
326 |
(*These arities are not part of the TPTP spec*) |
3d76c81b5ed2
improved non-interpretation of constants and numbers;
sultana
parents:
47691
diff
changeset
|
327 |
fun arity_of interpreted_symbol = case interpreted_symbol of |
3d76c81b5ed2
improved non-interpretation of constants and numbers;
sultana
parents:
47691
diff
changeset
|
328 |
UMinus => 1 |
3d76c81b5ed2
improved non-interpretation of constants and numbers;
sultana
parents:
47691
diff
changeset
|
329 |
| Sum => 2 |
3d76c81b5ed2
improved non-interpretation of constants and numbers;
sultana
parents:
47691
diff
changeset
|
330 |
| Difference => 2 |
3d76c81b5ed2
improved non-interpretation of constants and numbers;
sultana
parents:
47691
diff
changeset
|
331 |
| Product => 2 |
3d76c81b5ed2
improved non-interpretation of constants and numbers;
sultana
parents:
47691
diff
changeset
|
332 |
| Quotient => 2 |
3d76c81b5ed2
improved non-interpretation of constants and numbers;
sultana
parents:
47691
diff
changeset
|
333 |
| Quotient_E => 2 |
3d76c81b5ed2
improved non-interpretation of constants and numbers;
sultana
parents:
47691
diff
changeset
|
334 |
| Quotient_T => 2 |
3d76c81b5ed2
improved non-interpretation of constants and numbers;
sultana
parents:
47691
diff
changeset
|
335 |
| Quotient_F => 2 |
3d76c81b5ed2
improved non-interpretation of constants and numbers;
sultana
parents:
47691
diff
changeset
|
336 |
| Remainder_E => 2 |
3d76c81b5ed2
improved non-interpretation of constants and numbers;
sultana
parents:
47691
diff
changeset
|
337 |
| Remainder_T => 2 |
3d76c81b5ed2
improved non-interpretation of constants and numbers;
sultana
parents:
47691
diff
changeset
|
338 |
| Remainder_F => 2 |
3d76c81b5ed2
improved non-interpretation of constants and numbers;
sultana
parents:
47691
diff
changeset
|
339 |
| Floor => 1 |
3d76c81b5ed2
improved non-interpretation of constants and numbers;
sultana
parents:
47691
diff
changeset
|
340 |
| Ceiling => 1 |
3d76c81b5ed2
improved non-interpretation of constants and numbers;
sultana
parents:
47691
diff
changeset
|
341 |
| Truncate => 1 |
3d76c81b5ed2
improved non-interpretation of constants and numbers;
sultana
parents:
47691
diff
changeset
|
342 |
| Round => 1 |
3d76c81b5ed2
improved non-interpretation of constants and numbers;
sultana
parents:
47691
diff
changeset
|
343 |
| To_Int => 1 |
3d76c81b5ed2
improved non-interpretation of constants and numbers;
sultana
parents:
47691
diff
changeset
|
344 |
| To_Rat => 1 |
3d76c81b5ed2
improved non-interpretation of constants and numbers;
sultana
parents:
47691
diff
changeset
|
345 |
| To_Real => 1 |
3d76c81b5ed2
improved non-interpretation of constants and numbers;
sultana
parents:
47691
diff
changeset
|
346 |
| Less => 2 |
3d76c81b5ed2
improved non-interpretation of constants and numbers;
sultana
parents:
47691
diff
changeset
|
347 |
| LessEq => 2 |
3d76c81b5ed2
improved non-interpretation of constants and numbers;
sultana
parents:
47691
diff
changeset
|
348 |
| Greater => 2 |
3d76c81b5ed2
improved non-interpretation of constants and numbers;
sultana
parents:
47691
diff
changeset
|
349 |
| GreaterEq => 2 |
3d76c81b5ed2
improved non-interpretation of constants and numbers;
sultana
parents:
47691
diff
changeset
|
350 |
| EvalEq => 2 |
3d76c81b5ed2
improved non-interpretation of constants and numbers;
sultana
parents:
47691
diff
changeset
|
351 |
| Is_Int => 1 |
3d76c81b5ed2
improved non-interpretation of constants and numbers;
sultana
parents:
47691
diff
changeset
|
352 |
| Is_Rat => 1 |
3d76c81b5ed2
improved non-interpretation of constants and numbers;
sultana
parents:
47691
diff
changeset
|
353 |
| Distinct => 1 |
3d76c81b5ed2
improved non-interpretation of constants and numbers;
sultana
parents:
47691
diff
changeset
|
354 |
| Apply=> 2 |
3d76c81b5ed2
improved non-interpretation of constants and numbers;
sultana
parents:
47691
diff
changeset
|
355 |
|
47570
df3c9aa6c9dc
improved threading of thy-values through interpret functions;
sultana
parents:
47569
diff
changeset
|
356 |
fun interpret_symbol config language const_map symb thy = |
46844 | 357 |
case symb of |
358 |
Uninterpreted n => |
|
359 |
(*Constant would have been added to the map at the time of |
|
360 |
declaration*) |
|
361 |
the_const config thy language const_map n |
|
362 |
| Interpreted_ExtraLogic interpreted_symbol => |
|
47692
3d76c81b5ed2
improved non-interpretation of constants and numbers;
sultana
parents:
47691
diff
changeset
|
363 |
(*FIXME not interpreting*) |
3d76c81b5ed2
improved non-interpretation of constants and numbers;
sultana
parents:
47691
diff
changeset
|
364 |
Sign.mk_const thy ((Sign.full_name thy (mk_binding config |
3d76c81b5ed2
improved non-interpretation of constants and numbers;
sultana
parents:
47691
diff
changeset
|
365 |
(string_of_interpreted_symbol interpreted_symbol))), []) |
46844 | 366 |
| Interpreted_Logic logic_symbol => |
367 |
(case logic_symbol of |
|
368 |
Equals => HOLogic.eq_const Term.dummyT |
|
369 |
| NEquals => |
|
370 |
HOLogic.mk_not (HOLogic.eq_const Term.dummyT $ Bound 1 $ Bound 0) |
|
371 |
|> (Term.absdummy Term.dummyT #> Term.absdummy Term.dummyT) |
|
372 |
| Or => HOLogic.disj |
|
373 |
| And => HOLogic.conj |
|
374 |
| Iff => HOLogic.eq_const HOLogic.boolT |
|
375 |
| If => HOLogic.imp |
|
376 |
| Fi => @{term "\<lambda> x. \<lambda> y. y \<longrightarrow> x"} |
|
377 |
| Xor => |
|
378 |
@{term |
|
379 |
"\<lambda> x. \<lambda> y. \<not> (x \<longleftrightarrow> y)"} |
|
380 |
| Nor => @{term "\<lambda> x. \<lambda> y. \<not> (x \<or> y)"} |
|
381 |
| Nand => @{term "\<lambda> x. \<lambda> y. \<not> (x \<and> y)"} |
|
382 |
| Not => HOLogic.Not |
|
383 |
| Op_Forall => HOLogic.all_const Term.dummyT |
|
384 |
| Op_Exists => HOLogic.exists_const Term.dummyT |
|
385 |
| True => @{term "True"} |
|
386 |
| False => @{term "False"} |
|
387 |
) |
|
388 |
| TypeSymbol _ => |
|
389 |
raise MISINTERPRET_SYMBOL |
|
390 |
("Cannot have TypeSymbol in term", symb) |
|
48829
6ed588c4f963
look in current directory first before looking up includes in the TPTP directory, as required by Geoff
blanchet
parents:
47729
diff
changeset
|
391 |
| System _ => |
46844 | 392 |
raise MISINTERPRET_SYMBOL |
47510 | 393 |
("Cannot interpret system symbol", symb) |
46844 | 394 |
|
395 |
(*Apply a function to a list of arguments*) |
|
396 |
val mapply = fold (fn x => fn y => y $ x) |
|
47570
df3c9aa6c9dc
improved threading of thy-values through interpret functions;
sultana
parents:
47569
diff
changeset
|
397 |
|
df3c9aa6c9dc
improved threading of thy-values through interpret functions;
sultana
parents:
47569
diff
changeset
|
398 |
fun mapply' (args, thy) f = |
df3c9aa6c9dc
improved threading of thy-values through interpret functions;
sultana
parents:
47569
diff
changeset
|
399 |
let |
df3c9aa6c9dc
improved threading of thy-values through interpret functions;
sultana
parents:
47569
diff
changeset
|
400 |
val (f', thy') = f thy |
df3c9aa6c9dc
improved threading of thy-values through interpret functions;
sultana
parents:
47569
diff
changeset
|
401 |
in (mapply args f', thy') end |
df3c9aa6c9dc
improved threading of thy-values through interpret functions;
sultana
parents:
47569
diff
changeset
|
402 |
|
46844 | 403 |
(*As above, but for products*) |
404 |
fun mtimes thy = |
|
405 |
fold (fn x => fn y => |
|
406 |
Sign.mk_const thy |
|
47692
3d76c81b5ed2
improved non-interpretation of constants and numbers;
sultana
parents:
47691
diff
changeset
|
407 |
("Product_Type.Pair", [Term.dummyT, Term.dummyT]) $ y $ x) |
46844 | 408 |
|
47570
df3c9aa6c9dc
improved threading of thy-values through interpret functions;
sultana
parents:
47569
diff
changeset
|
409 |
fun mtimes' (args, thy) f = |
df3c9aa6c9dc
improved threading of thy-values through interpret functions;
sultana
parents:
47569
diff
changeset
|
410 |
let |
df3c9aa6c9dc
improved threading of thy-values through interpret functions;
sultana
parents:
47569
diff
changeset
|
411 |
val (f', thy') = f thy |
df3c9aa6c9dc
improved threading of thy-values through interpret functions;
sultana
parents:
47569
diff
changeset
|
412 |
in (mtimes thy' args f', thy') end |
df3c9aa6c9dc
improved threading of thy-values through interpret functions;
sultana
parents:
47569
diff
changeset
|
413 |
|
47692
3d76c81b5ed2
improved non-interpretation of constants and numbers;
sultana
parents:
47691
diff
changeset
|
414 |
datatype tptp_atom_value = |
3d76c81b5ed2
improved non-interpretation of constants and numbers;
sultana
parents:
47691
diff
changeset
|
415 |
Atom_App of tptp_term |
3d76c81b5ed2
improved non-interpretation of constants and numbers;
sultana
parents:
47691
diff
changeset
|
416 |
| Atom_Arity of string * int (*FIXME instead of int could use type list*) |
47570
df3c9aa6c9dc
improved threading of thy-values through interpret functions;
sultana
parents:
47569
diff
changeset
|
417 |
|
47692
3d76c81b5ed2
improved non-interpretation of constants and numbers;
sultana
parents:
47691
diff
changeset
|
418 |
(*Adds constants to signature when explicit type declaration isn't |
3d76c81b5ed2
improved non-interpretation of constants and numbers;
sultana
parents:
47691
diff
changeset
|
419 |
expected, e.g. FOL. "formula_level" means that the constants are to be interpreted |
3d76c81b5ed2
improved non-interpretation of constants and numbers;
sultana
parents:
47691
diff
changeset
|
420 |
as predicates, otherwise as functions over individuals.*) |
3d76c81b5ed2
improved non-interpretation of constants and numbers;
sultana
parents:
47691
diff
changeset
|
421 |
fun type_atoms_to_thy config formula_level type_map tptp_atom_value thy = |
46844 | 422 |
let |
423 |
val ind_type = interpret_type config thy type_map (Defined_type Type_Ind) |
|
424 |
val value_type = |
|
425 |
if formula_level then |
|
426 |
interpret_type config thy type_map (Defined_type Type_Bool) |
|
427 |
else ind_type |
|
47692
3d76c81b5ed2
improved non-interpretation of constants and numbers;
sultana
parents:
47691
diff
changeset
|
428 |
in case tptp_atom_value of |
3d76c81b5ed2
improved non-interpretation of constants and numbers;
sultana
parents:
47691
diff
changeset
|
429 |
Atom_App (Term_Func (symb, tptp_ts)) => |
46844 | 430 |
let |
47692
3d76c81b5ed2
improved non-interpretation of constants and numbers;
sultana
parents:
47691
diff
changeset
|
431 |
val thy' = fold (fn t => |
3d76c81b5ed2
improved non-interpretation of constants and numbers;
sultana
parents:
47691
diff
changeset
|
432 |
type_atoms_to_thy config false type_map (Atom_App t)) tptp_ts thy |
46844 | 433 |
in |
434 |
case symb of |
|
435 |
Uninterpreted const_name => |
|
47692
3d76c81b5ed2
improved non-interpretation of constants and numbers;
sultana
parents:
47691
diff
changeset
|
436 |
declare_const_ifnot config const_name |
3d76c81b5ed2
improved non-interpretation of constants and numbers;
sultana
parents:
47691
diff
changeset
|
437 |
(mk_fun_type (replicate (length tptp_ts) ind_type) value_type I) thy' |
3d76c81b5ed2
improved non-interpretation of constants and numbers;
sultana
parents:
47691
diff
changeset
|
438 |
|> snd |
46844 | 439 |
| _ => thy' |
440 |
end |
|
47692
3d76c81b5ed2
improved non-interpretation of constants and numbers;
sultana
parents:
47691
diff
changeset
|
441 |
| Atom_App _ => thy |
3d76c81b5ed2
improved non-interpretation of constants and numbers;
sultana
parents:
47691
diff
changeset
|
442 |
| Atom_Arity (const_name, n_args) => |
3d76c81b5ed2
improved non-interpretation of constants and numbers;
sultana
parents:
47691
diff
changeset
|
443 |
declare_const_ifnot config const_name |
3d76c81b5ed2
improved non-interpretation of constants and numbers;
sultana
parents:
47691
diff
changeset
|
444 |
(mk_fun_type (replicate n_args ind_type) value_type I) thy |
3d76c81b5ed2
improved non-interpretation of constants and numbers;
sultana
parents:
47691
diff
changeset
|
445 |
|> snd |
46844 | 446 |
end |
447 |
||
47692
3d76c81b5ed2
improved non-interpretation of constants and numbers;
sultana
parents:
47691
diff
changeset
|
448 |
(*FIXME only used until interpretation is implemented*) |
3d76c81b5ed2
improved non-interpretation of constants and numbers;
sultana
parents:
47691
diff
changeset
|
449 |
fun add_interp_symbols_to_thy config type_map thy = |
46844 | 450 |
let |
47692
3d76c81b5ed2
improved non-interpretation of constants and numbers;
sultana
parents:
47691
diff
changeset
|
451 |
val ind_symbols = [UMinus, Sum, Difference, Product, Quotient, Quotient_E, |
3d76c81b5ed2
improved non-interpretation of constants and numbers;
sultana
parents:
47691
diff
changeset
|
452 |
Quotient_T, Quotient_F, Remainder_E, Remainder_T, Remainder_F, Floor, |
3d76c81b5ed2
improved non-interpretation of constants and numbers;
sultana
parents:
47691
diff
changeset
|
453 |
Ceiling, Truncate, Round, To_Int, To_Rat, To_Real, Distinct, Apply] |
3d76c81b5ed2
improved non-interpretation of constants and numbers;
sultana
parents:
47691
diff
changeset
|
454 |
val bool_symbols = [Less, LessEq, Greater, GreaterEq, EvalEq, Is_Int, Is_Rat] |
3d76c81b5ed2
improved non-interpretation of constants and numbers;
sultana
parents:
47691
diff
changeset
|
455 |
fun add_interp_symbol_to_thy formula_level symbol = |
3d76c81b5ed2
improved non-interpretation of constants and numbers;
sultana
parents:
47691
diff
changeset
|
456 |
type_atoms_to_thy config formula_level type_map |
3d76c81b5ed2
improved non-interpretation of constants and numbers;
sultana
parents:
47691
diff
changeset
|
457 |
(Atom_Arity (string_of_interpreted_symbol symbol, arity_of symbol)) |
46844 | 458 |
in |
47692
3d76c81b5ed2
improved non-interpretation of constants and numbers;
sultana
parents:
47691
diff
changeset
|
459 |
fold (add_interp_symbol_to_thy false) ind_symbols thy |
3d76c81b5ed2
improved non-interpretation of constants and numbers;
sultana
parents:
47691
diff
changeset
|
460 |
|> fold (add_interp_symbol_to_thy true) bool_symbols |
46844 | 461 |
end |
462 |
||
463 |
(*Next batch of functions give info about Isabelle/HOL types*) |
|
464 |
fun is_fun (Type ("fun", _)) = true |
|
465 |
| is_fun _ = false |
|
466 |
fun is_prod (Type ("Product_Type.prod", _)) = true |
|
467 |
| is_prod _ = false |
|
468 |
fun dom_type (Type ("fun", [ty1, _])) = ty1 |
|
469 |
fun is_prod_typed thy config symb = |
|
470 |
let |
|
471 |
fun symb_type const_name = |
|
472 |
Sign.the_const_type thy (full_name thy config const_name) |
|
473 |
in |
|
474 |
case symb of |
|
475 |
Uninterpreted const_name => |
|
476 |
if is_fun (symb_type const_name) then |
|
477 |
symb_type const_name |> dom_type |> is_prod |
|
478 |
else false |
|
479 |
| _ => false |
|
480 |
end |
|
481 |
||
482 |
(* |
|
483 |
Information needed to be carried around: |
|
484 |
- constant mapping: maps constant names to Isabelle terms with fully-qualified |
|
485 |
names. This is fixed, and it is determined by declaration lines earlier |
|
486 |
in the script (i.e. constants must be declared before appearing in terms. |
|
487 |
- type context: maps bound variables to their Isabelle type. This is discarded |
|
47515 | 488 |
after each call of interpret_term since variables' cannot be bound across |
46844 | 489 |
terms. |
490 |
*) |
|
47570
df3c9aa6c9dc
improved threading of thy-values through interpret functions;
sultana
parents:
47569
diff
changeset
|
491 |
fun interpret_term formula_level config language const_map var_types type_map |
df3c9aa6c9dc
improved threading of thy-values through interpret functions;
sultana
parents:
47569
diff
changeset
|
492 |
tptp_t thy = |
46844 | 493 |
case tptp_t of |
494 |
Term_Func (symb, tptp_ts) => |
|
495 |
let |
|
47692
3d76c81b5ed2
improved non-interpretation of constants and numbers;
sultana
parents:
47691
diff
changeset
|
496 |
val thy' = |
3d76c81b5ed2
improved non-interpretation of constants and numbers;
sultana
parents:
47691
diff
changeset
|
497 |
type_atoms_to_thy config formula_level type_map (Atom_App tptp_t) thy |
46844 | 498 |
in |
499 |
case symb of |
|
500 |
Interpreted_ExtraLogic Apply => |
|
501 |
(*apply the head of the argument list to the tail*) |
|
47570
df3c9aa6c9dc
improved threading of thy-values through interpret functions;
sultana
parents:
47569
diff
changeset
|
502 |
(mapply' |
df3c9aa6c9dc
improved threading of thy-values through interpret functions;
sultana
parents:
47569
diff
changeset
|
503 |
(fold_map (interpret_term false config language const_map |
df3c9aa6c9dc
improved threading of thy-values through interpret functions;
sultana
parents:
47569
diff
changeset
|
504 |
var_types type_map) (tl tptp_ts) thy') |
df3c9aa6c9dc
improved threading of thy-values through interpret functions;
sultana
parents:
47569
diff
changeset
|
505 |
(interpret_term formula_level config language const_map |
df3c9aa6c9dc
improved threading of thy-values through interpret functions;
sultana
parents:
47569
diff
changeset
|
506 |
var_types type_map (hd tptp_ts))) |
46844 | 507 |
| _ => |
508 |
(*apply symb to tptp_ts*) |
|
509 |
if is_prod_typed thy' config symb then |
|
47570
df3c9aa6c9dc
improved threading of thy-values through interpret functions;
sultana
parents:
47569
diff
changeset
|
510 |
let |
df3c9aa6c9dc
improved threading of thy-values through interpret functions;
sultana
parents:
47569
diff
changeset
|
511 |
val (t, thy'') = |
df3c9aa6c9dc
improved threading of thy-values through interpret functions;
sultana
parents:
47569
diff
changeset
|
512 |
mtimes' |
df3c9aa6c9dc
improved threading of thy-values through interpret functions;
sultana
parents:
47569
diff
changeset
|
513 |
(fold_map (interpret_term false config language const_map |
df3c9aa6c9dc
improved threading of thy-values through interpret functions;
sultana
parents:
47569
diff
changeset
|
514 |
var_types type_map) (tl tptp_ts) thy') |
df3c9aa6c9dc
improved threading of thy-values through interpret functions;
sultana
parents:
47569
diff
changeset
|
515 |
(interpret_term false config language const_map |
df3c9aa6c9dc
improved threading of thy-values through interpret functions;
sultana
parents:
47569
diff
changeset
|
516 |
var_types type_map (hd tptp_ts)) |
df3c9aa6c9dc
improved threading of thy-values through interpret functions;
sultana
parents:
47569
diff
changeset
|
517 |
in (interpret_symbol config language const_map symb thy' $ t, thy'') |
df3c9aa6c9dc
improved threading of thy-values through interpret functions;
sultana
parents:
47569
diff
changeset
|
518 |
end |
46844 | 519 |
else |
47570
df3c9aa6c9dc
improved threading of thy-values through interpret functions;
sultana
parents:
47569
diff
changeset
|
520 |
( |
df3c9aa6c9dc
improved threading of thy-values through interpret functions;
sultana
parents:
47569
diff
changeset
|
521 |
mapply' |
df3c9aa6c9dc
improved threading of thy-values through interpret functions;
sultana
parents:
47569
diff
changeset
|
522 |
(fold_map (interpret_term false config language const_map |
df3c9aa6c9dc
improved threading of thy-values through interpret functions;
sultana
parents:
47569
diff
changeset
|
523 |
var_types type_map) tptp_ts thy') |
df3c9aa6c9dc
improved threading of thy-values through interpret functions;
sultana
parents:
47569
diff
changeset
|
524 |
(`(interpret_symbol config language const_map symb)) |
df3c9aa6c9dc
improved threading of thy-values through interpret functions;
sultana
parents:
47569
diff
changeset
|
525 |
) |
46844 | 526 |
end |
527 |
| Term_Var n => |
|
528 |
(if language = THF orelse language = TFF then |
|
529 |
(case AList.lookup (op =) var_types n of |
|
530 |
SOME ty => |
|
531 |
(case ty of |
|
532 |
SOME ty => Free (n, ty) |
|
533 |
| NONE => Free (n, Term.dummyT) (*to infer the variable's type*) |
|
534 |
) |
|
535 |
| NONE => |
|
536 |
raise MISINTERPRET_TERM ("Could not type variable", tptp_t)) |
|
537 |
else (*variables range over individuals*) |
|
538 |
Free (n, interpret_type config thy type_map (Defined_type Type_Ind)), |
|
539 |
thy) |
|
540 |
| Term_Conditional (tptp_formula, tptp_t1, tptp_t2) => |
|
47691 | 541 |
let |
542 |
val (t_fmla, thy') = |
|
543 |
interpret_formula config language const_map var_types type_map tptp_formula thy |
|
544 |
val ([t1, t2], thy'') = |
|
545 |
fold_map (interpret_term formula_level config language const_map var_types type_map) |
|
546 |
[tptp_t1, tptp_t2] thy' |
|
47692
3d76c81b5ed2
improved non-interpretation of constants and numbers;
sultana
parents:
47691
diff
changeset
|
547 |
in (mk_n_fun 3 @{const_name If} $ t_fmla $ t1 $ t2, thy'') end |
46844 | 548 |
| Term_Num (number_kind, num) => |
549 |
let |
|
47692
3d76c81b5ed2
improved non-interpretation of constants and numbers;
sultana
parents:
47691
diff
changeset
|
550 |
(*FIXME hack*) |
3d76c81b5ed2
improved non-interpretation of constants and numbers;
sultana
parents:
47691
diff
changeset
|
551 |
val ind_type = interpret_type config thy type_map (Defined_type Type_Ind) |
3d76c81b5ed2
improved non-interpretation of constants and numbers;
sultana
parents:
47691
diff
changeset
|
552 |
val prefix = case number_kind of |
3d76c81b5ed2
improved non-interpretation of constants and numbers;
sultana
parents:
47691
diff
changeset
|
553 |
Int_num => "intn_" |
3d76c81b5ed2
improved non-interpretation of constants and numbers;
sultana
parents:
47691
diff
changeset
|
554 |
| Real_num => "realn_" |
3d76c81b5ed2
improved non-interpretation of constants and numbers;
sultana
parents:
47691
diff
changeset
|
555 |
| Rat_num => "ratn_" |
3d76c81b5ed2
improved non-interpretation of constants and numbers;
sultana
parents:
47691
diff
changeset
|
556 |
(*FIXME hack -- for Int_num should be |
3d76c81b5ed2
improved non-interpretation of constants and numbers;
sultana
parents:
47691
diff
changeset
|
557 |
HOLogic.mk_number @{typ "int"} (the (Int.fromString num))*) |
3d76c81b5ed2
improved non-interpretation of constants and numbers;
sultana
parents:
47691
diff
changeset
|
558 |
in declare_const_ifnot config (prefix ^ num) ind_type thy end |
46844 | 559 |
| Term_Distinct_Object str => |
47570
df3c9aa6c9dc
improved threading of thy-values through interpret functions;
sultana
parents:
47569
diff
changeset
|
560 |
declare_constant config ("do_" ^ str) |
47514 | 561 |
(interpret_type config thy type_map (Defined_type Type_Ind)) thy |
46844 | 562 |
|
47691 | 563 |
and interpret_formula config language const_map var_types type_map tptp_fmla thy = |
46844 | 564 |
case tptp_fmla of |
565 |
Pred app => |
|
47570
df3c9aa6c9dc
improved threading of thy-values through interpret functions;
sultana
parents:
47569
diff
changeset
|
566 |
interpret_term true config language const_map |
df3c9aa6c9dc
improved threading of thy-values through interpret functions;
sultana
parents:
47569
diff
changeset
|
567 |
var_types type_map (Term_Func app) thy |
46844 | 568 |
| Fmla (symbol, tptp_formulas) => |
569 |
(case symbol of |
|
570 |
Interpreted_ExtraLogic Apply => |
|
47570
df3c9aa6c9dc
improved threading of thy-values through interpret functions;
sultana
parents:
47569
diff
changeset
|
571 |
mapply' |
df3c9aa6c9dc
improved threading of thy-values through interpret functions;
sultana
parents:
47569
diff
changeset
|
572 |
(fold_map (interpret_formula config language const_map |
df3c9aa6c9dc
improved threading of thy-values through interpret functions;
sultana
parents:
47569
diff
changeset
|
573 |
var_types type_map) (tl tptp_formulas) thy) |
df3c9aa6c9dc
improved threading of thy-values through interpret functions;
sultana
parents:
47569
diff
changeset
|
574 |
(interpret_formula config language const_map |
df3c9aa6c9dc
improved threading of thy-values through interpret functions;
sultana
parents:
47569
diff
changeset
|
575 |
var_types type_map (hd tptp_formulas)) |
46844 | 576 |
| Uninterpreted const_name => |
577 |
let |
|
578 |
val (args, thy') = (fold_map (interpret_formula config language |
|
579 |
const_map var_types type_map) tptp_formulas thy) |
|
47692
3d76c81b5ed2
improved non-interpretation of constants and numbers;
sultana
parents:
47691
diff
changeset
|
580 |
val thy' = |
3d76c81b5ed2
improved non-interpretation of constants and numbers;
sultana
parents:
47691
diff
changeset
|
581 |
type_atoms_to_thy config true type_map |
3d76c81b5ed2
improved non-interpretation of constants and numbers;
sultana
parents:
47691
diff
changeset
|
582 |
(Atom_Arity (const_name, length tptp_formulas)) thy' |
46844 | 583 |
in |
584 |
(if is_prod_typed thy' config symbol then |
|
47570
df3c9aa6c9dc
improved threading of thy-values through interpret functions;
sultana
parents:
47569
diff
changeset
|
585 |
mtimes thy' args (interpret_symbol config language |
df3c9aa6c9dc
improved threading of thy-values through interpret functions;
sultana
parents:
47569
diff
changeset
|
586 |
const_map symbol thy') |
46844 | 587 |
else |
588 |
mapply args |
|
47570
df3c9aa6c9dc
improved threading of thy-values through interpret functions;
sultana
parents:
47569
diff
changeset
|
589 |
(interpret_symbol config language const_map symbol thy'), |
46844 | 590 |
thy') |
591 |
end |
|
592 |
| _ => |
|
593 |
let |
|
594 |
val (args, thy') = |
|
595 |
fold_map |
|
596 |
(interpret_formula config language |
|
597 |
const_map var_types type_map) |
|
598 |
tptp_formulas thy |
|
599 |
in |
|
600 |
(if is_prod_typed thy' config symbol then |
|
47570
df3c9aa6c9dc
improved threading of thy-values through interpret functions;
sultana
parents:
47569
diff
changeset
|
601 |
mtimes thy' args (interpret_symbol config language |
df3c9aa6c9dc
improved threading of thy-values through interpret functions;
sultana
parents:
47569
diff
changeset
|
602 |
const_map symbol thy') |
46844 | 603 |
else |
604 |
mapply args |
|
47570
df3c9aa6c9dc
improved threading of thy-values through interpret functions;
sultana
parents:
47569
diff
changeset
|
605 |
(interpret_symbol config language const_map symbol thy'), |
46844 | 606 |
thy') |
607 |
end) |
|
608 |
| Sequent _ => |
|
47510 | 609 |
(*FIXME unsupported*) |
610 |
raise MISINTERPRET_FORMULA ("'Sequent' unsupported", tptp_fmla) |
|
46844 | 611 |
| Quant (quantifier, bindings, tptp_formula) => |
612 |
let |
|
613 |
val var_types' = |
|
47692
3d76c81b5ed2
improved non-interpretation of constants and numbers;
sultana
parents:
47691
diff
changeset
|
614 |
ListPair.unzip bindings |
47729 | 615 |
|> (apsnd ((map o Option.map) (interpret_type config thy type_map))) |
47692
3d76c81b5ed2
improved non-interpretation of constants and numbers;
sultana
parents:
47691
diff
changeset
|
616 |
|> ListPair.zip |
3d76c81b5ed2
improved non-interpretation of constants and numbers;
sultana
parents:
47691
diff
changeset
|
617 |
|> List.rev |
46844 | 618 |
fun fold_bind f = |
619 |
fold |
|
620 |
(fn (n, ty) => fn t => |
|
621 |
case ty of |
|
622 |
NONE => |
|
623 |
f (n, |
|
624 |
if language = THF then Term.dummyT |
|
625 |
else |
|
626 |
interpret_type config thy type_map |
|
627 |
(Defined_type Type_Ind), |
|
628 |
t) |
|
629 |
| SOME ty => f (n, ty, t) |
|
630 |
) |
|
631 |
var_types' |
|
632 |
in case quantifier of |
|
633 |
Forall => |
|
634 |
interpret_formula config language const_map (var_types' @ var_types) |
|
635 |
type_map tptp_formula thy |
|
636 |
|>> fold_bind HOLogic.mk_all |
|
637 |
| Exists => |
|
638 |
interpret_formula config language const_map (var_types' @ var_types) |
|
639 |
type_map tptp_formula thy |
|
640 |
|>> fold_bind HOLogic.mk_exists |
|
641 |
| Lambda => |
|
642 |
interpret_formula config language const_map (var_types' @ var_types) |
|
643 |
type_map tptp_formula thy |
|
644 |
|>> fold_bind (fn (n, ty, rest) => lambda (Free (n, ty)) rest) |
|
645 |
| Epsilon => |
|
646 |
let val (t, thy') = |
|
647 |
interpret_formula config language const_map var_types type_map |
|
648 |
(Quant (Lambda, bindings, tptp_formula)) thy |
|
649 |
in ((HOLogic.choice_const Term.dummyT) $ t, thy') end |
|
650 |
| Iota => |
|
651 |
let val (t, thy') = |
|
652 |
interpret_formula config language const_map var_types type_map |
|
653 |
(Quant (Lambda, bindings, tptp_formula)) thy |
|
654 |
in (Const (@{const_name The}, Term.dummyT) $ t, thy') end |
|
655 |
| Dep_Prod => |
|
656 |
raise MISINTERPRET_FORMULA ("Unsupported", tptp_fmla) |
|
657 |
| Dep_Sum => |
|
658 |
raise MISINTERPRET_FORMULA ("Unsupported", tptp_fmla) |
|
659 |
end |
|
47359 | 660 |
| Conditional (fmla1, fmla2, fmla3) => |
661 |
let |
|
662 |
val interp = interpret_formula config language const_map var_types type_map |
|
663 |
val (((fmla1', fmla2'), fmla3'), thy') = |
|
664 |
interp fmla1 thy |
|
665 |
||>> interp fmla2 |
|
666 |
||>> interp fmla3 |
|
667 |
in (HOLogic.mk_conj (HOLogic.mk_imp (fmla1', fmla2'), |
|
668 |
HOLogic.mk_imp (HOLogic.mk_not fmla1', fmla3')), |
|
669 |
thy') |
|
670 |
end |
|
671 |
| Let (tptp_let_list, tptp_formula) => (*FIXME not yet implemented*) |
|
672 |
raise MISINTERPRET_FORMULA ("'Let' not yet implemented", tptp_fmla) |
|
46844 | 673 |
| Atom tptp_atom => |
674 |
(case tptp_atom of |
|
675 |
TFF_Typed_Atom (symbol, tptp_type_opt) => |
|
676 |
(*FIXME ignoring type info*) |
|
47570
df3c9aa6c9dc
improved threading of thy-values through interpret functions;
sultana
parents:
47569
diff
changeset
|
677 |
(interpret_symbol config language const_map symbol thy, thy) |
46844 | 678 |
| THF_Atom_term tptp_term => |
47570
df3c9aa6c9dc
improved threading of thy-values through interpret functions;
sultana
parents:
47569
diff
changeset
|
679 |
interpret_term true config language const_map var_types |
df3c9aa6c9dc
improved threading of thy-values through interpret functions;
sultana
parents:
47569
diff
changeset
|
680 |
type_map tptp_term thy |
46844 | 681 |
| THF_Atom_conn_term symbol => |
47570
df3c9aa6c9dc
improved threading of thy-values through interpret functions;
sultana
parents:
47569
diff
changeset
|
682 |
(interpret_symbol config language const_map symbol thy, thy)) |
47510 | 683 |
| Type_fmla _ => |
46844 | 684 |
raise MISINTERPRET_FORMULA |
685 |
("Cannot interpret types as formulas", tptp_fmla) |
|
686 |
| THF_typing (tptp_formula, _) => (*FIXME ignoring type info*) |
|
687 |
interpret_formula config language |
|
688 |
const_map var_types type_map tptp_formula thy |
|
689 |
||
690 |
(*Extract the type from a typing*) |
|
691 |
local |
|
692 |
fun extract_type tptp_type = |
|
693 |
case tptp_type of |
|
694 |
Fmla_type typ => fmlatype_to_type typ |
|
695 |
| _ => tptp_type |
|
696 |
in |
|
697 |
fun typeof_typing (THF_typing (_, tptp_type)) = extract_type tptp_type |
|
698 |
fun typeof_tff_typing (Atom (TFF_Typed_Atom (_, SOME tptp_type))) = |
|
699 |
extract_type tptp_type |
|
700 |
end |
|
701 |
fun nameof_typing |
|
702 |
(THF_typing |
|
703 |
((Atom (THF_Atom_term (Term_Func (Uninterpreted str, [])))), _)) = str |
|
704 |
fun nameof_tff_typing (Atom (TFF_Typed_Atom (Uninterpreted str, _))) = str |
|
705 |
||
48829
6ed588c4f963
look in current directory first before looking up includes in the TPTP directory, as required by Geoff
blanchet
parents:
47729
diff
changeset
|
706 |
fun resolve_include_path path_prefixes path_suffix = |
6ed588c4f963
look in current directory first before looking up includes in the TPTP directory, as required by Geoff
blanchet
parents:
47729
diff
changeset
|
707 |
case find_first (fn prefix => File.exists (Path.append prefix path_suffix)) |
6ed588c4f963
look in current directory first before looking up includes in the TPTP directory, as required by Geoff
blanchet
parents:
47729
diff
changeset
|
708 |
path_prefixes of |
6ed588c4f963
look in current directory first before looking up includes in the TPTP directory, as required by Geoff
blanchet
parents:
47729
diff
changeset
|
709 |
SOME prefix => Path.append prefix path_suffix |
6ed588c4f963
look in current directory first before looking up includes in the TPTP directory, as required by Geoff
blanchet
parents:
47729
diff
changeset
|
710 |
| NONE => |
6ed588c4f963
look in current directory first before looking up includes in the TPTP directory, as required by Geoff
blanchet
parents:
47729
diff
changeset
|
711 |
error ("Cannot find include file " ^ quote (Path.implode path_suffix)) |
6ed588c4f963
look in current directory first before looking up includes in the TPTP directory, as required by Geoff
blanchet
parents:
47729
diff
changeset
|
712 |
|
6ed588c4f963
look in current directory first before looking up includes in the TPTP directory, as required by Geoff
blanchet
parents:
47729
diff
changeset
|
713 |
fun interpret_line config inc_list type_map const_map path_prefixes line thy = |
46844 | 714 |
case line of |
47569
fce9d97a3258
exceptions related to interpreting tptp problems now mention the relevant position in the tptp file;
sultana
parents:
47558
diff
changeset
|
715 |
Include (_, quoted_path, inc_list) => |
46844 | 716 |
interpret_file' |
717 |
config |
|
47511 | 718 |
inc_list |
48829
6ed588c4f963
look in current directory first before looking up includes in the TPTP directory, as required by Geoff
blanchet
parents:
47729
diff
changeset
|
719 |
path_prefixes |
6ed588c4f963
look in current directory first before looking up includes in the TPTP directory, as required by Geoff
blanchet
parents:
47729
diff
changeset
|
720 |
(resolve_include_path path_prefixes |
6ed588c4f963
look in current directory first before looking up includes in the TPTP directory, as required by Geoff
blanchet
parents:
47729
diff
changeset
|
721 |
(quoted_path |> unenclose |> Path.explode)) |
46844 | 722 |
type_map |
723 |
const_map |
|
724 |
thy |
|
47569
fce9d97a3258
exceptions related to interpreting tptp problems now mention the relevant position in the tptp file;
sultana
parents:
47558
diff
changeset
|
725 |
| Annotated_Formula (_, lang, label, role, tptp_formula, annotation_opt) => |
47511 | 726 |
(*interpret a line only if "label" is in "inc_list", or if "inc_list" is |
727 |
empty (in which case interpret all lines)*) |
|
728 |
(*FIXME could work better if inc_list were sorted*) |
|
729 |
if null inc_list orelse is_some (List.find (fn x => x = label) inc_list) then |
|
730 |
case role of |
|
731 |
Role_Type => |
|
732 |
let |
|
733 |
val (tptp_ty, name) = |
|
734 |
if lang = THF then |
|
735 |
(typeof_typing tptp_formula (*assuming tptp_formula is a typing*), |
|
736 |
nameof_typing tptp_formula (*and that the LHS is a (atom) name*)) |
|
737 |
else |
|
738 |
(typeof_tff_typing tptp_formula, |
|
739 |
nameof_tff_typing tptp_formula) |
|
740 |
in |
|
741 |
case tptp_ty of |
|
742 |
Defined_type Type_Type => (*add new type*) |
|
743 |
(*generate an Isabelle/HOL type to interpret this TPTP type, |
|
744 |
and add it to both the Isabelle/HOL theory and to the type_map*) |
|
46844 | 745 |
let |
47511 | 746 |
val (type_map', thy') = |
747 |
declare_type |
|
748 |
config |
|
749 |
(Atom_type name, name) |
|
750 |
type_map |
|
751 |
thy |
|
752 |
in ((type_map', |
|
753 |
const_map, |
|
754 |
[]), |
|
755 |
thy') |
|
46844 | 756 |
end |
47513
50a424b89952
improved naming of 'distinct objects' in tptp import
sultana
parents:
47511
diff
changeset
|
757 |
|
47511 | 758 |
| _ => (*declaration of constant*) |
759 |
(*Here we populate the map from constants to the Isabelle/HOL |
|
760 |
terms they map to (which in turn contain their types).*) |
|
761 |
let |
|
762 |
val ty = interpret_type config thy type_map tptp_ty |
|
763 |
(*make sure that the theory contains all the types appearing |
|
764 |
in this constant's signature. Exception is thrown if encounter |
|
765 |
an undeclared types.*) |
|
766 |
val (t, thy') = |
|
767 |
let |
|
768 |
fun analyse_type thy thf_ty = |
|
769 |
if #cautious config then |
|
770 |
case thf_ty of |
|
771 |
Fn_type (thf_ty1, thf_ty2) => |
|
772 |
(analyse_type thy thf_ty1; |
|
773 |
analyse_type thy thf_ty2) |
|
774 |
| Atom_type ty_name => |
|
47548 | 775 |
if type_exists config thy ty_name then () |
47511 | 776 |
else |
777 |
raise MISINTERPRET_TYPE |
|
778 |
("Type (in signature of " ^ |
|
779 |
name ^ ") has not been declared", |
|
780 |
Atom_type ty_name) |
|
781 |
| _ => () |
|
782 |
else () (*skip test if we're not being cautious.*) |
|
783 |
in |
|
784 |
analyse_type thy tptp_ty; |
|
785 |
declare_constant config name ty thy |
|
786 |
end |
|
787 |
(*register a mapping from name to t. Constants' type |
|
788 |
declarations should occur at most once, so it's justified to |
|
789 |
use "::". Note that here we use a constant's name rather |
|
790 |
than the possibly- new one, since all references in the |
|
791 |
theory will be to this name.*) |
|
792 |
val const_map' = ((name, t) :: const_map) |
|
793 |
in ((type_map,(*type_map unchanged, since a constant's |
|
794 |
declaration shouldn't include any new types.*) |
|
795 |
const_map',(*typing table of constant was extended*) |
|
796 |
[]),(*no formulas were interpreted*) |
|
797 |
thy')(*theory was extended with new constant*) |
|
798 |
end |
|
799 |
end |
|
47513
50a424b89952
improved naming of 'distinct objects' in tptp import
sultana
parents:
47511
diff
changeset
|
800 |
|
47511 | 801 |
| _ => (*i.e. the AF is not a type declaration*) |
802 |
let |
|
803 |
(*gather interpreted term, and the map of types occurring in that term*) |
|
804 |
val (t, thy') = |
|
805 |
interpret_formula config lang |
|
806 |
const_map [] type_map tptp_formula thy |
|
807 |
|>> HOLogic.mk_Trueprop |
|
808 |
(*type_maps grow monotonically, so return the newest value (type_mapped); |
|
809 |
there's no need to unify it with the type_map parameter.*) |
|
810 |
in |
|
811 |
((type_map, const_map, |
|
47548 | 812 |
[(label, role, |
47511 | 813 |
Syntax.check_term (Proof_Context.init_global thy') t, |
814 |
TPTP_Proof.extract_inference_info annotation_opt)]), thy') |
|
815 |
end |
|
816 |
else (*do nothing if we're not to includ this AF*) |
|
817 |
((type_map, const_map, []), thy) |
|
47569
fce9d97a3258
exceptions related to interpreting tptp problems now mention the relevant position in the tptp file;
sultana
parents:
47558
diff
changeset
|
818 |
|
48829
6ed588c4f963
look in current directory first before looking up includes in the TPTP directory, as required by Geoff
blanchet
parents:
47729
diff
changeset
|
819 |
and interpret_problem config inc_list path_prefixes lines type_map const_map thy = |
6ed588c4f963
look in current directory first before looking up includes in the TPTP directory, as required by Geoff
blanchet
parents:
47729
diff
changeset
|
820 |
let val thy_with_symbols = add_interp_symbols_to_thy config type_map thy in |
47511 | 821 |
fold (fn line => |
822 |
fn ((type_map, const_map, lines), thy) => |
|
823 |
let |
|
824 |
(*process the line, ignoring the type-context for variables*) |
|
825 |
val ((type_map', const_map', l'), thy') = |
|
48829
6ed588c4f963
look in current directory first before looking up includes in the TPTP directory, as required by Geoff
blanchet
parents:
47729
diff
changeset
|
826 |
interpret_line config inc_list type_map const_map path_prefixes |
6ed588c4f963
look in current directory first before looking up includes in the TPTP directory, as required by Geoff
blanchet
parents:
47729
diff
changeset
|
827 |
line thy |
47688 | 828 |
(*FIXME |
47569
fce9d97a3258
exceptions related to interpreting tptp problems now mention the relevant position in the tptp file;
sultana
parents:
47558
diff
changeset
|
829 |
handle |
fce9d97a3258
exceptions related to interpreting tptp problems now mention the relevant position in the tptp file;
sultana
parents:
47558
diff
changeset
|
830 |
(*package all exceptions to include position information, |
fce9d97a3258
exceptions related to interpreting tptp problems now mention the relevant position in the tptp file;
sultana
parents:
47558
diff
changeset
|
831 |
even relating to multiple levels of "include"ed files*) |
fce9d97a3258
exceptions related to interpreting tptp problems now mention the relevant position in the tptp file;
sultana
parents:
47558
diff
changeset
|
832 |
(*FIXME "exn" contents may appear garbled due to markup |
fce9d97a3258
exceptions related to interpreting tptp problems now mention the relevant position in the tptp file;
sultana
parents:
47558
diff
changeset
|
833 |
FIXME this appears as ML source position *) |
fce9d97a3258
exceptions related to interpreting tptp problems now mention the relevant position in the tptp file;
sultana
parents:
47558
diff
changeset
|
834 |
MISINTERPRET (pos_list, exn) => |
fce9d97a3258
exceptions related to interpreting tptp problems now mention the relevant position in the tptp file;
sultana
parents:
47558
diff
changeset
|
835 |
raise MISINTERPRET |
fce9d97a3258
exceptions related to interpreting tptp problems now mention the relevant position in the tptp file;
sultana
parents:
47558
diff
changeset
|
836 |
(TPTP_Syntax.pos_of_line line :: pos_list, exn) |
fce9d97a3258
exceptions related to interpreting tptp problems now mention the relevant position in the tptp file;
sultana
parents:
47558
diff
changeset
|
837 |
| exn => raise MISINTERPRET |
fce9d97a3258
exceptions related to interpreting tptp problems now mention the relevant position in the tptp file;
sultana
parents:
47558
diff
changeset
|
838 |
([TPTP_Syntax.pos_of_line line], exn) |
47688 | 839 |
*) |
47511 | 840 |
in |
841 |
((type_map', |
|
842 |
const_map', |
|
843 |
l' @ lines),(*append is sufficient, union would be overkill*) |
|
844 |
thy') |
|
845 |
end) |
|
846 |
lines (*lines of the problem file*) |
|
47692
3d76c81b5ed2
improved non-interpretation of constants and numbers;
sultana
parents:
47691
diff
changeset
|
847 |
((type_map, const_map, []), thy_with_symbols) (*initial values*) |
47511 | 848 |
end |
46844 | 849 |
|
48829
6ed588c4f963
look in current directory first before looking up includes in the TPTP directory, as required by Geoff
blanchet
parents:
47729
diff
changeset
|
850 |
and interpret_file' config inc_list path_prefixes file_name = |
46844 | 851 |
let |
852 |
val file_name' = Path.expand file_name |
|
853 |
in |
|
854 |
if Path.is_absolute file_name' then |
|
855 |
Path.implode file_name |
|
856 |
|> TPTP_Parser.parse_file |
|
48829
6ed588c4f963
look in current directory first before looking up includes in the TPTP directory, as required by Geoff
blanchet
parents:
47729
diff
changeset
|
857 |
|> interpret_problem config inc_list path_prefixes |
47510 | 858 |
else error "Could not determine absolute path to file" |
46844 | 859 |
end |
860 |
||
48829
6ed588c4f963
look in current directory first before looking up includes in the TPTP directory, as required by Geoff
blanchet
parents:
47729
diff
changeset
|
861 |
and interpret_file cautious path_prefixes file_name = |
46844 | 862 |
let |
863 |
val config = |
|
864 |
{cautious = cautious, |
|
865 |
problem_name = |
|
866 |
SOME (TPTP_Problem_Name.parse_problem_name ((Path.base #> Path.implode) |
|
47520 | 867 |
file_name))} |
48829
6ed588c4f963
look in current directory first before looking up includes in the TPTP directory, as required by Geoff
blanchet
parents:
47729
diff
changeset
|
868 |
in interpret_file' config [] path_prefixes file_name end |
46844 | 869 |
|
48829
6ed588c4f963
look in current directory first before looking up includes in the TPTP directory, as required by Geoff
blanchet
parents:
47729
diff
changeset
|
870 |
fun import_file cautious path_prefixes file_name type_map const_map thy = |
46844 | 871 |
let |
872 |
val prob_name = |
|
873 |
TPTP_Problem_Name.parse_problem_name (Path.implode (Path.base file_name)) |
|
874 |
val (result, thy') = |
|
48829
6ed588c4f963
look in current directory first before looking up includes in the TPTP directory, as required by Geoff
blanchet
parents:
47729
diff
changeset
|
875 |
interpret_file cautious path_prefixes file_name type_map const_map thy |
47520 | 876 |
(*FIXME doesn't check if problem has already been interpreted*) |
46844 | 877 |
in TPTP_Data.map (cons ((prob_name, result))) thy' end |
878 |
||
879 |
val _ = |
|
46961
5c6955f487e5
outer syntax command definitions based on formal command_spec derived from theory header declarations;
wenzelm
parents:
46951
diff
changeset
|
880 |
Outer_Syntax.improper_command @{command_spec "import_tptp"} "import TPTP problem" |
46951 | 881 |
(Parse.path >> (fn path => |
47366
f5a304ca037e
improved import_tptp to use standard TPTP directory structure; extended the TPTP testing theory to include an example of using the import_tptp command;
sultana
parents:
47360
diff
changeset
|
882 |
Toplevel.theory (fn thy => |
47558
55b42f9af99d
phase out "$TPTP_PROBLEMS_PATH"; prefer "$TPTP" for consistency with CASC setup
blanchet
parents:
47548
diff
changeset
|
883 |
(*NOTE: assumes include files are located at $TPTP/Axioms |
55b42f9af99d
phase out "$TPTP_PROBLEMS_PATH"; prefer "$TPTP" for consistency with CASC setup
blanchet
parents:
47548
diff
changeset
|
884 |
(which is how TPTP is organised)*) |
48829
6ed588c4f963
look in current directory first before looking up includes in the TPTP directory, as required by Geoff
blanchet
parents:
47729
diff
changeset
|
885 |
import_file true [Path.dir path, Path.explode "$TPTP"] path [] [] thy))) |
46844 | 886 |
|
887 |
end |