package dolmen

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

Module Dolmen_std.IdSource

Standard implementation of identifiers

Type definitions

Sourcetype namespace = Namespace.t
Sourcetype 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
Sourceval sort : namespace

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

Sourceval var : namespace

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

Sourceval term : namespace

The usual namespace for terms.

Sourceval attr : namespace

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

Sourceval decl : namespace

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

Sourceval track : namespace

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

Sourceval mk : namespace -> string -> t

Make an identifier from its namespace and name.

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

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

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

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

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

An identifier with an additional name for tracking purposes.

Usual comparison functions

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

Usual functions for hashing, comparisons, equality.

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

Printing functions.

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

Maps for ids

Additional functions

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

Create an identifier.

Sourceval ns : t -> namespace

Accessor for the id's namespace.

Sourceval name : t -> Name.t

Accessor for the id's name.

Standard attributes

Sourceval stmt : t

Used to attach names to extension statements.

Sourceval ac_symbol : t

Used to denote associative-commutative symbols.

Sourceval predicate_def : t

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

Sourceval case_split : t

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

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

Sourceval rwrt_rule : t

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

Sourceval tptp_role : t

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

Sourceval 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