PMap (transformers.States.PMap)

type index_mode =

| Static
| Dynamic

module type PMapImpl = sig ... end

module type OpenPMapType = sig ... end

module type PMapType = sig ... end

module Make
  (I_Cons : functor (S : MyMonadicSMemory.S) -> PMapImpl with type entry = S.t)
  (S : MyMonadicSMemory.S) : 
  PMapType
    with type entry = S.t
     and type t = I_Cons(S).t * Gillian.Gil_syntax.Expr.t option

module MakeOpen
  (I_Cons : functor (S : MyMonadicSMemory.S) -> PMapImpl with type entry = S.t)
  (S : MyMonadicSMemory.S) : 
  OpenPMapType with type entry = S.t and type t = I_Cons(S).t

module type PMapIndex = sig ... end

module LocationIndex : PMapIndex

module StringIndex : PMapIndex

module IntegerIndex : PMapIndex

type 'e t_base_sat := 'e MyUtils.ExpMap.t

type 'e t_base_ent := 'e MyUtils.ExpMapEnt.t

type 'e t_split_sat := 'e MyUtils.ExpMap.t * 'e MyUtils.ExpMap.t

type 'e t_split_ent := 'e MyUtils.ExpMapEnt.t * 'e MyUtils.ExpMapEnt.t

type 'e t_aloc := 'e MyUtils.SMap.t

module BaseImplSat
  (I : PMapIndex)
  (S : MyMonadicSMemory.S) : 
  PMapImpl with type t = S.t t_base_sat and type entry = S.t

module BaseImplEnt
  (I : PMapIndex)
  (S : MyMonadicSMemory.S) : 
  PMapImpl with type t = S.t t_base_ent and type entry = S.t

module SplitImplSat
  (I : PMapIndex)
  (S : MyMonadicSMemory.S) : 
  PMapImpl with type t = S.t t_split_sat and type entry = S.t

module SplitImplEnt
  (I : PMapIndex)
  (S : MyMonadicSMemory.S) : 
  PMapImpl with type t = S.t t_split_ent and type entry = S.t

module ALocImpl
  (S : MyMonadicSMemory.S) : 
  PMapImpl with type t = S.t t_aloc and type entry = S.t