https://github.com/EasyCrypt/easycrypt
Tip revision: 846710a2a656834065e745d19416ebdc83158f55 authored by Benjamin Gregoire on 14 July 2019, 06:50:07 UTC
Start restructuration of the code to be able to avant mutual dependency between type and mpath
Start restructuration of the code to be able to avant mutual dependency between type and mpath
Tip revision: 846710a
ecIdent.ml
(* --------------------------------------------------------------------
* Copyright (c) - 2012--2016 - IMDEA Software Institute
* Copyright (c) - 2012--2018 - Inria
* Copyright (c) - 2012--2018 - Ecole Polytechnique
*
* Distributed under the terms of the CeCILL-C-V1 license
* -------------------------------------------------------------------- *)
(* -------------------------------------------------------------------- *)
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)