From 362f2f36a44fa6ab4fe28264ed572d721adece70 Mon Sep 17 00:00:00 2001 From: xleroy Date: Fri, 3 Jan 2014 17:09:54 +0000 Subject: Introduce and use the platform-specific Archi module giving: - endianness - alignment constraints for 8-byte types (which is 4 for x86 ABI and 8 for other ABIs) - NaN handling options (superceding the Nan module, removed). git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2402 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- lib/Floats.v | 13 ++++++------- 1 file changed, 6 insertions(+), 7 deletions(-) (limited to 'lib') diff --git a/lib/Floats.v b/lib/Floats.v index 0a30836..5502927 100644 --- a/lib/Floats.v +++ b/lib/Floats.v @@ -26,6 +26,7 @@ Require Import Fcalc_round. Require Import Fcalc_bracket. Require Import Fprop_Sterbenz. Require Import Program. +Require Archi. Close Scope R_scope. @@ -268,18 +269,15 @@ Definition singleoflongu (n:int64): float:= (**r conversion from unsigned 64-bit - a choice function determining which of the payload arguments to choose, when an operation is given two NaN arguments. *) -Parameter default_pl : bool*nan_pl 53. -Parameter choose_binop_pl : bool -> nan_pl 53 -> bool -> nan_pl 53 -> bool. - Definition binop_pl (x y: binary64) : bool*nan_pl 53 := match x, y with | B754_nan s1 pl1, B754_nan s2 pl2 => - if choose_binop_pl s1 pl1 s2 pl2 + if Archi.choose_binop_pl s1 pl1 s2 pl2 then (s2, transform_quiet_pl pl2) else (s1, transform_quiet_pl pl1) | B754_nan s1 pl1, _ => (s1, transform_quiet_pl pl1) | _, B754_nan s2 pl2 => (s2, transform_quiet_pl pl2) - | _, _ => default_pl + | _, _ => Archi.default_pl end. Definition add: float -> float -> float := b64_plus binop_pl mode_NE. (**r addition *) @@ -1235,8 +1233,9 @@ Proof. etransitivity. apply H. symmetry. etransitivity. apply H0. f_equal. destruct Bsign; reflexivity. - - destruct f as [[]|[]| |]; try discriminate; try reflexivity. - simpl. destruct (choose_binop_pl b n b n); auto. + - destruct f as [[]|[]| |]; try discriminate; simpl. + auto. auto. auto. auto. + destruct (Archi.choose_binop_pl b n b n); auto. Qed. Program Definition pow2_float (b:bool) (e:Z) (H:-1023 < e < 1023) : float := -- cgit v1.2.3