Functor Tptp.Make

module Make: functor (L : ParseLocation.S) -> functor (I : Id) -> functor (T : Term  with type location := L.t and type id := I.t) -> functor (S : Statement  with type location := L.t and type id := I.t and type term := T.t) -> Language_intf.S  with type statement = S.t

Functor to generate a parser for the TPTP format.

Parameters:

`L`	:	`ParseLocation.S`
`I`	:	`Id`
`T`	:	`Term with type location := L.t and type id := I.t`
`S`	:	`Statement with type location := L.t and type id := I.t and type term := T.t`

type token

The type of tokens produced by the language lexer.

type statement

The type of top-level directives recognised by the parser.

module Lexer: Lex_intf.S 
    with type token := token

The Lexer module for the language.

module Parser: Parse_intf.S 
    with type token := token
     and type statement := statement

The Parser module for the language.

val find : ?dir:string -> string -> string option

Helper function to find a file using a language specification. Separates directory and file because most include directives in languages are relative to the directory of the original file being processed.

val parse_file : string -> statement list

Parse the given file.

val parse_input : [ `File of string | `Stdin ] -> unit -> statement option

Incremental parsing. Given an input to read (either a file, or stdin), returns a generator that will incrementally parse the statements. In case of a syntax error, the current line will be completely consumed and parsing will restart at the beginning of the next line. Useful to process input from stdin, or even large files where it would be impractical to parse the entire file before processing it.