dolmen 0.7 · OCaml Package

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 {
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 =

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

package dolmen

Type definitions

Common definitions

Type definitions

Exceptions

Native Tags

Printing

Substitutions

Identifiers

Types

Terms