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
    
    Incremental
    
    MenhirInterpreter
    
    S
    
    T
  - Statement
  - Term
dolmen.class
- Dolmen_class
  - Logic
    
    Make
    
    I
    
    L
    
    S
    
    Lexer
    
    Parser
    
    Incremental
    
    MenhirInterpreter
    
    T
    
    S
    
    S
    
    Lexer
    
    Parser
    
    Incremental
    
    MenhirInterpreter
dolmen.dimacs
- Dolmen_dimacs
  - Make
    
    L
    
    Lexer
    
    Parser
    
    Incremental
    
    MenhirInterpreter
    
    S
    
    T
  - Statement
  - Term
dolmen.icnf
- Dolmen_icnf
  - Make
    
    L
    
    Lexer
    
    Parser
    
    Incremental
    
    MenhirInterpreter
    
    S
    
    T
  - Statement
  - Term
dolmen.intf
- Dolmen_intf
  - Id
    
    Escape
    
    Logic
  - Language
    
    S
    
    Lexer
    
    Parser
    
    Incremental
    
    MenhirInterpreter
  - Lex
    
    S
  - Location
    
    S
  - Msg
  - Parse
    
    S
    
    Incremental
    
    MenhirInterpreter
  - Stmt
    
    Logic
  - Tag
    
    S
    
    Smtlib_Base
    
    Zf_Base
  - Term
    
    Ae_Arith
    
    Ae_Base
    
    Logic
    
    Smtlib_Arith_Common
    
    Smtlib_Array
    
    Smtlib_Base
    
    Smtlib_Bitv
    
    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
    
    Tptp_Arith
    
    Int
    
    Rat
    
    Real
    
    Tptp_Arith_Common
    
    Tptp_Base
  - Tok
  - Ty
    
    Ae_Arith
    
    Ae_Base
    
    Smtlib_Array
    
    Smtlib_Base
    
    Smtlib_Bitv
    
    Smtlib_Float
    
    Smtlib_Int
    
    Smtlib_Real
    
    Smtlib_Real_Int
    
    Smtlib_String
    
    Tff
    
    Const
    
    Var
    
    Tptp_Arith
    
    Tptp_Base
dolmen.line
- Dolmen_line
dolmen.smtlib2
- Dolmen_smtlib2
dolmen.smtlib2.poly
- Dolmen_smtlib2_poly
  - Id
  - Make
    
    I
    
    L
    
    Lexer
    
    Parser
    
    Incremental
    
    MenhirInterpreter
    
    S
    
    T
  - Statement
  - Term
dolmen.smtlib2.v6
- Dolmen_smtlib2_v6
  - Id
  - Make
    
    I
    
    L
    
    Lexer
    
    Parser
    
    Incremental
    
    MenhirInterpreter
    
    S
    
    T
  - Statement
  - Term
dolmen.std
- Dolmen_std
  - Escape
    
    Make
    
    Id
  - Expr
    
    Filter
    
    S
    
    Id
    
    Print
    
    Subst
    
    S
    
    Var
    
    Tags
    
    Term
    
    Bitv
    
    Const
    
    Cstr
    
    Field
    
    Float
    
    Int
    
    Rat
    
    Real
    
    String
    
    RegLan
    
    Var
    
    Ty
    
    Const
    
    Var
  - Id
  - Loc
  - Misc
  - Msg
  - Normalize
    
    Smtlib
    
    Tptp
  - Pretty
  - Statement
  - Tag
  - Term
  - Tok
  - Transformer
    
    Make
    
    Lex
    
    Loc
    
    Parse
    
    Incremental
    
    MenhirInterpreter
    
    Ty
  - Vec
dolmen.tptp
- Dolmen_tptp
dolmen.tptp.v6_3_0
- Dolmen_tptp_v6_3_0
  - Id
  - Make
    
    I
    
    L
    
    Lexer
    
    Parser
    
    Incremental
    
    MenhirInterpreter
    
    S
    
    T
  - Statement
  - Term
dolmen.zf
- Dolmen_zf
  - Id
  - Make
    
    I
    
    L
    
    Lexer
    
    Parser
    
    Incremental
    
    MenhirInterpreter
    
    S
    
    T
  - Statement
  - Term

Legend:
Library
Module
Module type
Parameter
Class
Class type

Functor to generate a parser for the iCNF format.

Parameters

module L : Dolmen_intf.Location.S

module T : Term with type location := L.t

module S : Statement with type location := L.t and type term := T.t

Signature

type token

The type of tokens produced by the language lexer.

type statement = S.t

The type of top-level directives recognised by the parser.

module Lexer : Dolmen_intf.Lex.S with type token := token

The Lexer module for the language.

module Parser : 
  Dolmen_intf.Parse.S with type token := token and type statement := statement

The Parser module for the language.

val find : ?dir:string -> string -> string option

Helper function to find a file using a language specification. Separates directory and file because most include directives in languages are relative to the directory of the original file being processed.

val parse_file : string -> L.file * statement list

Parse the given file.

parameter dir:
optional directory to use if the file path is relative.

val parse_file_lazy : string -> L.file * statement list Lazy.t

Parse the given file.

parameter dir:
optional directory to use if the file path is relative.

val parse_input : 
  [ `Stdin | `File of string | `Contents of string * string ] ->
  L.file * (unit -> statement option) * (unit -> unit)

Incremental parsing. Given an input to read (either a file, stdin, or some contents of the form (filename, s) where s is the contents to parse), returns a generator that will incrementally parse the statements, together with a cleanup function to close file descriptors. In case of a syntax error, the current line will be completely consumed and parsing will restart at the beginning of the next line. Useful to process input from stdin, or even large files where it would be impractical to parse the entire file before processing it.