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 {
id_ty : 'ty;
index : index;(*

unique index

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

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

and type_ =
| Type
and type_fun = {
arity : int;
mutable alias : type_alias;
}
and type_alias =
| No_alias
| Alias of {
alias_vars : ty_var list;
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 =
| TyVar of ty_var(*

Type variables

*)
| TyApp of ty_cst * ty list(*

Application

*)
| Arrow of ty list * ty(*

Function type

*)
| Pi of ty_var list * ty(*

Type quantification

*)

Type descriptions.

and ty = private {
mutable ty_hash : hash;
mutable ty_tags : Tag.map;
mutable ty_descr : ty_descr;
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 =
| Var of term_var(*

Variables

*)
| Cst of term_cst(*

Constants

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

Application

*)
| Binder of binder * term(*

Binders

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

Pattern matching

*)

Term descriptions.

and binder =
| Let_seq of (term_var * term) list
| Let_par of (term_var * term) list
| Lambda of ty_var list * term_var list
| Exists of ty_var list * term_var list
| Forall of ty_var list * term_var list

Binders.

and term = {
term_ty : ty;
term_descr : term_descr;
mutable term_hash : hash;
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.