package dolmen

  1. Overview
  2. Docs
A parser library for automated deduction

Install 

dune-project
 Dependency

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

Authors

  1. G
    Guillaume Bury <guillaume.bury@gmail.com>

Maintainers

  1. G
    Guillaume Bury <guillaume.bury@gmail.com>

Sources

dolmen-0.7.tbz
sha256=ff2889fa9d467d5b4d87ae4f819a64358715f457cc6226b455463c2fcd4ab2af
sha512=d6ba56945aabcf0886e83fcf44c45f2f8afcf68e48d2f0b25f9cd8e60d18106fae3976fee49d3e291b2e0ab3266837ad5eff800dc51fe2b3aab15ad81ea58cbb

doc/dolmen.class/Dolmen_class/Logic/Make/argument-2-I/index.html

Parameter Make.I

type t

The type of identifiers.

type namespace

The type of namespaces. Namespaces are used to distinguish identifiers with the same name, but that occur in different contexts. For instance, in smtlib, sorts and terms live in different namespaces; so a term constant can have the same name as a sort, and still be syntactically different.

val sort : namespace

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

val var : namespace

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

val term : namespace

The usual namespace for terms.

val attr : namespace

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

val decl : namespace

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

val track : namespace

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

val mk : namespace -> string -> t

Make an identifier from its namespace and name.

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

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

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

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

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

An identifier with an additional name for tracking purposes.