sig
  type name = NameInt of int | NameString of string
  and 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_unknown
  and optional_info = Ast_tptp.general_data list
  and general_data =
      GString of string
    | GVar of string
    | GInt of int
    | GColumn of Ast_tptp.general_data * Ast_tptp.general_data
    | GNode of string * Ast_tptp.general_data list
    | GList of Ast_tptp.general_data list
  val role_of_string : string -> Ast_tptp.role
  val string_of_role : Ast_tptp.role -> string
  val pp_role : Ast_tptp.role CCFormat.printer
  val string_of_name : Ast_tptp.name -> string
  val pp_name : Ast_tptp.name CCFormat.printer
  val pp_general : Ast_tptp.general_data CCFormat.printer
  val pp_general_debugf : Ast_tptp.general_data CCFormat.printer
  val pp_generals : Ast_tptp.general_data list CCFormat.printer
  type 'a t =
      CNF of Ast_tptp.name * Ast_tptp.role * 'a list * Ast_tptp.optional_info
    | FOF of Ast_tptp.name * Ast_tptp.role * 'a * Ast_tptp.optional_info
    | TFF of Ast_tptp.name * Ast_tptp.role * 'a * Ast_tptp.optional_info
    | THF of Ast_tptp.name * Ast_tptp.role * 'a * Ast_tptp.optional_info
    | TypeDecl of Ast_tptp.name * string * 'a * Ast_tptp.optional_info
    | NewType of Ast_tptp.name * string * 'a * Ast_tptp.optional_info
    | Include of string
    | IncludeOnly of string * Ast_tptp.name list
  type 'a declaration = 'a Ast_tptp.t
  val get_name : 'a Ast_tptp.t -> Ast_tptp.name
  val pp : 'a CCFormat.printer -> 'a t CCFormat.printer
  val to_string : 'a CCFormat.printer -> 'a t -> string
end