package dolmen

  1. Overview
  2. Docs
A parser library for automated deduction

Install

Dune Dependency

Authors

Maintainers

Sources

dolmen-0.8.tbz
sha256=3ee4b4b028b18ab0066cb4648fa14cd4d628a3afd79455f85fb796a9969ac80c
sha512=06d455f0221814dae44d9d8614cab7c1d4fb43a383e603a92ffc9cf4a753d42c5f2a0f3c5ae64aa6cf02da769c4666b130443ae2cf8fa0918c906d46e0caec9a

Description

Dolmen is a parser library. It currently targets languages used in automated theorem provers, but may be extended to other domains.

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 cna be used ot 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 for Linux and MacOs can be found on the release pages (starting from the v0.6 release, see the latest release).

The libraries can be installed using:

opam install dolmen dolmen_type dolmen_loop

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:

  • 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:

Dependencies (5)

  1. seq
  2. fmt >= "0.8.7"
  3. dune >= "3.0"
  4. menhir >= "20211230"
  5. ocaml >= "4.08" & != "5.0.0"

Dev Dependencies (3)

  1. mdx with-test
  2. qcheck with-test
  3. odoc with-doc

Used by (8)

  1. archsat < "1.1"
  2. colibri2 >= "0.4"
  3. colibrics >= "0.4"
  4. dolmen_bin = "0.8"
  5. dolmen_loop = "0.8"
  6. dolmen_lsp = "0.8"
  7. dolmen_model < "0.8.1"
  8. dolmen_type = "0.8"

Conflicts

None

OCaml

Innovation. Community. Security.