ecPV.mli

(* -------------------------------------------------------------------- *)
open EcMaps
open EcPath
open EcEnv
open EcAst

(* -------------------------------------------------------------------- *)
type alias_clash =
 | AC_concrete_abstract of mpath * xpath
 | AC_abstract_abstract of mpath * mpath

exception AliasClash of env * alias_clash

(* -------------------------------------------------------------------- *)
module Mnpv : Map.S with type key = prog_var
module Snpv : Set.S with module M = Map.MakeBase(Mnpv)

(* -------------------------------------------------------------------- *)
module PVMap : sig
  type 'a t

  val create : env -> 'a t
  val add    : prog_var -> 'a -> 'a t -> 'a t
  val find   : prog_var -> 'a t -> 'a option
  val raw    : 'a t -> 'a Mnpv.t
end

(* -------------------------------------------------------------------- *)
module Mpv : sig
  type ('a,'b) t

  val empty : ('a,'b) t

  val check_npv_mp :
    env -> xpath -> mpath -> use use_restr -> unit

  val check_mp_mp :
    env -> mpath -> use use_restr -> mpath -> use use_restr -> unit

  val check_npv : env -> prog_var -> ('a,'b) t -> unit

  val check_glob : env -> mpath -> ('a,'b) t -> unit

  val add : env -> prog_var -> 'a -> ('a,'b) t -> ('a,'b) t

  val remove : env -> prog_var -> ('a,'b) t -> ('a,'b) t

  val add_glob : env -> mpath -> 'b -> ('a,'b) t -> ('a,'b) t

  val find : env -> prog_var -> ('a,'b) t -> 'a

  val mem : env -> prog_var -> ('a,'b) t -> bool

  val find_glob : env -> mpath -> ('a,'b) t -> 'b

  val pvs : ('a,'b) t -> 'a Mnpv.t

  val esubst  : env -> (expr, unit) t -> expr -> expr 
  val issubst : env -> (expr, unit) t -> instr list -> instr list
  val isubst  : env -> (expr, unit) t -> instr -> instr 
  val ssubst  : env -> (expr, unit) t -> stmt -> stmt
end

(* -------------------------------------------------------------------- *)
exception MemoryClash

module PVM : sig
  type subst

  val empty : subst

  val add : env -> prog_var -> EcIdent.t -> form -> subst -> subst

  val of_list : env -> ((prog_var * EcIdent.t) * form) list -> subst

  val add_glob : env -> mpath -> EcIdent.t -> form -> subst -> subst

  val of_mpv : (form,form) Mpv.t -> EcIdent.t -> subst

  val find : env -> prog_var -> memory -> subst -> form

  val subst      : env -> subst -> form  -> form

  val subst1     : env -> prog_var -> EcIdent.t -> form -> form -> form
end

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

  val empty : t

  val is_empty : t -> bool

  val pick : t -> [`Global of mpath | `PV of prog_var] option

  val add      : env -> prog_var -> ty -> t -> t
  val add_glob : env -> mpath -> t -> t
  val remove   : env -> prog_var -> t -> t
  val union    : t -> t -> t
  val diff     : t -> t -> t
  val inter    : t -> t -> t
  val subset   : t -> t -> bool

  val interdep     : env -> t -> t -> t
  val indep        : env -> t -> t -> bool
  val check_depend : env -> t -> mpath -> unit
  val elements     : t -> (prog_var * ty) list * mpath list
  val ntr_elements : t -> (prog_var * ty) list * mpath list

  val mem_pv   : env -> prog_var -> t -> bool
  val mem_glob : env -> mpath -> t -> bool

  val fv : env -> EcMemory.memory -> form -> t

  val pp : env -> Format.formatter -> t -> unit

  val iter : (prog_var -> ty -> unit) -> (mpath -> unit) -> t -> unit

  val check_notmod : EcEnv.env -> EcTypes.prog_var -> t -> bool
