{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE CPP #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE DeriveLift #-}
{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}

{- HLINT ignore "Unused LANGUAGE pragma" -}

-- |
-- Module      :   Grisette.Internal.SymPrim.FP
-- Copyright   :   (c) Sirui Lu 2024
-- License     :   BSD-3-Clause (see the LICENSE file)
--
-- Maintainer  :   siruilu@cs.washington.edu
-- Stability   :   Experimental
-- Portability :   GHC only
module Grisette.Internal.SymPrim.FP
  ( ValidFP,
    FP (..),
    FP16,
    FP32,
    FP64,
    withValidFPProofs,
    FPRoundingMode (..),
    allFPRoundingMode,
    NotRepresentableFPError (..),
    ConvertibleBound (..),
    nextFP,
    prevFP,
    withUnsafeValidFP,
    checkDynamicValidFP,
    invalidFPMessage,
  )
where

import Control.DeepSeq (NFData (rnf))
import Control.Exception (Exception, throw)
import qualified Data.Binary as Binary
import Data.Bits (Bits (complement, shiftL, shiftR, xor, (.&.)))
import Data.Bytes.Serial (Serial (deserialize, serialize))
import Data.Hashable (Hashable (hashWithSalt))
import Data.Int (Int16, Int32, Int64)
import Data.Maybe (fromJust)
import Data.Proxy (Proxy (Proxy))
import Data.Ratio (numerator)
import Data.SBV
  ( BVIsNonZero,
    FloatingPoint,
    SWord,
    SymVal (literal, unliteral),
    ValidFloat,
    Word16,
    Word32,
    Word64,
    denominator,
    infinity,
    nan,
    sFloatingPointAsSWord,
    sWordAsSFloatingPoint,
  )
import Data.SBV.Float (fpEncodeFloat)
import qualified Data.SBV.Float as SBVF
import qualified Data.SBV.Internals as SBVI
import qualified Data.Serialize as Cereal
import Data.Type.Bool (type (&&), type (||))
import Data.Type.Equality (type (:~:) (Refl), type (==))
import GHC.Exception (Exception (displayException))
import GHC.Generics (Generic)
import GHC.Natural (Natural)
import GHC.TypeNats
  ( CmpNat,
    KnownNat,
    Nat,
    natVal,
    type (+),
    type (<=),
  )
import Grisette.Internal.Core.Data.Class.BitCast
  ( BitCast (bitCast),
    BitCastCanonical (bitCastCanonicalValue),
    BitCastOr (bitCastOr),
    bitCastOrCanonical,
  )
import Grisette.Internal.Core.Data.Class.BitVector (SizedBV (sizedBVConcat))
import Grisette.Internal.Core.Data.Class.Function (Apply (FunType, apply))
import Grisette.Internal.Core.Data.Class.IEEEFP
  ( IEEEFPConstants
      ( fpMaxNormalized,
        fpMaxSubnormal,
        fpMinNormalized,
        fpMinSubnormal,
        fpNaN,
        fpNegativeInfinite,
        fpNegativeZero,
        fpPositiveInfinite,
        fpPositiveZero
      ),
    IEEEFPConvertible (fromFPOr, toFP),
    IEEEFPOp
      ( fpAbs,
        fpMaximum,
        fpMaximumNumber,
        fpMinimum,
        fpMinimumNumber,
        fpNeg,
        fpRem
      ),
    IEEEFPRoundingMode (rna, rne, rtn, rtp, rtz),
    IEEEFPRoundingOp (fpAdd, fpDiv, fpFMA, fpMul, fpRoundToIntegral, fpSqrt, fpSub),
    IEEEFPToAlgReal,
    fpIsInfinite,
    fpIsNaN,
    fpIsNegativeInfinite,
    fpIsNegativeZero,
    fpIsPositiveInfinite,
    fpIsPositiveZero,
    fpIsZero,
  )
import Grisette.Internal.SymPrim.AlgReal
  ( AlgReal (AlgExactRational),
    UnsupportedAlgRealOperation (UnsupportedAlgRealOperation, msg, op),
  )
import Grisette.Internal.SymPrim.BV (IntN, WordN, WordN16, WordN32, WordN64)
import Grisette.Internal.Utils.Parameterized
  ( KnownProof (KnownProof),
    knownAdd,
    unsafeAxiom,
    unsafeLeqProof,
    withKnownProof,
    withLeqProof,
  )
import Language.Haskell.TH.Syntax (Lift (liftTyped))
import LibBF
  ( BFOpts,
    BigFloat,
    RoundMode,
    Status,
    allowSubnormal,
    bfAdd,
    bfDiv,
    bfFMA,
    bfFromInteger,
    bfIsInf,
    bfIsNaN,
    bfIsNeg,
    bfIsPos,
    bfIsZero,
    bfMul,
    bfNaN,
    bfNegInf,
    bfNegZero,
    bfPosInf,
    bfPosZero,
    bfRoundFloat,
    bfRoundInt,
    bfSqrt,
    bfSub,
    expBits,
    precBits,
    rnd,
    pattern NearAway,
    pattern NearEven,
    pattern ToNegInf,
    pattern ToPosInf,
    pattern ToZero,
  )
import Test.QuickCheck (frequency, oneof)
import qualified Test.QuickCheck as QC

-- $setup
-- >>> import Grisette.Core
-- >>> import Grisette.SymPrim
-- >>> import Grisette.Backend
-- >>> import Data.Proxy

bvIsNonZeroFromGEq1 ::
  forall w r proxy.
  (1 <= w) =>
  proxy w ->
  ((BVIsNonZero w) => r) ->
  r
bvIsNonZeroFromGEq1 _ r1 = case unsafeAxiom :: w :~: 1 of
  Refl -> r1

-- | A type-level proof that the given bit-widths are valid for a floating-point
-- number.
type ValidFP (eb :: Nat) (sb :: Nat) = ValidFloat eb sb

-- | Check if the given floating-point type is valid.
checkDynamicValidFP :: Natural -> Natural -> Bool
checkDynamicValidFP eb sb =
  eb >= 2 && eb <= 61 && sb >= 2 && sb <= 4611686018427387902

-- | A message thrown when the floating-point type is invalid.
invalidFPMessage :: String
invalidFPMessage =
  "Invalid floating point type `SFloatingPoint eb sb'\n`n"
    <> "  A valid float of type 'SFloatingPoint eb sb' must satisfy:\n"
    <> "        eb `elem` [2 .. 61]\n"
    <> "        sb `elem` [2 .. 4611686018427387902]\n\n"
    <> "  Given type falls outside of this range, or the sizes are not known naturals."

#if MIN_VERSION_sbv(12,0,0)
-- | Provide an (unsafe) type-level proof that the given floating-point type is
-- valid.
withUnsafeValidFP ::
  forall eb sb r. (KnownNat eb, KnownNat sb) => ((ValidFP eb sb) => r) -> r
withUnsafeValidFP r =
  let eb = natVal (Proxy @eb)
      sb = natVal (Proxy @sb)
   in if checkDynamicValidFP eb sb
        then case unsafeAxiom @True
          @( ((CmpNat eb 2 == 'EQ) || (CmpNat eb 2 == 'GT))
               && ( ((CmpNat eb 29 == 'EQ) || (CmpNat eb 29 == 'LT))
                      && ( ((CmpNat sb 2 == 'EQ) || (CmpNat sb 2 == 'GT))
                             && ( (CmpNat sb 1073741822 == 'EQ)
                                    || (CmpNat sb 1073741822 == 'LT)
                                )
                         )
                  )
           ) of
          Refl -> r
        else error invalidFPMessage
#else
-- | Provide an (unsafe) type-level proof that the given floating-point type is
-- valid.
withUnsafeValidFP ::
  forall eb sb r. (KnownNat eb, KnownNat sb) => ((ValidFP eb sb) => r) -> r
withUnsafeValidFP r =
  let eb = natVal (Proxy @eb)
      sb = natVal (Proxy @sb)
   in if checkDynamicValidFP eb sb
        then case unsafeAxiom @True
          @( ((CmpNat eb 2 == 'EQ) || (CmpNat eb 2 == 'GT))
               && ( ((CmpNat eb 61 == 'EQ) || (CmpNat eb 61 == 'LT))
                      && ( ((CmpNat sb 2 == 'EQ) || (CmpNat sb 2 == 'GT))
                             && ( (CmpNat sb 4611686018427387902 == 'EQ)
                                    || (CmpNat sb 4611686018427387902 == 'LT)
                                )
                         )
                  )
           ) of
          Refl -> r
        else error invalidFPMessage
#endif

-- | IEEE 754 floating-point number with @eb@ exponent bits and @sb@ significand
-- bits.
--
-- >>> 1.0 + 2.0 :: FP 11 53
-- 3.0
--
-- More operations are available. Please refer to "Grisette.Core#g:symops" for
-- more information.
newtype FP (eb :: Nat) (sb :: Nat) = FP {unFP :: FloatingPoint eb sb}
  deriving newtype (Eq, Show)

-- Workaround for https://github.com/GaloisInc/libBF-hs/pull/32, which affects
-- the correctness of the Ord instance for 'Data.SBV.FloatingPoint'.
instance (ValidFP eb sb) => Ord (FP eb sb) where
  FP x < FP y | isNaN x || isNaN y = False
  FP x < FP y = x < y
  FP x <= FP y | isNaN x || isNaN y = False
  FP x <= FP y = x <= y
  FP x > FP y | isNaN x || isNaN y = False
  FP x > FP y = x > y
  FP x >= FP y | isNaN x || isNaN y = False
  FP x >= FP y = x >= y

-- | IEEE 754 half-precision floating-point number.
type FP16 = FP 5 11

-- | IEEE 754 single-precision floating-point number.
type FP32 = FP 8 24

-- | IEEE 754 double-precision floating-point number.
type FP64 = FP 11 53

-- | Some type-level witnesses that could be derived from 'ValidFP'.
withValidFPProofs ::
  forall eb sb r.
  (ValidFP eb sb) =>
  ( ( KnownNat (eb + sb),
      BVIsNonZero (eb + sb),
      1 <= eb + sb,
      1 <= eb,
      1 <= sb
    ) =>
    r
  ) ->
  r
withValidFPProofs r =
  withKnownProof (knownAdd (KnownProof @eb) (KnownProof @sb)) $
    withLeqProof (unsafeLeqProof @1 @(eb + sb)) $
      withLeqProof (unsafeLeqProof @1 @eb) $
        withLeqProof (unsafeLeqProof @1 @sb) $
          bvIsNonZeroFromGEq1 (Proxy @(eb + sb)) r

instance (ValidFP eb sb, r ~ (eb + sb)) => BitCast (WordN r) (FP eb sb) where
  bitCast v = FP fp
    where
      sword :: SWord r
      sword = withValidFPProofs @eb @sb fromIntegral v
      fp :: FloatingPoint eb sb
      fp =
        withValidFPProofs @eb @sb $
          fromJust $
            unliteral $
              sWordAsSFloatingPoint sword

instance (ValidFP eb sb, r ~ (eb + sb)) => BitCast (IntN r) (FP eb sb) where
  bitCast x = withValidFPProofs @eb @sb $ bitCast (bitCast x :: WordN (eb + sb))

#define BITCAST_VIA_INTERMEDIATE(from, to, intermediate) \
  instance BitCast (from) (to) where \
    bitCast x = bitCast (bitCast x :: intermediate)

#if 1
BITCAST_VIA_INTERMEDIATE(Double, FP64, WordN 64)
BITCAST_VIA_INTERMEDIATE(Int64, FP64, WordN 64)
BITCAST_VIA_INTERMEDIATE(Word64, FP64, WordN 64)

BITCAST_VIA_INTERMEDIATE(Float, FP32, WordN 32)
BITCAST_VIA_INTERMEDIATE(Int32, FP32, WordN 32)
BITCAST_VIA_INTERMEDIATE(Word32, FP32, WordN 32)

BITCAST_VIA_INTERMEDIATE(Word16, FP16, WordN 16)
BITCAST_VIA_INTERMEDIATE(Int16, FP16, WordN 16)
#endif
instance NFData (FP eb sb) where
  rnf (FP x) = x `seq` ()

instance (ValidFP eb sb) => Lift (FP eb sb) where
  liftTyped fp = [||bitCast wordnValue||]
    where
      wordnValue = bitCastOrCanonical fp :: WordN (eb + sb)

instance (ValidFP eb sb) => Hashable (FP eb sb) where
  hashWithSalt salt x =
    hashWithSalt salt (bitCastOrCanonical x :: WordN (eb + sb))

deriving newtype instance (ValidFloat eb sb) => Num (FP eb sb)

deriving newtype instance (ValidFloat eb sb) => Fractional (FP eb sb)

deriving newtype instance (ValidFloat eb sb) => Floating (FP eb sb)

deriving newtype instance (ValidFloat eb sb) => Real (FP eb sb)

deriving newtype instance (ValidFloat eb sb) => RealFrac (FP eb sb)

deriving newtype instance (ValidFloat eb sb) => RealFloat (FP eb sb)

instance (ValidFloat eb sb) => QC.Arbitrary (FP eb sb) where
  arbitrary = do
    frequency
      [ ( 3,
          withValidFPProofs @eb @sb $
            bitCast
              <$> (QC.arbitrary :: QC.Gen (WordN (eb + sb)))
        ),
        ( 5,
          -- mostly normalized numbers
          withValidFPProofs @eb @sb $ do
            e <- egen
            s <- sgen
            msb <- msbGen
            smsb <- smsbGen
            return $ bitCast (sizedBVConcat e s `xor` msb `xor` smsb)
        ),
        ( 4,
          -- mostly denormalized numbers
          withValidFPProofs @eb @sb $ do
            s <- sgen
            msb <- msbGen
            smsb <- smsbGen
            return $
              bitCast (sizedBVConcat 0 s `xor` msb .&. complement smsb)
        ),
        (1, oneof $ return <$> [nan, 0, -0, infinity, -infinity])
      ]
    where
      eb = fromIntegral $ natVal (Proxy @eb) :: Int
      sb = fromIntegral $ natVal (Proxy @sb) :: Int
      egen = withValidFPProofs @eb @sb $ QC.arbitrary :: QC.Gen (WordN eb)
      sgen = withValidFPProofs @eb @sb $ QC.arbitrary :: QC.Gen (WordN sb)
      msbGen =
        withValidFPProofs @eb @sb $
          oneof [return 0, return $ 1 `shiftL` (eb + sb - 1)] ::
          QC.Gen (WordN (eb + sb))
      smsbGen =
        withValidFPProofs @eb @sb $
          oneof [return 0, return $ 1 `shiftL` (sb - 1)] ::
          QC.Gen (WordN (eb + sb))

-- | Rounding mode for floating-point operations.
data FPRoundingMode
  = -- | Round to nearest, ties to even.
    RNE
  | -- | Round to nearest, ties to away from zero.
    RNA
  | -- | Round towards positive infinity.
    RTP
  | -- | Round towards negative infinity.
    RTN
  | -- | Round towards zero.
    RTZ
  deriving (Eq, Ord, Generic, Lift)
  deriving anyclass (Hashable, NFData, Serial)

instance Show FPRoundingMode where
  show RNE = "rne"
  show RNA = "rna"
  show RTP = "rtp"
  show RTN = "rtn"
  show RTZ = "rtz"

-- | All IEEE 754 rounding modes.
allFPRoundingMode :: [FPRoundingMode]
allFPRoundingMode = [RNE, RNA, RTP, RTN, RTZ]

instance QC.Arbitrary FPRoundingMode where
  arbitrary = QC.elements [RNE, RNA, RTP, RTN, RTZ]

instance
  (ValidFP eb sb, n ~ (eb + sb)) =>
  BitCastCanonical (FP eb sb) (WordN n)
  where
  bitCastCanonicalValue _ =
    withValidFPProofs @eb @sb $
      sizedBVConcat (shiftR (-1) 1 :: WordN eb) highsb
    where
      sb = fromIntegral $ natVal (Proxy @sb) :: Int
      highsb = withValidFPProofs @eb @sb $ shiftL 3 (sb - 2) :: WordN sb

instance
  (ValidFP eb sb, n ~ (eb + sb)) =>
  BitCastCanonical (FP eb sb) (IntN n)
  where
  bitCastCanonicalValue n =
    withValidFPProofs @eb @sb $
      bitCast (bitCastCanonicalValue n :: WordN n)

#define BIT_CAST_CANONICAL_VIA_INTERMEDIATE(from, to, intermediate) \
  instance BitCastCanonical (from) (to) where \
    bitCastCanonicalValue x = bitCast (bitCastCanonicalValue x :: intermediate)

#if 1
BIT_CAST_CANONICAL_VIA_INTERMEDIATE(FP64, Word64, WordN64)
BIT_CAST_CANONICAL_VIA_INTERMEDIATE(FP64, Int64, WordN64)
BIT_CAST_CANONICAL_VIA_INTERMEDIATE(FP64, Double, WordN64)
BIT_CAST_CANONICAL_VIA_INTERMEDIATE(FP32, Word32, WordN32)
BIT_CAST_CANONICAL_VIA_INTERMEDIATE(FP32, Int32, WordN32)
BIT_CAST_CANONICAL_VIA_INTERMEDIATE(FP32, Float, WordN32)
BIT_CAST_CANONICAL_VIA_INTERMEDIATE(FP16, Word16, WordN16)
BIT_CAST_CANONICAL_VIA_INTERMEDIATE(FP16, Int16, WordN16)
#endif

instance (ValidFP eb sb, r ~ (eb + sb)) => BitCastOr (FP eb sb) (WordN r) where
  bitCastOr d (FP f)
    | isNaN f = d
    | otherwise = wordn
    where
      wordn :: WordN (eb + sb)
      wordn =
        withValidFPProofs @eb @sb $
          fromIntegral $
            fromJust $
              unliteral $
                sFloatingPointAsSWord $
                  literal f

instance
  (ValidFP eb sb, n ~ (eb + sb)) =>
  BitCastOr (FP eb sb) (IntN n)
  where
  bitCastOr d n =
    withValidFPProofs @eb @sb $
      bitCast (bitCastOr (bitCast d) n :: WordN n)

#define BIT_CAST_OR_VIA_INTERMEDIATE(from, to, intermediate) \
  instance BitCastOr (from) (to) where \
    bitCastOr d x = bitCast (bitCastOr (bitCast d) x :: intermediate)

#if 1
BIT_CAST_OR_VIA_INTERMEDIATE(FP64, Word64, WordN64)
BIT_CAST_OR_VIA_INTERMEDIATE(FP64, Int64, WordN64)
BIT_CAST_OR_VIA_INTERMEDIATE(FP64, Double, WordN64)
BIT_CAST_OR_VIA_INTERMEDIATE(FP32, Word32, WordN32)
BIT_CAST_OR_VIA_INTERMEDIATE(FP32, Int32, WordN32)
BIT_CAST_OR_VIA_INTERMEDIATE(FP32, Float, WordN32)
BIT_CAST_OR_VIA_INTERMEDIATE(FP16, Word16, WordN16)
BIT_CAST_OR_VIA_INTERMEDIATE(FP16, Int16, WordN16)
#endif

-- | An error thrown when bitcasting or converting t'FP' NaN to other types.
data NotRepresentableFPError
  = NaNError
  | FPUnderflowError
  | FPOverflowError
  deriving (Show, Eq, Ord, Generic)

instance Exception NotRepresentableFPError where
  displayException NaNError =
    "Converting NaN value cannot be done precisely with SMT-LIB2"
  displayException FPUnderflowError =
    "Converting FP values that cannot be represented by non-FP types due to "
      <> "underflowing"
  displayException FPOverflowError =
    "Converting FP values that cannot be represented by non-FP types due to "
      <> "overflowing"

instance (ValidFP eb sb) => IEEEFPConstants (FP eb sb) where
  fpPositiveInfinite = FP infinity
  {-# INLINE fpPositiveInfinite #-}
  fpNegativeInfinite = FP $ -infinity
  {-# INLINE fpNegativeInfinite #-}
  fpNaN = FP nan
  {-# INLINE fpNaN #-}
  fpNegativeZero = FP $ -0
  {-# INLINE fpNegativeZero #-}
  fpPositiveZero = FP 0
  {-# INLINE fpPositiveZero #-}

  fpMinNormalized =
    withValidFPProofs @eb @sb $
      bitCast $
        (1 :: WordN (eb + sb)) `shiftL` fromIntegral (natVal (Proxy @sb) - 1)
  {-# INLINE fpMinNormalized #-}

  fpMaxNormalized =
    withValidFPProofs @eb @sb $
      bitCast $
        complement
          ( (1 :: WordN (eb + sb))
              `shiftL` fromIntegral (natVal (Proxy @sb) - 1)
          )
          `shiftL` 1
          `shiftR` 1
  {-# INLINE fpMaxNormalized #-}

  fpMinSubnormal = withValidFPProofs @eb @sb $ bitCast (1 :: WordN (eb + sb))
  {-# INLINE fpMinSubnormal #-}

  fpMaxSubnormal =
    withValidFPProofs @eb @sb $
      bitCast
        ( (1 :: WordN (eb + sb))
            `shiftL` fromIntegral (natVal (Proxy @sb) - 1)
            - 1
        )
  {-# INLINE fpMaxSubnormal #-}

cmpHandleNegZero :: (ValidFP eb sb) => FP eb sb -> FP eb sb -> Bool
cmpHandleNegZero x y =
  if fpIsZero x && fpIsZero y then fpIsNegativeZero x else x < y

instance (ValidFP eb sb) => IEEEFPOp (FP eb sb) where
  fpAbs = abs
  {-# INLINE fpAbs #-}
  fpNeg = negate
  {-# INLINE fpNeg #-}
  fpRem = SBVI.fpRemH
  {-# INLINE fpRem #-}
  fpMinimum a b
    | fpIsNaN a || fpIsNaN b = fpNaN
    | cmpHandleNegZero a b = a
    | otherwise = b
  {-# INLINE fpMinimum #-}
  fpMinimumNumber a b
    | fpIsNaN a = b
    | fpIsNaN b = a
    | cmpHandleNegZero a b = a
    | otherwise = b
  {-# INLINE fpMinimumNumber #-}
  fpMaximum a b
    | fpIsNaN a || fpIsNaN b = fpNaN
    | cmpHandleNegZero a b = b
    | otherwise = a
  {-# INLINE fpMaximum #-}
  fpMaximumNumber a b
    | fpIsNaN a = b
    | fpIsNaN b = a
    | cmpHandleNegZero a b = b
    | otherwise = a
  {-# INLINE fpMaximumNumber #-}

instance IEEEFPRoundingMode FPRoundingMode where
  rne = RNE
  {-# INLINE rne #-}
  rna = RNA
  {-# INLINE rna #-}
  rtp = RTP
  {-# INLINE rtp #-}
  rtn = RTN
  {-# INLINE rtn #-}
  rtz = RTZ
  {-# INLINE rtz #-}

libBFRoundingMode :: FPRoundingMode -> RoundMode
libBFRoundingMode RNE = NearEven
libBFRoundingMode RNA = NearAway
libBFRoundingMode RTP = ToPosInf
libBFRoundingMode RTN = ToNegInf
libBFRoundingMode RTZ = ToZero

libBFOpts ::
  forall eb sb. (ValidFP eb sb) => FPRoundingMode -> FP eb sb -> BFOpts
libBFOpts mode _ = rnd rd <> precBits sb <> expBits eb <> allowSubnormal
  where
    eb = fromIntegral $ natVal (Proxy @eb) :: Int
    sb = fromIntegral $ natVal (Proxy @sb) :: Word
    rd = libBFRoundingMode mode

toLibBF :: forall eb sb. (ValidFP eb sb) => FP eb sb -> BigFloat
toLibBF f
  | fpIsNegativeZero f = bfNegZero
  | fpIsPositiveZero f = bfPosZero
  | fpIsPositiveInfinite f = bfPosInf
  | fpIsNegativeInfinite f = bfNegInf
  | fpIsNaN f = bfNaN
  | otherwise =
      SBVF.fpValue $
        uncurry (fpEncodeFloat eb sb) $
          decodeFloat f
  where
    eb = fromIntegral $ natVal (Proxy @eb) :: Int
    sb = fromIntegral $ natVal (Proxy @sb) :: Int

fromLibBF :: forall eb sb. (ValidFP eb sb) => BigFloat -> FP eb sb
fromLibBF f
  | bfIsNeg f && bfIsZero f = fpNegativeZero
  | bfIsPos f && bfIsZero f = fpPositiveZero
  | bfIsNeg f && bfIsInf f = fpNegativeInfinite
  | bfIsPos f && bfIsInf f = fpPositiveInfinite
  | bfIsNaN f = fpNaN
  | otherwise = uncurry encodeFloat $ decodeFloat fp
  where
    fp = SBVF.FP eb sb f
    eb = fromIntegral $ natVal (Proxy @eb) :: Int
    sb = fromIntegral $ natVal (Proxy @sb) :: Int

liftLibBF1 ::
  (ValidFP eb sb) =>
  (BFOpts -> BigFloat -> (BigFloat, Status)) ->
  FPRoundingMode ->
  FP eb sb ->
  FP eb sb
liftLibBF1 f rd x = fromLibBF $ fst $ f opts xbf
  where
    opts = libBFOpts rd x
    xbf = toLibBF x

liftLibBF2 ::
  (ValidFP eb sb) =>
  (BFOpts -> BigFloat -> BigFloat -> (BigFloat, Status)) ->
  FPRoundingMode ->
  FP eb sb ->
  FP eb sb ->
  FP eb sb
liftLibBF2 f rd l r = fromLibBF $ fst $ f opts lbf rbf
  where
    opts = libBFOpts rd l
    lbf = toLibBF l
    rbf = toLibBF r

liftLibBF3 ::
  (ValidFP eb sb) =>
  (BFOpts -> BigFloat -> BigFloat -> BigFloat -> (BigFloat, Status)) ->
  FPRoundingMode ->
  FP eb sb ->
  FP eb sb ->
  FP eb sb ->
  FP eb sb
liftLibBF3 f rd x y z = fromLibBF $ fst $ f opts xbf ybf zbf
  where
    opts = libBFOpts rd x
    xbf = toLibBF x
    ybf = toLibBF y
    zbf = toLibBF z

instance (ValidFP eb sb) => IEEEFPRoundingOp (FP eb sb) FPRoundingMode where
  fpAdd = liftLibBF2 bfAdd
  {-# INLINE fpAdd #-}
  fpSub = liftLibBF2 bfSub
  {-# INLINE fpSub #-}
  fpMul = liftLibBF2 bfMul
  {-# INLINE fpMul #-}
  fpDiv = liftLibBF2 bfDiv
  {-# INLINE fpDiv #-}
  fpFMA = liftLibBF3 bfFMA
  {-# INLINE fpFMA #-}
  fpSqrt = liftLibBF1 bfSqrt
  {-# INLINE fpSqrt #-}
  fpRoundToIntegral rd x =
    fromLibBF $ fst $ bfRoundInt (libBFRoundingMode rd) $ toLibBF x
  {-# INLINE fpRoundToIntegral #-}

instance
  (ValidFP eb sb) =>
  IEEEFPConvertible AlgReal (FP eb sb) FPRoundingMode
  where
  fromFPOr d _ fp
    | fpIsInfinite fp = d
    | fpIsNaN fp = d
    | otherwise =
        let (m, n) = decodeFloat fp
         in fromRational (toRational m * (2 ^^ n))
  toFP mode (AlgExactRational v) = fromLibBF $ fst $ bfDiv opts n d
    where
      opts = libBFOpts mode (undefined :: FP eb sb)
      n = bfFromInteger $ numerator v
      d = bfFromInteger $ denominator v
  toFP _ r =
    throw
      UnsupportedAlgRealOperation {op = "toFP", msg = show r}

instance
  (ValidFP eb sb) =>
  IEEEFPToAlgReal AlgReal (FP eb sb) FPRoundingMode

roundRationalToInteger :: FPRoundingMode -> Rational -> Integer
roundRationalToInteger mode r
  | d == 1 = n
  | d == 2 = case mode of
      RNE -> if even ndivd then ndivd else ndivd + 1
      RNA -> if n > 0 then ndivd + 1 else ndivd
      RTP -> ndivd + 1
      RTN -> ndivd
      RTZ -> if n > 0 then ndivd else ndivd + 1
  | otherwise = case mode of
      RNE -> if nmodd > d `div` 2 then ndivd + 1 else ndivd
      RNA -> if nmodd > d `div` 2 then ndivd + 1 else ndivd
      RTP -> ndivd + 1
      RTN -> ndivd
      RTZ -> if n > 0 then ndivd else ndivd + 1
  where
    n = numerator r
    d = denominator r
    ndivd = n `div` d
    nmodd = n `mod` d

instance
  (ValidFP eb sb) =>
  IEEEFPConvertible Integer (FP eb sb) FPRoundingMode
  where
  fromFPOr d mode fp
    | fpIsInfinite fp = d
    | fpIsNaN fp = d
    | otherwise =
        let r = fromFPOr (fromIntegral d) mode fp
         in case r of
              AlgExactRational v -> roundRationalToInteger mode v
              _ -> error "Should not happen"
  toFP mode r = toFP mode (fromIntegral r :: AlgReal)

instance
  (ValidFP eb sb, KnownNat n, 1 <= n) =>
  IEEEFPConvertible (WordN n) (FP eb sb) FPRoundingMode
  where
  fromFPOr d mode fp
    | fpIsInfinite fp = d
    | fpIsNaN fp = d
    | otherwise =
        let p = fromFPOr (fromIntegral d :: Integer) mode fp
         in if p < (fromIntegral (minBound :: WordN n))
              || p > (fromIntegral (maxBound :: WordN n))
              then d
              else fromIntegral p
  toFP mode r = toFP mode (fromIntegral r :: AlgReal)

instance
  (ValidFP eb sb, KnownNat n, 1 <= n) =>
  IEEEFPConvertible (IntN n) (FP eb sb) FPRoundingMode
  where
  fromFPOr d mode fp
    | fpIsInfinite fp = d
    | fpIsNaN fp = d
    | otherwise =
        let p = fromFPOr (fromIntegral d :: Integer) mode fp
         in if p < (fromIntegral (minBound :: IntN n))
              || p > (fromIntegral (maxBound :: IntN n))
              then d
              else fromIntegral p
  toFP mode r = toFP mode (fromIntegral r :: AlgReal)

instance
  (ValidFP eb sb, ValidFP eb' sb') =>
  IEEEFPConvertible (FP eb' sb') (FP eb sb) FPRoundingMode
  where
  fromFPOr _ = toFP
  toFP mode fp
    | fpIsNegativeInfinite fp = fpNegativeInfinite
    | fpIsPositiveInfinite fp = fpPositiveInfinite
    | fpIsNaN fp = fpNaN
    | fpIsNegativeZero fp = fpNegativeZero
    | fpIsPositiveZero fp = fpPositiveZero
    | otherwise =
        let bffp = toLibBF fp
            opts = libBFOpts mode (undefined :: FP eb sb)
         in fromLibBF $ fst $ bfRoundFloat opts bffp

-- | Next representable floating-point number.
--
-- Note:
--
-- > nextFP(+inf) = +inf
-- > nextFP(-inf) = -maxNormalized
-- > nextFP(NaN) = NaN
--
-- The function do not distinguish between -0 and +0.
nextFP :: forall eb sb. (ValidFP eb sb) => FP eb sb -> FP eb sb
nextFP x
  | fpIsNaN x = fpNaN
  | fpIsNegativeInfinite x = -fpMaxNormalized
  | x == -fpMinNormalized = -fpMaxSubnormal
  | x == -fpMinSubnormal = 0
  | x == 0 = fpMinSubnormal
  | x == fpMaxSubnormal = fpMinNormalized
  | x == fpMaxNormalized = fpPositiveInfinite
  | fpIsPositiveInfinite x = fpPositiveInfinite
  | x > 0 =
      withValidFPProofs @eb @sb $
        bitCast ((bitCastOrCanonical x :: WordN (eb + sb)) + 1)
  | otherwise =
      withValidFPProofs @eb @sb $
        bitCast ((bitCastOrCanonical x :: WordN (eb + sb)) - 1)

-- | Previous representable floating-point number.
--
-- Note:
--
-- > prevFP(+inf) = +maxNormalized
-- > prevFP(-inf) = -inf
-- > prevFP(NaN) = NaN
--
-- The function do not distinguish between -0 and +0.
prevFP :: forall eb sb. (ValidFP eb sb) => FP eb sb -> FP eb sb
prevFP x
  | fpIsNaN x = fpNaN
  | fpIsPositiveInfinite x = fpMaxNormalized
  | x == fpMinNormalized = fpMaxSubnormal
  | x == fpMinSubnormal = 0
  | x == 0 = -fpMinSubnormal
  | x == -fpMaxSubnormal = -fpMinNormalized
  | x == -fpMaxNormalized = fpNegativeInfinite
  | fpIsNegativeInfinite x = fpNegativeInfinite
  | x > 0 =
      withValidFPProofs @eb @sb $
        bitCast ((bitCastOrCanonical x :: WordN (eb + sb)) - 1)
  | otherwise =
      withValidFPProofs @eb @sb $
        bitCast ((bitCastOrCanonical x :: WordN (eb + sb)) + 1)

-- | Bounds for converting bit vectors to floating-point numbers. Out-of-range
-- FP values cannot be converted to a representable bit-vector.
class ConvertibleBound bv where
  convertibleLowerBound ::
    forall eb sb n.
    (ValidFP eb sb, KnownNat n, 1 <= n) =>
    bv n ->
    FPRoundingMode ->
    FP eb sb
  convertibleUpperBound ::
    forall eb sb n.
    (ValidFP eb sb, KnownNat n, 1 <= n) =>
    bv n ->
    FPRoundingMode ->
    FP eb sb

instance ConvertibleBound WordN where
  convertibleLowerBound _ RTP = nextFP $ -1
  convertibleLowerBound _ RTZ = nextFP $ -1
  convertibleLowerBound _ RTN = 0
  convertibleLowerBound _ RNA = nextFP $ -0.5
  convertibleLowerBound _ RNE = -0.5
  convertibleUpperBound ::
    forall eb sb n.
    (ValidFP eb sb, KnownNat n, 1 <= n) =>
    WordN n ->
    FPRoundingMode ->
    FP eb sb
  convertibleUpperBound _ mode
    | ebn < n = fpMaxNormalized
    | ebn == n && sb <= n = fpMaxNormalized
    | ebn >= n && sb > n = case mode of
        RTP -> toFP rne (maxBound :: WordN n)
        RTZ -> prevFP $ toFP rne (maxBound :: WordN n) + 1
        RTN -> prevFP $ toFP rne (maxBound :: WordN n) + 1
        RNA -> prevFP $ toFP rne (maxBound :: WordN n) + 0.5
        RNE -> prevFP $ toFP rne (maxBound :: WordN n) + 0.5
    | ebn > n && sb == n = toFP rne (maxBound :: WordN n)
    -- ebn > n && sb < n
    | otherwise =
        prevFP $ toFP rne (maxBound `div` 2 + 1 :: WordN n) * 2
    where
      n = natVal (Proxy @n)
      eb = natVal (Proxy @eb)
      ebn = 2 ^ (eb - 1)
      sb = natVal (Proxy @sb)

instance ConvertibleBound IntN where
  convertibleLowerBound ::
    forall eb sb n.
    (ValidFP eb sb, KnownNat n, 1 <= n) =>
    IntN n ->
    FPRoundingMode ->
    FP eb sb
  convertibleLowerBound _ mode
    | ebn <= n - 1 = -fpMaxNormalized
    | ebn > n - 1 && sb <= n - 1 = toFP rne (minBound :: IntN n)
    -- ebn > n - 1 && sb > n - 1
    | otherwise = case mode of
        RTP -> nextFP $ toFP rne (minBound :: IntN n) - 1
        RTZ -> nextFP $ toFP rne (minBound :: IntN n) - 1
        RTN -> toFP rne (minBound :: IntN n)
        RNA ->
          if sb == n
            then toFP rne (minBound :: IntN n) - 0.5
            else nextFP $ toFP rne (minBound :: IntN n) - 0.5
        RNE -> toFP rne (minBound :: IntN n) - 0.5
    where
      n = natVal (Proxy @n)
      eb = natVal (Proxy @eb)
      ebn = 2 ^ (eb - 1)
      sb = natVal (Proxy @sb)
  convertibleUpperBound ::
    forall eb sb n.
    (ValidFP eb sb, KnownNat n, 1 <= n) =>
    IntN n ->
    FPRoundingMode ->
    FP eb sb
  convertibleUpperBound _ mode
    | ebn < n - 1 = fpMaxNormalized
    | ebn == n - 1 && sb <= n - 1 = fpMaxNormalized
    | ebn >= n - 1 && sb > n - 1 = case mode of
        RTP -> toFP rne (maxBound :: IntN n)
        RTZ -> prevFP $ toFP rne (maxBound :: IntN n) + 1
        RTN -> prevFP $ toFP rne (maxBound :: IntN n) + 1
        RNA -> prevFP $ toFP rne (maxBound :: IntN n) + 0.5
        RNE -> prevFP $ toFP rne (maxBound :: IntN n) + 0.5
    | ebn > n - 1 && sb == n - 1 = toFP rne (maxBound :: IntN n)
    -- ebn > n - 1 && sb < n - 1
    | otherwise =
        prevFP $ toFP rne (maxBound `div` 2 + 1 :: IntN n) * 2
    where
      n = natVal (Proxy @n)
      eb = natVal (Proxy @eb)
      ebn = 2 ^ (eb - 1)
      sb = natVal (Proxy @sb)

instance Apply (FP eb sb) where
  type FunType (FP eb sb) = FP eb sb
  apply = id

instance Apply FPRoundingMode where
  type FunType FPRoundingMode = FPRoundingMode
  apply = id

instance (ValidFP eb sb) => Serial (FP eb sb) where
  serialize x =
    withValidFPProofs @eb @sb $
      serialize (bitCastOrCanonical x :: WordN (eb + sb))
  deserialize = do
    w :: WordN (eb + sb) <- withValidFPProofs @eb @sb deserialize
    return $ withValidFPProofs @eb @sb $ bitCast w

instance (ValidFP eb sb) => Cereal.Serialize (FP eb sb) where
  put = serialize
  get = deserialize

instance (ValidFP eb sb) => Binary.Binary (FP eb sb) where
  put = serialize
  get = deserialize