Require Import Coqlib.
Require Import Integers.
Require Import Values.
Require Import Floats.
Require Import Memory.
Require Import Lia.
    
Definition bits_of_float x :=
  match x with
  | Vfloat f => Vlong (Float.to_bits f)
  | _ => Vundef
  end.

Definition bits_of_single x :=
  match x with
  | Vsingle f => Vint (Float32.to_bits f)
  | _ => Vundef
  end.

Definition float_of_bits x :=
  match x with
  | Vlong f => Vfloat (Float.of_bits f)
  | _ => Vundef
  end.

Definition single_of_bits x :=
  match x with
  | Vint f => Vsingle (Float32.of_bits f)
  | _ => Vundef
  end.

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.

Lemma float_bits_normalize:
  forall v1,
  ExtValues.float_of_bits (Val.normalize (ExtValues.bits_of_float v1) AST.Tlong) =
  Val.normalize v1 AST.Tfloat.
Proof.
  destruct v1; cbn; trivial.
  f_equal.
  apply Float.of_to_bits.
Qed.

Lemma single_bits_normalize:
  forall v1,
  ExtValues.single_of_bits (Val.normalize (ExtValues.bits_of_single v1) AST.Tint) =
  Val.normalize v1 AST.Tsingle.
Proof.
  destruct v1; cbn; trivial.
  f_equal.
  apply Float32.of_to_bits.
Qed.