Module Dolmen_std.Expr

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.