author | wenzelm |
Wed, 06 Jul 2005 10:41:43 +0200 | |
changeset 16709 | a4679ac06502 |
parent 16199 | ee95ab217fee |
child 16741 | 7a6c17b826c0 |
permissions | -rw-r--r-- |
15347 | 1 |
(* Author: Jia Meng, Cambridge University Computer Laboratory |
2 |
ID: $Id$ |
|
3 |
Copyright 2004 University of Cambridge |
|
4 |
||
5 |
ML data structure for storing/printing FOL clauses and arity clauses. |
|
6 |
Typed equality is treated differently. |
|
7 |
*) |
|
8 |
||
9 |
signature RES_CLAUSE = |
|
10 |
sig |
|
11 |
exception ARCLAUSE of string |
|
12 |
exception CLAUSE of string |
|
13 |
type arityClause |
|
14 |
type classrelClause |
|
15 |
val classrelClauses_of : |
|
16 |
string * string list -> classrelClause list |
|
17 |
type clause |
|
18 |
val keep_types : bool ref |
|
19 |
val make_axiom_arity_clause : |
|
20 |
string * (string * string list list) -> arityClause |
|
21 |
val make_axiom_classrelClause : |
|
15531 | 22 |
string * string option -> classrelClause |
15347 | 23 |
val make_axiom_clause : Term.term -> string * int -> clause |
24 |
val make_axiom_clause_thm : Thm.thm -> string * int -> clause |
|
25 |
val make_conjecture_clause : Term.term -> clause |
|
26 |
val make_conjecture_clause_thm : Thm.thm -> clause |
|
27 |
val make_hypothesis_clause : Term.term -> clause |
|
28 |
val make_hypothesis_clause_thm : Thm.thm -> clause |
|
29 |
val special_equal : bool ref |
|
30 |
val tptp_arity_clause : arityClause -> string |
|
31 |
val tptp_classrelClause : classrelClause -> string |
|
32 |
val tptp_clause : clause -> string list |
|
16039
dfe264950511
Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents:
15956
diff
changeset
|
33 |
val clause_info : clause -> string * string |
15347 | 34 |
val tptp_clauses2str : string list -> string |
35 |
val typed : unit -> unit |
|
36 |
val untyped : unit -> unit |
|
15608 | 37 |
val clause2tptp : clause -> string * string list |
38 |
val tfree_clause : string -> string |
|
15347 | 39 |
end; |
40 |
||
41 |
structure ResClause : RES_CLAUSE = |
|
42 |
struct |
|
43 |
||
44 |
(* Added for typed equality *) |
|
45 |
val special_equal = ref false; (* by default,equality does not carry type information *) |
|
46 |
val eq_typ_wrapper = "typeinfo"; (* default string *) |
|
47 |
||
48 |
||
49 |
val schematic_var_prefix = "V_"; |
|
50 |
val fixed_var_prefix = "v_"; |
|
51 |
||
52 |
||
53 |
val tvar_prefix = "Typ_"; |
|
54 |
val tfree_prefix = "typ_"; |
|
55 |
||
56 |
||
57 |
val clause_prefix = "cls_"; |
|
58 |
||
59 |
val arclause_prefix = "arcls_" |
|
60 |
||
61 |
val const_prefix = "const_"; |
|
62 |
val tconst_prefix = "tconst_"; |
|
63 |
||
16199
ee95ab217fee
no longer emits literals for type class HOL.type; also minor tidying
paulson
parents:
16039
diff
changeset
|
64 |
val class_prefix = "class_"; |
15347 | 65 |
|
66 |
||
67 |
||
68 |
(**** some useful functions ****) |
|
69 |
||
70 |
val const_trans_table = |
|
71 |
Symtab.make [("op =", "equal"), |
|
72 |
("op <=", "lessequals"), |
|
73 |
("op <", "less"), |
|
74 |
("op &", "and"), |
|
75 |
("op |", "or"), |
|
76 |
("op -->", "implies"), |
|
77 |
("op :", "in"), |
|
78 |
("op Un", "union"), |
|
79 |
("op Int", "inter")]; |
|
80 |
||
81 |
||
82 |
||
15610 | 83 |
(*Escaping of special characters. |
84 |
Alphanumeric characters are left unchanged. |
|
85 |
The character _ goes to __ |
|
86 |
Characters in the range ASCII space to / go to _A to _P, respectively. |
|
87 |
Other printing characters go to _NNN where NNN is the decimal ASCII code.*) |
|
88 |
local |
|
89 |
||
90 |
val A_minus_space = Char.ord #"A" - Char.ord #" "; |
|
91 |
||
15347 | 92 |
fun ascii_of_c c = |
15610 | 93 |
if Char.isAlphaNum c then String.str c |
94 |
else if c = #"_" then "__" |
|
95 |
else if #" " <= c andalso c <= #"/" |
|
96 |
then "_" ^ String.str (Char.chr (Char.ord c + A_minus_space)) |
|
97 |
else if Char.isPrint c then ("_" ^ Int.toString (Char.ord c)) |
|
98 |
else "" |
|
15347 | 99 |
|
15610 | 100 |
in |
101 |
||
102 |
val ascii_of = String.translate ascii_of_c; |
|
103 |
||
104 |
end; |
|
15347 | 105 |
|
106 |
||
107 |
(* another version of above functions that remove chars that may not be allowed by Vampire *) |
|
108 |
fun make_schematic_var v = schematic_var_prefix ^ (ascii_of v); |
|
109 |
fun make_fixed_var x = fixed_var_prefix ^ (ascii_of x); |
|
110 |
||
111 |
fun make_schematic_type_var v = tvar_prefix ^ (ascii_of v); |
|
112 |
fun make_fixed_type_var x = tfree_prefix ^ (ascii_of x); |
|
113 |
||
114 |
fun make_fixed_const c = const_prefix ^ (ascii_of c); |
|
115 |
fun make_fixed_type_const c = tconst_prefix ^ (ascii_of c); |
|
116 |
||
117 |
fun make_type_class clas = class_prefix ^ (ascii_of clas); |
|
118 |
||
119 |
||
120 |
||
121 |
||
122 |
fun lookup_const c = |
|
123 |
case Symtab.lookup (const_trans_table,c) of |
|
15531 | 124 |
SOME c' => c' |
125 |
| NONE => make_fixed_const c; |
|
15347 | 126 |
|
127 |
||
128 |
||
129 |
(***** definitions and functions for FOL clauses, prepared for conversion into TPTP format or SPASS format. *****) |
|
130 |
||
131 |
val keep_types = ref true; (* default is true *) |
|
132 |
fun untyped () = (keep_types := false); |
|
133 |
fun typed () = (keep_types := true); |
|
134 |
||
135 |
||
136 |
datatype kind = Axiom | Hypothesis | Conjecture; |
|
137 |
fun name_of_kind Axiom = "axiom" |
|
138 |
| name_of_kind Hypothesis = "hypothesis" |
|
139 |
| name_of_kind Conjecture = "conjecture"; |
|
140 |
||
141 |
type clause_id = int; |
|
142 |
type axiom_name = string; |
|
143 |
||
144 |
||
145 |
type polarity = bool; |
|
146 |
||
147 |
type indexname = Term.indexname; |
|
148 |
||
149 |
||
150 |
(* "tag" is used for vampire specific syntax *) |
|
151 |
type tag = bool; |
|
152 |
||
153 |
||
154 |
||
155 |
fun string_of_indexname (name,index) = name ^ "_" ^ (string_of_int index); |
|
156 |
||
157 |
||
158 |
val id_ref = ref 0; |
|
159 |
fun generate_id () = |
|
160 |
let val id = !id_ref |
|
161 |
in |
|
162 |
(id_ref:=id + 1; id) |
|
163 |
end; |
|
164 |
||
165 |
||
166 |
||
167 |
(**** Isabelle FOL clauses ****) |
|
168 |
||
169 |
(* by default it is false *) |
|
170 |
val tagged = ref false; |
|
171 |
||
172 |
type pred_name = string; |
|
173 |
type sort = Term.sort; |
|
174 |
type fol_type = string; |
|
175 |
||
176 |
||
177 |
datatype type_literal = LTVar of string | LTFree of string; |
|
178 |
||
179 |
||
180 |
datatype folTerm = UVar of string * fol_type| Fun of string * fol_type * folTerm list; |
|
181 |
datatype predicate = Predicate of pred_name * fol_type * folTerm list; |
|
182 |
||
183 |
||
184 |
datatype literal = Literal of polarity * predicate * tag; |
|
185 |
||
186 |
||
187 |
datatype typ_var = FOLTVar of indexname | FOLTFree of string; |
|
188 |
||
189 |
||
190 |
(* ML datatype used to repsent one single clause: disjunction of literals. *) |
|
191 |
datatype clause = |
|
192 |
Clause of {clause_id: clause_id, |
|
193 |
axiom_name: axiom_name, |
|
194 |
kind: kind, |
|
195 |
literals: literal list, |
|
196 |
types_sorts: (typ_var * sort) list, |
|
197 |
tvar_type_literals: type_literal list, |
|
198 |
tfree_type_literals: type_literal list }; |
|
199 |
||
200 |
||
201 |
exception CLAUSE of string; |
|
202 |
||
203 |
||
204 |
||
205 |
(*** make clauses ***) |
|
206 |
||
207 |
||
208 |
fun make_clause (clause_id,axiom_name,kind,literals,types_sorts,tvar_type_literals,tfree_type_literals) = |
|
209 |
Clause {clause_id = clause_id, axiom_name = axiom_name, kind = kind, literals = literals, types_sorts = types_sorts,tvar_type_literals = tvar_type_literals,tfree_type_literals = tfree_type_literals}; |
|
210 |
||
211 |
||
212 |
||
213 |
fun type_of (Type (a, [])) = (make_fixed_type_const a,[]) |
|
214 |
| type_of (Type (a, Ts)) = |
|
215 |
let val foltyps_ts = map type_of Ts |
|
15774 | 216 |
val (folTyps,ts) = ListPair.unzip foltyps_ts |
15347 | 217 |
val ts' = ResLib.flat_noDup ts |
218 |
in |
|
219 |
(((make_fixed_type_const a) ^ (ResLib.list_to_string folTyps)),ts') |
|
220 |
end |
|
221 |
| type_of (TFree (a, s)) = (make_fixed_type_var a, [((FOLTFree a),s)]) |
|
222 |
| type_of (TVar (v, s)) = (make_schematic_type_var (string_of_indexname v), [((FOLTVar v),s)]); |
|
15390 | 223 |
|
224 |
(* added: checkMeta: string -> bool *) |
|
225 |
(* Any meta vars like ?x should be treated as universal vars,although it is represented as "Free(...)" by Isabelle *) |
|
226 |
fun checkMeta s = |
|
227 |
let val chars = explode s |
|
228 |
in |
|
229 |
["M", "E", "T", "A", "H", "Y", "P", "1"] prefix chars |
|
230 |
end; |
|
231 |
||
15347 | 232 |
|
233 |
fun pred_name_type (Const(c,T)) = (lookup_const c,type_of T) |
|
15390 | 234 |
| pred_name_type (Free(x,T)) = |
235 |
let val is_meta = checkMeta x |
|
236 |
in |
|
237 |
if is_meta then (raise CLAUSE("Predicate Not First Order")) else |
|
238 |
(make_fixed_var x,type_of T) |
|
239 |
end |
|
15347 | 240 |
| pred_name_type (Var(_,_)) = raise CLAUSE("Predicate Not First Order") |
241 |
| pred_name_type _ = raise CLAUSE("Predicate input unexpected"); |
|
242 |
||
15615 | 243 |
|
244 |
(* For type equality *) |
|
245 |
(* here "arg_typ" is the type of "="'s argument's type, not the type of the equality *) |
|
246 |
(* Find type of equality arg *) |
|
247 |
fun eq_arg_type (Type("fun",[T,_])) = |
|
248 |
let val (folT,_) = type_of T; |
|
249 |
in |
|
250 |
folT |
|
251 |
end; |
|
252 |
||
253 |
||
254 |
||
15347 | 255 |
fun fun_name_type (Const(c,T)) = (lookup_const c,type_of T) |
256 |
| fun_name_type (Free(x,T)) = (make_fixed_var x,type_of T) |
|
257 |
| fun_name_type _ = raise CLAUSE("Function Not First Order"); |
|
258 |
||
259 |
||
15615 | 260 |
|
15347 | 261 |
fun term_of (Var(ind_nm,T)) = |
262 |
let val (folType,ts) = type_of T |
|
263 |
in |
|
264 |
(UVar(make_schematic_var(string_of_indexname ind_nm),folType),ts) |
|
265 |
end |
|
266 |
| term_of (Free(x,T)) = |
|
15390 | 267 |
let val is_meta = checkMeta x |
268 |
val (folType,ts) = type_of T |
|
15347 | 269 |
in |
15390 | 270 |
if is_meta then (UVar(make_schematic_var x,folType),ts) |
271 |
else |
|
272 |
(Fun(make_fixed_var x,folType,[]),ts) |
|
15347 | 273 |
end |
15615 | 274 |
| term_of (Const(c,T)) = (* impossible to be equality *) |
15347 | 275 |
let val (folType,ts) = type_of T |
276 |
in |
|
277 |
(Fun(lookup_const c,folType,[]),ts) |
|
278 |
end |
|
279 |
| term_of (app as (t $ a)) = |
|
280 |
let val (f,args) = strip_comb app |
|
281 |
fun term_of_aux () = |
|
282 |
let val (funName,(funType,ts1)) = fun_name_type f |
|
15774 | 283 |
val (args',ts2) = ListPair.unzip (map term_of args) |
15347 | 284 |
val ts3 = ResLib.flat_noDup (ts1::ts2) |
285 |
in |
|
286 |
(Fun(funName,funType,args'),ts3) |
|
287 |
end |
|
15615 | 288 |
fun term_of_eq ((Const ("op =", typ)),args) = |
289 |
let val arg_typ = eq_arg_type typ |
|
15774 | 290 |
val (args',ts) = ListPair.unzip (map term_of args) |
15615 | 291 |
val equal_name = lookup_const ("op =") |
292 |
in |
|
293 |
(Fun(equal_name,arg_typ,args'),ResLib.flat_noDup ts) |
|
294 |
end |
|
15347 | 295 |
in |
15615 | 296 |
case f of Const ("op =", typ) => term_of_eq (f,args) |
297 |
| Const(_,_) => term_of_aux () |
|
15390 | 298 |
| Free(s,_) => if (checkMeta s) then (raise CLAUSE("Function Not First Order")) else term_of_aux () |
15347 | 299 |
| _ => raise CLAUSE("Function Not First Order") |
300 |
end |
|
15390 | 301 |
| term_of _ = raise CLAUSE("Function Not First Order"); |
302 |
||
15347 | 303 |
|
304 |
||
305 |
||
306 |
fun pred_of_eq ((Const ("op =", typ)),args) = |
|
307 |
let val arg_typ = eq_arg_type typ |
|
15774 | 308 |
val (args',ts) = ListPair.unzip (map term_of args) |
15347 | 309 |
val equal_name = lookup_const "op =" |
310 |
in |
|
311 |
(Predicate(equal_name,arg_typ,args'),ResLib.flat_noDup ts) |
|
312 |
end; |
|
313 |
||
314 |
||
315 |
(* changed for non-equality predicate *) |
|
316 |
(* The input "pred" cannot be an equality *) |
|
317 |
fun pred_of_nonEq (pred,args) = |
|
318 |
let val (predName,(predType,ts1)) = pred_name_type pred |
|
15774 | 319 |
val (args',ts2) = ListPair.unzip (map term_of args) |
15347 | 320 |
val ts3 = ResLib.flat_noDup (ts1::ts2) |
321 |
in |
|
322 |
(Predicate(predName,predType,args'),ts3) |
|
323 |
end; |
|
324 |
||
325 |
||
326 |
(* Changed for typed equality *) |
|
327 |
(* First check if the predicate is an equality or not, then call different functions for equality and non-equalities *) |
|
328 |
fun predicate_of term = |
|
329 |
let val (pred,args) = strip_comb term |
|
330 |
in |
|
331 |
case pred of (Const ("op =", _)) => pred_of_eq (pred,args) |
|
332 |
| _ => pred_of_nonEq (pred,args) |
|
333 |
end; |
|
334 |
||
335 |
||
336 |
||
337 |
fun literals_of_term ((Const("Trueprop",_) $ P),lits_ts) = literals_of_term(P,lits_ts) |
|
338 |
| literals_of_term ((Const("op |",_) $ P $ Q),(lits,ts)) = |
|
339 |
let val (lits',ts') = literals_of_term(P,(lits,ts)) |
|
340 |
in |
|
341 |
literals_of_term(Q,(lits',ts')) |
|
342 |
end |
|
343 |
| literals_of_term ((Const("Not",_) $ P),(lits,ts)) = |
|
344 |
let val (pred,ts') = predicate_of P |
|
345 |
val lits' = Literal(false,pred,false) :: lits |
|
346 |
val ts'' = ResLib.no_rep_app ts ts' |
|
347 |
in |
|
348 |
(lits',ts'') |
|
349 |
end |
|
350 |
| literals_of_term (P,(lits,ts)) = |
|
351 |
let val (pred,ts') = predicate_of P |
|
352 |
val lits' = Literal(true,pred,false) :: lits |
|
353 |
val ts'' = ResLib.no_rep_app ts ts' |
|
354 |
in |
|
355 |
(lits',ts'') |
|
15956 | 356 |
end; |
15347 | 357 |
|
358 |
||
15956 | 359 |
fun literals_of_thm thm = literals_of_term (prop_of thm, ([],[])); |
15347 | 360 |
|
16199
ee95ab217fee
no longer emits literals for type class HOL.type; also minor tidying
paulson
parents:
16039
diff
changeset
|
361 |
(*Make literals for sorted type variables*) |
15347 | 362 |
fun sorts_on_typs (_, []) = [] |
16199
ee95ab217fee
no longer emits literals for type class HOL.type; also minor tidying
paulson
parents:
16039
diff
changeset
|
363 |
| sorts_on_typs (v, "HOL.type" :: s) = |
ee95ab217fee
no longer emits literals for type class HOL.type; also minor tidying
paulson
parents:
16039
diff
changeset
|
364 |
sorts_on_typs (v,s) (*Ignore sort "type"*) |
ee95ab217fee
no longer emits literals for type class HOL.type; also minor tidying
paulson
parents:
16039
diff
changeset
|
365 |
| sorts_on_typs ((FOLTVar(indx)), (s::ss)) = |
ee95ab217fee
no longer emits literals for type class HOL.type; also minor tidying
paulson
parents:
16039
diff
changeset
|
366 |
LTVar((make_type_class s) ^ |
ee95ab217fee
no longer emits literals for type class HOL.type; also minor tidying
paulson
parents:
16039
diff
changeset
|
367 |
"(" ^ (make_schematic_type_var(string_of_indexname indx)) ^ ")") :: |
ee95ab217fee
no longer emits literals for type class HOL.type; also minor tidying
paulson
parents:
16039
diff
changeset
|
368 |
(sorts_on_typs ((FOLTVar(indx)), ss)) |
ee95ab217fee
no longer emits literals for type class HOL.type; also minor tidying
paulson
parents:
16039
diff
changeset
|
369 |
| sorts_on_typs ((FOLTFree(x)), (s::ss)) = |
ee95ab217fee
no longer emits literals for type class HOL.type; also minor tidying
paulson
parents:
16039
diff
changeset
|
370 |
LTFree((make_type_class s) ^ "(" ^ (make_fixed_type_var(x)) ^ ")") :: |
ee95ab217fee
no longer emits literals for type class HOL.type; also minor tidying
paulson
parents:
16039
diff
changeset
|
371 |
(sorts_on_typs ((FOLTFree(x)), ss)); |
15347 | 372 |
|
16199
ee95ab217fee
no longer emits literals for type class HOL.type; also minor tidying
paulson
parents:
16039
diff
changeset
|
373 |
(*Given a list of sorted type variables, return two separate lists. |
ee95ab217fee
no longer emits literals for type class HOL.type; also minor tidying
paulson
parents:
16039
diff
changeset
|
374 |
The first is for TVars, the second for TFrees.*) |
15347 | 375 |
fun add_typs_aux [] = ([],[]) |
376 |
| add_typs_aux ((FOLTVar(indx),s)::tss) = |
|
16199
ee95ab217fee
no longer emits literals for type class HOL.type; also minor tidying
paulson
parents:
16039
diff
changeset
|
377 |
let val vs = sorts_on_typs (FOLTVar(indx), s) |
ee95ab217fee
no longer emits literals for type class HOL.type; also minor tidying
paulson
parents:
16039
diff
changeset
|
378 |
val (vss,fss) = add_typs_aux tss |
ee95ab217fee
no longer emits literals for type class HOL.type; also minor tidying
paulson
parents:
16039
diff
changeset
|
379 |
in |
ee95ab217fee
no longer emits literals for type class HOL.type; also minor tidying
paulson
parents:
16039
diff
changeset
|
380 |
(ResLib.no_rep_app vs vss, fss) |
ee95ab217fee
no longer emits literals for type class HOL.type; also minor tidying
paulson
parents:
16039
diff
changeset
|
381 |
end |
15347 | 382 |
| add_typs_aux ((FOLTFree(x),s)::tss) = |
16199
ee95ab217fee
no longer emits literals for type class HOL.type; also minor tidying
paulson
parents:
16039
diff
changeset
|
383 |
let val fs = sorts_on_typs (FOLTFree(x), s) |
ee95ab217fee
no longer emits literals for type class HOL.type; also minor tidying
paulson
parents:
16039
diff
changeset
|
384 |
val (vss,fss) = add_typs_aux tss |
ee95ab217fee
no longer emits literals for type class HOL.type; also minor tidying
paulson
parents:
16039
diff
changeset
|
385 |
in |
ee95ab217fee
no longer emits literals for type class HOL.type; also minor tidying
paulson
parents:
16039
diff
changeset
|
386 |
(vss, ResLib.no_rep_app fs fss) |
ee95ab217fee
no longer emits literals for type class HOL.type; also minor tidying
paulson
parents:
16039
diff
changeset
|
387 |
end; |
15347 | 388 |
|
16199
ee95ab217fee
no longer emits literals for type class HOL.type; also minor tidying
paulson
parents:
16039
diff
changeset
|
389 |
fun add_typs (Clause cls) = add_typs_aux (#types_sorts cls) |
15347 | 390 |
|
391 |
||
392 |
(** make axiom clauses, hypothesis clauses and conjecture clauses. **) |
|
393 |
||
394 |
local |
|
395 |
fun replace_dot "." = "_" |
|
396 |
| replace_dot c = c; |
|
397 |
||
398 |
in |
|
399 |
||
400 |
fun proper_ax_name ax_name = |
|
401 |
let val chars = explode ax_name |
|
402 |
in |
|
403 |
implode (map replace_dot chars) |
|
404 |
end; |
|
405 |
end; |
|
406 |
||
407 |
fun make_axiom_clause_thm thm (name,number)= |
|
408 |
let val (lits,types_sorts) = literals_of_thm thm |
|
409 |
val cls_id = number |
|
410 |
val (tvar_lits,tfree_lits) = add_typs_aux types_sorts |
|
411 |
val ax_name = proper_ax_name name |
|
412 |
in |
|
413 |
make_clause(cls_id,ax_name,Axiom,lits,types_sorts,tvar_lits,tfree_lits) |
|
414 |
end; |
|
415 |
||
416 |
fun make_hypothesis_clause_thm thm = |
|
417 |
let val (lits,types_sorts) = literals_of_thm thm |
|
418 |
val cls_id = generate_id() |
|
419 |
val (tvar_lits,tfree_lits) = add_typs_aux types_sorts |
|
420 |
in |
|
421 |
make_clause(cls_id,"",Hypothesis,lits,types_sorts,tvar_lits,tfree_lits) |
|
422 |
end; |
|
423 |
||
424 |
||
425 |
fun make_conjecture_clause_thm thm = |
|
426 |
let val (lits,types_sorts) = literals_of_thm thm |
|
427 |
val cls_id = generate_id() |
|
428 |
val (tvar_lits,tfree_lits) = add_typs_aux types_sorts |
|
429 |
in |
|
430 |
make_clause(cls_id,"",Conjecture,lits,types_sorts,tvar_lits,tfree_lits) |
|
431 |
end; |
|
432 |
||
433 |
||
434 |
fun make_axiom_clause term (name,number)= |
|
435 |
let val (lits,types_sorts) = literals_of_term (term,([],[])) |
|
436 |
val cls_id = number |
|
437 |
val (tvar_lits,tfree_lits) = add_typs_aux types_sorts |
|
438 |
val ax_name = proper_ax_name name |
|
439 |
in |
|
440 |
make_clause(cls_id,ax_name,Axiom,lits,types_sorts,tvar_lits,tfree_lits) |
|
441 |
end; |
|
442 |
||
443 |
||
444 |
fun make_hypothesis_clause term = |
|
445 |
let val (lits,types_sorts) = literals_of_term (term,([],[])) |
|
446 |
val cls_id = generate_id() |
|
447 |
val (tvar_lits,tfree_lits) = add_typs_aux types_sorts |
|
448 |
in |
|
449 |
make_clause(cls_id,"",Hypothesis,lits,types_sorts,tvar_lits,tfree_lits) |
|
450 |
end; |
|
451 |
||
452 |
||
453 |
fun make_conjecture_clause term = |
|
454 |
let val (lits,types_sorts) = literals_of_term (term,([],[])) |
|
455 |
val cls_id = generate_id() |
|
456 |
val (tvar_lits,tfree_lits) = add_typs_aux types_sorts |
|
457 |
in |
|
458 |
make_clause(cls_id,"",Conjecture,lits,types_sorts,tvar_lits,tfree_lits) |
|
459 |
end; |
|
460 |
||
461 |
||
462 |
||
463 |
(**** Isabelle arities ****) |
|
464 |
||
465 |
exception ARCLAUSE of string; |
|
466 |
||
467 |
||
468 |
type class = string; |
|
469 |
type tcons = string; |
|
470 |
||
471 |
||
472 |
datatype arLit = TConsLit of bool * (class * tcons * string list) | TVarLit of bool * (class * string); |
|
473 |
||
474 |
datatype arityClause = |
|
475 |
ArityClause of {clause_id: clause_id, |
|
476 |
kind: kind, |
|
477 |
conclLit: arLit, |
|
478 |
premLits: arLit list}; |
|
479 |
||
480 |
||
481 |
fun get_TVars 0 = [] |
|
482 |
| get_TVars n = ("T_" ^ (string_of_int n)) :: get_TVars (n-1); |
|
483 |
||
484 |
||
485 |
||
486 |
fun pack_sort(_,[]) = raise ARCLAUSE("Empty Sort Found") |
|
487 |
| pack_sort(tvar, [cls]) = [(make_type_class cls, tvar)] |
|
488 |
| pack_sort(tvar, cls::srt) = (make_type_class cls,tvar) :: (pack_sort(tvar, srt)); |
|
489 |
||
490 |
||
491 |
fun make_TVarLit (b,(cls,str)) = TVarLit(b,(cls,str)); |
|
492 |
fun make_TConsLit (b,(cls,tcons,tvars)) = TConsLit(b,(make_type_class cls,make_fixed_type_const tcons,tvars)); |
|
493 |
||
494 |
||
495 |
fun make_arity_clause (clause_id,kind,conclLit,premLits) = |
|
496 |
ArityClause {clause_id = clause_id, kind = kind, conclLit = conclLit, premLits = premLits}; |
|
497 |
||
498 |
||
499 |
fun make_axiom_arity_clause (tcons,(res,args)) = |
|
500 |
let val cls_id = generate_id() |
|
501 |
val nargs = length args |
|
502 |
val tvars = get_TVars nargs |
|
503 |
val conclLit = make_TConsLit(true,(res,tcons,tvars)) |
|
15774 | 504 |
val tvars_srts = ListPair.zip (tvars,args) |
15347 | 505 |
val tvars_srts' = ResLib.flat_noDup(map pack_sort tvars_srts) |
506 |
val false_tvars_srts' = ResLib.pair_ins false tvars_srts' |
|
507 |
val premLits = map make_TVarLit false_tvars_srts' |
|
508 |
in |
|
509 |
make_arity_clause (cls_id,Axiom,conclLit,premLits) |
|
510 |
end; |
|
511 |
||
512 |
||
513 |
||
514 |
(**** Isabelle class relations ****) |
|
515 |
||
516 |
||
517 |
datatype classrelClause = |
|
518 |
ClassrelClause of {clause_id: clause_id, |
|
519 |
subclass: class, |
|
15531 | 520 |
superclass: class option}; |
15347 | 521 |
|
522 |
fun make_classrelClause (clause_id,subclass,superclass) = |
|
523 |
ClassrelClause {clause_id = clause_id,subclass = subclass, superclass = superclass}; |
|
524 |
||
525 |
||
526 |
fun make_axiom_classrelClause (subclass,superclass) = |
|
527 |
let val cls_id = generate_id() |
|
528 |
val sub = make_type_class subclass |
|
15531 | 529 |
val sup = case superclass of NONE => NONE |
530 |
| SOME s => SOME (make_type_class s) |
|
15347 | 531 |
in |
532 |
make_classrelClause(cls_id,sub,sup) |
|
533 |
end; |
|
534 |
||
535 |
||
536 |
||
537 |
fun classrelClauses_of_aux (sub,[]) = [] |
|
15531 | 538 |
| classrelClauses_of_aux (sub,(sup::sups)) = make_axiom_classrelClause(sub,SOME sup) :: (classrelClauses_of_aux (sub,sups)); |
15347 | 539 |
|
540 |
||
541 |
fun classrelClauses_of (sub,sups) = |
|
15531 | 542 |
case sups of [] => [make_axiom_classrelClause (sub,NONE)] |
15347 | 543 |
| _ => classrelClauses_of_aux (sub, sups); |
544 |
||
545 |
||
546 |
||
547 |
(***** convert clauses to tptp format *****) |
|
548 |
||
549 |
||
550 |
fun string_of_clauseID (Clause cls) = clause_prefix ^ (string_of_int (#clause_id cls)); |
|
551 |
||
552 |
||
553 |
fun string_of_kind (Clause cls) = name_of_kind (#kind cls); |
|
554 |
||
555 |
fun string_of_axiomName (Clause cls) = #axiom_name cls; |
|
556 |
||
557 |
(****!!!! Changed for typed equality !!!!****) |
|
558 |
fun wrap_eq_type typ t = eq_typ_wrapper ^"(" ^ t ^ "," ^ typ ^ ")"; |
|
559 |
||
560 |
||
561 |
(****!!!! Changed for typed equality !!!!****) |
|
562 |
(* Only need to wrap equality's arguments with "typeinfo" if the output clauses are typed && if we specifically ask for types to be included. *) |
|
563 |
fun string_of_equality (typ,terms) = |
|
564 |
let val [tstr1,tstr2] = map string_of_term terms |
|
565 |
in |
|
566 |
if ((!keep_types) andalso (!special_equal)) then |
|
567 |
"equal(" ^ (wrap_eq_type typ tstr1) ^ "," ^ (wrap_eq_type typ tstr2) ^ ")" |
|
568 |
else |
|
569 |
"equal(" ^ tstr1 ^ "," ^ tstr2 ^ ")" |
|
15615 | 570 |
end |
571 |
||
572 |
||
573 |
and |
|
574 |
string_of_term (UVar(x,_)) = x |
|
575 |
| string_of_term (Fun("equal",typ,terms)) = string_of_equality(typ,terms) |
|
576 |
| string_of_term (Fun (name,typ,[])) = name |
|
577 |
| string_of_term (Fun (name,typ,terms)) = |
|
578 |
let val terms' = map string_of_term terms |
|
579 |
in |
|
580 |
if (!keep_types) then name ^ (ResLib.list_to_string (typ :: terms')) |
|
581 |
else name ^ (ResLib.list_to_string terms') |
|
15347 | 582 |
end; |
583 |
||
584 |
||
585 |
||
586 |
(* Changed for typed equality *) |
|
587 |
(* before output the string of the predicate, check if the predicate corresponds to an equality or not. *) |
|
588 |
fun string_of_predicate (Predicate("equal",typ,terms)) = string_of_equality(typ,terms) |
|
589 |
| string_of_predicate (Predicate(name,_,[])) = name |
|
590 |
| string_of_predicate (Predicate(name,typ,terms)) = |
|
591 |
let val terms_as_strings = map string_of_term terms |
|
592 |
in |
|
593 |
if (!keep_types) then name ^ (ResLib.list_to_string (typ :: terms_as_strings)) |
|
594 |
else name ^ (ResLib.list_to_string terms_as_strings) |
|
595 |
end; |
|
596 |
||
597 |
||
598 |
||
599 |
||
600 |
fun tptp_literal (Literal(pol,pred,tag)) = |
|
601 |
let val pred_string = string_of_predicate pred |
|
602 |
val tagged_pol = if (tag andalso !tagged) then (if pol then "+++" else "---") |
|
603 |
else (if pol then "++" else "--") |
|
604 |
in |
|
605 |
tagged_pol ^ pred_string |
|
606 |
end; |
|
607 |
||
608 |
||
609 |
||
610 |
fun tptp_of_typeLit (LTVar x) = "--" ^ x |
|
611 |
| tptp_of_typeLit (LTFree x) = "++" ^ x; |
|
612 |
||
613 |
||
614 |
fun gen_tptp_cls (cls_id,ax_name,knd,lits) = |
|
615 |
let val ax_str = (if ax_name = "" then "" else ("_" ^ ax_name)) |
|
616 |
in |
|
617 |
"input_clause(" ^ cls_id ^ ax_str ^ "," ^ knd ^ "," ^ lits ^ ")." |
|
618 |
end; |
|
619 |
||
620 |
||
621 |
fun gen_tptp_type_cls (cls_id,knd,tfree_lit,idx) = "input_clause(" ^ cls_id ^ "_tcs" ^ (string_of_int idx) ^ "," ^ knd ^ ",[" ^ tfree_lit ^ "])."; |
|
622 |
||
623 |
||
624 |
fun tptp_clause_aux (Clause cls) = |
|
625 |
let val lits = map tptp_literal (#literals cls) |
|
626 |
val tvar_lits_strs = if (!keep_types) then (map tptp_of_typeLit (#tvar_type_literals cls)) else [] |
|
627 |
val tfree_lits = if (!keep_types) then (map tptp_of_typeLit (#tfree_type_literals cls)) else [] |
|
628 |
in |
|
629 |
(tvar_lits_strs @ lits,tfree_lits) |
|
630 |
end; |
|
631 |
||
15608 | 632 |
|
15347 | 633 |
fun tptp_clause cls = |
634 |
let val (lits,tfree_lits) = tptp_clause_aux cls (*"lits" includes the typing assumptions (TVars)*) |
|
635 |
val cls_id = string_of_clauseID cls |
|
636 |
val ax_name = string_of_axiomName cls |
|
637 |
val knd = string_of_kind cls |
|
638 |
val lits_str = ResLib.list_to_string' lits |
|
639 |
val cls_str = gen_tptp_cls(cls_id,ax_name,knd,lits_str) fun typ_clss k [] = [] |
|
640 |
| typ_clss k (tfree :: tfrees) = |
|
641 |
(gen_tptp_type_cls(cls_id,knd,tfree,k)) :: (typ_clss (k+1) tfrees) |
|
642 |
in |
|
643 |
cls_str :: (typ_clss 0 tfree_lits) |
|
644 |
end; |
|
645 |
||
16039
dfe264950511
Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents:
15956
diff
changeset
|
646 |
fun clause_info cls = |
dfe264950511
Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents:
15956
diff
changeset
|
647 |
let |
dfe264950511
Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents:
15956
diff
changeset
|
648 |
val cls_id = string_of_clauseID cls |
dfe264950511
Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents:
15956
diff
changeset
|
649 |
val ax_name = string_of_axiomName cls |
dfe264950511
Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents:
15956
diff
changeset
|
650 |
in |
dfe264950511
Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents:
15956
diff
changeset
|
651 |
((ax_name^""), cls_id) |
dfe264950511
Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents:
15956
diff
changeset
|
652 |
end; |
dfe264950511
Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents:
15956
diff
changeset
|
653 |
|
15347 | 654 |
|
15608 | 655 |
fun clause2tptp cls = |
656 |
let val (lits,tfree_lits) = tptp_clause_aux cls (*"lits" includes the typing assumptions (TVars)*) |
|
657 |
val cls_id = string_of_clauseID cls |
|
658 |
val ax_name = string_of_axiomName cls |
|
659 |
val knd = string_of_kind cls |
|
660 |
val lits_str = ResLib.list_to_string' lits |
|
661 |
val cls_str = gen_tptp_cls(cls_id,ax_name,knd,lits_str) |
|
662 |
in |
|
663 |
(cls_str,tfree_lits) |
|
664 |
end; |
|
665 |
||
666 |
||
667 |
fun tfree_clause tfree_lit = "input_clause(" ^ "tfree_tcs," ^ "conjecture" ^ ",[" ^ tfree_lit ^ "])."; |
|
668 |
||
15347 | 669 |
val delim = "\n"; |
670 |
val tptp_clauses2str = ResLib.list2str_sep delim; |
|
671 |
||
672 |
||
673 |
fun string_of_arClauseID (ArityClause arcls) = arclause_prefix ^ string_of_int(#clause_id arcls); |
|
674 |
||
675 |
||
676 |
fun string_of_arLit (TConsLit(b,(c,t,args))) = |
|
677 |
let val pol = if b then "++" else "--" |
|
678 |
val arg_strs = (case args of [] => "" | _ => ResLib.list_to_string args) |
|
679 |
in |
|
680 |
pol ^ c ^ "(" ^ t ^ arg_strs ^ ")" |
|
681 |
end |
|
682 |
| string_of_arLit (TVarLit(b,(c,str))) = |
|
683 |
let val pol = if b then "++" else "--" |
|
684 |
in |
|
685 |
pol ^ c ^ "(" ^ str ^ ")" |
|
686 |
end; |
|
687 |
||
688 |
||
689 |
fun string_of_conclLit (ArityClause arcls) = string_of_arLit (#conclLit arcls); |
|
690 |
||
691 |
||
692 |
fun strings_of_premLits (ArityClause arcls) = map string_of_arLit (#premLits arcls); |
|
693 |
||
694 |
||
695 |
fun string_of_arKind (ArityClause arcls) = name_of_kind(#kind arcls); |
|
696 |
||
697 |
fun tptp_arity_clause arcls = |
|
698 |
let val arcls_id = string_of_arClauseID arcls |
|
699 |
val concl_lit = string_of_conclLit arcls |
|
700 |
val prems_lits = strings_of_premLits arcls |
|
701 |
val knd = string_of_arKind arcls |
|
702 |
val all_lits = concl_lit :: prems_lits |
|
703 |
in |
|
15452 | 704 |
"input_clause(" ^ arcls_id ^ "," ^ knd ^ "," ^ (ResLib.list_to_string' all_lits) ^ ")." |
15347 | 705 |
|
706 |
end; |
|
707 |
||
708 |
||
709 |
val clrelclause_prefix = "relcls_"; |
|
710 |
||
711 |
||
712 |
fun tptp_classrelLits sub sup = |
|
713 |
let val tvar = "(T)" |
|
714 |
in |
|
15531 | 715 |
case sup of NONE => "[++" ^ sub ^ tvar ^ "]" |
716 |
| (SOME supcls) => "[--" ^ sub ^ tvar ^ ",++" ^ supcls ^ tvar ^ "]" |
|
15347 | 717 |
end; |
718 |
||
719 |
||
720 |
fun tptp_classrelClause (ClassrelClause cls) = |
|
721 |
let val relcls_id = clrelclause_prefix ^ string_of_int(#clause_id cls) |
|
722 |
val sub = #subclass cls |
|
723 |
val sup = #superclass cls |
|
724 |
val lits = tptp_classrelLits sub sup |
|
725 |
in |
|
726 |
"input_clause(" ^ relcls_id ^ ",axiom," ^ lits ^ ")." |
|
727 |
end; |
|
728 |
||
729 |
end; |