This code is free, under the BSD license.
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.
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.
Dolmen_class.LogicLogic languages for formal proofs
The following modules synthesize the implementation requirements for language classes:
Dolmen_intf.IdInterfaces for Identifiers. This module defines Interfaces that implementation of identifiers must respect in order to be used to instantiated the corresponding language classes.
Dolmen_intf.TermInterfaces for Terms. This module defines Interfaces that implementation of terms must respect in order to be used to instantiated the corresponding language classes.
Dolmen_intf.StmtInterfaces for statements. This module defines interfaces for statements, i.e top-level declarations in files.
Dolmen_intf.LocationInterface for file locations. This module defines an interface to store locations in files. These locations are used by the parsers to specify the locations of all parsed expressions whenever it is possible. This interface also requires some exceptions to be defined. These exceptions make use of locations to specify at which point in the file the parsing went wrong.
The following modules define standard implementations that can be used to directly instantiate the parser functors.
Dolmen_std.IdStandard implementation of identifiers
Dolmen_std.TermStandard implementation of terms
Dolmen_std.StatementStandard imlplementation of statements. This module provides a reasonable and standard implementation of statements, that can directly be used to instantiated the various functors of the dolmen library. These statements are closer to smtlib statements than to other languages statements because it is easier to express other languages statements using smtlib's than the other way around. Still, a generalisation of smtlib statements was needed so as not to lose some important distinctions between conjectures and assertions for instance.
Individual language parsers are available through the following modules:
Dolmen_dimacsDimacs language input
Dolmen_icnfiCNF language input
Dolmen_zfZipperposition format input
These parsers all create modules with the following interface:
Dolmen_intf.LanguageInterface for Dolmen languages modules