end

(* -------------------------------------------------------------------- *)
type 'a pvaccess = env -> PV.t -> 'a -> PV.t

val lp_write_r :                 lvalue     pvaccess
val i_write_r  : ?except:Sx.t -> instr      pvaccess
val is_write_r : ?except:Sx.t -> instr list pvaccess
val s_write_r  : ?except:Sx.t -> stmt       pvaccess
val f_write_r  : ?except:Sx.t -> xpath      pvaccess

val e_read_r      : expr       pvaccess
val form_read_r   : form       pvaccess
val i_read_r      : instr      pvaccess
val is_read_r     : instr list pvaccess
val s_read_r      : stmt       pvaccess
val f_read_r      : xpath      pvaccess

(* -------------------------------------------------------------------- *)
type 'a pvaccess0 = env -> 'a -> PV.t

val lp_write :                 lvalue     pvaccess0
val i_write  : ?except:Sx.t -> instr      pvaccess0
val is_write : ?except:Sx.t -> instr list pvaccess0
val s_write  : ?except:Sx.t -> stmt       pvaccess0
val f_write  : ?except:Sx.t -> xpath      pvaccess0

val e_read     : expr       pvaccess0
val form_read  : form       pvaccess0
val i_read     : instr      pvaccess0
val is_read    : instr list pvaccess0
val s_read     : stmt       pvaccess0
val f_read     : xpath      pvaccess0

(* -------------------------------------------------------------------- *)
exception EqObsInError

module Mpv2 : sig
  type t
  val empty : t
  type local
  val empty_local : local
  val enter_local: env -> local -> (EcIdent.t * ty) list ->
                   (EcIdent.t * ty) list -> local
  val to_form_ts_inv : t -> ts_inv -> ts_inv
  val to_form : t -> memory -> memory -> form -> form
  val of_form : env -> ts_inv -> t
  val needed_eq : env -> ts_inv -> t
  val union   : t -> t -> t
  val subset   : t -> t -> bool
  val equal    : t -> t -> bool
  val remove : env -> prog_var -> prog_var -> t -> t
  (* remove_glob mp t, mp should be a top abstract functor *)
  val remove_glob : mpath -> t -> t
  val add_glob : env -> mpath -> mpath -> t -> t
  val add_eqs_loc : env -> local -> t -> expr -> expr -> t
  val add_eqs : env -> expr -> expr -> t -> t
  val subst_l : env -> prog_var -> prog_var -> t -> t
  val subst_r : env -> prog_var -> prog_var -> t -> t
  val substs_l : env -> (prog_var * 'a) list -> prog_var list -> t -> t
  val substs_r : env -> (prog_var * 'a) list -> prog_var list -> t -> t

  val check_glob : t -> unit

  (* [mem x1 x2 eq] return true if (x1,x2) is in eq.
     x1 and x2 are assumed in normal form *)
  val mem : prog_var -> prog_var -> t -> bool
  val mem_glob : mpath -> t -> bool

  (* [iter fpv fabs eq] iterate fpv and fabs on all pair contained in eq.
     The argument given to both function are in normal form *)
  val iter :
    (prog_var -> prog_var -> ty -> unit) -> (mpath -> unit) -> t -> unit

  val eq_refl : PV.t -> t
  val fv2 : t -> PV.t
  val eq_fv2 : t -> t

  val split_nmod : env -> PV.t -> PV.t -> t -> t
  val split_mod : env -> PV.t -> PV.t -> t -> t

  val is_mod_pv' : env -> prog_var -> t -> bool
  val mem_pv_l : env -> prog_var -> t -> bool
  val mem_pv_r : env -> prog_var -> t -> bool
end

(* -------------------------------------------------------------------- *)
val i_eqobs_in_refl : env -> instr -> PV.t -> PV.t
val eqobs_inF_refl  : env -> EcPath.xpath -> PV.t -> PV.t