{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}

-- |
-- Module      :   Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalIEEEFPConvertibleTerm
-- 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.Prim.Internal.Instances.PEvalIEEEFPConvertibleTerm
  ( genericFPCast,
  )
where

import Data.Proxy (Proxy (Proxy))
import qualified Data.SBV as SBV
import qualified Data.SBV.Internals as SBVI
import GHC.TypeLits (KnownNat, Nat, type (<=))
import Grisette.Internal.Core.Data.Class.IEEEFP
  ( IEEEFPConstants
      ( fpNaN,
        fpNegativeInfinite,
        fpNegativeZero,
        fpPositiveInfinite,
        fpPositiveZero
      ),
    IEEEFPConvertible (fromFPOr, toFP),
    fpIsInfinite,
    fpIsNaN,
    fpIsNegativeInfinite,
    fpIsNegativeZero,
    fpIsPositiveInfinite,
    fpIsPositiveZero,
  )
import Grisette.Internal.SymPrim.AlgReal (AlgReal)
import Grisette.Internal.SymPrim.BV (IntN, WordN)
import Grisette.Internal.SymPrim.FP
  ( ConvertibleBound (convertibleLowerBound, convertibleUpperBound),
    FP,
    FPRoundingMode (RNA, RNE, RTN, RTP, RTZ),
    ValidFP,
  )
import Grisette.Internal.SymPrim.Prim.Internal.Instances.SupportedPrim
  ( bvIsNonZeroFromGEq1,
  )
import Grisette.Internal.SymPrim.Prim.Internal.Term
  ( PEvalIEEEFPConvertibleTerm
      ( pevalFromFPOrTerm,
        pevalToFPTerm,
        sbvFromFPOrTerm,
        sbvToFPTerm
      ),
    SBVRep (SBVType),
    SupportedPrim (conSBVTerm),
    Term,
    conTerm,
    fromFPOrTerm,
    toFPTerm,
    pattern ConTerm,
  )
import Grisette.Internal.SymPrim.Prim.Internal.Unfold (binaryUnfoldOnce)

-- | Generic implementation for floating-point casting operators for sbv.
genericFPCast ::
  forall a r.
  (SBV.HasKind a, SBV.HasKind r) =>
  SBV.SRoundingMode ->
  SBV.SBV a ->
  SBV.SBV r
genericFPCast :: forall a r.
(HasKind a, HasKind r) =>
SRoundingMode -> SBV a -> SBV r
genericFPCast SRoundingMode
rm SBV a
f = SVal -> SBV r
forall a. SVal -> SBV a
SBVI.SBV (Kind -> Either CV (Cached SV) -> SVal
SBVI.SVal Kind
kTo (Cached SV -> Either CV (Cached SV)
forall a b. b -> Either a b
Right ((State -> IO SV) -> Cached SV
forall a. (State -> IO a) -> Cached a
SBVI.cache State -> IO SV
r)))
  where
    kFrom :: Kind
kFrom = SBV a -> Kind
forall a. HasKind a => a -> Kind
SBVI.kindOf SBV a
f
    kTo :: Kind
kTo = Proxy r -> Kind
forall a. HasKind a => a -> Kind
SBVI.kindOf (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @r)
    r :: State -> IO SV
r State
st = do
      msv <- State -> SRoundingMode -> IO SV
forall a. State -> SBV a -> IO SV
SBVI.sbvToSV State
st SRoundingMode
rm
      xsv <- SBVI.sbvToSV st f
      SBVI.newExpr st kTo $
        SBVI.SBVApp
          (SBVI.IEEEFP (SBVI.FP_Cast kFrom kTo msv))
          [xsv]

boundedSBVFromFPTerm ::
  forall bv (n :: Nat) eb sb r.
  ( ValidFP eb sb,
    SBVI.HasKind r,
    SBVI.SymVal r,
    Bounded r,
    Num r,
    Ord r,
    SBVI.SBV r ~ SBVType (bv n),
    KnownNat n,
    1 <= n,
    ConvertibleBound bv
  ) =>
  SBVI.SBV r ->
  SBVType FPRoundingMode ->
  SBVType (FP eb sb) ->
  SBVI.SBV r
boundedSBVFromFPTerm :: forall (bv :: Nat -> *) (n :: Nat) (eb :: Nat) (sb :: Nat) r.
(ValidFP eb sb, HasKind r, SymVal r, Bounded r, Num r, Ord r,
 SBV r ~ SBVType (bv n), KnownNat n, 1 <= n, ConvertibleBound bv) =>
SBV r -> SBVType FPRoundingMode -> SBVType (FP eb sb) -> SBV r
boundedSBVFromFPTerm SBV r
d SBVType FPRoundingMode
mode SBVType (FP eb sb)
l =
  SBool -> SBV r -> SBV r -> SBV r
forall a. Mergeable a => SBool -> a -> a -> a
SBV.ite
    ( SBV (FloatingPoint eb sb) -> SBool
forall a. IEEEFloating a => SBV a -> SBool
SBV.fpIsNaN SBV (FloatingPoint eb sb)
SBVType (FP eb sb)
l
        SBool -> SBool -> SBool
SBV..|| SBV (FloatingPoint eb sb) -> SBool
forall a. IEEEFloating a => SBV a -> SBool
SBV.fpIsInfinite SBV (FloatingPoint eb sb)
SBVType (FP eb sb)
l
        SBool -> SBool -> SBool
SBV..|| SBV (FloatingPoint eb sb)
SBVType (FP eb sb)
l SBV (FloatingPoint eb sb) -> SBV (FloatingPoint eb sb) -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
SBV..< (bv n -> FPRoundingMode -> FP eb sb) -> SBV (FloatingPoint eb sb)
bound bv n -> FPRoundingMode -> FP eb sb
forall (eb :: Nat) (sb :: Nat) (n :: Nat).
(ValidFP eb sb, KnownNat n, 1 <= n) =>
bv 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
        SBool -> SBool -> SBool
SBV..|| SBV (FloatingPoint eb sb)
SBVType (FP eb sb)
l SBV (FloatingPoint eb sb) -> SBV (FloatingPoint eb sb) -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
SBV..> (bv n -> FPRoundingMode -> FP eb sb) -> SBV (FloatingPoint eb sb)
bound bv n -> FPRoundingMode -> FP eb sb
forall (eb :: Nat) (sb :: Nat) (n :: Nat).
(ValidFP eb sb, KnownNat n, 1 <= n) =>
bv 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
    )
    SBV r
d
    (SBV r -> SBV r) -> SBV r -> SBV r
forall a b. (a -> b) -> a -> b
$ SRoundingMode -> SBV (FloatingPoint eb sb) -> SBV r
forall a r.
(HasKind a, HasKind r) =>
SRoundingMode -> SBV a -> SBV r
genericFPCast SRoundingMode
SBVType FPRoundingMode
mode SBV (FloatingPoint eb sb)
SBVType (FP eb sb)
l
  where
    lst :: [(SRoundingMode, FPRoundingMode)]
