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