https://github.com/EasyCrypt/easycrypt
Tip revision: 69c9c2e226e29abd4e169d8439b83c6c0aa6aef6 authored by Benjamin Gregoire on 11 November 2022, 08:06:12 UTC
add few lemmas on dfun
add few lemmas on dfun
Tip revision: 69c9c2e
ecMemory.mli
(* -------------------------------------------------------------------- *)
open EcSymbols
open EcTypes
(* -------------------------------------------------------------------- *)
type memory = EcIdent.t
val mem_equal : memory -> memory -> bool
(* -------------------------------------------------------------------- *)
type proj_arg =
{ arg_ty : ty; (* type of the procedure argument "arg" *)
arg_pos : int; (* projection *)
}
type memtype
val mt_equal_gen : (ty -> ty -> bool) -> memtype -> memtype -> bool
val mt_equal : memtype -> memtype -> bool
val mt_fv : memtype -> int EcIdent.Mid.t
val mt_iter_ty : (ty -> unit) -> memtype -> unit
(* -------------------------------------------------------------------- *)
type memenv = memory * memtype
val mem_hash : memenv -> int
val me_equal_gen : (ty -> ty -> bool) -> memenv -> memenv -> bool
val me_equal : memenv -> memenv -> bool
(* -------------------------------------------------------------------- *)
val memory : memenv -> memory
val memtype : memenv -> memtype
(* -------------------------------------------------------------------- *)
(* [empty_local witharg id] if witharg then allows to use symbol "arg" *)
val empty_local : witharg:bool -> memory -> memenv
val empty_local_mt : witharg:bool -> memtype
val schema : memory -> memenv
val schema_mt : memtype
val abstract : memory -> memenv
val abstract_mt : memtype
val is_schema : memtype -> bool
exception DuplicatedMemoryBinding of symbol
val bindall : ovariable list -> memenv -> memenv
val bindall_mt : ovariable list -> memtype -> memtype
val bind_fresh : ovariable -> memenv -> memenv * ovariable
val bindall_fresh : ovariable list -> memenv -> memenv * ovariable list
(* -------------------------------------------------------------------- *)
val lookup :
symbol -> memtype -> (variable * proj_arg option * int option) option
val lookup_me :
symbol -> memenv -> (variable * proj_arg option * int option) option
val get_name :
symbol -> int option -> memenv -> symbol option
val is_bound : symbol -> memtype -> bool
val is_bound_pv : EcTypes.prog_var -> memtype -> bool
(* -------------------------------------------------------------------- *)
val mt_subst : (ty -> ty) -> memtype -> memtype
val me_subst : memory EcIdent.Mid.t -> (ty -> ty) -> memenv -> memenv
(* -------------------------------------------------------------------- *)
val for_printing : memtype -> (symbol option * ovariable list) option
val dump_memtype : memtype -> string
(* -------------------------------------------------------------------- *)
val local_type : memtype -> ty option
val has_locals : memtype -> bool