lst =
      [ (SRoundingMode
SBV.sRTP, FPRoundingMode
RTP),
        (SRoundingMode
SBV.sRTN, FPRoundingMode
RTN),
        (SRoundingMode
SBV.sRTZ, FPRoundingMode
RTZ),
        (SRoundingMode
SBV.sRNE, FPRoundingMode
RNE),
        (SRoundingMode
SBV.sRNA, FPRoundingMode
RNA)
      ]
    bound :: (bv n -> FPRoundingMode -> FP eb sb) -> SBV (FloatingPoint eb sb)
bound bv n -> FPRoundingMode -> FP eb sb
f =
      (SBV (FloatingPoint eb sb)
 -> (SRoundingMode, FPRoundingMode) -> SBV (FloatingPoint eb sb))
-> SBV (FloatingPoint eb sb)
-> [(SRoundingMode, FPRoundingMode)]
-> SBV (FloatingPoint eb sb)
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl
        ( \SBV (FloatingPoint eb sb)
acc (SRoundingMode
srm, FPRoundingMode
rm) ->
            SBool
-> SBV (FloatingPoint eb sb)
-> SBV (FloatingPoint eb sb)
-> SBV (FloatingPoint eb sb)
forall a. Mergeable a => SBool -> a -> a -> a
SBV.ite
              (SRoundingMode
SBVType FPRoundingMode
mode SRoundingMode -> SRoundingMode -> SBool
forall a. EqSymbolic a => a -> a -> SBool
SBV..== SRoundingMode
srm)
              (FP eb sb -> SBVType (FP eb sb)
forall t. SupportedPrim t => t -> SBVType t
conSBVTerm (bv n -> FPRoundingMode -> FP eb sb
f (bv n
forall a. HasCallStack => a
undefined :: bv n) FPRoundingMode
rm :: FP eb sb))
              SBV (FloatingPoint eb sb)
acc
        )
        (SBV (FloatingPoint eb sb)
SBVType (FP eb sb)
0 :: SBVType (FP eb sb))
        [(SRoundingMode, FPRoundingMode)]
lst

generalPevalFromFPOrTerm ::
  ( PEvalIEEEFPConvertibleTerm a,
    ValidFP eb sb,
    SupportedPrim a,
    IEEEFPConvertible a (FP eb sb) FPRoundingMode
  ) =>
  Term a ->
  Term FPRoundingMode ->
  Term (FP eb sb) ->
  Term a
generalPevalFromFPOrTerm :: forall a (eb :: Nat) (sb :: Nat).
(PEvalIEEEFPConvertibleTerm a, ValidFP eb sb, SupportedPrim a,
 IEEEFPConvertible a (FP eb sb) FPRoundingMode) =>
Term a -> Term FPRoundingMode -> Term (FP eb sb) -> Term a
generalPevalFromFPOrTerm (ConTerm a
d) (ConTerm FPRoundingMode
rd) (ConTerm FP eb sb
f) =
  a -> Term a
forall t. SupportedPrim t => t -> Term t
conTerm (a -> Term a) -> a -> Term a
forall a b. (a -> b) -> a -> b
$ a -> FPRoundingMode -> FP eb sb -> a
forall a fp mode.
IEEEFPConvertible a fp mode =>
a -> mode -> fp -> a
fromFPOr a
d FPRoundingMode
rd FP eb sb
f
generalPevalFromFPOrTerm Term a
d Term FPRoundingMode
_ (ConTerm FP eb sb
f) | FP eb sb -> Bool
forall a. RealFloat a => a -> Bool
fpIsNaN FP eb sb
f Bool -> Bool -> Bool
|| FP eb sb -> Bool
forall a. RealFloat a => a -> Bool
fpIsInfinite FP eb sb
f = Term a
d
generalPevalFromFPOrTerm Term a
d Term FPRoundingMode
rd Term (FP eb sb)
f = Term a -> Term FPRoundingMode -> Term (FP eb sb) -> Term a
forall a (eb :: Nat) (sb :: Nat).
(PEvalIEEEFPConvertibleTerm a, ValidFP eb sb) =>
Term a -> Term FPRoundingMode -> Term (FP eb sb) -> Term a
fromFPOrTerm Term a
d Term FPRoundingMode
rd Term (FP eb sb)
f

algRealPevalFromFPOrTerm ::
  ( PEvalIEEEFPConvertibleTerm AlgReal,
    ValidFP eb sb,
    IEEEFPConvertible AlgReal (FP eb sb) FPRoundingMode
  ) =>
  Term AlgReal ->
  Term FPRoundingMode ->
  Term (FP eb sb) ->
  Term AlgReal
algRealPevalFromFPOrTerm :: forall (eb :: Nat) (sb :: Nat).
(PEvalIEEEFPConvertibleTerm AlgReal, ValidFP eb sb,
 IEEEFPConvertible AlgReal (FP eb sb) FPRoundingMode) =>
Term AlgReal
-> Term FPRoundingMode -> Term (FP eb sb) -> Term AlgReal
algRealPevalFromFPOrTerm (ConTerm AlgReal
d) Term FPRoundingMode
_ (ConTerm FP eb sb
f) =
  AlgReal -> Term AlgReal
forall t. SupportedPrim t => t -> Term t
conTerm (AlgReal -> Term AlgReal) -> AlgReal -> Term 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
d FPRoundingMode
RNE FP eb sb
f
algRealPevalFromFPOrTerm Term AlgReal
d Term FPRoundingMode
_ (ConTerm FP eb sb
f) | FP eb sb -> Bool
forall a. RealFloat a => a -> Bool
fpIsNaN FP eb sb
f Bool -> Bool -> Bool
|| FP eb sb -> Bool
forall a. RealFloat a => a -> Bool
fpIsInfinite FP eb sb
f = Term AlgReal
d
algRealPevalFromFPOrTerm Term AlgReal
d Term FPRoundingMode
_ Term (FP eb sb)
f = Term AlgReal
-> Term FPRoundingMode -> Term (FP eb sb) -> Term AlgReal
forall a (eb :: Nat) (sb :: Nat).
(PEvalIEEEFPConvertibleTerm a, ValidFP eb sb) =>
Term a -> Term FPRoundingMode -> Term (FP eb sb) -> Term a
fromFPOrTerm Term AlgReal
d (FPRoundingMode -> Term FPRoundingMode
forall t. SupportedPrim t => t -> Term t
conTerm FPRoundingMode
RNE) Term (FP eb sb)
f

generalDoPevalToFPTerm ::
  ( PEvalIEEEFPConvertibleTerm a,
    ValidFP eb sb,
    IEEEFPConvertible a (FP eb sb) FPRoundingMode
  ) =>
  Term FPRoundingMode ->
  Term a ->
  Maybe (Term (FP eb sb))
