------------------------------------------------------------------------
-- The Agda standard library
--
-- Properties of operations on floats
------------------------------------------------------------------------

{-# OPTIONS --cubical-compatible --safe #-}

module Data.Float.Properties where

open import Data.Bool.Base as Bool using (Bool)
open import Data.Float.Base
import Data.Maybe.Base as Maybe
import Data.Maybe.Properties as Maybe
import Data.Nat.Properties as 
import Data.Word64.Base as Word64
import Data.Word64.Properties as Word64
open import Function.Base using (_∘_)
open import Relation.Nullary.Decidable as RN using (map′)
open import Relation.Binary.Core using (_⇒_)
open import Relation.Binary.Bundles using (Setoid; DecSetoid)
open import Relation.Binary.Structures
  using (IsEquivalence; IsDecEquivalence)
open import Relation.Binary.Definitions
  using (Reflexive; Symmetric; Transitive; Substitutive; Decidable; DecidableEquality)
import Relation.Binary.Construct.On as On
open import Relation.Binary.PropositionalEquality.Core
  using (_≡_; refl; cong; sym; trans; subst)
open import Relation.Binary.PropositionalEquality.Properties
  using (setoid; decSetoid)

------------------------------------------------------------------------
-- Primitive properties

open import Agda.Builtin.Float.Properties
  renaming (primFloatToWord64Injective to toWord64-injective)
  public

------------------------------------------------------------------------
-- Properties of _≈_

≈⇒≡ : _≈_  _≡_
≈⇒≡ eq = toWord64-injective _ _ (Maybe.map-injective Word64.≈⇒≡ eq)

≈-reflexive : _≡_  _≈_
≈-reflexive eq = cong (Maybe.map Word64.toℕ  toWord64) eq

≈-refl : Reflexive _≈_
≈-refl = refl

≈-sym : Symmetric _≈_
≈-sym = sym

≈-trans : Transitive _≈_
≈-trans = trans

≈-subst :  {}  Substitutive _≈_ 
≈-subst P x≈y p = subst P (≈⇒≡ x≈y) p

infix 4 _≈?_
_≈?_ : Decidable _≈_
_≈?_ = On.decidable (Maybe.map Word64.toℕ  toWord64) _≡_ (Maybe.≡-dec ℕ._≟_)

≈-isEquivalence : IsEquivalence _≈_
≈-isEquivalence = record
  { refl  = λ {i}  ≈-refl {i}
  ; sym   = λ {i j}  ≈-sym {i} {j}
  ; trans = λ {i j k}  ≈-trans {i} {j} {k}
  }

≈-setoid : Setoid _ _
≈-setoid = record
  { isEquivalence = ≈-isEquivalence
  }

≈-isDecEquivalence : IsDecEquivalence _≈_
≈-isDecEquivalence = record
  { isEquivalence = ≈-isEquivalence
  ; _≟_           = _≈?_
  }

≈-decSetoid : DecSetoid _ _
≈-decSetoid = record
  { isDecEquivalence = ≈-isDecEquivalence
  }
------------------------------------------------------------------------
-- Properties of _≡_

infix 4 _≟_
_≟_ : DecidableEquality Float
x  y = map′ ≈⇒≡ ≈-reflexive (x ≈? y)

≡-setoid : Setoid _ _
≡-setoid = setoid Float

≡-decSetoid : DecSetoid _ _
≡-decSetoid = decSetoid _≟_


------------------------------------------------------------------------
-- DEPRECATIONS

toWord-injective = toWord64-injective
{-# WARNING_ON_USAGE toWord-injective
"Warning: toWord-injective was deprecated in v2.1.
Please use toWord64-injective instead."
#-}