package dolmen
Legend:
Library
Module
Module type
Parameter
Class
Class type

Type definitions

Common definitions

type hash = private int
type index = private int
type 'a tag = 'a Tag.t

Type definitions

type builtin = < ty : ty ; ty_var : ty_var ; ty_cst : ty_cst ; term : term ; term_var : term_var ; term_cst : term_cst > Builtin.t

Extensible variant type for builtin operations.

and 'ty id = private {
  1. id_ty : 'ty;
  2. index : index;
    (*

    unique index

    *)
  3. path : Path.t;
  4. builtin : builtin;
  5. mutable tags : Tag.map;
}

The type of identifiers. 'ty is the type for representing the type of the id.

and type_ =
  1. | Type
and type_fun = {
  1. arity : int;
  2. mutable alias : type_alias;
}
and type_alias =
  1. | No_alias
  2. | Alias of {
    1. alias_vars : ty_var list;
    2. alias_body : ty;
    }
and ty_var = type_ id

Abbreviation for type variables.

and ty_cst = type_fun id

Type symbols have the expected length of their argument encoded.

and ty_descr =
  1. | TyVar of ty_var
    (*

    Type variables

    *)
  2. | TyApp of ty_cst * ty list
    (*

    Application

    *)
  3. | Arrow of ty list * ty
    (*

    Function type

    *)
  4. | Pi of ty_var list * ty
    (*

    Type quantification

    *)

Type descriptions.

and ty = private {
  1. mutable ty_hash : hash;
  2. mutable ty_tags : Tag.map;
  3. mutable ty_descr : ty_descr;
  4. mutable ty_head : ty;
}

Types, which wrap type description with a memoized hash and some tags.

and term_var = ty id

Term variables

and term_cst = ty id

Term symbols, which encode their expected type and term argument lists lengths.

and pattern = term

patterns are simply terms

and term_descr =
  1. | Var of term_var
    (*

    Variables

    *)
  2. | Cst of term_cst
    (*

    Constants

    *)
  3. | App of term * ty list * term list
    (*

    Application

    *)
  4. | Binder of binder * term
    (*

    Binders

    *)
  5. | Match of term * (pattern * term) list
    (*

    Pattern matching

    *)

Term descriptions.

and binder =
  1. | Let_seq of (term_var * term) list
  2. | Let_par of (term_var * term) list
  3. | Lambda of ty_var list * term_var list
  4. | Exists of ty_var list * term_var list
  5. | Forall of ty_var list * term_var list

Binders.

and term = {
  1. term_ty : ty;
  2. term_descr : term_descr;
  3. mutable term_hash : hash;
  4. mutable term_tags : Tag.map;
}

Term, which wrap term descriptions.

and formula = term

Alias for signature compatibility (with Dolmen_loop.Pipes.Make for instance).

Exceptions

exception Already_aliased of ty_cst
exception Type_already_defined of ty_cst
exception Record_type_expected of ty_cst

Native Tags

module Tags : sig ... end

Printing

module Print : sig ... end

Substitutions

module Subst : sig ... end

Module to handle substitutions

Identifiers

module Id : sig ... end

Types

module Ty : sig ... end

Terms

module Term : sig ... end

Signature required by terms for typing first-order polymorphic terms.