package dolmen

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.

• Dolmen_class.Logic Logic languages for formal proofs

The following modules synthesize the implementation requirements for language classes:

• Dolmen_intf.Id Interfaces 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.Term Interfaces 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.Stmt Interfaces for statements. This module defines interfaces for statements, i.e top-level declarations in files.
• Dolmen_intf.Location Interface 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.

Standard implementations

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

• Dolmen_std.Id Standard implementation of identifiers
• Dolmen_std.Term Standard implementation of terms
• Dolmen_std.Normalize Normalizing functions
• Dolmen_std.Statement Standard 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.
• Dolmen_std.ParseLocation

Language parsers

Individual language parsers are available through the following modules:

• Dolmen_dimacs Dimacs language input
• Dolmen_icnf iCNF language input
• Dolmen_smtlib2
• Dolmen_tptp
• Dolmen_zf Zipperposition format input

These parsers all create modules with the following interface:

• Dolmen_intf.Language Interface for Dolmen languages modules

Index

indexlist