more detailspoly_meth

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

3 files changed, 104 insertions, 37 deletions

diff --git a/typing/ctype.mli b/typing/ctype.mli
index 0af1459594..67c27332b8 100644
--- a/typing/ctype.mli
+++ b/typing/ctype.mli
@@ -122,6 +122,9 @@ val unify: Env.t -> type_expr -> type_expr -> unit
         (* Unify the two types given. Raise [Unify] if not possible. *)
 val unify_strict: Env.t -> type_expr -> type_expr -> unit
         (* Same as [unify], but do not allow conjunctive types in variants. *)
+val unify_var: Env.t -> type_expr -> type_expr -> unit
+        (* Same as [unify], but allow free univars when first type
+           is a variable. *)
 val filter_arrow: Env.t -> type_expr -> label -> type_expr * type_expr
         (* A special case of unification (with l:'a -> 'b). *)
 val filter_method: Env.t -> string -> private_flag -> type_expr -> type_expr
diff --git a/typing/typetexp.ml b/typing/typetexp.ml
index 2a03711a3a..b890b7efa6 100644
--- a/typing/typetexp.ml
+++ b/typing/typetexp.ml
@@ -34,6 +34,8 @@ type error =
   | Present_has_conjunction of string
   | Present_has_no_type of string
   | Multiple_constructor of string
+  | No_row_variable of string
+  | Bad_alias of string
 
 exception Error of Location.t * error
 
@@ -41,7 +43,7 @@ exception Error of Location.t * error
 
 let type_variables = ref (Tbl.empty : (string, type_expr) Tbl.t)
 let saved_type_variables = ref ([] : (string, type_expr) Tbl.t list)
-let univars        = ref ([] : (string * type_expr ref) list)
+let univars        = ref ([] : (string * type_expr) list)
 let pre_univars    = ref ([] : type_expr list)
 
 let used_variables = ref (Tbl.empty : (string, type_expr) Tbl.t)
@@ -79,11 +81,29 @@ let type_variable loc name =
   with Not_found ->
     raise(Error(loc, Unbound_type_variable ("'" ^ name)))
 
-type policy = Fixed | Extensible | Delayed
+let wrap_method ty =
+  match (Ctype.repr ty).desc with
+    Tpoly _ -> ty
+  | _ -> Ctype.newty (Tpoly (ty, []))
 
-let rec transl_type env policy styp =
+let new_pre_univar () =
+  let v = newvar () in pre_univars := v :: !pre_univars; v
+
+let rec swap_list = function
+    x :: y :: l -> y :: x :: swap_list l
+  | l -> l
+
+type policy = Fixed | Extensible | Delayed | Univars
+
+let rec transl_type env policy rowvar styp =
+  if rowvar <> None then begin
+    match styp.ptyp_desc with
+      Ptyp_variant _ | Ptyp_object _ | Ptyp_class _ -> ()
+    | _ -> raise(Error(styp.ptyp_loc, No_row_variable ""))
+  end;
   match styp.ptyp_desc with
-    Ptyp_any -> Ctype.newvar ()
+    Ptyp_any ->
+      if policy = Univars then new_pre_univar () else newvar ()
   | Ptyp_var name ->
       begin try
 	List.assoc name !univars
@@ -128,11 +148,11 @@ let rec transl_type env policy styp =
             end
       end
   | Ptyp_arrow(l, st1, st2) ->
-      let ty1 = transl_type env policy st1 in
-      let ty2 = transl_type env policy st2 in
+      let ty1 = transl_type env policy None st1 in
+      let ty2 = transl_type env policy None st2 in
       newty (Tarrow(l, ty1, ty2))
   | Ptyp_tuple stl ->
-      newty (Ttuple(List.map (transl_type env policy) stl))
+      newty (Ttuple(List.map (transl_type env policy None) stl))
   | Ptyp_constr(lid, stl) ->
       let (path, decl) =
         try
@@ -142,7 +162,7 @@ let rec transl_type env policy styp =
       if List.length stl <> decl.type_arity then
         raise(Error(styp.ptyp_loc, Type_arity_mismatch(lid, decl.type_arity,
                                                            List.length stl)));
