Module `Dolmen_std.Id`Source

Standard implementation of identifiers

Type definitions

Sourcetype value =

| Integer
(*
Integers (in base 10 notation), e.g. "123456789"
*)
| Rational
(*
Rational (using quotient notation with '/'), e.g. "123/456"
*)
| Real
(*
Real (using decimal floating point notation with exponent), e.g. "123.456e789"
*)
| Binary
(*
Bitvector in binary notation, e.g. "0b011010111010"
*)
| Hexadecimal
(*
Bitvector in hexadecimal notation, e.g. "0x9a23e5f"
*)
| Bitvector
(*
Bitvector litteral.
*)
| String
(*
String litterals.
*)

Types of lexical values typically encountered.

Sourcetype namespace =

| Var
(*
Namespace for variables. Not all variables are necessarily in this namespace, but ids in this namespace must be variables.
*)
| Sort
(*
Namepsace for sorts and types (only used in smtlib)
*)
| Term
(*
Most used namespace, used for terms in general (and types outside smtlib).
*)
| Attr
(*
Namespace for attributes (also called annotations).
*)
| Decl
(*
Namespace used for naming declarations/definitions/statements...
*)
| Track
(*
Namespace used to track specific values throughout some files.
*)
| Module of string
(*
Namespaces defined by modules (used for instance in dedukti).
*)
| Value of value
(*
The identifier is a value, encoded in a string. Examples include arithmetic constants (e.g. "123456", "123/456", "123.456e789"), bitvectors (i.e. binary notation), etc...
*)

Namespaces, used to record the lexical scop in which an identifier was parsed.

Sourcetype t = {

ns : namespace;
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

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

Namespace used by modules (for instance in dedulkti).

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.

Additional functions

Sourceval mk : namespace -> string -> t

Create an identifier.

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

Sourceval pp : Buffer.t -> t -> unit

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

Printing functions.

Sourceval split : t -> string list

Split an id into a list of strings (used notably for SMTLIb).

Standard attributes

Sourceval ac_symbol : t

Used to denote associative-commutative symbols.

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.

Install

Dune Dependency

Authors

Maintainers

Sources

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

Module `Dolmen_std.Id`Source

Type definitions

Implemented interfaces

Usual comparison functions

Additional functions

Standard attributes

package dolmen

Install

Dune Dependency

Authors

Maintainers

Sources

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

Module Dolmen_std.IdSource

Type definitions

Implemented interfaces

Usual comparison functions

Additional functions

Standard attributes

Module `Dolmen_std.Id`Source