package dolmen_loop

You can search for identifiers within the package.

in-package search v0.2.0

dolmen_loop
- Dolmen_loop
  - Code
  - Expr_intf
    
    Print
    
    S
  - Headers
    
    Field
    
    Make
    
    S
  - Headers_intf
    
    S
  - Logic
    
    S
    
    Lexer
    
    Parser
  - Parser
    
    Make
    
    State
  - Parser_intf
    
    S
  - Pipeline
    
    Make
    
    State
  - Report
    
    Conf
    
    Error
    
    T
    
    Warning
    
    Status
  - Response
    
    P
    
    S
    
    Lexer
    
    Parser
    
    S
    
    Lexer
    
    Parser
  - State
    
    M
    
    S
  - Typer
    
    Make
    
    Expr
    
    Print
    
    State
    
    Typer
    
    T
    
    T
    
    Const
    
    Cstr
    
    Field
    
    Var
    
    Tag
    
    Ty
    
    Const
    
    Var
    
    Typer
    
    State
  - Typer_intf
    
    S
    
    Typer
    
    Typer_Full
    
    Types

Legend:
Library
Module
Module type
Parameter
Class
Class type

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

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