generalDoPevalToFPTerm :: forall a (eb :: Nat) (sb :: Nat).
(PEvalIEEEFPConvertibleTerm a, ValidFP eb sb,
 IEEEFPConvertible a (FP eb sb) FPRoundingMode) =>
Term FPRoundingMode -> Term a -> Maybe (Term (FP eb sb))
generalDoPevalToFPTerm (ConTerm FPRoundingMode
rd) (ConTerm a
f) =
  Term (FP eb sb) -> Maybe (Term (FP eb sb))
forall a. a -> Maybe a
Just (Term (FP eb sb) -> Maybe (Term (FP eb sb)))
-> Term (FP eb sb) -> Maybe (Term (FP eb sb))
forall a b. (a -> b) -> a -> b
$ FP eb sb -> Term (FP eb sb)
forall t. SupportedPrim t => t -> Term t
conTerm (FP eb sb -> Term (FP eb sb)) -> FP eb sb -> Term (FP eb sb)
forall a b. (a -> b) -> a -> b
$ FPRoundingMode -> a -> FP eb sb
forall a fp mode. IEEEFPConvertible a fp mode => mode -> a -> fp
toFP FPRoundingMode
rd a
f
generalDoPevalToFPTerm Term FPRoundingMode
_ Term a
_ = Maybe (Term (FP eb sb))
forall a. Maybe a
Nothing

generalPevalToFPTerm ::
  ( PEvalIEEEFPConvertibleTerm a,
    ValidFP eb sb,
    IEEEFPConvertible a (FP eb sb) FPRoundingMode
  ) =>
  Term FPRoundingMode ->
  Term a ->
  Term (FP eb sb)
generalPevalToFPTerm :: forall a (eb :: Nat) (sb :: Nat).
(PEvalIEEEFPConvertibleTerm a, ValidFP eb sb,
 IEEEFPConvertible a (FP eb sb) FPRoundingMode) =>
Term FPRoundingMode -> Term a -> Term (FP eb sb)
generalPevalToFPTerm = PartialRuleBinary FPRoundingMode a (FP eb sb)
-> TotalRuleBinary FPRoundingMode a (FP eb sb)
-> TotalRuleBinary FPRoundingMode a (FP eb sb)
forall a b c.
SupportedPrim c =>
PartialRuleBinary a b c
-> TotalRuleBinary a b c -> TotalRuleBinary a b c
binaryUnfoldOnce PartialRuleBinary FPRoundingMode a (FP eb sb)
forall a (eb :: Nat) (sb :: Nat).
(PEvalIEEEFPConvertibleTerm a, ValidFP eb sb,
 IEEEFPConvertible a (FP eb sb) FPRoundingMode) =>
Term FPRoundingMode -> Term a -> Maybe (Term (FP eb sb))
generalDoPevalToFPTerm TotalRuleBinary FPRoundingMode a (FP eb sb)
forall a (eb :: Nat) (sb :: Nat).
(PEvalIEEEFPConvertibleTerm a, ValidFP eb sb,
 SupportedPrim (FP eb sb)) =>
Term FPRoundingMode -> Term a -> Term (FP eb sb)
toFPTerm

fpDoPevalToFPTerm ::
  ( ValidFP eb sb,
    ValidFP eb1 sb1,
    IEEEFPConvertible (FP eb1 sb1) (FP eb sb) FPRoundingMode
  ) =>
  Term FPRoundingMode ->
  Term (FP eb1 sb1) ->
  Maybe (Term (FP eb sb))
fpDoPevalToFPTerm :: forall (eb :: Nat) (sb :: Nat) (eb1 :: Nat) (sb1 :: Nat).
(ValidFP eb sb, ValidFP eb1 sb1,
 IEEEFPConvertible (FP eb1 sb1) (FP eb sb) FPRoundingMode) =>
Term FPRoundingMode -> Term (FP eb1 sb1) -> Maybe (Term (FP eb sb))
fpDoPevalToFPTerm (ConTerm FPRoundingMode
rd) (ConTerm FP eb1 sb1
f) =
  Term (FP eb sb) -> Maybe (Term (FP eb sb))
forall a. a -> Maybe a
Just (Term (FP eb sb) -> Maybe (Term (FP eb sb)))
-> Term (FP eb sb) -> Maybe (Term (FP eb sb))
forall a b. (a -> b) -> a -> b
$ FP eb sb -> Term (FP eb sb)
forall t. SupportedPrim t => t -> Term t
conTerm (FP eb sb -> Term (FP eb sb)) -> FP eb sb -> Term (FP eb sb)
forall a b. (a -> b) -> a -> b
$ FPRoundingMode -> FP eb1 sb1 -> FP eb sb
forall a fp mode. IEEEFPConvertible a fp mode => mode -> a -> fp
toFP FPRoundingMode
rd FP eb1 sb1
f
fpDoPevalToFPTerm Term FPRoundingMode
_ (ConTerm FP eb1 sb1
f)
  | FP eb1 sb1 -> Bool
forall a. RealFloat a => a -> Bool
fpIsNaN FP eb1 sb1
f = Term (FP eb sb) -> Maybe (Term (FP eb sb))
forall a. a -> Maybe a
Just (Term (FP eb sb) -> Maybe (Term (FP eb sb)))
-> Term (FP eb sb) -> Maybe (Term (FP eb sb))
forall a b. (a -> b) -> a -> b
$ FP eb sb -> Term (FP eb sb)
forall t. SupportedPrim t => t -> Term t
conTerm FP eb sb
forall a. IEEEFPConstants a => a
fpNaN
  | FP eb1 sb1 -> Bool
forall a. RealFloat a => a -> Bool
fpIsPositiveInfinite FP eb1 sb1
f = Term (FP eb sb) -> Maybe (Term (FP eb sb))
forall a. a -> Maybe a
Just (Term (FP eb sb) -> Maybe (Term (FP eb sb)))
-> Term (FP eb sb) -> Maybe (Term (FP eb sb))
forall a b. (a -> b) -> a -> b
$ FP eb sb -> Term (FP eb sb)
forall t. SupportedPrim t => t -> Term t
conTerm FP eb sb
forall a. IEEEFPConstants a => a
fpPositiveInfinite
  | FP eb1 sb1 -> Bool
forall a. RealFloat a => a -> Bool
fpIsNegativeInfinite FP eb1 sb1
f = Term (FP eb sb) -> Maybe (Term (FP eb sb))
forall a. a -> Maybe a
Just (Term (FP eb sb) -> Maybe (Term (FP eb sb)))
-> Term (FP eb sb) -> Maybe (Term (FP eb sb))
forall a b. (a -> b) -> a -> b
$ FP eb sb -> Term (FP eb sb)
forall t. SupportedPrim t => t -> Term t
conTerm FP eb sb
forall a. IEEEFPConstants a => a
fpNegativeInfinite
  | FP eb1 sb1 -> Bool
