summaryrefslogtreecommitdiff
path: root/typing.ml
diff options
context:
space:
mode:
authorGuillaume Seguin <guillaume@segu.in>2009-01-12 02:59:43 +0100
committerGuillaume Seguin <guillaume@segu.in>2009-01-12 02:59:43 +0100
commit85b8dd76bb90ccac6292c59fd1b989320434b897 (patch)
tree20915032908d354ed60e75b09644b4ffe55682d5 /typing.ml
parent2dec387f350c80bb779dd82dabd32cac44655101 (diff)
downloadpetitcaml-85b8dd76bb90ccac6292c59fd1b989320434b897.tar.gz
petitcaml-85b8dd76bb90ccac6292c59fd1b989320434b897.tar.bz2
[petitcaml] typing.ml : Update and fix a bad bunch of bugs
Diffstat (limited to 'typing.ml')
-rw-r--r--typing.ml267
1 files changed, 162 insertions, 105 deletions
diff --git a/typing.ml b/typing.ml
index 45008c3..23fece0 100644
--- a/typing.ml
+++ b/typing.ml
@@ -8,8 +8,6 @@ module Int =
module Imap = Map.Make(Int)
-let next_id = ref 1
-
let rec head = function
| Tvar tvar ->
begin
@@ -43,7 +41,7 @@ let canon_string t tvar_names =
Printf.sprintf "%s * %s" base (canon_aux t))
(canon_aux t)
l
- | Tproduct _ -> failwith "Unreachable matching"
+ | Tproduct _ -> failwith "canon_aux : Unreachable matching"
| Tlist t ->
Printf.sprintf "%s list" (canon_aux t)
| Tvar tvar ->
@@ -61,6 +59,11 @@ let canon_string t tvar_names =
in
s, !tvar_names
+let print_canon_string t =
+ let s, _ = (canon_string t Imap.empty)
+ in
+ Printf.printf "%s\n" s
+
exception TypingFailure of loc option * string
let typing_error l err = raise (TypingFailure (l, err))
@@ -106,7 +109,7 @@ and unify_products loc p1 p2 =
| l, [] -> false
| t1::l1, t2::l2 ->
unify loc t1 t2;
- unify_products loc p1 p2
+ unify_products loc l1 l2
module V = struct
type t = tvar
@@ -116,20 +119,44 @@ end
module Vset = Set.Make(V)
-let rec fvars t =
- match head t with
- | Tarrow (t1, t2) -> Vset.union (fvars t1) (fvars t2)
- | Tproduct l ->
- List.fold_left
- (fun base t -> Vset.union base (fvars t)) Vset.empty l
- | Tlist t -> fvars t
- | Tvar tv -> Vset.singleton tv
- | _ -> Vset.empty (* Tint, Tstring, Tbool, Tunit *)
+let rec fvars = function
+ | Tint
+ | Tstring
+ | Tbool
+ | Tunit -> Vset.empty
+ | Tarrow (t1, t2) -> Vset.union (fvars t1) (fvars t2)
+ | Tproduct l ->
+ List.fold_left
+ (fun base t -> Vset.union base (fvars t)) Vset.empty l
+ | Tlist t -> fvars t
+ | Tvar { def = Some t } -> fvars t
+ | Tvar tv -> Vset.singleton tv
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 ()
+
+let rec print_type = function
+ | Tint -> "int"
+ | Tstring -> "string"
+ | Tbool -> "bool"
+ | Tunit -> "unit"
+ | Tarrow (t1, t2) -> Printf.sprintf "%s -> %s" (print_type t1) (print_type t2)
+ | Tproduct (t::l) ->
+ List.fold_left (fun base t ->
+ Printf.sprintf "%s * %s" base (print_type t))
+ (print_type t)
+ l
+ | Tproduct _ -> failwith "print_type : Unreachable matching"
+ | Tlist t ->
+ Printf.sprintf "%s list" (print_type t)
+ | Tvar { id = id ; def = Some t } ->
+ Printf.sprintf "var { %d : %s }" id (print_type t)
+ | Tvar tvar ->
+ Printf.sprintf "var %d" tvar.id
+
let empty_env = { bindings = Smap.empty ; fvars = Vset.empty }
let add ident t env =
@@ -137,46 +164,66 @@ let add ident t env =
fvars = Vset.union env.fvars (fvars t) }
let add_gen ident t env =
- let new_env_fvars =
- Vset.filter (function tv -> not (occur tv t)) env.fvars
+ let binding_vars = Vset.diff (fvars t) env.fvars
in
- let binding_vars = Vset.diff (fvars t) new_env_fvars
- in
- { bindings =
- Smap.add ident { vars = binding_vars ; typ = t } env.bindings;
- fvars = new_env_fvars }
+ { env with bindings = Smap.add ident
+ { vars = binding_vars ; typ = t }
+ env.bindings }
-let rec replace_var orig dest t =
- match head t with
- | Tarrow (t1, t2) ->
- Tarrow (replace_var orig dest t1, replace_var orig dest t2)
- | Tproduct l ->
- Tproduct (List.map (function t -> replace_var orig dest t) l)
- | Tlist t ->
- Tlist (replace_var orig dest t)
- | Tvar tv when tv.id = orig ->
- Tvar { id = dest ; def = tv.def }
- | t -> t
+let rec replace_var orig new_tv = function
+ | Tarrow (t1, t2) ->
+ Tarrow (replace_var orig new_tv t1, replace_var orig new_tv t2)
+ | Tproduct l ->
+ Tproduct (List.map (replace_var orig new_tv) l)
+ | Tlist t ->
+ Tlist (replace_var orig new_tv t)
+ | Tvar tv when tv.id = orig ->
+ new_tv
+ | Tvar { id = id ; def = Some t } ->
+ Tvar { id = id ; def = Some (replace_var orig new_tv t) }
+ | t -> t
let use_freshvar tv t =
- let new_t = replace_var tv.id !next_id t
- in
- incr next_id;
- new_t
+ replace_var tv.id (Tvar (V.create())) t
let find ident env =
let binding = Smap.find ident env.bindings
in
Vset.fold use_freshvar binding.vars binding.typ
-let alloc_tvar () =
- let new_t = Tvar { id = !next_id ; def = None }
- in
- incr next_id;
- new_t
-
module Sset = Set.Make(String)
+let rec motif_vars loc vars m =
+ match m.m with
+ | Munderscore -> vars
+ | Mident ident when Sset.mem ident vars ->
+ typing_error loc
+ (Printf.sprintf "Variable %s non unique \
+ dans ce motif" ident)
+ | Mident ident -> Sset.add ident vars
+ | Mtuple l -> List.fold_left (motif_vars loc) vars l
+
+let rec add_motif_base add_func env m t =
+ match m.m with
+ | Munderscore -> env
+ | Mident ident -> add_func ident t env
+ | Mtuple l ->
+ begin
+ match head t with
+ | Tproduct lp ->
+ List.fold_left2 (fun env m t -> add_motif_base add_func
+ env
+ m
+ t)
+ env
+ l
+ lp
+ | _ -> failwith "add_motif_base : Unreachable matching"
+ end
+
+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
+
let rec w env e =
let w_aux e =
match e.e with
@@ -194,61 +241,80 @@ let rec w env e =
| Econst (Cbool _) -> Tbool
| Econst Cunit -> Tunit
| Econst (Cemptylist) ->
- Tlist (alloc_tvar ())
+ Tlist (Tvar (V.create ()))
| Etuple l ->
Tproduct (List.map (w env) l)
- | Ebinop (e1, And, e2)
- | Ebinop (e1, Or, e2) ->
+ | Ebinop (e1, OAnd, e2)
+ | Ebinop (e1, OOr, e2) ->
let t1 = w env e1
and t2 = w env e2
in
unify e1.loc t1 Tbool;
unify e2.loc t2 Tbool;
Tbool
- | Ebinop (e1, Eq, e2)
- | Ebinop (e1, Neq, e2)
- | Ebinop (e1, Lt, e2)
- | Ebinop (e1, Le, e2)
- | Ebinop (e1, Gt, e2)
- | Ebinop (e1, Ge, e2) ->
+ | Ebinop (e1, OEq, e2)
+ | Ebinop (e1, ONeq, e2)
+ | Ebinop (e1, OLt, e2)
+ | Ebinop (e1, OLe, e2)
+ | Ebinop (e1, OGt, e2)
+ | Ebinop (e1, OGe, e2) ->
let t1 = w env e1
and t2 = w env e2
in
unify e1.loc t1 Tint;
unify e2.loc t2 Tint;
Tbool
- | Ebinop (e1, Add, e2)
- | Ebinop (e1, Sub, e2)
- | Ebinop (e1, Mul, e2)
- | Ebinop (e1, Div, e2) ->
+ | Ebinop (e1, OAdd, e2)
+ | Ebinop (e1, OSub, e2)
+ | Ebinop (e1, OMul, e2)
+ | Ebinop (e1, ODiv, e2) ->
let t1 = w env e1
and t2 = w env e2
in
unify e1.loc t1 Tint;
unify e2.loc t2 Tint;
Tint
- | Eunop (Not, e) ->
+ | Eunop (ONot, e) ->
let t = w env e
in
unify e.loc t Tbool;
Tbool
- | Eunop (Neg, e) ->
+ | Eunop (ONeg, e) ->
let t = w env e
in
unify e.loc t Tint;
Tint
| Eletin (m, val_expr, body_expr) ->
- let m_t, env2 = w_motif env m
+ let m_t = w_motif m
and val_t = w env val_expr
in
unify val_expr.loc m_t val_t;
- w env2 body_expr
- | Elistcons (head, tail) ->
- let head_t = w env head
- and tail_t = w env tail
+ let env2 = add_motif_gen env m val_t
+ in
+ w env2 body_expr
+ | Efunc f when not f.recursive ->
+ let arg_t = w_motif f.arg
in
- unify head.loc (Tlist head_t) tail_t;
- Tlist head_t
+ let env2 = add_motif env f.arg arg_t
+ in
+ let return_t = w env2 f.body
+ in
+ Tarrow (arg_t, return_t)
+ | Efunc f -> (* f.recursive = true *)
+ let arg_t = w_motif f.arg
+ and return_t = Tvar (V.create ())
+ in
+ let env2 = add_motif env f.arg arg_t
+ in
+ let env3 =
+ let fname = match f.name with
+ | Some name -> name
+ | None -> failwith "w : Unreachable matching"
+ in
+ add fname (Tarrow (arg_t, return_t)) env2
+ in
+ unify f.body.loc (w env3 f.body) return_t;
+ Tarrow (arg_t, return_t)
| Eif (cond, then_expr, else_expr) ->
let cond_t = w env cond
and then_t = w env then_expr
@@ -257,75 +323,68 @@ let rec w env e =
unify cond.loc cond_t Tbool;
unify else_expr.loc else_t then_t;
then_t
- | Efunc f when not f.recursive ->
- let arg_t, env2 = w_motif_func env f.arg
- in
- let return_t = w env2 f.body
- in
- Tarrow (arg_t, return_t)
- | Efunc f -> (* f.recursive = true *)
- let arg_t, env2 = w_motif_func env f.arg
- and return_t = alloc_tvar ()
+ | Elistcons (head, tail) ->
+ let head_t = w env head
+ and tail_t = w env tail
in
- let env3 =
- let fname = match f.name with
- | Some name -> name
- | None -> failwith "Unreachable matching"
- in
- add fname (Tarrow (arg_t, return_t)) env2
- in
- unify f.body.loc (w env3 f.body) return_t;
- Tarrow (arg_t, return_t)
+ unify head.loc (Tlist head_t) tail_t;
+ Tlist head_t
| Ecall (func_expr, arg) ->
let func_t = w env func_expr
and arg_t = w env arg
- and alpha_t = alloc_tvar ()
+ and alpha_t = Tvar (V.create ())
in
unify func_expr.loc func_t (Tarrow (arg_t, alpha_t));
alpha_t
| Ematch (match_expr, empty_expr, head_m, tail_m, expr) ->
let match_t = w env match_expr
and empty_t = w env empty_expr
- and alpha_t = alloc_tvar ()
+ and alpha_t = Tvar (V.create ())
in
unify match_expr.loc match_t (Tlist alpha_t);
- begin
- match tail_m.m with
- | Mtuple _ ->
- typing_error e.loc "Motif interdit dans le \
- filtrage de la queue de liste"
- | _ -> ()
- end;
- let head_t, env2 = w_motif env head_m
+ let vars_base =
+ match tail_m.m with
+ | Mtuple _ ->
+ typing_error e.loc "Motif interdit dans le \
+ filtrage de la queue de \
+ liste"
+ | Mident ident -> Sset.singleton ident
+ | Munderscore -> Sset.empty
+ and head_t = w_motif head_m
in
- let tail_t, env3 = w_motif env2 tail_m
+ let tail_t = w_motif tail_m
in
- let result_t = w env3 expr
+ let env2 = add_motif_gen (add_motif_gen env
+ head_m
+ head_t)
+ tail_m
+ tail_t
+ and _ = motif_vars e.loc vars_base head_m
in
- unify expr.loc result_t empty_t;
- result_t
- | Eclos _ -> failwith "Unreachable matching"
+ let result_t = w env2 expr
+ in
+ unify expr.loc result_t empty_t;
+ result_t
+ | Eclos _ -> failwith "w : Unreachable matching"
in
let t = w_aux e
in
e.t <- Some t;
t
-and w_motif_base add_func env m =
- let new_env = ref env
- and vars = ref Sset.empty
+and w_motif m =
+ let vars = ref Sset.empty
in
let rec aux m =
match m.m with
- | Munderscore -> alloc_tvar ()
+ | Munderscore -> Tvar (V.create ())
| Mident ident when Sset.mem ident !vars ->
typing_error m.motif_loc
(Printf.sprintf "Variable %s non unique \
dans ce motif" ident)
| Mident ident ->
- let t = alloc_tvar ()
+ let t = Tvar (V.create ())
in
vars := Sset.add ident !vars;
- new_env := add_func ident t (!new_env);
t
| Mtuple l ->
Tproduct (List.map aux l)
@@ -333,9 +392,7 @@ and w_motif_base add_func env m =
let t = aux m
in
m.motif_t <- Some t;
- (t, !new_env)
-and w_motif env m = w_motif_base add_gen env m
-and w_motif_func env m = w_motif_base add env m
+ t
let base_env =
add "print_int" (Tarrow (Tint, Tunit))