AltErgoLib.Ty
Types
This module defines the representation of types.
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. |
| Tfarray of t * t | (* Functional arrays. |
| 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. |
| 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 "{__ |
}
Record types.
bodies of types definitions. Currently, bodies are inlined in the type t
for records and enumerations. But, this is not possible for recursive ADTs
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
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.
val vty_of : t -> Svty.t
Returns the set of type variables that occur in a given type.
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.
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
.
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.
Create a record type. trecord args name lbs
creates a record type with name name
, arguments args
and fields lbs
.
type subst = t M.t
The type of substitution, i.e. maps from type variables identifiers to types.
val print_subst : Stdlib.Format.formatter -> subst -> unit
Print function for substitutions.
val esubst : subst
The empty substitution, a.k.a. the identity.
union_subst u v
applies v
to u
, resulting in u'
. It then computes the union of u'
and v
, prioritizing bindings from u'
in case of conflict.
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).
Matching of types (non-destructive). matching pat t
returns a substitution subst
such that apply_subst subst pat
is equal to t
.
Shorten paths in type variables values. Unification in particular can create chains where the value
field of one type variable points to another and so on... This function short-circuits such chains so that the value of a type variable can be accessed directly.
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.
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
.