forall a. RealFloat a => a -> Bool
fpIsPositiveZero FP eb1 sb1
f = Term (FP eb sb) -> Maybe (Term (FP eb sb))
forall a. a -> Maybe a
Just (Term (FP eb sb) -> Maybe (Term (FP eb sb)))
-> Term (FP eb sb) -> Maybe (Term (FP eb sb))
forall a b. (a -> b) -> a -> b
$ FP eb sb -> Term (FP eb sb)
forall t. SupportedPrim t => t -> Term t
conTerm FP eb sb
forall a. IEEEFPConstants a => a
fpPositiveZero
  | FP eb1 sb1 -> Bool
forall a. RealFloat a => a -> Bool
fpIsNegativeZero FP eb1 sb1
f = Term (FP eb sb) -> Maybe (Term (FP eb sb))
forall a. a -> Maybe a
Just (Term (FP eb sb) -> Maybe (Term (FP eb sb)))
-> Term (FP eb sb) -> Maybe (Term (FP eb sb))
forall a b. (a -> b) -> a -> b
$ FP eb sb -> Term (FP eb sb)
forall t. SupportedPrim t => t -> Term t
conTerm FP eb sb
forall a. IEEEFPConstants a => a
fpNegativeZero
fpDoPevalToFPTerm Term FPRoundingMode
_ Term (FP eb1 sb1)
_ = Maybe (Term (FP eb sb))
forall a. Maybe a
Nothing

fpPevalToFPTerm ::
  ( ValidFP eb sb,
    ValidFP eb1 sb1,
    IEEEFPConvertible (FP eb1 sb1) (FP eb sb) FPRoundingMode
  ) =>
  Term FPRoundingMode ->
  Term (FP eb1 sb1) ->
  Term (FP eb sb)
fpPevalToFPTerm :: forall (eb :: Nat) (sb :: Nat) (eb1 :: Nat) (sb1 :: Nat).
(ValidFP eb sb, ValidFP eb1 sb1,
 IEEEFPConvertible (FP eb1 sb1) (FP eb sb) FPRoundingMode) =>
Term FPRoundingMode -> Term (FP eb1 sb1) -> Term (FP eb sb)
fpPevalToFPTerm = PartialRuleBinary FPRoundingMode (FP eb1 sb1) (FP eb sb)
-> TotalRuleBinary FPRoundingMode (FP eb1 sb1) (FP eb sb)
-> TotalRuleBinary FPRoundingMode (FP eb1 sb1) (FP eb sb)
forall a b c.
SupportedPrim c =>
PartialRuleBinary a b c
-> TotalRuleBinary a b c -> TotalRuleBinary a b c
binaryUnfoldOnce PartialRuleBinary FPRoundingMode (FP eb1 sb1) (FP eb sb)
forall (eb :: Nat) (sb :: Nat) (eb1 :: Nat) (sb1 :: Nat).
(ValidFP eb sb, ValidFP eb1 sb1,
 IEEEFPConvertible (FP eb1 sb1) (FP eb sb) FPRoundingMode) =>
Term FPRoundingMode -> Term (FP eb1 sb1) -> Maybe (Term (FP eb sb))
fpDoPevalToFPTerm TotalRuleBinary FPRoundingMode (FP eb1 sb1) (FP eb sb)
forall a (eb :: Nat) (sb :: Nat).
(PEvalIEEEFPConvertibleTerm a, ValidFP eb sb,
 SupportedPrim (FP eb sb)) =>
Term FPRoundingMode -> Term a -> Term (FP eb sb)
toFPTerm

instance PEvalIEEEFPConvertibleTerm Integer where
  pevalFromFPOrTerm :: forall (eb :: Nat) (sb :: Nat).
ValidFP eb sb =>
Term Integer
-> Term FPRoundingMode -> Term (FP eb sb) -> Term Integer
pevalFromFPOrTerm = Term Integer
-> Term FPRoundingMode -> Term (FP eb sb) -> Term Integer
forall a (eb :: Nat) (sb :: Nat).
(PEvalIEEEFPConvertibleTerm a, ValidFP eb sb, SupportedPrim a,
 IEEEFPConvertible a (FP eb sb) FPRoundingMode) =>
Term a -> Term FPRoundingMode -> Term (FP eb sb) -> Term a
generalPevalFromFPOrTerm
  pevalToFPTerm :: forall (eb :: Nat) (sb :: Nat).
ValidFP eb sb =>
Term FPRoundingMode -> Term Integer -> Term (FP eb sb)
pevalToFPTerm = Term FPRoundingMode -> Term Integer -> Term (FP eb sb)
forall a (eb :: Nat) (sb :: Nat).
(PEvalIEEEFPConvertibleTerm a, ValidFP eb sb,
 IEEEFPConvertible a (FP eb sb) FPRoundingMode) =>
Term FPRoundingMode -> Term a -> Term (FP eb sb)
generalPevalToFPTerm
  sbvFromFPOrTerm :: forall (eb :: Nat) (sb :: Nat).
ValidFP eb sb =>
SBVType Integer
-> SBVType FPRoundingMode -> SBVType (FP eb sb) -> SBVType Integer
sbvFromFPOrTerm SBVType Integer
d SBVType FPRoundingMode
mode SBVType (FP eb sb)
l =
    SBool -> SBVType Integer -> SBVType Integer -> SBVType Integer
forall a. Mergeable a => SBool -> a -> a -> a
SBV.ite (SBV (FloatingPoint eb sb) -> SBool
forall a. IEEEFloating a => SBV a -> SBool
SBV.fpIsNaN SBV (FloatingPoint eb sb)
SBVType (FP eb sb)
l SBool -> SBool -> SBool
SBV..|| SBV (FloatingPoint eb sb) -> SBool
forall a. IEEEFloating a => SBV a -> SBool
SBV.fpIsInfinite SBV (FloatingPoint eb sb)
SBVType (FP eb sb)
l) SBVType Integer
d (SBVType Integer -> SBVType Integer)
-> SBVType Integer -> SBVType Integer
forall a b. (a -> b) -> a -> b
$
      let r :: SReal
r = SRoundingMode -> SBV (FloatingPoint eb sb) -> SReal
forall (eb :: Nat) (sb :: Nat).
ValidFloat eb sb =>
SRoundingMode -> SFloatingPoint eb sb -> SReal
forall a (eb :: Nat) (sb :: Nat).
(IEEEFloatConvertible a, ValidFloat eb sb) =>
SRoundingMode -> SFloatingPoint eb sb -> SBV a
SBV.fromSFloatingPoint SRoundingMode
SBVType FPRoundingMode
mode SBV (FloatingPoint eb sb)
SBVType (FP eb sb)
l :: SBV.SReal
          ifloor :: SInteger
ifloor = SReal -> SInteger
SBV.sRealToSInteger SReal
r
          diff :: SReal
diff = SReal
r SReal -> SReal -> SReal
forall a. Num a => a -> a -> a
- SInteger -> SReal
forall a b.
(Integral a, HasKind a, Num a, SymVal a, HasKind b, Num b,
 SymVal b) =>
