Module Eq

module Eq: sig .. end

Équations du premier ordre et leur résolution

Pcf typé

type eqs = (T.Type.t * T.Type.t) list

type subst

Types des ensembles d'équations et des substitutions

val print_eqs : Pervasives.out_channel -> eqs -> unit

val print_subst : Pervasives.out_channel -> subst -> unit

Et leurs afficheurs

val fresh_var : unit -> int

Renvoie une variable de type fraîche.

val subst : subst -> int -> T.Type.t

Applique une substitution à une variable de type

val subst_type : subst -> T.Type.t -> T.Type.t

L'appel subst s t applique la substitution s au type t.

val mgu : eqs -> subst

Résolution des équations, renvoie une solution principale.

val mgu_incr : T.Type.t -> T.Type.t -> subst -> subst

Résolution incrémentale, on peut voir l'appel mgu_incr t1 t2 s comme renvoyant la substitution mgu(s(t1),s(t2)) o s.

type scheme = int list * T.Type.t

Schéma de type : une paire (vs,t), où vs est la liste des variables quantifiées dans le type ty.

val print_scheme : Pervasives.out_channel -> scheme -> unit

Afficheur

module Vars: sig .. end  with type elt = int

Ensembles de variables de types (ensembles de int, donc).

val dom : subst -> Vars.t

Support d'une substitution, i.e. ensemble des variables de type x telles que s(x) est différent de x.

val id : subst

Substitution identitée id(x) = x pour tout x.

val delta : int -> T.Type.t -> subst

L'appel delta x ty fabrique la substitution s(x) = ty et s(y) = y pour tout y différent de x

val comp : subst -> subst -> subst

Composition des substitutions, ne fonctionne que pour des substitutions de supports disjoints.