Module `Logic.Make`Source

Parameters

module L : Dolmen_intf.Location.S

module I : Dolmen_intf.Id.Logic

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

Sourceexception Extension_not_found of string

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

Supported languages

Sourcetype language =

| Alt_ergo
(*
Alt-ergo's native language
*)
| Dimacs
(*
Dimacs CNF format
*)
| ICNF
(*
iCNF format
*)
| Smtlib2 of Dolmen_smtlib2.Script.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.

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_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.

Source

val parse_file_lazy : 
  ?language:language ->
  string ->
  language * L.file * S.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.

Source

val parse_raw_lazy : 
  ?language:language ->
  filename:string ->
  string ->
  language * L.file * S.t list Lazy.t

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

parameter language
specify a language; overrides auto-detection.

Source

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

Source

module 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")

raises Extension_not_found
when the extension is not recognized.

Install

Dune Dependency

Authors

Maintainers

Sources

doc/dolmen.class/Dolmen_class/Logic/Make/index.html

Module `Logic.Make`Source

Parameters

Signature

Supported languages

High-level parsing

Mid-level parsing

package dolmen

Install

Dune Dependency

Authors

Maintainers

Sources

doc/dolmen.class/Dolmen_class/Logic/Make/index.html

Module Logic.MakeSource

Parameters

Signature

Supported languages

High-level parsing

Mid-level parsing

Module `Logic.Make`Source