SBV a -> SBV b
SBV.sFromIntegral SInteger
ifloor
       in SBool -> SBVType Integer -> SBVType Integer -> SBVType Integer
forall a. Mergeable a => SBool -> a -> a -> a
SBV.ite (SReal
diff SReal -> SReal -> SBool
forall a. EqSymbolic a => a -> a -> SBool
SBV..== SReal
0) SInteger
SBVType Integer
ifloor
            (SBVType Integer -> SBVType Integer)
-> SBVType Integer -> SBVType Integer
forall a b. (a -> b) -> a -> b
$ SBool -> SBVType Integer -> SBVType Integer -> SBVType Integer
forall a. Mergeable a => SBool -> a -> a -> a
SBV.ite (SRoundingMode
SBVType FPRoundingMode
mode SRoundingMode -> SRoundingMode -> SBool
forall a. EqSymbolic a => a -> a -> SBool
SBV..== SRoundingMode
SBV.sRTN) SInteger
SBVType Integer
ifloor
            (SBVType Integer -> SBVType Integer)
-> SBVType Integer -> SBVType Integer
forall a b. (a -> b) -> a -> b
$ SBool -> SBVType Integer -> SBVType Integer -> SBVType Integer
forall a. Mergeable a => SBool -> a -> a -> a
SBV.ite (SRoundingMode
SBVType FPRoundingMode
mode SRoundingMode -> SRoundingMode -> SBool
forall a. EqSymbolic a => a -> a -> SBool
SBV..== SRoundingMode
SBV.sRTP) (SInteger
ifloor SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SInteger
1)
            (SBVType Integer -> SBVType Integer)
-> SBVType Integer -> SBVType Integer
forall a b. (a -> b) -> a -> b
$ SBool -> SBVType Integer -> SBVType Integer -> SBVType Integer
forall a. Mergeable a => SBool -> a -> a -> a
SBV.ite
              (SRoundingMode
SBVType FPRoundingMode
mode SRoundingMode -> SRoundingMode -> SBool
forall a. EqSymbolic a => a -> a -> SBool
SBV..== SRoundingMode
SBV.sRTZ)
              (SBool -> SInteger -> SInteger -> SInteger
forall a. Mergeable a => SBool -> a -> a -> a
SBV.ite (SInteger
ifloor SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
SBV..< SInteger
0) (SInteger
ifloor SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SInteger
1) SInteger
ifloor)
            (SBVType Integer -> SBVType Integer)
-> SBVType Integer -> SBVType Integer
forall a b. (a -> b) -> a -> b
$ SBool -> SBVType Integer -> SBVType Integer -> SBVType Integer
forall a. Mergeable a => SBool -> a -> a -> a
SBV.ite
              (SReal
diff SReal -> SReal -> SBool
forall a. EqSymbolic a => a -> a -> SBool
SBV..== SReal
0.5)
              ( SBool -> SInteger -> SInteger -> SInteger
forall a. Mergeable a => SBool -> a -> a -> a
SBV.ite
                  (SRoundingMode
SBVType FPRoundingMode
mode SRoundingMode -> SRoundingMode -> SBool
forall a. EqSymbolic a => a -> a -> SBool
SBV..== SRoundingMode
SBV.sRNE)
                  ( SBool -> SInteger -> SInteger -> SInteger
forall a. Mergeable a => SBool -> a -> a -> a
SBV.ite
                      (SInteger -> SInteger -> SInteger
forall a. SDivisible a => a -> a -> a
SBV.sMod SInteger
ifloor SInteger
2 SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
SBV..== SInteger
0)
                      SInteger
ifloor
                      (SInteger
ifloor SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SInteger
1)
                  )
                  (SBool -> SInteger -> SInteger -> SInteger
forall a. Mergeable a => SBool -> a -> a -> a
SBV.ite (SInteger
ifloor SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
SBV..< SInteger
0) SInteger
ifloor (SInteger
ifloor SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SInteger
1))
              )
            (SBVType Integer -> SBVType Integer)
-> SBVType Integer -> SBVType Integer
forall a b. (a -> b) -> a -> b
$ SBool -> SInteger -> SInteger -> SInteger
forall a. Mergeable a => SBool -> a -> a -> a
SBV.ite
              (SReal
diff SReal -> SReal -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
SBV..< SReal
0.5)
              SInteger
ifloor
              (SInteger
ifloor SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SInteger
1)
  sbvToFPTerm :: forall (eb :: Nat) (sb :: Nat).
ValidFP eb sb =>
SBVType FPRoundingMode -> SBVType Integer -> SBVType (FP eb sb)
sbvToFPTerm SBVType FPRoundingMode
mode SBVType Integer
l =
    case SInteger -> Maybe Integer
forall a. SymVal a => SBV a -> Maybe a
SBV.unliteral SInteger
SBVType Integer
l of
      Maybe Integer
Nothing -> SRoundingMode -> SInteger -> SFloatingPoint eb sb
forall (eb :: Nat) (sb :: Nat).
ValidFloat eb sb =>
SRoundingMode -> SInteger -> SFloatingPoint eb sb
forall a (eb :: Nat) (sb :: Nat).
(IEEEFloatConvertible a, ValidFloat eb sb) =>
SRoundingMode -> SBV a -> SFloatingPoint eb sb
SBV.toSFloatingPoint SRoundingMode
SBVType FPRoundingMode
mode SInteger
SBVType Integer
l
      Just Integer
_ ->
        [Char] -> SBVType (FP eb sb)
forall a. HasCallStack => [Char] -> a
error ([Char] -> SBVType (FP eb sb)) -> [Char] -> SBVType (FP eb sb)
forall a b. (a -> b) -> a -> b
$
          [Char]
