package dolmen

You can search for identifiers within the package.

in-package search v0.2.0

A parser library for automated deduction

Install

Dune Dependency

github.com Readme Changelog Edit opam file Versions (11)

Authors

G

Guillaume Bury <guillaume.bury@gmail.com>

Maintainers

G

Guillaume Bury <guillaume.bury@gmail.com>

Sources

dolmen-0.8.1.tbz

sha256=80fc33ae81817a79c6e6b2f6c01c4cfcc0af02bfe4d2d1b87cf70b84cdde3928

sha512=3a44a99bce871161bc70cf909c813e9e6c91c590873cbc163c69b2ec90ab5be65bf0bf45430bc8d00d85d75cf0af004b06b8f5f1c9d4d47c8a30ab9f28762c04

doc/dolmen_smtlib2_poly/Dolmen_smtlib2_poly/Make/index.html

Module `Dolmen_smtlib2_poly.Make`Source

Functor to generate a parser for the Smtlib format.

Parameters

module L : Dolmen_intf.Location.S

module I : Id

module T : Term with type location := L.t and type id := I.t

module S : Statement with type location := L.t and type id := I.t and type term := T.t

Signature

type token

The type of tokens produced by the language lexer.

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.

module Parser : 
  Dolmen_intf.Parse.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 -> L.file * statement list

Parse the whole given file into a list.

val parse_file_lazy : string -> L.file * statement list Lazy.t

Parse the whole given file into a list.

val parse_raw_lazy : 
  filename:string ->
  string ->
  L.file * statement list Lazy.t

Parse the whole given string into a list.

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.

On This Page

Parameters
Signature

package dolmen

Install

Dune Dependency

Authors

Maintainers

Sources

doc/dolmen_smtlib2_poly/Dolmen_smtlib2_poly/Make/index.html

Module Dolmen_smtlib2_poly.MakeSource

Parameters

Signature

Module `Dolmen_smtlib2_poly.Make`Source