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

Reading and writing FOF and CNF formulas in TPTP format.

Note 1: This library supports only FOF and CNF formulas. Keywords and other constructions used for representation of other formulas are not supported. This besides other things means that strings "thf", "tff", "$thf" and "$tff" are not treated as keywords and can be used as ordinary functors (for example to_defined_word "$thf" does not fail).

Note 2: Comment lines can contain tabs. Comment blocks can contain non-printable characters and non-ASCII characters.

Note 3: Comment blocks are ignored and comment lines inside formulas are ignored too.

exception Input_closed

exception Parse_error of Stdlib.Lexing.position * string

exception Include_error of Stdlib.Lexing.position * string

type input

val create_in : Stdlib.Lexing.lexbuf -> input

val read : input -> Tptp_ast.tptp_input option

Returns None when EOF is reached.

Raises Input_closed when input was closed. Raises Parse_error when input contains syntax error.

val close_in : input -> unit

val write : 
  ?rfrac:float ->
  ?width:int ->
  Stdlib.Buffer.t ->
  Tptp_ast.tptp_input ->
  unit

The parameter width is the maximum number of characters per line. The parameter rfrac is the ribbon width, a fraction relative to width. The ribbon width is the maximum number of non-indentation characters per line.

val to_string : Tptp_ast.tptp_input -> string

module File : sig ... end