3.4 Environnement de typage
L'environnement de typage, nécessaire lors du typage pour les variables libres (comme les
primitives ou les paramètres formels) d'expressions est représenté par une liste d'association (string * quantified_type) list.
Il est nécessaire de faire une distinction entre les variables d'un type si elles sont
quantifiées (variables liées) ou si elles ne le sont pas (variables libres).
let rec vars_of_type t =
*
let rec vars vl = function
*
Const_type ® vl
*
Var_type (ref (Unknown n)) ® if mem n vl then vl else n::vl
*
Var_type (ref (Instanciated t)) ® vars vl t
*
Pair_type (t1,t2) ® vars (vars vl t1) t2
*
List_type t ® vars vl t
*
Fun_type (t1,t2) ® vars (vars vl t1) t2
*
in
*
vars [ ] t
*
;;
*
vars_of_type : ml_type ® int list = áfunñ
Pour calculer les variables libres et liées d'un schéma de type,
let free_vars_of_type (bv,t) =
*
subtract (vars_of_type t) bv
*
and bound_vars_of_type (fv,t) =
*
subtract (vars_of_type t) fv
*
;;
*
free_vars_of_type : int list * ml_type ® int list = áfunñ
*
bound_vars_of_type : int list * ml_type ® int list = áfunñ
let append l1 l2 = l1@l2;;
*
append : a list ® a list ® a list = áfunñ
let flat ll = list_it append ll [ ];;
*
flat : a list list ® a list = áfunñ
let free_vars_of_type_env l =
*
flat ( map (function (id,Forall gvt) ® free_vars_of_type gvt) l)
*
;;
*
free_vars_of_type_env : (a * quantified_type) list ® int list = áfunñ
Lors du typage d'un identificateur dans un environnement C, le vérificateur cherche
dans l'environnement le type quantifié associé à cet identificateur et en retourne une
instance, où les variables quantifiées valent de nouvelles variables (ou inconnues).
let type_instance st =
*
match st with Forall(gv,t) ®
*
let unknowns = map (function n ® n,new_unknown()) gv
*
in
*
let rec instance = function
*
Var_type (ref(Unknown n)) as t ® (try assoc n unknowns with Not_found ® t)
*
Var_type (ref(Instanciated t)) ® instance t
*
Const_type ct as t ® t
*
Pair_type (t1,t2) ® Pair_type (instance t1, instance t2)
*
List_type t ® List_type (instance t)
*
Fun_type (t1,t2) ® Fun_type (instance t1, instance t2)
*
in
*
instance t
*
;;
*
type_instance : quantified_type ® ml_type = áfunñ