diff options
| author |  xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2013-07-03 15:07:17 +0000 |
|---|---|---|
| committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2013-07-03 15:07:17 +0000 |
| commit | a0aaa3552d53b20a99566ac7116063fbb31b9964 (patch) | |
| tree | 72b86341e136accdba1c339230cee0f1ba5013d9 /lib | |
| parent | 18bbf6d3cfb15219c87ebc79a5dd58bf75f2b4c4 (diff) | |
Treat casts int64 -> float32 as primitive operations instead of two
casts int64 -> float64 -> float32. The latter causes double rounding
errors.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2290 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/Floats.v | 18 |
1 files changed, 18 insertions, 0 deletions
diff --git a/lib/Floats.v b/lib/Floats.v index 3edf39c..9df4106 100644 --- a/lib/Floats.v +++ b/lib/Floats.v @@ -174,11 +174,17 @@ Definition floatofint (n:int): float := (**r conversion from signed 32-bit int * binary_normalize64 (Int.signed n) 0 false. Definition floatofintu (n:int): float:= (**r conversion from unsigned 32-bit int *) binary_normalize64 (Int.unsigned n) 0 false. + Definition floatoflong (n:int64): float := (**r conversion from signed 64-bit int *) binary_normalize64 (Int64.signed n) 0 false. Definition floatoflongu (n:int64): float:= (**r conversion from unsigned 64-bit int *) binary_normalize64 (Int64.unsigned n) 0 false. +Definition singleoflong (n:int64): float := (**r conversion from signed 64-bit int to single-precision float *) + floatofbinary32 (binary_normalize32 (Int64.signed n) 0 false). +Definition singleoflongu (n:int64): float:= (**r conversion from unsigned 64-bit int to single-precision float *) + floatofbinary32 (binary_normalize32 (Int64.unsigned n) 0 false). + Definition add: float -> float -> float := b64_plus mode_NE. (**r addition *) Definition sub: float -> float -> float := b64_minus mode_NE. (**r subtraction *) Definition mul: float -> float -> float := b64_mult mode_NE. (**r multiplication *) @@ -319,6 +325,18 @@ Proof. intros; unfold singleoffloat; rewrite binary32offloatofbinary32; reflexivity. Qed. +Theorem singleoflong_idem: + forall n, singleoffloat (singleoflong n) = singleoflong n. +Proof. + intros; unfold singleoffloat, singleoflong; rewrite binary32offloatofbinary32; reflexivity. +Qed. + +Theorem singleoflongu_idem: + forall n, singleoffloat (singleoflongu n) = singleoflongu n. +Proof. + intros; unfold singleoffloat, singleoflongu; rewrite binary32offloatofbinary32; reflexivity. +Qed. + Definition is_single (f: float) : Prop := exists s, f = floatofbinary32 s. Theorem singleoffloat_is_single: |