Mark expansive subexpressions and allow generalizing nonexpansive ones.mark_expansive

Idea from Francois Pottier.
Modifies: ctype, typecore, typeclass.


git-svn-id: http://caml.inria.fr/svn/ocaml/branches/mark_expansive@5311 f963ae5c-01c2-4b8c-9fe0-0dff7051ff02

4 files changed, 131 insertions, 73 deletions

diff --git a/typing/ctype.ml b/typing/ctype.ml
index 17c3f6e4ce..f8c76ad541 100644
--- a/typing/ctype.ml
+++ b/typing/ctype.ml
@@ -103,16 +103,26 @@ let global_level = ref 1
 let saved_level = ref []
 let saved_global_level = ref []
 
+(* Start type definitions *)
 let init_def level = current_level := level; nongen_level := level
-let begin_def () =
+(* Start a generalizable expression that may contain expansive parts *)
+(* Usage of levels:                                *)
+(*  nongen = current + 2 / current + 1             *)
+(*  gen = current + 3 / generic - 1                *)
+(* second ones are only used during generalization *)
+let begin_let_def () =
   saved_level := (!current_level, !nongen_level) :: !saved_level;
-  incr current_level; nongen_level := !current_level
-let begin_class_def () =
+  current_level := !current_level + 3;
+  nongen_level := !current_level - 1
+(* Start a pure generalizable expression *)
+let begin_def () =
   saved_level := (!current_level, !nongen_level) :: !saved_level;
   incr current_level
+(* Raise the non-generalizable level *)
 let raise_nongen_level () =
   saved_level := (!current_level, !nongen_level) :: !saved_level;
   nongen_level := !current_level
+(* End any of the above (except init_def) *)
 let end_def () =
   let (cl, nl) = List.hd !saved_level in
   saved_level := List.tl !saved_level;
@@ -617,36 +627,65 @@ let rec update_level env level ty =
     end
   end
 
