https://github.com/EasyCrypt/easycrypt
Revision 60d29c1f11f6c79824022608f9f83503d983ce61 authored by Benjamin Gregoire on 13 September 2019, 06:39:19 UTC, committed by Benjamin Gregoire on 13 September 2019, 06:39:19 UTC
1 parent 0e717db
Raw File
Tip revision: 60d29c1f11f6c79824022608f9f83503d983ce61 authored by Benjamin Gregoire on 13 September 2019, 06:39:19 UTC
remove duplicate lemma get_none -> domNE
Tip revision: 60d29c1
ecUid.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

(* -------------------------------------------------------------------- *)
val unique : unit -> int

(* -------------------------------------------------------------------- *)
type uid = int
type uidmap

val create : unit -> uidmap
val lookup : uidmap -> symbol -> uid option
val forsym : uidmap -> symbol -> uid

(* -------------------------------------------------------------------- *)
val uid_equal   : uid -> uid -> bool
val uid_compare : uid -> uid -> int

module Muid : Map.S  with type key = uid
module Suid : Set.S  with module M = Map.MakeBase(Muid)

(* -------------------------------------------------------------------- *)
module NameGen : sig
  type t

  val ofint  : int -> string
  val bulk   : ?fmt:(string -> string) -> int -> string list
  val create : unit -> t
  val get    : t -> uid -> string
end
back to top