Module Logtk_parsers.Ast_tptpSource

TPTP Ast

Sourcetype name =
  1. | NameInt of int
  2. | NameString of string
    (*

    name of a formula

    *)
Sourceand role =
  1. | R_axiom
  2. | R_hypothesis
  3. | R_definition
  4. | R_assumption
  5. | R_lemma
  6. | R_theorem
  7. | R_conjecture
  8. | R_negated_conjecture
  9. | R_plain
  10. | R_finite of string
  11. | R_question
  12. | R_type
  13. | R_unknown
    (*

    formula role

    *)
Sourceand optional_info = general_data list
Sourceand general_data =
  1. | GString of string
  2. | GVar of string
  3. | GInt of int
  4. | GColumn of general_data * general_data
  5. | GNode of string * general_data list
  6. | GList of general_data list
Sourceval role_of_string : string -> role
Sourceval string_of_role : role -> string
Sourceval string_of_name : name -> string
Sourceval pp_general_debugf : general_data CCFormat.printer
Sourceval pp_generals : general_data list CCFormat.printer
Sourcetype 'a t =
  1. | CNF of name * role * 'a list * optional_info
  2. | FOF of name * role * 'a * optional_info
  3. | TFF of name * role * 'a * optional_info
  4. | THF of name * role * 'a * optional_info
  5. | TypeDecl of name * string * 'a * optional_info
  6. | NewType of name * string * 'a * optional_info
  7. | Include of string
  8. | IncludeOnly of string * name list
    (*

    top level declaration

    *)
Sourcetype 'a declaration = 'a t
Sourceval get_name : _ t -> name

Find the name of the declaration, or

IO

include Logtk.Interfaces.PRINT1 with type 'a t := 'a t
Sourceval to_string : 'a CCFormat.printer -> 'a t -> string