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

sha256=ff2889fa9d467d5b4d87ae4f819a64358715f457cc6226b455463c2fcd4ab2af

sha512=d6ba56945aabcf0886e83fcf44c45f2f8afcf68e48d2f0b25f9cd8e60d18106fae3976fee49d3e291b2e0ab3266837ad5eff800dc51fe2b3aab15ad81ea58cbb

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

Module `Dolmen_std.Namespace`Source

Type and std functions

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 t =

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

Sourceval hash : t -> int

Sourceval equal : t -> t -> bool

Sourceval compare : t -> t -> int

Std functions

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

Printing function.

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

Maps on namespaces

Creation

Sourceval var : t

The variable namespace.

Sourceval sort : t

The sort namespace.

Sourceval term : t

The term namespace.

Sourceval attr : t

Teh attribute namespace.

Sourceval decl : t

The declaration namespace.

Sourceval track : t

Namespace used for identifiers used for tracking/special identification.

On This Page

Type and std functions
Creation