Module ExtValues

Require Import Coqlib.
Require Import Integers.
Require Import Values.
Require Import Floats.
Require Import Memory.
Require Import Lia.


Definition bitwise_select_long b vtrue vfalse :=
  Int64.or (Int64.and (Int64.neg b) vtrue)
           (Int64.and (Int64.sub b Int64.one) vfalse).

Lemma bitwise_select_long_true :
  forall vtrue vfalse,
    bitwise_select_long Int64.one vtrue vfalse = vtrue.

Proof.

  intros. unfold bitwise_select_long. cbn.
  change (Int64.neg Int64.one) with Int64.mone.
  rewrite Int64.and_commut.
  rewrite Int64.and_mone.
  rewrite Int64.sub_idem.
  rewrite Int64.and_commut.
  rewrite Int64.and_zero.
  apply Int64.or_zero.
Qed.

Lemma bitwise_select_long_false :
forall vtrue vfalse,
bitwise_select_long Int64.zero vtrue vfalse = vfalse.

Proof.

  intros. unfold bitwise_select_long. cbn.
  rewrite Int64.neg_zero.
  rewrite Int64.and_commut.
  rewrite Int64.and_zero.
  rewrite Int64.sub_zero_r.
  change (Int64.neg Int64.one) with Int64.mone.
  rewrite Int64.and_commut.
  rewrite Int64.and_mone.
  rewrite Int64.or_commut.
  apply Int64.or_zero.
Qed.

Definition select01_long (vb : val) (vtrue : val) (vfalse : val) : val :=
  match vb with
  | (Vint b) =>
    if Int.eq b Int.one
    then vtrue
    else if Int.eq b Int.zero
         then vfalse
         else Vundef
  | _ => Vundef
  end.

Lemma normalize_select01:
  forall x y z, Val.normalize (select01_long x y z) AST.Tlong = select01_long x (Val.normalize y AST.Tlong) (Val.normalize z AST.Tlong).

Proof.

  unfold select01_long.
  intros.
  destruct x; cbn; trivial.
  destruct (Int.eq i Int.one); trivial.
  destruct (Int.eq i Int.zero); trivial.
Qed.

Lemma select01_long_true:
forall vt vf,
select01_long Vtrue vt vf = vt.

Proof.

intros. unfold select01_long. cbn.
rewrite Int.eq_true. reflexivity.
Qed.

Lemma select01_long_false:
forall vt vf,
select01_long Vfalse vt vf = vf.

Proof.

  intros. unfold select01_long. cbn.
  rewrite Int.eq_true.
  rewrite Int.eq_false. reflexivity.
  cbv. discriminate.
Qed.