package dolmen

  1. Overview
  2. Docs
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).

type ty_def_adt_case = {
  1. cstr : term_cst;
  2. tester : term_cst;
  3. dstrs : term_cst option array;
}

One case of the type definition for an algebraic datatype.

type ty_def =
  1. | Abstract
    (*

    Abstract types

    *)
  2. | Adt of {
    1. ty : ty_cst;
    2. record : bool;
    3. cases : ty_def_adt_case array;
    }
    (*

    Algebraic datatypes, including records (which are seen as a 1-case adt).

    *)

Type definitions.

Exceptions & Helpers

exception Already_aliased of ty_cst
exception Type_already_defined of ty_cst
exception Record_type_expected of ty_cst
exception Wildcard_already_set of ty_var
val with_cache : ?size:int -> ('a -> 'b) -> 'a -> 'b

Memoize the given function using a hashtable as cache. Useful to wrap functions such as Ty.Var.mk when some symbol is indexed over **simple** arguments (for instance in the case of bitvectors). By default, the size is the 16, which is the minmum size of a hashtbl.

WARNING: One must be careful about order of execution when using this function. In particular, eta-expansion can break the cache behaviour. For instance the following is a correct use of this function: (** correct version *) let add_one = with_cache ((+) 1) However, the following is incorrect and will instead create a new cache for each call to the function (** bad version *) let bad_add_one x = with_cache ((+) 1) x

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.

OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct