Revision 1dd51308999f3b164f0c95a2f858d420b2a5a2ff authored by Christian Doczkal on 12 May 2022, 08:35:59 UTC, committed by Pierre-Yves Strub on 17 October 2022, 13:31:22 UTC
1 parent fc2bfba
ecIdent.ml
(* -------------------------------------------------------------------- *)
open EcSymbols
open EcUtils
open EcMaps
(* -------------------------------------------------------------------- *)
type ident = {
id_symb : symbol;
id_tag : int;
}
type idents = ident list
(* -------------------------------------------------------------------- *)
let name x = x.id_symb
let id_compare i1 i2 = i2.id_tag - i1.id_tag
let tag x = x.id_tag
(* -------------------------------------------------------------------- *)
let id_equal : ident -> ident -> bool = (==)
let id_hash id = id.id_tag
let id_ntr_compare (id1 : ident) (id2 : ident) =
if id_equal id1 id2 then 0 else
match String.compare id1.id_symb id2.id_symb with
| 0 -> id_compare id1 id2
| n -> n
(* -------------------------------------------------------------------- *)
module Collection = MakeMSH(struct
type t = ident
let tag = fun (x : ident) -> x.id_tag
end)
module Sid = Collection.S
module Mid = Collection.M
module Hid = Collection.H
(* -------------------------------------------------------------------- *)
let fv_singleton x = Mid.singleton x 1
let fv_union m1 m2 = Mid.union (fun _ m n -> Some (m+n)) m1 m2
let fv_diff m1 m2 = Mid.diff (fun _ _ _ -> None) m1 m2
let fv_add x m = Mid.change (fun x -> Some ((odfl 0 x) + 1)) x m
(* -------------------------------------------------------------------- *)
type t = ident
let create (x : symbol) =
{ id_symb = x;
id_tag = EcUid.unique () }
let fresh (id : t) = create (name id)
let tostring (id : t) =
Printf.sprintf "%s/%d" id.id_symb id.id_tag
(* -------------------------------------------------------------------- *)
let pp_ident fmt id = Format.fprintf fmt "%s" (name id)
![swh spinner](/static/img/swh-spinner.gif)
Computing file changes ...