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 (* Basic operations on core types *)
19 (**** Type level management ****)
21 let generic_level = 100000000
23 (* Used to mark a type during a traversal. *)
25 let pivot_level = 2 * lowest_level - 1
26 (* pivot_level - lowest_level < lowest_level *)
28 (**** Some type creators ****)
32 let newty2 level desc
=
33 incr
new_id; { desc
= desc
; level
= level
; id
= !new_id }
34 let newgenty desc
= newty2 generic_level desc
35 let newgenvar () = newgenty Tvar
37 let newmarkedvar level =
38 incr new_id; { desc = Tvar; level = pivot_level - level; id = !new_id }
39 let newmarkedgenvar () =
41 { desc = Tvar; level = pivot_level - generic_level; id = !new_id }
44 (**** Representative of a type ****)
46 let rec field_kind_repr =
48 Fvar
{contents
= Some kind
} -> field_kind_repr kind
55 We do no path compression. Path compression does not seem to
56 improve notably efficiency, and it prevents from changing a
57 [Tlink] into another type (for instance, for undoing a
61 | {desc
= Tfield
(_
, k
, _
, t'
)} when field_kind_repr k
= Fabsent
->
65 let rec commu_repr = function
66 Clink r
when !r
<> Cunknown
-> commu_repr !r
69 let rec row_field_repr_aux tl
= function
70 Reither
(_
, tl'
, _
, {contents
= Some fi
}) ->
71 row_field_repr_aux (tl
@tl'
) fi
72 | Reither
(c
, tl'
, m
, r
) ->
73 Reither
(c
, tl
@tl'
, m
, r
)
74 | Rpresent
(Some _
) when tl
<> [] ->
75 Rpresent
(Some
(List.hd tl
))
78 let row_field_repr fi
= row_field_repr_aux [] fi
80 let rec rev_concat l ll
=
83 | l'
::ll
-> rev_concat (l'
@l
) ll
85 let rec row_repr_aux ll row
=
86 match (repr row
.row_more
).desc
with
88 let f = row
.row_fields
in
89 row_repr_aux (if f = [] then ll
else f::ll
) row'
91 if ll
= [] then row
else
92 {row
with row_fields
= rev_concat row
.row_fields ll
}
94 let row_repr row
= row_repr_aux [] row
96 let rec row_field tag row
=
97 let rec find = function
98 | (tag'
,f) :: fields
->
99 if tag
= tag'
then row_field_repr f else find fields
101 match repr row
.row_more
with
102 | {desc
=Tvariant row'
} -> row_field tag row'
104 in find row
.row_fields
106 let rec row_more row
=
107 match repr row
.row_more with
108 | {desc
=Tvariant row'
} -> row_more row'
112 let row = row_repr row in
115 (fun (_
,f) -> match row_field_repr f with Reither _
-> false | _
-> true)
120 for i
= 0 to String.length s
- 1 do
121 accu := 223 * !accu + Char.code s
.[i
]
123 (* reduce to 31 bits *)
124 accu := !accu land (1 lsl 31 - 1);
125 (* make it signed for 64 bits architectures *)
126 if !accu > 0x3FFFFFFF then !accu - (1 lsl 31) else !accu
131 | Tvariant
row when not
(static_row row) ->
134 let rec proxy_obj ty
=
136 Tfield
(_
, _
, _
, ty
) | Tlink ty
-> proxy_obj ty
137 | Tvar
| Tunivar
| Tconstr _
-> ty
143 (**** Utilities for private types ****)
145 let has_constr_row t
=
146 match (repr t
).desc
with
148 let rec check_row t
=
149 match (repr t
).desc
with
150 Tfield
(_
,_
,_
,t
) -> check_row t
155 (match row_more row with {desc
=Tconstr _
} -> true | _
-> false)
160 let l = String.length s
in
161 if l < 4 then false else String.sub s
(l-4) 4 = "#row"
164 (**********************************)
165 (* Utilities for type traversal *)
166 (**********************************)
168 let rec iter_row f row =
171 match row_field_repr fi
with
172 | Rpresent
(Some ty
) -> f ty
173 | Reither
(_
, tl
, _
, _
) -> List.iter
f tl
176 match (repr row.row_more).desc
with
177 Tvariant
row -> iter_row f row
178 | Tvar
| Tunivar
| Tsubst _
| Tconstr _
->
179 Misc.may
(fun (_
,l) -> List.iter
f l) row.row_name
182 let iter_type_expr f ty
=
185 | Tarrow
(_
, ty1
, ty2
, _
) -> f ty1
; f ty2
186 | Ttuple
l -> List.iter
f l
187 | Tconstr
(_
, l, _
) -> List.iter
f l
188 | Tobject
(ty
, {contents
= Some
(_
, p
)})
189 -> f ty
; List.iter
f p
190 | Tobject
(ty
, _
) -> f ty
191 | Tvariant
row -> iter_row f row; f (row_more row)
192 | Tfield
(_
, _
, ty1
, ty2
) -> f ty1
; f ty2
197 | Tpoly
(ty
, tyl
) -> f ty
; List.iter
f tyl
199 let rec iter_abbrev f = function
201 | Mcons
(_
, ty
, ty'
, rem
) -> f ty
; f ty'
; iter_abbrev f rem
202 | Mlink rem
-> iter_abbrev f !rem
204 let copy_row f fixed
row keep more
=
205 let fields = List.map
207 match row_field_repr fi
with
208 | Rpresent
(Some ty
) -> Rpresent
(Some
(f ty
))
209 | Reither
(c
, tl
, m
, e
) ->
210 let e = if keep
then e else ref None
in
211 let m = if row.row_fixed
then fixed
else m in
212 let tl = List.map
f tl in
217 match row.row_name
with None
-> None
218 | Some
(path
, tl) -> Some
(path
, List.map
f tl) in
219 { row_fields
= fields; row_more = more
;
220 row_bound
= (); row_fixed
= row.row_fixed
&& fixed
;
221 row_closed
= row.row_closed
; row_name
= name; }
223 let rec copy_kind = function
224 Fvar
{contents
= Some k
} -> copy_kind k
225 | Fvar _
-> Fvar
(ref None
)
226 | Fpresent
-> Fpresent
227 | Fabsent
-> assert false
230 if commu_repr c
= Cok
then Cok
else Clink
(ref Cunknown
)
232 (* Since univars may be used as row variables, we need to do some
233 encoding during substitution *)
234 let rec norm_univar ty
=
236 Tunivar
| Tsubst _
-> ty
237 | Tlink ty
-> norm_univar ty
238 | Ttuple
(ty
:: _
) -> norm_univar ty
241 let rec copy_type_desc f = function
243 | Tarrow
(p
, ty1
, ty2
, c
)-> Tarrow
(p
, f ty1
, f ty2
, copy_commu c
)
244 | Ttuple
l -> Ttuple
(List.map
f l)
245 | Tconstr
(p
, l, _
) -> Tconstr
(p
, List.map
f l, ref Mnil
)
246 | Tobject
(ty
, {contents
= Some
(p
, tl)})
247 -> Tobject
(f ty
, ref (Some
(p
, List.map
f tl)))
248 | Tobject
(ty
, _
) -> Tobject
(f ty
, ref None
)
249 | Tvariant
row -> assert false (* too ambiguous *)
250 | Tfield
(p
, k
, ty1
, ty2
) -> (* the kind is kept shared *)
251 Tfield
(p
, field_kind_repr k
, f ty1
, f ty2
)
253 | Tlink ty
-> copy_type_desc f ty
.desc
254 | Tsubst ty
-> assert false
257 let tyl = List.map
(fun x
-> norm_univar (f x
)) tyl in
261 (* Utilities for copying *)
263 let saved_desc = ref []
264 (* Saved association of generic nodes with their description. *)
266 let save_desc ty desc
=
267 saved_desc := (ty
, desc
)::!saved_desc
269 let saved_kinds = ref [] (* duplicated kind variables *)
270 let new_kinds = ref [] (* new kind variables *)
272 (match !r
with None
-> () | Some _
-> assert false);
273 if not
(List.memq r
!new_kinds) then begin
274 saved_kinds := r
:: !saved_kinds;
276 new_kinds := r'
:: !new_kinds;
280 (* Restored type descriptions. *)
281 let cleanup_types () =
282 List.iter
(fun (ty
, desc
) -> ty
.desc
<- desc
) !saved_desc;
283 List.iter
(fun r -> r := None
) !saved_kinds;
284 saved_desc := []; saved_kinds := []; new_kinds := []
287 let rec mark_type ty
=
289 if ty.level
>= lowest_level then begin
290 ty.level
<- pivot_level - ty.level
;
291 iter_type_expr mark_type ty
294 let mark_type_node ty =
296 if ty.level
>= lowest_level then begin
297 ty.level
<- pivot_level - ty.level
;
300 let mark_type_params ty =
301 iter_type_expr mark_type ty
303 (* Remove marks from a type. *)
304 let rec unmark_type ty =
306 if ty.level
< lowest_level then begin
307 ty.level
<- pivot_level - ty.level
;
308 iter_type_expr unmark_type ty
311 let unmark_type_decl decl
=
312 List.iter
unmark_type decl
.type_params
;
313 begin match decl
.type_kind
with
315 | Type_variant
(cstrs
, priv
) ->
316 List.iter
(fun (c
, tl) -> List.iter
unmark_type tl) cstrs
317 | Type_record
(lbls
, rep
, priv
) ->
318 List.iter
(fun (c
, mut
, t
) -> unmark_type t
) lbls
320 begin match decl
.type_manifest
with
322 | Some
ty -> unmark_type ty
325 let unmark_class_signature sign
=
326 unmark_type sign
.cty_self
;
327 Vars.iter
(fun l (m, v
, t
) -> unmark_type t
) sign
.cty_vars
329 let rec unmark_class_type =
331 Tcty_constr
(p
, tyl, cty
) ->
332 List.iter
unmark_type tyl; unmark_class_type cty
333 | Tcty_signature sign
->
334 unmark_class_signature sign
335 | Tcty_fun
(_
, ty, cty
) ->
336 unmark_type ty; unmark_class_type cty
339 (*******************************************)
340 (* Memorization of abbreviation expansion *)
341 (*******************************************)
343 (* Search whether the expansion has been memorized. *)
344 let rec find_expans p1
= function
346 | Mcons
(p2
, ty0, ty, _
) when Path.same p1 p2
-> Some
ty
347 | Mcons
(_
, _
, _
, rem
) -> find_expans p1 rem
348 | Mlink
{contents
= rem
} -> find_expans p1 rem
350 (* debug: check for cycles in abbreviation. only works with -principal
351 let rec check_expans visited ty =
353 assert (not (List.memq ty visited));
355 Tconstr (path, args, abbrev) ->
356 begin match find_expans path !abbrev with
357 Some ty' -> check_expans (ty :: visited) ty'
364 (* Contains the list of saved abbreviation expansions. *)
366 let cleanup_abbrev () =
367 (* Remove all memorized abbreviation expansions. *)
368 List.iter
(fun abbr
-> abbr
:= Mnil
) !memo;
371 let memorize_abbrev mem path v v'
=
372 (* Memorize the expansion of an abbreviation. *)
373 mem
:= Mcons
(path
, v
, v'
, !mem
);
374 (* check_expans [] v; *)
377 let rec forget_abbrev_rec mem path
=
381 | Mcons
(path'
, _
, _
, rem
) when Path.same path path'
->
383 | Mcons
(path'
, v
, v'
, rem
) ->
384 Mcons
(path'
, v
, v'
, forget_abbrev_rec rem path
)
386 mem'
:= forget_abbrev_rec !mem' path
;
389 let forget_abbrev mem path
=
390 try mem
:= forget_abbrev_rec !mem path
with Exit
-> ()
392 (* debug: check for invalid abbreviations
393 let rec check_abbrev_rec = function
395 | Mcons (_, ty1, ty2, rem) ->
398 check_abbrev_rec !mem'
400 let check_memorized_abbrevs () =
401 List.for_all (fun mem -> check_abbrev_rec !mem) !memo
404 (**********************************)
405 (* Utilities for labels *)
406 (**********************************)
409 String.length
l > 0 && l.[0] = '?'
412 if is_optional l then String.sub
l 1 (String.length
l - 1)
415 let rec extract_label_aux hd
l = function
416 [] -> raise Not_found
417 | (l'
,t
as p
) :: ls
->
418 if label_name l'
= l then (l'
, t
, List.rev hd
, ls
)
419 else extract_label_aux (p
::hd
) l ls
421 let extract_label l ls
= extract_label_aux [] l ls
424 (**********************************)
425 (* Utilities for backtracking *)
426 (**********************************)
429 Ctype
of type_expr
* type_desc
430 | Clevel
of type_expr
* int
432 (Path.t
* type_expr list
) option ref * (Path.t
* type_expr list
) option
433 | Crow
of row_field option ref * row_field option
434 | Ckind
of field_kind
option ref * field_kind
option
435 | Ccommu
of commutable
ref * commutable
436 | Cuniv
of type_expr
option ref * type_expr
option
438 let undo_change = function
439 Ctype
(ty, desc
) -> ty.desc
<- desc
440 | Clevel
(ty, level
) -> ty.level
<- level
441 | Cname
(r, v
) -> r := v
442 | Crow
(r, v
) -> r := v
443 | Ckind
(r, v
) -> r := v
444 | Ccommu
(r, v
) -> r := v
445 | Cuniv
(r, v
) -> r := v
448 Change
of change
* changes
ref
452 type snapshot
= changes
ref * int
454 let trail = Weak.create
1
455 let last_snapshot = ref 0
458 match Weak.get
trail 0 with None
-> ()
460 let r'
= ref Unchanged
in
461 r := Change
(ch
, r'
);
462 Weak.set
trail 0 (Some
r'
)
465 if ty.id
<= !last_snapshot then log_change (Ctype
(ty, ty.desc
))
466 let link_type ty ty'
= log_type ty; ty.desc
<- Tlink
ty'
467 (* ; assert (check_memorized_abbrevs ()) *)
468 (* ; check_expans [] ty' *)
469 let set_level ty level
=
470 if ty.id
<= !last_snapshot then log_change (Clevel
(ty, ty.level
));
472 let set_univar rty
ty =
473 log_change (Cuniv
(rty
, !rty
)); rty
:= Some
ty
475 log_change (Cname
(nm
, !nm
)); nm
:= v
476 let set_row_field e v
=
477 log_change (Crow
(e, !e)); e := Some v
479 log_change (Ckind
(rk
, !rk
)); rk
:= Some k
481 log_change (Ccommu
(rc
, !rc
)); rc
:= c
484 let old = !last_snapshot in
485 last_snapshot := !new_id;
486 match Weak.get
trail 0 with Some
r -> (r, old)
488 let r = ref Unchanged
in
489 Weak.set
trail 0 (Some
r);
492 let rec rev_log accu = function
494 | Invalid
-> assert false
495 | Change
(ch
, next
) ->
500 let backtrack (changes
, old) =
502 Unchanged
-> last_snapshot := old
503 | Invalid
-> failwith
"Btype.backtrack"
504 | Change _
as change
->
506 let backlog = rev_log [] change
in
507 List.iter
undo_change backlog;
508 changes
:= Unchanged
;
509 last_snapshot := old;
510 Weak.set
trail 0 (Some changes
)