package dolmen

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

Standard implementation of identifiers

Type definitions

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

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

    *)
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 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 mod_name : string -> namespace

Namespace used by modules (for instance in dedulkti).

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.

Standard attributes

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.

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