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