https://github.com/EasyCrypt/easycrypt
Tip revision: a79f9aeb6de046ca12210d26317fab59c175d0dd authored by Pierre-Yves Strub on 08 July 2014, 09:43:21 UTC
Fix bug w.r.t. _tools presence detection.
Fix bug w.r.t. _tools presence detection.
Tip revision: a79f9ae
ecIdent.ml
(* Copyright (c) - 2012-2014 - IMDEA Software Institute and INRIA
* Distributed under the terms of the CeCILL-B 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 tag x = x.id_tag
(* -------------------------------------------------------------------- *)
let id_equal : ident -> ident -> bool = (==)
let id_compare i1 i2 = i2.id_tag - i1.id_tag
let id_hash id = id.id_tag
(* -------------------------------------------------------------------- *)
module IdComparable = struct
type t = ident
let compare = id_compare
end
module Mid = Map.Make(IdComparable)
module Sid = Set.MakeOfMap(Mid)
(* -------------------------------------------------------------------- *)
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)