"SBV's toSFloatingPoint does not regard the rounding mode for "
            [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
"integers. This should never be called. "

instance PEvalIEEEFPConvertibleTerm AlgReal where
  pevalFromFPOrTerm :: forall (eb :: Nat) (sb :: Nat).
ValidFP eb sb =>
Term AlgReal
-> Term FPRoundingMode -> Term (FP eb sb) -> Term AlgReal
pevalFromFPOrTerm = Term AlgReal
-> Term FPRoundingMode -> Term (FP eb sb) -> Term AlgReal
forall (eb :: Nat) (sb :: Nat).
(PEvalIEEEFPConvertibleTerm AlgReal, ValidFP eb sb,
 IEEEFPConvertible AlgReal (FP eb sb) FPRoundingMode) =>
Term AlgReal
-> Term FPRoundingMode -> Term (FP eb sb) -> Term AlgReal
algRealPevalFromFPOrTerm
  pevalToFPTerm :: forall (eb :: Nat) (sb :: Nat).
ValidFP eb sb =>
Term FPRoundingMode -> Term AlgReal -> Term (FP eb sb)
pevalToFPTerm = Term FPRoundingMode -> Term AlgReal -> Term (FP eb sb)
forall a (eb :: Nat) (sb :: Nat).
(PEvalIEEEFPConvertibleTerm a, ValidFP eb sb,
 IEEEFPConvertible a (FP eb sb) FPRoundingMode) =>
Term FPRoundingMode -> Term a -> Term (FP eb sb)
generalPevalToFPTerm
  sbvFromFPOrTerm :: forall (eb :: Nat) (sb :: Nat).
ValidFP eb sb =>
SBVType AlgReal
-> SBVType FPRoundingMode -> SBVType (FP eb sb) -> SBVType AlgReal
sbvFromFPOrTerm SBVType AlgReal
d SBVType FPRoundingMode
mode SBVType (FP eb sb)
l =
    SBool -> SBVType AlgReal -> SBVType AlgReal -> SBVType AlgReal
forall a. Mergeable a => SBool -> a -> a -> a
SBV.ite (SBV (FloatingPoint eb sb) -> SBool
forall a. IEEEFloating a => SBV a -> SBool
SBV.fpIsNaN SBV (FloatingPoint eb sb)
SBVType (FP eb sb)
l SBool -> SBool -> SBool
SBV..|| SBV (FloatingPoint eb sb) -> SBool
forall a. IEEEFloating a => SBV a -> SBool
SBV.fpIsInfinite SBV (FloatingPoint eb sb)
SBVType (FP eb sb)
l) SBVType AlgReal
d (SBVType AlgReal -> SBVType AlgReal)
-> SBVType AlgReal -> SBVType AlgReal
forall a b. (a -> b) -> a -> b
$
      SRoundingMode -> SBV (FloatingPoint eb sb) -> SReal
forall (eb :: Nat) (sb :: Nat).
ValidFloat eb sb =>
SRoundingMode -> SFloatingPoint eb sb -> SReal
forall a (eb :: Nat) (sb :: Nat).
(IEEEFloatConvertible a, ValidFloat eb sb) =>
SRoundingMode -> SFloatingPoint eb sb -> SBV a
SBV.fromSFloatingPoint SRoundingMode
SBVType FPRoundingMode
mode SBV (FloatingPoint eb sb)
SBVType (FP eb sb)
l
  sbvToFPTerm :: forall (eb :: Nat) (sb :: Nat).
ValidFP eb sb =>
SBVType FPRoundingMode -> SBVType AlgReal -> SBVType (FP eb sb)
sbvToFPTerm SBVType FPRoundingMode
rm SBVType AlgReal
l =
    case SReal -> Maybe AlgReal
forall a. SymVal a => SBV a -> Maybe a
SBV.unliteral SReal
SBVType AlgReal
l of
      Maybe AlgReal
Nothing -> SRoundingMode -> SReal -> SFloatingPoint eb sb
forall (eb :: Nat) (sb :: Nat).
ValidFloat eb sb =>
SRoundingMode -> SReal -> SFloatingPoint eb sb
forall a (eb :: Nat) (sb :: Nat).
(IEEEFloatConvertible a, ValidFloat eb sb) =>
SRoundingMode -> SBV a -> SFloatingPoint eb sb
SBV.toSFloatingPoint SRoundingMode
SBVType FPRoundingMode
rm SReal
SBVType AlgReal
l
      Just AlgReal
_ ->
        [Char] -> SBVType (FP eb sb)
forall a. HasCallStack => [Char] -> a
error ([Char] -> SBVType (FP eb sb)) -> [Char] -> SBVType (FP eb sb)
forall a b. (a -> b) -> a -> b
$
          [Char]
"SBV is buggy on converting literal AlgReal to an FP. "
            [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
"This should never be called. "
            [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
"https://github.com/LeventErkok/sbv/pull/718"

instance (KnownNat n, 1 <= n) => PEvalIEEEFPConvertibleTerm (WordN n) where
  pevalFromFPOrTerm :: forall (eb :: Nat) (sb :: Nat).
ValidFP eb sb =>
Term (WordN n)
-> Term FPRoundingMode -> Term (FP eb sb) -> Term (WordN n)
pevalFromFPOrTerm = Term (WordN n)
-> Term FPRoundingMode -> Term (FP eb sb) -> Term (WordN n)
forall a (eb :: Nat) (sb :: Nat).
(PEvalIEEEFPConvertibleTerm a, ValidFP eb sb, SupportedPrim a,
 IEEEFPConvertible a (FP eb sb) FPRoundingMode) =>
Term a -> Term FPRoundingMode -> Term (FP eb sb) -> Term a
generalPevalFromFPOrTerm
  pevalToFPTerm :: forall (eb :: Nat) (sb :: Nat).
ValidFP eb sb =>
Term FPRoundingMode -> Term (WordN n) -> Term (FP eb sb)
pevalToFPTerm = Term FPRoundingMode -> Term (WordN n) -> Term (FP eb sb)
forall a (eb :: Nat) (sb :: Nat).
(PEvalIEEEFPConvertibleTerm a, ValidFP eb sb,
 IEEEFPConvertible a (FP eb sb) FPRoundingMode) =>
Term FPRoundingMode -> Term a -> Term (FP eb sb)
generalPevalToFPTerm
  sbvFromFPOrTerm :: forall (eb :: Nat) (sb :: Nat).
ValidFP eb sb =>
SBVType (WordN n)
-> SBVType FPRoundingMode
-> SBVType (FP eb sb)
-> SBVType (WordN n)
sbvFromFPOrTerm = Proxy n
-> (BVIsNonZero n =>
    SBVType (WordN n)
    -> SBVType FPRoundingMode
    -> SBVType (FP eb sb)
    -> SBVType (WordN n))
-> SBVType (WordN n)
-> SBVType FPRoundingMode
-> SBVType (FP eb sb)
-> SBVType (WordN n)
forall (w :: Nat) r (proxy :: Nat -> *).
(1 <= w) =>
proxy w -> (BVIsNonZero w => r) -> r
bvIsNonZeroFromGEq1 (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @n) ((BVIsNonZero n =>
  SBVType (WordN n)
  -> SBVType FPRoundingMode
  -> SBVType (FP eb sb)
  -> SBVType (WordN n))
 -> SBVType (WordN n)
 -> SBVType FPRoundingMode
 -> SBVType (FP eb sb)
 -> SBVType (WordN n))
-> (BVIsNonZero n =>
    SBVType (WordN n)
    -> SBVType FPRoundingMode
    -> SBVType (FP eb sb)
    -> SBVType (WordN n))
-> SBVType (WordN n)
-> SBVType FPRoundingMode
-> SBVType (FP eb sb)
-> SBVType (WordN n)
forall a b. (a -> b) -> a -> b
$ forall (bv :: Nat -> *) (n :: Nat) (eb :: Nat) (sb :: Nat) r.
(ValidFP eb sb, HasKind r, SymVal r, Bounded r, Num r, Ord r,
 SBV r ~ SBVType (bv n), KnownNat n, 1 <= n, ConvertibleBound bv) =>
SBV r -> SBVType FPRoundingMode -> SBVType (FP eb sb) -> SBV r
boundedSBVFromFPTerm @WordN
  sbvToFPTerm :: forall (eb :: Nat) (sb :: Nat).
ValidFP eb sb =>
SBVType FPRoundingMode -> SBVType (WordN n) -> SBVType (FP eb sb)
sbvToFPTerm SBVType FPRoundingMode
mode SBVType (WordN n)
l = Proxy n
-> (BVIsNonZero n => SBVType (FP eb sb)) -> SBVType (FP eb sb)
forall (w :: Nat) r (proxy :: Nat -> *).
(1 <= w) =>
proxy w -> (BVIsNonZero w => r) -> r
bvIsNonZeroFromGEq1 (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @n) ((BVIsNonZero n => SBVType (FP eb sb)) -> SBVType (FP eb sb))
-> (BVIsNonZero n => SBVType (FP eb sb)) -> SBVType (FP eb sb)
forall a b. (a -> b) -> a -> b
$ SRoundingMode -> SBV (WordN n) -> SBV (FloatingPoint eb sb)
forall a r.
(HasKind a, HasKind r) =>
SRoundingMode -> SBV a -> SBV r
genericFPCast SRoundingMode
SBVType FPRoundingMode
mode SBV (WordN n)
SBVType (WordN n)
l

instance (KnownNat n, 1 <= n) => PEvalIEEEFPConvertibleTerm (IntN n) where
  pevalFromFPOrTerm :: forall (eb :: Nat) (sb :: Nat).
ValidFP eb sb =>
Term (IntN n)
-> Term FPRoundingMode -> Term (FP eb sb) -> Term (IntN n)
pevalFromFPOrTerm = Term (IntN n)
-> Term FPRoundingMode -> Term (FP eb sb) -> Term (IntN n)
forall a (eb :: Nat) (sb :: Nat).
(PEvalIEEEFPConvertibleTerm a, ValidFP eb sb, SupportedPrim a,
 IEEEFPConvertible a (FP eb sb) FPRoundingMode) =>
Term a -> Term FPRoundingMode -> Term (FP eb sb) -> Term a
generalPevalFromFPOrTerm
  pevalToFPTerm :: forall (eb :: Nat) (sb :: Nat).
ValidFP eb sb =>
Term FPRoundingMode -> Term (IntN n) -> Term (FP eb sb)
pevalToFPTerm = Term FPRoundingMode -> Term (IntN n) -> Term (FP eb sb)
forall a (eb :: Nat) (sb :: Nat).
(PEvalIEEEFPConvertibleTerm a, ValidFP eb sb,
 IEEEFPConvertible a (FP eb sb) FPRoundingMode) =>
Term FPRoundingMode -> Term a -> Term (FP eb sb)
generalPevalToFPTerm
  sbvFromFPOrTerm :: forall (eb :: Nat) (sb :: Nat).
ValidFP eb sb =>
SBVType (IntN n)
-> SBVType FPRoundingMode -> SBVType (FP eb sb) -> SBVType (IntN n)
sbvFromFPOrTerm = Proxy n
-> (BVIsNonZero n =>
    SBVType (IntN n)
    -> SBVType FPRoundingMode
    -> SBVType (FP eb sb)
    -> SBVType (IntN n))
-> SBVType (IntN n)
-> SBVType FPRoundingMode
-> SBVType (FP eb sb)
-> SBVType (IntN n)
forall (w :: Nat) r (proxy :: Nat -> *).
(1 <= w) =>
proxy w -> (BVIsNonZero w => r) -> r
bvIsNonZeroFromGEq1 (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @n) ((BVIsNonZero n =>
  SBVType (IntN n)
  -> SBVType FPRoundingMode
  -> SBVType (FP eb sb)
  -> SBVType (IntN n))
 -> SBVType (IntN n)
 -> SBVType FPRoundingMode
 -> SBVType (FP eb sb)
 -> SBVType (IntN n))
-> (BVIsNonZero n =>
    SBVType (IntN n)
    -> SBVType FPRoundingMode
    -> SBVType (FP eb sb)
    -> SBVType (IntN n))
-> SBVType (IntN n)
-> SBVType FPRoundingMode
-> SBVType (FP eb sb)
-> SBVType (IntN n)
forall a b. (a -> b) -> a -> b
$ forall (bv :: Nat -> *) (n :: Nat) (eb :: Nat) (sb :: Nat) r.
(ValidFP eb sb, HasKind r, SymVal r, Bounded r, Num r, Ord r,
 SBV r ~ SBVType (bv n), KnownNat n, 1 <= n, ConvertibleBound bv) =>
SBV r -> SBVType FPRoundingMode -> SBVType (FP eb sb) -> SBV r
boundedSBVFromFPTerm @IntN
  sbvToFPTerm :: forall (eb :: Nat) (sb :: Nat).
ValidFP eb sb =>
SBVType FPRoundingMode -> SBVType (IntN n) -> SBVType (FP eb sb)
sbvToFPTerm SBVType FPRoundingMode
mode SBVType (IntN n)
l = Proxy n
-> (BVIsNonZero n => SBVType (FP eb sb)) -> SBVType (FP eb sb)
forall (w :: Nat) r (proxy :: Nat -> *).
(1 <= w) =>
proxy w -> (BVIsNonZero w => r) -> r
bvIsNonZeroFromGEq1 (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @n) ((BVIsNonZero n => SBVType (FP eb sb)) -> SBVType (FP eb sb))
-> (BVIsNonZero n => SBVType (FP eb sb)) -> SBVType (FP eb sb)
forall a b. (a -> b) -> a -> b
$ SRoundingMode -> SBV (IntN n) -> SBV (FloatingPoint eb sb)
forall a r.
(HasKind a, HasKind r) =>
SRoundingMode -> SBV a -> SBV r
genericFPCast SRoundingMode
SBVType FPRoundingMode
mode SBV (IntN n)
SBVType (IntN n)
l

instance (ValidFP eb sb) => PEvalIEEEFPConvertibleTerm (FP eb sb) where
  pevalFromFPOrTerm :: forall (eb :: Nat) (sb :: Nat).
ValidFP eb sb =>
Term (FP eb sb)
-> Term FPRoundingMode -> Term (FP eb sb) -> Term (FP eb sb)
pevalFromFPOrTerm Term (FP eb sb)
_ = Term FPRoundingMode -> Term (FP eb sb) -> Term (FP eb sb)
forall (eb :: Nat) (sb :: Nat) (eb1 :: Nat) (sb1 :: Nat).
(ValidFP eb sb, ValidFP eb1 sb1,
 IEEEFPConvertible (FP eb1 sb1) (FP eb sb) FPRoundingMode) =>
Term FPRoundingMode -> Term (FP eb1 sb1) -> Term (FP eb sb)
fpPevalToFPTerm
  pevalToFPTerm :: forall (eb :: Nat) (sb :: Nat).
ValidFP eb sb =>
Term FPRoundingMode -> Term (FP eb sb) -> Term (FP eb sb)
pevalToFPTerm = Term FPRoundingMode -> Term (FP eb sb) -> Term (FP eb sb)
forall (eb :: Nat) (sb :: Nat) (eb1 :: Nat) (sb1 :: Nat).
(ValidFP eb sb, ValidFP eb1 sb1,
 IEEEFPConvertible (FP eb1 sb1) (FP eb sb) FPRoundingMode) =>
Term FPRoundingMode -> Term (FP eb1 sb1) -> Term (FP eb sb)
fpPevalToFPTerm
  sbvFromFPOrTerm :: forall (eb :: Nat) (sb :: Nat).
ValidFP eb sb =>
SBVType (FP eb sb)
-> SBVType FPRoundingMode
-> SBVType (FP eb sb)
-> SBVType (FP eb sb)
sbvFromFPOrTerm SBVType (FP eb sb)
_ SBVType FPRoundingMode
rm SBVType (FP eb sb)
v = case (SRoundingMode -> Maybe RoundingMode
forall a. SymVal a => SBV a -> Maybe a
SBV.unliteral SRoundingMode
SBVType FPRoundingMode
rm, SBV (FloatingPoint eb sb) -> Maybe (FloatingPoint eb sb)
forall a. SymVal a => SBV a -> Maybe a
SBV.unliteral SBV (FloatingPoint eb sb)
SBVType (FP eb sb)
v) of
    (Just RoundingMode
_, Just FloatingPoint eb sb
_) ->
      [Char] -> SBVType (FP eb sb)
forall a. HasCallStack => [Char] -> a
error ([Char] -> SBVType (FP eb sb)) -> [Char] -> SBVType (FP eb sb)
forall a b. (a -> b) -> a -> b
$
        [Char]
"SBV is buggy on converting literal FP to another FP with different "
          [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
"precision. This should never be called. "
          [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
"https://github.com/LeventErkok/sbv/pull/717"
    (Maybe RoundingMode, Maybe (FloatingPoint eb sb))
_ ->
      SBool
-> SBVType (FP eb sb) -> SBVType (FP eb sb) -> SBVType (FP eb sb)
forall a. Mergeable a => SBool -> a -> a -> a
SBV.ite (SBV (FloatingPoint eb sb) -> SBool
forall a. IEEEFloating a => SBV a -> SBool
SBV.fpIsNaN SBV (FloatingPoint eb sb)
SBVType (FP eb sb)
v) (FP eb sb -> SBVType (FP eb sb)
forall t. SupportedPrim t => t -> SBVType t
conSBVTerm (FP eb sb
forall a. IEEEFPConstants a => a
fpNaN :: FP eb sb)) (SBVType (FP eb sb) -> SBVType (FP eb sb))
-> SBVType (FP eb sb) -> SBVType (FP eb sb)
forall a b. (a -> b) -> a -> b
$
        SRoundingMode
-> SBV (FloatingPoint eb sb) -> SBV (FloatingPoint eb sb)
forall (eb :: Nat) (sb :: Nat).
ValidFloat eb sb =>
SRoundingMode -> SBV (FloatingPoint eb sb) -> SFloatingPoint eb sb
forall a (eb :: Nat) (sb :: Nat).
(IEEEFloatConvertible a, ValidFloat eb sb) =>
SRoundingMode -> SBV a -> SFloatingPoint eb sb
SBV.toSFloatingPoint SRoundingMode
SBVType FPRoundingMode
rm SBV (FloatingPoint eb sb)
SBVType (FP eb sb)
v
  sbvToFPTerm ::
    forall eb1 sb1.
    (ValidFP eb sb, ValidFP eb1 sb1) =>
    SBVType FPRoundingMode ->
    SBVType (FP eb sb) ->
    SBVType (FP eb1 sb1)
  sbvToFPTerm :: forall (eb1 :: Nat) (sb1 :: Nat).
(ValidFP eb sb, ValidFP eb1 sb1) =>
SBVType FPRoundingMode
-> SBVType (FP eb sb) -> SBVType (FP eb1 sb1)
sbvToFPTerm SBVType FPRoundingMode
rm SBVType (FP eb sb)
v = case (SRoundingMode -> Maybe RoundingMode
forall a. SymVal a => SBV a -> Maybe a
SBV.unliteral SRoundingMode
SBVType FPRoundingMode
rm, SBV (FloatingPoint eb sb) -> Maybe (FloatingPoint eb sb)
forall a. SymVal a => SBV a -> Maybe a
SBV.unliteral SBV (FloatingPoint eb sb)
SBVType (FP eb sb)
v) of
    (Just RoundingMode
_, Just FloatingPoint eb sb
_) ->
      [Char] -> SBVType (FP eb1 sb1)
forall a. HasCallStack => [Char] -> a
error ([Char] -> SBVType (FP eb1 sb1)) -> [Char] -> SBVType (FP eb1 sb1)
forall a b. (a -> b) -> a -> b
$
        [Char]
"SBV is buggy on converting literal FP to another FP with different "
          [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
"precision. This should never be called. "
          [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
"https://github.com/LeventErkok/sbv/pull/717"
    (Maybe RoundingMode, Maybe (FloatingPoint eb sb))
_ ->
      SBool
-> SBVType (FP eb1 sb1)
-> SBVType (FP eb1 sb1)
-> SBVType (FP eb1 sb1)
forall a. Mergeable a => SBool -> a -> a -> a
SBV.ite (SBV (FloatingPoint eb sb) -> SBool
forall a. IEEEFloating a => SBV a -> SBool
SBV.fpIsNaN SBV (FloatingPoint eb sb)
SBVType (FP eb sb)
v) (FP eb1 sb1 -> SBVType (FP eb1 sb1)
forall t. SupportedPrim t => t -> SBVType t
conSBVTerm (FP eb1 sb1
forall a. IEEEFPConstants a => a
fpNaN :: FP eb1 sb1)) (SBVType (FP eb1 sb1) -> SBVType (FP eb1 sb1))
-> SBVType (FP eb1 sb1) -> SBVType (FP eb1 sb1)
forall a b. (a -> b) -> a -> b
$
        SRoundingMode
-> SBV (FloatingPoint eb sb) -> SBV (FloatingPoint eb1 sb1)
forall (eb :: Nat) (sb :: Nat).
ValidFloat eb sb =>
SRoundingMode -> SBV (FloatingPoint eb sb) -> SFloatingPoint eb sb
forall a (eb :: Nat) (sb :: Nat).
(IEEEFloatConvertible a, ValidFloat eb sb) =>
SRoundingMode -> SBV a -> SFloatingPoint eb sb
SBV.toSFloatingPoint SRoundingMode
SBVType FPRoundingMode
rm SBV (FloatingPoint eb sb)
SBVType (FP eb sb)
v