Module FPExtra

Require Import Coqlib.
Require Import Compopts.
Require Import AST Integers Floats.
Require Import Op CminorSel.
Require Import OpHelpers.
Require Import SelectOp SplitLong.
Require Import Values ExtValues.
Require Import DecBoolOps.

Local Open Scope cminorsel_scope.
Local Open Scope string_scope.

Definition e_andl a b := Eop Oandl (a ::: b ::: Enil).
Definition e_addl a b := Eop Oaddl (a ::: b ::: Enil).
Definition e_orl a b := Eop Oorl (a ::: b ::: Enil).
Definition e_constl n := Eop (Olongconst (Int64.repr n)) Enil.
Definition e_float_of_longu a := Eop Ofloatoflongu (a ::: Enil).
Definition e_float_of_long a := Eop Ofloatoflong (a ::: Enil).
Definition e_single_of_float a := Eop Osingleoffloat (a ::: Enil).
Definition e_ite ty c vc v1 v2 := Eop (Osel c ty) (v1 ::: v2 ::: vc ::: Enil).
Definition e_cmpluimm c v n := Eop (Ocmp (Ccompluimm c n)) (v ::: Enil).
Definition e_absl a := Eop (Oabsdifflimm Int64.zero) (a ::: Enil).

Definition a_var := Eletvar 0%nat.

Definition e_single_of_longu a :=
  Elet a (e_single_of_float (e_float_of_longu
    (e_ite Tlong (Ccompu0 Cne) (e_cmpluimm Cle a_var (Int64.repr (2^53))) a_var
           (e_andl (e_orl a_var (e_addl (e_andl a_var (e_constl 2047))
                                        (e_constl 2047)))
                   (e_constl (-2048))))))%Z.

Theorem e_single_of_longu_correct :
  forall (ge : genv) (sp: val) cmenv memenv
         (le : letenv) (expr_a : expr) (va : val)
         (EVAL_a : eval_expr ge sp cmenv memenv le expr_a va),
  eval_expr ge sp cmenv memenv le (e_single_of_longu expr_a)
            (Val.maketotal (Val.singleoflongu va)).

Proof.

  intros.
  unfold e_single_of_longu.
  repeat econstructor. eassumption.
  cbn.
  destruct va; cbn.
  all: try reflexivity.
  f_equal.
  unfold Int64.ltu.
  change (Int64.unsigned (Int64.repr 9007199254740992))%Z with 9007199254740992%Z.
  destruct zlt as [LT | GE]; cbn.
  { change (Int.eq Int.zero Int.zero) with true. cbn.
    f_equal.
    symmetry.
    apply Float32.of_longu_double_2.
    lia.
  }
  change (Int.eq Int.one Int.zero) with false. cbn.
  f_equal.
  symmetry.
  apply Float32.of_longu_double_1.
  lia.
Qed.

Definition e_single_of_long a :=
  Elet a (e_single_of_float (e_float_of_long
    (e_ite Tlong (Ccompu0 Cne) (e_cmpluimm Cle (e_absl a_var) (Int64.repr (2^53))) a_var
           (e_andl (e_orl a_var (e_addl (e_andl a_var (e_constl 2047))
                                        (e_constl 2047)))
                   (e_constl (-2048))))))%Z.

Theorem e_single_of_long_correct :
  forall (ge : genv) (sp: val) cmenv memenv
         (le : letenv) (expr_a : expr) (va : val)
         (EVAL_a : eval_expr ge sp cmenv memenv le expr_a va),
  eval_expr ge sp cmenv memenv le (e_single_of_long expr_a)
            (Val.maketotal (Val.singleoflong va)).

Proof.

  intros.
  unfold e_single_of_long.
  repeat econstructor. eassumption.
  cbn.
  destruct va; cbn.
  all: try reflexivity.
  f_equal.
  unfold Int64.ltu.
  change (Int64.unsigned (Int64.repr 9007199254740992))%Z with 9007199254740992%Z.
  destruct zlt as [LT | GE]; cbn.
  { change (Int.eq Int.zero Int.zero) with true. cbn.
    f_equal.
    symmetry.
    apply Float32.of_long_double_2.
    unfold long_absdiff, Z_abs_diff in LT.
    change (Int64.signed Int64.zero) with 0%Z in LT.
    rewrite Z.sub_0_r in LT.
    rewrite Int64.unsigned_repr in LT.
    lia.
    pose proof (Int64.signed_range i).
    change Int64.min_signed with (-9223372036854775808)%Z in *.
    change Int64.max_signed with (9223372036854775807)%Z in *.
    change Int64.max_unsigned with (18446744073709551615)%Z.
    lia.
  }
  change (Int.eq Int.one Int.zero) with false. cbn.
  f_equal.
  symmetry.
  apply Float32.of_long_double_1.
  unfold long_absdiff, Z_abs_diff in GE.
  change (Int64.signed Int64.zero) with 0%Z in GE.
  rewrite Z.sub_0_r in GE.
  rewrite Int64.unsigned_repr in GE.
  lia.
  pose proof (Int64.signed_range i).
  change Int64.min_signed with (-9223372036854775808)%Z in *.
  change Int64.max_signed with (9223372036854775807)%Z in *.
  change Int64.max_unsigned with (18446744073709551615)%Z.
  lia.
Qed.