Module AltErgoLib.TySource

Types

This module defines the representation of types.

Definition

Sourcetype t =
  1. | Tint
    (*

    Integer numbers

    *)
  2. | Treal
    (*

    Real numbers

    *)
  3. | Tbool
    (*

    Booleans

    *)
  4. | Tunit
    (*

    The unit type

    *)
  5. | Tvar of tvar
    (*

    Type variables

    *)
  6. | Tbitv of int
    (*

    Bitvectors of a given length

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

    *)
  8. | Tfarray of t * t
    (*

    Functional arrays. TFarray (src,dst) maps values of type src to values of type dst.

    *)
  9. | Tsum of Hstring.t * Hstring.t list
    (*

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

    *)
  10. | 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.

    *)
  11. | Trecord of trecord
    (*

    Record type.

    *)
Sourceand tvar = {
  1. v : int;
    (*

    Unique identifier

    *)
  2. 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).

Sourceand trecord = {
  1. mutable args : t list;
    (*

    Arguments passed to the record constructor

    *)
  2. name : Hstring.t;
    (*

    Name of the record type

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

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

    *)
  4. record_constr : Hstring.t;
    (*

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

    *)
}

Record types.

Sourcetype adt_constr = {
  1. constr : Hstring.t;
    (*

    constructor of an ADT type

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

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

    *)
}
Sourcetype type_body =
  1. | 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

Sourcemodule Svty : Set.S with type elt = int

Sets of type variables, indexed by their identifier.

Sourcemodule Set : Set.S with type elt = t

Sets of types

Sourceval 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

Sourceval type_body : Hstring.t -> t list -> type_body

Type inspection

Sourceval hash : t -> int

Hash function

Sourceval equal : t -> t -> bool

Equality function

Sourceval compare : t -> t -> int

Comparison function

Sourceval print : Format.formatter -> t -> unit

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

Sourceval print_list : Format.formatter -> t list -> unit

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

Sourceval print_full : Format.formatter -> t -> unit

Print function including the record fields.

Sourceval vty_of : t -> Svty.t

Returns the set of type variables that occur in a given type.

Building types

Sourceval tunit : t

The unit type.

Sourceval fresh_var : unit -> tvar

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

Sourceval fresh_tvar : unit -> t

Wrap the fresh_var function to return a type.

Sourceval fresh_empty_text : unit -> t

Return a fesh abstract type.

Sourceval text : t list -> string -> t

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

Sourceval tsum : string -> string list -> t

Create an enumeration type. tsum name enums creates an enumeration named name, with constructors enums.

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

Sourceval trecord : ?record_constr:string -> t list -> string -> (string * t) list -> t

Create a record type. trecord args name lbs creates a record type with name name, arguments args and fields lbs.

Substitutions

Sourcemodule M : Map.S with type key = int

Maps from type variables identifiers.

Sourcetype subst = t M.t

The type of substitution, i.e. maps from type variables identifiers to types.

Sourceval compare_subst : subst -> subst -> int

Comparison of substitutions.

Sourceval equal_subst : subst -> subst -> bool

Equality of substitutions.

Sourceval print_subst : Format.formatter -> subst -> unit

Print function for substitutions.

Sourceval esubst : subst

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

Sourceval apply_subst : subst -> t -> t

Substitution application.

Sourceval union_subst : subst -> subst -> subst

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.

Unification/Matching

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

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

Sourceval matching : subst -> t -> t -> subst

Matching of types (non-destructive). matching pat t returns a substitution subst such that apply_subst subst pat is equal to t.

Sourceval shorten : t -> 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.

Manipulations on types

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

Sourceval fresh_list : t list -> subst -> t list * subst

Same as fresh but on lists of types.

Sourceval 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 Assertion_failure

    if one type in vars is not a type variable.

Sourceval monomorphize : t -> t

Return a monomorphized variant of the given type, where type variable without values have been replaced by abstract types.