1 (***********************************************************************)
5 (* Xavier Leroy, 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 (* Inclusion checks for the core language *)
23 (* Inclusion between value descriptions *)
27 let value_descriptions env vd1 vd2
=
28 if Ctype.moregeneral env
true vd1
.val_type vd2
.val_type
then begin
29 match (vd1
.val_kind
, vd2
.val_kind
) with
30 (Val_prim p1
, Val_prim p2
) ->
31 if p1
= p2
then Tcoerce_none
else raise Dont_match
32 | (Val_prim p
, _
) -> Tcoerce_primitive p
33 | (_
, Val_prim p
) -> raise Dont_match
34 | (_
, _
) -> Tcoerce_none
38 (* Inclusion between "private" annotations *)
40 let private_flags priv1 priv2
=
41 match (priv1
, priv2
) with (Private
, Public
) -> false | (_
, _
) -> true
43 (* Inclusion between manifest types (particularly for private row types) *)
45 let is_absrow env ty
=
47 Tconstr
(Pident id
, _
, _
) ->
48 begin match Ctype.expand_head env ty
with
49 {desc
=Tobject _
|Tvariant _
} -> true
54 let type_manifest env ty1 params1 ty2 params2
=
55 let ty1'
= Ctype.expand_head env
ty1 and ty2'
= Ctype.expand_head env ty2
in
56 match ty1'
.desc
, ty2'
.desc
with
57 Tvariant row1
, Tvariant row2
when is_absrow env
(Btype.row_more row2
) ->
58 let row1 = Btype.row_repr
row1 and row2
= Btype.row_repr row2
in
59 Ctype.equal env
true (ty1::params1
) (row2
.row_more
::params2
) &&
60 (match row1.row_more
with {desc
=Tvar
|Tconstr _
} -> true | _
-> false) &&
62 Ctype.merge_row_fields
row1.row_fields row2
.row_fields
in
63 (not row2
.row_closed
||
64 row1.row_closed
&& Ctype.filter_row_fields
false r1 = []) &&
66 (fun (_
,f
) -> match Btype.row_field_repr f
with
67 Rabsent
| Reither _
-> true | Rpresent _
-> false)
69 let to_equal = ref (List.combine params1 params2
) in
72 match Btype.row_field_repr f1
, Btype.row_field_repr f2
with
74 (Rpresent
(Some t2
) | Reither
(false, [t2
], _
, _
)) ->
75 to_equal := (t1
,t2
) :: !to_equal; true
76 | Rpresent None
, (Rpresent None
| Reither
(true, [], _
, _
)) -> true
77 | Reither
(c1
,tl1
,_
,_
), Reither
(c2
,tl2
,_
,_
)
78 when List.length tl1
= List.length tl2
&& c1
= c2
->
79 to_equal := List.combine tl1 tl2
@ !to_equal; true
80 | Rabsent
, (Reither _
| Rabsent
) -> true
83 let tl1, tl2
= List.split
!to_equal in
84 Ctype.equal env
true tl1 tl2
85 | Tobject
(fi1
, _
), Tobject
(fi2
, _
)
86 when is_absrow env
(snd
(Ctype.flatten_fields fi2
)) ->
87 let (fields2
,rest2
) = Ctype.flatten_fields fi2
in
88 Ctype.equal env
true (ty1::params1
) (rest2
::params2
) &&
89 let (fields1
,rest1
) = Ctype.flatten_fields fi1
in
90 (match rest1
with {desc
=Tnil
|Tvar
|Tconstr _
} -> true | _
-> false) &&
91 let pairs, miss1
, miss2
= Ctype.associate_fields fields1 fields2
in
94 List.split
(List.map
(fun (_
,_
,t1
,_
,t2
) -> t1
, t2
) pairs) in
95 Ctype.equal env
true (params1
@ tl1) (params2
@ tl2
)
97 Ctype.equal env
true (ty1 :: params1
) (ty2
:: params2
)
99 (* Inclusion between type declarations *)
101 let type_declarations env id decl1 decl2
=
102 decl1
.type_arity
= decl2
.type_arity
&&
103 begin match (decl1
.type_kind
, decl2
.type_kind
) with
104 (_
, Type_abstract
) -> true
105 | (Type_variant
(cstrs1
, priv1
), Type_variant
(cstrs2
, priv2
)) ->
106 private_flags priv1 priv2
&&
108 (fun (cstr1
, arg1
) (cstr2
, arg2
) ->
112 Ctype.equal env
true (ty1::decl1
.type_params
)
113 (ty2
::decl2
.type_params
))
116 | (Type_record
(labels1
,rep1
,priv1
), Type_record
(labels2
,rep2
,priv2
)) ->
117 private_flags priv1 priv2
&&
120 (fun (lbl1
, mut1
, ty1) (lbl2
, mut2
, ty2
) ->
121 lbl1
= lbl2
&& mut1
= mut2
&&
122 Ctype.equal env
true (ty1::decl1
.type_params
)
123 (ty2
::decl2
.type_params
))
127 begin match (decl1
.type_manifest, decl2
.type_manifest) with
129 Ctype.equal env
true decl1
.type_params decl2
.type_params
130 | (Some
ty1, Some ty2
) ->
131 type_manifest env
ty1 decl1
.type_params ty2 decl2
.type_params
132 | (None
, Some ty2
) ->
134 Btype.newgenty
(Tconstr
(Pident id
, decl2
.type_params
, ref Mnil
))
136 Ctype.equal env
true decl1
.type_params decl2
.type_params
&&
137 Ctype.equal env
false [ty1] [ty2
]
139 if match decl2
.type_kind
with
140 | Type_record
(_
,_
,priv
) | Type_variant
(_
,priv
) -> priv
= Private
142 match decl2
.type_manifest with None
-> true
143 | Some ty
-> Btype.has_constr_row
(Ctype.expand_head env ty
)
146 (fun (co1
,cn1
,ct1
) (co2
,cn2
,ct2
) -> (not co1
|| co2
) && (not cn1
|| cn2
))
147 decl1
.type_variance decl2
.type_variance
150 (* Inclusion between exception declarations *)
152 let exception_declarations env ed1 ed2
=
153 Misc.for_all2
(fun ty1 ty2
-> Ctype.equal env
false [ty1] [ty2
]) ed1 ed2
155 (* Inclusion between class types *)
156 let encode_val (mut
, ty
) rem
=
158 Asttypes.Mutable
-> Predef.type_unit
159 | Asttypes.Immutable
-> Btype.newgenty Tvar
163 let meths meths1 meths2
=
165 (fun nam t2
(ml1
, ml2
) ->
167 Meths.find nam meths1
:: ml1
174 let vars vars1 vars2
=
176 (fun lab v2
(vl1
, vl2
) ->
178 encode_val (Vars.find lab vars1
) vl1