-(* Generalize and lower levels of contravariant branches simultaneously *)
+(* 
+   Function [update_level] will never try to expand an abbreviation in
+   this case ([current_level] is greater than the binding time of any
+   type constructor path). So, it can be called with the empty
+   environnement.
+*)
+let make_nongen ty =
+  try
+    update_level Env.empty !nongen_level ty
+  with Unify [_, ty'] ->
+    raise (Unify [ty, ty'])
 
-let rec generalize_expansive env var_level ty =
+(*
+   New implementation of generalization, to be used with begin_let_def.
+   All potentially dangerous variables must have their level lowered
+   to !nongen_level beforehand using make_nongen.
+*)
+let rec generalize_let_def env ty =
   let ty = repr ty in
-  if ty.level <> generic_level then begin
-    if ty.level > var_level then begin
+  if ty.level < generic_level - 1 && ty.level > !current_level + 1 then begin
+    if ty.level >= !current_level + 3
+    then set_level ty (generic_level - 1)
+    else set_level ty (!current_level + 1);
+    match ty.desc with
+      Tconstr (path, tyl, abbrev) ->
+        let decl = Env.find_type path env in
+        abbrev := Mnil;
+        List.iter2
+          (fun (co,cn) t ->
+            if cn then generalize_let_cn env t
+            else generalize_let_def env t)
+          decl.type_variance tyl
+    | Tarrow (_, t1, t2, _) ->
+        generalize_let_cn env t1;
+        generalize_let_def env t2
+    | _ ->
+        iter_type_expr (generalize_let_def env) ty
+  end
+
+and generalize_let_cn env ty =
+  let ty = repr ty in
+  if ty.level <> generic_level && ty.level > !current_level then begin
+    if ty.level < !current_level + 3
+    then update_level env !nongen_level ty
+    else begin
       set_level ty generic_level;
-      match ty.desc with
-        Tconstr (path, tyl, abbrev) ->
-          let variance =
-            try (Env.find_type path env).type_variance
-            with Not_found -> List.map (fun _ -> (true,true)) tyl in
-          abbrev := Mnil;
-          List.iter2
-            (fun (co,cn) t ->
-              if cn then update_level env var_level t
-              else generalize_expansive env var_level t)
-            variance tyl
-      | Tarrow (_, t1, t2, _) ->
-          update_level env var_level t1;
-          generalize_expansive env var_level t2
-      | _ ->
-          iter_type_expr (generalize_expansive env var_level) ty
+      begin match ty.desc with
+        Tconstr (path, tyl, abbrev) -> abbrev := Mnil
+      | _ -> ()
+      end;
+      iter_type_expr (generalize_let_cn env) ty
     end
   end
 
-let generalize_expansive env ty =
+let generalize_let_def env ty =
   simple_abbrevs := Mnil;
   try
-    generalize_expansive env !nongen_level ty
+    generalize_let_def env ty;
+    generalize ty
   with Unify [_, ty'] ->
     raise (Unify [ty, ty'])
 
diff --git a/typing/ctype.mli b/typing/ctype.mli
index e0da260fcb..de453d25f8 100644
--- a/typing/ctype.mli
+++ b/typing/ctype.mli
@@ -27,12 +27,14 @@ exception Recursive_abbrev
 
 val init_def: int -> unit
         (* Set the initial variable level *)
+val begin_let_def: unit -> unit
+        (* Start a generalizable expression that may contain expansive parts *)
 val begin_def: unit -> unit
         (* Raise the variable level by one at the beginning of a definition. *)
-val end_def: unit -> unit
-        (* Lower the variable level by one at the end of a definition *)
-val begin_class_def: unit -> unit
 val raise_nongen_level: unit -> unit
+        (* Also raise non-generalizable target level *)
+val end_def: unit -> unit
+        (* Recover old levels at the end of a definition *)
 val reset_global_level: unit -> unit
         (* Reset the global level before typing an expression *)
 val increase_global_level: unit -> int
@@ -85,9 +87,11 @@ val generalize: type_expr -> unit
         (* Generalize in-place the given type *)
 val iterative_generalization: int -> type_expr list -> type_expr list
         (* Efficient repeated generalization of a type *)
-val generalize_expansive: Env.t -> type_expr -> unit
-        (* Generalize the covariant part of a type, making
-           contravariant branches non-generalizable *)
+val make_nongen: type_expr -> unit
+        (* Make non-generalizable the given type *)
+val generalize_let_def: Env.t -> type_expr -> unit
+        (* Generalize a let definition, making non-generalizable
+           contravariant branches marked by make_nongen *)
 val generalize_global: type_expr -> unit
         (* Generalize the structure of a type, lowering variables
            to !global_level *)
diff --git a/typing/typeclass.ml b/typing/typeclass.ml
index 3f616ca8ba..6721d057a3 100644
--- a/typing/typeclass.ml
+++ b/typing/typeclass.ml
@@ -414,13 +414,15 @@ let rec class_field cl_num self_type meths vars
   | Pcf_val (lab, mut, sexp, loc) ->
       if StringSet.mem lab inh_vals then
         Location.prerr_warning loc (Warnings.Hide_instance_variable lab);
-      if !Clflags.principal then Ctype.begin_def ();
+      if !Clflags.principal then begin
+        Ctype.raise_nongen_level (); Ctype.begin_def ()
+      end;
       let exp =
         try type_exp val_env sexp with Ctype.Unify [(ty, _)] ->
           raise(Error(loc, Make_nongen_seltype ty))
       in
       if !Clflags.principal then begin
-        Ctype.end_def ();
+        Ctype.end_def (); Ctype.end_def ();
         Ctype.generalize_structure exp.exp_type
       end;
       let (id, val_env, met_env, par_env) =
@@ -769,14 +771,14 @@ and class_expr cl_num val_env met_env scl =
       let (vals, met_env) =
         List.fold_right
           (fun id (vals, met_env) ->
-             Ctype.begin_def ();
+             Ctype.begin_let_def ();
              let expr =
                Typecore.type_exp val_env
                  {pexp_desc = Pexp_ident (Longident.Lident (Ident.name id));
                   pexp_loc = Location.none}
              in
              Ctype.end_def ();
-             Ctype.generalize expr.exp_type;
+             Ctype.generalize_let_def val_env expr.exp_type;
              let desc =
                {val_type = expr.exp_type; val_kind = Val_ivar (Immutable,
                                                                cl_num)}
@@ -793,7 +795,7 @@ and class_expr cl_num val_env met_env scl =
        cl_loc = scl.pcl_loc;
        cl_type = cl.cl_type}
   | Pcl_constraint (scl', scty) ->
-      Ctype.begin_class_def ();
+      Ctype.begin_def ();
       let context = Typetexp.narrow () in
       let cl = class_expr cl_num val_env met_env scl' in
       Typetexp.widen context;
@@ -912,7 +914,7 @@ let class_infos define_class kind
     (res, env) =
 
   reset_type_variables ();
-  Ctype.begin_class_def ();
+  Ctype.begin_def ();
   
   (* Introduce class parameters *)
   let params =
@@ -1182,7 +1184,7 @@ let type_classes define_class approx kind env cls =
       cls
   in
   Ctype.init_def (Ident.current_time ());
-  Ctype.begin_class_def ();
+  Ctype.begin_def ();
   let (res, env) =
     List.fold_left (initial_env define_class approx) ([], env) cls
   in
diff --git a/typing/typecore.ml b/typing/typecore.ml
index d6db977f2b..8f36e13256 100644
--- a/typing/typecore.ml
+++ b/typing/typecore.ml
@@ -788,18 +788,22 @@ let rec type_exp env sexp =
   | Pexp_function _ ->     (* defined in type_expect *)
       type_expect env sexp (newvar())
   | Pexp_apply(sfunct, sargs) ->
-      if !Clflags.principal then begin_def ();
+      if !Clflags.principal then (begin_def (); raise_nongen_level ());
       let funct = type_exp env sfunct in
       if !Clflags.principal then begin
-        end_def ();
+        end_def (); end_def ();
         generalize_structure funct.exp_type
       end;
       let (args, ty_res) = type_application env funct sargs in
       let funct = {funct with exp_type = instance funct.exp_type} in
-      { exp_desc = Texp_apply(funct, args);
-        exp_loc = sexp.pexp_loc;
-        exp_type = ty_res;
-        exp_env = env }
+      let res =
+        { exp_desc = Texp_apply(funct, args);
+          exp_loc = sexp.pexp_loc;
+          exp_type = ty_res;
+          exp_env = env }
+      in
+      if not (is_nonexpansive res) then make_nongen res.exp_type;
+      res
   | Pexp_match(sarg, caselist) ->
       let arg = type_exp env sarg in
       let ty_res = newvar() in
@@ -848,7 +852,7 @@ let rec type_exp env sexp =
             Env.lookup_label lid env
           with Not_found ->
             raise(Error(sexp.pexp_loc, Unbound_label lid)) in
-        begin_def ();
+        begin_let_def ();
         if !Clflags.principal then begin_def ();
         let (vars, ty_arg, ty_res) = instance_label true label in
         if !Clflags.principal then begin
@@ -863,11 +867,12 @@ let rec type_exp env sexp =
         end;
         let arg = type_argument env sarg ty_arg in
         end_def ();
-        if vars <> [] && not (is_nonexpansive arg) then
-          generalize_expansive env arg.exp_type;
+        generalize_let_def env arg.exp_type;
         check_univars env "field value" arg label.lbl_arg vars;
         num_fields := Array.length label.lbl_all;
-        (label, {arg with exp_type = instance arg.exp_type}) in
+        let ty_arg = instance arg.exp_type in
+        if label.lbl_mut = Mutable then make_nongen ty_arg;
+        (label, {arg with exp_type = ty_arg}) in
       let lbl_exp_list = List.map type_label_exp lid_sexp_list in
       let rec check_duplicates seen_pos lid_sexp lbl_exp =
         match (lid_sexp, lbl_exp) with
@@ -935,13 +940,12 @@ let rec type_exp env sexp =
           raise(Error(sexp.pexp_loc, Unbound_label lid)) in
       if label.lbl_mut = Immutable then
         raise(Error(sexp.pexp_loc, Label_not_mutable lid));
-      begin_def ();
+      begin_let_def ();
       let (vars, ty_arg, ty_res) = instance_label true label in
       unify_exp env record ty_res;
       let newval = type_expect env snewval ty_arg in
       end_def ();
-      if vars <> [] && not (is_nonexpansive newval) then
-        generalize_expansive env newval.exp_type;
+      generalize_let_def env newval.exp_type;
       check_univars env "field value" newval label.lbl_arg vars;
       { exp_desc = Texp_setfield(record, label, newval);
         exp_loc = sexp.pexp_loc;
@@ -950,6 +954,7 @@ let rec type_exp env sexp =
   | Pexp_array(sargl) ->
       let ty = newvar() in
       let argl = List.map (fun sarg -> type_expect env sarg ty) sargl in
+      make_nongen ty;
       { exp_desc = Texp_array argl;
         exp_loc = sexp.pexp_loc;
         exp_type = instance (Predef.type_array ty);
@@ -1057,7 +1062,7 @@ let rec type_exp env sexp =
         exp_type = body.exp_type;
         exp_env = env }
   | Pexp_send (e, met) ->
-      if !Clflags.principal then begin_def ();
+      if !Clflags.principal then begin_let_def ();
       let obj = type_exp env e in
       begin try
         let (exp, typ) =
@@ -1107,7 +1112,7 @@ let rec type_exp env sexp =
         in
         if !Clflags.principal then begin
           end_def ();
-          generalize_structure typ;
+          generalize_let_def env typ;
         end;
         let typ =
           match repr typ with
@@ -1128,10 +1133,11 @@ let rec type_exp env sexp =
           | _ ->
               assert false
         in
-          { exp_desc = exp;
-            exp_loc = sexp.pexp_loc;
-            exp_type = typ;
-            exp_env = env }
+        make_nongen typ;
+        { exp_desc = exp;
+          exp_loc = sexp.pexp_loc;
+          exp_type = typ;
+          exp_env = env }
       with Unify _ ->
         raise(Error(e.pexp_loc, Undefined_method (obj.exp_type, met)))
       end
@@ -1144,9 +1150,11 @@ let rec type_exp env sexp =
           None ->
             raise(Error(sexp.pexp_loc, Virtual_class cl))
         | Some ty ->
+            let ty_res = instance ty in
+            make_nongen ty_res;
             { exp_desc = Texp_new (cl_path, cl_decl);
               exp_loc = sexp.pexp_loc;
-              exp_type = instance ty;
+              exp_type = ty_res;
               exp_env = env }
         end
   | Pexp_setinstvar (lab, snewval) ->
@@ -1212,6 +1220,7 @@ let rec type_exp env sexp =
       let context = Typetexp.narrow () in
       let modl = !type_module env smodl in
       let (id, new_env) = Env.enter_module name modl.mod_type env in
+      raise_nongen_level ();
       Ctype.init_def(Ident.current_time());
       Typetexp.widen context;
       let body = type_exp new_env sbody in
@@ -1225,6 +1234,7 @@ let rec type_exp env sexp =
       with Unify _ ->
         raise(Error(sexp.pexp_loc, Scoping_let_module(name, body.exp_type)))
       end;
+      end_def ();
       { exp_desc = Texp_letmodule(id, modl, body);
         exp_loc = sexp.pexp_loc;
         exp_type = ty;
@@ -1268,11 +1278,11 @@ and type_argument env sarg ty_expected' =
   | {desc = Tarrow("",ty_arg,ty_res,_); level = lv}, _ ->
       (* apply optional arguments when expected type is "" *)
       (* we must be very careful about not breaking the semantics *)
-      if !Clflags.principal then begin_def ();
+      if !Clflags.principal then begin_let_def ();
       let texp = type_exp env sarg in
       if !Clflags.principal then begin
         end_def ();
-        generalize_structure texp.exp_type
+        generalize_let_def env texp.exp_type
       end;
       let rec make_args args ty_fun =
         match (expand_head env ty_fun).desc with
@@ -1337,9 +1347,10 @@ and type_application env funct sargs =
   let ignored = ref [] in
   let rec type_unknown_args args omitted ty_fun = function
       [] ->
+        let args = List.rev args in
         (List.map
            (function None, x -> None, x | Some f, x -> Some (f ()), x)
-           (List.rev args),
+           args,
          instance (result_type omitted ty_fun))
     | (l1, sarg1) :: sargl ->
         let (ty1, ty2) =
@@ -1595,9 +1606,11 @@ and type_expect ?in_function env sexp ty_expected =
         try unify env ty_arg (type_option(newvar()))
         with Unify _ -> assert false
       end;
+      raise_nongen_level ();
       let cases, partial =
         type_cases ~in_function:(loc,ty_fun) env ty_arg ty_res
           (Some sexp.pexp_loc) caselist in
+      end_def ();
       let all_labeled ty =
         let ls, tvar = list_labels env ty in
         not (tvar || List.exists (fun l -> l = "" || l.[0] = '?') ls)
@@ -1629,10 +1642,11 @@ and type_expect ?in_function env sexp ty_expected =
         | Tpoly (ty', tl) ->
             if sty <> None then set_type ty;
             (* One more level to generalize locally *)
-            begin_def ();
+            begin_def (); raise_nongen_level ();
             let vars, ty'' = instance_poly true tl ty' in
             let exp = type_expect env sbody ty'' in
-            end_def ();
+            end_def (); end_def ();
+            (* Pexp_poly is only used in protected (non-expansive) contexts *)
             check_univars env "method" exp ty_expected vars;
             { exp with exp_type = ty }
         | _ -> assert false
@@ -1713,7 +1727,7 @@ and type_cases ?in_function env ty_arg ty_res partial_loc caselist =
 (* Typing of let bindings *)
 
 and type_let env rec_flag spat_sexp_list =
-  begin_def();
+  begin_let_def();
   if !Clflags.principal then begin_def ();
   let (pat_list, new_env, force) =
     type_pattern_list env (List.map (fun (spat, sexp) -> spat) spat_sexp_list)
@@ -1743,13 +1757,9 @@ and type_let env rec_flag spat_sexp_list =
     (fun pat exp -> ignore(Parmatch.check_partial env pat.pat_loc [pat, exp]))
     pat_list exp_list;
   end_def();
-  List.iter2
-    (fun pat exp ->
-       if not (is_nonexpansive exp) then
-         iter_pattern (fun pat -> generalize_expansive env pat.pat_type) pat)
-    pat_list exp_list;
   List.iter
-    (fun pat -> iter_pattern (fun pat -> generalize pat.pat_type) pat)
+    (fun pat ->
+      iter_pattern (fun pat -> generalize_let_def env pat.pat_type) pat)
     pat_list;
   (List.combine pat_list exp_list, new_env)
 
@@ -1757,17 +1767,20 @@ and type_let env rec_flag spat_sexp_list =
 
 let type_binding env rec_flag spat_sexp_list =
   Typetexp.reset_type_variables();
+  begin_let_def ();
+  ignore (increase_global_level ());
+  end_def ();
   type_let env rec_flag spat_sexp_list
 
 (* Typing of toplevel expressions *)
 
 let type_expression env sexp =
   Typetexp.reset_type_variables();
-  begin_def();
+  begin_let_def();
+  ignore (increase_global_level ());
   let exp = type_exp env sexp in
   end_def();
-  if is_nonexpansive exp then generalize exp.exp_type
-  else generalize_expansive env exp.exp_type;
+  generalize_let_def env exp.exp_type;
   exp
 
 (* Error report *)