package dolmen

  1. Overview
  2. Docs
package dolmen
Legend:
Library
Module
Module type
Parameter
Class
Class type

Parameters

module T : Dolmen_intf.Term.Logic with type location := L.t and type id := I.t
module S : Dolmen_intf.Stmt.Logic with type location := L.t and type id := I.t and type term := T.t

Signature

exception Extension_not_found of string

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

Supported languages

type language =
  1. | Alt_ergo
    (*

    Alt-ergo's native language

    *)
  2. | Dimacs
    (*

    Dimacs CNF format

    *)
  3. | ICNF
    (*

    iCNF format

    *)
  4. | Smtlib2 of Dolmen_smtlib2.version
    (*

    Smtlib v2 latest version

    *)
  5. | Tptp of Dolmen_tptp.version
    (*

    TPTP format (including THF), latest version

    *)
  6. | 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 * L.file * S.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 * L.file * S.t list Stdlib.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 * L.file * (unit -> S.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 := S.t and type file := L.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")

OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct