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