https://github.com/EasyCrypt/easycrypt
Revision 4268b0f798c01613557a638903393c5bcc7b7ef0 authored by Pierre-Yves Strub on 14 October 2020, 06:33:40 UTC, committed by Pierre-Yves Strub on 14 October 2020, 06:34:14 UTC
This imports the variables of M in the active module scope.
1 parent 7ba9ba4
Raw File
Tip revision: 4268b0f798c01613557a638903393c5bcc7b7ef0 authored by Pierre-Yves Strub on 14 October 2020, 06:33:40 UTC
New command in modules: import var M
Tip revision: 4268b0f
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