package dolmen

  1. Overview
  2. Docs
A parser library that targets languages used in automated theorem provers

Install

Dune Dependency

Authors

Maintainers

Sources

dolmen-0.4.tar.gz
md5=6e23e37c0fd2de8d964a50f3de7ed2ed
sha512=ed6439256fbd6e6b3c0de70d0b7567503f4e898541106387fd8005d5c02c21b2391129ff0902e72355392bcf176617be77c80b9a823b5870475a599ed44fc030

Description

Dolmen is a parser library. It currently targets languages used in automated theorem provers, but may be extended ot 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 to instantiate its parsers.

README

Dolmen

A library providing flexible parsers for input languages.

LICENSE

BSD2, see file LICENSE.

Documentation

Online documentation can be found at http://gbury.github.io/dolmen. There is also a tutorial.

Build & Install

With opam:

opam pin add dolmen https://github.com/Gbury/dolmen.git

Manually:

make -C src
make -C src install

Current state

Currently the following parsers are working:

  • dimacs

  • iCNF

  • smtlib

  • tptp

  • zf (zipperposition format)

The following parsers are either work in progress, or soon to be work in progress:

  • coq

  • dedukti

Architecture

This library provides functors to create parsers from a given representation of terms. This allows users to have a parser that directly outputs temrs in the desired form, without needing to translate the parser output into the specific AST used in a project.

Parsers (actually, the functors which generates parsers) typically takes four module arguments:

  • A representation of locations in files. This is used for reporting parsing and lexing errors, but also to attach to each expression parsed its location.

  • A representation of identifiers. In some languages, there are syntactic scopes, which are handled using namespaces for variable names. In order to not pollute the Term module with it, the namespaces are dealt with in this module separately.

  • A representation of terms. The functions in this module are used by the parser to build the various types, terms and formulas corresponding to the grammar of the input language. All functions of this module typically takes as first (optional) argument a location (of the type defined by the previous argument) so that is is possible to have locations for expressions.

  • A representation of top-level directives. Languages usually defines several top-level directives to more easily distinguish type definitions, axioms, lemma, theorems to prove, new assertions, or even sometimes direct commands for the solver (to set some options for instance). Again, the functions in this module usually have a first optional argument to set the location of the directives.

Some simple implementation of theses modules are provided in this library. See the next section for more information.

Example

Examples of how to use the parsers can be found in src/main.ml . As mentionned in the previous section, default implementation for the required functor arguments are provided, and can be used.

For instance, the following code instantiates a parser for the smtlib language and try to parse a file named "example.smt2" in the home of the current user:


open Dolmen
module P = Smtlib.Make(ParseLocation)(Id)(Term)(Statement)

let _ = P.parse_file "~/example.smt2"

For more examples, see the tutorial.

Future work

  • Adding new languages

  • Improve error reporting

  • Dynamic detection of input language

Dependencies (3)

  1. dune < "1.10"
  2. menhir >= "20180523"
  3. ocaml >= "4.02.3" & != "5.0.0"

Dev Dependencies

None

Used by (2)

  1. archsat
  2. msat = "0.7"

Conflicts

None

OCaml

Innovation. Community. Security.