package dolmen_loop

You can search for identifiers within the package.

in-package search v0.2.0

Package contains no libraries

This is an instanciation of the Logic class with the standard implementation of parsed terms and statements of Dolmen.

include Dolmen.Class.Logic.S
  with type statement := Dolmen.Std.Statement.t
   and type file := Dolmen.Std.Loc.file

exception Extension_not_found of string

Raised when trying to find a language given a file extension.

Supported languages

type language =

| Alt_ergo
(*
Alt-ergo's native language
*)
| Dimacs
(*
Dimacs CNF format
*)
| ICNF
(*
iCNF format
*)
| Smtlib2 of Dolmen_smtlib2.version
(*
Smtlib v2 latest version
*)
| Tptp of Dolmen_tptp.version
(*
TPTP format (including THF), latest version
*)
| Zf
(*
Zipperposition format
*)

The languages supported by the Logic class.

val enum : (string * language) list

Enumeration of languages together with an appropriate name. Can be used for command-line arguments (for instance, with cmdliner).

val string_of_language : language -> string

String representation of the variant

High-level parsing

val find : ?language:language -> ?dir:string -> string -> string option

Tries and find the given file, using the language specification.

val parse_file : 
  ?language:language ->
  string ->
  language * Dolmen.Std.Loc.file * Dolmen.Std.Statement.t list

Given a filename, parse the file, and return the detected language together with the list of statements parsed.

parameter language
specify a language; overrides auto-detection.

val parse_file_lazy : 
  ?language:language ->
  string ->
  language * Dolmen.Std.Loc.file * Dolmen.Std.Statement.t list Lazy.t

Given a filename, parse the file, and return the detected language together with the list of statements parsed.

parameter language
specify a language; overrides auto-detection.

val parse_input : 
  ?language:language ->
  [< `File of string
  | `Stdin of language
  | `Raw of string * language * string ] ->
  language
  * Dolmen.Std.Loc.file
  * (unit ->
  Dolmen.Std.Statement.t option)
  * (unit ->
  unit)

Incremental parsing of either a file (see parse_file), stdin (with given language), or some arbitrary contents, of the form `Raw (filename, language, contents). Returns a triplet (lan, gen, cl), containing the language detexted lan, a genratro function gen for parsing the input, and a cleanup function cl to call in order to cleanup the file descriptors.

parameter language
specify a language for parsing, overrides auto-detection and stdin specification.

Mid-level parsing

module type S =
  Dolmen_intf.Language.S
    with type statement := Dolmen.Std.Statement.t
     and type file := Dolmen.Std.Loc.file

The type of language modules.

val of_language : language -> language * string * (module S)

val of_extension : string -> language * string * (module S)

val of_filename : string -> language * string * (module S)

These function take as argument either a language, a filename, or an extension, and return a triple:

language
language file extension (starting with a dot)
appropriate parsing module

Extensions should start with a dot (for instance : ".smt2")

raises Extension_not_found
when the extension is not recognized.