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