From a0aaa3552d53b20a99566ac7116063fbb31b9964 Mon Sep 17 00:00:00 2001 From: xleroy Date: Wed, 3 Jul 2013 15:07:17 +0000 Subject: 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 --- lib/Floats.v | 18 ++++++++++++++++++ 1 file changed, 18 insertions(+) (limited to 'lib') 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: -- cgit v1.2.3