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.

• 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:

• Language_intf

Index

indexlist