Legend:
Library
Module
Module type
Parameter
Class
Class type
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
The following modules synthesize the implementation requirements for language classes:
Id_intf
Term_intf
Stmt_intf
Location_intf
Standard implementations
The following modules define standard implementations that can be used to directly instantiate the parser functors.
Id
Term
Normalize
Statement
ParseLocation
Language parsers
Individual language parsers are available through the following modules:
Dimacs
ICNF
Smtlib
Tptp
Zf
These parsers all create modules with the following interface: