dolmen

A parser library for automated deduction
Legend:
Library
Module
Module type
Parameter
Class
Class type
Library dolmen.std
Module Dolmen_std
module Builtin : sig ... end

This module defines the builtins that are defined by Dolmen.

module Escape : sig ... end

Escaping identifiers

module Expr : sig ... end
module Id : sig ... end

Standard implementation of identifiers

module Loc : sig ... end

Standard implementation of file locations.

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

Names

module Namespace : sig ... end
module Normalize : sig ... end

Normalizing functions

module Path : sig ... end

Paths

module Pretty : sig ... end

Pretty printing annotations

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

module Stats : sig ... end
module Tag : sig ... end

Tags

module Term : sig ... end

Standard implementation of terms

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

Resieable arrays