Module FactMsgHelpers

Require Import Coqlib Util Utf8 IdealExpr AbIdealEnv AdomLib Integers FastArith.
Require Import IdealIntervals ZIntervals.

Fixpoint simplify_bool_expr_aux (e:iexpr) : iexpr * bool :=
  match e with
  | IEvar _ _ | IEconst _ | IEZitv _ => (e, false)
  | IEunop op e => (IEunop op (simplify_expr e), false)
  | IEbinop (IOcmp Ceq) (e as e1) (IEconst (INz z) as e2)
  | IEbinop (IOcmp Ceq) (IEconst (INz z) as e1) (e as e2) =>
    if Zfasteqb z F0 then
      let '(e', b) := simplify_bool_expr_aux e in
      (e', negb b)
    else (IEbinop (IOcmp Ceq) (simplify_expr e1) (simplify_expr e2), false)
  | IEbinop (IOcmp Cne) (e as e1) (IEconst (INz z) as e2)
  | IEbinop (IOcmp Cne) (IEconst (INz z) as e1) (e as e2) =>
    if Zfasteqb z F0 then simplify_bool_expr_aux e
    else (IEbinop (IOcmp Cne) (simplify_expr e1) (simplify_expr e2), false)
  | IEbinop (IOcmp c) e1 e2 =>
    (IEbinop (IOcmp c) (simplify_expr e1) (simplify_expr e2), false)
  | IEbinop (IOcmpf c) e1 e2 =>
    (IEbinop (IOcmpf c) (simplify_expr e1) (simplify_expr e2), false)
  | IEbinop op e1 e2 =>
    (IEbinop op (simplify_expr e1) (simplify_expr e2), false)
  end
with simplify_expr (e:iexpr) : iexpr :=
  let e0 := IEconst (INz F0) in
  match e with
  | IEvar _ _ | IEconst _ | IEZitv _ => e
  | IEunop op e => IEunop op (simplify_expr e)
  | IEbinop (IOcmp Ceq as op) (e as e1) (IEconst (INz z) as e2)
  | IEbinop (IOcmp Ceq as op) (IEconst (INz z) as e1) (e as e2) =>
    if Zfasteqb z F0 then
      match simplify_bool_expr_aux e with
      | (e', true) => IEbinop (IOcmp Cne) e' e0
      | (e', false) => IEbinop (IOcmp Ceq) e' e0
      end
    else IEbinop op (simplify_expr e1) (simplify_expr e2)
  | IEbinop (IOcmp Cne as op) (e as e1) (IEconst (INz z) as e2)
  | IEbinop (IOcmp Cne as op) (IEconst (INz z) as e1) (e as e2) =>
    if Zfasteqb z F0 then
      match simplify_bool_expr_aux e with
      | (e', false) => IEbinop (IOcmp Cne) e' e0
      | (e', true) => IEbinop (IOcmp Ceq) e' e0
      end
    else IEbinop op (simplify_expr e1) (simplify_expr e2)
  | IEbinop op e1 e2 => IEbinop op (simplify_expr e1) (simplify_expr e2)
  end.

Lemma simplify_expr_correct_aux:
  forall e,
    (forall ρ n, eval_iexpr ρ e (INz n) ->
     forall e' b, simplify_bool_expr_aux e = (e', b) ->
       exists n', eval_iexpr ρ e' (INz n') /\ xorb (Zcmp Ceq n 0) (Zcmp Ceq n' 0) = b)
      /\
    (forall ρ n, eval_iexpr ρ e n -> eval_iexpr ρ (simplify_expr e) n).

Lemma simplify_expr_correct:
  forall e ρ n, eval_iexpr ρ e n -> eval_iexpr ρ (simplify_expr e) n.

Definition is_bool_expr (e:iexpr) (c:query_chan) : bool :=
  match e with
  | IEbinop (IOcmp _ | IOcmpf _) _ _ => true
  | IEvar _ _ => c.(get_itv) e ⊑ NotBot (Just (Az (ZITV F0 F1)))
  | IEconst (INz z) => Zfasteqb z F0 || Zfasteqb z F1
  | _ => false
  end.

Lemma is_bool_expr_correct:
  forall e ρ n c,
    eval_iexpr ρ e (INz n) -> ρ ∈ γ c ->
    is_bool_expr e c = true ->
    n = 0 \/ n = 1.

Definition simplify_bool_expr (e:iexpr) (c:query_chan) : iexpr * bool :=
  let '(e, b) := simplify_bool_expr_aux e in
  if is_bool_expr e c then (e, b)
  else (IEbinop (IOcmp (if b then Ceq else Cne)) e (IEconst (INz F0)), false).

Lemma simplify_bool_expr_correct:
  ∀ e ρ n, eval_iexpr ρ e (INz n) ->
  ∀ c, ρ ∈ γ c ->
  ∀ e' b, simplify_bool_expr e c = (e', b) ->
    eval_iexpr ρ e' (INz (if xorb (n =? 0) b then F0 else F1)).

Section assume_unfold.

  Context {A:Type} {J:join_op A (A+⊥)} (assume:iexpr -> bool -> A * query_chan -> A+⊥).

  Definition trivial_ite_assume (e:ite_iexpr) (b:bool) (ab:A) : A+⊥ :=
    match e, b with
    | Leaf (IEconst (INz z)), false => if Zfasteqb z F1 then Bot else NotBot ab
    | Leaf (IEconst (INz z)), true => if Zfasteqb z F0 then Bot else NotBot ab
    | _, _ => NotBot ab
    end.

  Fixpoint ite_assume (fuel:nat) (e:ite_iexpr) (b:bool) (ab:A * query_chan) : A+⊥ :=
    match fuel with
    | O => ret (fst ab)
    | S fuel =>
      match e with
      | Leaf e =>
        let '(e, b') := simplify_bool_expr e (snd ab) in
        let b := xorb b b' in
        do ab' <- assume e b ab;
        match e with
          | IEvar _ x =>
            match (snd ab).(get_eq_expr) x with
              | None => ret ab'
              | Some e' => ite_assume fuel e' b (ab', snd ab)
            end
          | _ => ret ab'
        end
      | Ite c et ef =>
        let abtrue :=
          do abtrue <- trivial_ite_assume et b (fst ab);
          do abtrue <- trivial_ite_assume (Leaf c) true abtrue;
          do abtrue <- ite_assume fuel (Leaf c) true (abtrue, snd ab);
          ite_assume fuel et b (abtrue, snd ab)
        in
        let abfalse :=
          do abfalse <- trivial_ite_assume ef b (fst ab);
          do abfalse <- trivial_ite_assume (Leaf c) false abfalse;
          do abfalse <- ite_assume fuel (Leaf c) false (abfalse, snd ab);
          ite_assume fuel ef b (abfalse, snd ab)
        in
        match abtrue, abfalse with
          | Bot, x | x, Bot => x
          | NotBot ab1, NotBot ab2 => ab1 ⊔ ab2
        end
      end
    end.

  Definition ite_assume_fuel := 20%nat.
  Global Opaque ite_assume_fuel.

  Definition assume_unfold e := ite_assume ite_assume_fuel (Leaf e).

  Context (γA:gamma_op A (var -> ideal_num))
          (ρ:var -> ideal_num)
          (join_correct_ρ:forall x y:A, ρ ∈ (γ x ∪ γ y) -> ρ ∈ γ ((x ⊔ y):_+⊥))
          (assume_sound_ρ:forall e (b:bool) x,
                            ρ ∈ γ x ->
                            eval_iexpr ρ e (INz (if b then F1 else F0)) ->
                            ρ ∈ γ (assume e b x)).

  Lemma trivial_ite_assume_correct:
    forall e (b:bool) x,
      ρ ∈ γ x ->
      eval_ite_iexpr ρ e (INz (if b then F1 else F0)) ->
      ρ ∈ γ (trivial_ite_assume e b x).

  Lemma ite_assume_correct:
    forall fuel e (b:bool) ab,
      ρ ∈ γ ab ->
      eval_ite_iexpr ρ e (INz (if b then F1 else F0)) ->
      ρ ∈ γ (ite_assume fuel e b ab).

  Lemma assume_unfold_correct:
    forall e (b:bool) ab,
      ρ ∈ γ ab ->
      eval_iexpr ρ e (INz (if b then F1 else F0)) ->
      ρ ∈ γ (assume_unfold e b ab).

End assume_unfold.