2016-02-18 07:11:59 -08:00
|
|
|
(**************************************************************************)
|
|
|
|
(* *)
|
|
|
|
(* OCaml *)
|
|
|
|
(* *)
|
|
|
|
(* Xavier Leroy, projet Cristal, INRIA Rocquencourt *)
|
|
|
|
(* *)
|
|
|
|
(* Copyright 1996 Institut National de Recherche en Informatique et *)
|
|
|
|
(* en Automatique. *)
|
|
|
|
(* *)
|
|
|
|
(* All rights reserved. This file is distributed under the terms of *)
|
|
|
|
(* the GNU Lesser General Public License version 2.1, with the *)
|
|
|
|
(* special exception on linking described in the file LICENSE. *)
|
|
|
|
(* *)
|
|
|
|
(**************************************************************************)
|
1995-08-09 08:06:35 -07:00
|
|
|
|
2020-10-15 05:47:19 -07:00
|
|
|
open Local_store
|
|
|
|
|
2018-09-13 02:45:37 -07:00
|
|
|
let lowest_scope = 0
|
|
|
|
let highest_scope = 100000000
|
|
|
|
|
2018-08-28 09:06:52 -07:00
|
|
|
type t =
|
2018-08-28 09:07:01 -07:00
|
|
|
| Local of { name: string; stamp: int }
|
|
|
|
| Scoped of { name: string; stamp: int; scope: int }
|
2018-08-28 09:06:52 -07:00
|
|
|
| Global of string
|
2018-08-28 09:07:11 -07:00
|
|
|
| Predef of { name: string; stamp: int }
|
|
|
|
(* the stamp is here only for fast comparison, but the name of
|
|
|
|
predefined identifiers is always unique. *)
|
1995-05-04 03:15:53 -07:00
|
|
|
|
|
|
|
(* A stamp of 0 denotes a persistent identifier *)
|
|
|
|
|
2020-10-15 05:47:19 -07:00
|
|
|
let currentstamp = s_ref 0
|
|
|
|
let predefstamp = s_ref 0
|
1995-05-04 03:15:53 -07:00
|
|
|
|
2018-08-28 09:07:01 -07:00
|
|
|
let create_scoped ~scope s =
|
1995-05-04 03:15:53 -07:00
|
|
|
incr currentstamp;
|
2018-08-28 09:07:01 -07:00
|
|
|
Scoped { name = s; stamp = !currentstamp; scope }
|
2018-08-28 09:06:45 -07:00
|
|
|
|
2018-08-28 09:07:01 -07:00
|
|
|
let create_local s =
|
2018-08-28 09:06:45 -07:00
|
|
|
incr currentstamp;
|
2018-08-28 09:07:01 -07:00
|
|
|
Local { name = s; stamp = !currentstamp }
|
2018-08-28 09:06:52 -07:00
|
|
|
|
2018-08-28 09:07:11 -07:00
|
|
|
let create_predef s =
|
|
|
|
incr predefstamp;
|
|
|
|
Predef { name = s; stamp = !predefstamp }
|
1995-05-04 03:15:53 -07:00
|
|
|
|
1996-04-22 04:15:41 -07:00
|
|
|
let create_persistent s =
|
2018-08-28 09:06:52 -07:00
|
|
|
Global s
|
|
|
|
|
|
|
|
let name = function
|
|
|
|
| Local { name; _ }
|
2018-08-28 09:07:01 -07:00
|
|
|
| Scoped { name; _ }
|
2018-08-28 09:06:52 -07:00
|
|
|
| Global name
|
2018-08-28 09:07:11 -07:00
|
|
|
| Predef { name; _ } -> name
|
2018-08-28 09:06:52 -07:00
|
|
|
|
|
|
|
let rename = function
|
2018-08-28 09:07:11 -07:00
|
|
|
| Local { name; stamp = _ }
|
|
|
|
| Scoped { name; stamp = _; scope = _ } ->
|
2018-08-28 09:06:52 -07:00
|
|
|
incr currentstamp;
|
2018-08-28 09:07:01 -07:00
|
|
|
Local { name; stamp = !currentstamp }
|
2018-08-28 09:06:52 -07:00
|
|
|
| id ->
|
|
|
|
Misc.fatal_errorf "Ident.rename %s" (name id)
|
|
|
|
|
|
|
|
let unique_name = function
|
2018-08-28 09:07:01 -07:00
|
|
|
| Local { name; stamp }
|
2018-08-30 10:15:32 -07:00
|
|
|
| Scoped { name; stamp } -> name ^ "_" ^ Int.to_string stamp
|
2018-09-13 02:40:59 -07:00
|
|
|
| Global name ->
|
|
|
|
(* we're adding a fake stamp, because someone could have named his unit
|
|
|
|
[Foo_123] and since we're using unique_name to produce symbol names,
|
|
|
|
we might clash with an ident [Local { "Foo"; 123 }]. *)
|
|
|
|
name ^ "_0"
|
|
|
|
| Predef { name; _ } ->
|
|
|
|
(* we know that none of the predef names (currently) finishes in
|
|
|
|
"_<some number>", and that their name is unique. *)
|
|
|
|
name
|
2018-08-28 09:06:52 -07:00
|
|
|
|
|
|
|
let unique_toplevel_name = function
|
2018-08-28 09:07:01 -07:00
|
|
|
| Local { name; stamp }
|
2018-08-30 10:15:32 -07:00
|
|
|
| Scoped { name; stamp } -> name ^ "/" ^ Int.to_string stamp
|
2018-08-28 09:06:52 -07:00
|
|
|
| Global name
|
2018-08-28 09:07:11 -07:00
|
|
|
| Predef { name; _ } -> name
|
2018-08-28 09:06:52 -07:00
|
|
|
|
|
|
|
let persistent = function
|
|
|
|
| Global _ -> true
|
|
|
|
| _ -> false
|
|
|
|
|
|
|
|
let equal i1 i2 =
|
|
|
|
match i1, i2 with
|
|
|
|
| Local { name = name1; _ }, Local { name = name2; _ }
|
2018-08-28 09:07:01 -07:00
|
|
|
| Scoped { name = name1; _ }, Scoped { name = name2; _ }
|
2018-08-28 09:07:11 -07:00
|
|
|
| Global name1, Global name2 ->
|
2018-08-28 09:06:52 -07:00
|
|
|
name1 = name2
|
2018-08-28 09:07:11 -07:00
|
|
|
| Predef { stamp = s1; _ }, Predef { stamp = s2 } ->
|
|
|
|
(* if they don't have the same stamp, they don't have the same name *)
|
|
|
|
s1 = s2
|
2018-08-28 09:06:52 -07:00
|
|
|
| _ ->
|
|
|
|
false
|
1995-05-04 03:15:53 -07:00
|
|
|
|
2020-02-13 07:38:03 -08:00
|
|
|
let same i1 i2 =
|
|
|
|
match i1, i2 with
|
|
|
|
| Local { stamp = s1; _ }, Local { stamp = s2; _ }
|
|
|
|
| Scoped { stamp = s1; _ }, Scoped { stamp = s2; _ }
|
|
|
|
| Predef { stamp = s1; _ }, Predef { stamp = s2 } ->
|
|
|
|
s1 = s2
|
|
|
|
| Global name1, Global name2 ->
|
|
|
|
name1 = name2
|
|
|
|
| _ ->
|
|
|
|
false
|
2015-11-28 06:09:09 -08:00
|
|
|
|
2018-08-28 09:06:52 -07:00
|
|
|
let stamp = function
|
2018-08-28 09:07:01 -07:00
|
|
|
| Local { stamp; _ }
|
|
|
|
| Scoped { stamp; _ } -> stamp
|
2018-08-28 09:06:52 -07:00
|
|
|
| _ -> 0
|
|
|
|
|
|
|
|
let scope = function
|
2018-08-28 09:07:01 -07:00
|
|
|
| Scoped { scope; _ } -> scope
|
2018-09-13 02:45:37 -07:00
|
|
|
| Local _ -> highest_scope
|
|
|
|
| Global _ | Predef _ -> lowest_scope
|
1996-07-15 09:35:35 -07:00
|
|
|
|
2003-05-12 02:34:05 -07:00
|
|
|
let reinit_level = ref (-1)
|
|
|
|
|
2010-01-22 04:48:24 -08:00
|
|
|
let reinit () =
|
2003-05-12 02:34:05 -07:00
|
|
|
if !reinit_level < 0
|
|
|
|
then reinit_level := !currentstamp
|
|
|
|
else currentstamp := !reinit_level
|
|
|
|
|
2018-08-28 09:06:52 -07:00
|
|
|
let global = function
|
2018-08-28 09:07:01 -07:00
|
|
|
| Local _
|
|
|
|
| Scoped _ -> false
|
2018-08-28 09:06:52 -07:00
|
|
|
| Global _
|
2018-08-28 09:07:11 -07:00
|
|
|
| Predef _ -> true
|
2004-01-04 06:32:34 -08:00
|
|
|
|
2018-08-28 09:07:11 -07:00
|
|
|
let is_predef = function
|
|
|
|
| Predef _ -> true
|
2018-08-28 09:06:52 -07:00
|
|
|
| _ -> false
|
1995-05-04 03:15:53 -07:00
|
|
|
|
2018-09-14 02:29:21 -07:00
|
|
|
let print ~with_scope ppf =
|
|
|
|
let open Format in
|
|
|
|
function
|
2018-08-28 09:07:11 -07:00
|
|
|
| Global name -> fprintf ppf "%s!" name
|
|
|
|
| Predef { name; stamp = n } ->
|
|
|
|
fprintf ppf "%s%s!" name
|
2018-09-14 02:29:21 -07:00
|
|
|
(if !Clflags.unique_ids then sprintf "/%i" n else "")
|
2018-08-28 09:06:52 -07:00
|
|
|
| Local { name; stamp = n } ->
|
|
|
|
fprintf ppf "%s%s" name
|
2018-09-14 02:29:21 -07:00
|
|
|
(if !Clflags.unique_ids then sprintf "/%i" n else "")
|
2018-08-28 09:07:01 -07:00
|
|
|
| Scoped { name; stamp = n; scope } ->
|
2018-09-14 02:29:21 -07:00
|
|
|
fprintf ppf "%s%s%s" name
|
|
|
|
(if !Clflags.unique_ids then sprintf "/%i" n else "")
|
|
|
|
(if with_scope then sprintf "[%i]" scope else "")
|
|
|
|
|
|
|
|
let print_with_scope ppf id = print ~with_scope:true ppf id
|
|
|
|
|
|
|
|
let print ppf id = print ~with_scope:false ppf id
|
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) ->
|
2020-02-13 07:38:03 -08:00
|
|
|
let c = String.compare (name id) (name k.ident) in
|
1995-05-04 03:15:53 -07:00
|
|
|
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)
|
|
|
|
|
2018-09-18 06:49:18 -07:00
|
|
|
let rec min_binding = function
|
|
|
|
Empty -> raise Not_found
|
|
|
|
| Node (Empty, d, _, _) -> d
|
|
|
|
| Node (l, _, _, _) -> min_binding l
|
|
|
|
|
|
|
|
let rec remove_min_binding = function
|
|
|
|
Empty -> invalid_arg "Map.remove_min_elt"
|
|
|
|
| Node (Empty, _, r, _) -> r
|
|
|
|
| Node (l, d, r, _) -> balance (remove_min_binding l) d r
|
|
|
|
|
|
|
|
let merge t1 t2 =
|
|
|
|
match (t1, t2) with
|
|
|
|
(Empty, t) -> t
|
|
|
|
| (t, Empty) -> t
|
|
|
|
| (_, _) ->
|
|
|
|
let d = min_binding t2 in
|
|
|
|
balance t1 d (remove_min_binding t2)
|
|
|
|
|
|
|
|
let rec remove id = function
|
|
|
|
Empty ->
|
|
|
|
Empty
|
|
|
|
| (Node (l, k, r, h) as m) ->
|
2020-02-13 07:38:03 -08:00
|
|
|
let c = String.compare (name id) (name k.ident) in
|
2018-09-18 06:49:18 -07:00
|
|
|
if c = 0 then
|
|
|
|
match k.previous with
|
|
|
|
| None -> merge l r
|
|
|
|
| Some k -> Node (l, k, r, h)
|
|
|
|
else if c < 0 then
|
|
|
|
let ll = remove id l in if l == ll then m else balance ll k r
|
|
|
|
else
|
|
|
|
let rr = remove id r in if r == rr then m else balance l k rr
|
|
|
|
|
2018-08-28 09:07:11 -07:00
|
|
|
let rec find_previous id = function
|
1995-05-04 03:15:53 -07:00
|
|
|
None ->
|
|
|
|
raise Not_found
|
|
|
|
| Some k ->
|
2018-08-28 09:07:11 -07:00
|
|
|
if same id k.ident then k.data else find_previous id k.previous
|
1995-05-04 03:15:53 -07:00
|
|
|
|
|
|
|
let rec find_same id = function
|
|
|
|
Empty ->
|
|
|
|
raise Not_found
|
|
|
|
| Node(l, k, r, _) ->
|
2020-02-13 07:38:03 -08:00
|
|
|
let c = String.compare (name id) (name k.ident) in
|
1995-05-04 03:15:53 -07:00
|
|
|
if c = 0 then
|
2018-08-28 09:07:11 -07:00
|
|
|
if same id k.ident
|
1995-05-04 03:15:53 -07:00
|
|
|
then k.data
|
2018-08-28 09:07:11 -07:00
|
|
|
else find_previous id k.previous
|
1995-05-04 03:15:53 -07:00
|
|
|
else
|
|
|
|
find_same id (if c < 0 then l else r)
|
|
|
|
|
2018-08-28 09:06:52 -07:00
|
|
|
let rec find_name n = function
|
1995-05-04 03:15:53 -07:00
|
|
|
Empty ->
|
|
|
|
raise Not_found
|
|
|
|
| Node(l, k, r, _) ->
|
2020-02-13 07:38:03 -08:00
|
|
|
let c = String.compare n (name k.ident) in
|
1995-05-04 03:15:53 -07:00
|
|
|
if c = 0 then
|
2016-10-03 07:02:37 -07:00
|
|
|
k.ident, k.data
|
1995-05-04 03:15:53 -07:00
|
|
|
else
|
2018-08-28 09:06:52 -07:00
|
|
|
find_name n (if c < 0 then l else r)
|
2003-11-25 01:20:45 -08:00
|
|
|
|
2012-10-29 00:54:06 -07:00
|
|
|
let rec get_all = function
|
|
|
|
| None -> []
|
2016-10-03 07:02:37 -07:00
|
|
|
| Some k -> (k.ident, k.data) :: get_all k.previous
|
2012-10-29 00:54:06 -07:00
|
|
|
|
2018-08-28 09:06:52 -07:00
|
|
|
let rec find_all n = function
|
2012-10-29 00:54:06 -07:00
|
|
|
Empty ->
|
|
|
|
[]
|
|
|
|
| Node(l, k, r, _) ->
|
2020-02-13 07:38:03 -08:00
|
|
|
let c = String.compare n (name k.ident) in
|
2012-10-29 00:54:06 -07:00
|
|
|
if c = 0 then
|
2016-10-03 07:02:37 -07:00
|
|
|
(k.ident, k.data) :: get_all k.previous
|
2012-10-29 00:54:06 -07:00
|
|
|
else
|
2018-08-28 09:06:52 -07:00
|
|
|
find_all n (if c < 0 then l else r)
|
2012-10-29 00:54:06 -07:00
|
|
|
|
|
|
|
let rec fold_aux f stack accu = function
|
2003-11-25 01:20:45 -08:00
|
|
|
Empty ->
|
|
|
|
begin match stack with
|
|
|
|
[] -> accu
|
2012-10-29 00:54:06 -07:00
|
|
|
| a :: l -> fold_aux f l accu a
|
2003-11-25 01:20:45 -08:00
|
|
|
end
|
|
|
|
| Node(l, k, r, _) ->
|
2012-10-29 00:54:06 -07:00
|
|
|
fold_aux f (l :: stack) (f k accu) r
|
|
|
|
|
|
|
|
let fold_name f tbl accu = fold_aux (fun k -> f k.ident k.data) [] accu tbl
|
|
|
|
|
|
|
|
let rec fold_data f d accu =
|
|
|
|
match d with
|
|
|
|
None -> accu
|
|
|
|
| Some k -> f k.ident k.data (fold_data f k.previous accu)
|
|
|
|
|
|
|
|
let fold_all f tbl accu =
|
|
|
|
fold_aux (fun k -> fold_data f (Some k)) [] accu tbl
|
2003-11-25 01:20:45 -08:00
|
|
|
|
2012-10-29 00:54:06 -07:00
|
|
|
(* let keys tbl = fold_name (fun k _ accu -> k::accu) tbl [] *)
|
2012-04-10 22:50:08 -07:00
|
|
|
|
|
|
|
let rec iter f = function
|
|
|
|
Empty -> ()
|
|
|
|
| Node(l, k, r, _) ->
|
|
|
|
iter f l; f k.ident k.data; iter f r
|
2014-04-07 08:43:20 -07:00
|
|
|
|
|
|
|
(* Idents for sharing keys *)
|
|
|
|
|
|
|
|
(* They should be 'totally fresh' -> neg numbers *)
|
|
|
|
let key_name = ""
|
|
|
|
|
|
|
|
let make_key_generator () =
|
|
|
|
let c = ref 1 in
|
2018-08-28 09:06:52 -07:00
|
|
|
function
|
2018-08-28 09:07:01 -07:00
|
|
|
| Local _
|
|
|
|
| Scoped _ ->
|
2018-08-28 09:06:52 -07:00
|
|
|
let stamp = !c in
|
|
|
|
decr c ;
|
2018-08-28 09:07:01 -07:00
|
|
|
Local { name = key_name; stamp = stamp }
|
2018-08-28 09:06:52 -07:00
|
|
|
| global_id ->
|
|
|
|
Misc.fatal_errorf "Ident.make_key_generator () %s" (name global_id)
|
2016-01-12 09:01:25 -08:00
|
|
|
|
|
|
|
let compare x y =
|
2018-08-28 09:06:52 -07:00
|
|
|
match x, y with
|
|
|
|
| Local x, Local y ->
|
|
|
|
let c = x.stamp - y.stamp in
|
|
|
|
if c <> 0 then c
|
|
|
|
else compare x.name y.name
|
|
|
|
| Local _, _ -> 1
|
|
|
|
| _, Local _ -> (-1)
|
2018-08-28 09:07:01 -07:00
|
|
|
| Scoped x, Scoped y ->
|
|
|
|
let c = x.stamp - y.stamp in
|
|
|
|
if c <> 0 then c
|
|
|
|
else compare x.name y.name
|
|
|
|
| Scoped _, _ -> 1
|
|
|
|
| _, Scoped _ -> (-1)
|
2018-08-28 09:06:52 -07:00
|
|
|
| Global x, Global y -> compare x y
|
|
|
|
| Global _, _ -> 1
|
|
|
|
| _, Global _ -> (-1)
|
2018-08-28 09:07:11 -07:00
|
|
|
| Predef { stamp = s1; _ }, Predef { stamp = s2; _ } -> compare s1 s2
|
2016-01-12 09:01:25 -08:00
|
|
|
|
|
|
|
let output oc id = output_string oc (unique_name id)
|
2018-08-28 09:06:52 -07:00
|
|
|
let hash i = (Char.code (name i).[0]) lxor (stamp i)
|
2016-01-12 09:01:25 -08:00
|
|
|
|
|
|
|
let original_equal = equal
|
|
|
|
include Identifiable.Make (struct
|
|
|
|
type nonrec t = t
|
|
|
|
let compare = compare
|
|
|
|
let output = output
|
|
|
|
let print = print
|
|
|
|
let hash = hash
|
|
|
|
let equal = same
|
|
|
|
end)
|
|
|
|
let equal = original_equal
|