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 = 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 : Stdlib.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.

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