https://github.com/EasyCrypt/easycrypt
Revision a549eb44e2b03ffed06fdc356fcad09a49c247bf authored by Pierre-Yves Strub on 19 November 2021, 06:23:34 UTC, committed by Pierre-Yves Strub on 19 November 2021, 06:27:09 UTC
This can be done by adding the "opaque" tag, e.g.:

  op [opaque] myop = ...

solve #94
1 parent 10e1563
Raw File
Tip revision: a549eb44e2b03ffed06fdc356fcad09a49c247bf authored by Pierre-Yves Strub on 19 November 2021, 06:23:34 UTC
Add an option to define opaque operators
Tip revision: a549eb4
ecIdent.mli
(* --------------------------------------------------------------------
 * Copyright (c) - 2012--2016 - IMDEA Software Institute
 * Copyright (c) - 2012--2021 - Inria
 * Copyright (c) - 2012--2021 - 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
back to top