67 type type_literal |
67 type type_literal |
68 val add_typs_aux2 : (typ_var * string list) list -> type_literal list * type_literal list |
68 val add_typs_aux2 : (typ_var * string list) list -> type_literal list * type_literal list |
69 val gen_tptp_cls : int * string * string * string -> string |
69 val gen_tptp_cls : int * string * string * string -> string |
70 val gen_tptp_type_cls : int * string * string * string * int -> string |
70 val gen_tptp_type_cls : int * string * string * string * int -> string |
71 val tptp_of_typeLit : type_literal -> string |
71 val tptp_of_typeLit : type_literal -> string |
|
72 |
72 end; |
73 end; |
73 |
74 |
74 structure ResClause: RES_CLAUSE = |
75 structure ResClause: RES_CLAUSE = |
75 struct |
76 struct |
76 |
77 |
686 and string_of_term (UVar(x,_)) = x |
687 and string_of_term (UVar(x,_)) = x |
687 | string_of_term (Fun("equal",[typ],terms)) = string_of_equality(typ,terms) |
688 | string_of_term (Fun("equal",[typ],terms)) = string_of_equality(typ,terms) |
688 | string_of_term (Fun (name,typs,[])) = name (*Overloaded consts like 0 don't get types!*) |
689 | string_of_term (Fun (name,typs,[])) = name (*Overloaded consts like 0 don't get types!*) |
689 | string_of_term (Fun (name,typs,terms)) = |
690 | string_of_term (Fun (name,typs,terms)) = |
690 let val terms_as_strings = map string_of_term terms |
691 let val terms_as_strings = map string_of_term terms |
691 in name ^ (paren_pack (terms_as_strings @ typs)) end |
692 val typs' = if !keep_types then typs else [] |
|
693 in name ^ (paren_pack (terms_as_strings @ typs')) end |
692 | string_of_term _ = error "string_of_term"; |
694 | string_of_term _ = error "string_of_term"; |
693 |
695 |
694 (* before output the string of the predicate, check if the predicate corresponds to an equality or not. *) |
696 (* before output the string of the predicate, check if the predicate corresponds to an equality or not. *) |
695 fun string_of_predicate (Predicate("equal",[typ],terms)) = string_of_equality(typ,terms) |
697 fun string_of_predicate (Predicate("equal",[typ],terms)) = string_of_equality(typ,terms) |
696 | string_of_predicate (Predicate(name,typs,terms)) = |
698 | string_of_predicate (Predicate(name,typs,terms)) = |
697 let val terms_as_strings = map string_of_term terms |
699 let val terms_as_strings = map string_of_term terms |
698 in name ^ (paren_pack (terms_as_strings @ typs)) end |
700 val typs' = if !keep_types then typs else [] |
|
701 in name ^ (paren_pack (terms_as_strings @ typs')) end |
699 | string_of_predicate _ = error "string_of_predicate"; |
702 | string_of_predicate _ = error "string_of_predicate"; |
700 |
703 |
701 |
704 |
702 fun string_of_clausename (cls_id,ax_name) = |
705 fun string_of_clausename (cls_id,ax_name) = |
703 clause_prefix ^ ascii_of ax_name ^ "_" ^ Int.toString cls_id; |
706 clause_prefix ^ ascii_of ax_name ^ "_" ^ Int.toString cls_id; |