{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}

-- |
-- Module      :   Grisette.Internal.Core.Data.Class.SafeFromFP
-- 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.Core.Data.Class.SafeFromFP (SafeFromFP (..)) where

import Control.Monad.Error.Class (MonadError (throwError))
import GHC.TypeLits (KnownNat, type (<=))
import Grisette.Internal.Core.Control.Monad.Class.Union (MonadUnion)
import Grisette.Internal.Core.Data.Class.IEEEFP
  ( IEEEFPConvertible (fromFPOr),
    IEEEFPRoundingMode (rna, rne, rtn, rtp, rtz),
    fpIsNaN,
    fpIsNegativeInfinite,
    fpIsPositiveInfinite,
  )
import Grisette.Internal.Core.Data.Class.ITEOp (ITEOp (symIte))
import Grisette.Internal.Core.Data.Class.SimpleMergeable (mrgIf)
import Grisette.Internal.Core.Data.Class.Solvable (Solvable (con))
import Grisette.Internal.Core.Data.Class.SymEq (SymEq ((.==)))
import Grisette.Internal.Core.Data.Class.SymIEEEFP
  ( SymIEEEFPTraits
      ( symFpIsNaN,
        symFpIsNegativeInfinite,
        symFpIsPositiveInfinite
      ),
  )
import Grisette.Internal.Core.Data.Class.SymOrd (SymOrd ((.<), (.>)))
import Grisette.Internal.Core.Data.Class.TryMerge
  ( TryMerge,
    mrgSingle,
    tryMerge,
  )
import Grisette.Internal.SymPrim.AlgReal (AlgReal)
import Grisette.Internal.SymPrim.BV (IntN, WordN)
import Grisette.Internal.SymPrim.FP
  ( ConvertibleBound (convertibleLowerBound, convertibleUpperBound),
    FP,
    FPRoundingMode,
    NotRepresentableFPError
      ( FPOverflowError,
        FPUnderflowError,
        NaNError
      ),
    ValidFP,
  )
import Grisette.Internal.SymPrim.SymAlgReal (SymAlgReal)
import Grisette.Internal.SymPrim.SymBV (SymIntN, SymWordN)
import Grisette.Internal.SymPrim.SymFP (SymFP, SymFPRoundingMode)
import Grisette.Internal.SymPrim.SymInteger (SymInteger)

-- | Safe conversion from floating point numbers that throws exceptions when
-- the result isn't representable by the type.
class
  (MonadError e m, TryMerge m, IEEEFPConvertible a fp fprd) =>
  SafeFromFP e a fp fprd m
  where
  safeFromFP :: fprd -> fp -> m a

instance
  (MonadError NotRepresentableFPError m, TryMerge m, ValidFP eb sb) =>
  SafeFromFP NotRepresentableFPError AlgReal (FP eb sb) FPRoundingMode m
  where
  safeFromFP :: FPRoundingMode -> FP eb sb -> m AlgReal
safeFromFP FPRoundingMode
mode FP eb sb
a
    | FP eb sb -> Bool
forall a. RealFloat a => a -> Bool
fpIsPositiveInfinite FP eb sb
a = m AlgReal -> m AlgReal
forall (m :: * -> *) a. (TryMerge m, Mergeable a) => m a -> m a
tryMerge (m AlgReal -> m AlgReal) -> m AlgReal -> m AlgReal
forall a b. (a -> b) -> a -> b
$ NotRepresentableFPError -> m AlgReal
forall a. NotRepresentableFPError -> m a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError NotRepresentableFPError
FPOverflowError
    | FP eb sb -> Bool
forall a. RealFloat a => a -> Bool
fpIsNegativeInfinite FP eb sb
a = m AlgReal -> m AlgReal
forall (m :: * -> *) a. (TryMerge m, Mergeable a) => m a -> m a
tryMerge (m AlgReal -> m AlgReal) -> m AlgReal -> m AlgReal
forall a b. (a -> b) -> a -> b
$ NotRepresentableFPError -> m AlgReal
forall a. NotRepresentableFPError -> m a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError NotRepresentableFPError
FPUnderflowError
    | FP eb sb -> Bool
forall a. RealFloat a => a -> Bool
fpIsNaN FP eb sb
a = m AlgReal -> m AlgReal
forall (m :: * -> *) a. (TryMerge m, Mergeable a) => m a -> m a
tryMerge (m AlgReal -> m AlgReal) -> m AlgReal -> m AlgReal
forall a b. (a -> b) -> a -> b
$ NotRepresentableFPError -> m AlgReal
forall a. NotRepresentableFPError -> m a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError NotRepresentableFPError
NaNError
    | Bool
otherwise = AlgReal -> m AlgReal
forall (m :: * -> *) a.
(TryMerge m, Applicative m, Mergeable a) =>
a -> m a
mrgSingle (AlgReal -> m AlgReal) -> AlgReal -> m AlgReal
forall a b. (a -> b) -> a -> b
$ AlgReal -> FPRoundingMode -> FP eb sb -> AlgReal
forall a fp mode.
IEEEFPConvertible a fp mode =>
a -> mode -> fp -> a
fromFPOr AlgReal
forall a. HasCallStack => a
undefined FPRoundingMode
mode FP eb sb
a

instance
  (MonadError NotRepresentableFPError m, MonadUnion m, ValidFP eb sb) =>
  SafeFromFP
    NotRepresentableFPError
    SymAlgReal
    (SymFP eb sb)
    SymFPRoundingMode
    m
  where
  safeFromFP :: SymFPRoundingMode -> SymFP eb sb -> m SymAlgReal
safeFromFP SymFPRoundingMode
mode SymFP eb sb
a =
    SymBool -> m SymAlgReal -> m SymAlgReal -> m SymAlgReal
