package dolmen

  1. Overview
  2. Docs
package dolmen
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 : Buffer.t -> t -> unit
val print : 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.

val tptp_kind : t

The tagged statement is of the given kind (e.g. tff, thf, ...). Should be used as a function symbol applied to the actual tptp kind.

OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct