package dolmen

  1. Overview
  2. Docs
A parser library for automated deduction

Install 

dune-project
 Dependency

github.com Readme Changelog Edit opam file Versions (11)

Authors

  1. G
    Guillaume Bury <guillaume.bury@gmail.com>

Maintainers

  1. G
    Guillaume Bury <guillaume.bury@gmail.com>

Sources

dolmen-0.9.tbz
sha256=003db53854bacc3a33fa55ed69cf79817c10369a4f7c6be944af1dcc36578a0a
sha512=3f8570f41c8c559c2907734efca98eecfc0f28ec3bce9dde500d5777a97391121a89ca66e7135d40b15161fe890d7b40fa53daba83eab0accf71fff136d45c74

doc/dolmen.std/Dolmen_std/Namespace/index.html

Module Dolmen_std.NamespaceSource

Type and std functions

Sourcetype value =
  1. | Integer
    (*

    Integers (in base 10 notation), e.g. "123456789"

    *)
  2. | Rational
    (*

    Rational (using quotient notation with '/'), e.g. "123/456"

    *)
  3. | Real
    (*

    Real (using decimal floating point notation with exponent), e.g. "123.456e789"

    *)
  4. | Binary
    (*

    Bitvector in binary notation, e.g. "0b011010111010"

    *)
  5. | Hexadecimal
    (*

    Bitvector in hexadecimal notation, e.g. "0x9a23e5f"

    *)
  6. | Bitvector
    (*

    Bitvector litteral.

    *)
  7. | String
    (*

    String litterals.

    *)

Types of lexical values typically encountered.

Sourcetype t =
  1. | Var
    (*

    Namespace for variables. Not all variables are necessarily in this namespace, but ids in this namespace must be variables.

    *)
  2. | Sort
    (*

    Namepsace for sorts and types (only used in smtlib)

    *)
  3. | Term
    (*

    Most used namespace, used for terms in general (and types outside smtlib).

    *)
  4. | Attr
    (*

    Namespace for attributes (also called annotations).

    *)
  5. | Decl
    (*

    Namespace used for naming declarations/definitions/statements...

    *)
  6. | Track
    (*

    Namespace used to track specific values throughout some files.

    *)
  7. | Value of value
    (*

    The identifier is a value, encoded in a string. Examples include arithmetic constants (e.g. "123456", "123/456", "123.456e789"), bitvectors (i.e. binary notation), etc...

    *)

Namespaces, used to record the lexical scop in which an identifier was parsed.

Sourceval hash : t -> int
Sourceval equal : t -> t -> bool
Sourceval compare : t -> t -> int

Std functions

Sourceval print : Format.formatter -> t -> unit

Printing function.

Sourcemodule Map : Maps.S with type key := t

Maps on namespaces

Creation

Sourceval var : t

The variable namespace.

Sourceval sort : t

The sort namespace.

Sourceval term : t

The term namespace.

Sourceval attr : t

Teh attribute namespace.

Sourceval decl : t

The declaration namespace.

Sourceval track : t

Namespace used for identifiers used for tracking/special identification.