forall (u :: * -> *) a.
(SymBranching u, Mergeable a) =>
SymBool -> u a -> u a -> u a
mrgIf (SymFP eb sb -> SymBool
forall a. SymIEEEFPTraits a => a -> SymBool
symFpIsPositiveInfinite SymFP eb sb
a) (m SymAlgReal -> m SymAlgReal
forall (m :: * -> *) a. (TryMerge m, Mergeable a) => m a -> m a
tryMerge (m SymAlgReal -> m SymAlgReal) -> m SymAlgReal -> m SymAlgReal
forall a b. (a -> b) -> a -> b
$ NotRepresentableFPError -> m SymAlgReal
forall a. NotRepresentableFPError -> m a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError NotRepresentableFPError
FPOverflowError)
      (m SymAlgReal -> m SymAlgReal) -> m SymAlgReal -> m SymAlgReal
forall a b. (a -> b) -> a -> b
$ SymBool -> m SymAlgReal -> m SymAlgReal -> m SymAlgReal
forall (u :: * -> *) a.
(SymBranching u, Mergeable a) =>
SymBool -> u a -> u a -> u a
mrgIf
        (SymFP eb sb -> SymBool
forall a. SymIEEEFPTraits a => a -> SymBool
symFpIsNegativeInfinite SymFP eb sb
a)
        (m SymAlgReal -> m SymAlgReal
forall (m :: * -> *) a. (TryMerge m, Mergeable a) => m a -> m a
tryMerge (m SymAlgReal -> m SymAlgReal) -> m SymAlgReal -> m SymAlgReal
forall a b. (a -> b) -> a -> b
$ NotRepresentableFPError -> m SymAlgReal
forall a. NotRepresentableFPError -> m a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError NotRepresentableFPError
FPUnderflowError)
      (m SymAlgReal -> m SymAlgReal) -> m SymAlgReal -> m SymAlgReal
forall a b. (a -> b) -> a -> b
$ SymBool -> m SymAlgReal -> m SymAlgReal -> m SymAlgReal
forall (u :: * -> *) a.
(SymBranching u, Mergeable a) =>
SymBool -> u a -> u a -> u a
mrgIf (SymFP eb sb -> SymBool
forall a. SymIEEEFPTraits a => a -> SymBool
symFpIsNaN SymFP eb sb
a) (m SymAlgReal -> m SymAlgReal
forall (m :: * -> *) a. (TryMerge m, Mergeable a) => m a -> m a
tryMerge (m SymAlgReal -> m SymAlgReal) -> m SymAlgReal -> m SymAlgReal
forall a b. (a -> b) -> a -> b
$ NotRepresentableFPError -> m SymAlgReal
forall a. NotRepresentableFPError -> m a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError NotRepresentableFPError
NaNError)
      (m SymAlgReal -> m SymAlgReal) -> m SymAlgReal -> m SymAlgReal
forall a b. (a -> b) -> a -> b
$ SymAlgReal -> m SymAlgReal
forall (m :: * -> *) a.
(TryMerge m, Applicative m, Mergeable a) =>
a -> m a
mrgSingle
      (SymAlgReal -> m SymAlgReal) -> SymAlgReal -> m SymAlgReal
forall a b. (a -> b) -> a -> b
$ SymAlgReal -> SymFPRoundingMode -> SymFP eb sb -> SymAlgReal
forall a fp mode.
IEEEFPConvertible a fp mode =>
a -> mode -> fp -> a
fromFPOr SymAlgReal
0 SymFPRoundingMode
mode SymFP eb sb
a

instance
  (MonadError NotRepresentableFPError m, TryMerge m, ValidFP eb sb) =>
  SafeFromFP NotRepresentableFPError Integer (FP eb sb) FPRoundingMode m
  where
  safeFromFP :: FPRoundingMode -> FP eb sb -> m Integer
safeFromFP FPRoundingMode
mode FP eb sb
a
    | FP eb sb -> Bool
forall a. RealFloat a => a -> Bool
fpIsPositiveInfinite FP eb sb
a = m Integer -> m Integer
forall (m :: * -> *) a. (TryMerge m, Mergeable a) => m a -> m a
tryMerge (m Integer -> m Integer) -> m Integer -> m Integer
forall a b. (a -> b) -> a -> b
$ NotRepresentableFPError -> m Integer
forall a. NotRepresentableFPError -> m a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError NotRepresentableFPError
FPOverflowError
    | FP eb sb -> Bool
forall a. RealFloat a => a -> Bool
fpIsNegativeInfinite FP eb sb
a = m Integer -> m Integer
forall (m :: * -> *) a. (TryMerge m, Mergeable a) => m a -> m a
tryMerge (m Integer -> m Integer) -> m Integer -> m Integer
forall a b. (a -> b) -> a -> b
$ NotRepresentableFPError -> m Integer
forall a. NotRepresentableFPError -> m a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError NotRepresentableFPError
FPUnderflowError
    | FP eb sb -> Bool
forall a. RealFloat a => a -> Bool
fpIsNaN FP eb sb
a = m Integer -> m Integer
forall (m :: * -> *) a. (TryMerge m, Mergeable a) => m a -> m a
tryMerge (m Integer -> m Integer) -> m Integer -> m Integer
forall a b. (a -> b) -> a -> b
$ NotRepresentableFPError -> m Integer
forall a. NotRepresentableFPError -> m a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError NotRepresentableFPError
NaNError
    | Bool
otherwise = Integer -> m Integer
forall (m :: * -> *) a.
(TryMerge m, Applicative m, Mergeable a) =>
a -> m a
mrgSingle (Integer -> m Integer) -> Integer -> m Integer
forall a b. (a -> b) -> a -> b
$ Integer -> FPRoundingMode -> FP eb sb -> Integer
forall a fp mode.
IEEEFPConvertible a fp mode =>
a -> mode -> fp -> a
fromFPOr Integer
0 FPRoundingMode
mode FP eb sb
a

instance
  (MonadError NotRepresentableFPError m, MonadUnion m, ValidFP eb sb) =>
  SafeFromFP
    NotRepresentableFPError
    SymInteger
    (SymFP eb sb)
    SymFPRoundingMode
    m
  where
  safeFromFP :: SymFPRoundingMode -> SymFP eb sb -> m SymInteger
