206 |
206 |
207 val tagged = ref false; |
207 val tagged = ref false; |
208 |
208 |
209 type pred_name = string; |
209 type pred_name = string; |
210 type sort = Term.sort; |
210 type sort = Term.sort; |
211 type fol_type = string; |
211 |
|
212 |
|
213 |
|
214 datatype typ_var = FOLTVar of indexname | FOLTFree of string; |
|
215 |
|
216 datatype fol_type = AtomV of string |
|
217 | AtomF of string |
|
218 | Comp of string * fol_type list; |
|
219 |
|
220 fun string_of_fol_type (AtomV x) = x |
|
221 | string_of_fol_type (AtomF x) = x |
|
222 | string_of_fol_type (Comp(tcon,tps)) = |
|
223 let val tstrs = map string_of_fol_type tps |
|
224 in |
|
225 tcon ^ (paren_pack tstrs) |
|
226 end; |
|
227 |
212 |
228 |
213 datatype type_literal = LTVar of string | LTFree of string; |
229 datatype type_literal = LTVar of string | LTFree of string; |
214 |
230 |
215 datatype folTerm = UVar of string * fol_type |
231 datatype folTerm = UVar of string * fol_type |
216 | Fun of string * fol_type list * folTerm list; |
232 | Fun of string * fol_type list * folTerm list; |
217 datatype predicate = Predicate of pred_name * fol_type list * folTerm list; |
233 datatype predicate = Predicate of pred_name * fol_type list * folTerm list; |
218 |
234 |
219 datatype literal = Literal of polarity * predicate * tag; |
235 datatype literal = Literal of polarity * predicate * tag; |
220 |
|
221 datatype typ_var = FOLTVar of indexname | FOLTFree of string; |
|
222 |
236 |
223 fun mk_typ_var_sort (TFree(a,s)) = (FOLTFree a,s) |
237 fun mk_typ_var_sort (TFree(a,s)) = (FOLTFree a,s) |
224 | mk_typ_var_sort (TVar(v,s)) = (FOLTVar v,s); |
238 | mk_typ_var_sort (TVar(v,s)) = (FOLTVar v,s); |
225 |
239 |
226 |
240 |
239 functions: (string*int) list}; |
253 functions: (string*int) list}; |
240 |
254 |
241 |
255 |
242 exception CLAUSE of string * term; |
256 exception CLAUSE of string * term; |
243 |
257 |
|
258 fun get_literals (c as Clause(cls)) = #literals cls; |
|
259 |
|
260 fun components_of_literal (Literal (pol,pred,tag)) = ((pol,pred),tag); |
|
261 |
|
262 fun predicate_name (Predicate(predname,_,_)) = predname; |
|
263 |
244 |
264 |
245 (*** make clauses ***) |
265 (*** make clauses ***) |
246 |
266 |
247 fun isFalse (Literal (pol,Predicate(a,_,[]),_)) = |
267 fun isFalse (Literal (pol,Predicate(a,_,[]),_)) = |
248 (pol andalso a = "c_False") orelse |
268 (pol andalso a = "c_False") orelse |
291 (*Initialize the type suppression mechanism with the current theory before |
311 (*Initialize the type suppression mechanism with the current theory before |
292 producing any clauses!*) |
312 producing any clauses!*) |
293 fun init thy = (const_typargs := Sign.const_typargs thy); |
313 fun init thy = (const_typargs := Sign.const_typargs thy); |
294 |
314 |
295 |
315 |
296 (*Flatten a type to a string while accumulating sort constraints on the TFrees and |
316 (*Flatten a type to a fol_type while accumulating sort constraints on the TFrees and |
297 TVars it contains.*) |
317 TVars it contains.*) |
298 fun type_of (Type (a, Ts)) = |
318 fun type_of (Type (a, Ts)) = |
299 let val (folTyps, (ts, funcs)) = types_of Ts |
319 let val (folTyps, (ts, funcs)) = types_of Ts |
300 val t = make_fixed_type_const a |
320 val t = make_fixed_type_const a |
301 in |
321 in |
302 ((t ^ paren_pack folTyps), (ts, (t, length Ts)::funcs)) |
322 (Comp(t,folTyps), (ts, (t, length Ts)::funcs)) |
303 end |
323 end |
304 | type_of (TFree (a,s)) = |
324 | type_of (TFree (a,s)) = |
305 let val t = make_fixed_type_var a |
325 let val t = make_fixed_type_var a |
306 in (t, ([((FOLTFree a),s)], [(t,0)])) end |
326 in (AtomF(t), ([((FOLTFree a),s)], [(t,0)])) end |
307 | type_of (TVar (v, s)) = (make_schematic_type_var v, ([((FOLTVar v),s)], [])) |
327 | type_of (TVar (v, s)) = (AtomV(make_schematic_type_var v), ([((FOLTVar v),s)], [])) |
308 and types_of Ts = |
328 and types_of Ts = |
309 let val foltyps_ts = map type_of Ts |
329 let val foltyps_ts = map type_of Ts |
310 val (folTyps,ts_funcs) = ListPair.unzip foltyps_ts |
330 val (folTyps,ts_funcs) = ListPair.unzip foltyps_ts |
311 val (ts, funcslist) = ListPair.unzip ts_funcs |
331 val (ts, funcslist) = ListPair.unzip ts_funcs |
312 in |
332 in |
445 |
465 |
446 |
466 |
447 val literals_of_term = literals_of_term1 ([],[],[],[]); |
467 val literals_of_term = literals_of_term1 ([],[],[],[]); |
448 |
468 |
449 |
469 |
|
470 fun predicate_ord (Predicate(predname1,_,_),Predicate(predname2,_,_)) = string_ord (predname1,predname2); |
|
471 |
|
472 |
|
473 fun literal_ord (Literal(false,_,_),Literal(true,_,_)) = LESS |
|
474 | literal_ord (Literal(true,_,_),Literal(false,_,_)) = GREATER |
|
475 | literal_ord (Literal(_,pred1,_),Literal(_,pred2,_)) = predicate_ord(pred1,pred2); |
|
476 |
|
477 fun sort_lits lits = sort literal_ord lits; |
|
478 |
|
479 |
|
480 |
450 (* FIX: not sure what to do with these funcs *) |
481 (* FIX: not sure what to do with these funcs *) |
451 |
482 |
452 (*Make literals for sorted type variables*) |
483 (*Make literals for sorted type variables*) |
453 fun sorts_on_typs (_, []) = ([]) |
484 fun sorts_on_typs (_, []) = ([]) |
454 | sorts_on_typs (v, "HOL.type" :: s) = |
485 | sorts_on_typs (v, "HOL.type" :: s) = |
520 |
551 |
521 (* FIX add preds and funcs to add typs aux here *) |
552 (* FIX add preds and funcs to add typs aux here *) |
522 |
553 |
523 fun make_axiom_clause_thm thm (ax_name,cls_id) = |
554 fun make_axiom_clause_thm thm (ax_name,cls_id) = |
524 let val (lits,types_sorts, preds, funcs) = literals_of_term (prop_of thm) |
555 let val (lits,types_sorts, preds, funcs) = literals_of_term (prop_of thm) |
|
556 val lits' = sort_lits lits |
525 val (tvar_lits,tfree_lits, preds) = add_typs_aux types_sorts preds |
557 val (tvar_lits,tfree_lits, preds) = add_typs_aux types_sorts preds |
526 val tvars = get_tvar_strs types_sorts |
558 val tvars = get_tvar_strs types_sorts |
527 in |
559 in |
528 make_clause(cls_id,ax_name,Axiom, |
560 make_clause(cls_id,ax_name,Axiom, |
529 lits,types_sorts,tvar_lits,tfree_lits, |
561 lits',types_sorts,tvar_lits,tfree_lits, |
530 tvars, preds, funcs) |
562 tvars, preds, funcs) |
531 end; |
563 end; |
532 |
564 |
533 |
565 |
534 (* check if a clause is FOL first*) |
566 (* check if a clause is FOL first*) |
554 (*before converting an axiom clause to "clause" format, check if it is FOL*) |
586 (*before converting an axiom clause to "clause" format, check if it is FOL*) |
555 fun make_axiom_clause term (ax_name,cls_id) = |
587 fun make_axiom_clause term (ax_name,cls_id) = |
556 let val _ = check_is_fol_term term |
588 let val _ = check_is_fol_term term |
557 handle TERM("check_is_fol_term",_) => raise CLAUSE("Axiom is not FOL", term) |
589 handle TERM("check_is_fol_term",_) => raise CLAUSE("Axiom is not FOL", term) |
558 val (lits,types_sorts, preds,funcs) = literals_of_term term |
590 val (lits,types_sorts, preds,funcs) = literals_of_term term |
|
591 val lits' = sort_lits lits |
559 val (tvar_lits,tfree_lits, preds) = add_typs_aux types_sorts preds |
592 val (tvar_lits,tfree_lits, preds) = add_typs_aux types_sorts preds |
560 val tvars = get_tvar_strs types_sorts |
593 val tvars = get_tvar_strs types_sorts |
561 in |
594 in |
562 make_clause(cls_id,ax_name,Axiom, |
595 make_clause(cls_id,ax_name,Axiom, |
563 lits,types_sorts,tvar_lits,tfree_lits, |
596 lits',types_sorts,tvar_lits,tfree_lits, |
564 tvars, preds,funcs) |
597 tvars, preds,funcs) |
565 end; |
598 end; |
566 |
599 |
567 |
600 |
568 |
601 |
677 |
710 |
678 (*Only need to wrap equality's arguments with "typeinfo" if the output clauses are typed |
711 (*Only need to wrap equality's arguments with "typeinfo" if the output clauses are typed |
679 and if we specifically ask for types to be included. *) |
712 and if we specifically ask for types to be included. *) |
680 fun string_of_equality (typ,terms) = |
713 fun string_of_equality (typ,terms) = |
681 let val [tstr1,tstr2] = map string_of_term terms |
714 let val [tstr1,tstr2] = map string_of_term terms |
|
715 val typ' = string_of_fol_type typ |
682 in |
716 in |
683 if !keep_types andalso !special_equal |
717 if !keep_types andalso !special_equal |
684 then "equal(" ^ (wrap_eq_type typ tstr1) ^ "," ^ |
718 then "equal(" ^ (wrap_eq_type typ' tstr1) ^ "," ^ |
685 (wrap_eq_type typ tstr2) ^ ")" |
719 (wrap_eq_type typ' tstr2) ^ ")" |
686 else "equal(" ^ tstr1 ^ "," ^ tstr2 ^ ")" |
720 else "equal(" ^ tstr1 ^ "," ^ tstr2 ^ ")" |
687 end |
721 end |
688 and string_of_term (UVar(x,_)) = x |
722 and string_of_term (UVar(x,_)) = x |
689 | string_of_term (Fun("equal",[typ],terms)) = string_of_equality(typ,terms) |
723 | string_of_term (Fun("equal",[typ],terms)) = string_of_equality(typ,terms) |
690 | string_of_term (Fun (name,typs,[])) = name (*Overloaded consts like 0 don't get types!*) |
724 | string_of_term (Fun (name,typs,[])) = name (*Overloaded consts like 0 don't get types!*) |
691 | string_of_term (Fun (name,typs,terms)) = |
725 | string_of_term (Fun (name,typs,terms)) = |
692 let val terms_as_strings = map string_of_term terms |
726 let val terms_as_strings = map string_of_term terms |
693 val typs' = if !keep_types then typs else [] |
727 val typs' = if !keep_types then map string_of_fol_type typs else [] |
694 in name ^ (paren_pack (terms_as_strings @ typs')) end |
728 in name ^ (paren_pack (terms_as_strings @ typs')) end |
695 | string_of_term _ = error "string_of_term"; |
729 | string_of_term _ = error "string_of_term"; |
696 |
730 |
697 (* before output the string of the predicate, check if the predicate corresponds to an equality or not. *) |
731 (* before output the string of the predicate, check if the predicate corresponds to an equality or not. *) |
698 fun string_of_predicate (Predicate("equal",[typ],terms)) = string_of_equality(typ,terms) |
732 fun string_of_predicate (Predicate("equal",[typ],terms)) = string_of_equality(typ,terms) |
699 | string_of_predicate (Predicate(name,typs,terms)) = |
733 | string_of_predicate (Predicate(name,typs,terms)) = |
700 let val terms_as_strings = map string_of_term terms |
734 let val terms_as_strings = map string_of_term terms |
701 val typs' = if !keep_types then typs else [] |
735 val typs' = if !keep_types then map string_of_fol_type typs else [] |
702 in name ^ (paren_pack (terms_as_strings @ typs')) end |
736 in name ^ (paren_pack (terms_as_strings @ typs')) end |
703 | string_of_predicate _ = error "string_of_predicate"; |
737 | string_of_predicate _ = error "string_of_predicate"; |
704 |
738 |
705 |
739 |
706 fun string_of_clausename (cls_id,ax_name) = |
740 fun string_of_clausename (cls_id,ax_name) = |