Id (u.03cf4de216353ef524802c691cd262ad.dolmen.0.4.1.doc.dolmen.std.Dolmen

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...
*)
| Module of string
(*
Namespaces defined by modules (used for instance in dedukti).
*)

Sourcetype t = {

}

The type of identifiers, basically a name together with a namespace.

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

Namespace used by modules (for instance in dedulkti).

Sourceval hash : t -> int

Sourceval equal : t -> t -> bool

Sourceval compare : t -> t -> int

Usual functions for hashing, comparisons, equality.

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