package dolmen

You can search for identifiers within the package.

in-package search v0.2.0

On This Page

Parameters
Signature

package dolmen

dolmen
- Dolmen
dolmen.ae
- Dolmen_ae
  - Id
  - Make
    
    I
    
    L
    
    Lexer
    
    Parser
    
    S
    
    T
  - Statement
  - Term
dolmen.class
- Dolmen_class
  - Logic
    
    Make
    
    E
    
    Smtlib2
    
    I
    
    L
    
    S
    
    Lexer
    
    Parser
    
    T
    
    S
    
    S
    
    Lexer
    
    Parser
  - Response
    
    Make
    
    I
    
    L
    
    S
    
    Lexer
    
    Parser
    
    T
    
    S
    
    S
    
    Lexer
    
    Parser
dolmen.dimacs
- Dolmen_dimacs
  - Make
    
    L
    
    Lexer
    
    Parser
    
    S
    
    T
  - Statement
  - Term
dolmen.icnf
- Dolmen_icnf
  - Make
    
    L
    
    Lexer
    
    Parser
    
    S
    
    T
  - Statement
  - Term
dolmen.intf
- Dolmen_intf
  - Ext
    
    Logic
    
    Smtlib2
  - Id
    
    Escape
    
    Logic
  - Language
    
    S
    
    Lexer
    
    Parser
  - Lex
    
    S
  - Location
    
    S
  - Map
    
    S
  - Msg
  - Parse
    
    S
  - Pretty
  - Stmt
    
    Logic
    
    Response
  - Tag
    
    Ae_Base
    
    S
    
    Smtlib_Base
    
    Zf_Base
  - Term
    
    Ae_Arith
    
    Int
    
    Real
    
    Ae_Arith_Common
    
    Ae_Array
    
    Ae_Base
    
    Ae_Bitv
    
    Dimacs
    
    Logic
    
    Smtlib_Arith_Common
    
    Smtlib_Array
    
    Smtlib_Base
    
    Smtlib_Bitv
    
    Smtlib_Bvconv
    
    Smtlib_Float
    
    Bitv
    
    Float
    
    Real
    
    Smtlib_Float_Bitv
    
    Smtlib_Float_Float
    
    Smtlib_Float_Real
    
    Smtlib_Int
    
    Smtlib_Real
    
    Smtlib_Real_Int
    
    Int
    
    Real
    
    Smtlib_String
    
    String
    
    RegLan
    
    Smtlib_String_RegLan
    
    Smtlib_String_String
    
    RegLan
    
    Tff
    
    Const
    
    Cstr
    
    Field
    
    Var
    
    Thf
    
    Const
    
    Cstr
    
    Field
    
    Var
    
    Tptp_Tff_Arith
    
    Int
    
    Rat
    
    Real
    
    Tptp_Tff_Arith_Common
    
    Tptp_Tff_Core
    
    Tptp_Thf_Core
    
    Const
    
    Tptp_Thf_Core_Const
    
    Zf_Arith
    
    Int
    
    Zf_Base
  - Tok
  - Ty
    
    Ae_Arith
    
    Ae_Array
    
    Ae_Base
    
    Ae_Bitv
    
    Smtlib_Array
    
    Smtlib_Base
    
    Smtlib_Bitv
    
    Smtlib_Float
    
    Smtlib_Int
    
    Smtlib_Real
    
    Smtlib_Real_Int
    
    Smtlib_String
    
    Tff
    
    Const
    
    Var
    
    Thf
    
    Const
    
    Var
    
    Tptp_Arith
    
    Tptp_Base
    
    Zf_Arith
    
    Zf_Base
dolmen.line
- Dolmen_line
dolmen.smtlib2
- Dolmen_smtlib2
  - Response
  - Script
dolmen.smtlib2.poly
- Dolmen_smtlib2_poly
  - Extension
  - Id
  - Make
    
    E
    
    I
    
    L
    
    Lexer
    
    Parser
    
    S
    
    T
  - Print
    
    L
    
    M
  - Statement
  - Term
dolmen.smtlib2.v6
- Dolmen_smtlib2_v6
dolmen.smtlib2.v6_response
- Dolmen_smtlib2_v6_response
  - Id
  - Make
    
    I
    
    L
    
    Lexer
    
    Parser
    
    S
    
    T
  - Statement
  - Term
dolmen.smtlib2.v6_script
- Dolmen_smtlib2_v6_script
  - Extension
  - Id
  - Make
    
    E
    
    I
    
    L
    
    Lexer
    
    Parser
    
    S
    
    T
  - Print
  - Statement
  - Term
dolmen.std
- Dolmen_std
  - Answer
  - Builtin
  - Escape
    
    Make
    
    Id
  - Expr
    
    Id
    
    Print
    
    Subst
    
    S
    
    Var
    
    Tags
    
    Term
    
    Array
    
    Bitv
    
    Const
    
    Array
    
    Bitv
    
    Float
    
    Int
    
    Rat
    
    Real
    
    String
    
    Reg_Lang
    
    Cstr
    
    Field
    
    Float
    
    Int
    
    Rat
    
    Real
    
    String
    
    RegLan
    
    Var
    
    Ty
    
    Const
    
    Var
  - Extensions
    
    Smtlib2
  - Id
    
    Map
  - Loc
  - Maps
    
    Int
    
    Make
    
    String
  - Maps_string
  - Misc
  - Msg
  - Name
    
    Map
  - Namespace
    
    Map
  - Normalize
    
    Smtlib
    
    Tptp
  - Path
  - Pretty
  - Statement
  - Stats
    
    Float
    
    Floats
  - Tag
  - Term
  - Timer
  - Tok
  - Transformer
    
    Make
    
    Lex
    
    Loc
    
    Parse
    
    Ty
  - Vec
dolmen.tptp
- Dolmen_tptp
dolmen.tptp.v6_3_0
- Dolmen_tptp_v6_3_0
  - Id
  - Make
    
    I
    
    L
    
    Lexer
    
    Parser
    
    S
    
    T
  - Statement
  - Term
dolmen.zf
- Dolmen_zf
  - Id
  - Make
    
    I
    
    L
    
    Lexer
    
    Parser
    
    S
    
    T
  - Statement
  - Term

Legend:
Library
Module
Module type
Parameter
Class
Class type

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

module E : 
  Dolmen_intf.Ext.Logic
    with type location := L.t
     and type term := T.t
     and type statement := S.t

Signature

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_all : 
  ?language:language ->
  [< `File of string
  | `Stdin of language
  | `Raw of string * language * string ] ->
  language * L.file * S.t list Stdlib.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.

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, stdin (with given language), or some arbitrary contents, of the form `Raw (filename, language, contents). Returns a quadruplet (lan, file, gen, cl), containing:

the language lan detected
a file value that stores the metadata about file locations
a genrator function gen for parsing the input,
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")

raises Extension_not_found
when the extension is not recognized.