package dolmen
Install
Dune Dependency
Authors
Maintainers
Sources
sha256=c5c85f77e3924f378e8d82f166eefe4131b4e041bf9cdeca467410f33c71fa61
sha512=42feb39d13cfdc8a2054abe85ccc47755f45059cda7d95e9261b5a9fd5c730f420732547b3fa19c4af059474f887ef78c119ab5933375a5ea2dbe888f65a3e4f
Description
Dolmen aims at providing tools to help in writing programs in the field of theorem proving, SMT solving, and model checking. The project includes a few libraries, a CLI binary and an LSP server, split over several opam packages.
This is the Dolmen parser library. It currently targets languages used in automated theorem provers, as well as model checking, and may be extended to other domains later.
Dolmen provides functors that takes as arguments a representation of terms and statements, and returns a module that can parse files (or streams of tokens) into the provided representation of terms or statements. This is meant so that Dolmen can be used as a drop-in replacement of existing parser, in order to factorize parsers among projects.
Additionally, Dolmen also provides a standard implementation of terms and statements that can be used to instantiate its parsers.
README
Dolmen
A library providing flexible parsers and typecheckers for languages used in automated deduction.
LICENSE
BSD2, see file LICENSE.
Documentation
Online documentation for the libraries can be found at http://gbury.github.io/dolmen. There is also a tutorial.
Installation
The main method of installation is to use opam. See this page for information about how to install opam on your system. Once you have installed and configured opam, you can use the following command to install the dolmen cli and lsp binaries:
opam install dolmen_bin dolmen_lsp
Additionally, pre-built binaries can be found on the release pages (starting from the v0.6 release for Linux and MacOS, and starting from the v0.8.1 release for Windows). You can get them on the latest release page.
The libraries can be installed using:
opam install dolmen dolmen_type dolmen_loop dolmen_model
Goals
The Dolmen project aims at providing an assortiment of tools to help handle languages that are used in automated deduction and formal logic.
More precisely, the Dolmen project provides:
A few OCaml libraries for:
parsing, see the parsing doc
typechecking, see the typing doc
writing main loops for binaries, the loop doc
A binary (which is using the above libraries), to parse and typecheck input files. This could be used to check a file against its language specification, and/or obtain detailed errors. See the bin doc
A LSP server so that the features of the above binary can also be used inside your favorite editor. See the dolmen lsp doc
Supported languages
| Language | Parsing | Typing | Model verification |
|---|---|---|---|
| ae (alt-ergo) | :heavy_check_mark: | :heavy_check_mark: | |
| dimacs | :heavy_check_mark: | :heavy_check_mark: | |
| iCNF | :heavy_check_mark: | :heavy_check_mark: | |
| smtlib | :heavy_check_mark: | :heavy_check_mark: | :heavy_check_mark: |
| tptp | :heavy_check_mark: | :heavy_check_mark: | |
| zf (zipperposition) | :heavy_check_mark: | :heavy_check_mark: |
Acknowledgements
This work is currently in part funded by OCamlPro
Dependencies (6)
Used by (8)
-
alt-ergo-lib
>= "2.6.0" -
archsat
< "1.1" -
dolmen_bin
>= "0.10" -
dolmen_loop
>= "0.10" -
dolmen_lsp
>= "0.10" -
dolmen_model
>= "0.10" -
dolmen_type
>= "0.10" -
smtml
>= "0.3.1"
Conflicts
None