Module Dolmen_std.Id

Standard implementation of identifiers

Type definitions

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

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 mk : namespace -> string -> t

Make an identifier from its namespace and name.

val indexed : namespace -> string -> string list -> t

Make an indexed identifier from a namespace, basename and list of indexes.

val qualified : namespace -> string list -> string -> t

Make a qualified identifier from a namespace, a list of modules (a path), and a base name.

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.

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

Printing functions.

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

Maps for ids

Additional functions

val create : namespace -> Name.t -> t

Create an identifier.

val ns : t -> namespace

Accessor for the id's namespace.

val name : t -> Name.t

Accessor for the id's name.

Standard attributes

val stmt : t

Used to attach names to extension statements.

val ac_symbol : t

Used to denote associative-commutative symbols.

val predicate_def : t

Used to differentiate between functions and predicates in alt-ergo.

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.