safeFromFP SymFPRoundingMode
mode SymFP eb sb
a =
    SymBool -> m SymInteger -> m SymInteger -> m SymInteger
forall (u :: * -> *) a.
(SymBranching u, Mergeable a) =>
SymBool -> u a -> u a -> u a
mrgIf (SymFP eb sb -> SymBool
forall a. SymIEEEFPTraits a => a -> SymBool
symFpIsPositiveInfinite SymFP eb sb
a) (m SymInteger -> m SymInteger
forall (m :: * -> *) a. (TryMerge m, Mergeable a) => m a -> m a
tryMerge (m SymInteger -> m SymInteger) -> m SymInteger -> m SymInteger
forall a b. (a -> b) -> a -> b
$ NotRepresentableFPError -> m SymInteger
forall a. NotRepresentableFPError -> m a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError NotRepresentableFPError
FPOverflowError)
      (m SymInteger -> m SymInteger) -> m SymInteger -> m SymInteger
forall a b. (a -> b) -> a -> b
$ SymBool -> m SymInteger -> m SymInteger -> m SymInteger
forall (u :: * -> *) a.
(SymBranching u, Mergeable a) =>
SymBool -> u a -> u a -> u a
mrgIf
        (SymFP eb sb -> SymBool
forall a. SymIEEEFPTraits a => a -> SymBool
symFpIsNegativeInfinite SymFP eb sb
a)
        (m SymInteger -> m SymInteger
forall (m :: * -> *) a. (TryMerge m, Mergeable a) => m a -> m a
tryMerge (m SymInteger -> m SymInteger) -> m SymInteger -> m SymInteger
forall a b. (a -> b) -> a -> b
$ NotRepresentableFPError -> m SymInteger
forall a. NotRepresentableFPError -> m a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError NotRepresentableFPError
FPUnderflowError)
      (m SymInteger -> m SymInteger) -> m SymInteger -> m SymInteger
forall a b. (a -> b) -> a -> b
$ SymBool -> m SymInteger -> m SymInteger -> m SymInteger
forall (u :: * -> *) a.
(SymBranching u, Mergeable a) =>
SymBool -> u a -> u a -> u a
mrgIf
        (SymFP eb sb -> SymBool
forall a. SymIEEEFPTraits a => a -> SymBool
symFpIsNaN SymFP eb sb
a)
        (m SymInteger -> m SymInteger
forall (m :: * -> *) a. (TryMerge m, Mergeable a) => m a -> m a
tryMerge (m SymInteger -> m SymInteger) -> m SymInteger -> m SymInteger
forall a b. (a -> b) -> a -> b
$ NotRepresentableFPError -> m SymInteger
forall a. NotRepresentableFPError -> m a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError NotRepresentableFPError
NaNError)
      (m SymInteger -> m SymInteger) -> m SymInteger -> m SymInteger
forall a b. (a -> b) -> a -> b
$ SymInteger -> m SymInteger
forall (m :: * -> *) a.
(TryMerge m, Applicative m, Mergeable a) =>
a -> m a
mrgSingle
      (SymInteger -> m SymInteger) -> SymInteger -> m SymInteger
forall a b. (a -> b) -> a -> b
$ SymInteger -> SymFPRoundingMode -> SymFP eb sb -> SymInteger
forall a fp mode.
IEEEFPConvertible a fp mode =>
a -> mode -> fp -> a
fromFPOr SymInteger
0 SymFPRoundingMode
mode SymFP eb sb
a

instance
  ( MonadError NotRepresentableFPError m,
    TryMerge m,
    ValidFP eb sb,
    KnownNat n,
    1 <= n
  ) =>
  SafeFromFP NotRepresentableFPError (WordN n) (FP eb sb) FPRoundingMode m
  where
  safeFromFP :: FPRoundingMode -> FP eb sb -> m (WordN n)
safeFromFP FPRoundingMode
mode FP eb sb
a = do
    p :: Integer <- FPRoundingMode -> FP eb sb -> m Integer
forall e a fp fprd (m :: * -> *).
SafeFromFP e a fp fprd m =>
fprd -> fp -> m a
safeFromFP FPRoundingMode
mode FP eb sb
a
    if p < (fromIntegral (minBound :: WordN n))
      then tryMerge $ throwError FPUnderflowError
      else
        if p > (fromIntegral (maxBound :: WordN n))
          then tryMerge $ throwError FPOverflowError
          else mrgSingle $ fromIntegral p

symConvertibleLowerBound ::
  forall conBV symBV n eb sb.
  ( ConvertibleBound conBV,
    ValidFP eb sb,
    KnownNat n,
    1 <= n,
    Solvable (conBV n) (symBV n)
  ) =>
  symBV n ->
  SymFPRoundingMode ->
  SymFP eb sb
symConvertibleLowerBound :: forall (conBV :: Nat -> *) (symBV :: Nat -> *) (n :: Nat)
       (eb :: Nat) (sb :: Nat).
(ConvertibleBound conBV, ValidFP eb sb, KnownNat n, 1 <= n,
 Solvable (conBV n) (symBV n)) =>
symBV n -> SymFPRoundingMode -> SymFP eb sb
symConvertibleLowerBound symBV n
_ SymFPRoundingMode
mode =
  SymBool -> SymFP eb sb -> SymFP eb sb -> SymFP eb sb
forall v. ITEOp v => SymBool -> v -> v -> v
symIte
    (SymFPRoundingMode
mode SymFPRoundingMode -> SymFPRoundingMode -> SymBool
forall a. SymEq a => a -> a -> SymBool
.== SymFPRoundingMode
forall mode. IEEEFPRoundingMode mode => mode
rne)
    (FP eb sb -> SymFP eb sb
forall c t. Solvable c t => c -> t
con (FP eb sb -> SymFP eb sb) -> FP eb sb -> SymFP eb sb
forall a b. (a -> b) -> a -> b
$ conBV n -> FPRoundingMode -> FP eb sb
forall (eb :: Nat) (sb :: Nat) (n :: Nat).
(ValidFP eb sb, KnownNat n, 1 <= n) =>
conBV n -> FPRoundingMode -> FP eb sb
forall (bv :: Nat -> *) (eb :: Nat) (sb :: Nat) (n :: Nat).
(ConvertibleBound bv, ValidFP eb sb, KnownNat n, 1 <= n) =>
bv n -> FPRoundingMode -> FP eb sb
convertibleLowerBound (conBV n
forall a. HasCallStack => a
undefined :: conBV n) FPRoundingMode
forall mode. IEEEFPRoundingMode mode => mode
rne)
    (SymFP eb sb -> SymFP eb sb) -> SymFP eb sb -> SymFP eb sb
forall a b. (a -> b) -> a -> b
$ SymBool -> SymFP eb sb -> SymFP eb sb -> SymFP eb sb
forall v. ITEOp v => SymBool -> v -> v -> v
symIte
      (SymFPRoundingMode
mode SymFPRoundingMode -> SymFPRoundingMode -> SymBool
forall a. SymEq a => a -> a -> SymBool
.== SymFPRoundingMode
forall mode. IEEEFPRoundingMode mode => mode
rna)
      (FP eb sb -> SymFP eb sb
forall c t. Solvable c t => c -> t
con (FP eb sb -> SymFP eb sb) -> FP eb sb -> SymFP eb sb
forall a b. (a -> b) -> a -> b
$ conBV n -> FPRoundingMode -> FP eb sb
forall (eb :: Nat) (sb :: Nat) (n :: Nat).
(ValidFP eb sb, KnownNat n, 1 <= n) =>
conBV n -> FPRoundingMode -> FP eb sb
forall (bv :: Nat -> *) (eb :: Nat) (sb :: Nat) (n :: Nat).
(ConvertibleBound bv, ValidFP eb sb, KnownNat n, 1 <= n) =>
bv n -> FPRoundingMode -> FP eb sb
convertibleLowerBound (conBV n
forall a. HasCallStack => a
undefined :: conBV n) FPRoundingMode
forall mode. IEEEFPRoundingMode mode => mode
rna)
    (SymFP eb sb -> SymFP eb sb) -> SymFP eb sb -> SymFP eb sb
forall a b. (a -> b) -> a -> b
$ SymBool -> SymFP eb sb -> SymFP eb sb -> SymFP eb sb
forall v. ITEOp v => SymBool -> v -> v -> v
symIte
      (SymFPRoundingMode
mode SymFPRoundingMode -> SymFPRoundingMode -> SymBool
forall a. SymEq a => a -> a -> SymBool
.== SymFPRoundingMode
forall mode. IEEEFPRoundingMode mode => mode
rtp)
      (FP eb sb -> SymFP eb sb
forall c t. Solvable c t => c -> t
con (FP eb sb -> SymFP eb sb) -> FP eb sb -> SymFP eb sb
forall a b. (a -> b) -> a -> b
$ conBV n -> FPRoundingMode -> FP eb sb
forall (eb :: Nat) (sb :: Nat) (n :: Nat).
(ValidFP eb sb, KnownNat n, 1 <= n) =>
conBV n -> FPRoundingMode -> FP eb sb
forall (bv :: Nat -> *) (eb :: Nat) (sb :: Nat) (n :: Nat).
(ConvertibleBound bv, ValidFP eb sb, KnownNat n, 1 <= n) =>
bv n -> FPRoundingMode -> FP eb sb
convertibleLowerBound (conBV n
forall a. HasCallStack => a
undefined :: conBV n) FPRoundingMode
forall mode. IEEEFPRoundingMode mode => mode
rtp)
    (SymFP eb sb -> SymFP eb sb) -> SymFP eb sb -> SymFP eb sb
forall a b. (a -> b) -> a -> b
$ SymBool -> SymFP eb sb -> SymFP eb sb -> SymFP eb sb
forall v. ITEOp v => SymBool -> v -> v -> v
symIte
      (SymFPRoundingMode
mode SymFPRoundingMode -> SymFPRoundingMode -> SymBool
forall a. SymEq a => a -> a -> SymBool
.== SymFPRoundingMode
forall mode. IEEEFPRoundingMode mode => mode
rtn)
      (FP eb sb -> SymFP eb sb
forall c t. Solvable c t => c -> t
con (FP eb sb -> SymFP eb sb) -> FP eb sb -> SymFP eb sb
forall a b. (a -> b) -> a -> b
$ conBV n -> FPRoundingMode -> FP eb sb
forall (eb :: Nat) (sb :: Nat) (n :: Nat).
(ValidFP eb sb, KnownNat n, 1 <= n) =>
conBV n -> FPRoundingMode -> FP eb sb
forall (bv :: Nat -> *) (eb :: Nat) (sb :: Nat) (n :: Nat).
(ConvertibleBound bv, ValidFP eb sb, KnownNat n, 1 <= n) =>
bv n -> FPRoundingMode -> FP eb sb
convertibleLowerBound (conBV n
forall a. HasCallStack => a
undefined :: conBV n) FPRoundingMode
forall mode. IEEEFPRoundingMode mode => mode
rtn)
      (FP eb sb -> SymFP eb sb
forall c t. Solvable c t => c -> t
con (FP eb sb -> SymFP eb sb) -> FP eb sb -> SymFP eb sb
forall a b. (a -> b) -> a -> b
$ conBV n -> FPRoundingMode -> FP eb sb
forall (eb :: Nat) (sb :: Nat) (n :: Nat).
(ValidFP eb sb, KnownNat n, 1 <= n) =>
conBV n -> FPRoundingMode -> FP eb sb
forall (bv :: Nat -> *) (eb :: Nat) (sb :: Nat) (n :: Nat).
(ConvertibleBound bv, ValidFP eb sb, KnownNat n, 1 <= n) =>
bv n -> FPRoundingMode -> FP eb sb
convertibleLowerBound (conBV n
forall a. HasCallStack => a
undefined :: conBV n) FPRoundingMode
forall mode. IEEEFPRoundingMode mode => mode
rtz)

