Module Dolmen_stdSource

Sourcemodule Answer : sig ... end

Standard implementation of answers.

Sourcemodule Builtin : sig ... end

This module defines the builtins that are defined by Dolmen.

Sourcemodule Escape : sig ... end

Escaping identifiers

Sourcemodule Expr : sig ... end
Sourcemodule Extensions : sig ... end
Sourcemodule Id : sig ... end

Standard implementation of identifiers

Sourcemodule Loc : sig ... end

Standard implementation of file locations.

Sourcemodule Maps : sig ... end
Sourcemodule Maps_string : sig ... end
Sourcemodule Misc : sig ... end
Sourcemodule Msg : sig ... end
Sourcemodule Name : sig ... end

Names

Sourcemodule Namespace : sig ... end
Sourcemodule Normalize : sig ... end

Normalizing functions

Sourcemodule Path : sig ... end

Paths

Sourcemodule Pretty : sig ... end

Pretty printing annotations

Sourcemodule Statement : sig ... end

Standard imlplementation of statements. This module provides a reasonable and standard implementation of statements, that can directly be used to instantiated the various functors of the dolmen library. These statements are closer to smtlib statements than to other languages statements because it is easier to express other languages statements using smtlib's than the other way around. Still, a generalisation of smtlib statements was needed so as not to lose some important distinctions between conjectures and assertions for instance.

Sourcemodule Stats : sig ... end
Sourcemodule Tag : sig ... end

Tags

Sourcemodule Term : sig ... end

Standard implementation of terms

Sourcemodule Timer : sig ... end
Sourcemodule Tok : sig ... end
Sourcemodule Transformer : sig ... end
Sourcemodule Vec : sig ... end

Resieable arrays