package dolmen
Install
Dune Dependency
Authors
Maintainers
Sources
sha256=81b034da2de84da19fb6368aaa39135f6259ee2773ff08c8f03da9ceeb10748c
sha512=98786ff1cc5b0c8bc4cb2dfe756ae15556c3876a206546b04374826be7d0a422dd5526d93f09cb0ea0d4985b71c408c182a951d4df908399c7e04b17c91a7d70
doc/dolmen_smtlib2_v6/Dolmen_smtlib2_v6/Make/index.html
Module Dolmen_smtlib2_v6.MakeSource
Functor to generate a parser for the Smtlib format.
Parameters
module L : Dolmen_intf.Location.SSignature
type statement = S.tThe type of top-level directives recognised by the parser.
module Lexer : Dolmen_intf.Lex.S with type token := tokenThe 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.