Legend:
Library
Module
Module type
Parameter
Class
Class type
Library
Module
Module type
Parameter
Class
Class type
package tptp
Legend:
Library
Module
Module type
Parameter
Class
Class type
Library
Module
Module type
Parameter
Class
Class type
AST for FOF and CNF formulas.
type tptp_input = | Fof_anno of fof_formula annotated_formula| Cnf_anno of cnf_formula annotated_formula| Include of file_name * formula_name list(*Empty list means that no selection was specified.
*)| Comment of comment_line
and 't annotated_formula = {af_name : formula_name;af_role : formula_role;af_formula : 't;af_annos : annotations option;
}Note: TPTP can distinguish between no useful info and empty useful info. But here are both represented by the empty list.
and atomic_word = | Plain_word of plain_word| Defined_word of defined_word| System_word of system_word
Note: Type atomic_word has no equivalent in TPTP. Type plain_word correspons to atomic_word from TPTP.
Alphanumeric characters include lowercase ('a'..'z') and uppercase ('A'..'Z') letters, digits ('0'..'9') and underscore.
Uppercase letter followed by zero or more alphanumeric characters.
In TPTP: variable.
Nonempty string which consists of ASCII characters from space to tilde.
In TPTP: atomic_word.
Dollar followed by lowercase letter and zero or more alphanumeric characters. Keywords ($fof, $cnf, $fot) are not allowed.
In TPTP: atomic_defined_word.
Two dollars followed by lowercase letter and zero or more alphanumeric characters.
In TPTP: atomic_system_word.
ASCII characters from space to tilde (empty string allowed).
In TPTP: distinct_object.
Printable ASCII characters (code >= 32 && code <= 126) or tabs (empty string allowed).
In TPTP: name.
and file_name = plain_wordand gdata = | G_func of plain_word * gterm list| G_var of var| G_number of Q.t| G_string of tptp_string| G_formula of gformula
val to_var : string -> varRaises Failure when the string is invalid.
val to_plain_word : string -> plain_wordRaises Failure when the string is invalid.
val to_defined_word : string -> defined_wordRaises Failure when the string is invalid.
val to_system_word : string -> system_wordRaises Failure when the string is invalid.
val to_tptp_string : string -> tptp_stringRaises Failure when the string is invalid.
val to_comment_line : string -> comment_lineRaises Failure when the string is invalid.
val tptp_input_equal : tptp_input -> tptp_input -> boolUseful when (=) causes stack overflow.