-      let args = List.map (transl_type env policy) stl in
+      let args = List.map (transl_type env policy None) stl in
       let params = List.map (fun _ -> Ctype.newvar ()) args in
       let cstr = newty (Tconstr(path, params, ref Mnil)) in
       begin try
@@ -152,14 +172,18 @@ let rec transl_type env policy styp =
       end;
       List.iter2
         (fun (sty, ty) ty' ->
-           try unify env ty ty' with Unify trace ->
-             raise (Error(sty.ptyp_loc, Type_mismatch trace)))
+           try unify_var env ty' ty with Unify trace ->
+             raise (Error(sty.ptyp_loc, Type_mismatch (swap_list trace))))
         (List.combine stl args) params;
       cstr
   | Ptyp_object fields ->
-      newobj (transl_fields env policy fields)
+      begin try
+	newobj (transl_fields env policy rowvar fields)
+      with Error (loc, No_row_variable _) when loc = Location.none ->
+	raise (Error(styp.ptyp_loc, No_row_variable "object "))
+      end
   | Ptyp_class(lid, stl, present) ->
-      if policy = Fixed then
+      if policy = Fixed & rowvar = None then
         raise(Error(styp.ptyp_loc, Unbound_row_variable lid));
       let (path, decl, is_variant) =
         try
@@ -185,8 +209,8 @@ let rec transl_type env policy styp =
       in
       if List.length stl <> decl.type_arity then
         raise(Error(styp.ptyp_loc, Type_arity_mismatch(lid, decl.type_arity,
-                                                           List.length stl)));
-      let args = List.map (transl_type env policy) stl in
+						       List.length stl)));
+      let args = List.map (transl_type env policy None) stl in
       let cstr = newty (Tconstr(path, args, ref Mnil)) in
       let ty =
         try Ctype.expand_head env cstr
@@ -196,8 +220,8 @@ let rec transl_type env policy styp =
       let params = Ctype.instance_list decl.type_params in
       List.iter2
         (fun (sty, ty') ty ->
-           try unify env ty' ty with Unify trace ->
-             raise (Error(sty.ptyp_loc, Type_mismatch trace)))
+           try unify_var env ty ty' with Unify trace ->
+             raise (Error(sty.ptyp_loc, Type_mismatch (swap_list trace))))
         (List.combine stl args) params;
       begin match ty.desc with
         Tvariant row ->
@@ -232,7 +256,7 @@ let rec transl_type env policy styp =
       else
         let ty' = new_global_var () in
         type_variables := Tbl.add alias ty' !type_variables;
-        let ty = transl_type env policy st in
+        let ty = transl_type env policy None st in
         begin try unify env ty ty' with Unify trace ->
           raise(Error(styp.ptyp_loc, Alias_type_mismatch trace))
         end;
@@ -256,9 +280,9 @@ let rec transl_type env policy styp =
               if List.length stl > 1 || c && stl <> [] then
                 raise(Error(styp.ptyp_loc, Present_has_conjunction l));
               match stl with [] -> Rpresent None
-              | st::_ -> Rpresent(Some(transl_type env policy st))
+              | st::_ -> Rpresent(Some(transl_type env policy None st))
             end else begin
-              let tl = List.map (transl_type env policy) stl in
+              let tl = List.map (transl_type env policy None) stl in
               bound := tl @ !bound;
               Reither(c, tl, ref None)
             end)
@@ -269,10 +293,19 @@ let rec transl_type env policy styp =
           raise(Error(styp.ptyp_loc, Present_has_no_type l)))
         present;
       let row =
