package dolmen

  1. Overview
  2. Docs
Legend:
Library
Module
Module type
Parameter
Class
Class type

Standard implementation of identifiers

Type definitions

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

type namespace =
  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. | Module of string
    (*

    Namespaces defined by modules (used for instance in dedukti).

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

type t = {
  1. ns : namespace;
  2. name : string;
}

The type of identifiers, basically a name together with a namespace.

Implemented interfaces

include Dolmen_intf.Id.Logic with type t := t and type namespace := namespace
val sort : namespace

The namespace for sorts (also called types). Currently only used for smtlib.

val var : namespace

Namespace for variables (when they can be syntatically distinguished from constants).

val term : namespace

The usual namespace for terms.

val attr : namespace

Namespace used for attributes (also called annotations) in smtlib.

val decl : namespace

Namespace used for declaration identifiers (for instance used to filter declarations during includes)

val track : namespace

Namespace used to tag and identify sub-terms occuring in files.

val mod_name : string -> namespace

Namespace used by modules (for instance in dedulkti).

val tracked : track:t -> namespace -> string -> t

An identifier with an additional name for tracking purposes.

Usual comparison functions

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

Usual functions for hashing, comparisons, equality.

Additional functions

val mk : namespace -> string -> t

Create an identifier.

val full_name : t -> string

Returns a full name for the identifier. NOTE: full names may not be unique and therefore not suitable for comparison of identifiers.

val pp : Stdlib.Buffer.t -> t -> unit
val print : Stdlib.Format.formatter -> t -> unit

Printing functions.

val split : t -> string list

Split an id into a list of strings (used notably for SMTLIb).

Standard attributes

val ac_symbol : t

Used to denote associative-commutative symbols.

val case_split : t

Used to annote axioms/antecedants which are case split in alt-ergo.

val theory_decl : t

Used to define theories; used primarily in alt-ergo where it affects what engine is used to trigger axioms in the theory.

val rwrt_rule : t

The tagged term is (or at least should be) a rewrite rule.

val tptp_role : t

The tagged statement has a tptp role. Should be used as a function symbol applied to the actual tptp role.

OCaml

Innovation. Community. Security.