Require Import Coqlib.
Require Import Integers.
Require Import Values.
Require Import Floats.

Definition bitwise_select_int b vtrue vfalse :=
  Val.or (Val.and (Val.neg b) vtrue)
         (Val.and (Val.sub b Vone) vfalse).

Lemma bitwise_select_int_true :
  forall vtrue vfalse,
    bitwise_select_int (Val.of_optbool (Some true)) (Vint vtrue) (Vint vfalse)
    = Vint vtrue.
Proof.
  intros. cbn. f_equal.
  change (Int.neg Int.one) with Int.mone.
  rewrite Int.and_commut.
  rewrite Int.and_mone.
  rewrite Int.sub_idem.
  rewrite Int.and_commut.
  rewrite Int.and_zero.
  apply Int.or_zero.
Qed.

Lemma bitwise_select_int_false :
  forall vtrue vfalse,
    bitwise_select_int (Val.of_optbool (Some false)) (Vint vtrue) (Vint vfalse)
    = Vint vfalse.
Proof.
  intros. cbn. f_equal.
  rewrite Int.neg_zero.
  rewrite Int.and_commut.
  rewrite Int.and_zero.
  rewrite Int.sub_zero_r.
  change (Int.neg Int.one) with Int.mone.
  rewrite Int.and_commut.
  rewrite Int.and_mone.
  rewrite Int.or_commut.
  apply Int.or_zero.
Qed.

Definition bitwise_select_long b vtrue vfalse :=
  let b' := Val.longofint b in
  Val.orl (Val.andl (Val.negl b') vtrue)
          (Val.andl (Val.subl b' (Vlong Int64.one)) vfalse).

Lemma bitwise_select_long_true :
  forall vtrue vfalse,
    bitwise_select_long (Val.of_optbool (Some true)) (Vlong vtrue) (Vlong vfalse)
    = Vlong vtrue.
Proof.
  intros. cbn. f_equal.
  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 (Val.of_optbool (Some false)) (Vlong vtrue) (Vlong vfalse)
    = Vlong vfalse.
Proof.
  intros. cbn. f_equal.
  change (Int64.repr (Int.signed Int.zero)) with Int64.zero.
  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.