From f070949a7559675af3e551e16e5cae95af5d4285 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Mon, 4 May 2020 11:51:12 +0200 Subject: Do not use the list notation `[]` The rest of the code base uses `nil`, so let's be consistent. Also, this avoids depending on `Import ListNotations`. --- lib/Floats.v | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) (limited to 'lib/Floats.v') diff --git a/lib/Floats.v b/lib/Floats.v index 13350dd0..00d00a57 100644 --- a/lib/Floats.v +++ b/lib/Floats.v @@ -223,10 +223,10 @@ Definition cons_pl (x: float) (l: list (bool * positive)) := match x with B754_nan s p _ => (s, p) :: l | _ => l end. Definition unop_nan (x: float) : {x : float | is_nan _ _ x = true} := - quiet_nan_64 (Archi.choose_nan_64 (cons_pl x [])). + quiet_nan_64 (Archi.choose_nan_64 (cons_pl x nil)). Definition binop_nan (x y: float) : {x : float | is_nan _ _ x = true} := - quiet_nan_64 (Archi.choose_nan_64 (cons_pl x (cons_pl y []))). + quiet_nan_64 (Archi.choose_nan_64 (cons_pl x (cons_pl y nil))). (** For fused multiply-add, the order in which arguments are examined to select a NaN payload varies across platforms. E.g. in [fma x y z], @@ -236,7 +236,7 @@ Definition binop_nan (x y: float) : {x : float | is_nan _ _ x = true} := Definition fma_nan_1 (x y z: float) : {x : float | is_nan _ _ x = true} := let '(a, b, c) := Archi.fma_order x y z in - quiet_nan_64 (Archi.choose_nan_64 (cons_pl a (cons_pl b (cons_pl c [])))). + quiet_nan_64 (Archi.choose_nan_64 (cons_pl a (cons_pl b (cons_pl c nil)))). (** One last wrinkle for fused multiply-add: [fma zero infinity nan] can return either the quiesced [nan], or the default NaN arising out @@ -248,7 +248,7 @@ Definition fma_nan (x y z: float) : {x : float | is_nan _ _ x = true} := match x, y with | B754_infinity _, B754_zero _ | B754_zero _, B754_infinity _ => if Archi.fma_invalid_mul_is_nan - then quiet_nan_64 (Archi.choose_nan_64 (Archi.default_nan_64 :: cons_pl z [])) + then quiet_nan_64 (Archi.choose_nan_64 (Archi.default_nan_64 :: cons_pl z nil)) else fma_nan_1 x y z | _, _ => fma_nan_1 x y z @@ -1011,20 +1011,20 @@ Definition cons_pl (x: float32) (l: list (bool * positive)) := match x with B754_nan s p _ => (s, p) :: l | _ => l end. Definition unop_nan (x: float32) : {x : float32 | is_nan _ _ x = true} := - quiet_nan_32 (Archi.choose_nan_32 (cons_pl x [])). + quiet_nan_32 (Archi.choose_nan_32 (cons_pl x nil)). Definition binop_nan (x y: float32) : {x : float32 | is_nan _ _ x = true} := - quiet_nan_32 (Archi.choose_nan_32 (cons_pl x (cons_pl y []))). + quiet_nan_32 (Archi.choose_nan_32 (cons_pl x (cons_pl y nil))). Definition fma_nan_1 (x y z: float32) : {x : float32 | is_nan _ _ x = true} := let '(a, b, c) := Archi.fma_order x y z in - quiet_nan_32 (Archi.choose_nan_32 (cons_pl a (cons_pl b (cons_pl c [])))). + quiet_nan_32 (Archi.choose_nan_32 (cons_pl a (cons_pl b (cons_pl c nil)))). Definition fma_nan (x y z: float32) : {x : float32 | is_nan _ _ x = true} := match x, y with | B754_infinity _, B754_zero _ | B754_zero _, B754_infinity _ => if Archi.fma_invalid_mul_is_nan - then quiet_nan_32 (Archi.choose_nan_32 (Archi.default_nan_32 :: cons_pl z [])) + then quiet_nan_32 (Archi.choose_nan_32 (Archi.default_nan_32 :: cons_pl z nil)) else fma_nan_1 x y z | _, _ => fma_nan_1 x y z -- cgit From 65ad896aed67aa06845e0b2ac9f7f98179f6e170 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Mon, 4 May 2020 12:03:05 +0200 Subject: Revert "Do not use the list notation `[]`" On some versions of Coq, "nil" is of type "Rlist"... This reverts commit f070949a7559675af3e551e16e5cae95af5d4285. --- lib/Floats.v | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) (limited to 'lib/Floats.v') diff --git a/lib/Floats.v b/lib/Floats.v index 00d00a57..13350dd0 100644 --- a/lib/Floats.v +++ b/lib/Floats.v @@ -223,10 +223,10 @@ Definition cons_pl (x: float) (l: list (bool * positive)) := match x with B754_nan s p _ => (s, p) :: l | _ => l end. Definition unop_nan (x: float) : {x : float | is_nan _ _ x = true} := - quiet_nan_64 (Archi.choose_nan_64 (cons_pl x nil)). + quiet_nan_64 (Archi.choose_nan_64 (cons_pl x [])). Definition binop_nan (x y: float) : {x : float | is_nan _ _ x = true} := - quiet_nan_64 (Archi.choose_nan_64 (cons_pl x (cons_pl y nil))). + quiet_nan_64 (Archi.choose_nan_64 (cons_pl x (cons_pl y []))). (** For fused multiply-add, the order in which arguments are examined to select a NaN payload varies across platforms. E.g. in [fma x y z], @@ -236,7 +236,7 @@ Definition binop_nan (x y: float) : {x : float | is_nan _ _ x = true} := Definition fma_nan_1 (x y z: float) : {x : float | is_nan _ _ x = true} := let '(a, b, c) := Archi.fma_order x y z in - quiet_nan_64 (Archi.choose_nan_64 (cons_pl a (cons_pl b (cons_pl c nil)))). + quiet_nan_64 (Archi.choose_nan_64 (cons_pl a (cons_pl b (cons_pl c [])))). (** One last wrinkle for fused multiply-add: [fma zero infinity nan] can return either the quiesced [nan], or the default NaN arising out @@ -248,7 +248,7 @@ Definition fma_nan (x y z: float) : {x : float | is_nan _ _ x = true} := match x, y with | B754_infinity _, B754_zero _ | B754_zero _, B754_infinity _ => if Archi.fma_invalid_mul_is_nan - then quiet_nan_64 (Archi.choose_nan_64 (Archi.default_nan_64 :: cons_pl z nil)) + then quiet_nan_64 (Archi.choose_nan_64 (Archi.default_nan_64 :: cons_pl z [])) else fma_nan_1 x y z | _, _ => fma_nan_1 x y z @@ -1011,20 +1011,20 @@ Definition cons_pl (x: float32) (l: list (bool * positive)) := match x with B754_nan s p _ => (s, p) :: l | _ => l end. Definition unop_nan (x: float32) : {x : float32 | is_nan _ _ x = true} := - quiet_nan_32 (Archi.choose_nan_32 (cons_pl x nil)). + quiet_nan_32 (Archi.choose_nan_32 (cons_pl x [])). Definition binop_nan (x y: float32) : {x : float32 | is_nan _ _ x = true} := - quiet_nan_32 (Archi.choose_nan_32 (cons_pl x (cons_pl y nil))). + quiet_nan_32 (Archi.choose_nan_32 (cons_pl x (cons_pl y []))). Definition fma_nan_1 (x y z: float32) : {x : float32 | is_nan _ _ x = true} := let '(a, b, c) := Archi.fma_order x y z in - quiet_nan_32 (Archi.choose_nan_32 (cons_pl a (cons_pl b (cons_pl c nil)))). + quiet_nan_32 (Archi.choose_nan_32 (cons_pl a (cons_pl b (cons_pl c [])))). Definition fma_nan (x y z: float32) : {x : float32 | is_nan _ _ x = true} := match x, y with | B754_infinity _, B754_zero _ | B754_zero _, B754_infinity _ => if Archi.fma_invalid_mul_is_nan - then quiet_nan_32 (Archi.choose_nan_32 (Archi.default_nan_32 :: cons_pl z nil)) + then quiet_nan_32 (Archi.choose_nan_32 (Archi.default_nan_32 :: cons_pl z [])) else fma_nan_1 x y z | _, _ => fma_nan_1 x y z -- cgit From e464549037dcf94494c5aea462e6c3854b44976d Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Mon, 4 May 2020 12:04:38 +0200 Subject: Import ListNotations explicitly So as not to depend on an implicit import from module Program. (See PR #352.) --- lib/Floats.v | 1 + 1 file changed, 1 insertion(+) (limited to 'lib/Floats.v') diff --git a/lib/Floats.v b/lib/Floats.v index 13350dd0..6a126c3f 100644 --- a/lib/Floats.v +++ b/lib/Floats.v @@ -22,6 +22,7 @@ Require Import Binary Bits Core. Require Import IEEE754_extra. Require Import Program. Require Archi. +Import ListNotations. Close Scope R_scope. Open Scope Z_scope. -- cgit From ab0d9476db875a82cf293623d18552b62f239d5c Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Mon, 21 Sep 2020 14:15:57 +0200 Subject: Support the use of already-installed MenhirLib and Flocq libraries configure flags -use-external-Flocq and -use external-MenhirLib. --- lib/Floats.v | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) (limited to 'lib/Floats.v') diff --git a/lib/Floats.v b/lib/Floats.v index 6a126c3f..b7769420 100644 --- a/lib/Floats.v +++ b/lib/Floats.v @@ -17,8 +17,7 @@ (** Formalization of floating-point numbers, using the Flocq library. *) Require Import Coqlib Zbits Integers. -(*From Flocq*) -Require Import Binary Bits Core. +From Flocq Require Import Binary Bits Core. Require Import IEEE754_extra. Require Import Program. Require Archi. -- cgit