package tptp

You can search for identifiers within the package.

in-package search v0.2.0

tptp
- Tptp
  - File
- Tptp_ast
- Tptp_lexer
- Tptp_parser
- Tptp_printer

Legend:
Library
Module
Module type
Parameter
Class
Class type

type tptp_input =

| Fof_anno of fof_formula annotated_formula
| Cnf_anno of cnf_formula annotated_formula
| Include of file_name * formula_name list
| Comment of comment_line

and !'t annotated_formula = {

af_name : formula_name;
af_role : formula_role;
af_formula : 't;
af_annos : annotations option;

}

and annotations = {

a_source : gterm;
a_useful_info : gterm list;

}

and formula_role =

| R_axiom
| R_hypothesis
| R_definition
| R_assumption
| R_lemma
| R_theorem
| R_corollary
| R_conjecture
| R_negated_conjecture
| R_plain
| R_fi_domain
| R_fi_functors
| R_fi_predicates
| R_type
| R_unknown

and fof_formula =

| Sequent of formula list * formula list
| Formula of formula

and formula =

| Binop of binop * formula * formula
| Not of formula
| Quant of quant * var * formula
| Atom of atom

and binop =

| Equiv
| Implies
| Implies_rev
| Xor
| Nor
| Nand
| Or
| And

and quant =

| All
| Exists

and cnf_formula =

| Clause of literal list

and literal =

| Lit of sign * atom

and sign =

| Pos
| Neg

and atom =

| Equals of term * term
| Pred of atomic_word * term list

and term =

| Var of var
| Func of atomic_word * term list
| Number of Q.t
| String of tptp_string

and atomic_word =

| Plain_word of plain_word
| Defined_word of defined_word
| System_word of system_word

and var = private string

and plain_word = private string

and defined_word = private string

and system_word = private string

and tptp_string = private string

and comment_line = private string

and formula_name =

| N_word of plain_word
| N_integer of Z.t

and file_name = plain_word

and gterm =

| G_data of gdata
| G_cons of gdata * gterm
| G_list of gterm list

and 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

and gformula =

| G_fof of fof_formula
| G_cnf of cnf_formula
| G_fot of term

val to_var : string -> var

val to_plain_word : string -> plain_word

val to_defined_word : string -> defined_word

val to_system_word : string -> system_word

val to_tptp_string : string -> tptp_string

val to_comment_line : string -> comment_line