open import 1Lab.Type

open import Data.Maybe.Base
open import Data.Word.Base
open import Data.Dec.Base
open import Data.Int.Base
open import Data.Id.Base

module Data.Float.Base where

headerπŸ”—

postulate Float : Type
{-# BUILTIN FLOAT Float #-}

private module P where primitive
  -- Relations
  primFloatInequality        : Float β†’ Float β†’ Bool
  primFloatEquality          : Float β†’ Float β†’ Bool
  primFloatLess              : Float β†’ Float β†’ Bool
  primFloatIsInfinite        : Float β†’ Bool
  primFloatIsNaN             : Float β†’ Bool
  primFloatIsNegativeZero    : Float β†’ Bool
  primFloatIsSafeInteger     : Float β†’ Bool
  -- Conversions
  primFloatToWord64          : Float β†’ Maybe Word64
  primFloatToWord64Injective : βˆ€ a b β†’ primFloatToWord64 a ≑ᡒ primFloatToWord64 b β†’ a ≑ᡒ b
  primNatToFloat             : Nat β†’ Float
  primIntToFloat             : Int β†’ Float
  primFloatRound             : Float β†’ Maybe Int
  primFloatFloor             : Float β†’ Maybe Int
  primFloatCeiling           : Float β†’ Maybe Int
  primFloatToRatio           : Float β†’ (Ξ£ Int Ξ» _ β†’ Int)
  primRatioToFloat           : Int β†’ Int β†’ Float
  primFloatDecode            : Float β†’ Maybe (Ξ£ Int Ξ» _ β†’ Int)
  primFloatEncode            : Int β†’ Int β†’ Maybe Float
  -- Operations
  primFloatPlus              : Float β†’ Float β†’ Float
  primFloatMinus             : Float β†’ Float β†’ Float
  primFloatTimes             : Float β†’ Float β†’ Float
  primFloatDiv               : Float β†’ Float β†’ Float
  primFloatPow               : Float β†’ Float β†’ Float
  primFloatNegate            : Float β†’ Float
  primFloatSqrt              : Float β†’ Float
  primFloatExp               : Float β†’ Float
  primFloatLog               : Float β†’ Float
  primFloatSin               : Float β†’ Float
  primFloatCos               : Float β†’ Float
  primFloatTan               : Float β†’ Float
  primFloatASin              : Float β†’ Float
  primFloatACos              : Float β†’ Float
  primFloatATan              : Float β†’ Float
  primFloatATan2             : Float β†’ Float β†’ Float
  primFloatSinh              : Float β†’ Float
  primFloatCosh              : Float β†’ Float
  primFloatTanh              : Float β†’ Float
  primFloatASinh             : Float β†’ Float
  primFloatACosh             : Float β†’ Float
  primFloatATanh             : Float β†’ Float

open P public renaming
  ( primFloatInequality to _float≠_
  ; primFloatEquality   to _float=_
  ; primFloatLess       to _float<_

  ; primFloatIsInfinite     to is-infinite?
  ; primFloatIsNaN          to is-nan?
  ; primFloatIsNegativeZero to is-neg0?
  ; primFloatIsSafeInteger  to is-integer?

  ; primFloatToWord64       to float→word64
  ; primNatToFloat          to nat→float
  ; primIntToFloat          to int→float
  ; primFloatRound          to round
  ; primFloatFloor          to floor
  ; primFloatCeiling        to ceiling
  ; primFloatToRatio        to float→ratio
  ; primRatioToFloat        to ratio→float

  ; primFloatDecode         to decode-float
  ; primFloatEncode         to encode-float

  ; primFloatPlus           to _+,_
  ; primFloatMinus          to _-,_
  ; primFloatTimes          to _*,_
  ; primFloatDiv            to _/,_
  )
  using ()

instance
  Discrete-Float : Discrete Float
  Discrete-Float  = Discrete-inj' _ (P.primFloatToWord64Injective _ _)

  Number-Float : Number Float
  Number-Float .Number.Constraint _ = ⊀
  Number-Float .Number.fromNat s = nat→float s