1995-08-09 08:06:35 -07:00
|
|
|
(***********************************************************************)
|
|
|
|
(* *)
|
1996-04-30 07:53:58 -07:00
|
|
|
(* Objective Caml *)
|
1995-08-09 08:06:35 -07:00
|
|
|
(* *)
|
|
|
|
(* Xavier Leroy, projet Cristal, INRIA Rocquencourt *)
|
|
|
|
(* *)
|
1996-04-30 07:53:58 -07:00
|
|
|
(* Copyright 1996 Institut National de Recherche en Informatique et *)
|
1999-11-17 10:59:06 -08:00
|
|
|
(* en Automatique. All rights reserved. This file is distributed *)
|
|
|
|
(* under the terms of the Q Public License version 1.0. *)
|
1995-08-09 08:06:35 -07:00
|
|
|
(* *)
|
|
|
|
(***********************************************************************)
|
|
|
|
|
|
|
|
(* $Id$ *)
|
|
|
|
|
2000-03-13 08:49:01 -08:00
|
|
|
open Format
|
1995-05-04 03:15:53 -07:00
|
|
|
|
2004-01-04 06:32:34 -08:00
|
|
|
type t = { stamp: int; name: string; mutable flags: int }
|
|
|
|
|
|
|
|
let global_flag = 1
|
|
|
|
let predef_exn_flag = 2
|
1995-05-04 03:15:53 -07:00
|
|
|
|
|
|
|
(* A stamp of 0 denotes a persistent identifier *)
|
|
|
|
|
|
|
|
let currentstamp = ref 0
|
|
|
|
|
1996-04-22 04:15:41 -07:00
|
|
|
let create s =
|
1995-05-04 03:15:53 -07:00
|
|
|
incr currentstamp;
|
2004-01-04 06:32:34 -08:00
|
|
|
{ name = s; stamp = !currentstamp; flags = 0 }
|
|
|
|
|
|
|
|
let create_predef_exn s =
|
|
|
|
incr currentstamp;
|
|
|
|
{ name = s; stamp = !currentstamp; flags = predef_exn_flag }
|
1995-05-04 03:15:53 -07:00
|
|
|
|
1996-04-22 04:15:41 -07:00
|
|
|
let create_persistent s =
|
2004-01-04 06:32:34 -08:00
|
|
|
{ name = s; stamp = 0; flags = global_flag }
|
1995-05-04 03:15:53 -07:00
|
|
|
|
2000-05-15 23:27:44 -07:00
|
|
|
let rename i =
|
|
|
|
incr currentstamp;
|
|
|
|
{ i with stamp = !currentstamp }
|
|
|
|
|
1995-05-04 03:15:53 -07:00
|
|
|
let name i = i.name
|
|
|
|
|
2004-01-04 06:32:34 -08:00
|
|
|
let stamp i = i.stamp
|
|
|
|
|
1995-07-02 09:50:08 -07:00
|
|
|
let unique_name i = i.name ^ "_" ^ string_of_int i.stamp
|
|
|
|
|
2003-05-12 02:09:16 -07:00
|
|
|
let unique_toplevel_name i = i.name ^ "/" ^ string_of_int i.stamp
|
|
|
|
|
1995-05-04 03:15:53 -07:00
|
|
|
let persistent i = (i.stamp = 0)
|
|
|
|
|
|
|
|
let equal i1 i2 = i1.name = i2.name
|
|
|
|
|
|
|
|
let same i1 i2 = i1 = i2
|
|
|
|
(* Possibly more efficient version (with a real compiler, at least):
|
|
|
|
if i1.stamp <> 0
|
|
|
|
then i1.stamp = i2.stamp
|
2000-12-28 05:07:42 -08:00
|
|
|
else i2.stamp = 0 && i1.name = i2.name *)
|
1995-05-04 03:15:53 -07:00
|
|
|
|
1996-07-15 09:35:35 -07:00
|
|
|
let binding_time i = i.stamp
|
|
|
|
|
|
|
|
let current_time() = !currentstamp
|
1998-11-11 08:58:05 -08:00
|
|
|
let set_current_time t = currentstamp := max !currentstamp t
|
1996-07-15 09:35:35 -07:00
|
|
|
|
2003-05-12 02:34:05 -07:00
|
|
|
let reinit_level = ref (-1)
|
|
|
|
|
|
|
|
let reinit () =
|
|
|
|
if !reinit_level < 0
|
|
|
|
then reinit_level := !currentstamp
|
|
|
|
else currentstamp := !reinit_level
|
|
|
|
|
1995-05-04 03:15:53 -07:00
|
|
|
let hide i =
|
2000-05-15 23:27:44 -07:00
|
|
|
{ i with stamp = -1 }
|
1995-05-04 03:15:53 -07:00
|
|
|
|
|
|
|
let make_global i =
|
2004-01-04 06:32:34 -08:00
|
|
|
i.flags <- i.flags lor global_flag
|
1995-05-04 03:15:53 -07:00
|
|
|
|
|
|
|
let global i =
|
2004-01-04 06:32:34 -08:00
|
|
|
(i.flags land global_flag) <> 0
|
|
|
|
|
|
|
|
let is_predef_exn i =
|
|
|
|
(i.flags land predef_exn_flag) <> 0
|
1995-05-04 03:15:53 -07:00
|
|
|
|
2000-03-13 08:49:01 -08:00
|
|
|
let print ppf i =
|
1995-05-04 03:15:53 -07:00
|
|
|
match i.stamp with
|
2000-03-13 08:49:01 -08:00
|
|
|
| 0 -> fprintf ppf "%s!" i.name
|
|
|
|
| -1 -> fprintf ppf "%s#" i.name
|
2004-01-04 06:32:34 -08:00
|
|
|
| n -> fprintf ppf "%s/%i%s" i.name n (if global i then "g" else "")
|
1995-05-04 03:15:53 -07:00
|
|
|
|
|
|
|
type 'a tbl =
|
|
|
|
Empty
|
|
|
|
| Node of 'a tbl * 'a data * 'a tbl * int
|
|
|
|
|
|
|
|
and 'a data =
|
|
|
|
{ ident: t;
|
|
|
|
data: 'a;
|
|
|
|
previous: 'a data option }
|
|
|
|
|
|
|
|
let empty = Empty
|
|
|
|
|
|
|
|
(* Inline expansion of height for better speed
|
|
|
|
* let height = function
|
|
|
|
* Empty -> 0
|
|
|
|
* | Node(_,_,_,h) -> h
|
|
|
|
*)
|
|
|
|
|
|
|
|
let mknode l d r =
|
|
|
|
let hl = match l with Empty -> 0 | Node(_,_,_,h) -> h
|
|
|
|
and hr = match r with Empty -> 0 | Node(_,_,_,h) -> h in
|
|
|
|
Node(l, d, r, (if hl >= hr then hl + 1 else hr + 1))
|
|
|
|
|
|
|
|
let balance l d r =
|
|
|
|
let hl = match l with Empty -> 0 | Node(_,_,_,h) -> h
|
|
|
|
and hr = match r with Empty -> 0 | Node(_,_,_,h) -> h in
|
|
|
|
if hl > hr + 1 then
|
1997-10-31 05:02:30 -08:00
|
|
|
match l with
|
|
|
|
| Node (ll, ld, lr, _)
|
|
|
|
when (match ll with Empty -> 0 | Node(_,_,_,h) -> h) >=
|
|
|
|
(match lr with Empty -> 0 | Node(_,_,_,h) -> h) ->
|
|
|
|
mknode ll ld (mknode lr d r)
|
|
|
|
| Node (ll, ld, Node(lrl, lrd, lrr, _), _) ->
|
|
|
|
mknode (mknode ll ld lrl) lrd (mknode lrr d r)
|
|
|
|
| _ -> assert false
|
1995-05-04 03:15:53 -07:00
|
|
|
else if hr > hl + 1 then
|
1997-10-31 05:02:30 -08:00
|
|
|
match r with
|
|
|
|
| Node (rl, rd, rr, _)
|
|
|
|
when (match rr with Empty -> 0 | Node(_,_,_,h) -> h) >=
|
|
|
|
(match rl with Empty -> 0 | Node(_,_,_,h) -> h) ->
|
|
|
|
mknode (mknode l d rl) rd rr
|
|
|
|
| Node (Node (rll, rld, rlr, _), rd, rr, _) ->
|
|
|
|
mknode (mknode l d rll) rld (mknode rlr rd rr)
|
|
|
|
| _ -> assert false
|
1995-05-04 03:15:53 -07:00
|
|
|
else
|
|
|
|
mknode l d r
|
|
|
|
|
|
|
|
let rec add id data = function
|
|
|
|
Empty ->
|
|
|
|
Node(Empty, {ident = id; data = data; previous = None}, Empty, 1)
|
|
|
|
| Node(l, k, r, h) ->
|
|
|
|
let c = compare id.name k.ident.name in
|
|
|
|
if c = 0 then
|
|
|
|
Node(l, {ident = id; data = data; previous = Some k}, r, h)
|
|
|
|
else if c < 0 then
|
|
|
|
balance (add id data l) k r
|
|
|
|
else
|
|
|
|
balance l k (add id data r)
|
|
|
|
|
|
|
|
let rec find_stamp s = function
|
|
|
|
None ->
|
|
|
|
raise Not_found
|
|
|
|
| Some k ->
|
|
|
|
if k.ident.stamp = s then k.data else find_stamp s k.previous
|
|
|
|
|
|
|
|
let rec find_same id = function
|
|
|
|
Empty ->
|
|
|
|
raise Not_found
|
|
|
|
| Node(l, k, r, _) ->
|
|
|
|
let c = compare id.name k.ident.name in
|
|
|
|
if c = 0 then
|
|
|
|
if id.stamp = k.ident.stamp
|
|
|
|
then k.data
|
|
|
|
else find_stamp id.stamp k.previous
|
|
|
|
else
|
|
|
|
find_same id (if c < 0 then l else r)
|
|
|
|
|
|
|
|
let rec find_name name = function
|
|
|
|
Empty ->
|
|
|
|
raise Not_found
|
|
|
|
| Node(l, k, r, _) ->
|
|
|
|
let c = compare name k.ident.name in
|
|
|
|
if c = 0 then
|
|
|
|
k.data
|
|
|
|
else
|
|
|
|
find_name name (if c < 0 then l else r)
|
2003-11-25 01:20:45 -08:00
|
|
|
|
|
|
|
let rec keys_aux stack accu = function
|
|
|
|
Empty ->
|
|
|
|
begin match stack with
|
|
|
|
[] -> accu
|
|
|
|
| a :: l -> keys_aux l accu a
|
|
|
|
end
|
|
|
|
| Node(l, k, r, _) ->
|
|
|
|
keys_aux (l :: stack) (k.ident :: accu) r
|
|
|
|
|
|
|
|
let keys tbl = keys_aux [] [] tbl
|