From d18b928154a48ff8d90aaff69eca7d6eb3dfa0ab Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Tue, 28 Aug 2018 18:56:07 +0200 Subject: Implement classify on primitive float --- test-suite/primitive/float/classify.v | 23 +++++++++++++++++++++++ 1 file changed, 23 insertions(+) create mode 100644 test-suite/primitive/float/classify.v (limited to 'test-suite/primitive/float/classify.v') diff --git a/test-suite/primitive/float/classify.v b/test-suite/primitive/float/classify.v new file mode 100644 index 0000000000..e4373415cb --- /dev/null +++ b/test-suite/primitive/float/classify.v @@ -0,0 +1,23 @@ +Require Import ZArith Floats. + +Definition epsilon := Eval compute in ldexp one (-1024)%Z. + +Check (eq_refl : classify one = PNormal). +Check (eq_refl : classify (- one)%float = NNormal). +Check (eq_refl : classify epsilon = PSubn). +Check (eq_refl : classify (- epsilon)%float = NSubn). +Check (eq_refl : classify zero = PZero). +Check (eq_refl : classify neg_zero = NZero). +Check (eq_refl : classify infinity = PInf). +Check (eq_refl : classify neg_infinity = NInf). +Check (eq_refl : classify nan = NaN). + +Check (eq_refl PNormal <: classify one = PNormal). +Check (eq_refl NNormal <: classify (- one)%float = NNormal). +Check (eq_refl PSubn <: classify epsilon = PSubn). +Check (eq_refl NSubn <: classify (- epsilon)%float = NSubn). +Check (eq_refl PZero <: classify zero = PZero). +Check (eq_refl NZero <: classify neg_zero = NZero). +Check (eq_refl PInf <: classify infinity = PInf). +Check (eq_refl NInf <: classify neg_infinity = NInf). +Check (eq_refl NaN <: classify nan = NaN). -- cgit v1.2.3 From f0bf1511e59e528e090a87cfcc220f93c2431ecd Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Sun, 9 Jun 2019 10:41:10 +0200 Subject: Add tests for primitive floats with 'native_compute' Tests are updated to include native computations. --- test-suite/primitive/float/classify.v | 10 ++++++++++ 1 file changed, 10 insertions(+) (limited to 'test-suite/primitive/float/classify.v') diff --git a/test-suite/primitive/float/classify.v b/test-suite/primitive/float/classify.v index e4373415cb..22e3fca844 100644 --- a/test-suite/primitive/float/classify.v +++ b/test-suite/primitive/float/classify.v @@ -21,3 +21,13 @@ Check (eq_refl NZero <: classify neg_zero = NZero). Check (eq_refl PInf <: classify infinity = PInf). Check (eq_refl NInf <: classify neg_infinity = NInf). Check (eq_refl NaN <: classify nan = NaN). + +Check (eq_refl PNormal <<: classify one = PNormal). +Check (eq_refl NNormal <<: classify (- one)%float = NNormal). +Check (eq_refl PSubn <<: classify epsilon = PSubn). +Check (eq_refl NSubn <<: classify (- epsilon)%float = NSubn). +Check (eq_refl PZero <<: classify zero = PZero). +Check (eq_refl NZero <<: classify neg_zero = NZero). +Check (eq_refl PInf <<: classify infinity = PInf). +Check (eq_refl NInf <<: classify neg_infinity = NInf). +Check (eq_refl NaN <<: classify nan = NaN). -- cgit v1.2.3