package dolmen

You can search for identifiers within the package.

in-package search v0.2.0

On This Page

Interface definition
Concrete positions
Lexbuf

package dolmen

dolmen
- Dolmen
  - Intf
dolmen.class
- Dolmen_class
  - Logic
    
    Make
    
    I
    
    L
    
    S
    
    Lexer
    
    Parser
    
    Incremental
    
    MenhirInterpreter
    
    T
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
    
    Logic
  - Language
    
    S
    
    Lexer
    
    Parser
    
    Incremental
    
    MenhirInterpreter
  - Lex
    
    S
  - Location
    
    S
  - Parse
    
    S
    
    Incremental
    
    MenhirInterpreter
  - Stmt
    
    Logic
  - Term
    
    Logic
dolmen.line
- Dolmen_line
dolmen.smtlib
- Dolmen_smtlib
  - Id
  - Make
    
    I
    
    L
    
    Lexer
    
    Parser
    
    Incremental
    
    MenhirInterpreter
    
    S
    
    T
  - Statement
  - Term
dolmen.std
- Dolmen_std
  - Id
  - Misc
  - Normalize
    
    Smtlib
    
    Tptp
  - ParseLocation
  - Statement
  - Term
  - Transformer
    
    Make
    
    Lex
    
    Loc
    
    Parse
    
    Incremental
    
    MenhirInterpreter
    
    Ty
dolmen.tptp
- Dolmen_tptp
  - 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

Standard implementation of file locations.

Interface definition

module type S = Dolmen_intf.Location.S

An anstract module type for providing locations. Used as argumentby much of the functors provided in Dolmen. This module (ParseLocation) implements this specification.

Concrete positions

type t = {

file : string;
start_line : int;
start_column : int;
stop_line : int;
stop_column : int;

}

exception Uncaught of t * exn

exception Lexing_error of t * string

exception Syntax_error of t * string

Exceptions that may occur during parsing

val hash : t -> int

val eq : t -> t -> bool

Hash and equality

val mk : string -> int -> int -> int -> int -> t

val mk_pair : string -> (int * int) -> (int * int) -> t

val mk_pos : Lexing.position -> Lexing.position -> t

Construction functions

val pp : Buffer.t -> t -> unit

val fmt : Format.formatter -> t -> unit

val fmt_hint : Format.formatter -> t -> unit

Printing functions

val combine : t -> t -> t

Location that spans the two given positions. The file is assumed to be the same in both case, and is chosen from one of the two positions.

val combine_list : t list -> t

N-ary version of combine.

raises Invalid_argument
if the list is empty

val smaller : t -> t -> bool

smaller p1 p2 is true if p1 is included in p2, ie p1 is a sub-location of p2 (interval inclusion)

Lexbuf

val set_file : Lexing.lexbuf -> string -> unit

Change the file name used for positions in this lexbuf

val mk_lexbuf : [ `Stdin | `File of string ] -> Lexing.lexbuf * (unit -> unit)

Returns the lexbuf associetd with the given file or stdin, with the correct filename, together with a function to close the associated file descriptor.

val of_lexbuf : Lexing.lexbuf -> t

Recover a position from a lexbuf