3476 lines
116 KiB
OCaml
3476 lines
116 KiB
OCaml
(***********************************************************************)
|
|
(* *)
|
|
(* Objective Caml *)
|
|
(* *)
|
|
(* Xavier Leroy and Jerome Vouillon, projet Cristal, INRIA Rocquencourt*)
|
|
(* *)
|
|
(* Copyright 1996 Institut National de Recherche en Informatique et *)
|
|
(* en Automatique. All rights reserved. This file is distributed *)
|
|
(* under the terms of the Q Public License version 1.0. *)
|
|
(* *)
|
|
(***********************************************************************)
|
|
|
|
(* $Id$ *)
|
|
|
|
(* Operations on core types *)
|
|
|
|
open Misc
|
|
open Asttypes
|
|
open Types
|
|
open Btype
|
|
|
|
(*
|
|
Type manipulation after type inference
|
|
======================================
|
|
If one wants to manipulate a type after type inference (for
|
|
instance, during code generation or in the debugger), one must
|
|
first make sure that the type levels are correct, using the
|
|
function [correct_levels]. Then, this type can be correctely
|
|
manipulated by [apply], [expand_head] and [moregeneral].
|
|
*)
|
|
|
|
(*
|
|
General notes
|
|
=============
|
|
- As much sharing as possible should be kept : it makes types
|
|
smaller and better abbreviated.
|
|
When necessary, some sharing can be lost. Types will still be
|
|
printed correctly (+++ TO DO...), and abbreviations defined by a
|
|
class do not depend on sharing thanks to constrained
|
|
abbreviations. (Of course, even if some sharing is lost, typing
|
|
will still be correct.)
|
|
- All nodes of a type have a level : that way, one know whether a
|
|
node need to be duplicated or not when instantiating a type.
|
|
- Levels of a type are decreasing (generic level being considered
|
|
as greatest).
|
|
- The level of a type constructor is superior to the binding
|
|
time of its path.
|
|
- Recursive types without limitation should be handled (even if
|
|
there is still an occur check). This avoid treating specially the
|
|
case for objects, for instance. Furthermore, the occur check
|
|
policy can then be easily changed.
|
|
*)
|
|
|
|
(*
|
|
A faire
|
|
=======
|
|
- Revoir affichage des types.
|
|
- Etendre la portee d'un alias [... as 'a] a tout le type englobant.
|
|
- #-type implementes comme de vraies abreviations.
|
|
- Niveaux plus fins pour les identificateurs :
|
|
Champ [global] renomme en [level];
|
|
Niveau -1 : global
|
|
0 : module toplevel
|
|
1 : module contenu dans module toplevel
|
|
...
|
|
En fait, incrementer le niveau a chaque fois que l'on rentre dans
|
|
un module.
|
|
|
|
3 4 6
|
|
\ / /
|
|
1 2 5
|
|
\|/
|
|
0
|
|
|
|
[Subst] doit ecreter les niveaux (pour qu'un variable non
|
|
generalisable dans un module de niveau 2 ne se retrouve pas
|
|
generalisable lorsque l'on l'utilise au niveau 0).
|
|
|
|
- Traitement de la trace de l'unification separe de la fonction
|
|
[unify].
|
|
*)
|
|
|
|
(**** Errors ****)
|
|
|
|
exception Unify of (type_expr * type_expr) list
|
|
|
|
exception Tags of label * label
|
|
|
|
exception Subtype of
|
|
(type_expr * type_expr) list * (type_expr * type_expr) list
|
|
|
|
exception Cannot_expand
|
|
|
|
exception Cannot_apply
|
|
|
|
exception Recursive_abbrev
|
|
|
|
(**** Type level management ****)
|
|
|
|
let current_level = ref 0
|
|
let nongen_level = ref 0
|
|
let global_level = ref 1
|
|
let saved_level = ref []
|
|
|
|
let init_def level = current_level := level; nongen_level := level
|
|
let begin_def () =
|
|
saved_level := (!current_level, !nongen_level) :: !saved_level;
|
|
incr current_level; nongen_level := !current_level
|
|
let begin_class_def () =
|
|
saved_level := (!current_level, !nongen_level) :: !saved_level;
|
|
incr current_level
|
|
let raise_nongen_level () =
|
|
saved_level := (!current_level, !nongen_level) :: !saved_level;
|
|
nongen_level := !current_level
|
|
let end_def () =
|
|
let (cl, nl) = List.hd !saved_level in
|
|
saved_level := List.tl !saved_level;
|
|
current_level := cl; nongen_level := nl
|
|
|
|
let reset_global_level () =
|
|
global_level := !current_level + 1
|
|
let increase_global_level () =
|
|
let gl = !global_level in
|
|
global_level := !current_level;
|
|
gl
|
|
let restore_global_level gl =
|
|
global_level := gl
|
|
|
|
(**** Whether a path points to an object type (with hidden row variable) ****)
|
|
let is_object_type path =
|
|
let name =
|
|
match path with Path.Pident id -> Ident.name id
|
|
| Path.Pdot(_, s,_) -> s
|
|
| Path.Papply _ -> assert false
|
|
in name.[0] = '#'
|
|
|
|
(**** Abbreviations without parameters ****)
|
|
(* Shall reset after generalizing *)
|
|
let simple_abbrevs = ref Mnil
|
|
let proper_abbrevs path tl abbrev =
|
|
if !Clflags.principal || tl <> [] || is_object_type path then abbrev
|
|
else simple_abbrevs
|
|
|
|
(**** Some type creators ****)
|
|
|
|
(* Re-export generic type creators *)
|
|
|
|
let newty2 = Btype.newty2
|
|
let newty desc = newty2 !current_level desc
|
|
let new_global_ty desc = newty2 !global_level desc
|
|
|
|
let newvar () = newty2 !current_level Tvar
|
|
let newvar2 level = newty2 level Tvar
|
|
let new_global_var () = newty2 !global_level Tvar
|
|
|
|
let newobj fields = newty (Tobject (fields, ref None))
|
|
|
|
let newconstr path tyl = newty (Tconstr (path, tyl, ref Mnil))
|
|
|
|
let none = newty (Ttuple []) (* Clearly ill-formed type *)
|
|
|
|
(**** Representative of a type ****)
|
|
|
|
(* Re-export repr *)
|
|
let repr = repr
|
|
|
|
(**** Type maps ****)
|
|
|
|
module TypePairs =
|
|
Hashtbl.Make (struct
|
|
type t = type_expr * type_expr
|
|
let equal (t1, t1') (t2, t2') = (t1 == t2) && (t1' == t2')
|
|
let hash (t, t') = t.id + 93 * t'.id
|
|
end)
|
|
|
|
(**********************************************)
|
|
(* Miscellaneous operations on object types *)
|
|
(**********************************************)
|
|
|
|
|
|
(**** Object field manipulation. ****)
|
|
|
|
let dummy_method = "*dummy method*"
|
|
|
|
let object_fields ty =
|
|
match (repr ty).desc with
|
|
Tobject (fields, _) -> fields
|
|
| _ -> assert false
|
|
|
|
let flatten_fields ty =
|
|
let rec flatten l ty =
|
|
let ty = repr ty in
|
|
match ty.desc with
|
|
Tfield(s, k, ty1, ty2) ->
|
|
flatten ((s, k, ty1)::l) ty2
|
|
| _ ->
|
|
(l, ty)
|
|
in
|
|
let (l, r) = flatten [] ty in
|
|
(Sort.list (fun (n, _, _) (n', _, _) -> n < n') l, r)
|
|
|
|
let build_fields level =
|
|
List.fold_right
|
|
(fun (s, k, ty1) ty2 -> newty2 level (Tfield(s, k, ty1, ty2)))
|
|
|
|
let associate_fields fields1 fields2 =
|
|
let rec associate p s s' =
|
|
function
|
|
(l, []) ->
|
|
(List.rev p, (List.rev s) @ l, List.rev s')
|
|
| ([], l') ->
|
|
(List.rev p, List.rev s, (List.rev s') @ l')
|
|
| ((n, k, t)::r, (n', k', t')::r') when n = n' ->
|
|
associate ((n, k, t, k', t')::p) s s' (r, r')
|
|
| ((n, k, t)::r, ((n', k', t')::_ as l')) when n < n' ->
|
|
associate p ((n, k, t)::s) s' (r, l')
|
|
| (((n, k, t)::r as l), (n', k', t')::r') (* when n > n' *) ->
|
|
associate p s ((n', k', t')::s') (l, r')
|
|
in
|
|
associate [] [] [] (fields1, fields2)
|
|
|
|
(**** Check whether an object is open ****)
|
|
|
|
(* +++ Il faudra penser a eventuellement expanser l'abreviation *)
|
|
let rec object_row ty =
|
|
let ty = repr ty in
|
|
match ty.desc with
|
|
Tobject (t, _) -> object_row t
|
|
| Tfield(_, _, _, t) -> object_row t
|
|
| _ -> ty
|
|
|
|
let opened_object ty =
|
|
match (object_row ty).desc with
|
|
| Tvar -> true
|
|
| Tunivar -> true
|
|
| Tconstr _ -> true
|
|
| _ -> false
|
|
|
|
(**** Close an object ****)
|
|
|
|
let close_object ty =
|
|
let rec close ty =
|
|
let ty = repr ty in
|
|
match ty.desc with
|
|
Tvar ->
|
|
link_type ty (newty2 ty.level Tnil)
|
|
| Tfield(_, _, _, ty') -> close ty'
|
|
| _ -> assert false
|
|
in
|
|
match (repr ty).desc with
|
|
Tobject (ty, _) -> close ty
|
|
| _ -> assert false
|
|
|
|
(**** Row variable of an object type ****)
|
|
|
|
let row_variable ty =
|
|
let rec find ty =
|
|
let ty = repr ty in
|
|
match ty.desc with
|
|
Tfield (_, _, _, ty) -> find ty
|
|
| Tvar -> ty
|
|
| _ -> assert false
|
|
in
|
|
match (repr ty).desc with
|
|
Tobject (fi, _) -> find fi
|
|
| _ -> assert false
|
|
|
|
(**** Object name manipulation ****)
|
|
(* +++ Bientot obsolete *)
|
|
|
|
let set_object_name id rv params ty =
|
|
match (repr ty).desc with
|
|
Tobject (fi, nm) ->
|
|
set_name nm (Some (Path.Pident id, rv::params))
|
|
| _ ->
|
|
assert false
|
|
|
|
let remove_object_name ty =
|
|
match (repr ty).desc with
|
|
Tobject (_, nm) -> set_name nm None
|
|
| Tconstr (_, _, _) -> ()
|
|
| _ -> fatal_error "Ctype.remove_object_name"
|
|
|
|
(**** Hiding of private methods ****)
|
|
|
|
let hide_private_methods ty =
|
|
match (repr ty).desc with
|
|
Tobject (fi, nm) ->
|
|
nm := None;
|
|
let (fl, _) = flatten_fields fi in
|
|
List.iter
|
|
(function (_, k, _) ->
|
|
match field_kind_repr k with
|
|
Fvar r -> set_kind r Fabsent
|
|
| _ -> ())
|
|
fl
|
|
| _ ->
|
|
assert false
|
|
|
|
|
|
(*******************************)
|
|
(* Operations on class types *)
|
|
(*******************************)
|
|
|
|
|
|
let rec signature_of_class_type =
|
|
function
|
|
Tcty_constr (_, _, cty) -> signature_of_class_type cty
|
|
| Tcty_signature sign -> sign
|
|
| Tcty_fun (_, ty, cty) -> signature_of_class_type cty
|
|
|
|
let self_type cty =
|
|
repr (signature_of_class_type cty).cty_self
|
|
|
|
let rec class_type_arity =
|
|
function
|
|
Tcty_constr (_, _, cty) -> class_type_arity cty
|
|
| Tcty_signature _ -> 0
|
|
| Tcty_fun (_, _, cty) -> 1 + class_type_arity cty
|
|
|
|
|
|
(*******************************************)
|
|
(* Miscellaneous operations on row types *)
|
|
(*******************************************)
|
|
|
|
let sort_row_fields = Sort.list (fun (p,_) (q,_) -> p < q)
|
|
|
|
let rec merge_rf r1 r2 pairs fi1 fi2 =
|
|
match fi1, fi2 with
|
|
(l1,f1 as p1)::fi1', (l2,f2 as p2)::fi2' ->
|
|
if l1 = l2 then merge_rf r1 r2 ((l1,f1,f2)::pairs) fi1' fi2' else
|
|
if l1 < l2 then merge_rf (p1::r1) r2 pairs fi1' fi2 else
|
|
merge_rf r1 (p2::r2) pairs fi1 fi2'
|
|
| [], _ -> (List.rev r1, List.rev_append r2 fi2, pairs)
|
|
| _, [] -> (List.rev_append r1 fi1, List.rev r2, pairs)
|
|
|
|
let merge_row_fields fi1 fi2 =
|
|
match fi1, fi2 with
|
|
[], _ | _, [] -> (fi1, fi2, [])
|
|
| [p1], _ when not (List.mem_assoc (fst p1) fi2) -> (fi1, fi2, [])
|
|
| _, [p2] when not (List.mem_assoc (fst p2) fi1) -> (fi1, fi2, [])
|
|
| _ -> merge_rf [] [] [] (sort_row_fields fi1) (sort_row_fields fi2)
|
|
|
|
let rec filter_row_fields erase = function
|
|
[] -> []
|
|
| (l,f as p)::fi ->
|
|
let fi = filter_row_fields erase fi in
|
|
match row_field_repr f with
|
|
Rabsent -> fi
|
|
| Reither(_,_,false,e) when erase -> set_row_field e Rabsent; fi
|
|
| _ -> p :: fi
|
|
|
|
(**************************************)
|
|
(* Check genericity of type schemes *)
|
|
(**************************************)
|
|
|
|
|
|
exception Non_closed
|
|
|
|
let rec closed_schema_rec ty =
|
|
let ty = repr ty in
|
|
if ty.level >= lowest_level then begin
|
|
let level = ty.level in
|
|
ty.level <- pivot_level - level;
|
|
match ty.desc with
|
|
Tvar when level <> generic_level ->
|
|
raise Non_closed
|
|
| Tfield(_, kind, t1, t2) ->
|
|
if field_kind_repr kind = Fpresent then
|
|
closed_schema_rec t1;
|
|
closed_schema_rec t2
|
|
| Tvariant row ->
|
|
let row = row_repr row in
|
|
iter_row closed_schema_rec row;
|
|
if not (static_row row) then closed_schema_rec row.row_more
|
|
| _ ->
|
|
iter_type_expr closed_schema_rec ty
|
|
end
|
|
|
|
(* Return whether all variables of type [ty] are generic. *)
|
|
let closed_schema ty =
|
|
try
|
|
closed_schema_rec ty;
|
|
unmark_type ty;
|
|
true
|
|
with Non_closed ->
|
|
unmark_type ty;
|
|
false
|
|
|
|
exception Non_closed of type_expr * bool
|
|
|
|
let free_variables = ref []
|
|
let really_closed = ref None
|
|
|
|
let rec free_vars_rec real ty =
|
|
let ty = repr ty in
|
|
if ty.level >= lowest_level then begin
|
|
ty.level <- pivot_level - ty.level;
|
|
begin match ty.desc, !really_closed with
|
|
Tvar, _ ->
|
|
free_variables := (ty, real) :: !free_variables
|
|
| Tconstr (path, tl, _), Some env ->
|
|
begin try
|
|
let (_, body) = Env.find_type_expansion path env in
|
|
if (repr body).level <> generic_level then
|
|
free_variables := (ty, real) :: !free_variables
|
|
with Not_found -> ()
|
|
end;
|
|
List.iter (free_vars_rec true) tl
|
|
(* Do not count "virtual" free variables
|
|
| Tobject(ty, {contents = Some (_, p)}) ->
|
|
free_vars_rec false ty; List.iter (free_vars_rec true) p
|
|
*)
|
|
| Tobject (ty, _), _ ->
|
|
free_vars_rec false ty
|
|
| Tfield (_, _, ty1, ty2), _ ->
|
|
free_vars_rec true ty1; free_vars_rec false ty2
|
|
| Tvariant row, _ ->
|
|
let row = row_repr row in
|
|
iter_row (free_vars_rec true) row;
|
|
if not (static_row row) then free_vars_rec false row.row_more
|
|
| _ ->
|
|
iter_type_expr (free_vars_rec true) ty
|
|
end;
|
|
end
|
|
|
|
let free_vars ?env ty =
|
|
free_variables := [];
|
|
really_closed := env;
|
|
free_vars_rec true ty;
|
|
let res = !free_variables in
|
|
free_variables := [];
|
|
really_closed := None;
|
|
res
|
|
|
|
let free_variables ?env ty =
|
|
let tl = List.map fst (free_vars ?env ty) in
|
|
unmark_type ty;
|
|
tl
|
|
|
|
let rec closed_type ty =
|
|
match free_vars ty with
|
|
[] -> ()
|
|
| (v, real) :: _ -> raise (Non_closed (v, real))
|
|
|
|
let closed_parameterized_type params ty =
|
|
List.iter mark_type params;
|
|
let ok =
|
|
try closed_type ty; true with Non_closed _ -> false in
|
|
List.iter unmark_type params;
|
|
unmark_type ty;
|
|
ok
|
|
|
|
let closed_type_decl decl =
|
|
try
|
|
List.iter mark_type decl.type_params;
|
|
begin match decl.type_kind with
|
|
Type_abstract ->
|
|
()
|
|
| Type_variant v ->
|
|
List.iter (fun (_, tyl) -> List.iter closed_type tyl) v
|
|
| Type_record(r, rep) ->
|
|
List.iter (fun (_, _, ty) -> closed_type ty) r
|
|
end;
|
|
begin match decl.type_manifest with
|
|
None -> ()
|
|
| Some ty -> closed_type ty
|
|
end;
|
|
unmark_type_decl decl;
|
|
None
|
|
with Non_closed (ty, _) ->
|
|
unmark_type_decl decl;
|
|
Some ty
|
|
|
|
type closed_class_failure =
|
|
CC_Method of type_expr * bool * string * type_expr
|
|
| CC_Value of type_expr * bool * string * type_expr
|
|
|
|
exception Failure of closed_class_failure
|
|
|
|
let closed_class params sign =
|
|
let ty = object_fields (repr sign.cty_self) in
|
|
let (fields, rest) = flatten_fields ty in
|
|
List.iter mark_type params;
|
|
mark_type rest;
|
|
List.iter
|
|
(fun (lab, _, ty) -> if lab = dummy_method then mark_type ty)
|
|
fields;
|
|
try
|
|
mark_type_node (repr sign.cty_self);
|
|
List.iter
|
|
(fun (lab, kind, ty) ->
|
|
if field_kind_repr kind = Fpresent then
|
|
try closed_type ty with Non_closed (ty0, real) ->
|
|
raise (Failure (CC_Method (ty0, real, lab, ty))))
|
|
fields;
|
|
mark_type_params (repr sign.cty_self);
|
|
List.iter unmark_type params;
|
|
unmark_class_signature sign;
|
|
None
|
|
with Failure reason ->
|
|
mark_type_params (repr sign.cty_self);
|
|
List.iter unmark_type params;
|
|
unmark_class_signature sign;
|
|
Some reason
|
|
|
|
|
|
(**********************)
|
|
(* Type duplication *)
|
|
(**********************)
|
|
|
|
|
|
(* Duplicate a type, preserving only type variables *)
|
|
let duplicate_type ty =
|
|
Subst.type_expr Subst.identity ty
|
|
|
|
(* Same, for class types *)
|
|
let duplicate_class_type ty =
|
|
Subst.class_type Subst.identity ty
|
|
|
|
|
|
(*****************************)
|
|
(* Type level manipulation *)
|
|
(*****************************)
|
|
|
|
(*
|
|
It would be a bit more efficient to remove abbreviation expansions
|
|
rather than generalizing them: these expansions will usually not be
|
|
used anymore. However, this is not possible in the general case, as
|
|
[expand_abbrev] (via [subst]) requires these expansions to be
|
|
preserved. Does it worth duplicating this code ?
|
|
*)
|
|
let rec iter_generalize tyl ty =
|
|
let ty = repr ty in
|
|
if (ty.level > !current_level) && (ty.level <> generic_level) then begin
|
|
set_level ty generic_level;
|
|
begin match ty.desc with
|
|
Tconstr (_, _, abbrev) ->
|
|
iter_abbrev (iter_generalize tyl) !abbrev
|
|
| _ -> ()
|
|
end;
|
|
iter_type_expr (iter_generalize tyl) ty
|
|
end else
|
|
tyl := ty :: !tyl
|
|
|
|
let iter_generalize tyl ty =
|
|
simple_abbrevs := Mnil;
|
|
iter_generalize tyl ty
|
|
|
|
let generalize ty =
|
|
iter_generalize (ref []) ty
|
|
|
|
(* Efficient repeated generalisation of the same type *)
|
|
let iterative_generalization min_level tyl =
|
|
let tyl' = ref [] in
|
|
List.iter (iter_generalize tyl') tyl;
|
|
List.fold_right (fun ty l -> if ty.level <= min_level then l else ty::l)
|
|
!tyl' []
|
|
|
|
(* Generalize the structure and lower the variables *)
|
|
|
|
let rec generalize_structure var_level ty =
|
|
let ty = repr ty in
|
|
if ty.level <> generic_level then begin
|
|
if ty.desc = Tvar && ty.level > var_level then
|
|
set_level ty var_level
|
|
else if ty.level > !current_level then begin
|
|
set_level ty generic_level;
|
|
begin match ty.desc with
|
|
Tconstr (_, _, abbrev) -> abbrev := Mnil
|
|
| _ -> ()
|
|
end;
|
|
iter_type_expr (generalize_structure var_level) ty
|
|
end
|
|
end
|
|
|
|
let generalize_structure var_level ty =
|
|
simple_abbrevs := Mnil;
|
|
generalize_structure var_level ty
|
|
|
|
(* let generalize_expansive ty = generalize_structure !nongen_level ty *)
|
|
let generalize_global ty = generalize_structure !global_level ty
|
|
let generalize_structure ty = generalize_structure !current_level ty
|
|
|
|
(* Generalize the spine of a function, if the level >= !current_level *)
|
|
|
|
let rec generalize_spine ty =
|
|
let ty = repr ty in
|
|
if ty.level < !current_level || ty.level = generic_level then () else
|
|
match ty.desc with
|
|
Tarrow (_, _, ty', _) | Tpoly (ty', _) ->
|
|
set_level ty generic_level;
|
|
generalize_spine ty'
|
|
| _ -> ()
|
|
|
|
let forward_try_expand_once = (* Forward declaration *)
|
|
ref (fun env ty -> raise Cannot_expand)
|
|
|
|
(*
|
|
Lower the levels of a type (assume [level] is not
|
|
[generic_level]).
|
|
*)
|
|
(*
|
|
The level of a type constructor must be greater than its binding
|
|
time. That way, a type constructor cannot escape the scope of its
|
|
definition, as would be the case in
|
|
let x = ref []
|
|
module M = struct type t let _ = (x : t list ref) end
|
|
(without this constraint, the type system would actually be unsound.)
|
|
*)
|
|
let rec update_level env level ty =
|
|
let ty = repr ty in
|
|
if ty.level > level then begin
|
|
begin match ty.desc with
|
|
Tconstr(p, tl, abbrev) when level < Path.binding_time p ->
|
|
(* Try first to replace an abbreviation by its expansion. *)
|
|
begin try
|
|
link_type ty (!forward_try_expand_once env ty);
|
|
update_level env level ty
|
|
with Cannot_expand ->
|
|
(* +++ Levels should be restored... *)
|
|
raise (Unify [(ty, newvar2 level)])
|
|
end
|
|
| Tpackage (p, _, _) when level < Path.binding_time p ->
|
|
raise (Unify [(ty, newvar2 level)])
|
|
| Tobject(_, ({contents=Some(p, tl)} as nm))
|
|
when level < Path.binding_time p ->
|
|
set_name nm None;
|
|
update_level env level ty
|
|
| Tvariant row ->
|
|
let row = row_repr row in
|
|
begin match row.row_name with
|
|
| Some (p, tl) when level < Path.binding_time p ->
|
|
log_type ty;
|
|
ty.desc <- Tvariant {row with row_name = None}
|
|
| _ -> ()
|
|
end;
|
|
set_level ty level;
|
|
iter_type_expr (update_level env level) ty
|
|
| Tfield(lab, _, _, _) when lab = dummy_method ->
|
|
raise (Unify [(ty, newvar2 level)])
|
|
| _ ->
|
|
set_level ty level;
|
|
(* XXX what about abbreviations in Tconstr ? *)
|
|
iter_type_expr (update_level env level) ty
|
|
end
|
|
end
|
|
|
|
(* Generalize and lower levels of contravariant branches simultaneously *)
|
|
|
|
let rec generalize_expansive env var_level ty =
|
|
let ty = repr ty in
|
|
if ty.level <> generic_level then begin
|
|
if ty.level > var_level then 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,true)) tyl in
|
|
abbrev := Mnil;
|
|
List.iter2
|
|
(fun (co,cn,ct) t ->
|
|
if ct then update_level env var_level t
|
|
else generalize_expansive env var_level t)
|
|
variance tyl
|
|
| Tpackage (_, _, tyl) ->
|
|
List.iter (update_level env var_level) 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
|
|
end
|
|
end
|
|
|
|
let generalize_expansive env ty =
|
|
simple_abbrevs := Mnil;
|
|
try
|
|
generalize_expansive env !nongen_level ty
|
|
with Unify [_, ty'] ->
|
|
raise (Unify [ty, ty'])
|
|
|
|
(* Correct the levels of type [ty]. *)
|
|
let correct_levels ty =
|
|
duplicate_type ty
|
|
|
|
(* Only generalize the type ty0 in ty *)
|
|
let limited_generalize ty0 ty =
|
|
let ty0 = repr ty0 in
|
|
|
|
let graph = Hashtbl.create 17 in
|
|
let idx = ref lowest_level in
|
|
let roots = ref [] in
|
|
|
|
let rec inverse pty ty =
|
|
let ty = repr ty in
|
|
if (ty.level > !current_level) || (ty.level = generic_level) then begin
|
|
decr idx;
|
|
Hashtbl.add graph !idx (ty, ref pty);
|
|
if (ty.level = generic_level) || (ty == ty0) then
|
|
roots := ty :: !roots;
|
|
set_level ty !idx;
|
|
iter_type_expr (inverse [ty]) ty
|
|
end else if ty.level < lowest_level then begin
|
|
let (_, parents) = Hashtbl.find graph ty.level in
|
|
parents := pty @ !parents
|
|
end
|
|
|
|
and generalize_parents ty =
|
|
let idx = ty.level in
|
|
if idx <> generic_level then begin
|
|
set_level ty generic_level;
|
|
List.iter generalize_parents !(snd (Hashtbl.find graph idx));
|
|
(* Special case for rows: must generalize the row variable *)
|
|
match ty.desc with
|
|
Tvariant row ->
|
|
let more = row_more row in
|
|
let lv = more.level in
|
|
if (lv < lowest_level || lv > !current_level)
|
|
&& lv <> generic_level then set_level more generic_level
|
|
| _ -> ()
|
|
end
|
|
in
|
|
|
|
inverse [] ty;
|
|
if ty0.level < lowest_level then
|
|
iter_type_expr (inverse []) ty0;
|
|
List.iter generalize_parents !roots;
|
|
Hashtbl.iter
|
|
(fun _ (ty, _) ->
|
|
if ty.level <> generic_level then set_level ty !current_level)
|
|
graph
|
|
|
|
|
|
(*******************)
|
|
(* Instantiation *)
|
|
(*******************)
|
|
|
|
|
|
let rec find_repr p1 =
|
|
function
|
|
Mnil ->
|
|
None
|
|
| Mcons (Public, p2, ty, _, _) when Path.same p1 p2 ->
|
|
Some ty
|
|
| Mcons (_, _, _, _, rem) ->
|
|
find_repr p1 rem
|
|
| Mlink {contents = rem} ->
|
|
find_repr p1 rem
|
|
|
|
(*
|
|
Generic nodes are duplicated, while non-generic nodes are left
|
|
as-is.
|
|
During instantiation, the description of a generic node is first
|
|
replaced by a link to a stub ([Tsubst (newvar ())]). Once the
|
|
copy is made, it replaces the stub.
|
|
After instantiation, the description of generic node, which was
|
|
stored by [save_desc], must be put back, using [cleanup_types].
|
|
*)
|
|
|
|
let abbreviations = ref (ref Mnil)
|
|
(* Abbreviation memorized. *)
|
|
|
|
let rec copy ty =
|
|
let ty = repr ty in
|
|
match ty.desc with
|
|
Tsubst ty -> ty
|
|
| _ ->
|
|
if ty.level <> generic_level then ty else
|
|
let desc = ty.desc in
|
|
save_desc ty desc;
|
|
let t = newvar() in (* Stub *)
|
|
ty.desc <- Tsubst t;
|
|
t.desc <-
|
|
begin match desc with
|
|
| Tconstr (p, tl, _) ->
|
|
let abbrevs = proper_abbrevs p tl !abbreviations in
|
|
begin match find_repr p !abbrevs with
|
|
Some ty when repr ty != t -> (* XXX Commentaire... *)
|
|
Tlink ty
|
|
| _ ->
|
|
(*
|
|
One must allocate a new reference, so that abbrevia-
|
|
tions belonging to different branches of a type are
|
|
independent.
|
|
Moreover, a reference containing a [Mcons] must be
|
|
shared, so that the memorized expansion of an abbrevi-
|
|
ation can be released by changing the content of just
|
|
one reference.
|
|
*)
|
|
Tconstr (p, List.map copy tl,
|
|
ref (match !(!abbreviations) with
|
|
Mcons _ -> Mlink !abbreviations
|
|
| abbrev -> abbrev))
|
|
end
|
|
| Tvariant row0 ->
|
|
let row = row_repr row0 in
|
|
let more = repr row.row_more in
|
|
(* We must substitute in a subtle way *)
|
|
(* Tsubst takes a tuple containing the row var and the variant *)
|
|
begin match more.desc with
|
|
Tsubst {desc = Ttuple [_;ty2]} ->
|
|
(* This variant type has been already copied *)
|
|
ty.desc <- Tsubst ty2; (* avoid Tlink in the new type *)
|
|
Tlink ty2
|
|
| _ ->
|
|
(* If the row variable is not generic, we must keep it *)
|
|
let keep = more.level <> generic_level in
|
|
let more' =
|
|
match more.desc with
|
|
Tsubst ty -> ty
|
|
| Tconstr _ ->
|
|
if keep then save_desc more more.desc;
|
|
copy more
|
|
| Tvar | Tunivar ->
|
|
save_desc more more.desc;
|
|
if keep then more else newty more.desc
|
|
| _ -> assert false
|
|
in
|
|
(* Register new type first for recursion *)
|
|
more.desc <- Tsubst(newgenty(Ttuple[more';t]));
|
|
(* Return a new copy *)
|
|
Tvariant (copy_row copy true row keep more')
|
|
end
|
|
| Tfield (p, k, ty1, ty2) ->
|
|
begin match field_kind_repr k with
|
|
Fabsent -> Tlink (copy ty2)
|
|
| Fpresent -> copy_type_desc copy desc
|
|
| Fvar r ->
|
|
dup_kind r;
|
|
copy_type_desc copy desc
|
|
end
|
|
| _ -> copy_type_desc copy desc
|
|
end;
|
|
t
|
|
|
|
(**** Variants of instantiations ****)
|
|
|
|
let instance sch =
|
|
let ty = copy sch in
|
|
cleanup_types ();
|
|
ty
|
|
|
|
let instance_list schl =
|
|
let tyl = List.map copy schl in
|
|
cleanup_types ();
|
|
tyl
|
|
|
|
let instance_constructor cstr =
|
|
let ty_res = copy cstr.cstr_res in
|
|
let ty_args = List.map copy cstr.cstr_args in
|
|
cleanup_types ();
|
|
(ty_args, ty_res)
|
|
|
|
let instance_parameterized_type sch_args sch =
|
|
let ty_args = List.map copy sch_args in
|
|
let ty = copy sch in
|
|
cleanup_types ();
|
|
(ty_args, ty)
|
|
|
|
let instance_parameterized_type_2 sch_args sch_lst sch =
|
|
let ty_args = List.map copy sch_args in
|
|
let ty_lst = List.map copy sch_lst in
|
|
let ty = copy sch in
|
|
cleanup_types ();
|
|
(ty_args, ty_lst, ty)
|
|
|
|
let instance_class params cty =
|
|
let rec copy_class_type =
|
|
function
|
|
Tcty_constr (path, tyl, cty) ->
|
|
Tcty_constr (path, List.map copy tyl, copy_class_type cty)
|
|
| Tcty_signature sign ->
|
|
Tcty_signature
|
|
{cty_self = copy sign.cty_self;
|
|
cty_vars =
|
|
Vars.map (function (m, v, ty) -> (m, v, copy ty)) sign.cty_vars;
|
|
cty_concr = sign.cty_concr;
|
|
cty_inher =
|
|
List.map (fun (p,tl) -> (p, List.map copy tl)) sign.cty_inher}
|
|
| Tcty_fun (l, ty, cty) ->
|
|
Tcty_fun (l, copy ty, copy_class_type cty)
|
|
in
|
|
let params' = List.map copy params in
|
|
let cty' = copy_class_type cty in
|
|
cleanup_types ();
|
|
(params', cty')
|
|
|
|
(**** Instanciation for types with free universal variables ****)
|
|
|
|
module TypeHash = Hashtbl.Make(TypeOps)
|
|
module TypeSet = Set.Make(TypeOps)
|
|
|
|
type inv_type_expr =
|
|
{ inv_type : type_expr;
|
|
mutable inv_parents : inv_type_expr list }
|
|
|
|
let rec inv_type hash pty ty =
|
|
let ty = repr ty in
|
|
try
|
|
let inv = TypeHash.find hash ty in
|
|
inv.inv_parents <- pty @ inv.inv_parents
|
|
with Not_found ->
|
|
let inv = { inv_type = ty; inv_parents = pty } in
|
|
TypeHash.add hash ty inv;
|
|
iter_type_expr (inv_type hash [inv]) ty
|
|
|
|
let compute_univars ty =
|
|
let inverted = TypeHash.create 17 in
|
|
inv_type inverted [] ty;
|
|
let node_univars = TypeHash.create 17 in
|
|
let rec add_univar univ inv =
|
|
match inv.inv_type.desc with
|
|
Tpoly (ty, tl) when List.memq univ (List.map repr tl) -> ()
|
|
| _ ->
|
|
try
|
|
let univs = TypeHash.find node_univars inv.inv_type in
|
|
if not (TypeSet.mem univ !univs) then begin
|
|
univs := TypeSet.add univ !univs;
|
|
List.iter (add_univar univ) inv.inv_parents
|
|
end
|
|
with Not_found ->
|
|
TypeHash.add node_univars inv.inv_type (ref(TypeSet.singleton univ));
|
|
List.iter (add_univar univ) inv.inv_parents
|
|
in
|
|
TypeHash.iter (fun ty inv -> if ty.desc = Tunivar then add_univar ty inv)
|
|
inverted;
|
|
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 *)
|
|
|
|
(* Copy without sharing until there are no free univars left *)
|
|
(* all free univars must be included in [visited] *)
|
|
let rec copy_sep fixed 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 = if ty.desc = Tunivar then [] else 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 _ | Tpackage _ ->
|
|
(ty,(t,bound)) :: visited
|
|
| _ -> visited in
|
|
let copy_rec = copy_sep fixed free bound visited in
|
|
t.desc <-
|
|
begin match ty.desc with
|
|
| Tvariant row0 ->
|
|
let row = row_repr row0 in
|
|
let more = repr row.row_more in
|
|
(* We shall really check the level on the row variable *)
|
|
let keep = more.desc = Tvar && more.level <> generic_level in
|
|
let more' = copy_rec more in
|
|
let fixed' = fixed && (repr more').desc = Tvar in
|
|
let row = copy_row copy_rec fixed' row keep more' in
|
|
Tvariant row
|
|
| Tpoly (t1, tl) ->
|
|
let tl = List.map repr tl in
|
|
let tl' = List.map (fun t -> 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 fixed free bound visited t1, tl')
|
|
| _ -> copy_type_desc copy_rec ty.desc
|
|
end;
|
|
t
|
|
end
|
|
|
|
let instance_poly fixed univars sch =
|
|
let vars = List.map (fun _ -> newvar ()) univars in
|
|
let pairs = List.map2 (fun u v -> repr u, (v, [])) univars vars in
|
|
delayed_copy := [];
|
|
let ty = copy_sep fixed (compute_univars sch) [] pairs sch in
|
|
List.iter Lazy.force !delayed_copy;
|
|
delayed_copy := [];
|
|
cleanup_types ();
|
|
vars, ty
|
|
|
|
let instance_label fixed lbl =
|
|
let ty_res = copy lbl.lbl_res in
|
|
let vars, ty_arg =
|
|
match repr lbl.lbl_arg with
|
|
{desc = Tpoly (ty, tl)} ->
|
|
instance_poly fixed tl ty
|
|
| ty ->
|
|
[], copy lbl.lbl_arg
|
|
in
|
|
cleanup_types ();
|
|
(vars, ty_arg, ty_res)
|
|
|
|
(**** Instantiation with parameter substitution ****)
|
|
|
|
let unify' = (* Forward declaration *)
|
|
ref (fun env ty1 ty2 -> raise (Unify []))
|
|
|
|
let rec subst env level priv abbrev ty params args body =
|
|
if List.length params <> List.length args then raise (Unify []);
|
|
let old_level = !current_level in
|
|
current_level := level;
|
|
try
|
|
let body0 = newvar () in (* Stub *)
|
|
begin match ty with
|
|
None -> ()
|
|
| Some ({desc = Tconstr (path, tl, _)} as ty) ->
|
|
let abbrev = proper_abbrevs path tl abbrev in
|
|
memorize_abbrev abbrev priv path ty body0
|
|
| _ ->
|
|
assert false
|
|
end;
|
|
abbreviations := abbrev;
|
|
let (params', body') = instance_parameterized_type params body in
|
|
abbreviations := ref Mnil;
|
|
!unify' env body0 body';
|
|
List.iter2 (!unify' env) params' args;
|
|
current_level := old_level;
|
|
body'
|
|
with Unify _ as exn ->
|
|
current_level := old_level;
|
|
raise exn
|
|
|
|
(*
|
|
Only the shape of the type matters, not whether is is generic or
|
|
not. [generic_level] might be somewhat slower, but it ensures
|
|
invariants on types are enforced (decreasing levels.), and we don't
|
|
care about efficiency here.
|
|
*)
|
|
let apply env params body args =
|
|
try
|
|
subst env generic_level Public (ref Mnil) None params args body
|
|
with
|
|
Unify _ -> raise Cannot_apply
|
|
|
|
|
|
(****************************)
|
|
(* Abbreviation expansion *)
|
|
(****************************)
|
|
|
|
(*
|
|
If the environnement has changed, memorized expansions might not
|
|
be correct anymore, and so we flush the cache. This is safe but
|
|
quite pessimistic: it would be enough to flush the cache when a
|
|
type or module definition is overridden in the environnement.
|
|
*)
|
|
let previous_env = ref Env.empty
|
|
let string_of_kind = function Public -> "public" | Private -> "private"
|
|
let check_abbrev_env env =
|
|
if env != !previous_env then begin
|
|
(* prerr_endline "cleanup expansion cache"; *)
|
|
cleanup_abbrev ();
|
|
previous_env := env
|
|
end
|
|
|
|
(* Expand an abbreviation. The expansion is memorized. *)
|
|
(*
|
|
Assume the level is greater than the path binding time of the
|
|
expanded abbreviation.
|
|
*)
|
|
(*
|
|
An abbreviation expansion will fail in either of these cases:
|
|
1. The type constructor does not correspond to a manifest type.
|
|
2. The type constructor is defined in an external file, and this
|
|
file is not in the path (missing -I options).
|
|
3. The type constructor is not in the "local" environment. This can
|
|
happens when a non-generic type variable has been instantiated
|
|
afterwards to the not yet defined type constructor. (Actually,
|
|
this cannot happen at the moment due to the strong constraints
|
|
between type levels and constructor binding time.)
|
|
4. The expansion requires the expansion of another abbreviation,
|
|
and this other expansion fails.
|
|
*)
|
|
let expand_abbrev_gen kind find_type_expansion env ty =
|
|
check_abbrev_env env;
|
|
match ty with
|
|
{desc = Tconstr (path, args, abbrev); level = level} ->
|
|
let lookup_abbrev = proper_abbrevs path args abbrev in
|
|
begin match find_expans kind path !lookup_abbrev with
|
|
Some ty ->
|
|
(* prerr_endline
|
|
("found a "^string_of_kind kind^" expansion for "^Path.name path);*)
|
|
if level <> generic_level then
|
|
begin try
|
|
update_level env level ty
|
|
with Unify _ ->
|
|
(* XXX This should not happen.
|
|
However, levels are not correctly restored after a
|
|
typing error *)
|
|
()
|
|
end;
|
|
ty
|
|
| None ->
|
|
let (params, body) =
|
|
try find_type_expansion path env with Not_found ->
|
|
raise Cannot_expand
|
|
in
|
|
(* prerr_endline
|
|
("add a "^string_of_kind kind^" expansion for "^Path.name path);*)
|
|
let ty' = subst env level kind abbrev (Some ty) params args body in
|
|
(* Hack to name the variant type *)
|
|
begin match repr ty' with
|
|
{desc=Tvariant row} as ty when static_row row ->
|
|
ty.desc <- Tvariant { row with row_name = Some (path, args) }
|
|
| _ -> ()
|
|
end;
|
|
ty'
|
|
end
|
|
| _ ->
|
|
assert false
|
|
|
|
let expand_abbrev = expand_abbrev_gen Public Env.find_type_expansion
|
|
|
|
let safe_abbrev env ty =
|
|
let snap = Btype.snapshot () in
|
|
try ignore (expand_abbrev env ty); true
|
|
with Cannot_expand | Unify _ ->
|
|
Btype.backtrack snap;
|
|
false
|
|
|
|
let try_expand_once env ty =
|
|
let ty = repr ty in
|
|
match ty.desc with
|
|
Tconstr _ -> repr (expand_abbrev env ty)
|
|
| _ -> raise Cannot_expand
|
|
|
|
let _ = forward_try_expand_once := try_expand_once
|
|
|
|
(* Fully expand the head of a type.
|
|
Raise Cannot_expand if the type cannot be expanded.
|
|
May raise Unify, if a recursion was hidden in the type. *)
|
|
let rec try_expand_head env ty =
|
|
let ty' = try_expand_once env ty in
|
|
begin try
|
|
try_expand_head env ty'
|
|
with Cannot_expand ->
|
|
ty'
|
|
end
|
|
|
|
(* Expand once the head of a type *)
|
|
let expand_head_once env ty =
|
|
try expand_abbrev env (repr ty) with Cannot_expand -> assert false
|
|
|
|
(* Fully expand the head of a type. *)
|
|
let expand_head_unif env ty =
|
|
try try_expand_head env ty with Cannot_expand -> repr ty
|
|
|
|
let expand_head env ty =
|
|
let snap = Btype.snapshot () in
|
|
try try_expand_head env ty
|
|
with Cannot_expand | Unify _ -> (* expand_head shall never fail *)
|
|
Btype.backtrack snap;
|
|
repr ty
|
|
|
|
(* Implementing function [expand_head_opt], the compiler's own version of
|
|
[expand_head] used for type-based optimisations.
|
|
[expand_head_opt] uses [Env.find_type_expansion_opt] to access the
|
|
manifest type information of private abstract data types which is
|
|
normally hidden to the type-checker out of the implementation module of
|
|
the private abbreviation. *)
|
|
|
|
let expand_abbrev_opt = expand_abbrev_gen Private Env.find_type_expansion_opt
|
|
|
|
let try_expand_once_opt env ty =
|
|
let ty = repr ty in
|
|
match ty.desc with
|
|
Tconstr _ -> repr (expand_abbrev_opt env ty)
|
|
| _ -> raise Cannot_expand
|
|
|
|
let rec try_expand_head_opt env ty =
|
|
let ty' = try_expand_once_opt env ty in
|
|
begin try
|
|
try_expand_head_opt env ty'
|
|
with Cannot_expand ->
|
|
ty'
|
|
end
|
|
|
|
let expand_head_opt env ty =
|
|
let snap = Btype.snapshot () in
|
|
try try_expand_head_opt env ty
|
|
with Cannot_expand | Unify _ -> (* expand_head shall never fail *)
|
|
Btype.backtrack snap;
|
|
repr ty
|
|
|
|
(* Make sure that the type parameters of the type constructor [ty]
|
|
respect the type constraints *)
|
|
let enforce_constraints env ty =
|
|
match ty with
|
|
{desc = Tconstr (path, args, abbrev); level = level} ->
|
|
let decl = Env.find_type path env in
|
|
ignore
|
|
(subst env level Public (ref Mnil) None decl.type_params args
|
|
(newvar2 level))
|
|
| _ ->
|
|
assert false
|
|
|
|
(* Recursively expand the head of a type.
|
|
Also expand #-types. *)
|
|
let rec full_expand env ty =
|
|
let ty = repr (expand_head env ty) in
|
|
match ty.desc with
|
|
Tobject (fi, {contents = Some (_, v::_)}) when (repr v).desc = Tvar ->
|
|
newty2 ty.level (Tobject (fi, ref None))
|
|
| _ ->
|
|
ty
|
|
|
|
(*
|
|
Check whether the abbreviation expands to a well-defined type.
|
|
During the typing of a class, abbreviations for correspondings
|
|
types expand to non-generic types.
|
|
*)
|
|
let generic_abbrev env path =
|
|
try
|
|
let (_, body) = Env.find_type_expansion path env in
|
|
(repr body).level = generic_level
|
|
with
|
|
Not_found ->
|
|
false
|
|
|
|
|
|
(*****************)
|
|
(* Occur check *)
|
|
(*****************)
|
|
|
|
|
|
exception Occur
|
|
|
|
(* The marks are already used by [expand_abbrev]... *)
|
|
let visited = ref []
|
|
|
|
let rec non_recursive_abbrev env ty0 ty =
|
|
let ty = repr ty in
|
|
if ty == repr ty0 then raise Recursive_abbrev;
|
|
if not (List.memq ty !visited) then begin
|
|
visited := ty :: !visited;
|
|
match ty.desc with
|
|
Tconstr(p, args, abbrev) ->
|
|
begin try
|
|
non_recursive_abbrev env ty0 (try_expand_once_opt env ty)
|
|
with Cannot_expand ->
|
|
if !Clflags.recursive_types then () else
|
|
iter_type_expr (non_recursive_abbrev env ty0) ty
|
|
end
|
|
| Tobject _ | Tvariant _ ->
|
|
()
|
|
| _ ->
|
|
if !Clflags.recursive_types then () else
|
|
iter_type_expr (non_recursive_abbrev env ty0) ty
|
|
end
|
|
|
|
let correct_abbrev env path params ty =
|
|
check_abbrev_env env;
|
|
let ty0 = newgenvar () in
|
|
visited := [];
|
|
let abbrev = Mcons (Public, path, ty0, ty0, Mnil) in
|
|
simple_abbrevs := abbrev;
|
|
try
|
|
non_recursive_abbrev env ty0
|
|
(subst env generic_level Public (ref abbrev) None [] [] ty);
|
|
simple_abbrevs := Mnil;
|
|
visited := []
|
|
with exn ->
|
|
simple_abbrevs := Mnil;
|
|
visited := [];
|
|
raise exn
|
|
|
|
let rec occur_rec env visited ty0 ty =
|
|
if ty == ty0 then raise Occur;
|
|
match ty.desc with
|
|
Tconstr(p, tl, abbrev) ->
|
|
begin try
|
|
if List.memq ty visited || !Clflags.recursive_types then raise Occur;
|
|
iter_type_expr (occur_rec env (ty::visited) ty0) ty
|
|
with Occur -> try
|
|
let ty' = try_expand_head env ty in
|
|
(* Maybe we could simply make a recursive call here,
|
|
but it seems it could make the occur check loop
|
|
(see change in rev. 1.58) *)
|
|
if ty' == ty0 || List.memq ty' visited then raise Occur;
|
|
match ty'.desc with
|
|
Tobject _ | Tvariant _ -> ()
|
|
| _ ->
|
|
if not !Clflags.recursive_types then
|
|
iter_type_expr (occur_rec env (ty'::visited) ty0) ty'
|
|
with Cannot_expand ->
|
|
if not !Clflags.recursive_types then raise Occur
|
|
end
|
|
| Tobject _ | Tvariant _ ->
|
|
()
|
|
| _ ->
|
|
if not !Clflags.recursive_types then
|
|
iter_type_expr (occur_rec env visited ty0) ty
|
|
|
|
let type_changed = ref false (* trace possible changes to the studied type *)
|
|
|
|
let merge r b = if b then r := true
|
|
|
|
let occur env ty0 ty =
|
|
let old = !type_changed in
|
|
try
|
|
while type_changed := false; occur_rec env [] ty0 ty; !type_changed
|
|
do () (* prerr_endline "changed" *) done;
|
|
merge type_changed old
|
|
with exn ->
|
|
merge type_changed old;
|
|
raise (match exn with Occur -> Unify [] | _ -> exn)
|
|
|
|
|
|
(*****************************)
|
|
(* Polymorphic Unification *)
|
|
(*****************************)
|
|
|
|
(* Since we cannot duplicate universal variables, unification must
|
|
be done at meta-level, using bindings in univar_pairs *)
|
|
let rec unify_univar t1 t2 = function
|
|
(cl1, cl2) :: rem ->
|
|
let find_univ t cl =
|
|
try
|
|
let (_, r) = List.find (fun (t',_) -> t == repr t') cl in
|
|
Some r
|
|
with Not_found -> None
|
|
in
|
|
begin match find_univ t1 cl1, find_univ t2 cl2 with
|
|
Some {contents=Some t'2}, Some _ when t2 == repr t'2 ->
|
|
()
|
|
| Some({contents=None} as r1), Some({contents=None} as r2) ->
|
|
set_univar r1 t2; set_univar r2 t1
|
|
| None, None ->
|
|
unify_univar t1 t2 rem
|
|
| _ ->
|
|
raise (Unify [])
|
|
end
|
|
| [] -> raise (Unify [])
|
|
|
|
module TypeMap = Map.Make (TypeOps)
|
|
|
|
(* Test the occurence of free univars in a type *)
|
|
(* that's way too expansive. Must do some kind of cacheing *)
|
|
let occur_univar env ty =
|
|
let visited = ref TypeMap.empty in
|
|
let rec occur_rec bound ty =
|
|
let ty = repr ty in
|
|
if ty.level >= lowest_level &&
|
|
if TypeSet.is_empty bound then
|
|
(ty.level <- pivot_level - ty.level; true)
|
|
else try
|
|
let bound' = TypeMap.find ty !visited in
|
|
if TypeSet.exists (fun x -> not (TypeSet.mem x bound)) bound' then
|
|
(visited := TypeMap.add ty (TypeSet.inter bound bound') !visited;
|
|
true)
|
|
else false
|
|
with Not_found ->
|
|
visited := TypeMap.add ty bound !visited;
|
|
true
|
|
then
|
|
match ty.desc with
|
|
Tunivar ->
|
|
if not (TypeSet.mem ty bound) then raise (Unify [ty, newgenvar()])
|
|
| Tpoly (ty, tyl) ->
|
|
let bound = List.fold_right TypeSet.add (List.map repr tyl) bound in
|
|
occur_rec bound ty
|
|
| Tconstr (_, [], _) -> ()
|
|
| Tconstr (p, tl, _) ->
|
|
begin try
|
|
let td = Env.find_type p env in
|
|
List.iter2
|
|
(fun t (pos,neg,_) -> if pos || neg then occur_rec bound t)
|
|
tl td.type_variance
|
|
with Not_found ->
|
|
List.iter (occur_rec bound) tl
|
|
end
|
|
| _ -> iter_type_expr (occur_rec bound) ty
|
|
in
|
|
try
|
|
occur_rec TypeSet.empty ty; unmark_type ty
|
|
with exn ->
|
|
unmark_type ty; raise exn
|
|
|
|
(* Grouping univars by families according to their binders *)
|
|
let add_univars =
|
|
List.fold_left (fun s (t,_) -> TypeSet.add (repr t) s)
|
|
|
|
let get_univar_family univar_pairs univars =
|
|
if univars = [] then TypeSet.empty else
|
|
let rec insert s = function
|
|
cl1, (_::_ as cl2) ->
|
|
if List.exists (fun (t1,_) -> TypeSet.mem (repr t1) s) cl1 then
|
|
add_univars s cl2
|
|
else s
|
|
| _ -> s
|
|
in
|
|
let s = List.fold_right TypeSet.add univars TypeSet.empty in
|
|
List.fold_left insert s univar_pairs
|
|
|
|
(* Whether a family of univars escapes from a type *)
|
|
let univars_escape env univar_pairs vl ty =
|
|
let family = get_univar_family univar_pairs vl in
|
|
let visited = ref TypeSet.empty in
|
|
let rec occur t =
|
|
let t = repr t in
|
|
if TypeSet.mem t !visited then () else begin
|
|
visited := TypeSet.add t !visited;
|
|
match t.desc with
|
|
Tpoly (t, tl) ->
|
|
if List.exists (fun t -> TypeSet.mem (repr t) family) tl then ()
|
|
else occur t
|
|
| Tunivar ->
|
|
if TypeSet.mem t family then raise Occur
|
|
| Tconstr (_, [], _) -> ()
|
|
| Tconstr (p, tl, _) ->
|
|
begin try
|
|
let td = Env.find_type p env in
|
|
List.iter2 (fun t (pos,neg,_) -> if pos || neg then occur t)
|
|
tl td.type_variance
|
|
with Not_found ->
|
|
List.iter occur tl
|
|
end
|
|
| _ ->
|
|
iter_type_expr occur t
|
|
end
|
|
in
|
|
try occur ty; false with Occur -> true
|
|
|
|
(* Wrapper checking that no variable escapes and updating univar_pairs *)
|
|
let enter_poly env univar_pairs t1 tl1 t2 tl2 f =
|
|
let old_univars = !univar_pairs in
|
|
let known_univars =
|
|
List.fold_left (fun s (cl,_) -> add_univars s cl)
|
|
TypeSet.empty old_univars
|
|
in
|
|
let tl1 = List.map repr tl1 and tl2 = List.map repr tl2 in
|
|
if List.exists (fun t -> TypeSet.mem t known_univars) tl1 &&
|
|
univars_escape env old_univars tl1 (newty(Tpoly(t2,tl2)))
|
|
|| List.exists (fun t -> TypeSet.mem t known_univars) tl2 &&
|
|
univars_escape env old_univars tl2 (newty(Tpoly(t1,tl1)))
|
|
then raise (Unify []);
|
|
let cl1 = List.map (fun t -> t, ref None) tl1
|
|
and cl2 = List.map (fun t -> t, ref None) tl2 in
|
|
univar_pairs := (cl1,cl2) :: (cl2,cl1) :: old_univars;
|
|
try let res = f t1 t2 in univar_pairs := old_univars; res
|
|
with exn -> univar_pairs := old_univars; raise exn
|
|
|
|
let univar_pairs = ref []
|
|
|
|
|
|
(*****************)
|
|
(* Unification *)
|
|
(*****************)
|
|
|
|
|
|
|
|
let rec has_cached_expansion p abbrev =
|
|
match abbrev with
|
|
Mnil -> false
|
|
| Mcons(_, p', _, _, rem) -> Path.same p p' || has_cached_expansion p rem
|
|
| Mlink rem -> has_cached_expansion p !rem
|
|
|
|
(**** Transform error trace ****)
|
|
(* +++ Move it to some other place ? *)
|
|
|
|
let expand_trace env trace =
|
|
List.fold_right
|
|
(fun (t1, t2) rem ->
|
|
(repr t1, full_expand env t1)::(repr t2, full_expand env t2)::rem)
|
|
trace []
|
|
|
|
(* build a dummy variant type *)
|
|
let mkvariant fields closed =
|
|
newgenty
|
|
(Tvariant
|
|
{row_fields = fields; row_closed = closed; row_more = newvar();
|
|
row_bound = (); row_fixed = false; row_name = None })
|
|
|
|
(* force unification in Reither when one side has as non-conjunctive type *)
|
|
let rigid_variants = ref false
|
|
|
|
(**** Unification ****)
|
|
|
|
(* Return whether [t0] occurs in [ty]. Objects are also traversed. *)
|
|
let deep_occur t0 ty =
|
|
let rec occur_rec ty =
|
|
let ty = repr ty in
|
|
if ty.level >= lowest_level then begin
|
|
if ty == t0 then raise Occur;
|
|
ty.level <- pivot_level - ty.level;
|
|
iter_type_expr occur_rec ty
|
|
end
|
|
in
|
|
try
|
|
occur_rec ty; unmark_type ty; false
|
|
with Occur ->
|
|
unmark_type ty; true
|
|
|
|
(*
|
|
1. When unifying two non-abbreviated types, one type is made a link
|
|
to the other. When unifying an abbreviated type with a
|
|
non-abbreviated type, the non-abbreviated type is made a link to
|
|
the other one. When unifying to abbreviated types, these two
|
|
types are kept distincts, but they are made to (temporally)
|
|
expand to the same type.
|
|
2. Abbreviations with at least one parameter are systematically
|
|
expanded. The overhead does not seem to high, and that way
|
|
abbreviations where some parameters does not appear in the
|
|
expansion, such as ['a t = int], are correctly handled. In
|
|
particular, for this example, unifying ['a t] with ['b t] keeps
|
|
['a] and ['b] distincts. (Is it really important ?)
|
|
3. Unifying an abbreviation ['a t = 'a] with ['a] should not yield
|
|
['a t as 'a]. Indeed, the type variable would otherwise be lost.
|
|
This problem occurs for abbreviations expanding to a type
|
|
variable, but also to many other constrained abbreviations (for
|
|
instance, [(< x : 'a > -> unit) t = <x : 'a>]). The solution is
|
|
that, if an abbreviation is unified with some subpart of its
|
|
parameters, then the parameter actually does not get
|
|
abbreviated. It would be possible to check whether some
|
|
information is indeed lost, but it probably does not worth it.
|
|
*)
|
|
let rec unify env t1 t2 =
|
|
(* First step: special cases (optimizations) *)
|
|
if t1 == t2 then () else
|
|
let t1 = repr t1 in
|
|
let t2 = repr t2 in
|
|
if t1 == t2 then () else
|
|
|
|
try
|
|
type_changed := true;
|
|
match (t1.desc, t2.desc) with
|
|
(Tvar, Tconstr _) when deep_occur t1 t2 ->
|
|
unify2 env t1 t2
|
|
| (Tconstr _, Tvar) when deep_occur t2 t1 ->
|
|
unify2 env t1 t2
|
|
| (Tvar, _) ->
|
|
occur env t1 t2; occur_univar env t2;
|
|
update_level env t1.level t2;
|
|
link_type t1 t2
|
|
| (_, Tvar) ->
|
|
occur env t2 t1; occur_univar env t1;
|
|
update_level env t2.level t1;
|
|
link_type t2 t1
|
|
| (Tunivar, Tunivar) ->
|
|
unify_univar t1 t2 !univar_pairs;
|
|
update_level env t1.level t2;
|
|
link_type t1 t2
|
|
| (Tconstr (p1, [], a1), Tconstr (p2, [], a2))
|
|
when Path.same p1 p2
|
|
(* This optimization assumes that t1 does not expand to t2
|
|
(and conversely), so we fall back to the general case
|
|
when any of the types has a cached expansion. *)
|
|
&& not (has_cached_expansion p1 !a1
|
|
|| has_cached_expansion p2 !a2) ->
|
|
update_level env t1.level t2;
|
|
link_type t1 t2
|
|
| _ ->
|
|
unify2 env t1 t2
|
|
with Unify trace ->
|
|
raise (Unify ((t1, t2)::trace))
|
|
|
|
and unify2 env t1 t2 =
|
|
(* Second step: expansion of abbreviations *)
|
|
let rec expand_both t1'' t2'' =
|
|
let t1' = expand_head_unif env t1 in
|
|
let t2' = expand_head_unif env t2 in
|
|
(* Expansion may have changed the representative of the types... *)
|
|
if t1' == t1'' && t2' == t2'' then (t1',t2') else
|
|
expand_both t1' t2'
|
|
in
|
|
let t1', t2' = expand_both t1 t2 in
|
|
if t1' == t2' then () else
|
|
|
|
let t1 = repr t1 and t2 = repr t2 in
|
|
if (t1 == t1') || (t2 != t2') then
|
|
unify3 env t1 t1' t2 t2'
|
|
else
|
|
try unify3 env t2 t2' t1 t1' with Unify trace ->
|
|
raise (Unify (List.map (fun (x, y) -> (y, x)) trace))
|
|
|
|
and unify3 env t1 t1' t2 t2' =
|
|
(* Third step: truly unification *)
|
|
(* Assumes either [t1 == t1'] or [t2 != t2'] *)
|
|
let d1 = t1'.desc and d2 = t2'.desc in
|
|
|
|
let create_recursion = (t2 != t2') && (deep_occur t1' t2) in
|
|
occur env t1' t2;
|
|
update_level env t1'.level t2;
|
|
link_type t1' t2;
|
|
|
|
try
|
|
begin match (d1, d2) with
|
|
(Tvar, _) ->
|
|
occur_univar env t2
|
|
| (_, Tvar) ->
|
|
let td1 = newgenty d1 in
|
|
occur env t2' td1;
|
|
occur_univar env td1;
|
|
if t1 == t1' then begin
|
|
(* The variable must be instantiated... *)
|
|
let ty = newty2 t1'.level d1 in
|
|
update_level env t2'.level ty;
|
|
link_type t2' ty
|
|
end else begin
|
|
log_type t1';
|
|
t1'.desc <- d1;
|
|
update_level env t2'.level t1;
|
|
link_type t2' t1
|
|
end
|
|
| (Tarrow (l1, t1, u1, c1), Tarrow (l2, t2, u2, c2)) when l1 = l2
|
|
|| !Clflags.classic && not (is_optional l1 || is_optional l2) ->
|
|
unify env t1 t2; unify env u1 u2;
|
|
begin match commu_repr c1, commu_repr c2 with
|
|
Clink r, c2 -> set_commu r c2
|
|
| c1, Clink r -> set_commu r c1
|
|
| _ -> ()
|
|
end
|
|
| (Ttuple tl1, Ttuple tl2) ->
|
|
unify_list env tl1 tl2
|
|
| (Tconstr (p1, tl1, _), Tconstr (p2, tl2, _)) when Path.same p1 p2 ->
|
|
unify_list env tl1 tl2
|
|
| (Tobject (fi1, nm1), Tobject (fi2, _)) ->
|
|
unify_fields env fi1 fi2;
|
|
(* Type [t2'] may have been instantiated by [unify_fields] *)
|
|
(* XXX One should do some kind of unification... *)
|
|
begin match (repr t2').desc with
|
|
Tobject (_, {contents = Some (_, va::_)})
|
|
when let va = repr va in List.mem va.desc [Tvar; Tunivar; Tnil] ->
|
|
()
|
|
| Tobject (_, nm2) ->
|
|
set_name nm2 !nm1
|
|
| _ ->
|
|
()
|
|
end
|
|
| (Tvariant row1, Tvariant row2) ->
|
|
unify_row env row1 row2
|
|
| (Tfield _, Tfield _) -> (* Actually unused *)
|
|
unify_fields env t1' t2'
|
|
| (Tfield(f,kind,_,rem), Tnil) | (Tnil, Tfield(f,kind,_,rem)) ->
|
|
begin match field_kind_repr kind with
|
|
Fvar r when f <> dummy_method -> set_kind r Fabsent
|
|
| _ -> raise (Unify [])
|
|
end
|
|
| (Tnil, Tnil) ->
|
|
()
|
|
| (Tpoly (t1, []), Tpoly (t2, [])) ->
|
|
unify env t1 t2
|
|
| (Tpoly (t1, tl1), Tpoly (t2, tl2)) ->
|
|
enter_poly env univar_pairs t1 tl1 t2 tl2 (unify env)
|
|
| (Tpackage (p1, n1, tl1), Tpackage (p2, n2, tl2)) when Path.same p1 p2 && n1 = n2 ->
|
|
unify_list env tl1 tl2
|
|
| (_, _) ->
|
|
raise (Unify [])
|
|
end;
|
|
|
|
(* XXX Commentaires + changer "create_recursion" *)
|
|
if create_recursion then begin
|
|
match t2.desc with
|
|
Tconstr (p, tl, abbrev) ->
|
|
forget_abbrev abbrev p;
|
|
let t2'' = expand_head_unif env t2 in
|
|
if not (closed_parameterized_type tl t2'') then
|
|
link_type (repr t2) (repr t2')
|
|
| _ ->
|
|
() (* t2 has already been expanded by update_level *)
|
|
end
|
|
|
|
(*
|
|
(*
|
|
Can only be done afterwards, once the row variable has
|
|
(possibly) been instantiated.
|
|
*)
|
|
if t1 != t1' (* && t2 != t2' *) then begin
|
|
match (t1.desc, t2.desc) with
|
|
(Tconstr (p, ty::_, _), _)
|
|
when ((repr ty).desc <> Tvar)
|
|
&& weak_abbrev p
|
|
&& not (deep_occur t1 t2) ->
|
|
update_level env t1.level t2;
|
|
link_type t1 t2
|
|
| (_, Tconstr (p, ty::_, _))
|
|
when ((repr ty).desc <> Tvar)
|
|
&& weak_abbrev p
|
|
&& not (deep_occur t2 t1) ->
|
|
update_level env t2.level t1;
|
|
link_type t2 t1;
|
|
link_type t1' t2'
|
|
| _ ->
|
|
()
|
|
end
|
|
*)
|
|
with Unify trace ->
|
|
t1'.desc <- d1;
|
|
raise (Unify trace)
|
|
|
|
and unify_list env tl1 tl2 =
|
|
if List.length tl1 <> List.length tl2 then
|
|
raise (Unify []);
|
|
List.iter2 (unify env) tl1 tl2
|
|
|
|
and unify_fields env ty1 ty2 = (* Optimization *)
|
|
let (fields1, rest1) = flatten_fields ty1
|
|
and (fields2, rest2) = flatten_fields ty2 in
|
|
let (pairs, miss1, miss2) = associate_fields fields1 fields2 in
|
|
let l1 = (repr ty1).level and l2 = (repr ty2).level in
|
|
let va =
|
|
if miss1 = [] then rest2
|
|
else if miss2 = [] then rest1
|
|
else newty2 (min l1 l2) Tvar
|
|
in
|
|
let d1 = rest1.desc and d2 = rest2.desc in
|
|
try
|
|
unify env (build_fields l1 miss1 va) rest2;
|
|
unify env rest1 (build_fields l2 miss2 va);
|
|
List.iter
|
|
(fun (n, k1, t1, k2, t2) ->
|
|
unify_kind k1 k2;
|
|
try unify env t1 t2 with Unify trace ->
|
|
raise (Unify ((newty (Tfield(n, k1, t1, va)),
|
|
newty (Tfield(n, k2, t2, va)))::trace)))
|
|
pairs
|
|
with exn ->
|
|
log_type rest1; rest1.desc <- d1;
|
|
log_type rest2; rest2.desc <- d2;
|
|
raise exn
|
|
|
|
and unify_kind k1 k2 =
|
|
let k1 = field_kind_repr k1 in
|
|
let k2 = field_kind_repr k2 in
|
|
if k1 == k2 then () else
|
|
match k1, k2 with
|
|
(Fvar r, (Fvar _ | Fpresent)) -> set_kind r k2
|
|
| (Fpresent, Fvar r) -> set_kind r k1
|
|
| (Fpresent, Fpresent) -> ()
|
|
| _ -> assert false
|
|
|
|
and unify_pairs env tpl =
|
|
List.iter (fun (t1, t2) -> unify env t1 t2) tpl
|
|
|
|
and unify_row env row1 row2 =
|
|
let row1 = row_repr row1 and row2 = row_repr row2 in
|
|
let rm1 = row_more row1 and rm2 = row_more row2 in
|
|
if rm1 == rm2 then () else
|
|
let r1, r2, pairs = merge_row_fields row1.row_fields row2.row_fields in
|
|
if r1 <> [] && r2 <> [] then begin
|
|
let ht = Hashtbl.create (List.length r1) in
|
|
List.iter (fun (l,_) -> Hashtbl.add ht (hash_variant l) l) r1;
|
|
List.iter
|
|
(fun (l,_) ->
|
|
try raise (Tags(l, Hashtbl.find ht (hash_variant l)))
|
|
with Not_found -> ())
|
|
r2
|
|
end;
|
|
let more =
|
|
if row1.row_fixed then rm1 else
|
|
if row2.row_fixed then rm2 else
|
|
newgenvar ()
|
|
in update_level env (min rm1.level rm2.level) more;
|
|
let fixed = row1.row_fixed || row2.row_fixed
|
|
and closed = row1.row_closed || row2.row_closed in
|
|
let keep switch =
|
|
List.for_all
|
|
(fun (_,f1,f2) ->
|
|
let f1, f2 = switch f1 f2 in
|
|
row_field_repr f1 = Rabsent || row_field_repr f2 <> Rabsent)
|
|
pairs
|
|
in
|
|
let empty fields =
|
|
List.for_all (fun (_,f) -> row_field_repr f = Rabsent) fields in
|
|
(* Check whether we are going to build an empty type *)
|
|
if closed && (empty r1 || row2.row_closed) && (empty r2 || row1.row_closed)
|
|
&& List.for_all
|
|
(fun (_,f1,f2) ->
|
|
row_field_repr f1 = Rabsent || row_field_repr f2 = Rabsent)
|
|
pairs
|
|
then raise (Unify [mkvariant [] true, mkvariant [] true]);
|
|
let name =
|
|
if row1.row_name <> None && (row1.row_closed || empty r2) &&
|
|
(not row2.row_closed || keep (fun f1 f2 -> f1, f2) && empty r1)
|
|
then row1.row_name
|
|
else if row2.row_name <> None && (row2.row_closed || empty r1) &&
|
|
(not row1.row_closed || keep (fun f1 f2 -> f2, f1) && empty r2)
|
|
then row2.row_name
|
|
else None
|
|
in
|
|
let row0 = {row_fields = []; row_more = more; row_bound = ();
|
|
row_closed = closed; row_fixed = fixed; row_name = name} in
|
|
let set_more row rest =
|
|
let rest =
|
|
if closed then
|
|
filter_row_fields row.row_closed rest
|
|
else rest in
|
|
if rest <> [] && (row.row_closed || row.row_fixed)
|
|
|| closed && row.row_fixed && not row.row_closed then begin
|
|
let t1 = mkvariant [] true and t2 = mkvariant rest false in
|
|
raise (Unify [if row == row1 then (t1,t2) else (t2,t1)])
|
|
end;
|
|
let rm = row_more row in
|
|
if row.row_fixed then
|
|
if row0.row_more == rm then () else
|
|
if rm.desc = Tvar then link_type rm row0.row_more else
|
|
unify env rm row0.row_more
|
|
else
|
|
let ty = newty2 generic_level (Tvariant {row0 with row_fields = rest}) in
|
|
update_level env rm.level ty;
|
|
link_type rm ty
|
|
in
|
|
let md1 = rm1.desc and md2 = rm2.desc in
|
|
begin try
|
|
set_more row2 r1;
|
|
set_more row1 r2;
|
|
List.iter
|
|
(fun (l,f1,f2) ->
|
|
try unify_row_field env row1.row_fixed row2.row_fixed more l f1 f2
|
|
with Unify trace ->
|
|
raise (Unify ((mkvariant [l,f1] true,
|
|
mkvariant [l,f2] true) :: trace)))
|
|
pairs;
|
|
with exn ->
|
|
log_type rm1; rm1.desc <- md1; log_type rm2; rm2.desc <- md2; raise exn
|
|
end
|
|
|
|
and unify_row_field env fixed1 fixed2 more l f1 f2 =
|
|
let f1 = row_field_repr f1 and f2 = row_field_repr f2 in
|
|
if f1 == f2 then () else
|
|
match f1, f2 with
|
|
Rpresent(Some t1), Rpresent(Some t2) -> unify env t1 t2
|
|
| Rpresent None, Rpresent None -> ()
|
|
| Reither(c1, tl1, m1, e1), Reither(c2, tl2, m2, e2) ->
|
|
if e1 == e2 then () else
|
|
let redo =
|
|
(m1 || m2 ||
|
|
!rigid_variants && (List.length tl1 = 1 || List.length tl2 = 1)) &&
|
|
begin match tl1 @ tl2 with [] -> false
|
|
| t1 :: tl ->
|
|
if c1 || c2 then raise (Unify []);
|
|
List.iter (unify env t1) tl;
|
|
!e1 <> None || !e2 <> None
|
|
end in
|
|
if redo then unify_row_field env fixed1 fixed2 more l f1 f2 else
|
|
let tl1 = List.map repr tl1 and tl2 = List.map repr tl2 in
|
|
let rec remq tl = function [] -> []
|
|
| ty :: tl' ->
|
|
if List.memq ty tl then remq tl tl' else ty :: remq tl tl'
|
|
in
|
|
let tl2' = remq tl2 tl1 and tl1' = remq tl1 tl2 in
|
|
(* Is this handling of levels really principal? *)
|
|
List.iter (update_level env (repr more).level) (tl1' @ tl2');
|
|
let e = ref None in
|
|
let f1' = Reither(c1 || c2, tl1', m1 || m2, e)
|
|
and f2' = Reither(c1 || c2, tl2', m1 || m2, e) in
|
|
set_row_field e1 f1'; set_row_field e2 f2';
|
|
| Reither(_, _, false, e1), Rabsent -> set_row_field e1 f2
|
|
| Rabsent, Reither(_, _, false, e2) -> set_row_field e2 f1
|
|
| Rabsent, Rabsent -> ()
|
|
| Reither(false, tl, _, e1), Rpresent(Some t2) when not fixed1 ->
|
|
set_row_field e1 f2;
|
|
(try List.iter (fun t1 -> unify env t1 t2) tl
|
|
with exn -> e1 := None; raise exn)
|
|
| Rpresent(Some t1), Reither(false, tl, _, e2) when not fixed2 ->
|
|
set_row_field e2 f1;
|
|
(try List.iter (unify env t1) tl
|
|
with exn -> e2 := None; raise exn)
|
|
| Reither(true, [], _, e1), Rpresent None when not fixed1 ->
|
|
set_row_field e1 f2
|
|
| Rpresent None, Reither(true, [], _, e2) when not fixed2 ->
|
|
set_row_field e2 f1
|
|
| _ -> raise (Unify [])
|
|
|
|
|
|
let unify env ty1 ty2 =
|
|
try
|
|
unify env ty1 ty2
|
|
with Unify trace ->
|
|
raise (Unify (expand_trace env trace))
|
|
|
|
let unify_var env t1 t2 =
|
|
let t1 = repr t1 and t2 = repr t2 in
|
|
if t1 == t2 then () else
|
|
match t1.desc with
|
|
Tvar ->
|
|
begin try
|
|
occur env t1 t2;
|
|
update_level env t1.level t2;
|
|
link_type t1 t2
|
|
with Unify trace ->
|
|
raise (Unify (expand_trace env ((t1,t2)::trace)))
|
|
end
|
|
| _ ->
|
|
unify env t1 t2
|
|
|
|
let _ = unify' := unify_var
|
|
|
|
let unify_pairs env ty1 ty2 pairs =
|
|
univar_pairs := pairs;
|
|
unify env ty1 ty2
|
|
|
|
let unify env ty1 ty2 =
|
|
univar_pairs := [];
|
|
unify env ty1 ty2
|
|
|
|
|
|
(**** Special cases of unification ****)
|
|
|
|
(*
|
|
Unify [t] and [l:'a -> 'b]. Return ['a] and ['b].
|
|
In label mode, label mismatch is accepted when
|
|
(1) the requested label is ""
|
|
(2) the original label is not optional
|
|
*)
|
|
let rec filter_arrow env t l =
|
|
let t = expand_head_unif env t in
|
|
match t.desc with
|
|
Tvar ->
|
|
let t1 = newvar () and t2 = newvar () in
|
|
let t' = newty (Tarrow (l, t1, t2, Cok)) in
|
|
update_level env t.level t';
|
|
link_type t t';
|
|
(t1, t2)
|
|
| Tarrow(l', t1, t2, _)
|
|
when l = l' || !Clflags.classic && l = "" && not (is_optional l') ->
|
|
(t1, t2)
|
|
| _ ->
|
|
raise (Unify [])
|
|
|
|
(* Used by [filter_method]. *)
|
|
let rec filter_method_field env name priv ty =
|
|
let ty = repr ty in
|
|
match ty.desc with
|
|
Tvar ->
|
|
let level = ty.level in
|
|
let ty1 = newvar2 level and ty2 = newvar2 level in
|
|
let ty' = newty2 level (Tfield (name,
|
|
begin match priv with
|
|
Private -> Fvar (ref None)
|
|
| Public -> Fpresent
|
|
end,
|
|
ty1, ty2))
|
|
in
|
|
link_type ty ty';
|
|
ty1
|
|
| Tfield(n, kind, ty1, ty2) ->
|
|
let kind = field_kind_repr kind in
|
|
if (n = name) && (kind <> Fabsent) then begin
|
|
if priv = Public then
|
|
unify_kind kind Fpresent;
|
|
ty1
|
|
end else
|
|
filter_method_field env name priv ty2
|
|
| _ ->
|
|
raise (Unify [])
|
|
|
|
(* Unify [ty] and [< name : 'a; .. >]. Return ['a]. *)
|
|
let rec filter_method env name priv ty =
|
|
let ty = expand_head_unif env ty in
|
|
match ty.desc with
|
|
Tvar ->
|
|
let ty1 = newvar () in
|
|
let ty' = newobj ty1 in
|
|
update_level env ty.level ty';
|
|
link_type ty ty';
|
|
filter_method_field env name priv ty1
|
|
| Tobject(f, _) ->
|
|
filter_method_field env name priv f
|
|
| _ ->
|
|
raise (Unify [])
|
|
|
|
let check_filter_method env name priv ty =
|
|
ignore(filter_method env name priv ty)
|
|
|
|
let filter_self_method env lab priv meths ty =
|
|
let ty' = filter_method env lab priv ty in
|
|
try
|
|
Meths.find lab !meths
|
|
with Not_found ->
|
|
let pair = (Ident.create lab, ty') in
|
|
meths := Meths.add lab pair !meths;
|
|
pair
|
|
|
|
|
|
(***********************************)
|
|
(* Matching between type schemes *)
|
|
(***********************************)
|
|
|
|
(*
|
|
Update the level of [ty]. First check that the levels of generic
|
|
variables from the subject are not lowered.
|
|
*)
|
|
let moregen_occur env level ty =
|
|
let rec occur ty =
|
|
let ty = repr ty in
|
|
if ty.level > level then begin
|
|
if ty.desc = Tvar && ty.level >= generic_level - 1 then raise Occur;
|
|
ty.level <- pivot_level - ty.level;
|
|
match ty.desc with
|
|
Tvariant row when static_row row ->
|
|
iter_row occur row
|
|
| _ ->
|
|
iter_type_expr occur ty
|
|
end
|
|
in
|
|
begin try
|
|
occur ty; unmark_type ty
|
|
with Occur ->
|
|
unmark_type ty; raise (Unify [])
|
|
end;
|
|
(* also check for free univars *)
|
|
occur_univar env ty;
|
|
update_level env level ty
|
|
|
|
let may_instantiate inst_nongen t1 =
|
|
if inst_nongen then t1.level <> generic_level - 1
|
|
else t1.level = generic_level
|
|
|
|
let rec moregen inst_nongen type_pairs env t1 t2 =
|
|
if t1 == t2 then () else
|
|
let t1 = repr t1 in
|
|
let t2 = repr t2 in
|
|
if t1 == t2 then () else
|
|
|
|
try
|
|
match (t1.desc, t2.desc) with
|
|
(Tunivar, Tunivar) ->
|
|
unify_univar t1 t2 !univar_pairs
|
|
| (Tvar, _) when may_instantiate inst_nongen t1 ->
|
|
moregen_occur env t1.level t2;
|
|
occur env t1 t2;
|
|
link_type t1 t2
|
|
| (Tconstr (p1, [], _), Tconstr (p2, [], _)) when Path.same p1 p2 ->
|
|
()
|
|
| _ ->
|
|
let t1' = expand_head_unif env t1 in
|
|
let t2' = expand_head_unif env t2 in
|
|
(* Expansion may have changed the representative of the types... *)
|
|
let t1' = repr t1' and t2' = repr t2' in
|
|
if t1' == t2' then () else
|
|
begin try
|
|
TypePairs.find type_pairs (t1', t2')
|
|
with Not_found ->
|
|
TypePairs.add type_pairs (t1', t2') ();
|
|
match (t1'.desc, t2'.desc) with
|
|
(Tvar, _) when may_instantiate inst_nongen t1' ->
|
|
moregen_occur env t1'.level t2;
|
|
link_type t1' t2
|
|
| (Tarrow (l1, t1, u1, _), Tarrow (l2, t2, u2, _)) when l1 = l2
|
|
|| !Clflags.classic && not (is_optional l1 || is_optional l2) ->
|
|
moregen inst_nongen type_pairs env t1 t2;
|
|
moregen inst_nongen type_pairs env u1 u2
|
|
| (Ttuple tl1, Ttuple tl2) ->
|
|
moregen_list inst_nongen type_pairs env tl1 tl2
|
|
| (Tconstr (p1, tl1, _), Tconstr (p2, tl2, _))
|
|
when Path.same p1 p2 ->
|
|
moregen_list inst_nongen type_pairs env tl1 tl2
|
|
| Tpackage (p1, n1, tl1), Tpackage (p2, n2, tl2) when Path.same p1 p2 && n1 = n2 ->
|
|
moregen_list inst_nongen type_pairs env tl1 tl2
|
|
| (Tvariant row1, Tvariant row2) ->
|
|
moregen_row inst_nongen type_pairs env row1 row2
|
|
| (Tobject (fi1, nm1), Tobject (fi2, nm2)) ->
|
|
moregen_fields inst_nongen type_pairs env fi1 fi2
|
|
| (Tfield _, Tfield _) -> (* Actually unused *)
|
|
moregen_fields inst_nongen type_pairs env t1' t2'
|
|
| (Tnil, Tnil) ->
|
|
()
|
|
| (Tpoly (t1, []), Tpoly (t2, [])) ->
|
|
moregen inst_nongen type_pairs env t1 t2
|
|
| (Tpoly (t1, tl1), Tpoly (t2, tl2)) ->
|
|
enter_poly env univar_pairs t1 tl1 t2 tl2
|
|
(moregen inst_nongen type_pairs env)
|
|
| (_, _) ->
|
|
raise (Unify [])
|
|
end
|
|
with Unify trace ->
|
|
raise (Unify ((t1, t2)::trace))
|
|
|
|
and moregen_list inst_nongen type_pairs env tl1 tl2 =
|
|
if List.length tl1 <> List.length tl2 then
|
|
raise (Unify []);
|
|
List.iter2 (moregen inst_nongen type_pairs env) tl1 tl2
|
|
|
|
and moregen_fields inst_nongen type_pairs env ty1 ty2 =
|
|
let (fields1, rest1) = flatten_fields ty1
|
|
and (fields2, rest2) = flatten_fields ty2 in
|
|
let (pairs, miss1, miss2) = associate_fields fields1 fields2 in
|
|
if miss1 <> [] then raise (Unify []);
|
|
moregen inst_nongen type_pairs env rest1
|
|
(build_fields (repr ty2).level miss2 rest2);
|
|
List.iter
|
|
(fun (n, k1, t1, k2, t2) ->
|
|
moregen_kind k1 k2;
|
|
try moregen inst_nongen type_pairs env t1 t2 with Unify trace ->
|
|
raise (Unify ((newty (Tfield(n, k1, t1, rest2)),
|
|
newty (Tfield(n, k2, t2, rest2)))::trace)))
|
|
pairs
|
|
|
|
and moregen_kind k1 k2 =
|
|
let k1 = field_kind_repr k1 in
|
|
let k2 = field_kind_repr k2 in
|
|
if k1 == k2 then () else
|
|
match k1, k2 with
|
|
(Fvar r, (Fvar _ | Fpresent)) -> set_kind r k2
|
|
| (Fpresent, Fpresent) -> ()
|
|
| _ -> raise (Unify [])
|
|
|
|
and moregen_row inst_nongen type_pairs env row1 row2 =
|
|
let row1 = row_repr row1 and row2 = row_repr row2 in
|
|
let rm1 = repr row1.row_more and rm2 = repr row2.row_more in
|
|
if rm1 == rm2 then () else
|
|
let may_inst = rm1.desc = Tvar && may_instantiate inst_nongen rm1 in
|
|
let r1, r2, pairs = merge_row_fields row1.row_fields row2.row_fields in
|
|
let r1, r2 =
|
|
if row2.row_closed then
|
|
filter_row_fields may_inst r1, filter_row_fields false r2
|
|
else r1, r2
|
|
in
|
|
if r1 <> [] || row1.row_closed && (not row2.row_closed || r2 <> [])
|
|
then raise (Unify []);
|
|
begin match rm1.desc, rm2.desc with
|
|
Tunivar, Tunivar ->
|
|
unify_univar rm1 rm2 !univar_pairs
|
|
| Tunivar, _ | _, Tunivar ->
|
|
raise (Unify [])
|
|
| _ when static_row row1 -> ()
|
|
| _ when may_inst ->
|
|
if not (static_row row2) then moregen_occur env rm1.level rm2;
|
|
let ext =
|
|
if r2 = [] then rm2 else
|
|
let row_ext = {row2 with row_fields = r2} in
|
|
iter_row (moregen_occur env rm1.level) row_ext;
|
|
newty2 rm1.level (Tvariant row_ext)
|
|
in
|
|
link_type rm1 ext
|
|
| Tconstr _, Tconstr _ ->
|
|
moregen inst_nongen type_pairs env rm1 rm2
|
|
| _ -> raise (Unify [])
|
|
end;
|
|
List.iter
|
|
(fun (l,f1,f2) ->
|
|
let f1 = row_field_repr f1 and f2 = row_field_repr f2 in
|
|
if f1 == f2 then () else
|
|
match f1, f2 with
|
|
Rpresent(Some t1), Rpresent(Some t2) ->
|
|
moregen inst_nongen type_pairs env t1 t2
|
|
| Rpresent None, Rpresent None -> ()
|
|
| Reither(false, tl1, _, e1), Rpresent(Some t2) when may_inst ->
|
|
set_row_field e1 f2;
|
|
List.iter (fun t1 -> moregen inst_nongen type_pairs env t1 t2) tl1
|
|
| Reither(c1, tl1, _, e1), Reither(c2, tl2, m2, e2) ->
|
|
if e1 != e2 then begin
|
|
if c1 && not c2 then raise(Unify []);
|
|
set_row_field e1 (Reither (c2, [], m2, e2));
|
|
if List.length tl1 = List.length tl2 then
|
|
List.iter2 (moregen inst_nongen type_pairs env) tl1 tl2
|
|
else match tl2 with
|
|
t2 :: _ ->
|
|
List.iter (fun t1 -> moregen inst_nongen type_pairs env t1 t2)
|
|
tl1
|
|
| [] ->
|
|
if tl1 <> [] then raise (Unify [])
|
|
end
|
|
| Reither(true, [], _, e1), Rpresent None when may_inst ->
|
|
set_row_field e1 f2
|
|
| Reither(_, _, _, e1), Rabsent when may_inst ->
|
|
set_row_field e1 f2
|
|
| Rabsent, Rabsent -> ()
|
|
| _ -> raise (Unify []))
|
|
pairs
|
|
|
|
(* Must empty univar_pairs first *)
|
|
let moregen inst_nongen type_pairs env patt subj =
|
|
univar_pairs := [];
|
|
moregen inst_nongen type_pairs env patt subj
|
|
|
|
(*
|
|
Non-generic variable can be instanciated only if [inst_nongen] is
|
|
true. So, [inst_nongen] should be set to false if the subject might
|
|
contain non-generic variables (and we do not want them to be
|
|
instanciated).
|
|
Usually, the subject is given by the user, and the pattern
|
|
is unimportant. So, no need to propagate abbreviations.
|
|
*)
|
|
let moregeneral env inst_nongen pat_sch subj_sch =
|
|
let old_level = !current_level in
|
|
current_level := generic_level - 1;
|
|
(*
|
|
Generic variables are first duplicated with [instance]. So,
|
|
their levels are lowered to [generic_level - 1]. The subject is
|
|
then copied with [duplicate_type]. That way, its levels won't be
|
|
changed.
|
|
*)
|
|
let subj = duplicate_type (instance subj_sch) in
|
|
current_level := generic_level;
|
|
(* Duplicate generic variables *)
|
|
let patt = instance pat_sch in
|
|
let res =
|
|
try moregen inst_nongen (TypePairs.create 13) env patt subj; true with
|
|
Unify _ -> false
|
|
in
|
|
current_level := old_level;
|
|
res
|
|
|
|
|
|
(* Alternative approach: "rigidify" a type scheme,
|
|
and check validity after unification *)
|
|
(* Simpler, no? *)
|
|
|
|
let rec rigidify_rec vars ty =
|
|
let ty = repr ty in
|
|
if ty.level >= lowest_level then begin
|
|
ty.level <- pivot_level - ty.level;
|
|
match ty.desc with
|
|
| Tvar ->
|
|
if not (List.memq ty !vars) then vars := ty :: !vars
|
|
| Tvariant row ->
|
|
let row = row_repr row in
|
|
let more = repr row.row_more in
|
|
if more.desc = Tvar && not row.row_fixed then begin
|
|
let more' = newty2 more.level Tvar in
|
|
let row' = {row with row_fixed=true; row_fields=[]; row_more=more'}
|
|
in link_type more (newty2 ty.level (Tvariant row'))
|
|
end;
|
|
iter_row (rigidify_rec vars) row;
|
|
(* only consider the row variable if the variant is not static *)
|
|
if not (static_row row) then rigidify_rec vars (row_more row)
|
|
| _ ->
|
|
iter_type_expr (rigidify_rec vars) ty
|
|
end
|
|
|
|
let rigidify ty =
|
|
let vars = ref [] in
|
|
rigidify_rec vars ty;
|
|
unmark_type ty;
|
|
!vars
|
|
|
|
let all_distinct_vars env vars =
|
|
let tyl = ref [] in
|
|
List.for_all
|
|
(fun ty ->
|
|
let ty = expand_head env ty in
|
|
if List.memq ty !tyl then false else
|
|
(tyl := ty :: !tyl; ty.desc = Tvar))
|
|
vars
|
|
|
|
let matches env ty ty' =
|
|
let snap = snapshot () in
|
|
let vars = rigidify ty in
|
|
cleanup_abbrev ();
|
|
let ok =
|
|
try unify env ty ty'; all_distinct_vars env vars
|
|
with Unify _ -> false
|
|
in
|
|
backtrack snap;
|
|
ok
|
|
|
|
|
|
(*********************************************)
|
|
(* Equivalence between parameterized types *)
|
|
(*********************************************)
|
|
|
|
let expand_head_rigid env ty =
|
|
let old = !rigid_variants in
|
|
rigid_variants := true;
|
|
let ty' = expand_head_unif env ty in
|
|
rigid_variants := old; ty'
|
|
|
|
let normalize_subst subst =
|
|
if List.exists
|
|
(function {desc=Tlink _}, _ | _, {desc=Tlink _} -> true | _ -> false)
|
|
!subst
|
|
then subst := List.map (fun (t1,t2) -> repr t1, repr t2) !subst
|
|
|
|
let rec eqtype rename type_pairs subst env t1 t2 =
|
|
if t1 == t2 then () else
|
|
let t1 = repr t1 in
|
|
let t2 = repr t2 in
|
|
if t1 == t2 then () else
|
|
|
|
try
|
|
match (t1.desc, t2.desc) with
|
|
(Tvar, Tvar) when rename ->
|
|
begin try
|
|
normalize_subst subst;
|
|
if List.assq t1 !subst != t2 then raise (Unify [])
|
|
with Not_found ->
|
|
if List.exists (fun (_, t) -> t == t2) !subst then raise (Unify []);
|
|
subst := (t1, t2) :: !subst
|
|
end
|
|
| (Tconstr (p1, [], _), Tconstr (p2, [], _)) when Path.same p1 p2 ->
|
|
()
|
|
| _ ->
|
|
let t1' = expand_head_rigid env t1 in
|
|
let t2' = expand_head_rigid env t2 in
|
|
(* Expansion may have changed the representative of the types... *)
|
|
let t1' = repr t1' and t2' = repr t2' in
|
|
if t1' == t2' then () else
|
|
begin try
|
|
TypePairs.find type_pairs (t1', t2')
|
|
with Not_found ->
|
|
TypePairs.add type_pairs (t1', t2') ();
|
|
match (t1'.desc, t2'.desc) with
|
|
(Tvar, Tvar) when rename ->
|
|
begin try
|
|
normalize_subst subst;
|
|
if List.assq t1' !subst != t2' then raise (Unify [])
|
|
with Not_found ->
|
|
if List.exists (fun (_, t) -> t == t2') !subst then raise (Unify []);
|
|
subst := (t1', t2') :: !subst
|
|
end
|
|
| (Tarrow (l1, t1, u1, _), Tarrow (l2, t2, u2, _)) when l1 = l2
|
|
|| !Clflags.classic && not (is_optional l1 || is_optional l2) ->
|
|
eqtype rename type_pairs subst env t1 t2;
|
|
eqtype rename type_pairs subst env u1 u2;
|
|
| (Ttuple tl1, Ttuple tl2) ->
|
|
eqtype_list rename type_pairs subst env tl1 tl2
|
|
| (Tconstr (p1, tl1, _), Tconstr (p2, tl2, _))
|
|
when Path.same p1 p2 ->
|
|
eqtype_list rename type_pairs subst env tl1 tl2
|
|
| Tpackage (p1, n1, tl1), Tpackage (p2, n2, tl2) when Path.same p1 p2 && n1 = n2 ->
|
|
eqtype_list rename type_pairs subst env tl1 tl2
|
|
| (Tvariant row1, Tvariant row2) ->
|
|
eqtype_row rename type_pairs subst env row1 row2
|
|
| (Tobject (fi1, nm1), Tobject (fi2, nm2)) ->
|
|
eqtype_fields rename type_pairs subst env fi1 fi2
|
|
| (Tfield _, Tfield _) -> (* Actually unused *)
|
|
eqtype_fields rename type_pairs subst env t1' t2'
|
|
| (Tnil, Tnil) ->
|
|
()
|
|
| (Tpoly (t1, []), Tpoly (t2, [])) ->
|
|
eqtype rename type_pairs subst env t1 t2
|
|
| (Tpoly (t1, tl1), Tpoly (t2, tl2)) ->
|
|
enter_poly env univar_pairs t1 tl1 t2 tl2
|
|
(eqtype rename type_pairs subst env)
|
|
| (Tunivar, Tunivar) ->
|
|
unify_univar t1' t2' !univar_pairs
|
|
| (_, _) ->
|
|
raise (Unify [])
|
|
end
|
|
with Unify trace ->
|
|
raise (Unify ((t1, t2)::trace))
|
|
|
|
and eqtype_list rename type_pairs subst env tl1 tl2 =
|
|
if List.length tl1 <> List.length tl2 then
|
|
raise (Unify []);
|
|
List.iter2 (eqtype rename type_pairs subst env) tl1 tl2
|
|
|
|
and eqtype_fields rename type_pairs subst env ty1 ty2 =
|
|
let (fields2, rest2) = flatten_fields ty2 in
|
|
(* Try expansion, needed when called from Includecore.type_manifest *)
|
|
match expand_head_rigid env rest2 with
|
|
{desc=Tobject(ty2,_)} -> eqtype_fields rename type_pairs subst env ty1 ty2
|
|
| _ ->
|
|
let (fields1, rest1) = flatten_fields ty1 in
|
|
let (pairs, miss1, miss2) = associate_fields fields1 fields2 in
|
|
eqtype rename type_pairs subst env rest1 rest2;
|
|
if (miss1 <> []) || (miss2 <> []) then raise (Unify []);
|
|
List.iter
|
|
(function (n, k1, t1, k2, t2) ->
|
|
eqtype_kind k1 k2;
|
|
try eqtype rename type_pairs subst env t1 t2 with Unify trace ->
|
|
raise (Unify ((newty (Tfield(n, k1, t1, rest2)),
|
|
newty (Tfield(n, k2, t2, rest2)))::trace)))
|
|
pairs
|
|
|
|
and eqtype_kind k1 k2 =
|
|
let k1 = field_kind_repr k1 in
|
|
let k2 = field_kind_repr k2 in
|
|
match k1, k2 with
|
|
(Fvar _, Fvar _)
|
|
| (Fpresent, Fpresent) -> ()
|
|
| _ -> raise (Unify [])
|
|
|
|
and eqtype_row rename type_pairs subst env row1 row2 =
|
|
(* Try expansion, needed when called from Includecore.type_manifest *)
|
|
match expand_head_rigid env (row_more row2) with
|
|
{desc=Tvariant row2} -> eqtype_row rename type_pairs subst env row1 row2
|
|
| _ ->
|
|
let row1 = row_repr row1 and row2 = row_repr row2 in
|
|
let r1, r2, pairs = merge_row_fields row1.row_fields row2.row_fields in
|
|
if row1.row_closed <> row2.row_closed
|
|
|| not row1.row_closed && (r1 <> [] || r2 <> [])
|
|
|| filter_row_fields false (r1 @ r2) <> []
|
|
then raise (Unify []);
|
|
if not (static_row row1) then
|
|
eqtype rename type_pairs subst env row1.row_more row2.row_more;
|
|
List.iter
|
|
(fun (_,f1,f2) ->
|
|
match row_field_repr f1, row_field_repr f2 with
|
|
Rpresent(Some t1), Rpresent(Some t2) ->
|
|
eqtype rename type_pairs subst env t1 t2
|
|
| Reither(true, [], _, _), Reither(true, [], _, _) ->
|
|
()
|
|
| Reither(false, t1::tl1, _, _), Reither(false, t2::tl2, _, _) ->
|
|
eqtype rename type_pairs subst env t1 t2;
|
|
if List.length tl1 = List.length tl2 then
|
|
(* if same length allow different types (meaning?) *)
|
|
List.iter2 (eqtype rename type_pairs subst env) tl1 tl2
|
|
else begin
|
|
(* otherwise everything must be equal *)
|
|
List.iter (eqtype rename type_pairs subst env t1) tl2;
|
|
List.iter (fun t1 -> eqtype rename type_pairs subst env t1 t2) tl1
|
|
end
|
|
| Rpresent None, Rpresent None -> ()
|
|
| Rabsent, Rabsent -> ()
|
|
| _ -> raise (Unify []))
|
|
pairs
|
|
|
|
(* Two modes: with or without renaming of variables *)
|
|
let equal env rename tyl1 tyl2 =
|
|
try
|
|
univar_pairs := [];
|
|
eqtype_list rename (TypePairs.create 11) (ref []) env tyl1 tyl2; true
|
|
with
|
|
Unify _ -> false
|
|
|
|
(* Must empty univar_pairs first *)
|
|
let eqtype rename type_pairs subst env t1 t2 =
|
|
univar_pairs := [];
|
|
eqtype rename type_pairs subst env t1 t2
|
|
|
|
|
|
(*************************)
|
|
(* Class type matching *)
|
|
(*************************)
|
|
|
|
|
|
type class_match_failure =
|
|
CM_Virtual_class
|
|
| CM_Parameter_arity_mismatch of int * int
|
|
| CM_Type_parameter_mismatch of (type_expr * type_expr) list
|
|
| CM_Class_type_mismatch of class_type * class_type
|
|
| CM_Parameter_mismatch of (type_expr * type_expr) list
|
|
| CM_Val_type_mismatch of string * (type_expr * type_expr) list
|
|
| CM_Meth_type_mismatch of string * (type_expr * type_expr) list
|
|
| CM_Non_mutable_value of string
|
|
| CM_Non_concrete_value of string
|
|
| CM_Missing_value of string
|
|
| CM_Missing_method of string
|
|
| CM_Hide_public of string
|
|
| CM_Hide_virtual of string * string
|
|
| CM_Public_method of string
|
|
| CM_Private_method of string
|
|
| CM_Virtual_method of string
|
|
|
|
exception Failure of class_match_failure list
|
|
|
|
let rec moregen_clty trace type_pairs env cty1 cty2 =
|
|
try
|
|
match cty1, cty2 with
|
|
Tcty_constr (_, _, cty1), _ ->
|
|
moregen_clty true type_pairs env cty1 cty2
|
|
| _, Tcty_constr (_, _, cty2) ->
|
|
moregen_clty true type_pairs env cty1 cty2
|
|
| Tcty_fun (l1, ty1, cty1'), Tcty_fun (l2, ty2, cty2') when l1 = l2 ->
|
|
begin try moregen true type_pairs env ty1 ty2 with Unify trace ->
|
|
raise (Failure [CM_Parameter_mismatch (expand_trace env trace)])
|
|
end;
|
|
moregen_clty false type_pairs env cty1' cty2'
|
|
| Tcty_signature sign1, Tcty_signature sign2 ->
|
|
let ty1 = object_fields (repr sign1.cty_self) in
|
|
let ty2 = object_fields (repr sign2.cty_self) in
|
|
let (fields1, rest1) = flatten_fields ty1
|
|
and (fields2, rest2) = flatten_fields ty2 in
|
|
let (pairs, miss1, miss2) = associate_fields fields1 fields2 in
|
|
List.iter
|
|
(fun (lab, k1, t1, k2, t2) ->
|
|
begin try moregen true type_pairs env t1 t2 with Unify trace ->
|
|
raise (Failure [CM_Meth_type_mismatch
|
|
(lab, expand_trace env trace)])
|
|
end)
|
|
pairs;
|
|
Vars.iter
|
|
(fun lab (mut, v, ty) ->
|
|
let (mut', v', ty') = Vars.find lab sign1.cty_vars in
|
|
try moregen true type_pairs env ty' ty with Unify trace ->
|
|
raise (Failure [CM_Val_type_mismatch
|
|
(lab, expand_trace env trace)]))
|
|
sign2.cty_vars
|
|
| _ ->
|
|
raise (Failure [])
|
|
with
|
|
Failure error when trace || error = [] ->
|
|
raise (Failure (CM_Class_type_mismatch (cty1, cty2)::error))
|
|
|
|
let match_class_types ?(trace=true) env pat_sch subj_sch =
|
|
let type_pairs = TypePairs.create 53 in
|
|
let old_level = !current_level in
|
|
current_level := generic_level - 1;
|
|
(*
|
|
Generic variables are first duplicated with [instance]. So,
|
|
their levels are lowered to [generic_level - 1]. The subject is
|
|
then copied with [duplicate_type]. That way, its levels won't be
|
|
changed.
|
|
*)
|
|
let (_, subj_inst) = instance_class [] subj_sch in
|
|
let subj = duplicate_class_type subj_inst in
|
|
current_level := generic_level;
|
|
(* Duplicate generic variables *)
|
|
let (_, patt) = instance_class [] pat_sch in
|
|
let res =
|
|
let sign1 = signature_of_class_type patt in
|
|
let sign2 = signature_of_class_type subj in
|
|
let t1 = repr sign1.cty_self in
|
|
let t2 = repr sign2.cty_self in
|
|
TypePairs.add type_pairs (t1, t2) ();
|
|
let (fields1, rest1) = flatten_fields (object_fields t1)
|
|
and (fields2, rest2) = flatten_fields (object_fields t2) in
|
|
let (pairs, miss1, miss2) = associate_fields fields1 fields2 in
|
|
let error =
|
|
List.fold_right
|
|
(fun (lab, k, _) err ->
|
|
let err =
|
|
let k = field_kind_repr k in
|
|
begin match k with
|
|
Fvar r -> set_kind r Fabsent; err
|
|
| _ -> CM_Hide_public lab::err
|
|
end
|
|
in
|
|
if Concr.mem lab sign1.cty_concr then err
|
|
else CM_Hide_virtual ("method", lab) :: err)
|
|
miss1 []
|
|
in
|
|
let missing_method = List.map (fun (m, _, _) -> m) miss2 in
|
|
let error =
|
|
(List.map (fun m -> CM_Missing_method m) missing_method) @ error
|
|
in
|
|
(* Always succeeds *)
|
|
moregen true type_pairs env rest1 rest2;
|
|
let error =
|
|
List.fold_right
|
|
(fun (lab, k1, t1, k2, t2) err ->
|
|
try moregen_kind k1 k2; err with
|
|
Unify _ -> CM_Public_method lab::err)
|
|
pairs error
|
|
in
|
|
let error =
|
|
Vars.fold
|
|
(fun lab (mut, vr, ty) err ->
|
|
try
|
|
let (mut', vr', ty') = Vars.find lab sign1.cty_vars in
|
|
if mut = Mutable && mut' <> Mutable then
|
|
CM_Non_mutable_value lab::err
|
|
else if vr = Concrete && vr' <> Concrete then
|
|
CM_Non_concrete_value lab::err
|
|
else
|
|
err
|
|
with Not_found ->
|
|
CM_Missing_value lab::err)
|
|
sign2.cty_vars error
|
|
in
|
|
let error =
|
|
Vars.fold
|
|
(fun lab (_,vr,_) err ->
|
|
if vr = Virtual && not (Vars.mem lab sign2.cty_vars) then
|
|
CM_Hide_virtual ("instance variable", lab) :: err
|
|
else err)
|
|
sign1.cty_vars error
|
|
in
|
|
let error =
|
|
List.fold_right
|
|
(fun e l ->
|
|
if List.mem e missing_method then l else CM_Virtual_method e::l)
|
|
(Concr.elements (Concr.diff sign2.cty_concr sign1.cty_concr))
|
|
error
|
|
in
|
|
match error with
|
|
[] ->
|
|
begin try
|
|
moregen_clty trace type_pairs env patt subj;
|
|
[]
|
|
with
|
|
Failure r -> r
|
|
end
|
|
| error ->
|
|
CM_Class_type_mismatch (patt, subj)::error
|
|
in
|
|
current_level := old_level;
|
|
res
|
|
|
|
let rec equal_clty trace type_pairs subst env cty1 cty2 =
|
|
try
|
|
match cty1, cty2 with
|
|
Tcty_constr (_, _, cty1), Tcty_constr (_, _, cty2) ->
|
|
equal_clty true type_pairs subst env cty1 cty2
|
|
| Tcty_constr (_, _, cty1), _ ->
|
|
equal_clty true type_pairs subst env cty1 cty2
|
|
| _, Tcty_constr (_, _, cty2) ->
|
|
equal_clty true type_pairs subst env cty1 cty2
|
|
| Tcty_fun (l1, ty1, cty1'), Tcty_fun (l2, ty2, cty2') when l1 = l2 ->
|
|
begin try eqtype true type_pairs subst env ty1 ty2 with Unify trace ->
|
|
raise (Failure [CM_Parameter_mismatch (expand_trace env trace)])
|
|
end;
|
|
equal_clty false type_pairs subst env cty1' cty2'
|
|
| Tcty_signature sign1, Tcty_signature sign2 ->
|
|
let ty1 = object_fields (repr sign1.cty_self) in
|
|
let ty2 = object_fields (repr sign2.cty_self) in
|
|
let (fields1, rest1) = flatten_fields ty1
|
|
and (fields2, rest2) = flatten_fields ty2 in
|
|
let (pairs, miss1, miss2) = associate_fields fields1 fields2 in
|
|
List.iter
|
|
(fun (lab, k1, t1, k2, t2) ->
|
|
begin try eqtype true type_pairs subst env t1 t2 with
|
|
Unify trace ->
|
|
raise (Failure [CM_Meth_type_mismatch
|
|
(lab, expand_trace env trace)])
|
|
end)
|
|
pairs;
|
|
Vars.iter
|
|
(fun lab (_, _, ty) ->
|
|
let (_, _, ty') = Vars.find lab sign1.cty_vars in
|
|
try eqtype true type_pairs subst env ty' ty with Unify trace ->
|
|
raise (Failure [CM_Val_type_mismatch
|
|
(lab, expand_trace env trace)]))
|
|
sign2.cty_vars
|
|
| _ ->
|
|
raise
|
|
(Failure (if trace then []
|
|
else [CM_Class_type_mismatch (cty1, cty2)]))
|
|
with
|
|
Failure error when trace ->
|
|
raise (Failure (CM_Class_type_mismatch (cty1, cty2)::error))
|
|
|
|
let match_class_declarations env patt_params patt_type subj_params subj_type =
|
|
let type_pairs = TypePairs.create 53 in
|
|
let subst = ref [] in
|
|
let sign1 = signature_of_class_type patt_type in
|
|
let sign2 = signature_of_class_type subj_type in
|
|
let t1 = repr sign1.cty_self in
|
|
let t2 = repr sign2.cty_self in
|
|
TypePairs.add type_pairs (t1, t2) ();
|
|
let (fields1, rest1) = flatten_fields (object_fields t1)
|
|
and (fields2, rest2) = flatten_fields (object_fields t2) in
|
|
let (pairs, miss1, miss2) = associate_fields fields1 fields2 in
|
|
let error =
|
|
List.fold_right
|
|
(fun (lab, k, _) err ->
|
|
let err =
|
|
let k = field_kind_repr k in
|
|
begin match k with
|
|
Fvar r -> err
|
|
| _ -> CM_Hide_public lab::err
|
|
end
|
|
in
|
|
if Concr.mem lab sign1.cty_concr then err
|
|
else CM_Hide_virtual ("method", lab) :: err)
|
|
miss1 []
|
|
in
|
|
let missing_method = List.map (fun (m, _, _) -> m) miss2 in
|
|
let error =
|
|
(List.map (fun m -> CM_Missing_method m) missing_method) @ error
|
|
in
|
|
(* Always succeeds *)
|
|
eqtype true type_pairs subst env rest1 rest2;
|
|
let error =
|
|
List.fold_right
|
|
(fun (lab, k1, t1, k2, t2) err ->
|
|
let k1 = field_kind_repr k1 in
|
|
let k2 = field_kind_repr k2 in
|
|
match k1, k2 with
|
|
(Fvar _, Fvar _)
|
|
| (Fpresent, Fpresent) -> err
|
|
| (Fvar _, Fpresent) -> CM_Private_method lab::err
|
|
| (Fpresent, Fvar _) -> CM_Public_method lab::err
|
|
| _ -> assert false)
|
|
pairs error
|
|
in
|
|
let error =
|
|
Vars.fold
|
|
(fun lab (mut, vr, ty) err ->
|
|
try
|
|
let (mut', vr', ty') = Vars.find lab sign1.cty_vars in
|
|
if mut = Mutable && mut' <> Mutable then
|
|
CM_Non_mutable_value lab::err
|
|
else if vr = Concrete && vr' <> Concrete then
|
|
CM_Non_concrete_value lab::err
|
|
else
|
|
err
|
|
with Not_found ->
|
|
CM_Missing_value lab::err)
|
|
sign2.cty_vars error
|
|
in
|
|
let error =
|
|
Vars.fold
|
|
(fun lab (_,vr,_) err ->
|
|
if vr = Virtual && not (Vars.mem lab sign2.cty_vars) then
|
|
CM_Hide_virtual ("instance variable", lab) :: err
|
|
else err)
|
|
sign1.cty_vars error
|
|
in
|
|
let error =
|
|
List.fold_right
|
|
(fun e l ->
|
|
if List.mem e missing_method then l else CM_Virtual_method e::l)
|
|
(Concr.elements (Concr.diff sign2.cty_concr sign1.cty_concr))
|
|
error
|
|
in
|
|
match error with
|
|
[] ->
|
|
begin try
|
|
let lp = List.length patt_params in
|
|
let ls = List.length subj_params in
|
|
if lp <> ls then
|
|
raise (Failure [CM_Parameter_arity_mismatch (lp, ls)]);
|
|
List.iter2 (fun p s ->
|
|
try eqtype true type_pairs subst env p s with Unify trace ->
|
|
raise (Failure [CM_Type_parameter_mismatch
|
|
(expand_trace env trace)]))
|
|
patt_params subj_params;
|
|
(* old code: equal_clty false type_pairs subst env patt_type subj_type; *)
|
|
equal_clty false type_pairs subst env
|
|
(Tcty_signature sign1) (Tcty_signature sign2);
|
|
(* Use moregeneral for class parameters, need to recheck everything to
|
|
keeps relationships (PR#4824) *)
|
|
let clty_params = List.fold_right (fun ty cty -> Tcty_fun ("*",ty,cty)) in
|
|
match_class_types ~trace:false env
|
|
(clty_params patt_params patt_type) (clty_params subj_params subj_type)
|
|
with
|
|
Failure r -> r
|
|
end
|
|
| error ->
|
|
error
|
|
|
|
|
|
(***************)
|
|
(* Subtyping *)
|
|
(***************)
|
|
|
|
|
|
(**** Build a subtype of a given type. ****)
|
|
|
|
(* build_subtype:
|
|
[visited] traces traversed object and variant types
|
|
[loops] is a mapping from variables to variables, to reproduce
|
|
positive loops in a class type
|
|
[posi] true if the current variance is positive
|
|
[level] number of expansions/enlargement allowed on this branch *)
|
|
|
|
let warn = ref false (* whether double coercion might do better *)
|
|
let pred_expand n = if n mod 2 = 0 && n > 0 then pred n else n
|
|
let pred_enlarge n = if n mod 2 = 1 then pred n else n
|
|
|
|
type change = Unchanged | Equiv | Changed
|
|
let collect l = List.fold_left (fun c1 (_, c2) -> max c1 c2) Unchanged l
|
|
|
|
let rec filter_visited = function
|
|
[] -> []
|
|
| {desc=Tobject _|Tvariant _} :: _ as l -> l
|
|
| _ :: l -> filter_visited l
|
|
|
|
let memq_warn t visited =
|
|
if List.memq t visited then (warn := true; true) else false
|
|
|
|
let rec lid_of_path sharp = function
|
|
Path.Pident id ->
|
|
Longident.Lident (sharp ^ Ident.name id)
|
|
| Path.Pdot (p1, s, _) ->
|
|
Longident.Ldot (lid_of_path "" p1, sharp ^ s)
|
|
| Path.Papply (p1, p2) ->
|
|
Longident.Lapply (lid_of_path sharp p1, lid_of_path "" p2)
|
|
|
|
let find_cltype_for_path env p =
|
|
let path, cl_abbr = Env.lookup_type (lid_of_path "#" p) env in
|
|
match cl_abbr.type_manifest with
|
|
Some ty ->
|
|
begin match (repr ty).desc with
|
|
Tobject(_,{contents=Some(p',_)}) when Path.same p p' -> cl_abbr, ty
|
|
| _ -> raise Not_found
|
|
end
|
|
| None -> assert false
|
|
|
|
let has_constr_row' env t =
|
|
has_constr_row (expand_abbrev env t)
|
|
|
|
let rec build_subtype env visited loops posi level t =
|
|
let t = repr t in
|
|
match t.desc with
|
|
Tvar ->
|
|
if posi then
|
|
try
|
|
let t' = List.assq t loops in
|
|
warn := true;
|
|
(t', Equiv)
|
|
with Not_found ->
|
|
(t, Unchanged)
|
|
else
|
|
(t, Unchanged)
|
|
| Tarrow(l, t1, t2, _) ->
|
|
if memq_warn t visited then (t, Unchanged) else
|
|
let visited = t :: visited in
|
|
let (t1', c1) = build_subtype env visited loops (not posi) level t1 in
|
|
let (t2', c2) = build_subtype env visited loops posi level t2 in
|
|
let c = max c1 c2 in
|
|
if c > Unchanged then (newty (Tarrow(l, t1', t2', Cok)), c)
|
|
else (t, Unchanged)
|
|
| Ttuple tlist ->
|
|
if memq_warn t visited then (t, Unchanged) else
|
|
let visited = t :: visited in
|
|
let tlist' =
|
|
List.map (build_subtype env visited loops posi level) tlist
|
|
in
|
|
let c = collect tlist' in
|
|
if c > Unchanged then (newty (Ttuple (List.map fst tlist')), c)
|
|
else (t, Unchanged)
|
|
| Tconstr(p, tl, abbrev)
|
|
when level > 0 && generic_abbrev env p && safe_abbrev env t
|
|
&& not (has_constr_row' env t) ->
|
|
let t' = repr (expand_abbrev env t) in
|
|
let level' = pred_expand level in
|
|
begin try match t'.desc with
|
|
Tobject _ when posi && not (opened_object t') ->
|
|
let cl_abbr, body = find_cltype_for_path env p in
|
|
let ty =
|
|
subst env !current_level Public abbrev None
|
|
cl_abbr.type_params tl body in
|
|
let ty = repr ty in
|
|
let ty1, tl1 =
|
|
match ty.desc with
|
|
Tobject(ty1,{contents=Some(p',tl1)}) when Path.same p p' ->
|
|
ty1, tl1
|
|
| _ -> raise Not_found
|
|
in
|
|
(* Fix PR4505: do not set ty to Tvar when it appears in tl1,
|
|
as this occurence might break the occur check.
|
|
XXX not clear whether this correct anyway... *)
|
|
if List.exists (deep_occur ty) tl1 then raise Not_found;
|
|
ty.desc <- Tvar;
|
|
let t'' = newvar () in
|
|
let loops = (ty, t'') :: loops in
|
|
(* May discard [visited] as level is going down *)
|
|
let (ty1', c) =
|
|
build_subtype env [t'] loops posi (pred_enlarge level') ty1 in
|
|
assert (t''.desc = Tvar);
|
|
let nm =
|
|
if c > Equiv || deep_occur ty ty1' then None else Some(p,tl1) in
|
|
t''.desc <- Tobject (ty1', ref nm);
|
|
(try unify_var env ty t with Unify _ -> assert false);
|
|
(t'', Changed)
|
|
| _ -> raise Not_found
|
|
with Not_found ->
|
|
let (t'',c) = build_subtype env visited loops posi level' t' in
|
|
if c > Unchanged then (t'',c)
|
|
else (t, Unchanged)
|
|
end
|
|
| Tconstr(p, tl, abbrev) ->
|
|
(* Must check recursion on constructors, since we do not always
|
|
expand them *)
|
|
if memq_warn t visited then (t, Unchanged) else
|
|
let visited = t :: visited in
|
|
begin try
|
|
let decl = Env.find_type p env in
|
|
if level = 0 && generic_abbrev env p && safe_abbrev env t
|
|
&& not (has_constr_row' env t)
|
|
then warn := true;
|
|
let tl' =
|
|
List.map2
|
|
(fun (co,cn,_) t ->
|
|
if cn then
|
|
if co then (t, Unchanged)
|
|
else build_subtype env visited loops (not posi) level t
|
|
else
|
|
if co then build_subtype env visited loops posi level t
|
|
else (newvar(), Changed))
|
|
decl.type_variance tl
|
|
in
|
|
let c = collect tl' in
|
|
if c > Unchanged then (newconstr p (List.map fst tl'), c)
|
|
else (t, Unchanged)
|
|
with Not_found ->
|
|
(t, Unchanged)
|
|
end
|
|
| Tvariant row ->
|
|
let row = row_repr row in
|
|
if memq_warn t visited || not (static_row row) then (t, Unchanged) else
|
|
let level' = pred_enlarge level in
|
|
let visited =
|
|
t :: if level' < level then [] else filter_visited visited in
|
|
let fields = filter_row_fields false row.row_fields in
|
|
let fields =
|
|
List.map
|
|
(fun (l,f as orig) -> match row_field_repr f with
|
|
Rpresent None ->
|
|
if posi then
|
|
(l, Reither(true, [], false, ref None)), Unchanged
|
|
else
|
|
orig, Unchanged
|
|
| Rpresent(Some t) ->
|
|
let (t', c) = build_subtype env visited loops posi level' t in
|
|
let f =
|
|
if posi && level > 0
|
|
then Reither(false, [t'], false, ref None)
|
|
else Rpresent(Some t')
|
|
in (l, f), c
|
|
| _ -> assert false)
|
|
fields
|
|
in
|
|
let c = collect fields in
|
|
let row =
|
|
{ row_fields = List.map fst fields; row_more = newvar();
|
|
row_bound = (); row_closed = posi; row_fixed = false;
|
|
row_name = if c > Unchanged then None else row.row_name }
|
|
in
|
|
(newty (Tvariant row), Changed)
|
|
| Tobject (t1, _) ->
|
|
if memq_warn t visited || opened_object t1 then (t, Unchanged) else
|
|
let level' = pred_enlarge level in
|
|
let visited =
|
|
t :: if level' < level then [] else filter_visited visited in
|
|
let (t1', c) = build_subtype env visited loops posi level' t1 in
|
|
if c > Unchanged then (newty (Tobject (t1', ref None)), c)
|
|
else (t, Unchanged)
|
|
| Tfield(s, _, t1, t2) (* Always present *) ->
|
|
let (t1', c1) = build_subtype env visited loops posi level t1 in
|
|
let (t2', c2) = build_subtype env visited loops posi level t2 in
|
|
let c = max c1 c2 in
|
|
if c > Unchanged then (newty (Tfield(s, Fpresent, t1', t2')), c)
|
|
else (t, Unchanged)
|
|
| Tnil ->
|
|
if posi then
|
|
let v = newvar () in
|
|
(v, Changed)
|
|
else begin
|
|
warn := true;
|
|
(t, Unchanged)
|
|
end
|
|
| Tsubst _ | Tlink _ ->
|
|
assert false
|
|
| Tpoly(t1, tl) ->
|
|
let (t1', c) = build_subtype env visited loops posi level t1 in
|
|
if c > Unchanged then (newty (Tpoly(t1', tl)), c)
|
|
else (t, Unchanged)
|
|
| Tunivar | Tpackage _ ->
|
|
(t, Unchanged)
|
|
|
|
let enlarge_type env ty =
|
|
warn := false;
|
|
(* [level = 4] allows 2 expansions involving objects/variants *)
|
|
let (ty', _) = build_subtype env [] [] true 4 ty in
|
|
(ty', !warn)
|
|
|
|
(**** Check whether a type is a subtype of another type. ****)
|
|
|
|
(*
|
|
During the traversal, a trace of visited types is maintained. It
|
|
is printed in case of error.
|
|
Constraints (pairs of types that must be equals) are accumulated
|
|
rather than being enforced straight. Indeed, the result would
|
|
otherwise depend on the order in which these constraints are
|
|
enforced.
|
|
A function enforcing these constraints is returned. That way, type
|
|
variables can be bound to their actual values before this function
|
|
is called (see Typecore).
|
|
Only well-defined abbreviations are expanded (hence the tests
|
|
[generic_abbrev ...]).
|
|
*)
|
|
|
|
let subtypes = TypePairs.create 17
|
|
|
|
let subtype_error env trace =
|
|
raise (Subtype (expand_trace env (List.rev trace), []))
|
|
|
|
let private_abbrev env path =
|
|
try
|
|
let decl = Env.find_type path env in
|
|
decl.type_private = Private && decl.type_manifest <> None
|
|
with Not_found -> false
|
|
|
|
let rec subtype_rec env trace t1 t2 cstrs =
|
|
let t1 = repr t1 in
|
|
let t2 = repr t2 in
|
|
if t1 == t2 then cstrs else
|
|
|
|
begin try
|
|
TypePairs.find subtypes (t1, t2);
|
|
cstrs
|
|
with Not_found ->
|
|
TypePairs.add subtypes (t1, t2) ();
|
|
match (t1.desc, t2.desc) with
|
|
(Tvar, _) | (_, Tvar) ->
|
|
(trace, t1, t2, !univar_pairs)::cstrs
|
|
| (Tarrow(l1, t1, u1, _), Tarrow(l2, t2, u2, _)) when l1 = l2
|
|
|| !Clflags.classic && not (is_optional l1 || is_optional l2) ->
|
|
let cstrs = subtype_rec env ((t2, t1)::trace) t2 t1 cstrs in
|
|
subtype_rec env ((u1, u2)::trace) u1 u2 cstrs
|
|
| (Ttuple tl1, Ttuple tl2) ->
|
|
subtype_list env trace tl1 tl2 cstrs
|
|
| (Tconstr(p1, [], _), Tconstr(p2, [], _)) when Path.same p1 p2 ->
|
|
cstrs
|
|
| (Tconstr(p1, tl1, abbrev1), _)
|
|
when generic_abbrev env p1 && safe_abbrev env t1 ->
|
|
subtype_rec env trace (expand_abbrev env t1) t2 cstrs
|
|
| (_, Tconstr(p2, tl2, abbrev2))
|
|
when generic_abbrev env p2 && safe_abbrev env t2 ->
|
|
subtype_rec env trace t1 (expand_abbrev env t2) cstrs
|
|
| (Tconstr(p1, tl1, _), Tconstr(p2, tl2, _)) when Path.same p1 p2 ->
|
|
begin try
|
|
let decl = Env.find_type p1 env in
|
|
List.fold_left2
|
|
(fun cstrs (co, cn, _) (t1, t2) ->
|
|
if co then
|
|
if cn then
|
|
(trace, newty2 t1.level (Ttuple[t1]),
|
|
newty2 t2.level (Ttuple[t2]), !univar_pairs) :: cstrs
|
|
else subtype_rec env ((t1, t2)::trace) t1 t2 cstrs
|
|
else
|
|
if cn then subtype_rec env ((t2, t1)::trace) t2 t1 cstrs
|
|
else cstrs)
|
|
cstrs decl.type_variance (List.combine tl1 tl2)
|
|
with Not_found ->
|
|
(trace, t1, t2, !univar_pairs)::cstrs
|
|
end
|
|
| (Tconstr(p1, tl1, _), _) when private_abbrev env p1 ->
|
|
subtype_rec env trace (expand_abbrev_opt env t1) t2 cstrs
|
|
| (Tobject (f1, _), Tobject (f2, _))
|
|
when (object_row f1).desc = Tvar && (object_row f2).desc = Tvar ->
|
|
(* Same row variable implies same object. *)
|
|
(trace, t1, t2, !univar_pairs)::cstrs
|
|
| (Tobject (f1, _), Tobject (f2, _)) ->
|
|
subtype_fields env trace f1 f2 cstrs
|
|
| (Tvariant row1, Tvariant row2) ->
|
|
begin try
|
|
subtype_row env trace row1 row2 cstrs
|
|
with Exit ->
|
|
(trace, t1, t2, !univar_pairs)::cstrs
|
|
end
|
|
| (Tpoly (u1, []), Tpoly (u2, [])) ->
|
|
subtype_rec env trace u1 u2 cstrs
|
|
| (Tpoly (u1, tl1), Tpoly (u2, [])) ->
|
|
let _, u1' = instance_poly false tl1 u1 in
|
|
subtype_rec env trace u1' u2 cstrs
|
|
| (Tpoly (u1, tl1), Tpoly (u2,tl2)) ->
|
|
begin try
|
|
enter_poly env univar_pairs u1 tl1 u2 tl2
|
|
(fun t1 t2 -> subtype_rec env trace t1 t2 cstrs)
|
|
with Unify _ ->
|
|
(trace, t1, t2, !univar_pairs)::cstrs
|
|
end
|
|
| (_, _) ->
|
|
(trace, t1, t2, !univar_pairs)::cstrs
|
|
end
|
|
|
|
and subtype_list env trace tl1 tl2 cstrs =
|
|
if List.length tl1 <> List.length tl2 then
|
|
subtype_error env trace;
|
|
List.fold_left2
|
|
(fun cstrs t1 t2 -> subtype_rec env ((t1, t2)::trace) t1 t2 cstrs)
|
|
cstrs tl1 tl2
|
|
|
|
and subtype_fields env trace ty1 ty2 cstrs =
|
|
(* Assume that either rest1 or rest2 is not Tvar *)
|
|
let (fields1, rest1) = flatten_fields ty1 in
|
|
let (fields2, rest2) = flatten_fields ty2 in
|
|
let (pairs, miss1, miss2) = associate_fields fields1 fields2 in
|
|
let cstrs =
|
|
if rest2.desc = Tnil then cstrs else
|
|
if miss1 = [] then
|
|
subtype_rec env ((rest1, rest2)::trace) rest1 rest2 cstrs
|
|
else
|
|
(trace, build_fields (repr ty1).level miss1 rest1, rest2,
|
|
!univar_pairs) :: cstrs
|
|
in
|
|
let cstrs =
|
|
if miss2 = [] then cstrs else
|
|
(trace, rest1, build_fields (repr ty2).level miss2 (newvar ()),
|
|
!univar_pairs) :: cstrs
|
|
in
|
|
List.fold_left
|
|
(fun cstrs (_, k1, t1, k2, t2) ->
|
|
(* Theses fields are always present *)
|
|
subtype_rec env ((t1, t2)::trace) t1 t2 cstrs)
|
|
cstrs pairs
|
|
|
|
and subtype_row env trace row1 row2 cstrs =
|
|
let row1 = row_repr row1 and row2 = row_repr row2 in
|
|
let r1, r2, pairs =
|
|
merge_row_fields row1.row_fields row2.row_fields in
|
|
let more1 = repr row1.row_more
|
|
and more2 = repr row2.row_more in
|
|
match more1.desc, more2.desc with
|
|
Tconstr(p1,_,_), Tconstr(p2,_,_) when Path.same p1 p2 ->
|
|
subtype_rec env ((more1,more2)::trace) more1 more2 cstrs
|
|
| (Tvar|Tconstr _), (Tvar|Tconstr _)
|
|
when row1.row_closed && r1 = [] ->
|
|
List.fold_left
|
|
(fun cstrs (_,f1,f2) ->
|
|
match row_field_repr f1, row_field_repr f2 with
|
|
(Rpresent None|Reither(true,_,_,_)), Rpresent None ->
|
|
cstrs
|
|
| Rpresent(Some t1), Rpresent(Some t2) ->
|
|
subtype_rec env ((t1, t2)::trace) t1 t2 cstrs
|
|
| Reither(false, t1::_, _, _), Rpresent(Some t2) ->
|
|
subtype_rec env ((t1, t2)::trace) t1 t2 cstrs
|
|
| Rabsent, _ -> cstrs
|
|
| _ -> raise Exit)
|
|
cstrs pairs
|
|
| Tunivar, Tunivar
|
|
when row1.row_closed = row2.row_closed && r1 = [] && r2 = [] ->
|
|
let cstrs =
|
|
subtype_rec env ((more1,more2)::trace) more1 more2 cstrs in
|
|
List.fold_left
|
|
(fun cstrs (_,f1,f2) ->
|
|
match row_field_repr f1, row_field_repr f2 with
|
|
Rpresent None, Rpresent None
|
|
| Reither(true,[],_,_), Reither(true,[],_,_)
|
|
| Rabsent, Rabsent ->
|
|
cstrs
|
|
| Rpresent(Some t1), Rpresent(Some t2)
|
|
| Reither(false,[t1],_,_), Reither(false,[t2],_,_) ->
|
|
subtype_rec env ((t1, t2)::trace) t1 t2 cstrs
|
|
| _ -> raise Exit)
|
|
cstrs pairs
|
|
| _ ->
|
|
raise Exit
|
|
|
|
let subtype env ty1 ty2 =
|
|
TypePairs.clear subtypes;
|
|
univar_pairs := [];
|
|
(* Build constraint set. *)
|
|
let cstrs = subtype_rec env [(ty1, ty2)] ty1 ty2 [] in
|
|
TypePairs.clear subtypes;
|
|
(* Enforce constraints. *)
|
|
function () ->
|
|
List.iter
|
|
(function (trace0, t1, t2, pairs) ->
|
|
try unify_pairs env t1 t2 pairs with Unify trace ->
|
|
raise (Subtype (expand_trace env (List.rev trace0),
|
|
List.tl (List.tl trace))))
|
|
(List.rev cstrs)
|
|
|
|
(*******************)
|
|
(* Miscellaneous *)
|
|
(*******************)
|
|
|
|
(* Utility for printing. The resulting type is not used in computation. *)
|
|
let rec unalias_object ty =
|
|
let ty = repr ty in
|
|
match ty.desc with
|
|
Tfield (s, k, t1, t2) ->
|
|
newty2 ty.level (Tfield (s, k, t1, unalias_object t2))
|
|
| Tvar | Tnil ->
|
|
newty2 ty.level ty.desc
|
|
| Tunivar ->
|
|
ty
|
|
| Tconstr _ ->
|
|
newty2 ty.level Tvar
|
|
| _ ->
|
|
assert false
|
|
|
|
let unalias ty =
|
|
let ty = repr ty in
|
|
match ty.desc with
|
|
Tvar | Tunivar ->
|
|
ty
|
|
| Tvariant row ->
|
|
let row = row_repr row in
|
|
let more = row.row_more in
|
|
newty2 ty.level
|
|
(Tvariant {row with row_more = newty2 more.level more.desc})
|
|
| Tobject (ty, nm) ->
|
|
newty2 ty.level (Tobject (unalias_object ty, nm))
|
|
| _ ->
|
|
newty2 ty.level ty.desc
|
|
|
|
(* Return the arity (as for curried functions) of the given type. *)
|
|
let rec arity ty =
|
|
match (repr ty).desc with
|
|
Tarrow(_, t1, t2, _) -> 1 + arity t2
|
|
| _ -> 0
|
|
|
|
(* Check whether an abbreviation expands to itself. *)
|
|
let cyclic_abbrev env id ty =
|
|
let rec check_cycle seen ty =
|
|
let ty = repr ty in
|
|
match ty.desc with
|
|
Tconstr (p, tl, abbrev) ->
|
|
p = Path.Pident id || List.memq ty seen ||
|
|
begin try
|
|
check_cycle (ty :: seen) (expand_abbrev_opt env ty)
|
|
with
|
|
Cannot_expand -> false
|
|
| Unify _ -> true
|
|
end
|
|
| _ ->
|
|
false
|
|
in check_cycle [] ty
|
|
|
|
(* Normalize a type before printing, saving... *)
|
|
(* Cannot use mark_type because deep_occur uses it too *)
|
|
let rec normalize_type_rec env visited ty =
|
|
let ty = repr ty in
|
|
if not (TypeSet.mem ty !visited) then begin
|
|
visited := TypeSet.add ty !visited;
|
|
begin match ty.desc with
|
|
| Tvariant row ->
|
|
let row = row_repr row in
|
|
let fields = List.map
|
|
(fun (l,f0) ->
|
|
let f = row_field_repr f0 in l,
|
|
match f with Reither(b, ty::(_::_ as tyl), m, e) ->
|
|
let tyl' =
|
|
List.fold_left
|
|
(fun tyl ty ->
|
|
if List.exists (fun ty' -> equal env false [ty] [ty']) tyl
|
|
then tyl else ty::tyl)
|
|
[ty] tyl
|
|
in
|
|
if f != f0 || List.length tyl' < List.length tyl then
|
|
Reither(b, List.rev tyl', m, e)
|
|
else f
|
|
| _ -> f)
|
|
row.row_fields in
|
|
let fields =
|
|
List.sort (fun (p,_) (q,_) -> compare p q)
|
|
(List.filter (fun (_,fi) -> fi <> Rabsent) fields) in
|
|
log_type ty;
|
|
ty.desc <- Tvariant {row with row_fields = fields}
|
|
| Tobject (fi, nm) ->
|
|
begin match !nm with
|
|
| None -> ()
|
|
| Some (n, v :: l) ->
|
|
if deep_occur ty (newgenty (Ttuple l)) then
|
|
(* The abbreviation may be hiding something, so remove it *)
|
|
set_name nm None
|
|
else let v' = repr v in
|
|
begin match v'.desc with
|
|
| Tvar|Tunivar ->
|
|
if v' != v then set_name nm (Some (n, v' :: l))
|
|
| Tnil ->
|
|
log_type ty; ty.desc <- Tconstr (n, l, ref Mnil)
|
|
| _ -> set_name nm None
|
|
end
|
|
| _ ->
|
|
fatal_error "Ctype.normalize_type_rec"
|
|
end;
|
|
let fi = repr fi in
|
|
if fi.level < lowest_level then () else
|
|
let fields, row = flatten_fields fi in
|
|
let fi' = build_fields fi.level fields row in
|
|
log_type ty; fi.desc <- fi'.desc
|
|
| _ -> ()
|
|
end;
|
|
iter_type_expr (normalize_type_rec env visited) ty
|
|
end
|
|
|
|
let normalize_type env ty =
|
|
normalize_type_rec env (ref TypeSet.empty) ty
|
|
|
|
|
|
(*************************)
|
|
(* Remove dependencies *)
|
|
(*************************)
|
|
|
|
|
|
(*
|
|
Variables are left unchanged. Other type nodes are duplicated, with
|
|
levels set to generic level.
|
|
We cannot use Tsubst here, because unification may be called by
|
|
expand_abbrev.
|
|
*)
|
|
|
|
let nondep_hash = TypeHash.create 47
|
|
let nondep_variants = TypeHash.create 17
|
|
let clear_hash () =
|
|
TypeHash.clear nondep_hash; TypeHash.clear nondep_variants
|
|
|
|
let rec nondep_type_rec env id ty =
|
|
match ty.desc with
|
|
Tvar | Tunivar -> ty
|
|
| Tlink ty -> nondep_type_rec env id ty
|
|
| _ -> try TypeHash.find nondep_hash ty
|
|
with Not_found ->
|
|
let ty' = newgenvar () in (* Stub *)
|
|
TypeHash.add nondep_hash ty ty';
|
|
ty'.desc <-
|
|
begin match ty.desc with
|
|
| Tconstr(p, tl, abbrev) ->
|
|
if Path.isfree id p then
|
|
begin try
|
|
Tlink (nondep_type_rec env id
|
|
(expand_abbrev env (newty2 ty.level ty.desc)))
|
|
(*
|
|
The [Tlink] is important. The expanded type may be a
|
|
variable, or may not be completely copied yet
|
|
(recursive type), so one cannot just take its
|
|
description.
|
|
*)
|
|
with Cannot_expand | Unify _ ->
|
|
raise Not_found
|
|
end
|
|
else
|
|
Tconstr(p, List.map (nondep_type_rec env id) tl, ref Mnil)
|
|
| Tpackage(p, _, _) when Path.isfree id p ->
|
|
raise Not_found
|
|
| Tobject (t1, name) ->
|
|
Tobject (nondep_type_rec env id t1,
|
|
ref (match !name with
|
|
None -> None
|
|
| Some (p, tl) ->
|
|
if Path.isfree id p then None
|
|
else Some (p, List.map (nondep_type_rec env id) tl)))
|
|
| Tvariant row ->
|
|
let row = row_repr row in
|
|
let more = repr row.row_more in
|
|
(* We must keep sharing according to the row variable *)
|
|
begin try
|
|
let ty2 = TypeHash.find nondep_variants more in
|
|
(* This variant type has been already copied *)
|
|
TypeHash.add nondep_hash ty ty2;
|
|
Tlink ty2
|
|
with Not_found ->
|
|
(* Register new type first for recursion *)
|
|
TypeHash.add nondep_variants more ty';
|
|
let static = static_row row in
|
|
let more' = if static then newgenvar () else more in
|
|
(* Return a new copy *)
|
|
let row =
|
|
copy_row (nondep_type_rec env id) true row true more' in
|
|
match row.row_name with
|
|
Some (p, tl) when Path.isfree id p ->
|
|
Tvariant {row with row_name = None}
|
|
| _ -> Tvariant row
|
|
end
|
|
| _ -> copy_type_desc (nondep_type_rec env id) ty.desc
|
|
end;
|
|
ty'
|
|
|
|
let nondep_type env id ty =
|
|
try
|
|
let ty' = nondep_type_rec env id ty in
|
|
clear_hash ();
|
|
ty'
|
|
with Not_found ->
|
|
clear_hash ();
|
|
raise Not_found
|
|
|
|
let unroll_abbrev id tl ty =
|
|
let ty = repr ty and path = Path.Pident id in
|
|
if (ty.desc = Tvar) || (List.exists (deep_occur ty) tl)
|
|
|| is_object_type path then
|
|
ty
|
|
else
|
|
let ty' = newty2 ty.level ty.desc in
|
|
link_type ty (newty2 ty.level (Tconstr (path, tl, ref Mnil)));
|
|
ty'
|
|
|
|
(* Preserve sharing inside type declarations. *)
|
|
let nondep_type_decl env mid id is_covariant decl =
|
|
try
|
|
let params = List.map (nondep_type_rec env mid) decl.type_params in
|
|
let tk =
|
|
try match decl.type_kind with
|
|
Type_abstract ->
|
|
Type_abstract
|
|
| Type_variant cstrs ->
|
|
Type_variant
|
|
(List.map
|
|
(fun (c, tl) -> (c, List.map (nondep_type_rec env mid) tl))
|
|
cstrs)
|
|
| Type_record(lbls, rep) ->
|
|
Type_record
|
|
(List.map
|
|
(fun (c, mut, t) -> (c, mut, nondep_type_rec env mid t))
|
|
lbls,
|
|
rep)
|
|
with Not_found when is_covariant -> Type_abstract
|
|
and tm =
|
|
try match decl.type_manifest with
|
|
None -> None
|
|
| Some ty ->
|
|
Some (unroll_abbrev id params (nondep_type_rec env mid ty))
|
|
with Not_found when is_covariant ->
|
|
None
|
|
in
|
|
clear_hash ();
|
|
let priv =
|
|
match tm with
|
|
| Some ty when Btype.has_constr_row ty -> Private
|
|
| _ -> decl.type_private
|
|
in
|
|
{ type_params = params;
|
|
type_arity = decl.type_arity;
|
|
type_kind = tk;
|
|
type_manifest = tm;
|
|
type_private = priv;
|
|
type_variance = decl.type_variance;
|
|
}
|
|
with Not_found ->
|
|
clear_hash ();
|
|
raise Not_found
|
|
|
|
(* Preserve sharing inside class types. *)
|
|
let nondep_class_signature env id sign =
|
|
{ cty_self = nondep_type_rec env id sign.cty_self;
|
|
cty_vars =
|
|
Vars.map (function (m, v, t) -> (m, v, nondep_type_rec env id t))
|
|
sign.cty_vars;
|
|
cty_concr = sign.cty_concr;
|
|
cty_inher =
|
|
List.map (fun (p,tl) -> (p, List.map (nondep_type_rec env id) tl))
|
|
sign.cty_inher }
|
|
|
|
let rec nondep_class_type env id =
|
|
function
|
|
Tcty_constr (p, _, cty) when Path.isfree id p ->
|
|
nondep_class_type env id cty
|
|
| Tcty_constr (p, tyl, cty) ->
|
|
Tcty_constr (p, List.map (nondep_type_rec env id) tyl,
|
|
nondep_class_type env id cty)
|
|
| Tcty_signature sign ->
|
|
Tcty_signature (nondep_class_signature env id sign)
|
|
| Tcty_fun (l, ty, cty) ->
|
|
Tcty_fun (l, nondep_type_rec env id ty, nondep_class_type env id cty)
|
|
|
|
let nondep_class_declaration env id decl =
|
|
assert (not (Path.isfree id decl.cty_path));
|
|
let decl =
|
|
{ cty_params = List.map (nondep_type_rec env id) decl.cty_params;
|
|
cty_variance = decl.cty_variance;
|
|
cty_type = nondep_class_type env id decl.cty_type;
|
|
cty_path = decl.cty_path;
|
|
cty_new =
|
|
begin match decl.cty_new with
|
|
None -> None
|
|
| Some ty -> Some (nondep_type_rec env id ty)
|
|
end }
|
|
in
|
|
clear_hash ();
|
|
decl
|
|
|
|
let nondep_cltype_declaration env id decl =
|
|
assert (not (Path.isfree id decl.clty_path));
|
|
let decl =
|
|
{ clty_params = List.map (nondep_type_rec env id) decl.clty_params;
|
|
clty_variance = decl.clty_variance;
|
|
clty_type = nondep_class_type env id decl.clty_type;
|
|
clty_path = decl.clty_path }
|
|
in
|
|
clear_hash ();
|
|
decl
|
|
|
|
(* collapse conjonctive types in class parameters *)
|
|
let rec collapse_conj env visited ty =
|
|
let ty = repr ty in
|
|
if List.memq ty visited then () else
|
|
let visited = ty :: visited in
|
|
match ty.desc with
|
|
Tvariant row ->
|
|
let row = row_repr row in
|
|
List.iter
|
|
(fun (l,fi) ->
|
|
match row_field_repr fi with
|
|
Reither (c, t1::(_::_ as tl), m, e) ->
|
|
List.iter (unify env t1) tl;
|
|
set_row_field e (Reither (c, [t1], m, ref None))
|
|
| _ ->
|
|
())
|
|
row.row_fields;
|
|
iter_row (collapse_conj env visited) row
|
|
| _ ->
|
|
iter_type_expr (collapse_conj env visited) ty
|
|
|
|
let collapse_conj_params env params =
|
|
List.iter (collapse_conj env []) params
|