(*
 * Copyright (c) 2017-present,
 * Programming Research Laboratory (ROPAS), Seoul National University, Korea
 * This software is distributed under the term of the BSD-3 clause license.
 *)
(** * Memory operations.  *)

Set Implicit Arguments.

Require Import ZArith.
Require Import Monad hpattern vgtac VocabA Syn UserInputType DPow Global.
Require Import DomBasic DomAbs DomMem.

Module Make (Import M : Monad) (MB : MemBasic M).

Include MemOp M MB.

Section SemMem.

Variable mode : update_mode.

Variable g : G.t.

Fixpoint list_fold2_m {A B C : Type} (f : A -> B -> C -> m C)
         (l1 : list A) (l2 : list B) (acc : C) : m C :=
  match l1, l2 with
    | nil, nil => ret acc
    | (a :: l1')%list, (b :: l2')%list =>
      do acc' <- f a b acc ;
      list_fold2_m f l1' l2' acc'
    | _, _ => ret acc
  end.

Definition bind_arg f x v m :=
  mem_wupdate mode (PowLoc.singleton (loc_of_var (var_of_lvar (f, x)))) v m.

Definition bind_args vs f m :=
  match InterCfg.get_args (G.icfg g) f with
    | Some args => list_fold2_m (bind_arg f) args vs m
    | None => ret m
  end.

End SemMem.

End Make.