symConvertibleUpperBound ::
  forall conBV symBV n eb sb.
  ( ConvertibleBound conBV,
    ValidFP eb sb,
    KnownNat n,
    1 <= n,
    Solvable (conBV n) (symBV n)
  ) =>
  symBV n ->
  SymFPRoundingMode ->
  SymFP eb sb
symConvertibleUpperBound :: forall (conBV :: Nat -> *) (symBV :: Nat -> *) (n :: Nat)
       (eb :: Nat) (sb :: Nat).
(ConvertibleBound conBV, ValidFP eb sb, KnownNat n, 1 <= n,
 Solvable (conBV n) (symBV n)) =>
symBV n -> SymFPRoundingMode -> SymFP eb sb
symConvertibleUpperBound symBV n
_ SymFPRoundingMode
mode =
  SymBool -> SymFP eb sb -> SymFP eb sb -> SymFP eb sb
forall v. ITEOp v => SymBool -> v -> v -> v
symIte
    (SymFPRoundingMode
mode SymFPRoundingMode -> SymFPRoundingMode -> SymBool
forall a. SymEq a => a -> a -> SymBool
.== SymFPRoundingMode
forall mode. IEEEFPRoundingMode mode => mode
rne)
    (FP eb sb -> SymFP eb sb
forall c t. Solvable c t => c -> t
con (FP eb sb -> SymFP eb sb) -> FP eb sb -> SymFP eb sb
forall a b. (a -> b) -> a -> b
$ conBV n -> FPRoundingMode -> FP eb sb
forall (eb :: Nat) (sb :: Nat) (n :: Nat).
(ValidFP eb sb, KnownNat n, 1 <= n) =>
conBV n -> FPRoundingMode -> FP eb sb
forall (bv :: Nat -> *) (eb :: Nat) (sb :: Nat) (n :: Nat).
(ConvertibleBound bv, ValidFP eb sb, KnownNat n, 1 <= n) =>
bv n -> FPRoundingMode -> FP eb sb
convertibleUpperBound (conBV n
forall a. HasCallStack => a
undefined :: conBV n) FPRoundingMode
forall mode. IEEEFPRoundingMode mode => mode
rne)
    (SymFP eb sb -> SymFP eb sb) -> SymFP eb sb -> SymFP eb sb
forall a b. (a -> b) -> a -> b
$ SymBool -> SymFP eb sb -> SymFP eb sb -> SymFP eb sb
forall v. ITEOp v => SymBool -> v -> v -> v
symIte
      (SymFPRoundingMode
mode SymFPRoundingMode -> SymFPRoundingMode -> SymBool
forall a. SymEq a => a -> a -> SymBool
.== SymFPRoundingMode
forall mode. IEEEFPRoundingMode mode => mode
rna)
      (FP eb sb -> SymFP eb sb
forall c t. Solvable c t => c -> t
con (FP eb sb -> SymFP eb sb) -> FP eb sb -> SymFP eb sb
forall a b. (a -> b) -> a -> b
$ conBV n -> FPRoundingMode -> FP eb sb
forall (eb :: Nat) (sb :: Nat) (n :: Nat).
(ValidFP eb sb, KnownNat n, 1 <= n) =>
conBV n -> FPRoundingMode -> FP eb sb
forall (bv :: Nat -> *) (eb :: Nat) (sb :: Nat) (n :: Nat).
(ConvertibleBound bv, ValidFP eb sb, KnownNat n, 1 <= n) =>
bv n -> FPRoundingMode -> FP eb sb
convertibleUpperBound (conBV n
forall a. HasCallStack => a
undefined :: conBV n) FPRoundingMode
forall mode. IEEEFPRoundingMode mode => mode
rna)
    (SymFP eb sb -> SymFP eb sb) -> SymFP eb sb -> SymFP eb sb
forall a b. (a -> b) -> a -> b
$ SymBool -> SymFP eb sb -> SymFP eb sb -> SymFP eb sb
forall v. ITEOp v => SymBool -> v -> v -> v
symIte
      (SymFPRoundingMode
mode SymFPRoundingMode -> SymFPRoundingMode -> SymBool
forall a. SymEq a => a -> a -> SymBool
.== SymFPRoundingMode
forall mode. IEEEFPRoundingMode mode => mode
rtp)
      (FP eb sb -> SymFP eb sb
forall c t. Solvable c t => c -> t
con (FP eb sb -> SymFP eb sb) -> FP eb sb -> SymFP eb sb
forall a b. (a -> b) -> a -> b
$ conBV n -> FPRoundingMode -> FP eb sb
forall (eb :: Nat) (sb :: Nat) (n :: Nat).
(ValidFP eb sb, KnownNat n, 1 <= n) =>
conBV n -> FPRoundingMode -> FP eb sb
forall (bv :: Nat -> *) (eb :: Nat) (sb :: Nat) (n :: Nat).
(ConvertibleBound bv, ValidFP eb sb, KnownNat n, 1 <= n) =>
bv n -> FPRoundingMode -> FP eb sb
convertibleUpperBound (conBV n
forall a. HasCallStack => a
undefined :: conBV n) FPRoundingMode
forall mode. IEEEFPRoundingMode mode => mode
rtp)
    (SymFP eb sb -> SymFP eb sb) -> SymFP eb sb -> SymFP eb sb