-        { row_fields = fields; row_more = newvar ();
+        { row_fields = fields; row_more = newvar();
           row_bound = !bound; row_closed = closed; row_name = None } in
-      if policy = Fixed && not (Btype.static_row row) then
-        raise(Error(styp.ptyp_loc, Unbound_type_variable "[..]"));
+      let static = Btype.static_row row in
+      let row =
+        { row with row_more =
+            match rowvar with Some v -> v
+            | None ->
+	        if static then newty Tnil else
+	        if policy = Univars then new_pre_univar () else
+                if policy = Fixed && not static then
+                  raise(Error(styp.ptyp_loc, Unbound_type_variable "[..]"))
+	        else newvar ()
+        } in
       newty (Tvariant row)
   | Ptyp_poly(vars, st) ->
       (* aliases are stubs, in case one wants to redefine them *)
@@ -280,37 +313,56 @@ let rec transl_type env policy styp =
         List.map (fun name -> name, newty (Tlink (newty Tunivar))) vars in
       let old_univars = !univars in
       univars := ty_list @ !univars;
-      List.iter
-	(fun (alias, ty) ->
-	  if Tbl.mem alias !type_variables then
-            raise(Error(styp.ptyp_loc, Bound_type_variable alias));
-          aliases := Tbl.add alias (newty (Tlink ty)) !aliases)
-	vars ty_list;
       let ty = transl_type env policy None st in
       univars := old_univars;
-      newty (Tpoly(ty,ty_list))
+      newty (Tpoly(ty, List.map snd ty_list))
 
-and transl_fields env policy =
+and transl_fields env policy rowvar =
   function
     [] ->
       newty Tnil
   | {pfield_desc = Pfield_var} as field::_ ->
-      if policy = Fixed then
-        raise(Error(field.pfield_loc, Unbound_type_variable "<..>"));
-      newvar ()
+      begin match rowvar with
+	None ->
+	  if policy = Fixed then
+            raise(Error(field.pfield_loc, Unbound_type_variable ".."));
+	  if policy = Univars then new_pre_univar () else newvar ()
+      |	Some v -> v
+      end
   | {pfield_desc = Pfield(s, e)}::l ->
-      let ty1 = transl_type env policy e in
-      let ty2 = transl_fields env policy l in
+      let ty1 = transl_type env policy None e in
+      let ty2 = transl_fields env policy rowvar l in
         newty (Tfield (s, Fpresent, ty1, ty2))
 
 let transl_simple_type env fixed styp =
-  let typ = transl_type env (if fixed then Fixed else Extensible) styp in
+  univars := [];
+  let typ = transl_type env (if fixed then Fixed else Extensible) None styp in
   typ
 
+let transl_simple_type_univars env styp =
+  univars := [];
+  pre_univars := [];
+  begin_def ();
+  let typ = transl_type env Univars None styp in
+  end_def ();
+  generalize typ;
+  let univs = List.map repr !pre_univars in
+  pre_univars := [];
+  let univs =
+    List.fold_left
+      (fun acc v ->
+	if v.desc <> Tvar || v.level <> Btype.generic_level || List.memq v acc
+        then acc
+        else (v.desc <- Tunivar ; v :: acc))
+      [] univs
+  in
+  instance (Btype.newgenty (Tpoly (typ, univs)))
+
 let transl_simple_type_delayed env styp =
+  univars := [];
   used_variables := Tbl.empty;
   bindings := [];
-  let typ = transl_type env Delayed styp in
+  let typ = transl_type env Delayed None styp in
   let b = !bindings in
   used_variables := Tbl.empty;
   bindings := [];
@@ -373,3 +425,11 @@ let report_error ppf = function
       fprintf ppf "The present constructor %s has no type" l
   | Multiple_constructor l ->
       fprintf ppf "The variant constructor %s is multiply defined" l
+  | No_row_variable s ->
+      print_string "This ";
+      print_string s;
+      print_string "type has no row variable"
+  | Bad_alias name ->
+      print_string "The alias ";
+      print_string name;
+      print_string " cannot be used here. It captures universal variables."
diff --git a/typing/typetexp.mli b/typing/typetexp.mli
index b68de53c20..784dc27d4a 100644
--- a/typing/typetexp.mli
+++ b/typing/typetexp.mli
@@ -18,6 +18,8 @@ open Format;;
 
 val transl_simple_type:
         Env.t -> bool -> Parsetree.core_type -> Types.type_expr
+val transl_simple_type_univars:
+        Env.t -> Parsetree.core_type -> Types.type_expr
 val transl_simple_type_delayed:
         Env.t -> Parsetree.core_type -> Types.type_expr * (unit -> unit)
         (* Translate a type, but leave type variables unbound. Returns
@@ -45,6 +47,8 @@ type error =
   | Present_has_conjunction of string
   | Present_has_no_type of string
   | Multiple_constructor of string
+  | No_row_variable of string
+  | Bad_alias of string
 
 exception Error of Location.t * error