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.mli
(* --------------------------------------------------------------------
* 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 EcMaps
open EcSymbols
(* -------------------------------------------------------------------- *)
type ident = private {
id_symb : symbol;
id_tag : int;
}
type idents = ident list
type t = ident
val create : symbol -> t
val fresh : t -> t
val name : t -> symbol
val tag : t -> int
val tostring : t -> string
(* -------------------------------------------------------------------- *)
val id_equal : t -> t -> bool
val id_compare : t -> t -> int
val id_hash : t -> int
val id_ntr_compare : t -> t -> int
(* -------------------------------------------------------------------- *)
module Mid : Map.S with type key = t
module Sid : Set.S with module M = Map.MakeBase(Mid)
module Hid : EcMaps.EHashtbl.S with type key = ident
(* -------------------------------------------------------------------- *)
val fv_singleton : ident -> int Mid.t
val fv_union : int Mid.t -> int Mid.t -> int Mid.t
val fv_diff : int Mid.t -> 'a Mid.t -> int Mid.t
val fv_add : ident -> int Mid.t -> int Mid.t
(* -------------------------------------------------------------------- *)
val pp_ident : Format.formatter -> t -> unit