1 (***********************************************************************)
5 (* Xavier Leroy and Jerome Vouillon, projet Cristal, INRIA Rocquencourt*)
7 (* Copyright 1996 Institut National de Recherche en Informatique et *)
8 (* en Automatique. All rights reserved. This file is distributed *)
9 (* under the terms of the Q Public License version 1.0. *)
11 (***********************************************************************)
15 (* Operations on core types *)
23 Type manipulation after type inference
24 ======================================
25 If one wants to manipulate a type after type inference (for
26 instance, during code generation or in the debugger), one must
27 first make sure that the type levels are correct, using the
28 function [correct_levels]. Then, this type can be correctely
29 manipulated by [apply], [expand_head] and [moregeneral].
35 - As much sharing as possible should be kept : it makes types
36 smaller and better abbreviated.
37 When necessary, some sharing can be lost. Types will still be
38 printed correctly (+++ TO DO...), and abbreviations defined by a
39 class do not depend on sharing thanks to constrained
40 abbreviations. (Of course, even if some sharing is lost, typing
41 will still be correct.)
42 - All nodes of a type have a level : that way, one know whether a
43 node need to be duplicated or not when instantiating a type.
44 - Levels of a type are decreasing (generic level being considered
46 - The level of a type constructor is superior to the binding
48 - Recursive types without limitation should be handled (even if
49 there is still an occur check). This avoid treating specially the
50 case for objects, for instance. Furthermore, the occur check
51 policy can then be easily changed.
57 - Revoir affichage des types.
58 - Etendre la portee d'un alias [... as 'a] a tout le type englobant.
59 - #-type implementes comme de vraies abreviations.
60 - Niveaux plus fins pour les identificateurs :
61 Champ [global] renomme en [level];
64 1 : module contenu dans module toplevel
66 En fait, incrementer le niveau a chaque fois que l'on rentre dans
75 [Subst] doit ecreter les niveaux (pour qu'un variable non
76 generalisable dans un module de niveau 2 ne se retrouve pas
77 generalisable lorsque l'on l'utilise au niveau 0).
79 - Traitement de la trace de l'unification separe de la fonction
85 exception Unify
of (type_expr
* type_expr
) list
87 exception Tags
of label
* label
90 (type_expr
* type_expr
) list
* (type_expr
* type_expr
) list
92 exception Cannot_expand
94 exception Cannot_apply
96 exception Recursive_abbrev
98 (**** Type level management ****)
100 let current_level = ref 0
101 let nongen_level = ref 0
102 let global_level = ref 1
103 let saved_level = ref []
104 let saved_global_level = ref []
106 let init_def level
= current_level := level
; nongen_level := level
108 saved_level := (!current_level, !nongen_level) :: !saved_level;
109 incr
current_level; nongen_level := !current_level
110 let begin_class_def () =
111 saved_level := (!current_level, !nongen_level) :: !saved_level;
113 let raise_nongen_level () =
114 saved_level := (!current_level, !nongen_level) :: !saved_level;
115 nongen_level := !current_level
117 let (cl
, nl
) = List.hd
!saved_level in
118 saved_level := List.tl
!saved_level;
119 current_level := cl
; nongen_level := nl
121 let reset_global_level () =
122 global_level := !current_level + 1;
123 saved_global_level := []
124 let increase_global_level () =
125 let gl = !global_level in
126 global_level := !current_level;
128 let restore_global_level gl =
131 (* Abbreviations without parameters *)
132 (* Shall reset after generalizing *)
133 let simple_abbrevs = ref Mnil
134 let proper_abbrevs path tl abbrev
=
135 if !Clflags.principal
|| tl
<> [] then abbrev
else
136 let name = match path
with Path.Pident id
-> Ident.name id
137 | Path.Pdot
(_
, s
,_
) -> s
138 | Path.Papply _
-> assert false in
139 if name.[0] <> '#'
then simple_abbrevs else abbrev
141 (**** Some type creators ****)
143 (* Re-export generic type creators *)
145 let newty2 = Btype.newty2
146 let newty desc
= newty2 !current_level desc
147 let new_global_ty desc
= newty2 !global_level desc
149 let newvar () = newty2 !current_level Tvar
150 let newvar2 level
= newty2 level Tvar
151 let new_global_var () = newty2 !global_level Tvar
153 let newobj fields
= newty (Tobject
(fields
, ref None
))
155 let newconstr path tyl
= newty (Tconstr
(path
, tyl
, ref Mnil
))
157 let none = newty (Ttuple
[]) (* Clearly ill-formed type *)
159 (**** Representative of a type ****)
164 (**** Type maps ****)
168 type t
= type_expr
* type_expr
169 let equal (t1
, t1'
) (t2
, t2'
) = (t1
== t2
) && (t1'
== t2'
)
170 let hash (t
, t'
) = t
.id
+ 93 * t'
.id
173 (**********************************************)
174 (* Miscellaneous operations on object types *)
175 (**********************************************)
178 (**** Object field manipulation. ****)
180 let dummy_method = "*dummy method*"
182 let object_fields ty
=
183 match (repr ty
).desc
with
184 Tobject
(fields
, _
) -> fields
187 let flatten_fields ty
=
188 let rec flatten l ty
=
191 Tfield
(s
, k
, ty1
, ty2
) ->
192 flatten ((s
, k
, ty1
)::l
) ty2
196 let (l
, r
) = flatten [] ty in
197 (Sort.list
(fun (n
, _
, _
) (n'
, _
, _
) -> n
< n'
) l
, r
)
199 let build_fields level
=
201 (fun (s
, k
, ty1
) ty2
-> newty2 level
(Tfield
(s
, k
, ty1
, ty2
)))
203 let associate_fields fields1 fields2
=
204 let rec associate p s s'
=
207 (List.rev p
, (List.rev s
) @ l
, List.rev s'
)
209 (List.rev p
, List.rev s
, (List.rev s'
) @ l'
)
210 | ((n
, k
, t
)::r
, (n'
, k'
, t'
)::r'
) when n
= n'
->
211 associate ((n
, k
, t
, k'
, t'
)::p
) s s'
(r
, r'
)
212 | ((n
, k
, t
)::r
, ((n'
, k'
, t'
)::_
as l'
)) when n
< n'
->
213 associate p
((n
, k
, t
)::s
) s'
(r
, l'
)
214 | (((n
, k
, t
)::r
as l
), (n'
, k'
, t'
)::r'
) (* when n > n' *) ->
215 associate p s
((n'
, k'
, t'
)::s'
) (l
, r'
)
217 associate [] [] [] (fields1
, fields2
)
219 (**** Check whether an object is open ****)
221 (* +++ Il faudra penser a eventuellement expanser l'abreviation *)
222 let rec object_row ty =
225 Tobject
(t
, _
) -> object_row t
226 | Tfield
(_
, _
, _
, t
) -> object_row t
229 let opened_object ty =
230 match (object_row ty).desc
with
236 (**** Close an object ****)
238 let close_object ty =
243 link_type
ty (newty2 ty.level Tnil
)
244 | Tfield
(_
, _
, _
, ty'
) -> close ty'
247 match (repr ty).desc
with
248 Tobject
(ty, _
) -> close ty
251 (**** Row variable of an object type ****)
253 let row_variable ty =
257 Tfield
(_
, _
, _
, ty) -> find ty
261 match (repr ty).desc
with
262 Tobject
(fi
, _
) -> find fi
265 (**** Object name manipulation ****)
266 (* +++ Bientot obsolete *)
268 let set_object_name id rv params
ty =
269 match (repr ty).desc
with
271 set_name nm
(Some
(Path.Pident id
, rv
::params
))
275 let remove_object_name ty =
276 match (repr ty).desc
with
277 Tobject
(_
, nm
) -> set_name nm None
278 | Tconstr
(_
, _
, _
) -> ()
279 | _
-> fatal_error
"Ctype.remove_object_name"
281 (**** Hiding of private methods ****)
283 let hide_private_methods ty =
284 match (repr ty).desc
with
287 let (fl
, _
) = flatten_fields fi
in
289 (function (_
, k
, _
) ->
290 match field_kind_repr k
with
291 Fvar r
-> set_kind r Fabsent
298 (*******************************)
299 (* Operations on class types *)
300 (*******************************)
303 let rec signature_of_class_type =
305 Tcty_constr
(_
, _
, cty
) -> signature_of_class_type cty
306 | Tcty_signature sign
-> sign
307 | Tcty_fun
(_
, ty, cty
) -> signature_of_class_type cty
310 repr (signature_of_class_type cty
).cty_self
312 let rec class_type_arity =
314 Tcty_constr
(_
, _
, cty
) -> class_type_arity cty
315 | Tcty_signature _
-> 0
316 | Tcty_fun
(_
, _
, cty
) -> 1 + class_type_arity cty
319 (*******************************************)
320 (* Miscellaneous operations on row types *)
321 (*******************************************)
323 let sort_row_fields = Sort.list
(fun (p
,_
) (q
,_
) -> p
< q
)
325 let rec merge_rf r1 r2 pairs fi1 fi2
=
327 (l1
,f1
as p1
)::fi1'
, (l2
,f2
as p2
)::fi2'
->
328 if l1
= l2
then merge_rf r1 r2
((l1
,f1
,f2
)::pairs
) fi1' fi2'
else
329 if l1
< l2
then merge_rf (p1
::r1
) r2 pairs fi1' fi2
else
330 merge_rf r1
(p2
::r2
) pairs fi1 fi2'
331 | [], _
-> (List.rev r1
, List.rev_append r2 fi2
, pairs
)
332 | _
, [] -> (List.rev_append r1 fi1
, List.rev r2
, pairs
)
334 let merge_row_fields fi1 fi2
=
336 [], _
| _
, [] -> (fi1
, fi2
, [])
337 | [p1
], _
when not
(List.mem_assoc
(fst p1
) fi2
) -> (fi1
, fi2
, [])
338 | _
, [p2
] when not
(List.mem_assoc
(fst p2
) fi1
) -> (fi1
, fi2
, [])
339 | _
-> merge_rf [] [] [] (sort_row_fields fi1
) (sort_row_fields fi2
)
341 let rec filter_row_fields erase
= function
344 let fi = filter_row_fields erase
fi in
345 match row_field_repr f
with
347 | Reither
(_
,_
,false,e
) when erase
-> set_row_field e Rabsent
; fi
350 (**************************************)
351 (* Check genericity of type schemes *)
352 (**************************************)
357 let rec closed_schema_rec ty =
359 if ty.level
>= lowest_level
then begin
360 let level = ty.level in
361 ty.level <- pivot_level
- level;
363 Tvar
when level <> generic_level
->
365 | Tfield
(_
, kind
, t1
, t2
) ->
366 if field_kind_repr kind
= Fpresent
then
367 closed_schema_rec t1
;
370 let row = row_repr
row in
371 iter_row
closed_schema_rec row;
372 if not
(static_row
row) then closed_schema_rec row.row_more
374 iter_type_expr
closed_schema_rec ty
377 (* Return whether all variables of type [ty] are generic. *)
378 let closed_schema ty =
380 closed_schema_rec ty;
387 exception Non_closed
of type_expr
* bool
389 let free_variables = ref []
391 let rec free_vars_rec real ty =
393 if ty.level >= lowest_level
then begin
394 ty.level <- pivot_level
- ty.level;
395 begin match ty.desc
with
397 free_variables := (ty, real) :: !free_variables
398 (* Do not count "virtual" free variables
399 | Tobject(ty, {contents = Some (_, p)}) ->
400 free_vars_rec false ty; List.iter (free_vars_rec true) p
403 free_vars_rec false ty
404 | Tfield
(_
, _
, ty1
, ty2
) ->
405 free_vars_rec true ty1
; free_vars_rec false ty2
407 let row = row_repr
row in
408 iter_row
(free_vars_rec true) row;
409 if not
(static_row
row) then free_vars_rec false row.row_more
411 iter_type_expr
(free_vars_rec true) ty
416 free_variables := [];
417 free_vars_rec true ty;
418 let res = !free_variables in
419 free_variables := [];
422 let free_variables ty =
423 let tl = List.map fst
(free_vars ty) in
427 let rec closed_type ty =
428 match free_vars ty with
430 | (v
, real) :: _
-> raise
(Non_closed
(v
, real))
432 let closed_parameterized_type params
ty =
433 List.iter mark_type params
;
435 try closed_type ty; true with Non_closed _
-> false in
436 List.iter unmark_type params
;
440 let closed_type_decl decl
=
442 List.iter mark_type decl
.type_params
;
443 begin match decl
.type_kind
with
446 | Type_variant
(v
, priv
) ->
447 List.iter
(fun (_
, tyl
) -> List.iter
closed_type tyl
) v
448 | Type_record
(r
, rep
, priv
) ->
449 List.iter
(fun (_
, _
, ty) -> closed_type ty) r
451 begin match decl
.type_manifest
with
453 | Some
ty -> closed_type ty
455 unmark_type_decl decl
;
457 with Non_closed
(ty, _
) ->
458 unmark_type_decl decl
;
461 type closed_class_failure
=
462 CC_Method
of type_expr
* bool * string * type_expr
463 | CC_Value
of type_expr
* bool * string * type_expr
465 exception Failure
of closed_class_failure
467 let closed_class params sign
=
468 let ty = object_fields (repr sign
.cty_self
) in
469 let (fields
, rest
) = flatten_fields ty in
470 List.iter mark_type params
;
473 (fun (lab
, _
, ty) -> if lab
= dummy_method then mark_type
ty)
476 mark_type_node
(repr sign
.cty_self
);
478 (fun (lab
, kind
, ty) ->
479 if field_kind_repr kind
= Fpresent
then
480 try closed_type ty with Non_closed
(ty0
, real) ->
481 raise
(Failure
(CC_Method
(ty0
, real, lab
, ty))))
483 mark_type_params
(repr sign
.cty_self
);
484 List.iter unmark_type params
;
485 unmark_class_signature sign
;
487 with Failure reason
->
488 mark_type_params
(repr sign
.cty_self
);
489 List.iter unmark_type params
;
490 unmark_class_signature sign
;
494 (**********************)
495 (* Type duplication *)
496 (**********************)
499 (* Duplicate a type, preserving only type variables *)
500 let duplicate_type ty =
501 Subst.type_expr
Subst.identity
ty
503 (* Same, for class types *)
504 let duplicate_class_type ty =
505 Subst.class_type
Subst.identity
ty
508 (*****************************)
509 (* Type level manipulation *)
510 (*****************************)
513 It would be a bit more efficient to remove abbreviation expansions
514 rather than generalizing them: these expansions will usually not be
515 used anymore. However, this is not possible in the general case, as
516 [expand_abbrev] (via [subst]) requires these expansions to be
517 preserved. Does it worth duplicating this code ?
519 let rec iter_generalize tyl
ty =
521 if (ty.level > !current_level) && (ty.level <> generic_level
) then begin
522 set_level
ty generic_level
;
523 begin match ty.desc
with
524 Tconstr
(_
, _
, abbrev
) ->
525 iter_abbrev
(iter_generalize tyl
) !abbrev
528 iter_type_expr
(iter_generalize tyl
) ty
532 let iter_generalize tyl
ty =
533 simple_abbrevs := Mnil
;
534 iter_generalize tyl
ty
537 iter_generalize (ref []) ty
539 (* Efficient repeated generalisation of the same type *)
540 let iterative_generalization min_level tyl
=
542 List.iter
(iter_generalize tyl'
) tyl;
543 List.fold_right
(fun ty l
-> if ty.level <= min_level
then l
else ty::l
)
546 (* Generalize the structure and lower the variables *)
548 let rec generalize_structure var_level
ty =
550 if ty.level <> generic_level
then begin
551 if ty.desc
= Tvar
&& ty.level > var_level
then
552 set_level
ty var_level
553 else if ty.level > !current_level then begin
554 set_level
ty generic_level
;
555 begin match ty.desc
with
556 Tconstr
(_
, _
, abbrev
) -> abbrev
:= Mnil
559 iter_type_expr
(generalize_structure var_level
) ty
563 let generalize_structure var_level
ty =
564 simple_abbrevs := Mnil
;
565 generalize_structure var_level
ty
567 (* let generalize_expansive ty = generalize_structure !nongen_level ty *)
568 let generalize_global ty = generalize_structure !global_level ty
569 let generalize_structure ty = generalize_structure !current_level ty
571 (* Generalize the spine of a function, if the level >= !current_level *)
573 let rec generalize_spine ty =
575 if ty.level < !current_level || ty.level = generic_level
then () else
577 Tarrow
(_
, _
, ty'
, _
) | Tpoly
(ty'
, _
) ->
578 set_level
ty generic_level
;
582 let try_expand_once'
= (* Forward declaration *)
583 ref (fun env
ty -> raise Cannot_expand
)
586 Lower the levels of a type (assume [level] is not
590 The level of a type constructor must be greater than its binding
591 time. That way, a type constructor cannot escape the scope of its
592 definition, as would be the case in
594 module M = struct type t let _ = (x : t list ref) end
595 (without this constraint, the type system would actually be unsound.)
597 let rec update_level env
level ty =
599 if ty.level > level then begin
600 begin match ty.desc
with
601 Tconstr
(p
, tl, abbrev
) when level < Path.binding_time p
->
602 (* Try first to replace an abbreviation by its expansion. *)
604 link_type
ty (!try_expand_once' env
ty);
605 update_level env
level ty
606 with Cannot_expand
->
607 (* +++ Levels should be restored... *)
608 raise
(Unify
[(ty, newvar2 level)])
610 | Tobject
(_, ({contents
=Some
(p
, tl)} as nm
))
611 when level < Path.binding_time p
->
613 update_level env
level ty
615 let row = row_repr
row in
616 begin match row.row_name
with
617 | Some
(p
, tl) when level < Path.binding_time p
->
619 ty.desc
<- Tvariant
{row with row_name
= None
}
623 iter_type_expr
(update_level env
level) ty
624 | Tfield
(lab
, _, _, _) when lab
= dummy_method ->
625 raise
(Unify
[(ty, newvar2 level)])
628 (* XXX what about abbreviations in Tconstr ? *)
629 iter_type_expr
(update_level env
level) ty
633 (* Generalize and lower levels of contravariant branches simultaneously *)
635 let rec generalize_expansive env var_level
ty =
637 if ty.level <> generic_level
then begin
638 if ty.level > var_level
then begin
639 set_level
ty generic_level
;
641 Tconstr
(path
, tyl, abbrev
) ->
643 try (Env.find_type path env
).type_variance
644 with Not_found
-> List.map
(fun _ -> (true,true,true)) tyl in
648 if ct
then update_level env var_level t
649 else generalize_expansive env var_level t
)
651 | Tarrow
(_, t1
, t2
, _) ->
652 update_level env var_level t1
;
653 generalize_expansive env var_level t2
655 iter_type_expr
(generalize_expansive env var_level
) ty
659 let generalize_expansive env
ty =
660 simple_abbrevs := Mnil
;
662 generalize_expansive env
!nongen_level ty
663 with Unify
[_, ty'
] ->
664 raise
(Unify
[ty, ty'
])
666 (* Correct the levels of type [ty]. *)
667 let correct_levels ty =
670 (* Only generalize the type ty0 in ty *)
671 let limited_generalize ty0
ty =
672 let ty0 = repr ty0 in
674 let graph = Hashtbl.create
17 in
675 let idx = ref lowest_level
in
676 let roots = ref [] in
678 let rec inverse pty
ty =
680 if (ty.level > !current_level) || (ty.level = generic_level
) then begin
682 Hashtbl.add
graph !idx (ty, ref pty
);
683 if (ty.level = generic_level
) || (ty == ty0) then
684 roots := ty :: !roots;
686 iter_type_expr
(inverse [ty]) ty
687 end else if ty.level < lowest_level
then begin
688 let (_, parents
) = Hashtbl.find graph ty.level in
689 parents
:= pty
@ !parents
692 and generalize_parents
ty =
693 let idx = ty.level in
694 if idx <> generic_level
then begin
695 set_level
ty generic_level
;
696 List.iter generalize_parents
!(snd
(Hashtbl.find graph idx));
697 (* Special case for rows: must generalize the row variable *)
700 let more = row_more
row in
701 let lv = more.level in
702 if (lv < lowest_level
|| lv > !current_level)
703 && lv <> generic_level
then set_level
more generic_level
709 if ty0.level < lowest_level
then
710 iter_type_expr
(inverse []) ty0;
711 List.iter generalize_parents
!roots;
714 if ty.level <> generic_level
then set_level
ty !current_level)
718 (*******************)
720 (*******************)
723 let rec find_repr p1
=
727 | Mcons
(p2
, ty, _, _) when Path.same p1 p2
->
729 | Mcons
(_, _, _, rem
) ->
731 | Mlink
{contents
= rem
} ->
735 Generic nodes are duplicated, while non-generic nodes are left
737 During instantiation, the description of a generic node is first
738 replaced by a link to a stub ([Tsubst (newvar ())]). Once the
739 copy is made, it replaces the stub.
740 After instantiation, the description of generic node, which was
741 stored by [save_desc], must be put back, using [cleanup_types].
744 let abbreviations = ref (ref Mnil
)
745 (* Abbreviation memorized. *)
752 if ty.level <> generic_level
then ty else
753 let desc = ty.desc in
755 let t = newvar() in (* Stub *)
758 begin match desc with
759 | Tconstr
(p
, tl, _) ->
760 let abbrevs = proper_abbrevs p
tl !abbreviations in
761 begin match find_repr p
!abbrevs with
762 Some
ty when repr ty != t -> (* XXX Commentaire... *)
766 One must allocate a new reference, so that abbrevia-
767 tions belonging to different branches of a type are
769 Moreover, a reference containing a [Mcons] must be
770 shared, so that the memorized expansion of an abbrevi-
771 ation can be released by changing the content of just
774 Tconstr
(p
, List.map
copy tl,
775 ref (match !(!abbreviations) with
776 Mcons
_ -> Mlink
!abbreviations
780 let row = row_repr row0
in
781 let more = repr row.row_more
in
782 (* We must substitute in a subtle way *)
783 (* Tsubst takes a tuple containing the row var and the variant *)
784 begin match more.desc with
785 Tsubst
{desc = Ttuple
[_;ty2
]} ->
786 (* This variant type has been already copied *)
787 ty.desc <- Tsubst ty2
; (* avoid Tlink in the new type *)
790 (* If the row variable is not generic, we must keep it *)
791 let keep = more.level <> generic_level
in
796 if keep then save_desc
more more.desc;
799 save_desc
more more.desc;
800 if keep then more else newty more.desc
803 (* Register new type first for recursion *)
804 more.desc <- Tsubst
(newgenty
(Ttuple
[more'
;t]));
805 (* Return a new copy *)
806 Tvariant
(copy_row
copy true row keep more'
)
808 | Tfield
(p
, k
, ty1
, ty2
) ->
809 begin match field_kind_repr k
with
810 Fabsent
-> Tlink
(copy ty2
)
811 | Fpresent
-> copy_type_desc
copy desc
814 copy_type_desc
copy desc
816 | _ -> copy_type_desc
copy desc
820 (**** Variants of instantiations ****)
827 let instance_list schl
=
828 let tyl = List.map
copy schl
in
832 let instance_constructor cstr
=
833 let ty_res = copy cstr
.cstr_res
in
834 let ty_args = List.map
copy cstr
.cstr_args
in
838 let instance_parameterized_type sch_args sch
=
839 let ty_args = List.map
copy sch_args
in
844 let instance_parameterized_type_2 sch_args sch_lst sch
=
845 let ty_args = List.map
copy sch_args
in
846 let ty_lst = List.map
copy sch_lst
in
849 (ty_args, ty_lst, ty)
851 let instance_class params cty
=
852 let rec copy_class_type =
854 Tcty_constr
(path
, tyl, cty
) ->
855 Tcty_constr
(path
, List.map
copy tyl, copy_class_type cty
)
856 | Tcty_signature sign
->
858 {cty_self
= copy sign
.cty_self
;
860 Vars.map
(function (m
, v
, ty) -> (m
, v
, copy ty)) sign
.cty_vars
;
861 cty_concr
= sign
.cty_concr
;
863 List.map
(fun (p
,tl) -> (p
, List.map
copy tl)) sign
.cty_inher
}
864 | Tcty_fun
(l
, ty, cty
) ->
865 Tcty_fun
(l
, copy ty, copy_class_type cty
)
867 let params'
= List.map
copy params in
868 let cty'
= copy_class_type cty in
872 (**** Instanciation for types with free universal variables ****)
874 module TypeHash
= Hashtbl.Make
(TypeOps
)
875 module TypeSet
= Set.Make
(TypeOps
)
878 { inv_type
: type_expr
;
879 mutable inv_parents
: inv_type_expr list
}
881 let rec inv_type hash pty
ty =
884 let inv = TypeHash.find hash ty in
885 inv.inv_parents
<- pty
@ inv.inv_parents
887 let inv = { inv_type = ty; inv_parents
= pty
} in
888 TypeHash.add
hash ty inv;
889 iter_type_expr
(inv_type hash [inv]) ty
891 let compute_univars ty =
892 let inverted = TypeHash.create
17 in
893 inv_type inverted [] ty;
894 let node_univars = TypeHash.create
17 in
895 let rec add_univar univ
inv =
896 match inv.inv_type.desc with
897 Tpoly
(ty, tl) when List.memq univ
(List.map
repr tl) -> ()
900 let univs = TypeHash.find node_univars inv.inv_type in
901 if not
(TypeSet.mem univ
!univs) then begin
902 univs := TypeSet.add univ
!univs;
903 List.iter
(add_univar univ
) inv.inv_parents
906 TypeHash.add
node_univars inv.inv_type (ref(TypeSet.singleton univ
));
907 List.iter
(add_univar univ
) inv.inv_parents
909 TypeHash.iter
(fun ty inv -> if ty.desc = Tunivar
then add_univar ty inv)
912 try !(TypeHash.find node_univars ty) with Not_found
-> TypeSet.empty
914 let rec diff_list l1 l2
=
915 if l1
== l2
then [] else
916 match l1
with [] -> invalid_arg
"Ctype.diff_list"
917 | a
:: l1
-> a
:: diff_list l1 l2
919 let conflicts free bound
=
920 let bound = List.map
repr bound in
921 TypeSet.exists
(fun t -> List.memq
(repr t) bound) free
923 let delayed_copy = ref []
924 (* copying to do later *)
926 (* Copy without sharing until there are no free univars left *)
927 (* all free univars must be included in [visited] *)
928 let rec copy_sep fixed free
bound visited
ty =
930 let univars = free
ty in
931 if TypeSet.is_empty
univars then
932 if ty.level <> generic_level
then ty else
935 lazy (t.desc <- Tlink
(copy ty))
939 let t, bound_t
= List.assq
ty visited
in
940 let dl = if ty.desc = Tunivar
then [] else diff_list bound bound_t
in
941 if dl <> [] && conflicts univars dl then raise Not_found
;
943 with Not_found
-> begin
944 let t = newvar() in (* Stub *)
947 Tarrow
_ | Ttuple
_ | Tvariant
_ | Tconstr
_ | Tobject
_ ->
948 (ty,(t,bound)) :: visited
950 let copy_rec = copy_sep fixed free
bound visited in
952 begin match ty.desc with
954 let row = row_repr row0
in
955 let more = repr row.row_more
in
956 (* We shall really check the level on the row variable *)
957 let keep = more.desc = Tvar
&& more.level <> generic_level
in
958 let more'
= copy_rec more in
959 let fixed'
= fixed && (repr more'
).desc = Tvar
in
960 let row = copy_row
copy_rec fixed'
row keep more'
in
963 let tl = List.map
repr tl in
964 let tl'
= List.map
(fun t -> newty Tunivar
) tl in
965 let bound = tl @ bound in
967 List.map2
(fun ty t -> ty,(t,bound)) tl tl'
@ visited in
968 Tpoly
(copy_sep fixed free
bound visited t1
, tl'
)
969 | _ -> copy_type_desc
copy_rec ty.desc
974 let instance_poly fixed univars sch
=
975 let vars = List.map
(fun _ -> newvar ()) univars in
976 let pairs = List.map2
(fun u v
-> repr u
, (v
, [])) univars vars in
978 let ty = copy_sep fixed (compute_univars sch
) [] pairs sch
in
979 List.iter
Lazy.force
!delayed_copy;
984 let instance_label fixed lbl
=
985 let ty_res = copy lbl
.lbl_res
in
987 match repr lbl
.lbl_arg
with
988 {desc = Tpoly
(ty, tl)} ->
989 instance_poly fixed tl ty
994 (vars, ty_arg
, ty_res)
996 (**** Instantiation with parameter substitution ****)
998 let unify'
= (* Forward declaration *)
999 ref (fun env ty1 ty2
-> raise
(Unify
[]))
1001 let rec subst env
level abbrev
ty params args body
=
1002 if List.length
params <> List.length args
then raise
(Unify
[]);
1003 let old_level = !current_level in
1004 current_level := level;
1006 let body0 = newvar () in (* Stub *)
1009 | Some
({desc = Tconstr
(path
, tl, _)} as ty) ->
1010 let abbrev = proper_abbrevs path
tl abbrev in
1011 memorize_abbrev
abbrev path
ty body0
1015 abbreviations := abbrev;
1016 let (params'
, body'
) = instance_parameterized_type params body
in
1017 abbreviations := ref Mnil
;
1018 !unify' env
body0 body'
;
1019 List.iter2
(!unify' env
) params' args
;
1020 current_level := old_level;
1022 with Unify
_ as exn
->
1023 current_level := old_level;
1027 Only the shape of the type matters, not whether is is generic or
1028 not. [generic_level] might be somewhat slower, but it ensures
1029 invariants on types are enforced (decreasing levels.), and we don't
1030 care about efficiency here.
1032 let apply env
params body args
=
1034 subst env generic_level
(ref Mnil
) None
params args body
1036 Unify
_ -> raise Cannot_apply
1039 (****************************)
1040 (* Abbreviation expansion *)
1041 (****************************)
1044 If the environnement has changed, memorized expansions might not
1045 be correct anymore, and so we flush the cache. This is safe but
1046 quite pessimistic: it would be enough to flush the cache when a
1047 type or module definition is overriden in the environnement.
1049 let previous_env = ref Env.empty
1050 let check_abbrev_env env
=
1051 if env
!= !previous_env then begin
1056 (* Expand an abbreviation. The expansion is memorized. *)
1058 Assume the level is greater than the path binding time of the
1059 expanded abbreviation.
1062 An abbreviation expansion will fail in either of these cases:
1063 1. The type constructor does not correspond to a manifest type.
1064 2. The type constructor is defined in an external file, and this
1065 file is not in the path (missing -I options).
1066 3. The type constructor is not in the "local" environment. This can
1067 happens when a non-generic type variable has been instantiated
1068 afterwards to the not yet defined type constructor. (Actually,
1069 this cannot happen at the moment due to the strong constraints
1070 between type levels and constructor binding time.)
1071 4. The expansion requires the expansion of another abbreviation,
1072 and this other expansion fails.
1074 let expand_abbrev env
ty =
1075 check_abbrev_env env
;
1077 {desc = Tconstr
(path
, args
, abbrev); level = level} ->
1078 let lookup_abbrev = proper_abbrevs path args
abbrev in
1079 begin match find_expans path
!lookup_abbrev with
1081 if level <> generic_level
then
1083 update_level env
level ty
1085 (* XXX This should not happen.
1086 However, levels are not correctly restored after a
1092 let (params, body
) =
1093 try Env.find_type_expansion path env
with Not_found
->
1096 let ty'
= subst env
level abbrev (Some
ty) params args body
in
1097 (* Hack to name the variant type *)
1098 begin match repr ty'
with
1099 {desc=Tvariant
row} as ty when static_row
row ->
1100 ty.desc <- Tvariant
{ row with row_name
= Some
(path
, args
) }
1108 let safe_abbrev env
ty =
1109 let snap = Btype.snapshot
() in
1110 try ignore
(expand_abbrev env
ty); true
1111 with Cannot_expand
| Unify
_ ->
1112 Btype.backtrack
snap;
1115 let try_expand_once env
ty =
1118 Tconstr
_ -> repr (expand_abbrev env
ty)
1119 | _ -> raise Cannot_expand
1121 let _ = try_expand_once'
:= try_expand_once
1123 (* Fully expand the head of a type.
1124 Raise Cannot_expand if the type cannot be expanded.
1125 May raise Unify, if a recursion was hidden in the type. *)
1126 let rec try_expand_head env
ty =
1127 let ty'
= try_expand_once env
ty in
1129 try_expand_head env
ty'
1130 with Cannot_expand
->
1134 (* Expand once the head of a type *)
1135 let expand_head_once env
ty =
1136 try expand_abbrev env
(repr ty) with Cannot_expand
-> assert false
1138 (* Fully expand the head of a type. *)
1139 let expand_head_unif env
ty =
1140 try try_expand_head env
ty with Cannot_expand
-> repr ty
1142 let expand_head env
ty =
1143 let snap = Btype.snapshot
() in
1144 try try_expand_head env
ty
1145 with Cannot_expand
| Unify
_ -> (* expand_head shall never fail *)
1146 Btype.backtrack
snap;
1149 (* Make sure that the type parameters of the type constructor [ty]
1150 respect the type constraints *)
1151 let enforce_constraints env
ty =
1153 {desc = Tconstr
(path
, args
, abbrev); level = level} ->
1154 let decl = Env.find_type path env
in
1156 (subst env
level (ref Mnil
) None
decl.type_params args
(newvar2 level))
1160 (* Recursively expand the head of a type.
1161 Also expand #-types. *)
1162 let rec full_expand env
ty =
1163 let ty = repr (expand_head env
ty) in
1165 Tobject
(fi, {contents
= Some
(_, v
::_)}) when (repr v
).desc = Tvar
->
1166 newty2 ty.level (Tobject
(fi, ref None
))
1171 Check whether the abbreviation expands to a well-defined type.
1172 During the typing of a class, abbreviations for correspondings
1173 types expand to non-generic types.
1175 let generic_abbrev env path
=
1177 let (_, body
) = Env.find_type_expansion path env
in
1178 (repr body
).level = generic_level
1191 (* The marks are already used by [expand_abbrev]... *)
1192 let visited = ref []
1194 let rec non_recursive_abbrev env
ty0 ty =
1196 if ty == repr ty0 then raise Recursive_abbrev
;
1197 if not
(List.memq
ty !visited) then begin
1198 visited := ty :: !visited;
1200 Tconstr
(p
, args
, abbrev) ->
1202 non_recursive_abbrev env
ty0 (try_expand_head env
ty)
1203 with Cannot_expand
->
1204 if !Clflags.recursive_types
then () else
1205 iter_type_expr
(non_recursive_abbrev env
ty0) ty
1207 | Tobject
_ | Tvariant
_ ->
1210 if !Clflags.recursive_types
then () else
1211 iter_type_expr
(non_recursive_abbrev env
ty0) ty
1214 let correct_abbrev env path
params ty =
1215 check_abbrev_env env
;
1216 let ty0 = newgenvar
() in
1218 let abbrev = Mcons
(path
, ty0, ty0, Mnil
) in
1219 simple_abbrevs := abbrev;
1221 non_recursive_abbrev env
ty0
1222 (subst env generic_level
(ref abbrev) None
[] [] ty);
1223 simple_abbrevs := Mnil
;
1226 simple_abbrevs := Mnil
;
1230 let rec occur_rec env
visited ty0 ty =
1231 if ty == ty0 then raise Occur
;
1233 Tconstr
(p
, tl, abbrev) ->
1235 if List.memq
ty visited || !Clflags.recursive_types
then raise Occur
;
1236 iter_type_expr
(occur_rec env
(ty::visited) ty0) ty
1238 let ty'
= try_expand_head env
ty in
1239 (* Maybe we could simply make a recursive call here,
1240 but it seems it could make the occur check loop
1241 (see change in rev. 1.58) *)
1242 if ty'
== ty0 || List.memq
ty'
visited then raise Occur
;
1244 Tobject
_ | Tvariant
_ -> ()
1246 if not
!Clflags.recursive_types
then
1247 iter_type_expr
(occur_rec env
(ty'
::visited) ty0) ty'
1248 with Cannot_expand
->
1249 if not
!Clflags.recursive_types
then raise Occur
1251 | Tobject
_ | Tvariant
_ ->
1254 if not
!Clflags.recursive_types
then
1255 iter_type_expr
(occur_rec env
visited ty0) ty
1257 let type_changed = ref false (* trace possible changes to the studied type *)
1259 let merge r b
= if b
then r
:= true
1261 let occur env
ty0 ty =
1262 let old = !type_changed in
1264 while type_changed := false; occur_rec env
[] ty0 ty; !type_changed
1265 do () (* prerr_endline "changed" *) done;
1266 merge type_changed old
1268 merge type_changed old;
1269 raise
(match exn
with Occur
-> Unify
[] | _ -> exn
)
1272 (*****************************)
1273 (* Polymorphic Unification *)
1274 (*****************************)
1276 (* Since we cannot duplicate universal variables, unification must
1277 be done at meta-level, using bindings in univar_pairs *)
1278 let rec unify_univar t1 t2
= function
1279 (cl1
, cl2
) :: rem
->
1280 let find_univ t cl
=
1282 let (_, r
) = List.find (fun (t'
,_) -> t == repr t'
) cl
in
1284 with Not_found
-> None
1286 begin match find_univ t1 cl1
, find_univ t2 cl2
with
1287 Some
{contents
=Some
t'
2}, Some
_ when t2
== repr t'
2 ->
1289 | Some
({contents
=None
} as r1
), Some
({contents
=None
} as r2
) ->
1290 set_univar r1 t2
; set_univar r2 t1
1292 unify_univar t1 t2 rem
1296 | [] -> raise
(Unify
[])
1298 module TypeMap
= Map.Make
(TypeOps
)
1300 (* Test the occurence of free univars in a type *)
1301 (* that's way too expansive. Must do some kind of cacheing *)
1302 let occur_univar env
ty =
1303 let visited = ref TypeMap.empty
in
1304 let rec occur_rec bound ty =
1306 if ty.level >= lowest_level
&&
1307 if TypeSet.is_empty
bound then
1308 (ty.level <- pivot_level
- ty.level; true)
1310 let bound'
= TypeMap.find ty !visited in
1311 if TypeSet.exists
(fun x -> not
(TypeSet.mem
x bound)) bound'
then
1312 (visited := TypeMap.add
ty (TypeSet.inter
bound bound'
) !visited;
1316 visited := TypeMap.add
ty bound !visited;
1321 if not
(TypeSet.mem
ty bound) then raise
(Unify
[ty, newgenvar
()])
1322 | Tpoly
(ty, tyl) ->
1323 let bound = List.fold_right
TypeSet.add
(List.map
repr tyl) bound in
1325 | Tconstr
(_, [], _) -> ()
1326 | Tconstr
(p
, tl, _) ->
1328 let td = Env.find_type p env
in
1330 (fun t (pos
,neg
,_) -> if pos
|| neg
then occur_rec bound t)
1333 List.iter
(occur_rec bound) tl
1335 | _ -> iter_type_expr
(occur_rec bound) ty
1338 occur_rec TypeSet.empty
ty; unmark_type
ty
1340 unmark_type
ty; raise exn
1342 (* Grouping univars by families according to their binders *)
1344 List.fold_left
(fun s
(t,_) -> TypeSet.add
(repr t) s
)
1346 let get_univar_family univar_pairs
univars =
1347 if univars = [] then TypeSet.empty
else
1348 let rec insert s
= function
1349 cl1
, (_::_ as cl2
) ->
1350 if List.exists
(fun (t1
,_) -> TypeSet.mem
(repr t1
) s
) cl1
then
1355 let s = List.fold_right
TypeSet.add
univars TypeSet.empty
in
1356 List.fold_left
insert s univar_pairs
1358 (* Whether a family of univars escapes from a type *)
1359 let univars_escape env univar_pairs vl
ty =
1360 let family = get_univar_family univar_pairs vl
in
1361 let visited = ref TypeSet.empty
in
1364 if TypeSet.mem
t !visited then () else begin
1365 visited := TypeSet.add
t !visited;
1368 if List.exists
(fun t -> TypeSet.mem
(repr t) family) tl then ()
1371 if TypeSet.mem
t family then raise Occur
1372 | Tconstr
(_, [], _) -> ()
1373 | Tconstr
(p
, tl, _) ->
1375 let td = Env.find_type p env
in
1376 List.iter2
(fun t (pos
,neg
,_) -> if pos
|| neg
then occur t)
1382 iter_type_expr
occur t
1385 try occur ty; false with Occur
-> true
1387 (* Wrapper checking that no variable escapes and updating univar_pairs *)
1388 let enter_poly env univar_pairs t1 tl1 t2 tl2 f
=
1389 let old_univars = !univar_pairs
in
1391 List.fold_left
(fun s (cl
,_) -> add_univars s cl
)
1392 TypeSet.empty
old_univars
1394 let tl1 = List.map
repr tl1 and tl2
= List.map
repr tl2
in
1395 if List.exists
(fun t -> TypeSet.mem
t known_univars) tl1 &&
1396 univars_escape env
old_univars tl1 (newty(Tpoly
(t2
,tl2
)))
1397 || List.exists
(fun t -> TypeSet.mem
t known_univars) tl2
&&
1398 univars_escape env
old_univars tl2
(newty(Tpoly
(t1
,tl1)))
1399 then raise
(Unify
[]);
1400 let cl1 = List.map
(fun t -> t, ref None
) tl1
1401 and cl2
= List.map
(fun t -> t, ref None
) tl2
in
1402 univar_pairs
:= (cl1,cl2
) :: (cl2
,cl1) :: old_univars;
1403 try let res = f t1 t2
in univar_pairs
:= old_univars; res
1404 with exn
-> univar_pairs
:= old_univars; raise exn
1406 let univar_pairs = ref []
1415 let rec has_cached_expansion p
abbrev =
1418 | Mcons
(p'
, _, _, rem
) -> Path.same p p'
|| has_cached_expansion p rem
1419 | Mlink rem
-> has_cached_expansion p
!rem
1421 (**** Transform error trace ****)
1422 (* +++ Move it to some other place ? *)
1424 let expand_trace env trace
=
1426 (fun (t1
, t2
) rem
->
1427 (repr t1
, full_expand env t1
)::(repr t2
, full_expand env t2
)::rem
)
1430 (* build a dummy variant type *)
1431 let mkvariant fields closed
=
1434 {row_fields
= fields
; row_closed
= closed
; row_more
= newvar();
1435 row_bound
= (); row_fixed
= false; row_name
= None
})
1437 (**** Unification ****)
1439 (* Return whether [t0] occurs in [ty]. Objects are also traversed. *)
1440 let deep_occur t0
ty =
1441 let rec occur_rec ty =
1443 if ty.level >= lowest_level
then begin
1444 if ty == t0
then raise Occur
;
1445 ty.level <- pivot_level
- ty.level;
1446 iter_type_expr
occur_rec ty
1450 occur_rec ty; unmark_type
ty; false
1452 unmark_type
ty; true
1455 1. When unifying two non-abbreviated types, one type is made a link
1456 to the other. When unifying an abbreviated type with a
1457 non-abbreviated type, the non-abbreviated type is made a link to
1458 the other one. When unifying to abbreviated types, these two
1459 types are kept distincts, but they are made to (temporally)
1460 expand to the same type.
1461 2. Abbreviations with at least one parameter are systematically
1462 expanded. The overhead does not seem to high, and that way
1463 abbreviations where some parameters does not appear in the
1464 expansion, such as ['a t = int], are correctly handled. In
1465 particular, for this example, unifying ['a t] with ['b t] keeps
1466 ['a] and ['b] distincts. (Is it really important ?)
1467 3. Unifying an abbreviation ['a t = 'a] with ['a] should not yield
1468 ['a t as 'a]. Indeed, the type variable would otherwise be lost.
1469 This problem occurs for abbreviations expanding to a type
1470 variable, but also to many other constrained abbreviations (for
1471 instance, [(< x : 'a > -> unit) t = <x : 'a>]). The solution is
1472 that, if an abbreviation is unified with some subpart of its
1473 parameters, then the parameter actually does not get
1474 abbreviated. It would be possible to check whether some
1475 information is indeed lost, but it probably does not worth it.
1477 let rec unify env t1 t2
=
1478 (* First step: special cases (optimizations) *)
1479 if t1
== t2
then () else
1482 if t1 == t2 then () else
1485 type_changed := true;
1486 match (t1.desc, t2.desc) with
1487 (Tvar
, Tconstr
_) when deep_occur t1 t2 ->
1489 | (Tconstr
_, Tvar
) when deep_occur t2 t1 ->
1492 occur env
t1 t2; occur_univar env
t2;
1493 update_level env
t1.level t2;
1496 occur env
t2 t1; occur_univar env
t1;
1497 update_level env
t2.level t1;
1499 | (Tunivar
, Tunivar
) ->
1500 unify_univar t1 t2 !univar_pairs;
1501 update_level env
t1.level t2;
1503 | (Tconstr
(p1
, [], a1
), Tconstr
(p2
, [], a2
))
1504 when Path.same p1 p2
1505 (* This optimization assumes that t1 does not expand to t2
1506 (and conversely), so we fall back to the general case
1507 when any of the types has a cached expansion. *)
1508 && not
(has_cached_expansion p1
!a1
1509 || has_cached_expansion p2
!a2
) ->
1510 update_level env
t1.level t2;
1515 raise
(Unify
((t1, t2)::trace
))
1517 and unify2 env
t1 t2 =
1518 (* Second step: expansion of abbreviations *)
1519 let rec expand_both t1''
t2''
=
1520 let t1'
= expand_head_unif env
t1 in
1521 let t2'
= expand_head_unif env
t2 in
1522 (* Expansion may have changed the representative of the types... *)
1523 if t1'
== t1''
&& t2'
== t2''
then (t1'
,t2'
) else
1526 let t1'
, t2'
= expand_both t1 t2 in
1527 if t1'
== t2'
then () else
1529 let t1 = repr t1 and t2 = repr t2 in
1530 if (t1 == t1'
) || (t2 != t2'
) then
1531 unify3 env
t1 t1'
t2 t2'
1533 try unify3 env
t2 t2'
t1 t1'
with Unify trace
->
1534 raise
(Unify
(List.map
(fun (x, y
) -> (y
, x)) trace
))
1536 and unify3 env
t1 t1'
t2 t2'
=
1537 (* Third step: truly unification *)
1538 (* Assumes either [t1 == t1'] or [t2 != t2'] *)
1539 let d1 = t1'
.desc and d2
= t2'
.desc in
1541 let create_recursion = (t2 != t2'
) && (deep_occur t1'
t2) in
1543 update_level env
t1'
.level t2;
1547 begin match (d1, d2
) with
1551 let td1 = newgenty
d1 in
1553 occur_univar env
td1;
1554 if t1 == t1'
then begin
1555 (* The variable must be instantiated... *)
1556 let ty = newty2 t1'
.level d1 in
1557 update_level env
t2'
.level ty;
1562 update_level env
t2'
.level t1;
1565 | (Tarrow
(l1
, t1, u1
, c1
), Tarrow
(l2
, t2, u2
, c2
)) when l1
= l2
1566 || !Clflags.classic
&& not
(is_optional l1
|| is_optional l2
) ->
1567 unify env
t1 t2; unify env u1 u2
;
1568 begin match commu_repr c1
, commu_repr c2
with
1569 Clink r
, c2
-> set_commu r c2
1570 | c1
, Clink r
-> set_commu r c1
1573 | (Ttuple
tl1, Ttuple tl2
) ->
1574 unify_list env
tl1 tl2
1575 | (Tconstr
(p1
, tl1, _), Tconstr
(p2
, tl2
, _)) when Path.same p1 p2
->
1576 unify_list env
tl1 tl2
1577 | (Tobject
(fi1
, nm1
), Tobject
(fi2
, _)) ->
1578 unify_fields env fi1 fi2
;
1579 (* Type [t2'] may have been instantiated by [unify_fields] *)
1580 (* XXX One should do some kind of unification... *)
1581 begin match (repr t2'
).desc with
1582 Tobject
(_, {contents
= Some
(_, va
::_)})
1583 when let va = repr va in List.mem
va.desc [Tvar
; Tunivar
; Tnil
] ->
1585 | Tobject
(_, nm2
) ->
1590 | (Tvariant row1
, Tvariant row2
) ->
1591 unify_row env row1 row2
1592 | (Tfield
_, Tfield
_) -> (* Actually unused *)
1593 unify_fields env
t1'
t2'
1594 | (Tfield
(f
,kind
,_,rem
), Tnil
) | (Tnil
, Tfield
(f
,kind
,_,rem
)) ->
1595 begin match field_kind_repr kind
with
1596 Fvar r
when f
<> dummy_method -> set_kind r Fabsent
1597 | _ -> raise
(Unify
[])
1601 | (Tpoly
(t1, []), Tpoly
(t2, [])) ->
1603 | (Tpoly
(t1, tl1), Tpoly
(t2, tl2
)) ->
1604 enter_poly env
univar_pairs t1 tl1 t2 tl2
(unify env
)
1609 (* XXX Commentaires + changer "create_recursion" *)
1610 if create_recursion then begin
1612 Tconstr
(p
, tl, abbrev) ->
1613 forget_abbrev
abbrev p
;
1614 let t2''
= expand_head_unif env
t2 in
1615 if not
(closed_parameterized_type tl t2''
) then
1616 link_type
(repr t2) (repr t2'
)
1618 () (* t2 has already been expanded by update_level *)
1623 Can only be done afterwards, once the row variable has
1624 (possibly) been instantiated.
1626 if t1 != t1'
(* && t2 != t2' *) then begin
1627 match (t1.desc, t2.desc) with
1628 (Tconstr
(p
, ty::_, _), _)
1629 when ((repr ty).desc <> Tvar
)
1631 && not
(deep_occur t1 t2) ->
1632 update_level env
t1.level t2;
1634 | (_, Tconstr
(p
, ty::_, _))
1635 when ((repr ty).desc <> Tvar
)
1637 && not
(deep_occur t2 t1) ->
1638 update_level env
t2.level t1;
1649 and unify_list env
tl1 tl2
=
1650 if List.length
tl1 <> List.length tl2
then
1652 List.iter2
(unify env
) tl1 tl2
1654 and unify_fields env ty1 ty2
= (* Optimization *)
1655 let (fields1
, rest1
) = flatten_fields ty1
1656 and (fields2
, rest2
) = flatten_fields ty2
in
1657 let (pairs, miss1
, miss2
) = associate_fields fields1 fields2
in
1658 let l1 = (repr ty1
).level and l2
= (repr ty2
).level in
1660 if miss1
= [] then rest2
1661 else if miss2
= [] then rest1
1662 else newty2 (min
l1 l2
) Tvar
1664 let d1 = rest1
.desc and d2
= rest2
.desc in
1666 unify env
(build_fields l1 miss1
va) rest2
;
1667 unify env rest1
(build_fields l2 miss2
va);
1669 (fun (n
, k1
, t1, k2
, t2) ->
1671 try unify env
t1 t2 with Unify trace
->
1672 raise
(Unify
((newty (Tfield
(n
, k1
, t1, va)),
1673 newty (Tfield
(n
, k2
, t2, va)))::trace
)))
1676 log_type rest1
; rest1
.desc <- d1;
1677 log_type rest2
; rest2
.desc <- d2
;
1680 and unify_kind k1 k2
=
1681 let k1 = field_kind_repr
k1 in
1682 let k2 = field_kind_repr
k2 in
1683 if k1 == k2 then () else
1685 (Fvar r
, (Fvar
_ | Fpresent
)) -> set_kind r
k2
1686 | (Fpresent
, Fvar r
) -> set_kind r
k1
1687 | (Fpresent
, Fpresent
) -> ()
1690 and unify_pairs env tpl
=
1691 List.iter
(fun (t1, t2) -> unify env
t1 t2) tpl
1693 and unify_row env row1 row2
=
1694 let row1 = row_repr
row1 and row2
= row_repr row2
in
1695 let rm1 = row_more
row1 and rm2
= row_more row2
in
1696 if rm1 == rm2
then () else
1697 let r1, r2
, pairs = merge_row_fields row1.row_fields row2
.row_fields
in
1698 if r1 <> [] && r2
<> [] then begin
1699 let ht = Hashtbl.create
(List.length
r1) in
1700 List.iter
(fun (l
,_) -> Hashtbl.add
ht (hash_variant l
) l
) r1;
1703 try raise
(Tags
(l
, Hashtbl.find ht (hash_variant l
)))
1704 with Not_found
-> ())
1708 if row1.row_fixed
then rm1 else
1709 if row2
.row_fixed
then rm2
else
1711 in update_level env
(min
rm1.level rm2
.level) more;
1712 let fixed = row1.row_fixed
|| row2
.row_fixed
1713 and closed
= row1.row_closed
|| row2
.row_closed
in
1717 let f1, f2
= switch
f1 f2
in
1718 row_field_repr
f1 = Rabsent
|| row_field_repr f2
<> Rabsent
)
1722 List.for_all
(fun (_,f
) -> row_field_repr f
= Rabsent
) fields
in
1723 (* Check whether we are going to build an empty type *)
1724 if closed
&& (empty r1 || row2
.row_closed
) && (empty r2
|| row1.row_closed
)
1727 row_field_repr
f1 = Rabsent
|| row_field_repr f2
= Rabsent
)
1729 then raise
(Unify
[mkvariant [] true, mkvariant [] true]);
1731 if row1.row_name
<> None
&& (row1.row_closed
|| empty r2
) &&
1732 (not row2
.row_closed
|| keep (fun f1 f2
-> f1, f2
) && empty r1)
1734 else if row2
.row_name
<> None
&& (row2
.row_closed
|| empty r1) &&
1735 (not
row1.row_closed
|| keep (fun f1 f2
-> f2
, f1) && empty r2
)
1739 let row0 = {row_fields
= []; row_more
= more; row_bound
= ();
1740 row_closed
= closed
; row_fixed
= fixed; row_name
= name} in
1741 let set_more row rest
=
1744 filter_row_fields row.row_closed
rest
1746 if rest <> [] && (row.row_closed
|| row.row_fixed
)
1747 || closed
&& row.row_fixed
&& not
row.row_closed
then begin
1748 let t1 = mkvariant [] true and t2 = mkvariant rest false in
1749 raise
(Unify
[if row == row1 then (t1,t2) else (t2,t1)])
1751 let rm = row_more
row in
1752 if row.row_fixed
then
1753 if row0.row_more
== rm then () else
1754 if rm.desc = Tvar
then link_type
rm row0.row_more
else
1755 unify env
rm row0.row_more
1757 let ty = newty2 generic_level
(Tvariant
{row0 with row_fields
= rest}) in
1758 update_level env
rm.level ty;
1761 let md1 = rm1.desc and md2
= rm2
.desc in
1767 try unify_row_field env
row1.row_fixed row2
.row_fixed l
f1 f2
1769 raise
(Unify
((mkvariant [l
,f1] true,
1770 mkvariant [l
,f2
] true) :: trace
)))
1773 log_type
rm1; rm1.desc <- md1; log_type rm2
; rm2
.desc <- md2
; raise exn
1776 and unify_row_field env fixed1 fixed2 l
f1 f2
=
1777 let f1 = row_field_repr
f1 and f2
= row_field_repr f2
in
1778 if f1 == f2
then () else
1780 Rpresent
(Some
t1), Rpresent
(Some
t2) -> unify env
t1 t2
1781 | Rpresent None
, Rpresent None
-> ()
1782 | Reither
(c1
, tl1, m1
, e1
), Reither
(c2
, tl2
, m2
, e2
) ->
1783 if e1
== e2
then () else
1786 begin match tl1 @ tl2
with [] -> false
1788 if c1
|| c2
then raise
(Unify
[]);
1789 List.iter
(unify env
t1) tl;
1790 !e1
<> None
|| !e2
<> None
1792 if redo then unify_row_field env fixed1 fixed2 l
f1 f2
else
1793 let tl1 = List.map
repr tl1 and tl2
= List.map
repr tl2
in
1794 let rec remq tl = function [] -> []
1796 if List.memq
ty tl then remq tl tl'
else ty :: remq tl tl'
1798 let tl2'
= remq tl2 tl1 and tl1'
= remq tl1 tl2 in
1800 let f1'
= Reither
(c1
|| c2
, tl1'
, m1
|| m2
, e)
1801 and f2'
= Reither
(c1
|| c2
, tl2'
, m1
|| m2
, e) in
1802 set_row_field e1
f1'
; set_row_field e2 f2'
;
1803 | Reither
(_, _, false, e1
), Rabsent
-> set_row_field e1 f2
1804 | Rabsent
, Reither
(_, _, false, e2
) -> set_row_field e2
f1
1805 | Rabsent
, Rabsent
-> ()
1806 | Reither
(false, tl, _, e1
), Rpresent
(Some
t2) when not fixed1
->
1807 set_row_field e1 f2
;
1808 (try List.iter
(fun t1 -> unify env
t1 t2) tl
1809 with exn
-> e1
:= None
; raise exn
)
1810 | Rpresent
(Some
t1), Reither
(false, tl, _, e2
) when not fixed2
->
1811 set_row_field e2
f1;
1812 (try List.iter
(unify env
t1) tl
1813 with exn
-> e2
:= None
; raise exn
)
1814 | Reither
(true, [], _, e1
), Rpresent None
when not fixed1
->
1816 | Rpresent None
, Reither
(true, [], _, e2
) when not fixed2
->
1818 | _ -> raise
(Unify
[])
1821 let unify env ty1 ty2
=
1825 raise
(Unify
(expand_trace env trace
))
1827 let unify_var env
t1 t2 =
1828 let t1 = repr t1 and t2 = repr t2 in
1829 if t1 == t2 then () else
1834 update_level env
t1.level t2;
1837 raise
(Unify
(expand_trace env
((t1,t2)::trace
)))
1842 let _ = unify'
:= unify_var
1844 let unify_pairs env ty1 ty2
pairs =
1845 univar_pairs := pairs;
1848 let unify env ty1 ty2
=
1853 (**** Special cases of unification ****)
1856 Unify [t] and [l:'a -> 'b]. Return ['a] and ['b].
1857 In label mode, label mismatch is accepted when
1858 (1) the requested label is ""
1859 (2) the original label is not optional
1861 let rec filter_arrow env
t l
=
1862 let t = expand_head_unif env
t in
1865 let t1 = newvar () and t2 = newvar () in
1866 let t'
= newty (Tarrow
(l
, t1, t2, Cok
)) in
1867 update_level env
t.level t'
;
1870 | Tarrow
(l'
, t1, t2, _)
1871 when l
= l'
|| !Clflags.classic
&& l
= "" && not
(is_optional l'
) ->
1876 (* Used by [filter_method]. *)
1877 let rec filter_method_field env
name priv
ty =
1881 let level = ty.level in
1882 let ty1 = newvar2 level and ty2
= newvar2 level in
1883 let ty'
= newty2 level (Tfield
(name,
1884 begin match priv
with
1885 Private
-> Fvar
(ref None
)
1886 | Public
-> Fpresent
1892 | Tfield
(n
, kind
, ty1, ty2
) ->
1893 let kind = field_kind_repr
kind in
1894 if (n
= name) && (kind <> Fabsent
) then begin
1895 if priv
= Public
then
1896 unify_kind
kind Fpresent
;
1899 filter_method_field env
name priv ty2
1903 (* Unify [ty] and [< name : 'a; .. >]. Return ['a]. *)
1904 let rec filter_method env
name priv
ty =
1905 let ty = expand_head_unif env
ty in
1908 let ty1 = newvar () in
1909 let ty'
= newobj ty1 in
1910 update_level env
ty.level ty'
;
1912 filter_method_field env
name priv
ty1
1914 filter_method_field env
name priv f
1918 let check_filter_method env
name priv
ty =
1919 ignore
(filter_method env
name priv
ty)
1921 let filter_self_method env lab priv meths
ty =
1922 let ty'
= filter_method env lab priv
ty in
1924 Meths.find lab
!meths
1926 let pair = (Ident.create lab
, ty'
) in
1927 meths
:= Meths.add lab
pair !meths
;
1931 (***********************************)
1932 (* Matching between type schemes *)
1933 (***********************************)
1936 Update the level of [ty]. First check that the levels of generic
1937 variables from the subject are not lowered.
1939 let moregen_occur env
level ty =
1942 if ty.level > level then begin
1943 if ty.desc = Tvar
&& ty.level >= generic_level
- 1 then raise Occur
;
1944 ty.level <- pivot_level
- ty.level;
1946 Tvariant
row when static_row
row ->
1949 iter_type_expr
occur ty
1953 occur ty; unmark_type
ty
1955 unmark_type
ty; raise
(Unify
[])
1957 (* also check for free univars *)
1958 occur_univar env
ty;
1959 update_level env
level ty
1961 let may_instantiate inst_nongen
t1 =
1962 if inst_nongen
then t1.level <> generic_level
- 1
1963 else t1.level = generic_level
1965 let rec moregen inst_nongen type_pairs env
t1 t2 =
1966 if t1 == t2 then () else
1969 if t1 == t2 then () else
1972 match (t1.desc, t2.desc) with
1973 (Tunivar
, Tunivar
) ->
1974 unify_univar t1 t2 !univar_pairs
1975 | (Tvar
, _) when may_instantiate inst_nongen
t1 ->
1976 moregen_occur env
t1.level t2;
1979 | (Tconstr
(p1
, [], _), Tconstr
(p2
, [], _)) when Path.same p1 p2
->
1982 let t1'
= expand_head_unif env
t1 in
1983 let t2'
= expand_head_unif env
t2 in
1984 (* Expansion may have changed the representative of the types... *)
1985 let t1'
= repr t1'
and t2'
= repr t2'
in
1986 if t1'
== t2'
then () else
1988 TypePairs.find type_pairs
(t1'
, t2'
)
1990 TypePairs.add type_pairs
(t1'
, t2'
) ();
1991 match (t1'
.desc, t2'
.desc) with
1992 (Tvar
, _) when may_instantiate inst_nongen
t1 ->
1993 moregen_occur env
t1'
.level t2;
1995 | (Tarrow
(l1, t1, u1
, _), Tarrow
(l2
, t2, u2
, _)) when l1 = l2
1996 || !Clflags.classic
&& not
(is_optional
l1 || is_optional l2
) ->
1997 moregen inst_nongen type_pairs env
t1 t2;
1998 moregen inst_nongen type_pairs env u1 u2
1999 | (Ttuple
tl1, Ttuple
tl2) ->
2000 moregen_list inst_nongen type_pairs env
tl1 tl2
2001 | (Tconstr
(p1
, tl1, _), Tconstr
(p2
, tl2, _))
2002 when Path.same p1 p2
->
2003 moregen_list inst_nongen type_pairs env
tl1 tl2
2004 | (Tvariant
row1, Tvariant row2
) ->
2005 moregen_row inst_nongen type_pairs env
row1 row2
2006 | (Tobject
(fi1
, nm1
), Tobject
(fi2
, nm2
)) ->
2007 moregen_fields inst_nongen type_pairs env fi1 fi2
2008 | (Tfield
_, Tfield
_) -> (* Actually unused *)
2009 moregen_fields inst_nongen type_pairs env
t1'
t2'
2012 | (Tpoly
(t1, []), Tpoly
(t2, [])) ->
2013 moregen inst_nongen type_pairs env
t1 t2
2014 | (Tpoly
(t1, tl1), Tpoly
(t2, tl2)) ->
2015 enter_poly env
univar_pairs t1 tl1 t2 tl2
2016 (moregen inst_nongen type_pairs env
)
2021 raise
(Unify
((t1, t2)::trace
))
2023 and moregen_list inst_nongen type_pairs env
tl1 tl2 =
2024 if List.length
tl1 <> List.length
tl2 then
2026 List.iter2
(moregen inst_nongen type_pairs env
) tl1 tl2
2028 and moregen_fields inst_nongen type_pairs env
ty1 ty2
=
2029 let (fields1
, rest1
) = flatten_fields ty1
2030 and (fields2
, rest2
) = flatten_fields ty2
in
2031 let (pairs, miss1
, miss2
) = associate_fields fields1 fields2
in
2032 if miss1
<> [] then raise
(Unify
[]);
2033 moregen inst_nongen type_pairs env rest1
2034 (build_fields (repr ty2
).level miss2 rest2
);
2036 (fun (n
, k1, t1, k2, t2) ->
2038 try moregen inst_nongen type_pairs env
t1 t2 with Unify trace
->
2039 raise
(Unify
((newty (Tfield
(n
, k1, t1, rest2
)),
2040 newty (Tfield
(n
, k2, t2, rest2
)))::trace
)))
2043 and moregen_kind
k1 k2 =
2044 let k1 = field_kind_repr
k1 in
2045 let k2 = field_kind_repr
k2 in
2046 if k1 == k2 then () else
2048 (Fvar r
, (Fvar
_ | Fpresent
)) -> set_kind r
k2
2049 | (Fpresent
, Fpresent
) -> ()
2050 | _ -> raise
(Unify
[])
2052 and moregen_row inst_nongen type_pairs env
row1 row2
=
2053 let row1 = row_repr
row1 and row2
= row_repr row2
in
2054 let rm1 = repr row1.row_more
and rm2
= repr row2
.row_more
in
2055 if rm1 == rm2
then () else
2056 let may_inst = rm1.desc = Tvar
&& may_instantiate inst_nongen
rm1 in
2057 let r1, r2
, pairs = merge_row_fields row1.row_fields row2
.row_fields
in
2059 if row2
.row_closed
then
2060 filter_row_fields may_inst r1, filter_row_fields false r2
2063 if r1 <> [] || row1.row_closed
&& (not row2
.row_closed
|| r2
<> [])
2064 then raise
(Unify
[]);
2065 begin match rm1.desc, rm2
.desc with
2067 unify_univar rm1 rm2
!univar_pairs
2068 | Tunivar
, _ | _, Tunivar
->
2070 | _ when static_row
row1 -> ()
2071 | _ when may_inst ->
2072 if not
(static_row row2
) then moregen_occur env
rm1.level rm2
;
2074 if r2
= [] then rm2
else
2075 let row_ext = {row2
with row_fields
= r2
} in
2076 iter_row
(moregen_occur env
rm1.level) row_ext;
2077 newty2 rm1.level (Tvariant
row_ext)
2080 | Tconstr
_, Tconstr
_ ->
2081 moregen inst_nongen type_pairs env
rm1 rm2
2082 | _ -> raise
(Unify
[])
2086 let f1 = row_field_repr
f1 and f2
= row_field_repr f2
in
2087 if f1 == f2
then () else
2089 Rpresent
(Some
t1), Rpresent
(Some
t2) ->
2090 moregen inst_nongen type_pairs env
t1 t2
2091 | Rpresent None
, Rpresent None
-> ()
2092 | Reither
(false, tl1, _, e1
), Rpresent
(Some
t2) when may_inst ->
2093 set_row_field e1 f2
;
2094 List.iter
(fun t1 -> moregen inst_nongen type_pairs env
t1 t2) tl1
2095 | Reither
(c1
, tl1, _, e1
), Reither
(c2
, tl2, m2
, e2
) ->
2096 if e1
!= e2
then begin
2097 if c1
&& not c2
then raise
(Unify
[]);
2098 set_row_field e1
(Reither
(c2
, [], m2
, e2
));
2099 if List.length
tl1 = List.length
tl2 then
2100 List.iter2
(moregen inst_nongen type_pairs env
) tl1 tl2
2103 List.iter
(fun t1 -> moregen inst_nongen type_pairs env
t1 t2)
2106 if tl1 <> [] then raise
(Unify
[])
2108 | Reither
(true, [], _, e1
), Rpresent None
when may_inst ->
2110 | Reither
(_, _, _, e1
), Rabsent
when may_inst ->
2112 | Rabsent
, Rabsent
-> ()
2113 | _ -> raise
(Unify
[]))
2116 (* Must empty univar_pairs first *)
2117 let moregen inst_nongen type_pairs env patt subj
=
2119 moregen inst_nongen type_pairs env patt subj
2122 Non-generic variable can be instanciated only if [inst_nongen] is
2123 true. So, [inst_nongen] should be set to false if the subject might
2124 contain non-generic variables (and we do not want them to be
2126 Usually, the subject is given by the user, and the pattern
2127 is unimportant. So, no need to propagate abbreviations.
2129 let moregeneral env inst_nongen pat_sch subj_sch
=
2130 let old_level = !current_level in
2131 current_level := generic_level
- 1;
2133 Generic variables are first duplicated with [instance]. So,
2134 their levels are lowered to [generic_level - 1]. The subject is
2135 then copied with [duplicate_type]. That way, its levels won't be
2138 let subj = duplicate_type (instance subj_sch
) in
2139 current_level := generic_level
;
2140 (* Duplicate generic variables *)
2141 let patt = instance pat_sch
in
2143 try moregen inst_nongen
(TypePairs.create
13) env
patt subj; true with
2146 current_level := old_level;
2150 (* Alternative approach: "rigidify" a type scheme,
2151 and check validity after unification *)
2154 let rec rigidify_rec vars ty =
2156 if ty.level >= lowest_level
then begin
2157 ty.level <- pivot_level
- ty.level;
2160 if not
(List.memq
ty !vars) then vars := ty :: !vars
2162 let row = row_repr
row in
2163 let more = repr row.row_more
in
2164 if more.desc = Tvar
&& not
row.row_fixed
then begin
2165 let more'
= newty2 more.level Tvar
in
2166 let row'
= {row with row_fixed
=true; row_fields
=[]; row_more
=more'
}
2167 in link_type
more (newty2 ty.level (Tvariant
row'
))
2169 iter_row
(rigidify_rec vars) row;
2170 (* only consider the row variable if the variant is not static *)
2171 if not
(static_row
row) then rigidify_rec vars (row_more
row)
2173 iter_type_expr
(rigidify_rec vars) ty
2177 let vars = ref [] in
2178 rigidify_rec vars ty;
2182 let all_distinct_vars env
vars =
2186 let ty = expand_head env
ty in
2187 if List.memq
ty !tyl then false else
2188 (tyl := ty :: !tyl; ty.desc = Tvar
))
2191 let matches env
ty ty'
=
2192 let snap = snapshot
() in
2193 let vars = rigidify ty in
2196 try unify env
ty ty'
; all_distinct_vars env
vars
2197 with Unify
_ -> false
2203 (*********************************************)
2204 (* Equivalence between parameterized types *)
2205 (*********************************************)
2207 let normalize_subst subst =
2209 (function {desc=Tlink
_}, _ | _, {desc=Tlink
_} -> true | _ -> false)
2211 then subst := List.map
(fun (t1,t2) -> repr t1, repr t2) !subst
2213 let rec eqtype rename type_pairs
subst env
t1 t2 =
2214 if t1 == t2 then () else
2217 if t1 == t2 then () else
2220 match (t1.desc, t2.desc) with
2221 (Tvar
, Tvar
) when rename
->
2223 normalize_subst subst;
2224 if List.assq
t1 !subst != t2 then raise
(Unify
[])
2226 subst := (t1, t2) :: !subst
2228 | (Tconstr
(p1
, [], _), Tconstr
(p2
, [], _)) when Path.same p1 p2
->
2231 let t1'
= expand_head_unif env
t1 in
2232 let t2'
= expand_head_unif env
t2 in
2233 (* Expansion may have changed the representative of the types... *)
2234 let t1'
= repr t1'
and t2'
= repr t2'
in
2235 if t1'
== t2'
then () else
2237 TypePairs.find type_pairs
(t1'
, t2'
)
2239 TypePairs.add type_pairs
(t1'
, t2'
) ();
2240 match (t1'
.desc, t2'
.desc) with
2241 (Tvar
, Tvar
) when rename
->
2243 normalize_subst subst;
2244 if List.assq
t1'
!subst != t2'
then raise
(Unify
[])
2246 subst := (t1'
, t2'
) :: !subst
2248 | (Tarrow
(l1, t1, u1
, _), Tarrow
(l2
, t2, u2
, _)) when l1 = l2
2249 || !Clflags.classic
&& not
(is_optional
l1 || is_optional l2
) ->
2250 eqtype rename type_pairs
subst env
t1 t2;
2251 eqtype rename type_pairs
subst env u1 u2
;
2252 | (Ttuple
tl1, Ttuple
tl2) ->
2253 eqtype_list rename type_pairs
subst env
tl1 tl2
2254 | (Tconstr
(p1
, tl1, _), Tconstr
(p2
, tl2, _))
2255 when Path.same p1 p2
->
2256 eqtype_list rename type_pairs
subst env
tl1 tl2
2257 | (Tvariant
row1, Tvariant row2
) ->
2258 eqtype_row rename type_pairs
subst env
row1 row2
2259 | (Tobject
(fi1
, nm1
), Tobject
(fi2
, nm2
)) ->
2260 eqtype_fields rename type_pairs
subst env fi1 fi2
2261 | (Tfield
_, Tfield
_) -> (* Actually unused *)
2262 eqtype_fields rename type_pairs
subst env
t1'
t2'
2265 | (Tpoly
(t1, []), Tpoly
(t2, [])) ->
2266 eqtype rename type_pairs
subst env
t1 t2
2267 | (Tpoly
(t1, tl1), Tpoly
(t2, tl2)) ->
2268 enter_poly env
univar_pairs t1 tl1 t2 tl2
2269 (eqtype rename type_pairs
subst env
)
2270 | (Tunivar
, Tunivar
) ->
2271 unify_univar t1'
t2'
!univar_pairs
2276 raise
(Unify
((t1, t2)::trace
))
2278 and eqtype_list rename type_pairs
subst env
tl1 tl2 =
2279 if List.length
tl1 <> List.length
tl2 then
2281 List.iter2
(eqtype rename type_pairs
subst env
) tl1 tl2
2283 and eqtype_fields rename type_pairs
subst env
ty1 ty2
=
2284 let (fields2
, rest2
) = flatten_fields ty2
in
2285 (* Try expansion, needed when called from Includecore.type_manifest *)
2286 try match try_expand_head env rest2
with
2287 {desc=Tobject
(ty2
,_)} -> eqtype_fields rename type_pairs
subst env
ty1 ty2
2288 | _ -> raise Cannot_expand
2289 with Cannot_expand
->
2290 let (fields1
, rest1
) = flatten_fields ty1 in
2291 let (pairs, miss1
, miss2
) = associate_fields fields1 fields2
in
2292 eqtype rename type_pairs
subst env rest1 rest2
;
2293 if (miss1
<> []) || (miss2
<> []) then raise
(Unify
[]);
2295 (function (n
, k1, t1, k2, t2) ->
2297 try eqtype rename type_pairs
subst env
t1 t2 with Unify trace
->
2298 raise
(Unify
((newty (Tfield
(n
, k1, t1, rest2
)),
2299 newty (Tfield
(n
, k2, t2, rest2
)))::trace
)))
2302 and eqtype_kind
k1 k2 =
2303 let k1 = field_kind_repr
k1 in
2304 let k2 = field_kind_repr
k2 in
2307 | (Fpresent
, Fpresent
) -> ()
2308 | _ -> raise
(Unify
[])
2310 and eqtype_row rename type_pairs
subst env
row1 row2
=
2311 (* Try expansion, needed when called from Includecore.type_manifest *)
2312 try match try_expand_head env
(row_more row2
) with
2313 {desc=Tvariant row2
} -> eqtype_row rename type_pairs
subst env
row1 row2
2314 | _ -> raise Cannot_expand
2315 with Cannot_expand
->
2316 let row1 = row_repr
row1 and row2
= row_repr row2
in
2317 let r1, r2
, pairs = merge_row_fields row1.row_fields row2
.row_fields
in
2318 if row1.row_closed
<> row2
.row_closed
2319 || not
row1.row_closed
&& (r1 <> [] || r2
<> [])
2320 || filter_row_fields false (r1 @ r2
) <> []
2321 then raise
(Unify
[]);
2322 if not
(static_row
row1) then
2323 eqtype rename type_pairs
subst env
row1.row_more row2
.row_more
;
2326 match row_field_repr
f1, row_field_repr f2
with
2327 Rpresent
(Some
t1), Rpresent
(Some
t2) ->
2328 eqtype rename type_pairs
subst env
t1 t2
2329 | Reither
(true, [], _, _), Reither
(true, [], _, _) ->
2331 | Reither
(false, t1::tl1, _, _), Reither
(false, t2::tl2, _, _) ->
2332 eqtype rename type_pairs
subst env
t1 t2;
2333 if List.length
tl1 = List.length
tl2 then
2334 (* if same length allow different types (meaning?) *)
2335 List.iter2
(eqtype rename type_pairs
subst env
) tl1 tl2
2337 (* otherwise everything must be equal *)
2338 List.iter
(eqtype rename type_pairs
subst env
t1) tl2;
2339 List.iter
(fun t1 -> eqtype rename type_pairs
subst env
t1 t2) tl1
2341 | Rpresent None
, Rpresent None
-> ()
2342 | Rabsent
, Rabsent
-> ()
2343 | _ -> raise
(Unify
[]))
2346 (* Two modes: with or without renaming of variables *)
2347 let equal env rename tyl1 tyl2
=
2350 eqtype_list rename
(TypePairs.create
11) (ref []) env tyl1 tyl2
; true
2354 (* Must empty univar_pairs first *)
2355 let eqtype rename type_pairs
subst env
t1 t2 =
2357 eqtype rename type_pairs
subst env
t1 t2
2360 (*************************)
2361 (* Class type matching *)
2362 (*************************)
2365 type class_match_failure
=
2367 | CM_Parameter_arity_mismatch
of int * int
2368 | CM_Type_parameter_mismatch
of (type_expr
* type_expr
) list
2369 | CM_Class_type_mismatch
of class_type
* class_type
2370 | CM_Parameter_mismatch
of (type_expr
* type_expr
) list
2371 | CM_Val_type_mismatch
of string * (type_expr
* type_expr
) list
2372 | CM_Meth_type_mismatch
of string * (type_expr
* type_expr
) list
2373 | CM_Non_mutable_value
of string
2374 | CM_Non_concrete_value
of string
2375 | CM_Missing_value
of string
2376 | CM_Missing_method
of string
2377 | CM_Hide_public
of string
2378 | CM_Hide_virtual
of string * string
2379 | CM_Public_method
of string
2380 | CM_Private_method
of string
2381 | CM_Virtual_method
of string
2383 exception Failure
of class_match_failure list
2385 let rec moregen_clty trace type_pairs env cty1 cty2
=
2387 match cty1
, cty2
with
2388 Tcty_constr
(_, _, cty1
), _ ->
2389 moregen_clty true type_pairs env cty1 cty2
2390 | _, Tcty_constr
(_, _, cty2
) ->
2391 moregen_clty true type_pairs env cty1 cty2
2392 | Tcty_fun
(l1, ty1, cty1'
), Tcty_fun
(l2
, ty2
, cty2'
) when l1 = l2
->
2393 begin try moregen true type_pairs env
ty1 ty2
with Unify trace
->
2394 raise
(Failure
[CM_Parameter_mismatch
(expand_trace env trace
)])
2396 moregen_clty false type_pairs env cty1' cty2'
2397 | Tcty_signature sign1
, Tcty_signature sign2
->
2398 let ty1 = object_fields (repr sign1
.cty_self
) in
2399 let ty2 = object_fields (repr sign2
.cty_self
) in
2400 let (fields1
, rest1
) = flatten_fields ty1
2401 and (fields2
, rest2
) = flatten_fields ty2 in
2402 let (pairs, miss1
, miss2
) = associate_fields fields1 fields2
in
2404 (fun (lab
, k1, t1, k2, t2) ->
2405 begin try moregen true type_pairs env
t1 t2 with Unify trace
->
2406 raise
(Failure
[CM_Meth_type_mismatch
2407 (lab
, expand_trace env trace
)])
2411 (fun lab
(mut
, v
, ty) ->
2412 let (mut'
, v'
, ty'
) = Vars.find lab sign1
.cty_vars
in
2413 try moregen true type_pairs env
ty'
ty with Unify trace
->
2414 raise
(Failure
[CM_Val_type_mismatch
2415 (lab
, expand_trace env trace
)]))
2420 Failure error
when trace
->
2421 raise
(Failure
(CM_Class_type_mismatch
(cty1
, cty2
)::error
))
2423 let match_class_types env pat_sch subj_sch
=
2424 let type_pairs = TypePairs.create
53 in
2425 let old_level = !current_level in
2426 current_level := generic_level
- 1;
2428 Generic variables are first duplicated with [instance]. So,
2429 their levels are lowered to [generic_level - 1]. The subject is
2430 then copied with [duplicate_type]. That way, its levels won't be
2433 let (_, subj_inst
) = instance_class [] subj_sch
in
2434 let subj = duplicate_class_type subj_inst
in
2435 current_level := generic_level
;
2436 (* Duplicate generic variables *)
2437 let (_, patt) = instance_class [] pat_sch
in
2439 let sign1 = signature_of_class_type patt in
2440 let sign2 = signature_of_class_type subj in
2441 let t1 = repr sign1.cty_self
in
2442 let t2 = repr sign2.cty_self
in
2443 TypePairs.add
type_pairs (t1, t2) ();
2444 let (fields1
, rest1
) = flatten_fields (object_fields t1)
2445 and (fields2
, rest2
) = flatten_fields (object_fields t2) in
2446 let (pairs, miss1
, miss2
) = associate_fields fields1 fields2
in
2449 (fun (lab
, k
, _) err
->
2451 let k = field_kind_repr
k in
2453 Fvar r
-> set_kind r Fabsent
; err
2454 | _ -> CM_Hide_public lab
::err
2457 if Concr.mem lab
sign1.cty_concr
then err
2458 else CM_Hide_virtual
("method", lab
) :: err)
2461 let missing_method = List.map
(fun (m
, _, _) -> m
) miss2
in
2463 (List.map
(fun m
-> CM_Missing_method m
) missing_method) @ error
2465 (* Always succeeds *)
2466 moregen true type_pairs env rest1 rest2
;
2469 (fun (lab
, k1, t1, k2, t2) err ->
2470 try moregen_kind
k1 k2; err with
2471 Unify
_ -> CM_Public_method lab
::err)
2476 (fun lab
(mut
, vr
, ty) err ->
2478 let (mut'
, vr'
, ty'
) = Vars.find lab
sign1.cty_vars
in
2479 if mut
= Mutable
&& mut'
<> Mutable
then
2480 CM_Non_mutable_value lab
::err
2481 else if vr
= Concrete
&& vr'
<> Concrete
then
2482 CM_Non_concrete_value lab
::err
2486 CM_Missing_value lab
::err)
2487 sign2.cty_vars
error
2491 (fun lab
(_,vr
,_) err ->
2492 if vr
= Virtual
&& not
(Vars.mem lab
sign2.cty_vars
) then
2493 CM_Hide_virtual
("instance variable", lab
) :: err
2495 sign1.cty_vars
error
2500 if List.mem
e missing_method then l
else CM_Virtual_method
e::l
)
2501 (Concr.elements
(Concr.diff
sign2.cty_concr
sign1.cty_concr
))
2507 moregen_clty true type_pairs env
patt subj;
2513 CM_Class_type_mismatch
(patt, subj)::error
2515 current_level := old_level;
2518 let rec equal_clty trace
type_pairs subst env cty1 cty2
=
2520 match cty1
, cty2
with
2521 Tcty_constr
(_, _, cty1
), Tcty_constr
(_, _, cty2
) ->
2522 equal_clty true type_pairs subst env cty1 cty2
2523 | Tcty_constr
(_, _, cty1
), _ ->
2524 equal_clty true type_pairs subst env cty1 cty2
2525 | _, Tcty_constr
(_, _, cty2
) ->
2526 equal_clty true type_pairs subst env cty1 cty2
2527 | Tcty_fun
(l1, ty1, cty1'
), Tcty_fun
(l2
, ty2, cty2'
) when l1 = l2
->
2528 begin try eqtype true type_pairs subst env
ty1 ty2 with Unify trace
->
2529 raise
(Failure
[CM_Parameter_mismatch
(expand_trace env trace
)])
2531 equal_clty false type_pairs subst env cty1' cty2'
2532 | Tcty_signature
sign1, Tcty_signature
sign2 ->
2533 let ty1 = object_fields (repr sign1.cty_self
) in
2534 let ty2 = object_fields (repr sign2.cty_self
) in
2535 let (fields1
, rest1
) = flatten_fields ty1
2536 and (fields2
, rest2
) = flatten_fields ty2 in
2537 let (pairs, miss1
, miss2
) = associate_fields fields1 fields2
in
2539 (fun (lab
, k1, t1, k2, t2) ->
2540 begin try eqtype true type_pairs subst env
t1 t2 with
2542 raise
(Failure
[CM_Meth_type_mismatch
2543 (lab
, expand_trace env trace
)])
2547 (fun lab
(_, _, ty) ->
2548 let (_, _, ty'
) = Vars.find lab
sign1.cty_vars
in
2549 try eqtype true type_pairs subst env
ty ty'
with Unify trace
->
2550 raise
(Failure
[CM_Val_type_mismatch
2551 (lab
, expand_trace env trace
)]))
2555 (Failure
(if trace
then []
2556 else [CM_Class_type_mismatch
(cty1
, cty2
)]))
2558 Failure
error when trace
->
2559 raise
(Failure
(CM_Class_type_mismatch
(cty1
, cty2
)::error))
2561 (* XXX On pourrait autoriser l'instantiation du type des parametres... *)
2562 (* XXX Correct ? (variables de type dans parametres et corps de classe *)
2563 let match_class_declarations env patt_params patt_type subj_params subj_type
=
2564 let type_pairs = TypePairs.create
53 in
2565 let subst = ref [] in
2566 let sign1 = signature_of_class_type patt_type
in
2567 let sign2 = signature_of_class_type subj_type
in
2568 let t1 = repr sign1.cty_self
in
2569 let t2 = repr sign2.cty_self
in
2570 TypePairs.add
type_pairs (t1, t2) ();
2571 let (fields1
, rest1
) = flatten_fields (object_fields t1)
2572 and (fields2
, rest2
) = flatten_fields (object_fields t2) in
2573 let (pairs, miss1
, miss2
) = associate_fields fields1 fields2
in
2576 (fun (lab
, k, _) err ->
2578 let k = field_kind_repr
k in
2581 | _ -> CM_Hide_public lab
::err
2584 if Concr.mem lab
sign1.cty_concr
then err
2585 else CM_Hide_virtual
("method", lab
) :: err)
2588 let missing_method = List.map
(fun (m
, _, _) -> m
) miss2
in
2590 (List.map
(fun m
-> CM_Missing_method m
) missing_method) @ error
2592 (* Always succeeds *)
2593 eqtype true type_pairs subst env rest1 rest2
;
2596 (fun (lab
, k1, t1, k2, t2) err ->
2597 let k1 = field_kind_repr
k1 in
2598 let k2 = field_kind_repr
k2 in
2601 | (Fpresent
, Fpresent
) -> err
2602 | (Fvar
_, Fpresent
) -> CM_Private_method lab
::err
2603 | (Fpresent
, Fvar
_) -> CM_Public_method lab
::err
2604 | _ -> assert false)
2609 (fun lab
(mut
, vr
, ty) err ->
2611 let (mut'
, vr'
, ty'
) = Vars.find lab
sign1.cty_vars
in
2612 if mut
= Mutable
&& mut'
<> Mutable
then
2613 CM_Non_mutable_value lab
::err
2614 else if vr
= Concrete
&& vr'
<> Concrete
then
2615 CM_Non_concrete_value lab
::err
2619 CM_Missing_value lab
::err)
2620 sign2.cty_vars
error
2624 (fun lab
(_,vr
,_) err ->
2625 if vr
= Virtual
&& not
(Vars.mem lab
sign2.cty_vars
) then
2626 CM_Hide_virtual
("instance variable", lab
) :: err
2628 sign1.cty_vars
error
2633 if List.mem
e missing_method then l
else CM_Virtual_method
e::l
)
2634 (Concr.elements
(Concr.diff
sign2.cty_concr
sign1.cty_concr
))
2640 let lp = List.length patt_params
in
2641 let ls = List.length subj_params
in
2643 raise
(Failure
[CM_Parameter_arity_mismatch
(lp, ls)]);
2644 List.iter2
(fun p
s ->
2645 try eqtype true type_pairs subst env p
s with Unify trace
->
2646 raise
(Failure
[CM_Type_parameter_mismatch
2647 (expand_trace env trace
)]))
2648 patt_params subj_params
;
2649 equal_clty false type_pairs subst env patt_type subj_type
;
2663 (**** Build a subtype of a given type. ****)
2666 [visited] traces traversed object and variant types
2667 [loops] is a mapping from variables to variables, to reproduce
2668 positive loops in a class type
2669 [posi] true if the current variance is positive
2670 [level] number of expansions/enlargement allowed on this branch *)
2672 let warn = ref false (* whether double coercion might do better *)
2673 let pred_expand n
= if n
mod 2 = 0 && n
> 0 then pred n
else n
2674 let pred_enlarge n
= if n
mod 2 = 1 then pred n
else n
2676 type change
= Unchanged
| Equiv
| Changed
2677 let collect l
= List.fold_left
(fun c1
(_, c2
) -> max c1 c2
) Unchanged l
2679 let rec filter_visited = function
2681 | {desc=Tobject
_|Tvariant
_} :: _ as l
-> l
2682 | _ :: l
-> filter_visited l
2684 let memq_warn t visited =
2685 if List.memq
t visited then (warn := true; true) else false
2687 let rec lid_of_path sharp
= function
2689 Longident.Lident
(sharp ^
Ident.name id
)
2690 | Path.Pdot
(p1
, s, _) ->
2691 Longident.Ldot
(lid_of_path "" p1
, sharp ^
s)
2692 | Path.Papply
(p1
, p2
) ->
2693 Longident.Lapply
(lid_of_path sharp p1
, lid_of_path "" p2
)
2695 let find_cltype_for_path env p
=
2696 let path, cl_abbr
= Env.lookup_type
(lid_of_path "#" p
) env
in
2697 match cl_abbr
.type_manifest
with
2699 begin match (repr ty).desc with
2700 Tobject
(_,{contents
=Some
(p'
,_)}) when Path.same p p'
-> cl_abbr
, ty
2701 | _ -> raise Not_found
2703 | None
-> assert false
2705 let has_constr_row' env
t =
2706 has_constr_row (expand_abbrev env
t)
2708 let rec build_subtype env
visited loops posi
level t =
2714 let t'
= List.assq
t loops
in
2721 | Tarrow
(l
, t1, t2, _) ->
2722 if memq_warn t visited then (t, Unchanged
) else
2723 let visited = t :: visited in
2724 let (t1'
, c1
) = build_subtype env
visited loops
(not posi
) level t1 in
2725 let (t2'
, c2
) = build_subtype env
visited loops posi
level t2 in
2726 let c = max c1 c2
in
2727 if c > Unchanged
then (newty (Tarrow
(l
, t1'
, t2'
, Cok
)), c)
2730 if memq_warn t visited then (t, Unchanged
) else
2731 let visited = t :: visited in
2733 List.map
(build_subtype env
visited loops posi
level) tlist
2735 let c = collect tlist'
in
2736 if c > Unchanged
then (newty (Ttuple
(List.map fst
tlist'
)), c)
2738 | Tconstr
(p
, tl, abbrev)
2739 when level > 0 && generic_abbrev env p
&& safe_abbrev env
t
2740 && not
(has_constr_row' env
t) ->
2741 let t'
= repr (expand_abbrev env
t) in
2742 let level'
= pred_expand level in
2743 begin try match t'
.desc with
2744 Tobject
_ when posi
&& not
(opened_object t'
) ->
2745 let cl_abbr, body
= find_cltype_for_path env p
in
2747 subst env
!current_level abbrev None
cl_abbr.type_params
tl body
in
2751 Tobject
(ty1,{contents
=Some
(p'
,tl1)}) when Path.same p p'
->
2753 | _ -> raise Not_found
2756 let t''
= newvar () in
2757 let loops = (ty, t''
) :: loops in
2758 (* May discard [visited] as level is going down *)
2760 build_subtype env
[t'
] loops posi
(pred_enlarge level'
) ty1 in
2761 assert (t''
.desc = Tvar
);
2763 if c > Equiv
|| deep_occur ty ty1'
then None
else Some
(p
,tl1) in
2764 t''
.desc <- Tobject
(ty1'
, ref nm);
2765 (try unify_var env
ty t with Unify
_ -> assert false);
2767 | _ -> raise Not_found
2769 let (t''
,c) = build_subtype env
visited loops posi
level'
t'
in
2770 if c > Unchanged
then (t''
,c)
2773 | Tconstr
(p
, tl, abbrev) ->
2774 (* Must check recursion on constructors, since we do not always
2776 if memq_warn t visited then (t, Unchanged
) else
2777 let visited = t :: visited in
2779 let decl = Env.find_type p env
in
2780 if level = 0 && generic_abbrev env p
&& safe_abbrev env
t
2781 && not
(has_constr_row' env
t)
2787 if co
then (t, Unchanged
)
2788 else build_subtype env
visited loops (not posi
) level t
2790 if co
then build_subtype env
visited loops posi
level t
2791 else (newvar(), Changed
))
2792 decl.type_variance
tl
2794 let c = collect tl'
in
2795 if c > Unchanged
then (newconstr p
(List.map fst
tl'
), c)
2801 let row = row_repr
row in
2802 if memq_warn t visited || not
(static_row
row) then (t, Unchanged
) else
2803 let level'
= pred_enlarge level in
2805 t :: if level'
< level then [] else filter_visited visited in
2806 let fields = filter_row_fields false row.row_fields
in
2809 (fun (l
,f
as orig
) -> match row_field_repr f
with
2812 (l
, Reither
(true, [], false, ref None
)), Unchanged
2815 | Rpresent
(Some
t) ->
2816 let (t'
, c) = build_subtype env
visited loops posi
level'
t in
2818 if posi
&& level > 0
2819 then Reither
(false, [t'
], false, ref None
)
2820 else Rpresent
(Some
t'
)
2822 | _ -> assert false)
2825 let c = collect fields in
2827 { row_fields
= List.map fst
fields; row_more
= newvar();
2828 row_bound
= (); row_closed
= posi
; row_fixed
= false;
2829 row_name
= if c > Unchanged
then None
else row.row_name
}
2831 (newty (Tvariant
row), Changed
)
2832 | Tobject
(t1, _) ->
2833 if memq_warn t visited || opened_object t1 then (t, Unchanged
) else
2834 let level'
= pred_enlarge level in
2836 t :: if level'
< level then [] else filter_visited visited in
2837 let (t1'
, c) = build_subtype env
visited loops posi
level'
t1 in
2838 if c > Unchanged
then (newty (Tobject
(t1'
, ref None
)), c)
2840 | Tfield
(s, _, t1, t2) (* Always present *) ->
2841 let (t1'
, c1
) = build_subtype env
visited loops posi
level t1 in
2842 let (t2'
, c2
) = build_subtype env
visited loops posi
level t2 in
2843 let c = max c1 c2
in
2844 if c > Unchanged
then (newty (Tfield
(s, Fpresent
, t1'
, t2'
)), c)
2848 let v = newvar () in
2854 | Tsubst
_ | Tlink
_ ->
2857 let (t1'
, c) = build_subtype env
visited loops posi
level t1 in
2858 if c > Unchanged
then (newty (Tpoly
(t1'
, tl)), c)
2863 let enlarge_type env
ty =
2865 (* [level = 4] allows 2 expansions involving objects/variants *)
2866 let (ty'
, _) = build_subtype env
[] [] true 4 ty in
2869 (**** Check whether a type is a subtype of another type. ****)
2872 During the traversal, a trace of visited types is maintained. It
2873 is printed in case of error.
2874 Constraints (pairs of types that must be equals) are accumulated
2875 rather than being enforced straight. Indeed, the result would
2876 otherwise depend on the order in which these constraints are
2878 A function enforcing these constraints is returned. That way, type
2879 variables can be bound to their actual values before this function
2880 is called (see Typecore).
2881 Only well-defined abbreviations are expanded (hence the tests
2882 [generic_abbrev ...]).
2885 let subtypes = TypePairs.create
17
2887 let subtype_error env trace
=
2888 raise
(Subtype
(expand_trace env
(List.rev trace
), []))
2890 let rec subtype_rec env trace
t1 t2 cstrs
=
2893 if t1 == t2 then cstrs
else
2896 TypePairs.find subtypes (t1, t2);
2899 TypePairs.add
subtypes (t1, t2) ();
2900 match (t1.desc, t2.desc) with
2901 (Tvar
, _) | (_, Tvar
) ->
2902 (trace
, t1, t2, !univar_pairs)::cstrs
2903 | (Tarrow
(l1, t1, u1
, _), Tarrow
(l2
, t2, u2
, _)) when l1 = l2
2904 || !Clflags.classic
&& not
(is_optional
l1 || is_optional l2
) ->
2905 let cstrs = subtype_rec env
((t2, t1)::trace
) t2 t1 cstrs in
2906 subtype_rec env
((u1
, u2
)::trace
) u1 u2
cstrs
2907 | (Ttuple
tl1, Ttuple
tl2) ->
2908 subtype_list env trace
tl1 tl2 cstrs
2909 | (Tconstr
(p1
, [], _), Tconstr
(p2
, [], _)) when Path.same p1 p2
->
2911 | (Tconstr
(p1
, tl1, abbrev1
), _)
2912 when generic_abbrev env p1
&& safe_abbrev env
t1 ->
2913 subtype_rec env trace
(expand_abbrev env
t1) t2 cstrs
2914 | (_, Tconstr
(p2
, tl2, abbrev2
))
2915 when generic_abbrev env p2
&& safe_abbrev env
t2 ->
2916 subtype_rec env trace
t1 (expand_abbrev env
t2) cstrs
2917 | (Tconstr
(p1
, tl1, _), Tconstr
(p2
, tl2, _)) when Path.same p1 p2
->
2919 let decl = Env.find_type p1 env
in
2921 (fun cstrs (co
, cn
, _) (t1, t2) ->
2924 (trace
, newty2 t1.level (Ttuple
[t1]),
2925 newty2 t2.level (Ttuple
[t2]), !univar_pairs) :: cstrs
2926 else subtype_rec env
((t1, t2)::trace
) t1 t2 cstrs
2928 if cn
then subtype_rec env
((t2, t1)::trace
) t2 t1 cstrs
2930 cstrs decl.type_variance
(List.combine
tl1 tl2)
2932 (trace
, t1, t2, !univar_pairs)::cstrs
2934 | (Tobject
(f1, _), Tobject
(f2
, _))
2935 when (object_row f1).desc = Tvar
&& (object_row f2
).desc = Tvar
->
2936 (* Same row variable implies same object. *)
2937 (trace
, t1, t2, !univar_pairs)::cstrs
2938 | (Tobject
(f1, _), Tobject
(f2
, _)) ->
2939 subtype_fields env trace
f1 f2
cstrs
2940 | (Tvariant
row1, Tvariant row2
) ->
2942 subtype_row env trace
row1 row2
cstrs
2944 (trace
, t1, t2, !univar_pairs)::cstrs
2946 | (Tpoly
(u1
, []), Tpoly
(u2
, [])) ->
2947 subtype_rec env trace u1 u2
cstrs
2948 | (Tpoly
(u1
, tl1), Tpoly
(u2
,tl2)) ->
2950 enter_poly env
univar_pairs u1
tl1 u2
tl2
2951 (fun t1 t2 -> subtype_rec env trace
t1 t2 cstrs)
2953 (trace
, t1, t2, !univar_pairs)::cstrs
2956 (trace
, t1, t2, !univar_pairs)::cstrs
2959 and subtype_list env trace
tl1 tl2 cstrs =
2960 if List.length
tl1 <> List.length
tl2 then
2961 subtype_error env trace
;
2963 (fun cstrs t1 t2 -> subtype_rec env
((t1, t2)::trace
) t1 t2 cstrs)
2966 and subtype_fields env trace
ty1 ty2 cstrs =
2967 (* Assume that either rest1 or rest2 is not Tvar *)
2968 let (fields1
, rest1
) = flatten_fields ty1 in
2969 let (fields2
, rest2
) = flatten_fields ty2 in
2970 let (pairs, miss1
, miss2
) = associate_fields fields1 fields2
in
2972 if rest2
.desc = Tnil
then cstrs else
2974 subtype_rec env
((rest1
, rest2
)::trace
) rest1 rest2
cstrs
2976 (trace
, build_fields (repr ty1).level miss1 rest1
, rest2
,
2977 !univar_pairs) :: cstrs
2980 if miss2
= [] then cstrs else
2981 (trace
, rest1
, build_fields (repr ty2).level miss2
(newvar ()),
2982 !univar_pairs) :: cstrs
2985 (fun cstrs (_, k1, t1, k2, t2) ->
2986 (* Theses fields are always present *)
2987 subtype_rec env
((t1, t2)::trace
) t1 t2 cstrs)
2990 and subtype_row env trace
row1 row2
cstrs =
2991 let row1 = row_repr
row1 and row2
= row_repr row2
in
2993 merge_row_fields row1.row_fields row2
.row_fields
in
2994 let more1 = repr row1.row_more
2995 and more2
= repr row2
.row_more
in
2996 match more1.desc, more2
.desc with
2997 Tconstr
(p1
,_,_), Tconstr
(p2
,_,_) when Path.same p1 p2
->
2998 subtype_rec env
((more1,more2
)::trace
) more1 more2
cstrs
2999 | (Tvar
|Tconstr
_), (Tvar
|Tconstr
_)
3000 when row1.row_closed
&& r1 = [] ->
3002 (fun cstrs (_,f1,f2
) ->
3003 match row_field_repr
f1, row_field_repr f2
with
3004 (Rpresent None
|Reither
(true,_,_,_)), Rpresent None
->
3006 | Rpresent
(Some
t1), Rpresent
(Some
t2) ->
3007 subtype_rec env
((t1, t2)::trace
) t1 t2 cstrs
3008 | Reither
(false, t1::_, _, _), Rpresent
(Some
t2) ->
3009 subtype_rec env
((t1, t2)::trace
) t1 t2 cstrs
3010 | Rabsent
, _ -> cstrs
3014 when row1.row_closed
= row2
.row_closed
&& r1 = [] && r2
= [] ->
3016 subtype_rec env
((more1,more2
)::trace
) more1 more2
cstrs in
3018 (fun cstrs (_,f1,f2
) ->
3019 match row_field_repr
f1, row_field_repr f2
with
3020 Rpresent None
, Rpresent None
3021 | Reither
(true,[],_,_), Reither
(true,[],_,_)
3022 | Rabsent
, Rabsent
->
3024 | Rpresent
(Some
t1), Rpresent
(Some
t2)
3025 | Reither
(false,[t1],_,_), Reither
(false,[t2],_,_) ->
3026 subtype_rec env
((t1, t2)::trace
) t1 t2 cstrs
3032 let subtype env
ty1 ty2 =
3033 TypePairs.clear
subtypes;
3035 (* Build constraint set. *)
3036 let cstrs = subtype_rec env
[(ty1, ty2)] ty1 ty2 [] in
3037 TypePairs.clear
subtypes;
3038 (* Enforce constraints. *)
3041 (function (trace0
, t1, t2, pairs) ->
3042 try unify_pairs env
t1 t2 pairs with Unify trace
->
3043 raise
(Subtype
(expand_trace env
(List.rev trace0
),
3044 List.tl (List.tl trace
))))
3047 (*******************)
3049 (*******************)
3051 (* Utility for printing. The resulting type is not used in computation. *)
3052 let rec unalias_object ty =
3055 Tfield
(s, k, t1, t2) ->
3056 newty2 ty.level (Tfield
(s, k, t1, unalias_object t2))
3058 newty2 ty.level ty.desc
3062 newty2 ty.level Tvar
3072 let row = row_repr
row in
3073 let more = row.row_more
in
3075 (Tvariant
{row with row_more
= newty2 more.level more.desc})
3076 | Tobject
(ty, nm) ->
3077 newty2 ty.level (Tobject
(unalias_object ty, nm))
3079 newty2 ty.level ty.desc
3081 let unroll_abbrev id
tl ty =
3083 if (ty.desc = Tvar
) || (List.exists
(deep_occur ty) tl) then
3086 let ty'
= newty2 ty.level ty.desc in
3087 link_type
ty (newty2 ty.level (Tconstr
(Path.Pident id
, tl, ref Mnil
)));
3090 (* Return the arity (as for curried functions) of the given type. *)
3092 match (repr ty).desc with
3093 Tarrow
(_, t1, t2, _) -> 1 + arity t2
3096 (* Check whether an abbreviation expands to itself. *)
3097 let cyclic_abbrev env id
ty =
3098 let rec check_cycle seen
ty =
3101 Tconstr
(p
, tl, abbrev) ->
3102 p
= Path.Pident id
|| List.memq
ty seen
||
3104 check_cycle (ty :: seen
) (expand_abbrev env
ty)
3106 Cannot_expand
-> false
3111 in check_cycle [] ty
3113 (* Normalize a type before printing, saving... *)
3114 let rec normalize_type_rec env
ty =
3116 if ty.level >= lowest_level
then begin
3118 begin match ty.desc with
3120 let row = row_repr
row in
3121 let fields = List.map
3123 let f = row_field_repr
f in l
,
3124 match f with Reither
(b
, ty::(_::_ as tyl), m
, e) ->
3128 if List.exists
(fun ty'
-> equal env
false [ty] [ty'
]) tyl
3129 then tyl else ty::tyl)
3132 if List.length
tyl'
<= List.length
tyl then
3133 let f = Reither
(b
, List.rev
tyl'
, m
, ref None
) in
3140 List.sort
(fun (p
,_) (q
,_) -> compare p q
)
3141 (List.filter
(fun (_,fi) -> fi <> Rabsent
) fields) in
3143 ty.desc <- Tvariant
{row with row_fields
= fields}
3144 | Tobject
(fi, nm) ->
3145 begin match !nm with
3147 | Some
(n
, v :: l
) ->
3149 begin match v'
.desc with
3151 if v'
!= v then set_name
nm (Some
(n
, v'
:: l
))
3152 | Tnil
-> log_type
ty; ty.desc <- Tconstr
(n
, l
, ref Mnil
)
3153 | _ -> set_name
nm None
3156 fatal_error
"Ctype.normalize_type_rec"
3159 if fi.level < lowest_level
then () else
3160 let fields, row = flatten_fields fi in
3161 let fi'
= build_fields fi.level fields row in
3162 log_type
ty; fi.desc <- fi'
.desc
3165 iter_type_expr
(normalize_type_rec env
) ty
3168 let normalize_type env
ty =
3169 normalize_type_rec env
ty;
3173 (*************************)
3174 (* Remove dependencies *)
3175 (*************************)
3179 Variables are left unchanged. Other type nodes are duplicated, with
3180 levels set to generic level.
3181 During copying, the description of a (non-variable) node is first
3182 replaced by a link to a stub ([Tsubst (newgenvar ())]).
3183 Once the copy is made, it replaces the stub.
3184 After copying, the description of node, which was stored by
3185 [save_desc], must be put back, using [cleanup_types].
3188 let rec nondep_type_rec env id
ty =
3191 Tvar
| Tunivar
-> ty
3194 let desc = ty.desc in
3196 let ty'
= newgenvar
() in (* Stub *)
3197 ty.desc <- Tsubst
ty'
;
3199 begin match desc with
3200 | Tconstr
(p
, tl, abbrev) ->
3201 if Path.isfree id p
then
3203 Tlink
(nondep_type_rec env id
3204 (expand_abbrev env
(newty2 ty.level desc)))
3206 The [Tlink] is important. The expanded type may be a
3207 variable, or may not be completely copied yet
3208 (recursive type), so one cannot just take its
3211 with Cannot_expand
->
3215 Tconstr
(p
, List.map
(nondep_type_rec env id
) tl, ref Mnil
)
3216 | Tobject
(t1, name) ->
3217 Tobject
(nondep_type_rec env id
t1,
3218 ref (match !name with
3221 if Path.isfree id p
then None
3222 else Some
(p
, List.map
(nondep_type_rec env id
) tl)))
3224 let row = row_repr
row in
3225 let more = repr row.row_more
in
3226 (* We must substitute in a subtle way *)
3227 (* Tsubst denotes the variant itself, as the row var is unchanged *)
3228 begin match more.desc with
3230 (* This variant type has been already copied *)
3231 ty.desc <- Tsubst
ty2; (* avoid Tlink in the new type *)
3234 let static = static_row
row in
3235 (* Register new type first for recursion *)
3236 save_desc
more more.desc;
3237 more.desc <- ty.desc;
3238 let more'
= if static then newgenvar
() else more in
3239 (* Return a new copy *)
3241 copy_row
(nondep_type_rec env id
) true row true more'
in
3242 match row.row_name
with
3243 Some
(p
, tl) when Path.isfree id p
->
3244 Tvariant
{row with row_name
= None
}
3247 | _ -> copy_type_desc
(nondep_type_rec env id
) desc
3251 let nondep_type env id
ty =
3253 let ty'
= nondep_type_rec env id
ty in
3261 (* Preserve sharing inside type declarations. *)
3262 let nondep_type_decl env mid id is_covariant
decl =
3264 let params = List.map
(nondep_type_rec env mid
) decl.type_params
in
3266 { type_params
= params;
3267 type_arity
= decl.type_arity
;
3270 match decl.type_kind
with
3273 | Type_variant
(cstrs, priv
) ->
3274 Type_variant
(List.map
3275 (fun (c, tl) -> (c, List.map
(nondep_type_rec env mid
) tl))
3277 | Type_record
(lbls
, rep
, priv
) ->
3280 (fun (c, mut
, t) -> (c, mut
, nondep_type_rec env mid
t))
3283 with Not_found
when is_covariant
->
3288 match decl.type_manifest
with
3291 Some
(unroll_abbrev id
params (nondep_type_rec env mid
ty))
3292 with Not_found
when is_covariant
->
3295 type_variance
= decl.type_variance
;
3299 List.iter unmark_type
decl.type_params
;
3300 begin match decl.type_kind
with
3302 | Type_variant
(cstrs, priv
) ->
3303 List.iter
(fun (c, tl) -> List.iter unmark_type
tl) cstrs
3304 | Type_record
(lbls
, rep
, priv
) ->
3305 List.iter
(fun (c, mut
, t) -> unmark_type
t) lbls
3307 begin match decl.type_manifest
with
3309 | Some
ty -> unmark_type
ty
3316 (* Preserve sharing inside class types. *)
3317 let nondep_class_signature env id sign
=
3318 { cty_self
= nondep_type_rec env id sign
.cty_self
;
3320 Vars.map
(function (m
, v, t) -> (m
, v, nondep_type_rec env id
t))
3322 cty_concr
= sign
.cty_concr
;
3324 List.map
(fun (p
,tl) -> (p
, List.map
(nondep_type_rec env id
) tl))
3327 let rec nondep_class_type env id
=
3329 Tcty_constr
(p
, _, cty) when Path.isfree id p
->
3330 nondep_class_type env id
cty
3331 | Tcty_constr
(p
, tyl, cty) ->
3332 Tcty_constr
(p
, List.map
(nondep_type_rec env id
) tyl,
3333 nondep_class_type env id
cty)
3334 | Tcty_signature sign
->
3335 Tcty_signature
(nondep_class_signature env id sign
)
3336 | Tcty_fun
(l
, ty, cty) ->
3337 Tcty_fun
(l
, nondep_type_rec env id
ty, nondep_class_type env id
cty)
3339 let nondep_class_declaration env id
decl =
3340 assert (not
(Path.isfree id
decl.cty_path
));
3342 { cty_params
= List.map
(nondep_type_rec env id
) decl.cty_params
;
3343 cty_variance
= decl.cty_variance
;
3344 cty_type
= nondep_class_type env id
decl.cty_type
;
3345 cty_path
= decl.cty_path
;
3347 begin match decl.cty_new
with
3349 | Some
ty -> Some
(nondep_type_rec env id
ty)
3353 List.iter unmark_type
decl.cty_params
;
3354 unmark_class_type
decl.cty_type
;
3355 begin match decl.cty_new
with
3357 | Some
ty -> unmark_type
ty
3361 let nondep_cltype_declaration env id
decl =
3362 assert (not
(Path.isfree id
decl.clty_path
));
3364 { clty_params
= List.map
(nondep_type_rec env id
) decl.clty_params
;
3365 clty_variance
= decl.clty_variance
;
3366 clty_type
= nondep_class_type env id
decl.clty_type
;
3367 clty_path
= decl.clty_path
}
3370 List.iter unmark_type
decl.clty_params
;
3371 unmark_class_type
decl.clty_type
;
3374 (* collapse conjonctive types in class parameters *)
3375 let rec collapse_conj env
visited ty =
3377 if List.memq
ty visited then () else
3378 let visited = ty :: visited in
3381 let row = row_repr
row in
3384 match row_field_repr
fi with
3385 Reither
(c, t1::(_::_ as tl), m
, e) ->
3386 List.iter
(unify env
t1) tl;
3387 set_row_field
e (Reither
(c, [t1], m
, ref None
))
3391 iter_row
(collapse_conj env
visited) row
3393 iter_type_expr
(collapse_conj env
visited) ty
3395 let collapse_conj_params env
params =
3396 List.iter
(collapse_conj env
[]) params