l4/pkg/ocaml/contrib/typing/btype.ml

   1 (***********************************************************************)
   2 (*                                                                     *)
   3 (*                           Objective Caml                            *)
   4 (*                                                                     *)
   5 (* Xavier Leroy and Jerome Vouillon, projet Cristal, INRIA Rocquencourt*)
   6 (*                                                                     *)
   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.               *)
  10 (*                                                                     *)
  11 (***********************************************************************)
  12
  13 (* $Id: btype.ml 8922 2008-07-19 02:13:09Z garrigue $ *)
  14
  15 (* Basic operations on core types *)
  16
  17 open Types
  18
  19 (**** Type level management ****)
  20
  21 let generic_level = 100000000
  22
  23 (* Used to mark a type during a traversal. *)
  24 let lowest_level = 0
  25 let pivot_level = 2 * lowest_level - 1
  26     (* pivot_level - lowest_level < lowest_level *)
  27
  28 (**** Some type creators ****)
  29
  30 let new_id = ref (-1)
  31
  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
  36 (*
  37 let newmarkedvar level =
  38   incr new_id; { desc = Tvar; level = pivot_level - level; id = !new_id }
  39 let newmarkedgenvar () =
  40   incr new_id;
  41   { desc = Tvar; level = pivot_level - generic_level; id = !new_id }
  42 *)
  43
  44 (**** Representative of a type ****)
  45
  46 let rec field_kind_repr =
  47   function
  48     Fvar {contents = Some kind} -> field_kind_repr kind
  49   | kind                        -> kind
  50
  51 let rec repr =
  52   function
  53     {desc = Tlink t'} ->
  54       (*
  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
  58          unification).
  59       *)
  60       repr t'
  61   | {desc = Tfield (_, k, _, t')} when field_kind_repr k = Fabsent ->
  62       repr t'
  63   | t -> t
  64
  65 let rec commu_repr = function
  66     Clink r when !r <> Cunknown -> commu_repr !r
  67   | c -> c
  68
  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))
  76   | fi -> fi
  77
  78 let row_field_repr fi = row_field_repr_aux [] fi
  79
  80 let rec rev_concat l ll =
  81   match ll with
  82     [] -> l
  83   | l'::ll -> rev_concat (l'@l) ll
  84
  85 let rec row_repr_aux ll row =
  86   match (repr row.row_more).desc with
  87   | Tvariant row' ->
  88       let f = row.row_fields in
  89       row_repr_aux (if f = [] then ll else f::ll) row'
  90   | _ ->
  91       if ll = [] then row else
  92       {row with row_fields = rev_concat row.row_fields ll}
  93
  94 let row_repr row = row_repr_aux [] row
  95
  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
 100     | [] ->
 101         match repr row.row_more with
 102         | {desc=Tvariant row'} -> row_field tag row'
 103         | _ -> Rabsent
 104   in find row.row_fields
 105
 106 let rec row_more row =
 107   match repr row.row_more with
 108   | {desc=Tvariant row'} -> row_more row'
 109   | ty -> ty
 110
 111 let static_row row =
 112   let row = row_repr row in
 113   row.row_closed &&
 114   List.for_all
 115     (fun (_,f) -> match row_field_repr f with Reither _ -> false | _ -> true)
 116     row.row_fields
 117
 118 let hash_variant s =
 119   let accu = ref 0 in
 120   for i = 0 to String.length s - 1 do
 121     accu := 223 * !accu + Char.code s.[i]
 122   done;
 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
 127
 128 let proxy ty =
 129   let ty0 = repr ty in
 130   match ty0.desc with
 131   | Tvariant row when not (static_row row) ->
 132       row_more row
 133   | Tobject (ty, _) ->
 134       let rec proxy_obj ty =
 135         match ty.desc with
 136           Tfield (_, _, _, ty) | Tlink ty -> proxy_obj ty
 137         | Tvar | Tunivar | Tconstr _ -> ty
 138         | Tnil -> ty0
 139         | _ -> assert false
 140       in proxy_obj ty
 141   | _ -> ty0
 142
 143 (**** Utilities for fixed row private types ****)
 144
 145 let has_constr_row t =
 146   match (repr t).desc with
 147     Tobject(t,_) ->
 148       let rec check_row t =
 149         match (repr t).desc with
 150           Tfield(_,_,_,t) -> check_row t
 151         | Tconstr _ -> true
 152         | _ -> false
 153       in check_row t
 154   | Tvariant row ->
 155       (match row_more row with {desc=Tconstr _} -> true | _ -> false)
 156   | _ ->
 157       false
 158
 159 let is_row_name s =
 160   let l = String.length s in
 161   if l < 4 then false else String.sub s (l-4) 4 = "#row"
 162
 163
 164                   (**********************************)
 165                   (*  Utilities for type traversal  *)
 166                   (**********************************)
 167
 168 let rec iter_row f row =
 169   List.iter
 170     (fun (_, fi) ->
 171       match row_field_repr fi with
 172       | Rpresent(Some ty) -> f ty
 173       | Reither(_, tl, _, _) -> List.iter f tl
 174       | _ -> ())
 175     row.row_fields;
 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
 180   | _ -> assert false
 181
 182 let iter_type_expr f ty =
 183   match ty.desc with
 184     Tvar                -> ()
 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
 193   | Tnil                -> ()
 194   | Tlink ty            -> f ty
 195   | Tsubst ty           -> f ty
 196   | Tunivar             -> ()
 197   | Tpoly (ty, tyl)     -> f ty; List.iter f tyl
 198
 199 let rec iter_abbrev f = function
 200     Mnil                   -> ()
 201   | Mcons(_, _, ty, ty', rem) -> f ty; f ty'; iter_abbrev f rem
 202   | Mlink rem              -> iter_abbrev f !rem
 203
 204 let copy_row f fixed row keep more =
 205   let fields = List.map
 206       (fun (l, fi) -> l,
 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
 213             Reither(c, tl, m, e)
 214         | _ -> fi)
 215       row.row_fields in
 216   let name =
 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; }
 222
 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
 228
 229 let copy_commu c =
 230   if commu_repr c = Cok then Cok else Clink (ref Cunknown)
 231
 232 (* Since univars may be used as row variables, we need to do some
 233    encoding during substitution *)
 234 let rec norm_univar ty =
 235   match ty.desc with
 236     Tunivar | Tsubst _ -> ty
 237   | Tlink ty           -> norm_univar ty
 238   | Ttuple (ty :: _)   -> norm_univar ty
 239   | _                  -> assert false
 240
 241 let rec copy_type_desc f = function
 242     Tvar                -> Tvar
 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)
 252   | Tnil                -> Tnil
 253   | Tlink ty            -> copy_type_desc f ty.desc
 254   | Tsubst ty           -> assert false
 255   | Tunivar             -> Tunivar
 256   | Tpoly (ty, tyl)     ->
 257       let tyl = List.map (fun x -> norm_univar (f x)) tyl in
 258       Tpoly (f ty, tyl)
 259
 260
 261 (* Utilities for copying *)
 262
 263 let saved_desc = ref []
 264   (* Saved association of generic nodes with their description. *)
 265
 266 let save_desc ty desc =
 267   saved_desc := (ty, desc)::!saved_desc
 268
 269 let saved_kinds = ref [] (* duplicated kind variables *)
 270 let new_kinds = ref []   (* new kind variables *)
 271 let dup_kind r =
 272   (match !r with None -> () | Some _ -> assert false);
 273   if not (List.memq r !new_kinds) then begin
 274     saved_kinds := r :: !saved_kinds;
 275     let r' = ref None in
 276     new_kinds := r' :: !new_kinds;
 277     r := Some (Fvar r')
 278   end
 279
 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 := []
 285
 286 (* Mark a type. *)
 287 let rec mark_type ty =
 288   let ty = repr ty in
 289   if ty.level >= lowest_level then begin
 290     ty.level <- pivot_level - ty.level;
 291     iter_type_expr mark_type ty
 292   end
 293
 294 let mark_type_node ty =
 295   let ty = repr ty in
 296   if ty.level >= lowest_level then begin
 297     ty.level <- pivot_level - ty.level;
 298   end
 299
 300 let mark_type_params ty =
 301   iter_type_expr mark_type ty
 302
 303 (* Remove marks from a type. *)
 304 let rec unmark_type ty =
 305   let ty = repr ty in
 306   if ty.level < lowest_level then begin
 307     ty.level <- pivot_level - ty.level;
 308     iter_type_expr unmark_type ty
 309   end
 310
 311 let unmark_type_decl decl =
 312   List.iter unmark_type decl.type_params;
 313   begin match decl.type_kind with
 314     Type_abstract -> ()
 315   | Type_variant cstrs ->
 316       List.iter (fun (c, tl) -> List.iter unmark_type tl) cstrs
 317   | Type_record(lbls, rep) ->
 318       List.iter (fun (c, mut, t) -> unmark_type t) lbls
 319   end;
 320   begin match decl.type_manifest with
 321     None    -> ()
 322   | Some ty -> unmark_type ty
 323   end
 324
 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
 328
 329 let rec unmark_class_type =
 330   function
 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
 337
 338
 339                   (*******************************************)
 340                   (*  Memorization of abbreviation expansion *)
 341                   (*******************************************)
 342
 343 (* Search whether the expansion has been memorized. *)
 344 let rec find_expans priv p1 = function
 345     Mnil -> None
 346   | Mcons (priv', p2, ty0, ty, _)
 347     when priv' >= priv && Path.same p1 p2 -> Some ty
 348   | Mcons (_, _, _, _, rem)   -> find_expans priv p1 rem
 349   | Mlink {contents = rem} -> find_expans priv p1 rem
 350
 351 (* debug: check for cycles in abbreviation. only works with -principal
 352 let rec check_expans visited ty =
 353   let ty = repr ty in
 354   assert (not (List.memq ty visited));
 355   match ty.desc with
 356     Tconstr (path, args, abbrev) ->
 357       begin match find_expans path !abbrev with
 358         Some ty' -> check_expans (ty :: visited) ty'
 359       | None -> ()
 360       end
 361   | _ -> ()
 362 *)
 363
 364 let memo = ref []
 365         (* Contains the list of saved abbreviation expansions. *)
 366
 367 let cleanup_abbrev () =
 368         (* Remove all memorized abbreviation expansions. *)
 369   List.iter (fun abbr -> abbr := Mnil) !memo;
 370   memo := []
 371
 372 let memorize_abbrev mem priv path v v' =
 373         (* Memorize the expansion of an abbreviation. *)
 374   mem := Mcons (priv, path, v, v', !mem);
 375   (* check_expans [] v; *)
 376   memo := mem :: !memo
 377
 378 let rec forget_abbrev_rec mem path =
 379   match mem with
 380     Mnil ->
 381       assert false
 382   | Mcons (_, path', _, _, rem) when Path.same path path' ->
 383       rem
 384   | Mcons (priv, path', v, v', rem) ->
 385       Mcons (priv, path', v, v', forget_abbrev_rec rem path)
 386   | Mlink mem' ->
 387       mem' := forget_abbrev_rec !mem' path;
 388       raise Exit
 389
 390 let forget_abbrev mem path =
 391   try mem := forget_abbrev_rec !mem path with Exit -> ()
 392
 393 (* debug: check for invalid abbreviations
 394 let rec check_abbrev_rec = function
 395     Mnil -> true
 396   | Mcons (_, ty1, ty2, rem) ->
 397       repr ty1 != repr ty2
 398   | Mlink mem' ->
 399       check_abbrev_rec !mem'
 400
 401 let check_memorized_abbrevs () =
 402   List.for_all (fun mem -> check_abbrev_rec !mem) !memo
 403 *)
 404
 405                   (**********************************)
 406                   (*  Utilities for labels          *)
 407                   (**********************************)
 408
 409 let is_optional l =
 410   String.length l > 0 && l.[0] = '?'
 411
 412 let label_name l =
 413   if is_optional l then String.sub l 1 (String.length l - 1)
 414                    else l
 415
 416 let rec extract_label_aux hd l = function
 417     [] -> raise Not_found
 418   | (l',t as p) :: ls ->
 419       if label_name l' = l then (l', t, List.rev hd, ls)
 420       else extract_label_aux (p::hd) l ls
 421
 422 let extract_label l ls = extract_label_aux [] l ls
 423
 424
 425                   (**********************************)
 426                   (*  Utilities for backtracking    *)
 427                   (**********************************)
 428
 429 type change =
 430     Ctype of type_expr * type_desc
 431   | Clevel of type_expr * int
 432   | Cname of
 433       (Path.t * type_expr list) option ref * (Path.t * type_expr list) option
 434   | Crow of row_field option ref * row_field option
 435   | Ckind of field_kind option ref * field_kind option
 436   | Ccommu of commutable ref * commutable
 437   | Cuniv of type_expr option ref * type_expr option
 438
 439 let undo_change = function
 440     Ctype  (ty, desc)  -> ty.desc <- desc
 441   | Clevel (ty, level) -> ty.level <- level
 442   | Cname  (r, v) -> r := v
 443   | Crow   (r, v) -> r := v
 444   | Ckind  (r, v) -> r := v
 445   | Ccommu (r, v) -> r := v
 446   | Cuniv  (r, v) -> r := v
 447
 448 type changes =
 449     Change of change * changes ref
 450   | Unchanged
 451   | Invalid
 452
 453 type snapshot = changes ref * int
 454
 455 let trail = Weak.create 1
 456 let last_snapshot = ref 0
 457
 458 let log_change ch =
 459   match Weak.get trail 0 with None -> ()
 460   | Some r ->
 461       let r' = ref Unchanged in
 462       r := Change (ch, r');
 463       Weak.set trail 0 (Some r')
 464
 465 let log_type ty =
 466   if ty.id <= !last_snapshot then log_change (Ctype (ty, ty.desc))
 467 let link_type ty ty' = log_type ty; ty.desc <- Tlink ty'
 468   (* ; assert (check_memorized_abbrevs ()) *)
 469   (*  ; check_expans [] ty' *)
 470 let set_level ty level =
 471   if ty.id <= !last_snapshot then log_change (Clevel (ty, ty.level));
 472   ty.level <- level
 473 let set_univar rty ty =
 474   log_change (Cuniv (rty, !rty)); rty := Some ty
 475 let set_name nm v =
 476   log_change (Cname (nm, !nm)); nm := v
 477 let set_row_field e v =
 478   log_change (Crow (e, !e)); e := Some v
 479 let set_kind rk k =
 480   log_change (Ckind (rk, !rk)); rk := Some k
 481 let set_commu rc c =
 482   log_change (Ccommu (rc, !rc)); rc := c
 483
 484 let snapshot () =
 485   let old = !last_snapshot in
 486   last_snapshot := !new_id;
 487   match Weak.get trail 0 with Some r -> (r, old)
 488   | None ->
 489       let r = ref Unchanged in
 490       Weak.set trail 0 (Some r);
 491       (r, old)
 492
 493 let rec rev_log accu = function
 494     Unchanged -> accu
 495   | Invalid -> assert false
 496   | Change (ch, next) ->
 497       let d = !next in
 498       next := Invalid;
 499       rev_log (ch::accu) d
 500
 501 let backtrack (changes, old) =
 502   match !changes with
 503     Unchanged -> last_snapshot := old
 504   | Invalid -> failwith "Btype.backtrack"
 505   | Change _ as change ->
 506       cleanup_abbrev ();
 507       let backlog = rev_log [] change in
 508       List.iter undo_change backlog;
 509       changes := Unchanged;
 510       last_snapshot := old;
 511       Weak.set trail 0 (Some changes)