Library

Module

Module type

Parameter

Class

Class type

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

`type t = Dolmen.Std.Expr.term`

The type of terms and term variables.

`module Var : sig ... end`

A module for variables that occur in terms.

`module Const : sig ... end`

A module for constant symbols that occur in terms.

`module Cstr : sig ... end`

A module for Algebraic datatype constructors.

`module Field : sig ... end`

```
val define_adt :
Ty.Const.t ->
Ty.Var.t list ->
(Dolmen.Std.Path.t * (Ty.t * Dolmen.Std.Path.t option) list) list ->
(Cstr.t * (Ty.t * Const.t option) list) list
```

`define_aft t vars cstrs`

defines the type constant `t`

, parametrised over the type variables `ty_vars`

as defining an algebraic datatypes with constructors `cstrs`

. `cstrs`

is a list where each elements of the form `(name, l)`

defines a new constructor for the algebraic datatype, with the given name. The list `l`

defines the arguments to said constructor, each element of the list giving the type `ty`

of the argument expected by the constructor (which may contain any of the type variables in `vars`

), as well as an optional destructor name. If the construcotr name is `Some s`

, then the ADT definition also defines a function that acts as destructor for that particular field. This polymorphic function is expected to takes as arguments as many types as there are variables in `vars`

, an element of the algebraic datatype being defined, and returns a value for the given field. For instance, consider the following definition for polymorphic lists: ```
define_adt list [ty_var_a] [
"nil", [];
"const", [
(Ty.of_var ty_var_a , Some "hd");
(ty_list_a , Some "tl");
];
]
```

This definition defines the usual type of polymorphic linked lists, as well as two destructors "hd" and "tl". "hd" would have type `forall alpha. alpha list -> a`

, and be the partial function returning the head of the list.

```
val define_record :
Ty.Const.t ->
Ty.Var.t list ->
(Dolmen.Std.Path.t * Ty.t) list ->
Field.t list
```

Define a (previously abstract) type to be a record type, with the given fields.

Exception raised in case of typing error during term construction. `Wrong_type (t, ty)`

should be raised by term constructor functions when some term `t`

is expected to have type `ty`

, but does not have that type.

Raised when some constructor was expected to belong to some type but does not belong to the given type.

`exception Wrong_record_type of Field.t * Ty.Const.t`

Exception raised in case of typing error during term construction. This should be raised when the returned field was expected to be a field for the returned record type constant, but it was of another record type.

`exception Field_repeated of Field.t`

Field repeated in a record expression.

`exception Field_missing of Field.t`

Field missing in a record expression.

`exception Pattern_expected of t`

Raised when trying to create a pattern matching, but a non-pattern term was provided where a pattern was expected.

Raise when creating a pattern matching but an empty list of branches was provided

`exception Partial_pattern_match of t list`

Raised when a partial pattern matching was created. A list of terms not covered by the patterns is provided.

`exception Over_application of t list`

Raised when an application was provided too many term arguments. The extraneous arguments are returned by the exception.

Raised when a polymorphic application does not have an adequate number of arguments.

Given a constructor `c`

and a term `t`

, returns a terms that evaluates to `true`

iff `t`

has `c`

as head constructor.

Universally quantify the given formula over the type and terms variables.

Existencially quantify the given formula over the type and terms variables.

Bind a variable to an expressions. This function is called when typing a let-binding, before the body of the let-binding is typed. The returned expressions is used to replace the variable everywhere in the body of the let-binding being typed.

`pattern_match scrutinee branches`

creates a pattern match expression on the scrutinee with the given branches, each of the form `(pattern, body)`