forall a b. (a -> b) -> a -> b
$ SymBool -> SymFP eb sb -> SymFP eb sb -> SymFP eb sb
forall v. ITEOp v => SymBool -> v -> v -> v
symIte
      (SymFPRoundingMode
mode SymFPRoundingMode -> SymFPRoundingMode -> SymBool
forall a. SymEq a => a -> a -> SymBool
.== SymFPRoundingMode
forall mode. IEEEFPRoundingMode mode => mode
rtn)
      (FP eb sb -> SymFP eb sb
forall c t. Solvable c t => c -> t
con (FP eb sb -> SymFP eb sb) -> FP eb sb -> SymFP eb sb
forall a b. (a -> b) -> a -> b
$ conBV n -> FPRoundingMode -> FP eb sb
forall (eb :: Nat) (sb :: Nat) (n :: Nat).
(ValidFP eb sb, KnownNat n, 1 <= n) =>
conBV n -> FPRoundingMode -> FP eb sb
forall (bv :: Nat -> *) (eb :: Nat) (sb :: Nat) (n :: Nat).
(ConvertibleBound bv, ValidFP eb sb, KnownNat n, 1 <= n) =>
bv n -> FPRoundingMode -> FP eb sb
convertibleUpperBound (conBV n
forall a. HasCallStack => a
undefined :: conBV n) FPRoundingMode
forall mode. IEEEFPRoundingMode mode => mode
rtn)
      (FP eb sb -> SymFP eb sb
forall c t. Solvable c t => c -> t
con (FP eb sb -> SymFP eb sb) -> FP eb sb -> SymFP eb sb
forall a b. (a -> b) -> a -> b
$ conBV n -> FPRoundingMode -> FP eb sb
forall (eb :: Nat) (sb :: Nat) (n :: Nat).
(ValidFP eb sb, KnownNat n, 1 <= n) =>
conBV n -> FPRoundingMode -> FP eb sb
forall (bv :: Nat -> *) (eb :: Nat) (sb :: Nat) (n :: Nat).
(ConvertibleBound bv, ValidFP eb sb, KnownNat n, 1 <= n) =>
bv n -> FPRoundingMode -> FP eb sb
convertibleUpperBound (conBV n
forall a. HasCallStack => a
undefined :: conBV n) FPRoundingMode
forall mode. IEEEFPRoundingMode mode => mode
rtz)

instance
  ( MonadError NotRepresentableFPError m,
    MonadUnion m,
    ValidFP eb sb,
    KnownNat n,
    1 <= n
  ) =>
  SafeFromFP NotRepresentableFPError (SymWordN n) (SymFP eb sb) SymFPRoundingMode m
  where
  safeFromFP :: SymFPRoundingMode -> SymFP eb sb -> m (SymWordN n)
safeFromFP SymFPRoundingMode
mode SymFP eb sb
a =
    SymBool -> m (SymWordN n) -> m (SymWordN n) -> m (SymWordN n)
forall (u :: * -> *) a.
(SymBranching u, Mergeable a) =>
SymBool -> u a -> u a -> u a
mrgIf (SymFP eb sb -> SymBool
forall a. SymIEEEFPTraits a => a -> SymBool
symFpIsPositiveInfinite SymFP eb sb
a) (m (SymWordN n) -> m (SymWordN n)
forall (m :: * -> *) a. (TryMerge m, Mergeable a) => m a -> m a
tryMerge (m (SymWordN n) -> m (SymWordN n))
-> m (SymWordN n) -> m (SymWordN n)
forall a b. (a -> b) -> a -> b
$ NotRepresentableFPError -> m (SymWordN n)
forall a. NotRepresentableFPError -> m a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError NotRepresentableFPError
FPOverflowError)
      (m (SymWordN n) -> m (SymWordN n))
-> m (SymWordN n) -> m (SymWordN n)
forall a b. (a -> b) -> a -> b
$ SymBool -> m (SymWordN n) -> m (SymWordN n) -> m (SymWordN n)
forall (u :: * -> *) a.
(SymBranching u, Mergeable a) =>
SymBool -> u a -> u a -> u a
mrgIf
        (SymFP eb sb -> SymBool
forall a. SymIEEEFPTraits a => a -> SymBool
symFpIsNegativeInfinite SymFP eb sb
a)
        (m (SymWordN n) -> m (SymWordN n)
forall (m :: * -> *) a. (TryMerge m, Mergeable a) => m a -> m a
tryMerge (m (SymWordN n) -> m (SymWordN n))
-> m (SymWordN n) -> m (SymWordN n)
forall a b. (a -> b) -> a -> b
$ NotRepresentableFPError -> m (SymWordN n)
forall a. NotRepresentableFPError -> m a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError NotRepresentableFPError
FPUnderflowError)
      (m (SymWordN n) -> m (SymWordN n))
-> m (SymWordN n) -> m (SymWordN n)
forall a b. (a -> b) -> a -> b
$ SymBool -> m (SymWordN n) -> m (SymWordN n) -> m (SymWordN n)
forall (u :: * -> *) a.
(SymBranching u, Mergeable a) =>
SymBool -> u a -> u a -> u a
mrgIf (SymFP eb sb -> SymBool
forall a. SymIEEEFPTraits a => a -> SymBool
symFpIsNaN SymFP eb sb
a) (m (SymWordN n) -> m (SymWordN n)
forall (m :: * -> *) a. (TryMerge m, Mergeable a) => m a -> m a
tryMerge (m (SymWordN n) -> m (SymWordN n))
-> m (SymWordN n) -> m (SymWordN n)
forall a b. (a -> b) -> a -> b
$ NotRepresentableFPError -> m (SymWordN n)
forall a. NotRepresentableFPError -> m a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError NotRepresentableFPError
NaNError)
      (m (SymWordN n) -> m (SymWordN n))
