package dolmen
Functor to generate a parser for the TPTP format.
Parameters
module L : Dolmen_intf.Location.S
Signature
type statement = S.t
The type of top-level directives recognised by the parser.
module Lexer : Dolmen_intf.Lex.S with type token := token
The Lexer module for the language.
The Parser module for the language.
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_input :
[ `Stdin | `File of string | `Contents of string * string ] ->
L.file * (unit -> statement option) * (unit -> unit)
Incremental parsing. Given an input to read (either a file, stdin, or some contents of the form (filename, s)
where s
is the contents to parse), returns a generator that will incrementally parse the statements, together with a cleanup function to close file descriptors. 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.