First step of float revision (#1285)

* Updated Data.Float.Base to import correct version of primitives, and Data.Float.Properties to remove the strict inequality induced via Word64.

Author: wenkokke

.travis.yml

@@ -56,7 +56,7 @@ matrix:
              cd ../ &&
              git clone https://github.com/agda/agda &&
              cd agda &&
-             git checkout e9007b49996e041760fee0b4e44ac10f2721d22c &&
+             git checkout 0f4538c8dcd175b92acd577ca0bdca232f5cd17f &&
              cabal install --only-dependencies --dry -v > $HOME/installplan.txt ;
           fi
 

CHANGELOG.md

@@ -12,6 +12,14 @@ Bug-fixes
 Non-backwards compatible changes
 --------------------------------
 
+#### Changes to floating-point arithmetic
+
+* The functions in `Data.Float.Base` were updated following changes upstream,
+  in `Agda.Builtin.Float`, see <https://github.com/agda/agda/pull/4885>.
+
+* The bitwise binary relations on floating-point numbers (`_<_`, `_≈ᵇ_`, `_==_`)
+  have been removed without replacement, as they were deeply unintuitive, e.g., `∀ x → x < -x`.
+
 #### Reflection
 
 * The representation of reflected syntax in `Reflection.Term` and

src/Data/Float.agda

@@ -12,4 +12,4 @@ module Data.Float where
 -- Re-export base definitions and decidability of equality
 
 open import Data.Float.Base public
-open import Data.Float.Properties using (_≈?_; _<?_; _≟_; _==_) public
+open import Data.Float.Properties using (_≈?_; _≟_) public

src/Data/Float/Base.agda

@@ -20,36 +20,49 @@ open import Agda.Builtin.Float public
   using (Float)
   renaming
   -- Relations
-  ( primFloatEquality          to _≡ᵇ_
-  ; primFloatLess              to _≤ᵇ_
-  ; primFloatNumericalEquality to _≈ᵇ_
-  ; primFloatNumericalLess     to _≲ᵇ_
+  ( primFloatInequality        to infix 4 _≤ᵇ_
+  ; primFloatEquality          to infix 4 _≡ᵇ_
+  ; primFloatLess              to infix 4 _<ᵇ_
+  ; primFloatIsInfinite        to isInfinite
+  ; primFloatIsNaN             to isNaN
+  ; primFloatIsNegativeZero    to isNegativeZero
+  ; primFloatIsSafeInteger     to isSafeInteger
   -- Conversions
-  ; primShowFloat     to show
-  ; primFloatToWord64 to toWord
-  ; primNatToFloat    to fromℕ
+  ; primFloatToWord64          to toWord
+  ; primNatToFloat             to fromℕ
+  ; primIntToFloat             to fromℤ
+  ; primFloatRound             to round
+  ; primFloatFloor             to ⌊_⌋
+  ; primFloatCeiling           to ⌈_⌉
+  ; primFloatToRatio           to toRatio
+  ; primRatioToFloat           to fromRatio
+  ; primFloatDecode            to decode
+  ; primFloatEncode            to encode
+  ; primShowFloat              to show
   -- Operations
-  ; primFloatPlus   to infixl 6 _+_
-  ; primFloatMinus  to infixl 6 _-_
-  ; primFloatTimes  to infixl 7 _*_
-  ; primFloatDiv    to infixl 7 _÷_
-  ; primFloatNegate to -_
-  ; primFloatSqrt   to sqrt
-  ; primRound       to round
-  ; primFloor       to ⌊_⌋
-  ; primCeiling     to ⌈_⌉
-  ; primExp         to e^_
-  ; primLog         to log
-  ; primSin         to sin
-  ; primCos         to cos
-  ; primTan         to tan
-  ; primASin        to asin
-  ; primACos        to acos
-  ; primATan        to atan
+  ; primFloatPlus              to infixl 6 _+_
+  ; primFloatMinus             to infixl 6 _-_
+  ; primFloatTimes             to infixl 7 _*_
+  ; primFloatDiv               to infixl 7 _÷_
+  ; primFloatPow               to infixl 8 _**_
+  ; primFloatNegate            to infixr 9 -_
+  ; primFloatSqrt              to sqrt
+  ; primFloatExp               to infixr 9 e^_
+  ; primFloatLog               to log
+  ; primFloatSin               to sin
+  ; primFloatCos               to cos
+  ; primFloatTan               to tan
+  ; primFloatASin              to asin
+  ; primFloatACos              to acos
+  ; primFloatATan              to atan
+  ; primFloatATan2             to atan2
+  ; primFloatSinh              to sinh
+  ; primFloatCosh              to cosh
+  ; primFloatTanh              to tanh
+  ; primFloatASinh             to asinh
+  ; primFloatACosh             to acosh
+  ; primFloatATanh             to atanh
   )
 
 _≈_ : Rel Float _
 _≈_ = Word._≈_ on toWord
-
-_<_ : Rel Float _
-_<_ = Word._<_ on toWord

src/Data/Float/Properties.agda

@@ -83,20 +83,3 @@ x ≟ y = map′ ≈⇒≡ ≈-reflexive (x ≈? y)
 
 ≡-decSetoid : DecSetoid _ _
 ≡-decSetoid = decSetoid _≟_
-
-------------------------------------------------------------------------
--- Boolean equality test.
-
-infix 4 _==_
-_==_ : Float → Float → Bool
-w₁ == w₂ = RN.⌊ w₁ ≟ w₂ ⌋
-
-------------------------------------------------------------------------
--- Properties of _<_
-
-infix 4 _<?_
-_<?_ : Decidable _<_
-_<?_ = On.decidable toWord Word._<_ Wₚ._<?_
-
-<-strictTotalOrder-≈ : StrictTotalOrder _ _ _
-<-strictTotalOrder-≈ = On.strictTotalOrder Wₚ.<-strictTotalOrder-≈ toWord