open Access
open DFMapAVL
open DMem
open DomAbs
open DomBasic
open Global
open InterNode
open IntraNode
open Syn
open TStr
open UserInputType

type __ = Obj.t

module Acc = Access.Make(Loc)(PowLoc)

module Mem = Make(Loc)(Val)(PowLoc)

module Index = InterNode

module Table = FMapAVL'.Make(Index)

module type MemBasic =
 functor (M:Monad.Monad) ->
 sig
  val mem_find : Loc.t -> Mem.t -> Val.t M.m

  val mem_add : Loc.t -> Val.t -> Mem.t -> Mem.t M.m

  val mem_weak_add : Loc.t -> Val.t -> Mem.t -> Mem.t M.m

  val mem_pre_weak_add : Loc.t -> Val.t -> Mem.t -> Mem.t M.m
 end

module AccMem =
 struct
  (** val mem_find : Loc.t' -> Mem.t -> Val.t * Acc.t **)

  let mem_find l m0 =
    ((Mem.find l m0), (Acc.add Acc.USE l Acc.bot))

  (** val mem_add : Loc.t' -> Val.t -> Mem.t -> Mem.t * Acc.t **)

  let mem_add l v m0 =
    ((Mem.add l v m0), (Acc.add Acc.DEF l Acc.bot))

  (** val mem_weak_add : Loc.t' -> Val.t -> Mem.t -> Mem.t * Acc.t **)

  let mem_weak_add l v m0 =
    ((Mem.weak_add l v m0), (Acc.add Acc.ALL l Acc.bot))

  (** val mem_pre_weak_add : Loc.t' -> Val.t -> Mem.t -> Mem.t * Acc.t **)

  let mem_pre_weak_add l v m0 =
    ((Mem.fast_weak_add l v m0), (Acc.add Acc.ALL l Acc.bot))
 end

module IdMem =
 struct
  (** val mem_find : Loc.t' -> Mem.t -> Val.t **)

  let mem_find l m0 =
    Mem.find l m0

  (** val mem_add : Loc.t' -> Val.t -> Mem.t -> Mem.t **)

  let mem_add l v m0 =
    Mem.add l v m0

  (** val mem_weak_add : Loc.t' -> Val.t -> Mem.t -> Mem.t **)

  let mem_weak_add l v m0 =
    Mem.weak_add l v m0

  (** val mem_pre_weak_add : Loc.t' -> Val.t -> Mem.t -> Mem.t **)

  let mem_pre_weak_add l v m0 =
    Mem.fast_weak_add l v m0
 end

module MemOp =
 functor (M:Monad.Monad) ->
 functor (MB:sig
  val mem_find : Loc.t -> Mem.t -> Val.t M.m

  val mem_add : Loc.t -> Val.t -> Mem.t -> Mem.t M.m

  val mem_weak_add : Loc.t -> Val.t -> Mem.t -> Mem.t M.m

  val mem_pre_weak_add : Loc.t -> Val.t -> Mem.t -> Mem.t M.m
 end) ->
 struct
  (** val can_strong_update : update_mode -> G.t -> Loc.t -> bool **)

  let can_strong_update mode g l =
    match mode with
    | Weak -> false
    | Strong -> approx_one_loc g l

  (** val mem_lookup : PowLoc.t -> Mem.t -> Val.t M.m **)

  let mem_lookup lvs m0 =
    let find_join = fun loc acc_a ->
      M.bind acc_a (fun acc ->
        M.bind (MB.mem_find loc m0) (fun v -> M.ret (Val.join acc v)))
    in
    PowLoc.fold find_join lvs (M.ret Val.bot)

  (** val add : Loc.t -> Val.t -> Mem.t -> Mem.t M.m **)

  let add =
    MB.mem_add

  (** val weak_add : update_mode -> Loc.t -> Val.t -> Mem.t -> Mem.t M.m **)

  let weak_add = function
  | Weak -> MB.mem_pre_weak_add
  | Strong -> MB.mem_weak_add

  (** val mem_update :
      update_mode -> G.t -> Loc.t -> Val.t -> Mem.t -> Mem.t M.m **)

  let mem_update mode g l v m0 =
    if can_strong_update mode g l then add l v m0 else weak_add mode l v m0

  (** val mem_wupdate :
      update_mode -> PowLoc.t -> Val.t -> Mem.t -> Mem.t M.m **)

  let mem_wupdate mode lvs v m0 =
    let weak_add_v = fun lv m_a ->
      M.bind m_a (fun m1 -> weak_add mode lv v m1)
    in
    PowLoc.fold weak_add_v lvs (M.ret m0)
 end