108 |
120 |
109 val ascii_of = String.translate ascii_of_c; |
121 val ascii_of = String.translate ascii_of_c; |
110 |
122 |
111 end; |
123 end; |
112 |
124 |
|
125 |
113 (*Remove the initial ' character from a type variable, if it is present*) |
126 (*Remove the initial ' character from a type variable, if it is present*) |
114 fun trim_type_var s = |
127 fun trim_type_var s = |
115 if s <> "" andalso String.sub(s,0) = #"'" then String.extract(s,1,NONE) |
128 if s <> "" andalso String.sub(s,0) = #"'" then String.extract(s,1,NONE) |
116 else error ("trim_type: Malformed type variable encountered: " ^ s); |
129 else error ("trim_type: Malformed type variable encountered: " ^ s); |
117 |
130 |
118 fun ascii_of_indexname (v,0) = ascii_of v |
131 fun ascii_of_indexname (v,0) = ascii_of v |
119 | ascii_of_indexname (v,i) = ascii_of v ^ "_" ^ string_of_int i; |
132 | ascii_of_indexname (v,i) = ascii_of v ^ "_" ^ string_of_int i; |
120 |
133 |
121 fun make_schematic_var v = schematic_var_prefix ^ (ascii_of_indexname v); |
134 (* another version of above functions that remove chars that may not be allowed by Vampire *) |
|
135 fun make_schematic_var v = schematic_var_prefix ^ (ascii_of v); |
122 fun make_fixed_var x = fixed_var_prefix ^ (ascii_of x); |
136 fun make_fixed_var x = fixed_var_prefix ^ (ascii_of x); |
|
137 |
123 |
138 |
124 (*Type variables contain _H because the character ' translates to that.*) |
139 (*Type variables contain _H because the character ' translates to that.*) |
125 fun make_schematic_type_var (x,i) = |
140 fun make_schematic_type_var (x,i) = |
126 tvar_prefix ^ (ascii_of_indexname (trim_type_var x,i)); |
141 tvar_prefix ^ (ascii_of_indexname (trim_type_var x,i)); |
127 fun make_fixed_type_var x = tfree_prefix ^ (ascii_of (trim_type_var x)); |
142 fun make_fixed_type_var x = tfree_prefix ^ (ascii_of (trim_type_var x)); |
128 |
143 |
129 fun make_fixed_const c = |
144 fun make_fixed_const c = const_prefix ^ (ascii_of c); |
|
145 fun make_fixed_type_const c = tconst_prefix ^ (ascii_of c); |
|
146 |
|
147 fun make_type_class clas = class_prefix ^ (ascii_of clas); |
|
148 |
|
149 |
|
150 |
|
151 fun lookup_const c = |
130 case Symtab.lookup (const_trans_table,c) of |
152 case Symtab.lookup (const_trans_table,c) of |
131 SOME c' => c' |
153 SOME c' => c' |
132 | NONE => const_prefix ^ (ascii_of c); |
154 | NONE => make_fixed_const 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); |
|
138 |
|
139 fun make_type_class clas = class_prefix ^ (ascii_of clas); |
|
140 |
155 |
141 |
156 |
142 |
157 |
143 (***** definitions and functions for FOL clauses, prepared for conversion into TPTP format or SPASS format. *****) |
158 (***** definitions and functions for FOL clauses, prepared for conversion into TPTP format or SPASS format. *****) |
144 |
159 |
202 axiom_name: axiom_name, |
222 axiom_name: axiom_name, |
203 kind: kind, |
223 kind: kind, |
204 literals: literal list, |
224 literals: literal list, |
205 types_sorts: (typ_var * sort) list, |
225 types_sorts: (typ_var * sort) list, |
206 tvar_type_literals: type_literal list, |
226 tvar_type_literals: type_literal list, |
207 tfree_type_literals: type_literal list }; |
227 tfree_type_literals: type_literal list , |
|
228 tvars: string list, |
|
229 predicates: (string*int) list, |
|
230 functions: (string*int) list}; |
|
231 |
208 |
232 |
209 |
233 |
210 exception CLAUSE of string; |
234 exception CLAUSE of string; |
211 |
235 |
212 |
236 |
213 |
237 |
214 (*** make clauses ***) |
238 (*** make clauses ***) |
215 |
239 |
216 |
240 |
217 fun make_clause (clause_id,axiom_name,kind,literals, |
241 fun make_clause (clause_id,axiom_name,kind,literals,types_sorts,tvar_type_literals,tfree_type_literals,tvars, predicates, functions) = |
218 types_sorts,tvar_type_literals, |
242 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,tvars = tvars, predicates = predicates, functions = functions}; |
219 tfree_type_literals) = |
243 |
220 Clause {clause_id = clause_id, axiom_name = axiom_name, kind = kind, |
244 |
221 literals = literals, types_sorts = types_sorts, |
245 |
222 tvar_type_literals = tvar_type_literals, |
246 fun type_of (Type (a, [])) = let val t = make_fixed_type_const a |
223 tfree_type_literals = tfree_type_literals}; |
247 in |
224 |
248 (t,([],[(t,0)])) |
|
249 end |
225 |
250 |
226 (*Definitions of the current theory--to allow suppressing types.*) |
251 (*Definitions of the current theory--to allow suppressing types.*) |
227 val curr_defs = ref Defs.empty; |
252 val curr_defs = ref Defs.empty; |
228 |
253 |
229 (*Initialize the type suppression mechanism with the current theory before |
254 (*Initialize the type suppression mechanism with the current theory before |
230 producing any clauses!*) |
255 producing any clauses!*) |
231 fun init thy = (curr_defs := Theory.defs_of thy); |
256 fun init thy = (curr_defs := Theory.defs_of thy); |
|
257 (*<<<<<<< res_clause.ML |
|
258 *) |
|
259 |
|
260 (*Types aren't needed if the constant has at most one definition and is monomorphic*) |
|
261 (*fun no_types_needed s = |
|
262 (case Defs.fast_overloading_info (!curr_defs) s of |
|
263 NONE => true |
|
264 | SOME (T,len,_) => len <= 1 andalso null (typ_tvars T)) |
|
265 =======*) |
232 fun no_types_needed s = Defs.monomorphic (!curr_defs) s; |
266 fun no_types_needed s = Defs.monomorphic (!curr_defs) s; |
|
267 (*>>>>>>> 1.18*) |
233 |
268 |
|
269 |
234 (*Flatten a type to a string while accumulating sort constraints on the TFress and |
270 (*Flatten a type to a string while accumulating sort constraints on the TFress and |
235 TVars it contains.*) |
271 TVars it contains.*) |
236 fun type_of (Type (a, [])) = (make_fixed_type_const a,[]) |
272 fun type_of (Type (a, [])) = let val t = make_fixed_type_const a |
|
273 in |
|
274 (t,([],[(t,0)])) |
|
275 end |
237 | type_of (Type (a, Ts)) = |
276 | type_of (Type (a, Ts)) = |
238 let val foltyps_ts = map type_of Ts |
277 let val foltyps_ts = map type_of Ts |
239 val (folTyps,ts) = ListPair.unzip foltyps_ts |
278 val (folTyps,ts_funcs) = ListPair.unzip foltyps_ts |
240 val ts' = ResLib.flat_noDup ts |
279 val (ts, funcslist) = ListPair.unzip ts_funcs |
241 in |
280 val ts' = ResLib.flat_noDup ts |
242 (((make_fixed_type_const a) ^ (ResLib.list_to_string folTyps)), ts') |
281 val funcs' = (ResLib.flat_noDup funcslist) |
243 end |
282 val t = (make_fixed_type_const a) |
244 | type_of (TFree (a, s)) = (make_fixed_type_var a, [((FOLTFree a),s)]) |
283 in |
245 | type_of (TVar (v, s)) = (make_schematic_type_var v, [((FOLTVar v),s)]); |
284 ((t ^ (ResLib.list_to_string folTyps)),(ts', ((t,(length Ts))::funcs')) ) |
|
285 end |
|
286 | type_of (TFree (a, s)) = let val t = make_fixed_type_const a |
|
287 in |
|
288 (t, ([((FOLTFree a),s)],[(t,0)]) ) |
|
289 end |
|
290 |
|
291 | type_of (TVar (v, s)) = let val t =make_schematic_type_var ( v) |
|
292 in |
|
293 (t, ([((FOLTVar v),s)], [(*(t,0)*)])) |
|
294 end |
|
295 |
|
296 (* added: checkMeta: string -> bool *) |
|
297 (* Any meta vars like ?x should be treated as universal vars,although it is represented as "Free(...)" by Isabelle *) |
|
298 fun checkMeta s = |
|
299 let val chars = explode s |
|
300 in |
|
301 ["M", "E", "T", "A", "H", "Y", "P", "1"] prefix chars |
|
302 end; |
246 |
303 |
247 fun maybe_type_of c T = |
304 fun maybe_type_of c T = |
248 if no_types_needed c then ("",[]) else type_of T; |
305 if no_types_needed c then ("",([],[])) else type_of T; |
249 |
306 |
250 (* Any variables created via the METAHYPS tactical should be treated as |
307 (* Any variables created via the METAHYPS tactical should be treated as |
251 universal vars, although it is represented as "Free(...)" by Isabelle *) |
308 universal vars, although it is represented as "Free(...)" by Isabelle *) |
252 val isMeta = String.isPrefix "METAHYP1_" |
309 val isMeta = String.isPrefix "METAHYP1_" |
253 |
310 |
254 fun pred_name_type (Const(c,T)) = (make_fixed_const c, maybe_type_of c T) |
311 fun pred_name_type (Const(c,T)) = (let val t = make_fixed_const c |
|
312 val (typof,(folTyps,funcs)) = type_of T |
|
313 |
|
314 in |
|
315 (t, (typof,folTyps), (funcs)) |
|
316 end) |
255 | pred_name_type (Free(x,T)) = |
317 | pred_name_type (Free(x,T)) = |
256 if isMeta x then raise CLAUSE("Predicate Not First Order") |
318 let val is_meta = checkMeta x |
257 else (make_fixed_var x, type_of T) |
319 in |
|
320 if is_meta then (raise CLAUSE("Predicate Not First Order")) else |
|
321 (let val t = (make_fixed_var x) |
|
322 val (typof,(folTyps, funcs)) = type_of T |
|
323 in |
|
324 (t, (typof,folTyps),funcs) |
|
325 end) |
|
326 |
|
327 end |
258 | pred_name_type (Var(_,_)) = raise CLAUSE("Predicate Not First Order") |
328 | pred_name_type (Var(_,_)) = raise CLAUSE("Predicate Not First Order") |
259 | pred_name_type _ = raise CLAUSE("Predicate input unexpected"); |
329 | pred_name_type _ = raise CLAUSE("Predicate input unexpected"); |
260 |
330 |
261 |
331 |
262 (* For type equality *) |
332 (* For type equality *) |
265 fun eq_arg_type (Type("fun",[T,_])) = |
335 fun eq_arg_type (Type("fun",[T,_])) = |
266 let val (folT,_) = type_of T; |
336 let val (folT,_) = type_of T; |
267 in |
337 in |
268 folT |
338 folT |
269 end; |
339 end; |
270 |
340 |
271 fun fun_name_type (Const(c,T)) = (make_fixed_const c, maybe_type_of c T) |
341 |
272 | fun_name_type (Free(x,T)) = (make_fixed_var x,type_of T) |
342 |
273 | fun_name_type _ = raise CLAUSE("Function Not First Order"); |
343 (* FIX: retest with lcp's changes *) |
274 |
344 fun fun_name_type (Const(c,T)) args = (let val t = make_fixed_const c |
275 |
345 val (typof,(folTyps,funcs)) = maybe_type_of c T |
276 (* FIX - add in funcs and stuff to this *) |
346 val arity = if (!keep_types) then |
|
347 (length args)(*+ 1*) (*(length folTyps) *) |
|
348 else |
|
349 (length args)(* -1*) |
|
350 in |
|
351 (t, (typof,folTyps), ((t,arity)::funcs)) |
|
352 end) |
|
353 |
|
354 | fun_name_type (Free(x,T)) args = (let val t = (make_fixed_var x) |
|
355 val (typof,(folTyps,funcs)) = type_of T |
|
356 val arity = if (!keep_types) then |
|
357 (length args) (*+ 1*) (*(length folTyps)*) |
|
358 else |
|
359 (length args) (*-1*)(*(length args) + 1*)(*(length folTyps)*) |
|
360 in |
|
361 (t, (typof,folTyps), ((t,0)::funcs)) |
|
362 end) |
|
363 |
|
364 | fun_name_type _ args = raise CLAUSE("Function Not First Order"); |
|
365 |
277 |
366 |
278 fun term_of (Var(ind_nm,T)) = |
367 fun term_of (Var(ind_nm,T)) = |
279 let val (folType,ts) = type_of T |
368 let val (folType,(ts,funcs)) = type_of T |
280 in |
369 in |
281 (UVar(make_schematic_var ind_nm, folType), ts) |
370 (UVar(make_schematic_var(string_of_indexname ind_nm),folType),(ts, (funcs))) |
282 end |
371 end |
283 | term_of (Free(x,T)) = |
372 | term_of (Free(x,T)) = |
284 let val (folType,ts) = type_of T |
373 let val is_meta = checkMeta x |
285 in |
374 val (folType,(ts, funcs)) = type_of T |
286 if isMeta x then (UVar(make_schematic_var(x,0), folType), ts) |
375 in |
287 else (Fun(make_fixed_var x,folType,[]), ts) |
376 if is_meta then (UVar(make_schematic_var x,folType),(ts, (((make_schematic_var x),0)::funcs))) |
288 end |
377 else |
289 | term_of (Const(c,T)) = (* impossible to be equality *) |
378 (Fun(make_fixed_var x,folType,[]),(ts, (((make_fixed_var x),0)::funcs))) |
290 let val (folType,ts) = type_of T |
379 end |
291 in |
380 | term_of (Const(c,T)) = (* impossible to be equality *) |
292 (Fun(make_fixed_const c,folType,[]), ts) |
381 let val (folType,(ts,funcs)) = type_of T |
293 end |
382 in |
294 | term_of (app as (t $ a)) = |
383 (Fun(lookup_const c,folType,[]),(ts, (((lookup_const c),0)::funcs))) |
295 let val (f,args) = strip_comb app |
384 end |
296 fun term_of_aux () = |
385 | term_of (app as (t $ a)) = |
297 let val (funName,(funType,ts1)) = fun_name_type f |
386 let val (f,args) = strip_comb app |
298 val (args',ts2) = ListPair.unzip (map term_of args) |
387 fun term_of_aux () = |
299 val ts3 = ResLib.flat_noDup (ts1::ts2) |
388 let val (funName,(funType,ts1),funcs) = fun_name_type f args |
300 in |
389 val (args',ts_funcs) = ListPair.unzip (map term_of args) |
301 (Fun(funName,funType,args'),ts3) |
390 val (ts2,funcs') = ListPair.unzip ( ts_funcs) |
302 end |
391 val ts3 = ResLib.flat_noDup (ts1::ts2) |
303 fun term_of_eq ((Const ("op =", typ)),args) = |
392 val funcs'' = ResLib.flat_noDup((funcs::funcs')) |
304 let val arg_typ = eq_arg_type typ |
393 in |
305 val (args',ts) = ListPair.unzip (map term_of args) |
394 (Fun(funName,funType,args'),(ts3,funcs'')) |
306 val equal_name = make_fixed_const ("op =") |
395 end |
307 in |
396 fun term_of_eq ((Const ("op =", typ)),args) = |
308 (Fun(equal_name,arg_typ,args'),ResLib.flat_noDup ts) |
397 let val arg_typ = eq_arg_type typ |
309 end |
398 val (args',ts_funcs) = ListPair.unzip (map term_of args) |
310 in |
399 val (ts,funcs) = ListPair.unzip ( ts_funcs) |
311 case f of Const ("op =", typ) => term_of_eq (f,args) |
400 val equal_name = lookup_const ("op =") |
312 | Const(_,_) => term_of_aux () |
401 in |
313 | Free(s,_) => if isMeta s |
402 (Fun(equal_name,arg_typ,args'),(ResLib.flat_noDup ts, (((make_fixed_var equal_name),2):: ResLib.flat_noDup (funcs)))) |
314 then raise CLAUSE("Function Not First Order") |
403 end |
315 else term_of_aux() |
404 in |
316 | _ => raise CLAUSE("Function Not First Order") |
405 case f of Const ("op =", typ) => term_of_eq (f,args) |
317 end |
406 | Const(_,_) => term_of_aux () |
|
407 | Free(s,_) => if (checkMeta s) then (raise CLAUSE("Function Not First Order")) else term_of_aux () |
|
408 | _ => raise CLAUSE("Function Not First Order") |
|
409 end |
318 | term_of _ = raise CLAUSE("Function Not First Order"); |
410 | term_of _ = raise CLAUSE("Function Not First Order"); |
|
411 |
|
412 |
319 |
413 |
320 |
414 |
321 fun pred_of_eq ((Const ("op =", typ)),args) = |
415 fun pred_of_eq ((Const ("op =", typ)),args) = |
322 let val arg_typ = eq_arg_type typ |
416 let val arg_typ = eq_arg_type typ |
323 val (args',ts) = ListPair.unzip (map term_of args) |
417 val (args',ts_funcs) = ListPair.unzip (map term_of args) |
324 val equal_name = make_fixed_const "op =" |
418 val (ts,funcs) = ListPair.unzip ( ts_funcs) |
325 in |
419 val equal_name = lookup_const "op =" |
326 (Predicate(equal_name,arg_typ,args'),ResLib.flat_noDup ts) |
420 in |
327 end; |
421 (Predicate(equal_name,arg_typ,args'),ResLib.flat_noDup ts,([((make_fixed_var equal_name),2)]:(string*int)list), (ResLib.flat_noDup (funcs))) |
328 |
422 end; |
329 |
423 |
|
424 (* CHECK arity for predicate is set to (2*args) to account for type info. Is this right? *) |
330 (* changed for non-equality predicate *) |
425 (* changed for non-equality predicate *) |
331 (* The input "pred" cannot be an equality *) |
426 (* The input "pred" cannot be an equality *) |
332 fun pred_of_nonEq (pred,args) = |
427 fun pred_of_nonEq (pred,args) = |
333 let val (predName,(predType,ts1)) = pred_name_type pred |
428 let val (predName,(predType,ts1), pfuncs) = pred_name_type pred |
334 val (args',ts2) = ListPair.unzip (map term_of args) |
429 val (args',ts_funcs) = ListPair.unzip (map term_of args) |
|
430 val (ts2,ffuncs) = ListPair.unzip ( ts_funcs) |
335 val ts3 = ResLib.flat_noDup (ts1::ts2) |
431 val ts3 = ResLib.flat_noDup (ts1::ts2) |
336 in |
432 val ffuncs' = (ResLib.flat_noDup (ffuncs)) |
337 (Predicate(predName,predType,args'),ts3) |
433 val newfuncs = distinct (pfuncs@ffuncs') |
|
434 val pred_arity = (*if ((length ts3) <> 0) |
|
435 then |
|
436 ((length args) +(length ts3)) |
|
437 else*) |
|
438 (* just doing length args if untyped seems to work*) |
|
439 (if !keep_types then (length args)+1 else (length args)) |
|
440 in |
|
441 (Predicate(predName,predType,args'),ts3, [(predName, pred_arity)], newfuncs) |
338 end; |
442 end; |
339 |
443 |
340 |
444 |
341 (* Changed for typed equality *) |
445 (* Changed for typed equality *) |
342 (* First check if the predicate is an equality or not, then call different functions for equality and non-equalities *) |
446 (* First check if the predicate is an equality or not, then call different functions for equality and non-equalities *) |
346 case pred of (Const ("op =", _)) => pred_of_eq (pred,args) |
450 case pred of (Const ("op =", _)) => pred_of_eq (pred,args) |
347 | _ => pred_of_nonEq (pred,args) |
451 | _ => pred_of_nonEq (pred,args) |
348 end; |
452 end; |
349 |
453 |
350 |
454 |
351 fun literals_of_term ((Const("Trueprop",_) $ P),lits_ts) = literals_of_term (P,lits_ts) |
455 |
352 | literals_of_term ((Const("op |",_) $ P $ Q),(lits,ts)) = |
456 fun literals_of_term ((Const("Trueprop",_) $ P),lits_ts, preds, funcs) = literals_of_term(P,lits_ts, preds, funcs) |
353 let val (lits',ts') = literals_of_term (P,(lits,ts)) |
457 | literals_of_term ((Const("op |",_) $ P $ Q),(lits,ts), preds,funcs) = |
354 in |
458 let val (lits',ts', preds', funcs') = literals_of_term(P,(lits,ts), preds,funcs) |
355 literals_of_term (Q, (lits',ts')) |
459 in |
356 end |
460 literals_of_term(Q,(lits',ts'), distinct(preds'@preds), distinct(funcs'@funcs)) |
357 | literals_of_term ((Const("Not",_) $ P),(lits,ts)) = |
461 end |
358 let val (pred,ts') = predicate_of P |
462 | literals_of_term ((Const("Not",_) $ P),(lits,ts), preds, funcs) = |
359 val lits' = Literal(false,pred,false) :: lits |
463 let val (pred,ts', preds', funcs') = predicate_of P |
360 val ts'' = ResLib.no_rep_app ts ts' |
464 val lits' = Literal(false,pred,false) :: lits |
361 in |
465 val ts'' = ResLib.no_rep_app ts ts' |
362 (lits',ts'') |
466 in |
363 end |
467 (lits',ts'', distinct(preds'@preds), distinct(funcs'@funcs)) |
364 | literals_of_term (P,(lits,ts)) = |
468 end |
365 let val (pred,ts') = predicate_of P |
469 | literals_of_term (P,(lits,ts), preds, funcs) = |
366 val lits' = Literal(true,pred,false) :: lits |
470 let val (pred,ts', preds', funcs') = predicate_of P |
367 val ts'' = ResLib.no_rep_app ts ts' |
471 val lits' = Literal(true,pred,false) :: lits |
368 in |
472 val ts'' = ResLib.no_rep_app ts ts' |
369 (lits',ts'') |
473 in |
370 end; |
474 (lits',ts'', distinct(preds'@preds), distinct(funcs'@funcs)) |
371 |
475 end; |
372 fun literals_of_thm thm = literals_of_term (prop_of thm, ([],[])); |
476 |
373 |
477 |
|
478 fun literals_of_thm thm = literals_of_term (prop_of thm, ([],[]), [], []); |
|
479 |
|
480 |
|
481 (* FIX: not sure what to do with these funcs *) |
|
482 |
374 (*Make literals for sorted type variables*) |
483 (*Make literals for sorted type variables*) |
375 fun sorts_on_typs (_, []) = [] |
484 fun sorts_on_typs (_, []) = ([]) |
376 | sorts_on_typs (v, "HOL.type" :: s) = |
485 | sorts_on_typs (v, "HOL.type" :: s) = |
377 sorts_on_typs (v,s) (*Ignore sort "type"*) |
486 sorts_on_typs (v,s) (*Ignore sort "type"*) |
378 | sorts_on_typs ((FOLTVar(indx)), (s::ss)) = |
487 | sorts_on_typs ((FOLTVar(indx)), (s::ss)) = |
379 LTVar((make_type_class s) ^ |
488 (LTVar((make_type_class s) ^ |
380 "(" ^ (make_schematic_type_var indx) ^ ")") :: |
489 "(" ^ (make_schematic_type_var( indx)) ^ ")") :: |
381 (sorts_on_typs ((FOLTVar(indx)), ss)) |
490 (sorts_on_typs ((FOLTVar(indx)), ss))) |
382 | sorts_on_typs ((FOLTFree(x)), (s::ss)) = |
491 | sorts_on_typs ((FOLTFree(x)), (s::ss)) = |
383 LTFree((make_type_class s) ^ "(" ^ (make_fixed_type_var(x)) ^ ")") :: |
492 LTFree((make_type_class s) ^ "(" ^ (make_fixed_type_var(x)) ^ ")") :: |
384 (sorts_on_typs ((FOLTFree(x)), ss)); |
493 (sorts_on_typs ((FOLTFree(x)), ss)); |
385 |
494 |
|
495 |
|
496 fun takeUntil ch [] res = (res, []) |
|
497 | takeUntil ch (x::xs) res = if x = ch |
|
498 then |
|
499 (res, xs) |
|
500 else |
|
501 takeUntil ch xs (res@[x]) |
|
502 |
|
503 fun remove_type str = let val exp = explode str |
|
504 val (first,rest) = (takeUntil "(" exp []) |
|
505 in |
|
506 implode first |
|
507 end |
|
508 |
|
509 fun pred_of_sort (LTVar x) = ((remove_type x),1) |
|
510 | pred_of_sort (LTFree x) = ((remove_type x),1) |
|
511 |
|
512 |
|
513 |
|
514 |
386 (*Given a list of sorted type variables, return two separate lists. |
515 (*Given a list of sorted type variables, return two separate lists. |
387 The first is for TVars, the second for TFrees.*) |
516 The first is for TVars, the second for TFrees.*) |
388 fun add_typs_aux [] = ([],[]) |
517 fun add_typs_aux [] preds = ([],[], preds) |
|
518 | add_typs_aux ((FOLTVar(indx),s)::tss) preds = |
|
519 let val (vs) = sorts_on_typs (FOLTVar(indx), s) |
|
520 val preds' = (map pred_of_sort vs)@preds |
|
521 val (vss,fss, preds'') = add_typs_aux tss preds' |
|
522 in |
|
523 (ResLib.no_rep_app vs vss, fss, preds'') |
|
524 end |
|
525 | add_typs_aux ((FOLTFree(x),s)::tss) preds = |
|
526 let val (fs) = sorts_on_typs (FOLTFree(x), s) |
|
527 val preds' = (map pred_of_sort fs)@preds |
|
528 val (vss,fss, preds'') = add_typs_aux tss preds' |
|
529 in |
|
530 (vss, ResLib.no_rep_app fs fss,preds'') |
|
531 end; |
|
532 |
|
533 |
|
534 (*fun add_typs_aux [] = ([],[]) |
389 | add_typs_aux ((FOLTVar(indx),s)::tss) = |
535 | add_typs_aux ((FOLTVar(indx),s)::tss) = |
390 let val vs = sorts_on_typs (FOLTVar(indx), s) |
536 let val vs = sorts_on_typs (FOLTVar(indx), s) |
391 val (vss,fss) = add_typs_aux tss |
537 val (vss,fss) = add_typs_aux tss |
392 in |
538 in |
393 (ResLib.no_rep_app vs vss, fss) |
539 (ResLib.no_rep_app vs vss, fss) |
395 | add_typs_aux ((FOLTFree(x),s)::tss) = |
541 | add_typs_aux ((FOLTFree(x),s)::tss) = |
396 let val fs = sorts_on_typs (FOLTFree(x), s) |
542 let val fs = sorts_on_typs (FOLTFree(x), s) |
397 val (vss,fss) = add_typs_aux tss |
543 val (vss,fss) = add_typs_aux tss |
398 in |
544 in |
399 (vss, ResLib.no_rep_app fs fss) |
545 (vss, ResLib.no_rep_app fs fss) |
|
546 end;*) |
|
547 |
|
548 |
|
549 fun add_typs (Clause cls) preds = add_typs_aux (#types_sorts cls) preds |
|
550 |
|
551 |
|
552 (** make axiom clauses, hypothesis clauses and conjecture clauses. **) |
|
553 |
|
554 local |
|
555 fun replace_dot "." = "_" |
|
556 | replace_dot "'" = "" |
|
557 | replace_dot c = c; |
|
558 |
|
559 in |
|
560 |
|
561 fun proper_ax_name ax_name = |
|
562 let val chars = explode ax_name |
|
563 in |
|
564 implode (map replace_dot chars) |
|
565 end; |
|
566 end; |
|
567 |
|
568 fun get_tvar_strs [] = [] |
|
569 | get_tvar_strs ((FOLTVar(indx),s)::tss) = |
|
570 let val vstr =(make_schematic_type_var( indx)); |
|
571 val (vstrs) = get_tvar_strs tss |
|
572 in |
|
573 (distinct( vstr:: vstrs)) |
|
574 end |
|
575 | get_tvar_strs((FOLTFree(x),s)::tss) = |
|
576 let val (vstrs) = get_tvar_strs tss |
|
577 in |
|
578 (distinct( vstrs)) |
400 end; |
579 end; |
401 |
580 |
402 fun add_typs (Clause cls) = add_typs_aux (#types_sorts cls) |
581 (* FIX add preds and funcs to add typs aux here *) |
403 |
582 |
404 |
583 fun make_axiom_clause_thm thm (name,number)= |
405 (** make axiom clauses, hypothesis clauses and conjecture clauses. **) |
584 let val (lits,types_sorts, preds, funcs) = literals_of_thm thm |
406 |
585 val cls_id = number |
|
586 val (tvar_lits,tfree_lits, preds) = add_typs_aux types_sorts preds |
|
587 val tvars = get_tvar_strs types_sorts |
|
588 val ax_name = proper_ax_name name |
|
589 in |
|
590 make_clause(cls_id,ax_name,Axiom,lits,types_sorts,tvar_lits,tfree_lits,tvars, preds, funcs) |
|
591 end; |
|
592 |
|
593 |
407 |
594 |
408 fun make_conjecture_clause_thm thm = |
595 fun make_conjecture_clause_thm thm = |
409 let val (lits,types_sorts) = literals_of_thm thm |
596 let val (lits,types_sorts, preds, funcs) = literals_of_thm thm |
410 val cls_id = generate_id() |
597 val cls_id = generate_id() |
411 val (tvar_lits,tfree_lits) = add_typs_aux types_sorts |
598 val (tvar_lits,tfree_lits, preds) = add_typs_aux types_sorts preds |
412 in |
599 val tvars = get_tvar_strs types_sorts |
413 make_clause(cls_id,"",Conjecture,lits,types_sorts,tvar_lits,tfree_lits) |
600 in |
414 end; |
601 make_clause(cls_id,"",Conjecture,lits,types_sorts,tvar_lits,tfree_lits,tvars, preds, funcs) |
415 |
602 end; |
416 |
603 |
417 fun make_axiom_clause term (axname,cls_id) = |
604 |
418 let val (lits,types_sorts) = literals_of_term (term,([],[])) |
605 fun make_axiom_clause term (name,number)= |
419 val (tvar_lits,tfree_lits) = add_typs_aux types_sorts |
606 let val (lits,types_sorts, preds,funcs) = literals_of_term (term,([],[]), [],[]) |
|
607 val cls_id = number |
|
608 val (tvar_lits,tfree_lits, preds) = add_typs_aux types_sorts preds |
|
609 val tvars = get_tvar_strs types_sorts |
|
610 val ax_name = proper_ax_name name |
420 in |
611 in |
421 make_clause(cls_id,axname,Axiom,lits,types_sorts,tvar_lits,tfree_lits) |
612 make_clause(cls_id,ax_name,Axiom,lits,types_sorts,tvar_lits,tfree_lits,tvars, preds, funcs) |
422 end; |
613 end; |
423 |
614 |
424 |
615 |
425 fun make_hypothesis_clause term = |
616 fun make_hypothesis_clause term = |
426 let val (lits,types_sorts) = literals_of_term (term,([],[])) |
617 let val (lits,types_sorts, preds, funcs) = literals_of_term (term,([],[]),[],[]) |
427 val cls_id = generate_id() |
618 val cls_id = generate_id() |
428 val (tvar_lits,tfree_lits) = add_typs_aux types_sorts |
619 val (tvar_lits,tfree_lits, preds) = add_typs_aux types_sorts preds |
429 in |
620 val tvars = get_tvar_strs types_sorts |
430 make_clause(cls_id,"",Hypothesis,lits,types_sorts,tvar_lits,tfree_lits) |
621 in |
|
622 make_clause(cls_id,"",Hypothesis,lits,types_sorts,tvar_lits,tfree_lits,tvars, preds, funcs) |
431 end; |
623 end; |
432 |
624 |
433 |
625 |
434 fun make_conjecture_clause term = |
626 fun make_conjecture_clause term = |
435 let val (lits,types_sorts) = literals_of_term (term,([],[])) |
627 let val (lits,types_sorts, preds, funcs) = literals_of_term (term,([],[]),[],[]) |
436 val cls_id = generate_id() |
628 val cls_id = generate_id() |
437 val (tvar_lits,tfree_lits) = add_typs_aux types_sorts |
629 val (tvar_lits,tfree_lits, preds) = add_typs_aux types_sorts preds |
438 in |
630 val tvars = get_tvar_strs types_sorts |
439 make_clause(cls_id,"",Conjecture,lits,types_sorts,tvar_lits,tfree_lits) |
631 in |
|
632 make_clause(cls_id,"",Conjecture,lits,types_sorts,tvar_lits,tfree_lits,tvars, preds, funcs) |
440 end; |
633 end; |
441 |
634 |
442 |
635 |
443 |
636 |
444 (**** Isabelle arities ****) |
637 (**** Isabelle arities ****) |
563 |
757 |
564 |
758 |
565 |
759 |
566 (* Changed for typed equality *) |
760 (* Changed for typed equality *) |
567 (* before output the string of the predicate, check if the predicate corresponds to an equality or not. *) |
761 (* before output the string of the predicate, check if the predicate corresponds to an equality or not. *) |
568 fun string_of_predicate (Predicate("equal",typ,terms)) = |
762 fun string_of_predicate (Predicate("equal",typ,terms)) = string_of_equality(typ,terms) |
569 string_of_equality(typ,terms) |
763 | string_of_predicate (Predicate(name,_,[])) = name |
|
764 | string_of_predicate (Predicate(name,typ,terms)) = |
|
765 let val terms_as_strings = map string_of_term terms |
|
766 in |
|
767 if (!keep_types) then name ^ (ResLib.list_to_string (typ :: terms_as_strings)) |
|
768 else name ^ (ResLib.list_to_string terms_as_strings) |
|
769 end; |
|
770 |
|
771 |
|
772 |
|
773 (********************************) |
|
774 (* Code for producing DFG files *) |
|
775 (********************************) |
|
776 |
|
777 fun dfg_literal (Literal(pol,pred,tag)) = |
|
778 let val pred_string = string_of_predicate pred |
|
779 val tagged_pol =if pol then pred_string else "not(" ^pred_string ^ ")" |
|
780 in |
|
781 tagged_pol |
|
782 end; |
|
783 |
|
784 |
|
785 (* FIX: what does this mean? *) |
|
786 (*fun dfg_of_typeLit (LTVar x) = "not(" ^ x ^ ")" |
|
787 | dfg_of_typeLit (LTFree x) = "(" ^ x ^ ")";*) |
|
788 |
|
789 fun dfg_of_typeLit (LTVar x) = x |
|
790 | dfg_of_typeLit (LTFree x) = x ; |
|
791 |
|
792 |
|
793 fun strlist [] = "" |
|
794 | strlist (x::[]) = x |
|
795 | strlist (x::xs) = x ^ "," ^ (strlist xs) |
|
796 |
|
797 |
|
798 fun gen_dfg_cls (cls_id,ax_name,knd,lits, tvars,vars) = |
|
799 let val ax_str = (if ax_name = "" then "" else ("_" ^ ax_name)) |
|
800 val forall_str = if (vars = []) andalso (tvars = []) |
|
801 then |
|
802 "" |
|
803 else |
|
804 "forall([" ^ (strlist (vars@tvars))^ "]" |
|
805 in |
|
806 if forall_str = "" |
|
807 then |
|
808 "clause( %(" ^ knd ^ ")\n" ^ "or(" ^ lits ^ ") ,\n" ^ cls_id ^ ax_str ^ ")." |
|
809 else |
|
810 "clause( %(" ^ knd ^ ")\n" ^ forall_str ^ ",\n" ^ "or(" ^ lits ^ ")),\n" ^ cls_id ^ ax_str ^ ")." |
|
811 end; |
|
812 |
|
813 |
|
814 |
|
815 fun gen_dfg_type_cls (cls_id,knd,tfree_lit,idx,tvars, vars) = |
|
816 let val forall_str = if (vars = []) andalso (tvars = []) |
|
817 then |
|
818 "" |
|
819 else |
|
820 "forall([" ^ (strlist (vars@tvars))^"]" |
|
821 in |
|
822 if forall_str = "" |
|
823 then |
|
824 "clause( %(" ^ knd ^ ")\n" ^ "or( " ^ tfree_lit ^ ") ,\n" ^ cls_id ^ "_tcs" ^ (string_of_int idx) ^ ")." |
|
825 else |
|
826 "clause( %(" ^ knd ^ ")\n" ^ forall_str ^ ",\n" ^ "or( " ^ tfree_lit ^ ")),\n" ^ cls_id ^ "_tcs" ^ (string_of_int idx) ^ ")." |
|
827 end; |
|
828 |
|
829 |
|
830 |
|
831 fun dfg_clause_aux (Clause cls) = |
|
832 let val lits = map dfg_literal (#literals cls) |
|
833 val tvar_lits_strs = if (!keep_types) then (map dfg_of_typeLit (#tvar_type_literals cls)) else [] |
|
834 val tfree_lits = if (!keep_types) then (map dfg_of_typeLit (#tfree_type_literals cls)) else [] |
|
835 in |
|
836 (tvar_lits_strs @ lits,tfree_lits) |
|
837 end; |
|
838 |
|
839 |
|
840 fun dfg_folterms (Literal(pol,pred,tag)) = |
|
841 let val Predicate (predname, foltype, folterms) = pred |
|
842 in |
|
843 folterms |
|
844 end |
|
845 |
|
846 |
|
847 fun get_uvars (UVar(str,typ)) =(*if (substring (str, 0,2))= "V_" then *)[str] (*else []*) |
|
848 | get_uvars (Fun (str,typ,tlist)) = ResLib.flat_noDup(map get_uvars tlist) |
|
849 |
|
850 |
|
851 fun is_uvar (UVar(str,typ)) = true |
|
852 | is_uvar (Fun (str,typ,tlist)) = false; |
|
853 |
|
854 fun uvar_name (UVar(str,typ)) = str |
|
855 | uvar_name _ = (raise CLAUSE("Not a variable")); |
|
856 |
|
857 |
|
858 fun mergelist [] = [] |
|
859 | mergelist (x::xs ) = x@(mergelist xs) |
|
860 |
|
861 |
|
862 fun dfg_vars (Clause cls) = |
|
863 let val lits = (#literals cls) |
|
864 val folterms = mergelist(map dfg_folterms lits) |
|
865 val vars = ResLib.flat_noDup(map get_uvars folterms) |
|
866 in |
|
867 vars |
|
868 end |
|
869 |
|
870 |
|
871 fun dfg_tvars (Clause cls) =(#tvars cls) |
|
872 |
|
873 |
|
874 |
|
875 (* make this return funcs and preds too? *) |
|
876 fun string_of_predname (Predicate("equal",typ,terms)) = "EQUALITY" |
|
877 | string_of_predname (Predicate(name,_,[])) = name |
|
878 | string_of_predname (Predicate(name,typ,terms)) = name |
|
879 |
|
880 |
|
881 (* make this return funcs and preds too? *) |
|
882 |
|
883 fun string_of_predicate (Predicate("equal",typ,terms)) = string_of_equality(typ,terms) |
570 | string_of_predicate (Predicate(name,_,[])) = name |
884 | string_of_predicate (Predicate(name,_,[])) = name |
571 | string_of_predicate (Predicate(name,typ,terms)) = |
885 | string_of_predicate (Predicate(name,typ,terms)) = |
572 let val terms_as_strings = map string_of_term terms |
886 let val terms_as_strings = map string_of_term terms |
573 in |
887 in |
574 if !keep_types andalso typ<>"" |
888 if !keep_types andalso typ<>"" |
575 then name ^ (ResLib.list_to_string (terms_as_strings @ [typ])) |
889 then name ^ (ResLib.list_to_string (terms_as_strings @ [typ])) |
576 else name ^ (ResLib.list_to_string terms_as_strings) |
890 else name ^ (ResLib.list_to_string terms_as_strings) |
577 end; |
891 end; |
578 |
892 |
|
893 |
|
894 |
|
895 |
|
896 fun concat_with sep [] = "" |
|
897 | concat_with sep [x] = "(" ^ x ^ ")" |
|
898 | concat_with sep (x::xs) = "(" ^ x ^ ")" ^ sep ^ (concat_with sep xs); |
|
899 |
|
900 fun concat_with_comma [] = "" |
|
901 | concat_with_comma [x] = x |
|
902 | concat_with_comma (x::xs) = x ^ ", " ^ (concat_with_comma xs); |
|
903 |
|
904 |
|
905 fun dfg_pred (Literal(pol,pred,tag)) ax_name = (string_of_predname pred)^" "^ax_name |
|
906 |
|
907 fun dfg_clause cls = |
|
908 let val (lits,tfree_lits) = dfg_clause_aux cls (*"lits" includes the typing assumptions (TVars)*) |
|
909 val vars = dfg_vars cls |
|
910 val tvars = dfg_tvars cls |
|
911 val cls_id = string_of_clauseID cls |
|
912 val ax_name = string_of_axiomName cls |
|
913 val knd = string_of_kind cls |
|
914 val lits_str = concat_with_comma lits |
|
915 val cls_str = gen_dfg_cls(cls_id,ax_name,knd,lits_str,tvars, vars) |
|
916 fun typ_clss k [] = [] |
|
917 | typ_clss k (tfree :: tfrees) = |
|
918 (gen_dfg_type_cls(cls_id,knd,tfree,k, tvars,vars)) :: (typ_clss (k+1) tfrees) |
|
919 in |
|
920 cls_str :: (typ_clss 0 tfree_lits) |
|
921 end; |
|
922 |
|
923 fun clause_info cls = |
|
924 let |
|
925 val cls_id = string_of_clauseID cls |
|
926 val ax_name = string_of_axiomName cls |
|
927 in |
|
928 ((ax_name^""), cls_id) |
|
929 end; |
|
930 |
|
931 |
|
932 |
|
933 fun zip_concat name [] = [] |
|
934 | zip_concat name ((str, num)::xs) = (((str^name), num)::(zip_concat name xs)) |
|
935 |
|
936 |
|
937 (*fun funcs_of_cls (Clause cls) = let val funcs = #functions cls |
|
938 val name = #axiom_name cls |
|
939 in |
|
940 zip_concat name funcs |
|
941 end; |
|
942 |
|
943 |
|
944 fun preds_of_cls (Clause cls) = let val preds = #predicates cls |
|
945 ; val name = ("foo"^(#axiom_name cls)) |
|
946 in |
|
947 zip_concat name preds |
|
948 end |
|
949 *) |
|
950 |
|
951 fun funcs_of_cls (Clause cls) = #functions cls; |
|
952 |
|
953 |
|
954 fun preds_of_cls (Clause cls) = #predicates cls; |
|
955 |
|
956 |
|
957 |
|
958 |
|
959 fun string_of_arity (name, num) = name ^"," ^ (string_of_int num) |
|
960 |
|
961 |
|
962 fun string_of_preds preds = "predicates[" ^ (concat_with ", " (map string_of_arity preds)) ^ "].\n"; |
|
963 |
|
964 fun string_of_funcs funcs ="functions[" ^ (concat_with ", " (map string_of_arity funcs)) ^ "].\n" ; |
|
965 |
|
966 |
|
967 fun string_of_symbols predstr funcstr = "list_of_symbols.\n" ^ predstr ^ funcstr ^ "end_of_list.\n\n"; |
|
968 |
|
969 |
|
970 fun string_of_axioms axstr = "list_of_clauses(axioms,cnf).\n" ^ axstr ^ "end_of_list.\n\n"; |
|
971 |
|
972 |
|
973 fun string_of_conjectures conjstr = "list_of_clauses(conjectures,cnf).\n" ^ conjstr ^ "end_of_list.\n\n"; |
|
974 |
|
975 fun string_of_descrip () = "list_of_descriptions.\nname({*[ File : ],[ Names :]*}).\nauthor({*[ Source :]*}).\nstatus(unknown).\ndescription({*[ Refs :]*}).\nend_of_list.\n\n" |
|
976 |
|
977 |
|
978 fun string_of_start name = "%------------------------------------------------------------------------------\nbegin_problem(" ^ name ^ ").\n\n"; |
|
979 |
|
980 |
|
981 fun string_of_end () = "end_problem.\n%------------------------------------------------------------------------------"; |
|
982 |
|
983 val delim = "\n"; |
|
984 val dfg_clauses2str = ResLib.list2str_sep delim; |
|
985 |
|
986 |
|
987 fun clause2dfg cls = |
|
988 let val (lits,tfree_lits) = dfg_clause_aux cls (*"lits" includes the typing assumptions (TVars)*) |
|
989 val cls_id = string_of_clauseID cls |
|
990 val ax_name = string_of_axiomName cls |
|
991 val vars = dfg_vars cls |
|
992 val tvars = dfg_tvars cls |
|
993 val funcs = funcs_of_cls cls |
|
994 val preds = preds_of_cls cls |
|
995 val knd = string_of_kind cls |
|
996 val lits_str = concat_with_comma lits |
|
997 val cls_str = gen_dfg_cls(cls_id,ax_name,knd,lits_str,tvars,vars) |
|
998 in |
|
999 (cls_str,tfree_lits) |
|
1000 end; |
|
1001 |
|
1002 |
|
1003 |
|
1004 fun tfree_dfg_clause tfree_lit = "clause( %(conjecture)\n" ^ "or( " ^ tfree_lit ^ ")),\n" ^ "tfree_tcs" ^ ")." |
|
1005 |
|
1006 |
|
1007 fun gen_dfg_file fname axioms conjectures funcs preds tfrees= |
|
1008 let val (axstrs_tfrees) = (map clause2dfg axioms) |
|
1009 val (axstrs, atfrees) = ListPair.unzip axstrs_tfrees |
|
1010 val axstr = ResLib.list2str_sep delim axstrs |
|
1011 val (conjstrs_tfrees) = (map clause2dfg conjectures) |
|
1012 val (conjstrs, atfrees) = ListPair.unzip conjstrs_tfrees |
|
1013 val tfree_clss = map tfree_dfg_clause ((ResLib.flat_noDup atfrees) \\ tfrees) |
|
1014 val conjstr = ResLib.list2str_sep delim (tfree_clss@conjstrs) |
|
1015 val funcstr = string_of_funcs funcs |
|
1016 val predstr = string_of_preds preds |
|
1017 in |
|
1018 (string_of_start fname) ^ (string_of_descrip ()) ^ (string_of_symbols funcstr predstr ) ^ |
|
1019 (string_of_axioms axstr)^ |
|
1020 (string_of_conjectures conjstr) ^ (string_of_end ()) |
|
1021 end; |
|
1022 |
|
1023 |
|
1024 |
|
1025 fun clauses2dfg [] filename axioms conjectures funcs preds tfrees= |
|
1026 let val funcs' = ((ResLib.flat_noDup(map funcs_of_cls axioms))@funcs) |
|
1027 val preds' = ((ResLib.flat_noDup(map preds_of_cls axioms))@preds) |
|
1028 |
|
1029 |
|
1030 in |
|
1031 gen_dfg_file filename axioms conjectures funcs' preds' tfrees |
|
1032 (*(filename, axioms, conjectures, funcs, preds)*) |
|
1033 end |
|
1034 |clauses2dfg (cls::clss) filename axioms conjectures funcs preds tfrees = |
|
1035 let val (lits,tfree_lits) = dfg_clause_aux (cls) (*"lits" includes the typing assumptions (TVars)*) |
|
1036 val cls_id = string_of_clauseID cls |
|
1037 val ax_name = string_of_axiomName cls |
|
1038 val vars = dfg_vars cls |
|
1039 val tvars = dfg_tvars cls |
|
1040 val funcs' = distinct((funcs_of_cls cls)@funcs) |
|
1041 val preds' = distinct((preds_of_cls cls)@preds) |
|
1042 val knd = string_of_kind cls |
|
1043 val lits_str = concat_with ", " lits |
|
1044 val axioms' = if knd = "axiom" then (cls::axioms) else axioms |
|
1045 val conjectures' = if knd = "conjecture" then (cls::conjectures) else conjectures |
|
1046 in |
|
1047 clauses2dfg clss filename axioms' conjectures' funcs' preds' tfrees |
|
1048 end; |
|
1049 |
|
1050 |
|
1051 fun fileout f str = let val out = TextIO.openOut(f) |
|
1052 in |
|
1053 ResLib.writeln_strs out (str); TextIO.closeOut out |
|
1054 end; |
|
1055 |
|
1056 (*val filestr = clauses2dfg newcls "flump" [] [] [] []; |
|
1057 *) |
|
1058 (* fileout "flump.dfg" [filestr];*) |
|
1059 |
|
1060 |
|
1061 (*FIX: ask Jia what this is for *) |
|
1062 |
|
1063 |
|
1064 fun string_of_arClauseID (ArityClause arcls) = arclause_prefix ^ string_of_int(#clause_id arcls); |
|
1065 |
|
1066 |
|
1067 fun string_of_arLit (TConsLit(b,(c,t,args))) = |
|
1068 let val pol = if b then "++" else "--" |
|
1069 val arg_strs = (case args of [] => "" | _ => ResLib.list_to_string args) |
|
1070 in |
|
1071 pol ^ c ^ "(" ^ t ^ arg_strs ^ ")" |
|
1072 end |
|
1073 | string_of_arLit (TVarLit(b,(c,str))) = |
|
1074 let val pol = if b then "++" else "--" |
|
1075 in |
|
1076 pol ^ c ^ "(" ^ str ^ ")" |
|
1077 end; |
579 |
1078 |
|
1079 |
|
1080 fun string_of_conclLit (ArityClause arcls) = string_of_arLit (#conclLit arcls); |
|
1081 |
|
1082 |
|
1083 fun strings_of_premLits (ArityClause arcls) = map string_of_arLit (#premLits arcls); |
|
1084 |
|
1085 |
|
1086 fun string_of_arKind (ArityClause arcls) = name_of_kind(#kind arcls); |
|
1087 |
|
1088 (*FIX: would this have variables in a forall? *) |
|
1089 |
|
1090 fun dfg_arity_clause arcls = |
|
1091 let val arcls_id = string_of_arClauseID arcls |
|
1092 val concl_lit = string_of_conclLit arcls |
|
1093 val prems_lits = strings_of_premLits arcls |
|
1094 val knd = string_of_arKind arcls |
|
1095 val all_lits = concl_lit :: prems_lits |
|
1096 in |
|
1097 |
|
1098 "clause( %(" ^ knd ^ ")\n" ^ "or( " ^ (ResLib.list_to_string' all_lits) ^ ")),\n" ^ arcls_id ^ ")." |
|
1099 end; |
|
1100 |
|
1101 |
|
1102 val clrelclause_prefix = "relcls_"; |
|
1103 |
|
1104 (* FIX later. Doesn't seem to be used in clasimp *) |
|
1105 |
|
1106 (*fun tptp_classrelLits sub sup = |
|
1107 let val tvar = "(T)" |
|
1108 in |
|
1109 case sup of NONE => "[++" ^ sub ^ tvar ^ "]" |
|
1110 | (SOME supcls) => "[--" ^ sub ^ tvar ^ ",++" ^ supcls ^ tvar ^ "]" |
|
1111 end; |
|
1112 |
|
1113 |
|
1114 fun tptp_classrelClause (ClassrelClause cls) = |
|
1115 let val relcls_id = clrelclause_prefix ^ string_of_int(#clause_id cls) |
|
1116 val sub = #subclass cls |
|
1117 val sup = #superclass cls |
|
1118 val lits = tptp_classrelLits sub sup |
|
1119 in |
|
1120 "input_clause(" ^ relcls_id ^ ",axiom," ^ lits ^ ")." |
|
1121 end; |
|
1122 *) |
|
1123 |
|
1124 (********************************) |
|
1125 (* code to produce TPTP files *) |
|
1126 (********************************) |
|
1127 |
580 |
1128 |
581 |
1129 |
582 fun tptp_literal (Literal(pol,pred,tag)) = |
1130 fun tptp_literal (Literal(pol,pred,tag)) = |
583 let val pred_string = string_of_predicate pred |
1131 let val pred_string = string_of_predicate pred |
584 val tagged_pol = |
1132 val tagged_pol = if (tag andalso !tagged) then (if pol then "+++" else "---") |
585 if (tag andalso !tagged) then (if pol then "+++" else "---") |
1133 else (if pol then "++" else "--") |
586 else (if pol then "++" else "--") |
|
587 in |
1134 in |
588 tagged_pol ^ pred_string |
1135 tagged_pol ^ pred_string |
589 end; |
1136 end; |
590 |
1137 |
591 |
1138 |