-
Notifications
You must be signed in to change notification settings - Fork 125
/
qmlTypesCompare.ml
executable file
·298 lines (263 loc) · 11.9 KB
/
qmlTypesCompare.ml
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
(*
Copyright © 2011 MLstate
This file is part of OPA.
OPA is free software: you can redistribute it and/or modify it under the
terms of the GNU Affero General Public License, version 3, as published by
the Free Software Foundation.
OPA is distributed in the hope that it will be useful, but WITHOUT ANY
WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS
FOR A PARTICULAR PURPOSE. See the GNU Affero General Public License for
more details.
You should have received a copy of the GNU Affero General Public License
along with OPA. If not, see <http://www.gnu.org/licenses/>.
*)
(*
Author: 2011, François Pessaux <francois.pessaux@mlstate.com>
*)
(**
Strongly mapped on hmx_Compare.ml of the old HMX typechecker.
This module implements comparison on QML types with the semantics that
old HMX typechecker had when it first transformed QML types into HMX types
then compared the HMX types.
The idea is to remove the bridge between QML and HMX primitives since HMX
is not used anymore. However, QML still used some parts of HMX functions
for various things. That's the reason why this module exists.
*)
(* depends *)
module List = BaseList
(* shorthands *)
module Q = QmlAst
module TyPairSet : (BaseSetSig.S with type elt = QmlAst.ty * QmlAst.ty) =
BaseSet.Make (
struct
type t = QmlAst.ty * QmlAst.ty
let compare = Pervasives.compare
end
)
(**
sort the list of type variables [bvs] bounds in a TypeForall
according to the apparition order in the quantified type [t]
*)
(* TODO : extend to row and column variables *)
let sort_bound_vars env bvs t =
let rec aux memo (sbvs, bvs) t =
match t with
| Q.TypeSumSugar _ ->
(* They should have all disappeared. *)
assert false
| Q.TypeConst _ -> (sbvs, bvs)
| Q.TypeVar v ->
if List.mem v bvs then ((v :: sbvs), (List.remove_first v bvs))
else (sbvs, bvs)
| Q.TypeArrow (lt, u) ->
aux memo (List.fold_left (aux memo) (sbvs, bvs) lt) u
| Q.TypeRecord (Q.TyRow (fields, _)) -> aux_fields memo (sbvs, bvs) fields
| Q.TypeSum (Q.TyCol (l_fields, _)) ->
List.fold_left (aux_fields memo) (sbvs, bvs) l_fields
| Q.TypeName (lt, tn) ->
let (tsc, _) =
QmlTypes.Env.TypeIdent.find ~visibility_applies: true tn env in
let acc =
if List.mem t memo then (sbvs, bvs)
else
let t' = QmlTypes.Scheme.specialize ~typeident: tn ~ty: lt tsc in
aux (t :: memo) (sbvs, bvs) t' in
(* explore phantom types, because they don't appear in the body *)
let (vars, _, _) = QmlGenericScheme.export_unsafe tsc in
let (typevars, _, _) = QmlTypeVars.FreeVars.export_as_lists vars in
let count_t_c_freevars t _c = QmlTypes.freevars_of_ty t in
let phantomvars =
QmlGenericScheme.phantomvars_with_cache count_t_c_freevars tsc in
let fold_fun acc v t =
if QmlTypeVars.FreeVars.mem_typevar v phantomvars then aux memo acc t
else acc in
List.fold_left2 fold_fun acc typevars lt
| Q.TypeAbstract -> (sbvs, bvs)
| Q.TypeForall (_, _, _, t) -> aux memo (sbvs, bvs) t
and aux_fields memo (sbvs, bvs) fields =
let lt = List.map snd fields in
List.fold_left (aux memo) (sbvs, bvs) lt in
(* Note that it is legal to have variable not "seen", i.e. variable remaining
in [bvs] and not sent to [sbvs] after sorting because when a type name is
defined as an abstract type, since this latter doesn't have parameter,
parameters of the type name do not appear in the instantiation hence are
not "seen". As a result, they in effect are not removed from the list [bvs]
and not added in the list [sbvs]. *)
let (sbvs, _) = aux [] ([], bvs) t in
List.rev sbvs
let sort_row_fields fields =
List.sort (fun (n1, _) (n2, _) -> String.compare n1 n2) fields
let sort_col_cases (Q.TyCol (cases, ending)) =
(* First, for each case, sort the fields of the row forming the case. *)
let cases' = List.map sort_row_fields cases in
(* Now, sort each case according to the fields it has. *)
let cases'' =
List.sort
(fun case1 case2 ->
List.make_compare
(fun (n1, _) (n2, _) -> String.compare n1 n2) case1 case2)
cases' in
QmlAst.TyCol (cases'', ending)
let rec test_tys_eq env ?(bound_vars=[]) memo t1 t2 =
let call_aux ?(bound_vars=bound_vars) = test_tys_eq env ~bound_vars memo in
let is_bound v = List.mem v bound_vars in
if t1 == t2 then true (* speedup *) else
match t1, t2 with
| ((Q.TypeConst c), (Q.TypeConst d)) -> c = d
| ((Q.TypeVar v1), (Q.TypeVar v2)) when is_bound v1 && not (is_bound v2) ->
false
| ((Q.TypeVar v1), (Q.TypeVar v2)) when not (is_bound v1) && is_bound v2 ->
false
| ((Q.TypeVar v1), (Q.TypeVar v2)) -> v1 = v2
| ((Q.TypeArrow (lt, t)), (Q.TypeArrow (lu, u))) ->
((List.length lt) = (List.length lu)) &&
(List.for_all2 (call_aux ~bound_vars) lt lu) &&
(call_aux ~bound_vars t u)
| ((Q.TypeSum ts), (Q.TypeSum us)) -> cmp_col env memo ts us
| ((Q.TypeRecord rx), (Q.TypeRecord ry)) -> cmp_row env memo rx ry
| (Q.TypeRecord (Q.TyRow (tfs, trv))), (Q.TypeSum (Q.TyCol (ufs, ucv))) -> (
match trv with
| Some _ -> false
| None ->
match ucv with
| Some _ -> false
| None ->
(* No row/column variables -> compare fields *)
(match ufs with
| [ one ] ->
(* To be "equal", the sum must have only 1 case. *)
sort_and_cmp_fields env memo tfs one
| _ -> false)
)
| ((Q.TypeSum _), (Q.TypeRecord _)) -> call_aux ~bound_vars t2 t1
| ((Q.TypeName (ts, tn)), (Q.TypeName (us, un))) ->
if TyPairSet.mem (t1, t2) memo then true (* already seen, assumed equal *)
else (
let memo = TyPairSet.add (t1, t2) (TyPairSet.add (t2, t1) memo) in
let (tn, (te, _)) =
QmlTypes.Env.TypeIdent.findi ~visibility_applies: true tn env in
let (un, (ue, _)) =
QmlTypes.Env.TypeIdent.findi ~visibility_applies: true un env in
(* First, perform a test ensuring that both types have the same names
and the same arguments (by induction, they hence will be the
same). *)
let are_equal_by_name =
(QmlAst.TypeIdent.equal tn un) &&
((List.length ts) = (List.length us)) &&
(List.for_all2 (call_aux ~bound_vars) ts us) in
(* Types are equal just by their name and inductively by their
argument, then we are done, test is true. *)
if are_equal_by_name then true
else (
(* Ok, we are in the case where the 2 types are not equal by names.
This means that they have different name and/or different
arguments. *)
let t = QmlTypes.Scheme.specialize ~typeident: tn ~ty: ts te in
let u = QmlTypes.Scheme.specialize ~typeident: un ~ty: us ue in
(* If these types are abstract, then they have no more internal
representation (i.e. they are not abbreviations that could point on
a same representation, and they don't have any own structure) and
hence they are *different*. *)
if (t = QmlAst.TypeAbstract) && (u = QmlAst.TypeAbstract) then false
else test_tys_eq env ~bound_vars memo t u
)
)
| ((Q.TypeForall _), _) | (_, (Q.TypeForall _)) ->
(* let env_vars = env.Hmx_env.freevars_of_idents in *)
let t = (* generalize_in_type env_vars *) t1 in
let u = (* generalize_in_type env_vars *) t2 in
let res = (
match (t, u) with
| Q.TypeForall (t_bvs, t_row_vars, t_col_vars, t),
Q.TypeForall (u_bvs, _, _, u) ->
(* TODO : comparison is not correct !!! *)
(* quantification over row and column variables is not handled *)
let t_bvs = sort_bound_vars env t_bvs t in
let u_bvs = sort_bound_vars env u_bvs u in
if (List.length t_bvs) <> (List.length u_bvs) then false
else (
(* At this point, we are sure that the lists of quantified vars
are the same length. So we can safely transform the type t
into a pseudo scheme, call QmlTypes.instantiate on it with
a fake type ident since lists of quantified vars being the
same length, we won't get an error, so the fake ident won't
re-spring. *)
let fake_ident =
QmlAst.TypeIdent.of_string "__icmpty_broken_if_seen " in
let fake_quantif =
QmlTypeVars.FreeVars.add_list
(t_bvs, t_row_vars, t_col_vars) QmlTypeVars.FreeVars.empty in
let fake_sch = QmlGenericScheme.import fake_quantif t () in
let fake_ml_vars = List.map (fun v -> QmlAst.TypeVar v) t_bvs in
let fake_row_vars =
List.map (fun v -> QmlAst.TyRow ([], (Some v))) t_row_vars in
(* Instantiate the pseudo scheme built from the body of t.
Instantiation is done by replacing its variables by those of
u. *)
let t =
QmlTypes.Scheme.specialize
~typeident: fake_ident ~ty: fake_ml_vars
~ty_row: fake_row_vars fake_sch in
call_aux ~bound_vars: (t_bvs @ bound_vars) t u
)
| ((Q.TypeForall _), _) | (_, (Q.TypeForall _)) -> false
| _ -> assert false (* at least one of them should be a TypeForall *)
) in
res
| ((Q.TypeName (ts, tn)), u) ->
(* beware of type 'a nil = {nil:unit}, then int nil = float nil *)
if TyPairSet.mem (t1, t2) memo then false
else (
let memo = TyPairSet.add (t1, t2) memo in
let (tn, (te, _)) =
QmlTypes.Env.TypeIdent.findi ~visibility_applies: true tn env in
let t = QmlTypes.Scheme.specialize ~typeident: tn ~ty: ts te in
if t = QmlAst.TypeAbstract then false
else test_tys_eq env memo t u
)
| (_, (Q.TypeName (_, _))) -> call_aux ~bound_vars t2 t1
| (Q.TypeAbstract, _) | (_, Q.TypeAbstract) -> false
| (_, _) ->
(* Different constructors or not matching extern abstract type:
fall back on Pervasives' comparison *)
t1 = t2
and sort_and_cmp_fields env memo tfs ufs =
let cmp_field (tfn, tft) (ufn, uft) =
(tfn = ufn) && (test_tys_eq env memo tft uft) in
(* First, compare lists lengths. *)
if (List.length tfs) <> (List.length ufs) then false
else (
(* Sort the fields by name. *)
let tfs' = sort_row_fields tfs in
let ufs' = sort_row_fields ufs in
List.for_all2 cmp_field tfs' ufs'
)
(* Fields will be sorted by name by calling [sort_and_cmp_fields]. No need
to sort them in this function. *)
and cmp_row env memo (Q.TyRow (tfs, tv)) (Q.TyRow (ufs, uv)) =
let row_var_eq =
(match (tv, uv) with
| (None, None) -> true
| (None, (Some _)) | ((Some _), None) -> false
| ((Some v1), (Some v2)) -> (QmlAst.RowVar.equal v1 v2)) in
row_var_eq && (sort_and_cmp_fields env memo tfs ufs)
(* Since to sort cases, we need to sort fields of each row forming a case,
to avoid sorting several times, we don't use [cmp_row] and
[sort_and_cmp_fields] and directly sort the whole column in one shot here. *)
and cmp_col env memo (Q.TyCol (_tfs, tv) as tcol) (Q.TyCol (_ufs, uv) as ucol) =
let col_var_eq =
(match (tv, uv) with
| (None, None) -> true
| (None, (Some _)) | ((Some _), None) -> false
| ((Some v1), (Some v2)) -> QmlAst.ColVar.equal v1 v2) in
if not col_var_eq then false
else (
(* Sort the cases. *)
let tcol = sort_col_cases tcol in
let ucol = sort_col_cases ucol in
let ts = Q.column_to_records tcol in
let us = Q.column_to_records ucol in
((List.length ts) = (List.length us)) &&
(List.for_all2 (test_tys_eq env memo) ts us)
)
let equal_ty env t u = test_tys_eq env TyPairSet.empty t u