-> m (SymWordN n) -> m (SymWordN n)
forall a b. (a -> b) -> a -> b
$ SymBool -> m (SymWordN n) -> m (SymWordN n) -> m (SymWordN n)
forall (u :: * -> *) a.
(SymBranching u, Mergeable a) =>
SymBool -> u a -> u a -> u a
mrgIf
        (SymFP eb sb
a SymFP eb sb -> SymFP eb sb -> SymBool
forall a. SymOrd a => a -> a -> SymBool
.< SymWordN n -> SymFPRoundingMode -> SymFP eb sb
forall (conBV :: Nat -> *) (symBV :: Nat -> *) (n :: Nat)
       (eb :: Nat) (sb :: Nat).
(ConvertibleBound conBV, ValidFP eb sb, KnownNat n, 1 <= n,
 Solvable (conBV n) (symBV n)) =>
symBV n -> SymFPRoundingMode -> SymFP eb sb
symConvertibleLowerBound (SymWordN n
forall a. HasCallStack => a
undefined :: SymWordN n) SymFPRoundingMode
mode)
        (m (SymWordN n) -> m (SymWordN n)
forall (m :: * -> *) a. (TryMerge m, Mergeable a) => m a -> m a
tryMerge (m (SymWordN n) -> m (SymWordN n))
-> m (SymWordN n) -> m (SymWordN n)
forall a b. (a -> b) -> a -> b
$ NotRepresentableFPError -> m (SymWordN n)
forall a. NotRepresentableFPError -> m a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError NotRepresentableFPError
FPUnderflowError)
      (m (SymWordN n) -> m (SymWordN n))
-> m (SymWordN n) -> m (SymWordN n)
forall a b. (a -> b) -> a -> b
$ SymBool -> m (SymWordN n) -> m (SymWordN n) -> m (SymWordN n)
forall (u :: * -> *) a.
(SymBranching u, Mergeable a) =>
SymBool -> u a -> u a -> u a
mrgIf
        (SymFP eb sb
a SymFP eb sb -> SymFP eb sb -> SymBool
forall a. SymOrd a => a -> a -> SymBool
.> SymWordN n -> SymFPRoundingMode -> SymFP eb sb
forall (conBV :: Nat -> *) (symBV :: Nat -> *) (n :: Nat)
       (eb :: Nat) (sb :: Nat).
(ConvertibleBound conBV, ValidFP eb sb, KnownNat n, 1 <= n,
 Solvable (conBV n) (symBV n)) =>
symBV n -> SymFPRoundingMode -> SymFP eb sb
symConvertibleUpperBound (SymWordN n
forall a. HasCallStack => a
undefined :: SymWordN n) SymFPRoundingMode
mode)
        (m (SymWordN n) -> m (SymWordN n)
forall (m :: * -> *) a. (TryMerge m, Mergeable a) => m a -> m a
tryMerge (m (SymWordN n) -> m (SymWordN n))
-> m (SymWordN n) -> m (SymWordN n)
forall a b. (a -> b) -> a -> b
$ NotRepresentableFPError -> m (SymWordN n)
forall a. NotRepresentableFPError -> m a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError NotRepresentableFPError
FPOverflowError)
      (m (SymWordN n) -> m (SymWordN n))
-> m (SymWordN n) -> m (SymWordN n)
forall a b. (a -> b) -> a -> b
$ SymWordN n -> m (SymWordN n)
forall (m :: * -> *) a.
(TryMerge m, Applicative m, Mergeable a) =>
a -> m a
mrgSingle
      (SymWordN n -> m (SymWordN n)) -> SymWordN n -> m (SymWordN n)
forall a b. (a -> b) -> a -> b
$ SymWordN n -> SymFPRoundingMode -> SymFP eb sb -> SymWordN n
forall a fp mode.
IEEEFPConvertible a fp mode =>
a -> mode -> fp -> a
fromFPOr SymWordN n
0 SymFPRoundingMode
mode SymFP eb sb
a

instance
  ( MonadError NotRepresentableFPError m,
    TryMerge m,
    ValidFP eb sb,
    KnownNat n,
    1 <= n
  ) =>
  SafeFromFP NotRepresentableFPError (IntN n) (FP eb sb) FPRoundingMode m
  where
  safeFromFP :: FPRoundingMode -> FP eb sb -> m (IntN n)
safeFromFP FPRoundingMode
mode FP eb sb
a = do
    p :: Integer <- FPRoundingMode -> FP eb sb -> m Integer
forall e a fp fprd (m :: * -> *).
SafeFromFP e a fp fprd m =>
fprd -> fp -> m a
safeFromFP FPRoundingMode
mode FP eb sb
a
    if p < (fromIntegral (minBound :: IntN n))
      then tryMerge $ throwError FPUnderflowError
      else
        if p > (fromIntegral (maxBound :: IntN n))
          then tryMerge $ throwError FPOverflowError
          else mrgSingle $ fromIntegral p

instance
  ( MonadError NotRepresentableFPError m,
    MonadUnion m,
    ValidFP eb sb,
    KnownNat n,
    1 <= n
  ) =>
  SafeFromFP NotRepresentableFPError (SymIntN n) (SymFP eb sb) SymFPRoundingMode m
  where
  safeFromFP :: SymFPRoundingMode -> SymFP eb sb -> m (SymIntN n)
safeFromFP SymFPRoundingMode
mode SymFP eb sb
a =
    SymBool -> m (SymIntN n) -> m (SymIntN n) -> m (SymIntN n)
forall (u :: * -> *) a.
(SymBranching u, Mergeable a) =>
SymBool -> u a -> u a -> u a
mrgIf (SymFP eb sb -> SymBool
forall a. SymIEEEFPTraits a => a -> SymBool
symFpIsPositiveInfinite SymFP eb sb
a) (m (SymIntN n) -> m (SymIntN n)
forall (m :: * -> *) a. (TryMerge m, Mergeable a) => m a -> m a
tryMerge (m (SymIntN n) -> m (SymIntN n)) -> m (SymIntN n) -> m (SymIntN n)
forall a b. (a -> b) -> a -> b
$ NotRepresentableFPError -> m (SymIntN n)
forall a. NotRepresentableFPError -> m a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError NotRepresentableFPError
FPOverflowError)
      (m (SymIntN n) -> m (SymIntN n)) -> m (SymIntN n) -> m (SymIntN n)
