# Module `AltErgoLib.Ty`

### Definition

`type t`

`=`

`|`

`Tint`

Integer numbers

`|`

`Treal`

Real numbers

`|`

`Tbool`

Booleans

`|`

`Tunit`

The unit type

`|`

`Tvar of tvar`

Type variables

`|`

`Tbitv of int`

Bitvectors of a given length

`|`

`Text of t list * Hstring.t`

Abstract types applied to arguments.

`Text (args, s)`

is the application of the abstract type constructor`s`

to arguments`args`

.`|`

`Tfarray of t * t`

Functional arrays.

`TFarray (src,dst)`

maps values of type`src`

to values of type`dst`

.`|`

`Tsum of Hstring.t * Hstring.t list`

Enumeration, with its name, and the list of its constructors.

`|`

`Tadt of Hstring.t * t list`

Algebraic types applied to arguments.

`Tadt (s, args)`

is the application of the datatype constructor`s`

to arguments`args`

.`|`

`Trecord of trecord`

Record type.

`and tvar`

`=`

`{`

`v : int;`

Unique identifier

`mutable value : t option;`

Pointer to the current value of the type variable.

`}`

Type variables. The

`value`

field is mutated during unification, hence distinct types should have disjoints sets of type variables (see function`fresh`

).

`and trecord`

`=`

`{`

`mutable args : t list;`

Arguments passed to the record constructor

`name : Hstring.t;`

Name of the record type

`mutable lbs : (Hstring.t * t) list;`

List of fields of the record. Each field has a name, and an associated type.

`record_constr : Hstring.t;`

record constructor. Useful is case it's a specialization of an algeberaic datatype. Default value is "{__

`name`

"`}`

Record types.

`type adt_constr`

`=`

`{`

`constr : Hstring.t;`

constructor of an ADT type

`destrs : (Hstring.t * t) list;`

the list of destructors associated with the constructor and their respective types

`}`

`type type_body`

`=`

`|`

`Adt of adt_constr list`

body of an algebraic datatype

bodies of types definitions. Currently, bodies are inlined in the type

`t`

for records and enumerations. But, this is not possible for recursive ADTs

`module Svty : Stdlib.Set.S with type elt = int`

Sets of type variables, indexed by their identifier.

`module Set : Stdlib.Set.S with type elt = t`

Sets of types

`val assoc_destrs : Hstring.t -> adt_constr list -> (Hstring.t * t) list`

returns the list of destructors associated with the given consturctor. raises Not_found if the constructor is not in the given list

### Type inspection

`val hash : t -> int`

Hash function

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

Printing function for types (does not print the type of each fields for records).

`val print_list : Stdlib.Format.formatter -> t list -> unit`

Print function for lists of types (does not print the type of each fields for records).

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

Print function including the record fields.

### Building types

`val tunit : t`

The unit type.

`val fresh_var : unit -> tvar`

Generate a fresh type variable, guaranteed to be distinct from any other previously generated by this function.

`val fresh_empty_text : unit -> t`

Return a fesh abstract type.

`val text : t list -> string -> t`

Apply the abstract type constructor to the list of type arguments given.

`val tsum : string -> string list -> t`

Create an enumeration type.

`tsum name enums`

creates an enumeration named`name`

, with constructors`enums`

.

`val t_adt : ?body:(string * (string * t) list) list option -> string -> t list -> t`

Crearte and algebraic datatype. The body is a list of constructors, where each constructor is associated with the list of its destructors with their respective types. If

`body`

is none, then no definition will be registered for this type. The second argument is the name of the type. The third one provides its list of arguments.

### Substitutions

`module M : Stdlib.Map.S with type key = int`

Maps from type variables identifiers.

`val print_subst : Stdlib.Format.formatter -> subst -> unit`

Print function for substitutions.

`val esubst : subst`

The empty substitution, a.k.a. the identity.

### Unification/Matching

`exception`

`TypeClash of t * t`

Exception raised during matching or unification.

`TypeClash (u, v)`

is raised when`u`

and`v`

could not be matched or unified (`u`

and`v`

may be sub-types of the types being actually unified or matched).

`val unify : t -> t -> unit`

Destructive unification. Mutates the

`value`

fields of type variables.- raises TypeClash
when unification is impossible. In this case, the

`value`

fields of already mutated type variables are left modified, which may prevent future unifications.

### Manipulations on types

`val fresh : t -> subst -> t * subst`

Apply the given substitution, all while generating fresh variables for the variables not already bound in the substitution. Returns a substitution containing bindings from old variable to their fresh counterpart.

`val instantiate : t list -> t list -> t -> t`

`instantiate vars args t`

builds the substitutions mapping each type variable in`vars`

to the corresponding term in`args`

, then apply that substitution to`t`

.- raises Invalid_argument
if the lists

`vars`

and`args`

do not have the same length

- raises Assertion_failure
if one type in

`vars`

is not a type variable.