Dolmen doc

Dolmen

License

This code is free, under the BSD license.

Contents

Dolmen is a parser library, intended to considerably reduce the burden of having to parse different input languages. The main idea of dolmen is to provide an easy way to obtain a structured representation of an input, but not to completely abstract over the different input languages. Indeed, most languages are different enough that completeley abstracting over many of them would require specific encodings that would be detrimental to keeping the original structure of the input. Instead, the idea is to identify the core requirements of each language and provide easy way to obtain parsers for these languages when provided with an implementation that meets the requirements.

To that effect, dolmen mainly provides functors that take an adequate implementation of terms and top-level directives, and then return parsers for various languages.

Language classes

Some languages have enough similarities in either synatx or purpose to be packed into classes. Currently, the only class available is the Logic class that regroup languages used in formal proof.


Logic
Logic languages for formal proofs

The following modules synthesize the implementation requirements for language classes:


Id_intf
Interfaces for Identifiers.
Term_intf
Interfaces for Terms.
Stmt_intf
Interfaces for statements.
Location_intf
Interface for file locations.

Standard implementations

The following modules define standard implementations that can be used to directly instantiate the parser functors.


Id
Standard implementation of identifiers
Term
Standard implementation of terms
Statement
Standard imlplementation of statements.
ParseLocation
Standard implementation of file locations.

Language parsers

Individual language parsers are available through the following modules:


Dimacs
Dimacs language input
ICNF
iCNF language input
Smtlib
Smtlib language input
Tptp
TPTP language input
Zf
Zipperposition format input

These parsers all create modules with the following interface:


Language_intf
Interface for Dolmen languages modules

Index