summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGuillaume Seguin <guillaume@segu.in>2009-01-14 23:01:48 +0100
committerGuillaume Seguin <guillaume@segu.in>2009-01-14 23:01:48 +0100
commitf490f284951bd7fe9609732d7a2fef07fad0d5aa (patch)
tree9fa44e96374176fd0ffacea2f294cd2293d909bb
parent0c80d91036efe66957039b6bf0c88aa73ff7dc14 (diff)
downloadpetitcaml-f490f284951bd7fe9609732d7a2fef07fad0d5aa.tar.gz
petitcaml-f490f284951bd7fe9609732d7a2fef07fad0d5aa.tar.bz2
[petitcaml] Comment typing.ml
-rw-r--r--typing.ml105
1 files changed, 102 insertions, 3 deletions
diff --git a/typing.ml b/typing.ml
index 13598d4..40c8153 100644
--- a/typing.ml
+++ b/typing.ml
@@ -1,3 +1,7 @@
+(****************************************
+ typing.ml - typage par l'algorithme W
+ ****************************************)
+
open Ast
module Int =
@@ -8,6 +12,7 @@ module Int =
module Imap = Map.Make(Int)
+(* Retourne soit un type de base, soit un type non défini *)
let rec head = function
| Tvar tvar ->
begin
@@ -17,6 +22,7 @@ let rec head = function
end
| t -> t
+(* Applique récursivement l'opération "head" *)
let rec canon t =
match head t with
| Tarrow (t1, t2) -> Tarrow (canon t1, canon t2)
@@ -24,6 +30,9 @@ let rec canon t =
| Tlist t -> Tlist (canon t)
| t -> t
+(* Pour le debug et les erreurs : produit la représentation canonique d'un
+ type sous forme de chaîne de caractères
+ TODO : prendre en compte l'associativité des types *)
let canon_string t tvar_names =
let next_tvar_char = ref 97
and tvar_names = ref tvar_names
@@ -61,11 +70,13 @@ let canon_string t tvar_names =
in
s, !tvar_names
+(* Pour le debug *)
let print_canon_string t =
let s, _ = (canon_string t Imap.empty)
in
Printf.printf "%s\n" s
+(* Erreurs *)
exception TypingFailure of loc option * string
let typing_error l err = raise (TypingFailure (l, err))
@@ -80,6 +91,7 @@ let unification_error l t1 t2 =
in
typing_error l err
+(* Détermine si la variable var apparaît dans le type t_raw *)
let rec occur var t_raw =
match head t_raw with
| Tarrow (t1, t2) -> (occur var t1) || (occur var t2)
@@ -88,6 +100,7 @@ let rec occur var t_raw =
| Tvar tvar when tvar.id = var.id -> true
| t -> false
+(* Réalise l'unification des types t1 et t2 *)
let rec unify loc t1 t2 =
match (head t1, head t2) with
| (a, b) when a = b -> ()
@@ -104,7 +117,8 @@ let rec unify loc t1 t2 =
| (t1, Tvar tv2) ->
unify loc (Tvar tv2) t1
| (t1, t2) -> unification_error loc t1 t2
-and unify_products loc p1 p2 =
+and unify_products loc p1 p2 = (* Unifie les produits, équivalent à un
+ fold_left2 *)
match (p1, p2) with
| [], [] -> true
| [], l -> false
@@ -121,6 +135,7 @@ end
module Vset = Set.Make(V)
+(* Détermination des variables libres d'un type *)
let rec fvars = function
| Tint
| Tstring
@@ -138,8 +153,12 @@ type schema = { vars : Vset.t; typ : typ }
module Smap = Map.Make(String)
type env = { bindings : schema Smap.t; fvars : Vset.t }
-let print_fvars fvars = Vset.iter (function tv -> Printf.printf "%d " tv.id) fvars; print_newline ()
+(* Pour le debug : affiche de manière brute une liste de vars *)
+let print_vars vars =
+ Vset.iter (function tv -> Printf.printf "%d " tv.id) vars;
+ print_newline ()
+(* Pour le debug : affiche un type (représentation non canonique) *)
let rec print_type = function
| Tint -> "int"
| Tstring -> "string"
@@ -161,19 +180,24 @@ let rec print_type = function
let empty_env = { bindings = Smap.empty ; fvars = Vset.empty }
+(* Ajoute un identifiant typé à l'environnement sans généralisation *)
let add ident t env =
{ bindings = Smap.add ident { vars = Vset.empty ; typ = t } env.bindings;
fvars = Vset.union env.fvars (fvars t) }
+(* Vérifie les variables libres de l'environnement lors de la généralisation *)
let verify_fvars_folder tv current =
match head (Tvar tv) with
| Tvar tv -> Vset.add tv current
| _ -> current
+(* Ajoute un identifiant typé à l'environnement avec généralisation *)
let add_gen ident t env =
+ (* Vérifie les variables libres *)
let envfvars =
Vset.fold verify_fvars_folder env.fvars Vset.empty
in
+ (* Calcules les variables libres du type *)
let binding_vars = Vset.diff (fvars t) envfvars
in
{ bindings = Smap.add ident
@@ -181,6 +205,7 @@ let add_gen ident t env =
env.bindings ;
fvars = envfvars }
+(* Remplace la variable d'id orig par la fresh var new_tv *)
let rec replace_var orig new_tv = function
| Tarrow (t1, t2) ->
Tarrow (replace_var orig new_tv t1, replace_var orig new_tv t2)
@@ -194,11 +219,13 @@ let rec replace_var orig new_tv = function
Tvar { id = id ; def = Some (replace_var orig new_tv t) }
| t -> t
+(* Remplace si besoin les occurences de la variable tv par des fresh vars *)
let use_freshvar tv t =
match head (Tvar tv) with
| Tvar tv -> replace_var tv.id (Tvar (V.create())) t
| _ -> t
+(* Retourne le type associé à l'identifiant ident, muni de fresh vars *)
let find ident env =
let binding = Smap.find ident env.bindings
in
@@ -206,6 +233,7 @@ let find ident env =
module Sset = Set.Make(String)
+(* Détermine l'ensemble des variables apparaîssant dans le motif *)
let rec motif_vars loc vars m =
match m.m with
| Munderscore -> vars
@@ -216,6 +244,8 @@ let rec motif_vars loc vars m =
| Mident ident -> Sset.add ident vars
| Mtuple l -> List.fold_left (motif_vars loc) vars l
+(* Ajoute les identifiants du motif m typé comme t à l'environnement env
+ avec la fonction d'ajout add_func *)
let rec add_motif_base add_func env m t =
match m.m with
| Munderscore -> env
@@ -234,12 +264,18 @@ let rec add_motif_base add_func env m t =
| _ -> failwith "add_motif_base : Unreachable matching"
end
+(* Wrappers de la fonction précédente avec et sans généralisation *)
let add_motif_gen env m t = add_motif_base add_gen env m t
and add_motif env m t = add_motif_base add env m t
+(* L'algorithme w ! *)
let rec w env e =
let w_aux e =
match e.e with
+ (* Typage des identificateurs : on va chercher le type de
+ l'identificateur correspondant dans l'environnement
+ Au passage les free vars du type sont remplacées par des fresh
+ vars si besoin *)
| Eident ident ->
begin
try
@@ -249,14 +285,19 @@ let rec w env e =
(Printf.sprintf "Identifiant invalide : %s"
ident)
end
+ (* Typage des constantes : on retourne le type adéquat *)
| Econst (Cint _) -> Tint
| Econst (Cstring _) -> Tstring
| Econst (Cbool _) -> Tbool
| Econst Cunit -> Tunit
| Econst (Cemptylist) ->
Tlist (Tvar (V.create ()))
+ (* Typage des tuples : on retourne juste le type produit
+ correspondant *)
| Etuple l ->
Tproduct (List.map (w env) l)
+ (* Typage des opérateurs : on unifie les types avec ceux attendus
+ et on retourne le type correspondant *)
| Ebinop (e1, OAnd, e2)
| Ebinop (e1, OOr, e2) ->
let t1 = w env e1
@@ -298,6 +339,12 @@ let rec w env e =
unify e.loc t Tint;
Tint
| Eletin (m, val_expr, body_expr) ->
+ (* Typage du let in :
+ * On type le motif et l'expression de la valeur assignée
+ * On unifie ces deux types
+ * On ajoute les identificateurs du motif à l'environnement
+ avec généralisation
+ * On calcule et retourne le type du corps du let in *)
let m_t = w_motif m
and val_t = w env val_expr
in
@@ -306,6 +353,11 @@ let rec w env e =
in
w env2 body_expr
| Efunc f when not f.recursive ->
+ (* Typage des fonctions non récursives :
+ * On type l'argument
+ * On l'ajoute sans généralisation à l'environnement
+ * On type le corps de la fonction
+ * On retourne arg_t -> return_t *)
let arg_t = w_motif f.arg
in
let env2 = add_motif env f.arg arg_t
@@ -313,7 +365,11 @@ let rec w env e =
let return_t = w env2 f.body
in
Tarrow (arg_t, return_t)
- | Efunc f -> (* f.recursive = true *)
+ | Efunc f -> (* f.recursive = true ici *)
+ (* Typage des fonctions récursives :
+ Comme pour les fonctions non récursives, avec en plus
+ l'ajout du nom de la fonction à l'environnement avant
+ l'ajout des identificateurs de l'argument *)
let arg_t = w_motif f.arg
and return_t = Tvar (V.create ())
in
@@ -329,6 +385,11 @@ let rec w env e =
unify f.body.loc (w env2 f.body) return_t;
Tarrow (arg_t, return_t)
| Eif (cond, then_expr, else_expr) ->
+ (* Typage des if :
+ * On type la condition et les deux expressions de retour
+ * On unifie le type de la condition avec bool
+ * On unifie les types des deux expressions de retour
+ * On retourne le type d'une des expressions de retour *)
let cond_t = w env cond
and then_t = w env then_expr
and else_t = w env else_expr
@@ -337,12 +398,20 @@ let rec w env e =
unify else_expr.loc else_t then_t;
then_t
| Elistcons (head, tail) ->
+ (* Typage des listcons :
+ * On type la tête et la queue
+ * On unifie (head_t list) et tail_t
+ * On retourne le type de la queue (ou head_t list) *)
let head_t = w env head
and tail_t = w env tail
in
unify head.loc (Tlist head_t) tail_t;
Tlist head_t
| Ecall (func_expr, arg) ->
+ (* Typage des calls :
+ * On type la fonction et son argument
+ * On unifie le type de la fonction avec argument -> 'a
+ * On retourne le type donné à 'a par unification *)
let func_t = w env func_expr
and arg_t = w env arg
and alpha_t = Tvar (V.create ())
@@ -350,6 +419,32 @@ let rec w env e =
unify func_expr.loc func_t (Tarrow (arg_t, alpha_t));
alpha_t
| Ematch (match_expr, empty_expr, head_m, tail_m, expr) ->
+ (* Typage du match :
+ * On type l'expression matchée, l'expression retournée
+ dans le cas où la liste est vide, on détermine un type
+ brut pour les motifs dans le cas non vide ;
+ * On réalise l'unification du type de l'expression matchée
+ et des motifs représentant la liste dans le cas non vide
+ * On met à jour l'environnement avec les identifieurs
+ éventuels des motifs du cas non vide
+ Question : dans la sémantique de ocaml, on ne généralise
+ pas ici, ce qui peut provoquer d'ennuyeux problèmes à cet
+ endroit, par exemple avec :
+ let _ =
+ match [(function x -> x)] with
+ [] -> ()
+ | id::l ->
+ let _ = print_int (id 42)
+ in
+ print_string (id "42")
+ Au contraire, généraliser empêcherait de correctement
+ typer certaines autres expressions, donc le comportement
+ à adopter est difficiler à déterminer
+ * On détermine le type de l'expression retournée dans le cas
+ non vide, et on l'unifie avec celui de l'expression dans
+ le cas vide
+ * On retourne le type de l'expression retournée dans le cas
+ non vide *)
let match_t = w env match_expr
and empty_t = w env empty_expr
and head_t = w_motif head_m
@@ -382,6 +477,8 @@ let rec w env e =
e.t <- Some t;
t
and w_motif m =
+ (* Type un motif, tout en vérifiant l'unicité des variables apparaîssant
+ dans le motif *)
let vars = ref Sset.empty
in
let rec aux m =
@@ -404,6 +501,7 @@ and w_motif m =
m.motif_t <- Some t;
t
+(* Environnement de base, contenant les primitives *)
let base_env =
add "print_int" (Tarrow (Tint, Tunit))
(add "print_string" (Tarrow (Tstring, Tunit))
@@ -411,5 +509,6 @@ let base_env =
(add "read_int" (Tarrow (Tunit, Tint))
(add "read_line" (Tarrow (Tunit, Tstring)) empty_env))))
+(* L'ultime helper : type un ast dans l'environnement de base *)
let type_ast a =
w base_env a