package dolmen

  1. Overview
  2. Docs

Module Response.MakeSource

Parameters

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

Signature

Sourceexception Extension_not_found of string

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

Supported languages

Sourcetype language =
  1. | Smtlib2 of Dolmen_smtlib2.Response.version
    (*

    Smtlib v2 latest version

    *)

The languages supported by the Response class.

Sourceval enum : (string * language) list

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

Sourceval string_of_language : language -> string

String representation of the variant

High-level parsing

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

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

Sourceval parse_all : ?language:language -> [< `File of string | `Stdin of language | `Raw of string * language * string ] -> language * L.file * S.t list Lazy.t

Full (but lazy) 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, file, stmts), containing:

  • the language lan detected
  • a file value that stores the metadata about file locations
  • a lazy list of statements stmts; forcing this list will run the actual parsing of the whole input given as argument, and may raise errors, if any arises during the parsing (such as lexical errors, etc..)
  • parameter language

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

Sourceval 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

Sourcemodule type S = Dolmen_intf.Language.S with type statement := S.t and type file := L.file

The type of language modules.

Sourceval of_language : language -> language * string * (module S)
Sourceval of_extension : string -> language * string * (module S)
Sourceval 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")