package dolmen

You can search for identifiers within the package.

in-package search v0.2.0

A parser library for automated deduction

Install

Dune Dependency

github.com Readme Changelog Edit opam file Versions (11)

Authors

G

Guillaume Bury <guillaume.bury@gmail.com>

Maintainers

G

Guillaume Bury <guillaume.bury@gmail.com>

Sources

dolmen-0.9.tbz

sha256=003db53854bacc3a33fa55ed69cf79817c10369a4f7c6be944af1dcc36578a0a

sha512=3f8570f41c8c559c2907734efca98eecfc0f28ec3bce9dde500d5777a97391121a89ca66e7135d40b15161fe890d7b40fa53daba83eab0accf71fff136d45c74

doc/dolmen.std/Dolmen_std/Id/index.html

Module `Dolmen_std.Id`Source

Standard implementation of identifiers

Type definitions

Sourcetype namespace = Namespace.t

Sourcetype t = {

name : Name.t;
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 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.

On This Page

Type definitions
Implemented interfaces
Usual comparison functions
Additional functions
Standard attributes