open DItv
open DomAbs
open DomBasic
open DomMem
open Global
open InterNode
open SemEval
open SemMem
open Syn
open TStr
open UserInputType

(** val itv_prune : binop -> Itv.t -> Itv.t -> Itv.t **)

let itv_prune op x y =
  match x with
  | Itv.V (a, b) ->
    (match y with
     | Itv.V (c, d) ->
       (match op with
        | Lt -> Itv.gen_itv a (Itv.min' b (Itv.minus'_one d))
        | Gt -> Itv.gen_itv (Itv.max' a (Itv.plus'_one c)) b
        | Le -> Itv.gen_itv a (Itv.min' b d)
        | Ge -> Itv.gen_itv (Itv.max' a c) b
        | Eq -> Itv.meet x y
        | _ -> x)
     | Itv.Bot -> Itv.bot)
  | Itv.Bot -> Itv.bot

module Make =
 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
  module SemMem = Make(M)(MB)

  module SemEval = SemEval.Make(M)(MB)

  (** val prune : G.t -> update_mode -> t -> exp -> Mem.t -> Mem.t M.m **)

  let prune g mode node cond m0 =
    match cond with
    | BinOp (op, e1, e, _) ->
      (match e1 with
       | Lval (lv, _) ->
         let Coq_lval_intro (lh, o, _) = lv in
         (match lh with
          | VarLhost (x, is_global) ->
            (match o with
             | NoOffset ->
               let x_lv = SemEval.eval_var node x is_global in
               M.bind (SemMem.mem_lookup (PowLoc.singleton x_lv) m0)
                 (fun x_v ->
                 M.bind (SemEval.eval mode node e m0) (fun v ->
                   let x_v' =
                     modify_itv x_v
                       (itv_prune op (itv_of_val x_v) (itv_of_val v))
                   in
                   SemMem.mem_update mode g x_lv x_v' m0))
             | _ -> M.ret m0)
          | MemLhost _ -> M.ret m0)
       | _ -> M.ret m0)
    | _ -> M.ret m0
 end