logtk

Core types and algorithms for logic
IN THIS PACKAGE

TPTP Ast

type name =
| NameInt of int
| NameString of string(*

name of a formula

*)
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(*

formula role

*)
and optional_info = general_data list
and 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 -> role
val string_of_role : role -> string
val pp_role : role CCFormat.printer
val string_of_name : name -> string
val pp_name : name CCFormat.printer
val pp_general_debugf : general_data CCFormat.printer
val 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 list(*

top level declaration

*)
type 'a declaration = 'a t
val get_name : _ t -> name

Find the name of the declaration, or

  • raises Invalid_argument

    if the declaration is an include directive

IO

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