forall a b. (a -> b) -> a -> b
$ SymBool -> m (SymIntN n) -> m (SymIntN n) -> m (SymIntN n)
forall (u :: * -> *) a.
(SymBranching u, Mergeable a) =>
SymBool -> u a -> u a -> u a
mrgIf
        (SymFP eb sb -> SymBool
forall a. SymIEEEFPTraits a => a -> SymBool
symFpIsNegativeInfinite SymFP eb sb
a)
        (m (SymIntN n) -> m (SymIntN n)
forall (m :: * -> *) a. (TryMerge m, Mergeable a) => m a -> m a
tryMerge (m (SymIntN n) -> m (SymIntN n)) -> m (SymIntN n) -> m (SymIntN n)
forall a b. (a -> b) -> a -> b
$ NotRepresentableFPError -> m (SymIntN n)
forall a. NotRepresentableFPError -> m a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError NotRepresentableFPError
FPUnderflowError)
      (m (SymIntN n) -> m (SymIntN n)) -> m (SymIntN n) -> m (SymIntN n)
forall a b. (a -> b) -> a -> b
$ SymBool -> m (SymIntN n) -> m (SymIntN n) -> m (SymIntN n)
forall (u :: * -> *) a.
(SymBranching u, Mergeable a) =>
SymBool -> u a -> u a -> u a
mrgIf (SymFP eb sb -> SymBool
forall a. SymIEEEFPTraits a => a -> SymBool
symFpIsNaN SymFP eb sb
a) (m (SymIntN n) -> m (SymIntN n)
forall (m :: * -> *) a. (TryMerge m, Mergeable a) => m a -> m a
tryMerge (m (SymIntN n) -> m (SymIntN n)) -> m (SymIntN n) -> m (SymIntN n)
forall a b. (a -> b) -> a -> b
$ NotRepresentableFPError -> m (SymIntN n)
forall a. NotRepresentableFPError -> m a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError NotRepresentableFPError
NaNError)
      (m (SymIntN n) -> m (SymIntN n)) -> m (SymIntN n) -> m (SymIntN n)
forall a b. (a -> b) -> a -> b
$ SymBool -> m (SymIntN n) -> m (SymIntN n) -> m (SymIntN n)
forall (u :: * -> *) a.
(SymBranching u, Mergeable a) =>
SymBool -> u a -> u a -> u a
mrgIf
        (SymFP eb sb
a SymFP eb sb -> SymFP eb sb -> SymBool
forall a. SymOrd a => a -> a -> SymBool
.< SymIntN n -> SymFPRoundingMode -> SymFP eb sb
forall (conBV :: Nat -> *) (symBV :: Nat -> *) (n :: Nat)
       (eb :: Nat) (sb :: Nat).
(ConvertibleBound conBV, ValidFP eb sb, KnownNat n, 1 <= n,
 Solvable (conBV n) (symBV n)) =>
symBV n -> SymFPRoundingMode -> SymFP eb sb
symConvertibleLowerBound (SymIntN n
forall a. HasCallStack => a
undefined :: SymIntN n) SymFPRoundingMode
mode)
        (m (SymIntN n) -> m (SymIntN n)
forall (m :: * -> *) a. (TryMerge m, Mergeable a) => m a -> m a
tryMerge (m (SymIntN n) -> m (SymIntN n)) -> m (SymIntN n) -> m (SymIntN n)
forall a b. (a -> b) -> a -> b
$ NotRepresentableFPError -> m (SymIntN n)
forall a. NotRepresentableFPError -> m a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError NotRepresentableFPError
FPUnderflowError)
      (m (SymIntN n) -> m (SymIntN n)) -> m (SymIntN n) -> m (SymIntN n)
forall a b. (a -> b) -> a -> b
$ SymBool -> m (SymIntN n) -> m (SymIntN n) -> m (SymIntN n)
forall (u :: * -> *) a.
(SymBranching u, Mergeable a) =>
SymBool -> u a -> u a -> u a
mrgIf
        (SymFP eb sb
a SymFP eb sb -> SymFP eb sb -> SymBool
forall a. SymOrd a => a -> a -> SymBool
.> SymIntN n -> SymFPRoundingMode -> SymFP eb sb
forall (conBV :: Nat -> *) (symBV :: Nat -> *) (n :: Nat)
       (eb :: Nat) (sb :: Nat).
(ConvertibleBound conBV, ValidFP eb sb, KnownNat n, 1 <= n,
 Solvable (conBV n) (symBV n)) =>
symBV n -> SymFPRoundingMode -> SymFP eb sb
symConvertibleUpperBound (SymIntN n
forall a. HasCallStack => a
undefined :: SymIntN n) SymFPRoundingMode
mode)
        (m (SymIntN n) -> m (SymIntN n)
forall (m :: * -> *) a. (TryMerge m, Mergeable a) => m a -> m a
tryMerge (m (SymIntN n) -> m (SymIntN n)) -> m (SymIntN n) -> m (SymIntN n)
forall a b. (a -> b) -> a -> b
$ NotRepresentableFPError -> m (SymIntN n)
forall a. NotRepresentableFPError -> m a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError NotRepresentableFPError
FPOverflowError)
      (m (SymIntN n) -> m (SymIntN n)) -> m (SymIntN n) -> m (SymIntN n)
forall a b. (a -> b) -> a -> b
$ SymIntN n -> m (SymIntN n)
forall (m :: * -> *) a.
(TryMerge m, Applicative m, Mergeable a) =>
a -> m a
mrgSingle
      (SymIntN n -> m (SymIntN n)) -> SymIntN n -> m (SymIntN n)
forall a b. (a -> b) -> a -> b
$ SymIntN n -> SymFPRoundingMode -> SymFP eb sb -> SymIntN n
forall a fp mode.
IEEEFPConvertible a fp mode =>
a -> mode -> fp -> a
fromFPOr SymIntN n
0 SymFPRoundingMode
mode SymFP eb sb
a