Module Logtk_parsers.Ast_tptp
TPTP Ast
type name=|NameInt of int|NameString of stringname of a formula
type role=|R_axiom|R_hypothesis|R_definition|R_assumption|R_lemma|R_theorem|R_conjecture|R_negated_conjecture|R_plain|R_finite of string|R_question|R_type|R_unknownformula role
type optional_info= general_data listtype general_data=|GString of string|GVar of string|GInt of int|GColumn of general_data * general_data|GNode of string * general_data list|GList of general_data list
val role_of_string : string -> roleval string_of_role : role -> stringval pp_role : role CCFormat.printerval string_of_name : name -> stringval pp_name : name CCFormat.printerval pp_general : general_data CCFormat.printerval pp_general_debugf : general_data CCFormat.printerval pp_generals : general_data list CCFormat.printer
type 'a t=|CNF of name * role * 'a list * optional_info|FOF of name * role * 'a * optional_info|TFF of name * role * 'a * optional_info|THF of name * role * 'a * optional_info|TypeDecl of name * string * 'a * optional_info|NewType of name * string * 'a * optional_info|Include of string|IncludeOnly of string * name listtop level declaration
type 'a declaration= 'a t
val get_name : _ t -> nameFind the name of the declaration, or
- raises Invalid_argument
if the declaration is an include directive