https://github.com/EasyCrypt/easycrypt
Tip revision: aa6dc074f77deb2c8215b6281a0a0be9e358d461 authored by Pierre-Yves Strub on 19 October 2021, 10:19:36 UTC
Add a simple form of pattern selection in rewrite rules
Add a simple form of pattern selection in rewrite rules
Tip revision: aa6dc07
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)