https://github.com/EasyCrypt/easycrypt
Tip revision: 3f4a0bd5596888cd8d28b97687d477942187aa5f authored by Pierre-Yves Strub on 11 June 2022, 06:10:21 UTC
In loop fusion/fission, add more constraints on the epilog
In loop fusion/fission, add more constraints on the epilog
Tip revision: 3f4a0bd
ecBaseLogic.ml
(* -------------------------------------------------------------------- *)
open EcUtils
open EcTypes
open EcCoreFol
(* -------------------------------------------------------------------- *)
module Epoch = struct
type t = int
let init : t = 0
let lt = (<)
let leq = (<=)
let next (e : t) : t = e + 1
let max (e : t) (e' : t) = max e e'
let min (e : t) (e' : t) = min e e'
end
(* -------------------------------------------------------------------- *)
type local_kind =
| LD_var of ty * form option
| LD_mem of EcMemory.memtype
| LD_modty of mod_ns * EcModules.module_type
| LD_hyp of form
| LD_abs_st of EcModules.abs_uses
(* -------------------------------------------------------------------- *)
type l_local = {
l_id : EcIdent.t;
l_epoch : Epoch.t;
l_kind : local_kind;
}
type l_locals = l_local list
let l_id x = x.l_id
let l_epoch x = x.l_epoch
(* -------------------------------------------------------------------- *)
type hyps = {
h_tvar : EcDecl.ty_params;
h_local : l_local list;
}
let hyps_epoch (hyps : hyps) : Epoch.t =
List.fold_left (fun e l -> Epoch.max e l.l_epoch) Epoch.init hyps.h_local
let by_id_opt (id : EcIdent.t) (hyps : hyps) : l_local option =
List.ofind (EcIdent.id_equal id |- l_id) hyps.h_local