# package dolmen

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

`type t = term`

The type of terms and term variables.

`type ty = Ty.t`

`type ty_var = Ty.Var.t`

`type ty_const = Ty.Const.t`

The representation of term types, type variables, and type constants.

`type 'a tag = 'a Tag.t`

The type of tags used to annotate arbitrary terms.

`val hash : t -> int`

Hash function.

`val print : Stdlib.Format.formatter -> t -> unit`

Printing function.

Get the list of values bound to a list tag, returning the empty list if no value is bound.

Optionally bind an additional value to a list tag.

Bind a list of additional values to a list tag.

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

A module for Record fields.

Define a new record type.

```
val define_adt :
ty_const ->
ty_var list ->
(Path.t * (ty * Path.t option) list) list ->
(Cstr.t * (ty * 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.

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 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 Field_expected of term_cst`

A field was expected but the returned term constant is not a record field.

`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 Constructor_expected of Cstr.t`

Raised when trying to access the tester of an ADT constructor, but the constant provided was not a constructor.

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

Create a pattern match.

`val void : t`

The only inhabitant of type unit.

`val _true : t`

`val _false : t`

Some usual formulas.

`val int : string -> t`

`val rat : string -> t`

`val real : string -> t`

Real literals

Create a local function. The first pair of arguments are the variables that are free in the resulting quantified formula, and the second pair are the variables bound.

Universally quantify the given formula over the type and terms variables. The first pair of arguments are the variables that are free in the resulting quantified formula, and the second pair are the variables bound.

Existencially quantify the given formula over the type and terms variables. The first pair of arguments are the variables that are free in the resulting quantified formula, and the second pair are the variables bound.

Tag the given variable with the term, to mark it has been let-bound. Views might use that information to transparently replace a let-bound variable with its defining term.

Sequential let-binding. Variables can be bound to either terms or formulas.

Parrallel let-binding. Variables can be bound to either terms or formulas.

`module Bitv : sig ... end`

`module Float : sig ... end`

`module Int : sig ... end`

Integer operations.

`module Rat : sig ... end`

Rational operations

`module Real : sig ... end`

Real operations

`module String : sig ... end`

String operations