implement instance_sep, modify printtyp and typetexp

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

5 files changed, 216 insertions, 13 deletions

diff --git a/typing/ctype.ml b/typing/ctype.ml
index f41a51c8b6..12179f703f 100644
--- a/typing/ctype.ml
+++ b/typing/ctype.ml
@@ -703,6 +703,7 @@ let rec copy ty =
       end;
     t
 
+
 (**** Variants of instantiations ****)
 
 let instance sch =
@@ -759,6 +760,142 @@ let instance_class params cty =
   cleanup_types ();
   (params', cty')
 
+(**** Instanciation for types with free universal variables ****)
+
+module TypeHash = Hashtbl.Make(TypeOps)
+module TypeSet = Set.Make(TypeOps)
+
+let rec close_cycle ty cy = function
+    [] -> false
+  | (t, q, r) :: tl ->
+      if t == ty then (r := List.rev cy :: !r; true) else
+      close_cycle ty ((t, q)::cy) tl
+
+let type_hash_union ht ty s =
+  if TypeSet.is_empty s then () else
+  let s' =
+    try
+      let s0 = TypeHash.find ht ty in
+      TypeHash.remove ht ty;
+      TypeSet.union s0 s
+    with Not_found -> s
+  in
+  TypeHash.add ht ty s'
+
+let compute_univars ty =
+  let node_univars : TypeSet.t TypeHash.t = TypeHash.create 17 in
+  let rec free_rec visited ty =
+    let ty = repr ty in
+    if close_cycle ty [] visited then TypeSet.empty else
+    let cyr = ref [] in
+    let univars =
+      match ty.desc with
+	Tunivar ->
+          TypeSet.singleton ty
+      | Tpoly (ty, tyl) ->
+          let tyl = List.map repr tyl in
+          let visited = (ty, tyl, cyr) :: visited in
+          List.fold_right TypeSet.remove tyl (free_rec visited ty)
+      | _ ->
+          let visited = (ty, [], cyr) :: visited in
+          let r = ref TypeSet.empty in
+	  iter_type_expr
+            (fun t -> r := TypeSet.union !r (free_rec visited t))
+            ty;
+          !r
+    in
+    if not (TypeSet.is_empty univars) then begin
+      type_hash_union node_univars ty univars;
+      List.iter
+        (fun cy ->
+          ignore
+            (List.fold_left
+               (fun univars (ty, tyl) ->
+                 let univars = List.fold_right TypeSet.remove tyl univars in
+                 type_hash_union node_univars ty univars;
+                 univars)
+               univars cy))
+        !cyr
+    end;
+    univars
+  in
+  ignore (free_rec [] ty);
+  fun ty -> try TypeHash.find node_univars ty with Not_found -> TypeSet.empty
+
+let rec diff_list l1 l2 =
+  if l1 == l2 then [] else
+  match l1 with [] -> invalid_arg "Ctype.diff_list"
+  | a :: l1 -> a :: diff_list l1 l2
+
+let conflicts free bound =
+  let bound = List.map repr bound in
+  TypeSet.exists (fun t -> List.memq (repr t) bound) free
+
+let delayed_copy = ref []
+    (* copying to do later *)
+
+let rec copy_sep free bound visited ty =
+  let ty = repr ty in
+  let univars = free ty in
+  if TypeSet.is_empty univars then 
+    if ty.level <> generic_level then ty else
+    let t = newvar () in
+    delayed_copy :=
+      lazy (t.desc <- Tlink (copy ty))
+      :: !delayed_copy;
+    t
+  else try
+    let t, bound_t = List.assq ty visited in
+    let dl = diff_list bound bound_t in
+    if dl <> [] & conflicts univars dl then raise Not_found;
+    t
+  with Not_found -> begin
+    let t = newvar() in          (* Stub *)
+    let visited =
+      match ty.desc with
+	Tarrow _ | Ttuple _ | Tvariant _ | Tconstr _ | Tobject _ ->
+          (ty,(t,bound)) :: visited
+      |	_ -> visited in
+    t.desc <-
+      begin match ty.desc with
+      | Tconstr (p, tl, _) ->
+          begin match find_repr p !(!abbreviations) with
+            Some ty when repr ty != t ->
+              Tlink ty
+          | _ ->
+              Tconstr (p, List.map (copy_sep free bound visited) tl,
+                       ref (match !(!abbreviations) with
+                              Mcons _ -> Mlink !abbreviations
+                            | abbrev  -> abbrev))
+          end
+      | Tvariant row0 ->
+          let row = row_repr row0 in
+          (* We shall really check the level on the row variable *)
+          if (row_more row).level <> generic_level then Tvariant row else
+          Tvariant (copy_row (copy_sep free bound visited) row)
+      |	Tpoly (t1, tl) ->
+	  let tl = List.map repr tl in
+	  let tl' =
+	    List.map
+	      (fun t -> if t.level <> generic_level then t else newty Tunivar)
+	      tl in
+	  let bound = tl @ bound in
+	  let visited =
+	    List.map2 (fun ty t -> ty,(t,bound)) tl tl' @ visited in
+	  Tpoly (copy_sep free bound visited t1, tl')
+      | _ -> copy_type_desc (copy_sep free bound visited) ty.desc
+      end;
+    t
+  end
+
+let instance_sep sch =
+  delayed_copy := [];
+  let ty = copy_sep (compute_univars sch) [] [] sch in
+  List.iter Lazy.force !delayed_copy;
+  delayed_copy := [];
+  cleanup_types ();
+  ty
+
 (**** Instantiation with parameter substitution ****)
 
 let unify' = (* Forward declaration *)
@@ -2179,6 +2316,12 @@ let rec build_subtype env visited posi t =
         (t, false)
   | Tsubst _ | Tlink _ ->
       assert false
+  | Tpoly(t1, tl) ->
+      let (t1', c) = build_subtype env visited posi t1 in
+      if c then (new_global_ty (Tpoly(t1', tl)), true)
+      else (t, false)
+  | Tunivar ->
+      (t, false)
 
 let enlarge_type env ty =
   subtypes := [];
diff --git a/typing/printtyp.ml b/typing/printtyp.ml
index 2f6f6015ac..39113700a4 100644
--- a/typing/printtyp.ml
+++ b/typing/printtyp.ml
@@ -23,6 +23,16 @@ open Asttypes
 open Types
 open Btype
 
+(* Redefine it here since goal differs *)
+
+let rec opened_object ty =
+  match (repr ty).desc with
+    Tobject (t, _)     -> opened_object t
+  | Tfield(_, _, _, t) -> opened_object t
+  | Tvar               -> true
+  | Tunivar            -> true
+  | _                  -> false
+
 (* Print a long identifier *)
 
 let rec longident ppf = function
@@ -72,7 +82,11 @@ let name_of_type t =
 
 let check_name_of_type t = ignore(name_of_type t)
 
-let print_name_of_type ppf t = fprintf ppf "%s" (name_of_type t)
+let non_gen_mark sch ty =
+  if sch && ty.desc = Tvar && ty.level <> generic_level then "_" else "" 
+
+let print_name_of_type sch ppf t =
+  fprintf ppf "'%s%s" (non_gen_mark sch t) (name_of_type t)
 
 let visited_objects = ref ([] : type_expr list)
 let aliased = ref ([] : type_expr list)
@@ -139,6 +153,10 @@ let rec mark_loops_rec visited ty =
     | Tnil -> ()
     | Tsubst ty -> mark_loops_rec visited ty
     | Tlink _ -> fatal_error "Printtyp.mark_loops_rec (2)"
+    | Tpoly (ty, tyl) ->
+	List.iter (fun t -> add_alias (repr t)) tyl;
+	mark_loops_rec visited ty
+    | Tunivar -> ()
 
 let mark_loops ty =
   normalize_type Env.empty ty;
@@ -174,13 +192,12 @@ let rec typexp sch prio0 ppf ty =
   let ty = repr ty in
   let px = proxy ty in
   if List.mem_assq px !names then
-   let mark = if ty.desc = Tvar then non_gen_mark sch px else "" in
-   fprintf ppf "'%s%a" mark print_name_of_type px else
+    print_name_of_type sch ppf px else
 
   let pr_typ ppf prio =
    (match ty.desc with
     | Tvar ->
-        fprintf ppf "'%s%a" (non_gen_mark sch ty) print_name_of_type ty
+        print_name_of_type sch ppf ty
     | Tarrow(l, ty1, ty2) ->
         let pr_arrow l ty1 ppf ty2 =
           print_label ppf l;
@@ -258,12 +275,25 @@ let rec typexp sch prio0 ppf ty =
         typexp sch prio ppf ty
     | Tlink _ | Tnil | Tfield _ ->
         fatal_error "Printtyp.typexp"
+    | Tpoly (ty, []) ->
+	typexp sch prio ppf ty
+    | Tpoly (ty, tyl) ->
+        let pr_poly ppf =
+          fprintf ppf "%a.@ %a"
+            (print_list (print_name_of_type sch) (fun ppf -> fprintf ppf " "))
+            tyl
+            (typexp sch 3) ty in
+	if prio >= 1 then fprintf ppf "@[<1>(%t)@]" pr_poly
+        else fprintf ppf "@[%t@]" pr_poly
+    | Tunivar ->
+	print_name_of_type sch ppf ty
    ) in
   if is_aliased px then begin
     check_name_of_type px;
     if prio0 >= 1
-    then fprintf ppf "@[<1>(%a as '%a)@]" pr_typ 0 print_name_of_type px
-    else fprintf ppf "@[%a as '%a@]" pr_typ prio0 print_name_of_type px end
+    then fprintf ppf "@[<1>(%a as %a)@]" pr_typ 0 (print_name_of_type false) px
+    else fprintf ppf "@[%a as %a@]" pr_typ prio0 (print_name_of_type false) px
+  end
   else pr_typ ppf prio0
 
 and row_field sch ppf (l, f) =
@@ -306,26 +336,23 @@ and typobject sch ty fi ppf nm =
           Sort.list (fun (n, _) (n', _) -> n <= n') present_fields in
         typfields sch rest ppf sorted_fields in
       fprintf ppf "@[<2>< %a >@]" pr_fields fi
-  | Some (p, {desc = Tvar} :: tyl) ->
+  | Some (p, {desc = Tvar|Tunivar} :: tyl) ->
       fprintf ppf "@[%a%s#%a@]" (typargs sch) tyl (non_gen_mark sch ty) path p
   | _ ->
         fatal_error "Printtyp.typobject"
   end
 
-and non_gen_mark sch ty =
-    if sch && ty.level <> generic_level then "_" else "" 
-
 and typfields sch rest ppf = function
   | [] ->
       begin match rest.desc with
-      | Tvar -> fprintf ppf "%s.." (non_gen_mark sch rest)
+      | Tvar|Tunivar -> fprintf ppf "%s.." (non_gen_mark sch rest)
       | Tnil -> ()
       | _ -> fatal_error "typfields (1)"
       end
   | [(s, t)] ->
       fprintf ppf "%s : %a" s (typexp sch 0) t;
       begin match rest.desc with
-      | Tvar -> fprintf ppf ";@ "
+      | Tvar|Tunivar -> fprintf ppf ";@ "
       | Tnil -> ()
       | _ -> fatal_error "typfields (2)"
       end;
@@ -519,7 +546,7 @@ let rec perform_class_type sch params ppf = function
       let sty = repr sign.cty_self in
       let pr_param ppf sty =
        if is_aliased sty then
-        fprintf ppf "@ @[('%a)@]" print_name_of_type sty in
+        fprintf ppf "@ @[(%a)@]" (print_name_of_type false) sty in
 
       fprintf ppf "@[<hv 2>@[<2>object%a@]%a"
               pr_param sty
diff --git a/typing/types.ml b/typing/types.ml
index 82ec34cd3c..e2dabc1fa8 100644
--- a/typing/types.ml
+++ b/typing/types.ml
@@ -60,6 +60,13 @@ and field_kind =
   | Fpresent
   | Fabsent
 
+module TypeOps = struct
+  type t = type_expr
+  let compare t1 t2 = t1.id - t2.id
+  let hash t = t.id
+  let equal t1 t2 = t1 == t2
+end
+
 (* Maps of methods and instance variables *)
 
 module OrderedString = struct type t = string let compare = compare end
diff --git a/typing/types.mli b/typing/types.mli
index 095a063e19..86bd538817 100644
--- a/typing/types.mli
+++ b/typing/types.mli
@@ -60,6 +60,13 @@ and field_kind =
   | Fpresent
   | Fabsent
 
+module TypeOps : sig
+  type t = type_expr
+  val compare : t -> t -> int
+  val equal : t -> t -> bool
+  val hash : t -> int
+end
+
 (* Maps of methods and instance variables *)
 
 module Meths : Map.S with type key = string
diff --git a/typing/typetexp.ml b/typing/typetexp.ml
index 6fd71dd7bd..42a7d87ac3 100644
--- a/typing/typetexp.ml
+++ b/typing/typetexp.ml
@@ -262,6 +262,25 @@ let rec transl_type env policy styp =
       if policy = Fixed && not (Btype.static_row row) then
         raise(Error(styp.ptyp_loc, Unbound_type_variable "[..]"));
       newty (Tvariant row)
+  | Ptyp_poly(st, vars) ->
+      let ty_list = List.map (fun _ -> newty Tunivar) vars in
+      let old_univars = !univars in
+      univars := ty_list @ !univars;
+      begin_def ();
+      List.iter2
+	(fun alias ty ->
+	  if Tbl.mem alias !type_variables then
+            raise(Error(styp.ptyp_loc, Bound_type_variable alias));
+	  if Tbl.mem alias !aliases then
+            raise(Error(styp.ptyp_loc, Bound_type_variable alias));
+	  (* aliases are stubs, in case one wants to redefine them *)
+          aliases := Tbl.add alias (newty (Tlink ty)) !aliases)
+	vars ty_list;
+      end_def ();
+      let ty = transl_type env policy None st in
+      aliases := List.fold_right Tbl.remove vars !aliases;
+      univars := old_univars;
+      newty (Tpoly(ty,ty_list))
 
 and transl_fields env policy =
   function