    {-# Language DataKinds #-}
    {-# Language FlexibleContexts #-}
    {-# Language GADTs #-}
    {-# Language RankNTypes #-}
    {-# Language TypeApplications #-}
    {-# Language TypeOperators #-}

    -- | Working with floats of dynamic sizes.
    module What4.SFloat
      ( -- * Interface
        SFloat(..)
      , fpReprOf
      , fpSize
      , fpRepr
      , fpAsLit
      , fpIte

        -- * Constants
      , fpFresh
      , fpNaN
      , fpPosInf
      , fpNegInf
      , fpFromLit
      , fpFromRationalLit

        -- * Interchange formats
      , fpFromBinary
      , fpToBinary

        -- * Relations
      , SFloatRel
      , fpEq
      , fpEqIEEE
      , fpLtIEEE
      , fpGtIEEE

        -- * Arithmetic
      , SFloatBinArith
      , fpNeg
      , fpAbs
      , fpSqrt
      , fpAdd
      , fpSub
      , fpMul
      , fpDiv
      , fpMin
      , fpMax
      , fpFMA

        -- * Conversions
      , fpRound
      , fpToReal
      , fpFromReal
      , fpFromRational
      , fpToRational
      , fpFromInteger

        -- * Queries
      , fpIsInf
      , fpIsNaN
      , fpIsZero
      , fpIsNeg
      , fpIsSubnorm
      , fpIsNorm

      -- * Exceptions
      , UnsupportedFloat(..)
      , FPTypeError(..)
      ) where

    import Control.Exception
    import LibBF (BigFloat)

    import Data.Parameterized.Some
    import Data.Parameterized.NatRepr

    import What4.BaseTypes
    import What4.Panic(panic)
    import What4.SWord
    import What4.Interface

    -- | Symbolic floating point numbers.
    data SFloat sym where
      SFloat :: IsExpr (SymExpr sym) => SymFloat sym fpp -> SFloat sym

    --------------------------------------------------------------------------------

    -- | This exception is thrown if the operations try to create a
    -- floating point value we do not support
    data UnsupportedFloat =
      UnsupportedFloat { UnsupportedFloat -> String
    fpWho :: String, UnsupportedFloat -> Integer
    exponentBits, UnsupportedFloat -> Integer
    precisionBits :: Integer }
      deriving Int -> UnsupportedFloat -> ShowS
    [UnsupportedFloat] -> ShowS
    UnsupportedFloat -> String
    (Int -> UnsupportedFloat -> ShowS)
    -> (UnsupportedFloat -> String)
    -> ([UnsupportedFloat] -> ShowS)
    -> Show UnsupportedFloat
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: Int -> UnsupportedFloat -> ShowS
    showsPrec :: Int -> UnsupportedFloat -> ShowS
    $cshow :: UnsupportedFloat -> String
    show :: UnsupportedFloat -> String
    $cshowList :: [UnsupportedFloat] -> ShowS
    showList :: [UnsupportedFloat] -> ShowS
    Show

    -- | Throw 'UnsupportedFloat' exception
    unsupported ::
      String  {- ^ Label -} ->
      Integer {- ^ Exponent width -} ->
      Integer {- ^ Precision width -} ->
      IO a
    unsupported :: forall a. String -> Integer -> Integer -> IO a
    unsupported String
    l Integer
    e Integer
    p =
      UnsupportedFloat -> IO a
    forall e a. Exception e => e -> IO a
    throwIO UnsupportedFloat { fpWho :: String
    fpWho         = String
    l
                               , exponentBits :: Integer
    exponentBits  = Integer
    e
                               , precisionBits :: Integer
    precisionBits = Integer
    p }

    instance Exception UnsupportedFloat

    -- | This exceptoin is throws if the types don't match.
    data FPTypeError =
      FPTypeError { FPTypeError -> Some BaseTypeRepr
    fpExpected :: Some BaseTypeRepr
                  , FPTypeError -> Some BaseTypeRepr
    fpActual   :: Some BaseTypeRepr
                  }
        deriving Int -> FPTypeError -> ShowS
    [FPTypeError] -> ShowS
    FPTypeError -> String
    (Int -> FPTypeError -> ShowS)
    -> (FPTypeError -> String)
    -> ([FPTypeError] -> ShowS)
    -> Show FPTypeError
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: Int -> FPTypeError -> ShowS
    showsPrec :: Int -> FPTypeError -> ShowS
    $cshow :: FPTypeError -> String
    show :: FPTypeError -> String
    $cshowList :: [FPTypeError] -> ShowS
    showList :: [FPTypeError] -> ShowS
    Show

    instance Exception FPTypeError

    fpTypeMismatch :: BaseTypeRepr t1 -> BaseTypeRepr t2 -> IO a
    fpTypeMismatch :: forall (t1 :: BaseType) (t2 :: BaseType) a.
    BaseTypeRepr t1 -> BaseTypeRepr t2 -> IO a
    fpTypeMismatch BaseTypeRepr t1
    expect BaseTypeRepr t2
    actual =
      FPTypeError -> IO a
    forall e a. Exception e => e -> IO a
    throwIO FPTypeError { fpExpected :: Some BaseTypeRepr
    fpExpected = BaseTypeRepr t1 -> Some BaseTypeRepr
    forall k (f :: k -> Type) (x :: k). f x -> Some f
    Some BaseTypeRepr t1
    expect
                          , fpActual :: Some BaseTypeRepr
    fpActual   = BaseTypeRepr t2 -> Some BaseTypeRepr
    forall k (f :: k -> Type) (x :: k). f x -> Some f
    Some BaseTypeRepr t2
    actual
                          }
    fpTypeError :: FloatPrecisionRepr t1 -> FloatPrecisionRepr t2 -> IO a
    fpTypeError :: forall (t1 :: FloatPrecision) (t2 :: FloatPrecision) a.
    FloatPrecisionRepr t1 -> FloatPrecisionRepr t2 -> IO a
    fpTypeError FloatPrecisionRepr t1
    t1 FloatPrecisionRepr t2
    t2 =
      BaseTypeRepr ('BaseFloatType t1)
    -> BaseTypeRepr ('BaseFloatType t2) -> IO a
    forall (t1 :: BaseType) (t2 :: BaseType) a.
    BaseTypeRepr t1 -> BaseTypeRepr t2 -> IO a
    fpTypeMismatch (FloatPrecisionRepr t1 -> BaseTypeRepr ('BaseFloatType t1)
    forall (fpp :: FloatPrecision).
    FloatPrecisionRepr fpp -> BaseTypeRepr ('BaseFloatType fpp)
    BaseFloatRepr FloatPrecisionRepr t1
    t1) (FloatPrecisionRepr t2 -> BaseTypeRepr ('BaseFloatType t2)
    forall (fpp :: FloatPrecision).
    FloatPrecisionRepr fpp -> BaseTypeRepr ('BaseFloatType fpp)
    BaseFloatRepr FloatPrecisionRepr t2
    t2)

    --------------------------------------------------------------------------------
    -- | Construct the 'FloatPrecisionRepr' with the given parameters.
    fpRepr ::
      Integer {- ^ Exponent width -} ->
      Integer {- ^ Precision width -} ->
      Maybe (Some FloatPrecisionRepr)
    fpRepr :: Integer -> Integer -> Maybe (Some FloatPrecisionRepr)
    fpRepr Integer
    iE Integer
    iP =
      do Some NatRepr x
    e    <- Integer -> Maybe (Some NatRepr)
    forall a. Integral a => a -> Maybe (Some NatRepr)
    someNat Integer
    iE
         LeqProof 2 x
    LeqProof  <- NatRepr 2 -> NatRepr x -> Maybe (LeqProof 2 x)
    forall (m :: Nat) (n :: Nat).
    NatRepr m -> NatRepr n -> Maybe (LeqProof m n)
    testLeq (forall (n :: Nat). KnownNat n => NatRepr n
    knownNat @2) NatRepr x
    e
         Some NatRepr x
    p    <- Integer -> Maybe (Some NatRepr)
    forall a. Integral a => a -> Maybe (Some NatRepr)
    someNat Integer
    iP
         LeqProof 2 x
    LeqProof  <- NatRepr 2 -> NatRepr x -> Maybe (LeqProof 2 x)
    forall (m :: Nat) (n :: Nat).
    NatRepr m -> NatRepr n -> Maybe (LeqProof m n)
    testLeq (forall (n :: Nat). KnownNat n => NatRepr n
    knownNat @2) NatRepr x
    p
         Some FloatPrecisionRepr -> Maybe (Some FloatPrecisionRepr)
    forall a. a -> Maybe a
    forall (f :: Type -> Type) a. Applicative f => a -> f a
    pure (FloatPrecisionRepr ('FloatingPointPrecision x x)
    -> Some FloatPrecisionRepr
    forall k (f :: k -> Type) (x :: k). f x -> Some f
    Some (NatRepr x
    -> NatRepr x -> FloatPrecisionRepr ('FloatingPointPrecision x x)
    forall (eb :: Nat) (sb :: Nat).
    (2 <= eb, 2 <= sb) =>
    NatRepr eb
    -> NatRepr sb -> FloatPrecisionRepr ('FloatingPointPrecision eb sb)
    FloatingPointPrecisionRepr NatRepr x
    e NatRepr x
    p))

    fpReprOf ::
      IsExpr (SymExpr sym) => sym -> SymFloat sym fpp -> FloatPrecisionRepr fpp
    fpReprOf :: forall sym (fpp :: FloatPrecision).
    IsExpr (SymExpr sym) =>
    sym -> SymFloat sym fpp -> FloatPrecisionRepr fpp
    fpReprOf sym
    _ SymFloat sym fpp
    e =
      case SymFloat sym fpp -> BaseTypeRepr (BaseFloatType fpp)
    forall (tp :: BaseType). SymExpr sym tp -> BaseTypeRepr tp
    forall (e :: BaseType -> Type) (tp :: BaseType).
    IsExpr e =>
    e tp -> BaseTypeRepr tp
    exprType SymFloat sym fpp
    e of
        BaseFloatRepr FloatPrecisionRepr fpp
    r -> FloatPrecisionRepr fpp
    FloatPrecisionRepr fpp
    r

    fpSize :: SFloat sym -> (Integer,Integer)
    fpSize :: forall sym. SFloat sym -> (Integer, Integer)
    fpSize (SFloat SymFloat sym fpp
    f) =
      case SymFloat sym fpp -> BaseTypeRepr (BaseFloatType fpp)
    forall (tp :: BaseType). SymExpr sym tp -> BaseTypeRepr tp
    forall (e :: BaseType -> Type) (tp :: BaseType).
    IsExpr e =>
    e tp -> BaseTypeRepr tp
    exprType SymFloat sym fpp
    f of
        BaseFloatRepr (FloatingPointPrecisionRepr NatRepr eb
    e NatRepr sb
    p) -> (NatRepr eb -> Integer
    forall (n :: Nat). NatRepr n -> Integer
    intValue NatRepr eb
    e, NatRepr sb -> Integer
    forall (n :: Nat). NatRepr n -> Integer
    intValue NatRepr sb
    p)

    fpAsLit :: SFloat sym -> Maybe BigFloat
    fpAsLit :: forall sym. SFloat sym -> Maybe BigFloat
    fpAsLit (SFloat SymFloat sym fpp
    f) = SymFloat sym fpp -> Maybe BigFloat
    forall (fpp :: FloatPrecision).
    SymExpr sym (BaseFloatType fpp) -> Maybe BigFloat
    forall (e :: BaseType -> Type) (fpp :: FloatPrecision).
    IsExpr e =>
    e (BaseFloatType fpp) -> Maybe BigFloat
    asFloat SymFloat sym fpp
    f

    --------------------------------------------------------------------------------
    -- Constants

    -- | A fresh variable of the given type.
    fpFresh ::
      IsSymExprBuilder sym =>
      sym ->
      Integer ->
      Integer ->
      IO (SFloat sym)
    fpFresh :: forall sym.
    IsSymExprBuilder sym =>
    sym -> Integer -> Integer -> IO (SFloat sym)
    fpFresh sym
    sym Integer
    e Integer
    p
      | Just (Some FloatPrecisionRepr x
    fpp) <- Integer -> Integer -> Maybe (Some FloatPrecisionRepr)
    fpRepr Integer
    e Integer
    p =
        SymFloat sym x -> SFloat sym
    forall sym (fpp :: FloatPrecision).
    IsExpr (SymExpr sym) =>
    SymFloat sym fpp -> SFloat sym
    SFloat (SymFloat sym x -> SFloat sym)
    -> IO (SymFloat sym x) -> IO (SFloat sym)
    forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
    <$> sym
    -> SolverSymbol
    -> BaseTypeRepr ('BaseFloatType x)
    -> IO (SymFloat sym x)
    forall sym (tp :: BaseType).
    IsSymExprBuilder sym =>
    sym -> SolverSymbol -> BaseTypeRepr tp -> IO (SymExpr sym tp)
    forall (tp :: BaseType).
    sym -> SolverSymbol -> BaseTypeRepr tp -> IO (SymExpr sym tp)
    freshConstant sym
    sym SolverSymbol
    emptySymbol (FloatPrecisionRepr x -> BaseTypeRepr ('BaseFloatType x)
    forall (fpp :: FloatPrecision).
    FloatPrecisionRepr fpp -> BaseTypeRepr ('BaseFloatType fpp)
    BaseFloatRepr FloatPrecisionRepr x
    fpp)
      | Bool
    otherwise = String -> Integer -> Integer -> IO (SFloat sym)
    forall a. String -> Integer -> Integer -> IO a
    unsupported String
    "fpFresh" Integer
    e Integer
    p

    -- | Not a number
    fpNaN ::
      IsExprBuilder sym =>
      sym ->
      Integer {- ^ Exponent width -} ->
      Integer {- ^ Precision width -} ->
      IO (SFloat sym)
    fpNaN :: forall sym.
    IsExprBuilder sym =>
    sym -> Integer -> Integer -> IO (SFloat sym)
    fpNaN sym
    sym Integer
    e Integer
    p
      | Just (Some FloatPrecisionRepr x
    fpp) <- Integer -> Integer -> Maybe (Some FloatPrecisionRepr)
    fpRepr Integer
    e Integer
    p = SymFloat sym x -> SFloat sym
    forall sym (fpp :: FloatPrecision).
    IsExpr (SymExpr sym) =>
    SymFloat sym fpp -> SFloat sym
    SFloat (SymFloat sym x -> SFloat sym)
    -> IO (SymFloat sym x) -> IO (SFloat sym)
    forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
    <$> sym -> FloatPrecisionRepr x -> IO (SymFloat sym x)
    forall sym (fpp :: FloatPrecision).
    IsExprBuilder sym =>
    sym -> FloatPrecisionRepr fpp -> IO (SymFloat sym fpp)
    forall (fpp :: FloatPrecision).
    sym -> FloatPrecisionRepr fpp -> IO (SymFloat sym fpp)
    floatNaN sym
    sym FloatPrecisionRepr x
    fpp
      | Bool
    otherwise = String -> Integer -> Integer -> IO (SFloat sym)
    forall a. String -> Integer -> Integer -> IO a
    unsupported String
    "fpNaN" Integer
    e Integer
    p

    -- | Positive infinity
    fpPosInf ::
      IsExprBuilder sym =>
      sym ->
      Integer {- ^ Exponent width -} ->
      Integer {- ^ Precision width -} ->
      IO (SFloat sym)
    fpPosInf :: forall sym.
    IsExprBuilder sym =>
    sym -> Integer -> Integer -> IO (SFloat sym)
    fpPosInf sym
    sym Integer
    e Integer
    p
      | Just (Some FloatPrecisionRepr x
    fpp) <- Integer -> Integer -> Maybe (Some FloatPrecisionRepr)
    fpRepr Integer
    e Integer
    p = SymFloat sym x -> SFloat sym
    forall sym (fpp :: FloatPrecision).
    IsExpr (SymExpr sym) =>
    SymFloat sym fpp -> SFloat sym
    SFloat (SymFloat sym x -> SFloat sym)
    -> IO (SymFloat sym x) -> IO (SFloat sym)
    forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
    <$> sym -> FloatPrecisionRepr x -> IO (SymFloat sym x)
    forall sym (fpp :: FloatPrecision).
    IsExprBuilder sym =>
    sym -> FloatPrecisionRepr fpp -> IO (SymFloat sym fpp)
    forall (fpp :: FloatPrecision).
    sym -> FloatPrecisionRepr fpp -> IO (SymFloat sym fpp)
    floatPInf sym
    sym FloatPrecisionRepr x
    fpp
      | Bool
    otherwise = String -> Integer -> Integer -> IO (SFloat sym)
    forall a. String -> Integer -> Integer -> IO a
    unsupported String
    "fpPosInf" Integer
    e Integer
    p

    -- | Negative infinity
    fpNegInf ::
      IsExprBuilder sym =>
      sym ->
      Integer {- ^ Exponent width -} ->
      Integer {- ^ Precision width -} ->
      IO (SFloat sym)
    fpNegInf :: forall sym.
    IsExprBuilder sym =>
    sym -> Integer -> Integer -> IO (SFloat sym)
    fpNegInf sym
    sym Integer
    e Integer
    p
      | Just (Some FloatPrecisionRepr x
    fpp) <- Integer -> Integer -> Maybe (Some FloatPrecisionRepr)
    fpRepr Integer
    e Integer
    p = SymFloat sym x -> SFloat sym
    forall sym (fpp :: FloatPrecision).
    IsExpr (SymExpr sym) =>
    SymFloat sym fpp -> SFloat sym
    SFloat (SymFloat sym x -> SFloat sym)
    -> IO (SymFloat sym x) -> IO (SFloat sym)
    forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
    <$> sym -> FloatPrecisionRepr x -> IO (SymFloat sym x)
    forall sym (fpp :: FloatPrecision).
    IsExprBuilder sym =>
    sym -> FloatPrecisionRepr fpp -> IO (SymFloat sym fpp)
    forall (fpp :: FloatPrecision).
    sym -> FloatPrecisionRepr fpp -> IO (SymFloat sym fpp)
    floatNInf sym
    sym FloatPrecisionRepr x
    fpp
      | Bool
    otherwise = String -> Integer -> Integer -> IO (SFloat sym)
    forall a. String -> Integer -> Integer -> IO a
    unsupported String
    "fpNegInf" Integer
    e Integer
    p

    -- | A floating point number corresponding to the given BigFloat.
    fpFromLit ::
      IsExprBuilder sym =>
      sym ->
      Integer {- ^ Exponent width -} ->
      Integer {- ^ Precision width -} ->
      BigFloat ->
      IO (SFloat sym)
    fpFromLit :: forall sym.
    IsExprBuilder sym =>
    sym -> Integer -> Integer -> BigFloat -> IO (SFloat sym)
    fpFromLit sym
    sym Integer
    e Integer
    p BigFloat
    f
      | Just (Some FloatPrecisionRepr x
    fpp) <- Integer -> Integer -> Maybe (Some FloatPrecisionRepr)
    fpRepr Integer
    e Integer
    p = SymFloat sym x -> SFloat sym
    forall sym (fpp :: FloatPrecision).
    IsExpr (SymExpr sym) =>
    SymFloat sym fpp -> SFloat sym
    SFloat (SymFloat sym x -> SFloat sym)
    -> IO (SymFloat sym x) -> IO (SFloat sym)
    forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
    <$> sym -> FloatPrecisionRepr x -> BigFloat -> IO (SymFloat sym x)
    forall sym (fpp :: FloatPrecision).
    IsExprBuilder sym =>
    sym -> FloatPrecisionRepr fpp -> BigFloat -> IO (SymFloat sym fpp)
    forall (fpp :: FloatPrecision).
    sym -> FloatPrecisionRepr fpp -> BigFloat -> IO (SymFloat sym fpp)
    floatLit sym
    sym FloatPrecisionRepr x
    fpp BigFloat
    f
      | Bool
    otherwise = String -> Integer -> Integer -> IO (SFloat sym)
    forall a. String -> Integer -> Integer -> IO a
    unsupported String
    "fpFromLit" Integer
    e Integer
    p

    -- | A floating point number corresponding to the given rational.
    fpFromRationalLit ::
      IsExprBuilder sym =>
      sym ->
      Integer {- ^ Exponent width -} ->
      Integer {- ^ Precision width -} ->
      Rational ->
      IO (SFloat sym)
    fpFromRationalLit :: forall sym.
    IsExprBuilder sym =>
    sym -> Integer -> Integer -> Rational -> IO (SFloat sym)
    fpFromRationalLit sym
    sym Integer
    e Integer
    p Rational
    r
      | Just (Some FloatPrecisionRepr x
    fpp) <- Integer -> Integer -> Maybe (Some FloatPrecisionRepr)
    fpRepr Integer
    e Integer
    p = SymFloat sym x -> SFloat sym
    forall sym (fpp :: FloatPrecision).
    IsExpr (SymExpr sym) =>
    SymFloat sym fpp -> SFloat sym
    SFloat (SymFloat sym x -> SFloat sym)
    -> IO (SymFloat sym x) -> IO (SFloat sym)
    forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
    <$> sym -> FloatPrecisionRepr x -> Rational -> IO (SymFloat sym x)
    forall sym (fpp :: FloatPrecision).
    IsExprBuilder sym =>
    sym -> FloatPrecisionRepr fpp -> Rational -> IO (SymFloat sym fpp)
    forall (fpp :: FloatPrecision).
    sym -> FloatPrecisionRepr fpp -> Rational -> IO (SymFloat sym fpp)
    floatLitRational sym
    sym FloatPrecisionRepr x
    fpp Rational
    r
      | Bool
    otherwise = String -> Integer -> Integer -> IO (SFloat sym)
    forall a. String -> Integer -> Integer -> IO a
    unsupported String
    "fpFromRationalLit" Integer
    e Integer
    p

    -- | Make a floating point number with the given bit representation.
    fpFromBinary ::
      IsExprBuilder sym =>
      sym ->
      Integer {- ^ Exponent width -} ->
      Integer {- ^ Precision width -} ->
      SWord sym ->
      IO (SFloat sym)
    fpFromBinary :: forall sym.
    IsExprBuilder sym =>
    sym -> Integer -> Integer -> SWord sym -> IO (SFloat sym)
    fpFromBinary sym
    sym Integer
    e Integer
    p SWord sym
    swe
      | DBV SymBV sym w
    sw <- SWord sym
    swe
      , Just (Some FloatPrecisionRepr x
    fpp) <- Integer -> Integer -> Maybe (Some FloatPrecisionRepr)
    fpRepr Integer
    e Integer
    p
      , FloatingPointPrecisionRepr NatRepr eb
    ew NatRepr sb
    pw <- FloatPrecisionRepr x
    fpp
      , let expectW :: NatRepr (eb + sb)
    expectW = NatRepr eb -> NatRepr sb -> NatRepr (eb + sb)
    forall (m :: Nat) (n :: Nat).
    NatRepr m -> NatRepr n -> NatRepr (m + n)
    addNat NatRepr eb
    ew NatRepr sb
    pw
      , actual :: BaseTypeRepr (BaseBVType w)
    actual@(BaseBVRepr NatRepr w
    actualW)  <- SymBV sym w -> BaseTypeRepr (BaseBVType w)
    forall (tp :: BaseType). SymExpr sym tp -> BaseTypeRepr tp
    forall (e :: BaseType -> Type) (tp :: BaseType).
    IsExpr e =>
    e tp -> BaseTypeRepr tp
    exprType SymBV sym w
    sw =
        case NatRepr (eb + sb) -> NatRepr w -> Maybe ((eb + sb) :~: w)
    forall (a :: Nat) (b :: Nat).
    NatRepr a -> NatRepr b -> Maybe (a :~: b)
    forall {k} (f :: k -> Type) (a :: k) (b :: k).
    TestEquality f =>
    f a -> f b -> Maybe (a :~: b)
    testEquality NatRepr (eb + sb)
    expectW NatRepr w
    actualW of
          Just (eb + sb) :~: w
    Refl -> SymFloat sym ('FloatingPointPrecision eb sb) -> SFloat sym
    forall sym (fpp :: FloatPrecision).
    IsExpr (SymExpr sym) =>
    SymFloat sym fpp -> SFloat sym
    SFloat (SymFloat sym ('FloatingPointPrecision eb sb) -> SFloat sym)
    -> IO (SymFloat sym ('FloatingPointPrecision eb sb))
    -> IO (SFloat sym)
    forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
    <$> sym
    -> FloatPrecisionRepr ('FloatingPointPrecision eb sb)
    -> SymBV sym (eb + sb)
    -> IO (SymFloat sym ('FloatingPointPrecision eb sb))
    forall (eb :: Nat) (sb :: Nat).
    (2 <= eb, 2 <= sb) =>
    sym
    -> FloatPrecisionRepr (FloatingPointPrecision eb sb)
    -> SymBV sym (eb + sb)
    -> IO (SymFloat sym (FloatingPointPrecision eb sb))
    forall sym (eb :: Nat) (sb :: Nat).
    (IsExprBuilder sym, 2 <= eb, 2 <= sb) =>
    sym
    -> FloatPrecisionRepr (FloatingPointPrecision eb sb)
    -> SymBV sym (eb + sb)
    -> IO (SymFloat sym (FloatingPointPrecision eb sb))
    floatFromBinary sym
    sym FloatPrecisionRepr x
    FloatPrecisionRepr ('FloatingPointPrecision eb sb)
    fpp SymBV sym w
    SymBV sym (eb + sb)
    sw
          Maybe ((eb + sb) :~: w)
    Nothing -- we want to report type correct type errors! :-)
            | Just LeqProof 1 (eb + sb)
    LeqProof <- NatRepr 1 -> NatRepr (eb + sb) -> Maybe (LeqProof 1 (eb + sb))
    forall (m :: Nat) (n :: Nat).
    NatRepr m -> NatRepr n -> Maybe (LeqProof m n)
    testLeq (forall (n :: Nat). KnownNat n => NatRepr n
    knownNat @1) NatRepr (eb + sb)
    expectW ->
                    BaseTypeRepr ('BaseBVType (eb + sb))
    -> BaseTypeRepr (BaseBVType w) -> IO (SFloat sym)
    forall (t1 :: BaseType) (t2 :: BaseType) a.
    BaseTypeRepr t1 -> BaseTypeRepr t2 -> IO a
    fpTypeMismatch (NatRepr (eb + sb) -> BaseTypeRepr ('BaseBVType (eb + sb))
    forall (w :: Nat).
    (1 <= w) =>
    NatRepr w -> BaseTypeRepr ('BaseBVType w)
    BaseBVRepr NatRepr (eb + sb)
    expectW) BaseTypeRepr (BaseBVType w)
    actual
            | Bool
    otherwise -> String -> [String] -> IO (SFloat sym)
    forall a. HasCallStack => String -> [String] -> a
    panic String
    "fpFromBits" [ String
    "1 >= 2" ]
      | Bool
    otherwise = String -> Integer -> Integer -> IO (SFloat sym)
    forall a. String -> Integer -> Integer -> IO a
    unsupported String
    "fpFromBits" Integer
    e Integer
    p

    fpToBinary :: IsExprBuilder sym => sym -> SFloat sym -> IO (SWord sym)
    fpToBinary :: forall sym.
    IsExprBuilder sym =>
    sym -> SFloat sym -> IO (SWord sym)
    fpToBinary sym
    sym (SFloat SymFloat sym fpp
    f)
      | FloatingPointPrecisionRepr NatRepr eb
    e NatRepr sb
    p <- sym -> SymFloat sym fpp -> FloatPrecisionRepr fpp
    forall sym (fpp :: FloatPrecision).
    IsExpr (SymExpr sym) =>
    sym -> SymFloat sym fpp -> FloatPrecisionRepr fpp
    fpReprOf sym
    sym SymFloat sym fpp
    f
      , Just LeqProof 1 (eb + sb)
    LeqProof <- NatRepr 1 -> NatRepr (eb + sb) -> Maybe (LeqProof 1 (eb + sb))
    forall (m :: Nat) (n :: Nat).
    NatRepr m -> NatRepr n -> Maybe (LeqProof m n)
    testLeq (forall (n :: Nat). KnownNat n => NatRepr n
    knownNat @1) (NatRepr eb -> NatRepr sb -> NatRepr (eb + sb)
    forall (m :: Nat) (n :: Nat).
    NatRepr m -> NatRepr n -> NatRepr (m + n)
    addNat NatRepr eb
    e NatRepr sb
    p)
        = SymBV sym (eb + sb) -> SWord sym
    forall sym (w :: Nat).
    (IsExpr (SymExpr sym), 1 <= w) =>
    SymBV sym w -> SWord sym
    DBV (SymBV sym (eb + sb) -> SWord sym)
    -> IO (SymBV sym (eb + sb)) -> IO (SWord sym)
    forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
    <$> sym
    -> SymFloat sym ('FloatingPointPrecision eb sb)
    -> IO (SymBV sym (eb + sb))
    forall (eb :: Nat) (sb :: Nat).
    (2 <= eb, 2 <= sb) =>
    sym
    -> SymFloat sym (FloatingPointPrecision eb sb)
    -> IO (SymBV sym (eb + sb))
    forall sym (eb :: Nat) (sb :: Nat).
    (IsExprBuilder sym, 2 <= eb, 2 <= sb) =>
    sym
    -> SymFloat sym (FloatingPointPrecision eb sb)
    -> IO (SymBV sym (eb + sb))
    floatToBinary sym
    sym SymFloat sym fpp
    SymFloat sym ('FloatingPointPrecision eb sb)
    f
      | Bool
    otherwise = String -> [String] -> IO (SWord sym)
    forall a. HasCallStack => String -> [String] -> a
    panic String
    "fpToBinary" [ String
    "we messed up the types" ]

    --------------------------------------------------------------------------------
    -- Arithmetic

    fpNeg :: IsExprBuilder sym => sym -> SFloat sym -> IO (SFloat sym)
    fpNeg :: forall sym.
    IsExprBuilder sym =>
    sym -> SFloat sym -> IO (SFloat sym)
    fpNeg sym
    sym (SFloat SymFloat sym fpp
    fl) = SymFloat sym fpp -> SFloat sym
    forall sym (fpp :: FloatPrecision).
    IsExpr (SymExpr sym) =>
    SymFloat sym fpp -> SFloat sym
    SFloat (SymFloat sym fpp -> SFloat sym)
    -> IO (SymFloat sym fpp) -> IO (SFloat sym)
    forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
    <$> sym -> SymFloat sym fpp -> IO (SymFloat sym fpp)
    forall sym (fpp :: FloatPrecision).
    IsExprBuilder sym =>
    sym -> SymFloat sym fpp -> IO (SymFloat sym fpp)
    forall (fpp :: FloatPrecision).
    sym -> SymFloat sym fpp -> IO (SymFloat sym fpp)
    floatNeg sym
    sym SymFloat sym fpp
    fl

    fpAbs :: IsExprBuilder sym => sym -> SFloat sym -> IO (SFloat sym)
    fpAbs :: forall sym.
    IsExprBuilder sym =>
    sym -> SFloat sym -> IO (SFloat sym)
    fpAbs sym
    sym (SFloat SymFloat sym fpp
    fl) = SymFloat sym fpp -> SFloat sym
    forall sym (fpp :: FloatPrecision).
    IsExpr (SymExpr sym) =>
    SymFloat sym fpp -> SFloat sym
    SFloat (SymFloat sym fpp -> SFloat sym)
    -> IO (SymFloat sym fpp) -> IO (SFloat sym)
    forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
    <$> sym -> SymFloat sym fpp -> IO (SymFloat sym fpp)
    forall sym (fpp :: FloatPrecision).
    IsExprBuilder sym =>
    sym -> SymFloat sym fpp -> IO (SymFloat sym fpp)
    forall (fpp :: FloatPrecision).
    sym -> SymFloat sym fpp -> IO (SymFloat sym fpp)
    floatAbs sym
    sym SymFloat sym fpp
    fl

    fpSqrt :: IsExprBuilder sym => sym -> RoundingMode -> SFloat sym -> IO (SFloat sym)
    fpSqrt :: forall sym.
    IsExprBuilder sym =>
    sym -> RoundingMode -> SFloat sym -> IO (SFloat sym)
    fpSqrt sym
    sym RoundingMode
    r (SFloat SymFloat sym fpp
    fl) = SymFloat sym fpp -> SFloat sym
    forall sym (fpp :: FloatPrecision).
    IsExpr (SymExpr sym) =>
    SymFloat sym fpp -> SFloat sym
    SFloat (SymFloat sym fpp -> SFloat sym)
    -> IO (SymFloat sym fpp) -> IO (SFloat sym)
    forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
    <$> sym -> RoundingMode -> SymFloat sym fpp -> IO (SymFloat sym fpp)
    forall sym (fpp :: FloatPrecision).
    IsExprBuilder sym =>
    sym -> RoundingMode -> SymFloat sym fpp -> IO (SymFloat sym fpp)
    forall (fpp :: FloatPrecision).
    sym -> RoundingMode -> SymFloat sym fpp -> IO (SymFloat sym fpp)
    floatSqrt sym
    sym RoundingMode
    r SymFloat sym fpp
    fl

    fpBinArith ::
      IsExprBuilder sym =>
      (forall t.
          sym ->
          RoundingMode ->
          SymFloat sym t ->
          SymFloat sym t ->
          IO (SymFloat sym t)
      ) ->
      sym -> RoundingMode -> SFloat sym -> SFloat sym -> IO (SFloat sym)
    fpBinArith :: forall sym.
    IsExprBuilder sym =>
    (forall (t :: FloatPrecision).
     sym
     -> RoundingMode
     -> SymFloat sym t
     -> SymFloat sym t
     -> IO (SymFloat sym t))
    -> sym
    -> RoundingMode
    -> SFloat sym
    -> SFloat sym
    -> IO (SFloat sym)
    fpBinArith forall (t :: FloatPrecision).
    sym
    -> RoundingMode
    -> SymFloat sym t
    -> SymFloat sym t
    -> IO (SymFloat sym t)
    fun sym
    sym RoundingMode
    r (SFloat SymFloat sym fpp
    x) (SFloat SymFloat sym fpp
    y) =
      let t1 :: FloatPrecisionRepr fpp
    t1 = sym
    sym sym -> SymFloat sym fpp -> FloatPrecisionRepr fpp
    forall sym (fpp :: FloatPrecision).
    IsExpr (SymExpr sym) =>
    sym -> SymFloat sym fpp -> FloatPrecisionRepr fpp
    `fpReprOf` SymFloat sym fpp
    x
          t2 :: FloatPrecisionRepr fpp
    t2 = sym
    sym sym -> SymFloat sym fpp -> FloatPrecisionRepr fpp
    forall sym (fpp :: FloatPrecision).
    IsExpr (SymExpr sym) =>
    sym -> SymFloat sym fpp -> FloatPrecisionRepr fpp
    `fpReprOf` SymFloat sym fpp
    y
      in
      case FloatPrecisionRepr fpp
    -> FloatPrecisionRepr fpp -> Maybe (fpp :~: fpp)
    forall {k} (f :: k -> Type) (a :: k) (b :: k).
    TestEquality f =>
    f a -> f b -> Maybe (a :~: b)
    forall (a :: FloatPrecision) (b :: FloatPrecision).
    FloatPrecisionRepr a -> FloatPrecisionRepr b -> Maybe (a :~: b)
    testEquality FloatPrecisionRepr fpp
    t1 FloatPrecisionRepr fpp
    t2 of
        Just fpp :~: fpp
    Refl -> SymFloat sym fpp -> SFloat sym
    forall sym (fpp :: FloatPrecision).
    IsExpr (SymExpr sym) =>
    SymFloat sym fpp -> SFloat sym
    SFloat (SymFloat sym fpp -> SFloat sym)
    -> IO (SymFloat sym fpp) -> IO (SFloat sym)
    forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
    <$> sym
    -> RoundingMode
    -> SymFloat sym fpp
    -> SymFloat sym fpp
    -> IO (SymFloat sym fpp)
    forall (t :: FloatPrecision).
    sym
    -> RoundingMode
    -> SymFloat sym t
    -> SymFloat sym t
    -> IO (SymFloat sym t)
    fun sym
    sym RoundingMode
    r SymFloat sym fpp
    x SymFloat sym fpp
    SymFloat sym fpp
    y
        Maybe (fpp :~: fpp)
    _         -> FloatPrecisionRepr fpp -> FloatPrecisionRepr fpp -> IO (SFloat sym)
    forall (t1 :: FloatPrecision) (t2 :: FloatPrecision) a.
    FloatPrecisionRepr t1 -> FloatPrecisionRepr t2 -> IO a
    fpTypeError FloatPrecisionRepr fpp
    t1 FloatPrecisionRepr fpp
    t2

    type SFloatBinArith sym =
      sym -> RoundingMode -> SFloat sym -> SFloat sym -> IO (SFloat sym)

    fpAdd :: IsExprBuilder sym => SFloatBinArith sym
    fpAdd :: forall sym. IsExprBuilder sym => SFloatBinArith sym
    fpAdd = (forall (t :: FloatPrecision).
     sym
     -> RoundingMode
     -> SymFloat sym t
     -> SymFloat sym t
     -> IO (SymFloat sym t))
    -> sym
    -> RoundingMode
    -> SFloat sym
    -> SFloat sym
    -> IO (SFloat sym)
    forall sym.
    IsExprBuilder sym =>
    (forall (t :: FloatPrecision).
     sym
     -> RoundingMode
     -> SymFloat sym t
     -> SymFloat sym t
     -> IO (SymFloat sym t))
    -> sym
    -> RoundingMode
    -> SFloat sym
    -> SFloat sym
    -> IO (SFloat sym)
    fpBinArith sym
    -> RoundingMode
    -> SymFloat sym t
    -> SymFloat sym t
    -> IO (SymFloat sym t)
    forall sym (fpp :: FloatPrecision).
    IsExprBuilder sym =>
    sym
    -> RoundingMode
    -> SymFloat sym fpp
    -> SymFloat sym fpp
    -> IO (SymFloat sym fpp)
    forall (t :: FloatPrecision).
    sym
    -> RoundingMode
    -> SymFloat sym t
    -> SymFloat sym t
    -> IO (SymFloat sym t)
    floatAdd

    fpSub :: IsExprBuilder sym => SFloatBinArith sym
    fpSub :: forall sym. IsExprBuilder sym => SFloatBinArith sym
    fpSub = (forall (t :: FloatPrecision).
     sym
     -> RoundingMode
     -> SymFloat sym t
     -> SymFloat sym t
     -> IO (SymFloat sym t))
    -> sym
    -> RoundingMode
    -> SFloat sym
    -> SFloat sym
    -> IO (SFloat sym)
    forall sym.
    IsExprBuilder sym =>
    (forall (t :: FloatPrecision).
     sym
     -> RoundingMode
     -> SymFloat sym t
     -> SymFloat sym t
     -> IO (SymFloat sym t))
    -> sym
    -> RoundingMode
    -> SFloat sym
    -> SFloat sym
    -> IO (SFloat sym)
    fpBinArith sym
    -> RoundingMode
    -> SymFloat sym t
    -> SymFloat sym t
    -> IO (SymFloat sym t)
    forall sym (fpp :: FloatPrecision).
    IsExprBuilder sym =>
    sym
    -> RoundingMode
    -> SymFloat sym fpp
    -> SymFloat sym fpp
    -> IO (SymFloat sym fpp)
    forall (t :: FloatPrecision).
    sym
    -> RoundingMode
    -> SymFloat sym t
    -> SymFloat sym t
    -> IO (SymFloat sym t)
    floatSub

    fpMul :: IsExprBuilder sym => SFloatBinArith sym
    fpMul :: forall sym. IsExprBuilder sym => SFloatBinArith sym
    fpMul = (forall (t :: FloatPrecision).
     sym
     -> RoundingMode
     -> SymFloat sym t
     -> SymFloat sym t
     -> IO (SymFloat sym t))
    -> sym
    -> RoundingMode
    -> SFloat sym
    -> SFloat sym
    -> IO (SFloat sym)
    forall sym.
    IsExprBuilder sym =>
    (forall (t :: FloatPrecision).
     sym
     -> RoundingMode
     -> SymFloat sym t
     -> SymFloat sym t
     -> IO (SymFloat sym t))
    -> sym
    -> RoundingMode
    -> SFloat sym
    -> SFloat sym
    -> IO (SFloat sym)
    fpBinArith sym
    -> RoundingMode
    -> SymFloat sym t
    -> SymFloat sym t
    -> IO (SymFloat sym t)
    forall sym (fpp :: FloatPrecision).
    IsExprBuilder sym =>
    sym
    -> RoundingMode
    -> SymFloat sym fpp
    -> SymFloat sym fpp
    -> IO (SymFloat sym fpp)
    forall (t :: FloatPrecision).
    sym
    -> RoundingMode
    -> SymFloat sym t
    -> SymFloat sym t
    -> IO (SymFloat sym t)
    floatMul

    fpDiv :: IsExprBuilder sym => SFloatBinArith sym
    fpDiv :: forall sym. IsExprBuilder sym => SFloatBinArith sym
    fpDiv = (forall (t :: FloatPrecision).
     sym
     -> RoundingMode
     -> SymFloat sym t
     -> SymFloat sym t
     -> IO (SymFloat sym t))
    -> sym
    -> RoundingMode
    -> SFloat sym
    -> SFloat sym
    -> IO (SFloat sym)
    forall sym.
    IsExprBuilder sym =>
    (forall (t :: FloatPrecision).
     sym
     -> RoundingMode
     -> SymFloat sym t
     -> SymFloat sym t
     -> IO (SymFloat sym t))
    -> sym
    -> RoundingMode
    -> SFloat sym
    -> SFloat sym
    -> IO (SFloat sym)
    fpBinArith sym
    -> RoundingMode
    -> SymFloat sym t
    -> SymFloat sym t
    -> IO (SymFloat sym t)
    forall sym (fpp :: FloatPrecision).
    IsExprBuilder sym =>
    sym
    -> RoundingMode
    -> SymFloat sym fpp
    -> SymFloat sym fpp
    -> IO (SymFloat sym fpp)
    forall (t :: FloatPrecision).
    sym
    -> RoundingMode
    -> SymFloat sym t
    -> SymFloat sym t
    -> IO (SymFloat sym t)
    floatDiv

    fpMin :: IsExprBuilder sym => sym -> SFloat sym -> SFloat sym -> IO (SFloat sym)
    fpMin :: forall sym.
    IsExprBuilder sym =>
    sym -> SFloat sym -> SFloat sym -> IO (SFloat sym)
    fpMin sym
    sym (SFloat SymFloat sym fpp
    x) (SFloat SymFloat sym fpp
    y) =
      let t1 :: FloatPrecisionRepr fpp
    t1 = sym
    sym sym -> SymFloat sym fpp -> FloatPrecisionRepr fpp
    forall sym (fpp :: FloatPrecision).
    IsExpr (SymExpr sym) =>
    sym -> SymFloat sym fpp -> FloatPrecisionRepr fpp
    `fpReprOf` SymFloat sym fpp
    x
          t2 :: FloatPrecisionRepr fpp
    t2 = sym
    sym sym -> SymFloat sym fpp -> FloatPrecisionRepr fpp
    forall sym (fpp :: FloatPrecision).
    IsExpr (SymExpr sym) =>
    sym -> SymFloat sym fpp -> FloatPrecisionRepr fpp
    `fpReprOf` SymFloat sym fpp
    y
      in
      case FloatPrecisionRepr fpp
    -> FloatPrecisionRepr fpp -> Maybe (fpp :~: fpp)
    forall {k} (f :: k -> Type) (a :: k) (b :: k).
    TestEquality f =>
    f a -> f b -> Maybe (a :~: b)
    forall (a :: FloatPrecision) (b :: FloatPrecision).
    FloatPrecisionRepr a -> FloatPrecisionRepr b -> Maybe (a :~: b)
    testEquality FloatPrecisionRepr fpp
    t1 FloatPrecisionRepr fpp
    t2 of
        Just fpp :~: fpp
    Refl -> SymFloat sym fpp -> SFloat sym
    forall sym (fpp :: FloatPrecision).
    IsExpr (SymExpr sym) =>
    SymFloat sym fpp -> SFloat sym
    SFloat (SymFloat sym fpp -> SFloat sym)
    -> IO (SymFloat sym fpp) -> IO (SFloat sym)
    forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
    <$> sym
    -> SymFloat sym fpp -> SymFloat sym fpp -> IO (SymFloat sym fpp)
    forall sym (fpp :: FloatPrecision).
    IsExprBuilder sym =>
    sym
    -> SymFloat sym fpp -> SymFloat sym fpp -> IO (SymFloat sym fpp)
    forall (fpp :: FloatPrecision).
    sym
    -> SymFloat sym fpp -> SymFloat sym fpp -> IO (SymFloat sym fpp)
    floatMin sym
    sym SymFloat sym fpp
    x SymFloat sym fpp
    SymFloat sym fpp
    y
        Maybe (fpp :~: fpp)
    _         -> FloatPrecisionRepr fpp -> FloatPrecisionRepr fpp -> IO (SFloat sym)
    forall (t1 :: FloatPrecision) (t2 :: FloatPrecision) a.
    FloatPrecisionRepr t1 -> FloatPrecisionRepr t2 -> IO a
    fpTypeError FloatPrecisionRepr fpp
    t1 FloatPrecisionRepr fpp
    t2

    fpMax :: IsExprBuilder sym => sym -> SFloat sym -> SFloat sym -> IO (SFloat sym)
    fpMax :: forall sym.
    IsExprBuilder sym =>
    sym -> SFloat sym -> SFloat sym -> IO (SFloat sym)
    fpMax sym
    sym (SFloat SymFloat sym fpp
    x) (SFloat SymFloat sym fpp
    y) =
      let t1 :: FloatPrecisionRepr fpp
    t1 = sym
    sym sym -> SymFloat sym fpp -> FloatPrecisionRepr fpp
    forall sym (fpp :: FloatPrecision).
    IsExpr (SymExpr sym) =>
    sym -> SymFloat sym fpp -> FloatPrecisionRepr fpp
    `fpReprOf` SymFloat sym fpp
    x
          t2 :: FloatPrecisionRepr fpp
    t2 = sym
    sym sym -> SymFloat sym fpp -> FloatPrecisionRepr fpp
    forall sym (fpp :: FloatPrecision).
    IsExpr (SymExpr sym) =>
    sym -> SymFloat sym fpp -> FloatPrecisionRepr fpp
    `fpReprOf` SymFloat sym fpp
    y
      in
      case FloatPrecisionRepr fpp
    -> FloatPrecisionRepr fpp -> Maybe (fpp :~: fpp)
    forall {k} (f :: k -> Type) (a :: k) (b :: k).
    TestEquality f =>
    f a -> f b -> Maybe (a :~: b)
    forall (a :: FloatPrecision) (b :: FloatPrecision).
    FloatPrecisionRepr a -> FloatPrecisionRepr b -> Maybe (a :~: b)
    testEquality FloatPrecisionRepr fpp
    t1 FloatPrecisionRepr fpp
    t2 of
        Just fpp :~: fpp
    Refl -> SymFloat sym fpp -> SFloat sym
    forall sym (fpp :: FloatPrecision).
    IsExpr (SymExpr sym) =>
    SymFloat sym fpp -> SFloat sym
    SFloat (SymFloat sym fpp -> SFloat sym)
    -> IO (SymFloat sym fpp) -> IO (SFloat sym)
    forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
    <$> sym
    -> SymFloat sym fpp -> SymFloat sym fpp -> IO (SymFloat sym fpp)
    forall sym (fpp :: FloatPrecision).
    IsExprBuilder sym =>
    sym
    -> SymFloat sym fpp -> SymFloat sym fpp -> IO (SymFloat sym fpp)
    forall (fpp :: FloatPrecision).
    sym
    -> SymFloat sym fpp -> SymFloat sym fpp -> IO (SymFloat sym fpp)
    floatMax sym
    sym SymFloat sym fpp
    x SymFloat sym fpp
    SymFloat sym fpp
    y
        Maybe (fpp :~: fpp)
    _         -> FloatPrecisionRepr fpp -> FloatPrecisionRepr fpp -> IO (SFloat sym)
    forall (t1 :: FloatPrecision) (t2 :: FloatPrecision) a.
    FloatPrecisionRepr t1 -> FloatPrecisionRepr t2 -> IO a
    fpTypeError FloatPrecisionRepr fpp
    t1 FloatPrecisionRepr fpp
    t2

    fpFMA :: IsExprBuilder sym =>
      sym -> RoundingMode -> SFloat sym -> SFloat sym -> SFloat sym -> IO (SFloat sym)
    fpFMA :: forall sym.
    IsExprBuilder sym =>
    sym
    -> RoundingMode
    -> SFloat sym
    -> SFloat sym
    -> SFloat sym
    -> IO (SFloat sym)
    fpFMA sym
    sym RoundingMode
    r (SFloat SymFloat sym fpp
    x) (SFloat SymFloat sym fpp
    y) (SFloat SymFloat sym fpp
    z) =
      let t1 :: FloatPrecisionRepr fpp
    t1 = sym
    sym sym -> SymFloat sym fpp -> FloatPrecisionRepr fpp
    forall sym (fpp :: FloatPrecision).
    IsExpr (SymExpr sym) =>
    sym -> SymFloat sym fpp -> FloatPrecisionRepr fpp
    `fpReprOf` SymFloat sym fpp
    x
          t2 :: FloatPrecisionRepr fpp
    t2 = sym
    sym sym -> SymFloat sym fpp -> FloatPrecisionRepr fpp
    forall sym (fpp :: FloatPrecision).
    IsExpr (SymExpr sym) =>
    sym -> SymFloat sym fpp -> FloatPrecisionRepr fpp
    `fpReprOf` SymFloat sym fpp
    y
          t3 :: FloatPrecisionRepr fpp
    t3 = sym
    sym sym -> SymFloat sym fpp -> FloatPrecisionRepr fpp
    forall sym (fpp :: FloatPrecision).
    IsExpr (SymExpr sym) =>
    sym -> SymFloat sym fpp -> FloatPrecisionRepr fpp
    `fpReprOf` SymFloat sym fpp
    z
       in
       case (FloatPrecisionRepr fpp
    -> FloatPrecisionRepr fpp -> Maybe (fpp :~: fpp)
    forall {k} (f :: k -> Type) (a :: k) (b :: k).
    TestEquality f =>
    f a -> f b -> Maybe (a :~: b)
    forall (a :: FloatPrecision) (b :: FloatPrecision).
    FloatPrecisionRepr a -> FloatPrecisionRepr b -> Maybe (a :~: b)
    testEquality FloatPrecisionRepr fpp
    t1 FloatPrecisionRepr fpp
    t2, FloatPrecisionRepr fpp
    -> FloatPrecisionRepr fpp -> Maybe (fpp :~: fpp)
    forall {k} (f :: k -> Type) (a :: k) (b :: k).
    TestEquality f =>
    f a -> f b -> Maybe (a :~: b)
    forall (a :: FloatPrecision) (b :: FloatPrecision).
    FloatPrecisionRepr a -> FloatPrecisionRepr b -> Maybe (a :~: b)
    testEquality FloatPrecisionRepr fpp
    t2 FloatPrecisionRepr fpp
    t3) of
         (Just fpp :~: fpp
    Refl, Just fpp :~: fpp
    Refl) -> SymFloat sym fpp -> SFloat sym
    forall sym (fpp :: FloatPrecision).
    IsExpr (SymExpr sym) =>
    SymFloat sym fpp -> SFloat sym
    SFloat (SymFloat sym fpp -> SFloat sym)
    -> IO (SymFloat sym fpp) -> IO (SFloat sym)
    forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
    <$> sym
    -> RoundingMode
    -> SymFloat sym fpp
    -> SymFloat sym fpp
    -> SymFloat sym fpp
    -> IO (SymFloat sym fpp)
    forall sym (fpp :: FloatPrecision).
    IsExprBuilder sym =>
    sym
    -> RoundingMode
    -> SymFloat sym fpp
    -> SymFloat sym fpp
    -> SymFloat sym fpp
    -> IO (SymFloat sym fpp)
    forall (fpp :: FloatPrecision).
    sym
    -> RoundingMode
    -> SymFloat sym fpp
    -> SymFloat sym fpp
    -> SymFloat sym fpp
    -> IO (SymFloat sym fpp)
    floatFMA sym
    sym RoundingMode
    r SymFloat sym fpp
    x SymFloat sym fpp
    SymFloat sym fpp
    y SymFloat sym fpp
    SymFloat sym fpp
    z
         (Maybe (fpp :~: fpp)
    Nothing, Maybe (fpp :~: fpp)
    _) -> FloatPrecisionRepr fpp -> FloatPrecisionRepr fpp -> IO (SFloat sym)
    forall (t1 :: FloatPrecision) (t2 :: FloatPrecision) a.
    FloatPrecisionRepr t1 -> FloatPrecisionRepr t2 -> IO a
    fpTypeError FloatPrecisionRepr fpp
    t1 FloatPrecisionRepr fpp
    t2
         (Maybe (fpp :~: fpp)
    _, Maybe (fpp :~: fpp)
    Nothing) -> FloatPrecisionRepr fpp -> FloatPrecisionRepr fpp -> IO (SFloat sym)
    forall (t1 :: FloatPrecision) (t2 :: FloatPrecision) a.
    FloatPrecisionRepr t1 -> FloatPrecisionRepr t2 -> IO a
    fpTypeError FloatPrecisionRepr fpp
    t2 FloatPrecisionRepr fpp
    t3

    fpIte :: IsExprBuilder sym =>
      sym -> Pred sym -> SFloat sym -> SFloat sym -> IO (SFloat sym)
    fpIte :: forall sym.
    IsExprBuilder sym =>
    sym -> Pred sym -> SFloat sym -> SFloat sym -> IO (SFloat sym)
    fpIte sym
    sym Pred sym
    p (SFloat SymFloat sym fpp
    x) (SFloat SymFloat sym fpp
    y) =
      let t1 :: FloatPrecisionRepr fpp
    t1 = sym
    sym sym -> SymFloat sym fpp -> FloatPrecisionRepr fpp
    forall sym (fpp :: FloatPrecision).
    IsExpr (SymExpr sym) =>
    sym -> SymFloat sym fpp -> FloatPrecisionRepr fpp
    `fpReprOf` SymFloat sym fpp
    x
          t2 :: FloatPrecisionRepr fpp
    t2 = sym
    sym sym -> SymFloat sym fpp -> FloatPrecisionRepr fpp
    forall sym (fpp :: FloatPrecision).
    IsExpr (SymExpr sym) =>
    sym -> SymFloat sym fpp -> FloatPrecisionRepr fpp
    `fpReprOf` SymFloat sym fpp
    y
      in
      case FloatPrecisionRepr fpp
    -> FloatPrecisionRepr fpp -> Maybe (fpp :~: fpp)
    forall {k} (f :: k -> Type) (a :: k) (b :: k).
    TestEquality f =>
    f a -> f b -> Maybe (a :~: b)
    forall (a :: FloatPrecision) (b :: FloatPrecision).
    FloatPrecisionRepr a -> FloatPrecisionRepr b -> Maybe (a :~: b)
    testEquality FloatPrecisionRepr fpp
    t1 FloatPrecisionRepr fpp
    t2 of
        Just fpp :~: fpp
    Refl -> SymFloat sym fpp -> SFloat sym
    forall sym (fpp :: FloatPrecision).
    IsExpr (SymExpr sym) =>
    SymFloat sym fpp -> SFloat sym
    SFloat (SymFloat sym fpp -> SFloat sym)
    -> IO (SymFloat sym fpp) -> IO (SFloat sym)
    forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
    <$> sym
    -> Pred sym
    -> SymFloat sym fpp
    -> SymFloat sym fpp
    -> IO (SymFloat sym fpp)
    forall sym (fpp :: FloatPrecision).
    IsExprBuilder sym =>
    sym
    -> Pred sym
    -> SymFloat sym fpp
    -> SymFloat sym fpp
    -> IO (SymFloat sym fpp)
    forall (fpp :: FloatPrecision).
    sym
    -> Pred sym
    -> SymFloat sym fpp
    -> SymFloat sym fpp
    -> IO (SymFloat sym fpp)
    floatIte sym
    sym Pred sym
    p SymFloat sym fpp
    x SymFloat sym fpp
    SymFloat sym fpp
    y
        Maybe (fpp :~: fpp)
    _         -> FloatPrecisionRepr fpp -> FloatPrecisionRepr fpp -> IO (SFloat sym)
    forall (t1 :: FloatPrecision) (t2 :: FloatPrecision) a.
    FloatPrecisionRepr t1 -> FloatPrecisionRepr t2 -> IO a
    fpTypeError FloatPrecisionRepr fpp
    t1 FloatPrecisionRepr fpp
    t2

    --------------------------------------------------------------------------------

    fpRel ::
      IsExprBuilder sym =>
      (forall t.
        sym ->
        SymFloat sym t ->
        SymFloat sym t ->
        IO (Pred sym)
      ) ->
      sym -> SFloat sym -> SFloat sym -> IO (Pred sym)
    fpRel :: forall sym.
    IsExprBuilder sym =>
    (forall (t :: FloatPrecision).
     sym -> SymFloat sym t -> SymFloat sym t -> IO (Pred sym))
    -> sym -> SFloat sym -> SFloat sym -> IO (Pred sym)
    fpRel forall (t :: FloatPrecision).
    sym -> SymFloat sym t -> SymFloat sym t -> IO (Pred sym)
    fun sym
    sym (SFloat SymFloat sym fpp
    x) (SFloat SymFloat sym fpp
    y) =
      let t1 :: FloatPrecisionRepr fpp
    t1 = sym
    sym sym -> SymFloat sym fpp -> FloatPrecisionRepr fpp
    forall sym (fpp :: FloatPrecision).
    IsExpr (SymExpr sym) =>
    sym -> SymFloat sym fpp -> FloatPrecisionRepr fpp
    `fpReprOf` SymFloat sym fpp
    x
          t2 :: FloatPrecisionRepr fpp
    t2 = sym
    sym sym -> SymFloat sym fpp -> FloatPrecisionRepr fpp
    forall sym (fpp :: FloatPrecision).
    IsExpr (SymExpr sym) =>
    sym -> SymFloat sym fpp -> FloatPrecisionRepr fpp
    `fpReprOf` SymFloat sym fpp
    y
      in
      case FloatPrecisionRepr fpp
    -> FloatPrecisionRepr fpp -> Maybe (fpp :~: fpp)
    forall {k} (f :: k -> Type) (a :: k) (b :: k).
    TestEquality f =>
    f a -> f b -> Maybe (a :~: b)
    forall (a :: FloatPrecision) (b :: FloatPrecision).
    FloatPrecisionRepr a -> FloatPrecisionRepr b -> Maybe (a :~: b)
    testEquality FloatPrecisionRepr fpp
    t1 FloatPrecisionRepr fpp
    t2 of
        Just fpp :~: fpp
    Refl -> sym -> SymFloat sym fpp -> SymFloat sym fpp -> IO (Pred sym)
    forall (t :: FloatPrecision).
    sym -> SymFloat sym t -> SymFloat sym t -> IO (Pred sym)
    fun sym
    sym SymFloat sym fpp
    x SymFloat sym fpp
    SymFloat sym fpp
    y
        Maybe (fpp :~: fpp)
    _         -> FloatPrecisionRepr fpp -> FloatPrecisionRepr fpp -> IO (Pred sym)
    forall (t1 :: FloatPrecision) (t2 :: FloatPrecision) a.
    FloatPrecisionRepr t1 -> FloatPrecisionRepr t2 -> IO a
    fpTypeError FloatPrecisionRepr fpp
    t1 FloatPrecisionRepr fpp
    t2

    type SFloatRel sym =
      sym -> SFloat sym -> SFloat sym -> IO (Pred sym)

    fpEq :: IsExprBuilder sym => SFloatRel sym
    fpEq :: forall sym. IsExprBuilder sym => SFloatRel sym
    fpEq = (forall (t :: FloatPrecision).
     sym
     -> SymFloat sym t
     -> SymFloat sym t
     -> IO (SymExpr sym BaseBoolType))
    -> sym -> SFloat sym -> SFloat sym -> IO (SymExpr sym BaseBoolType)
    forall sym.
    IsExprBuilder sym =>
    (forall (t :: FloatPrecision).
     sym -> SymFloat sym t -> SymFloat sym t -> IO (Pred sym))
    -> sym -> SFloat sym -> SFloat sym -> IO (Pred sym)
    fpRel sym
    -> SymFloat sym t
    -> SymFloat sym t
    -> IO (SymExpr sym BaseBoolType)
    forall sym (fpp :: FloatPrecision).
    IsExprBuilder sym =>
    sym -> SymFloat sym fpp -> SymFloat sym fpp -> IO (Pred sym)
    forall (t :: FloatPrecision).
    sym
    -> SymFloat sym t
    -> SymFloat sym t
    -> IO (SymExpr sym BaseBoolType)
    floatEq

    fpEqIEEE :: IsExprBuilder sym => SFloatRel sym
    fpEqIEEE :: forall sym. IsExprBuilder sym => SFloatRel sym
    fpEqIEEE = (forall (t :: FloatPrecision).
     sym
     -> SymFloat sym t
     -> SymFloat sym t
     -> IO (SymExpr sym BaseBoolType))
    -> sym -> SFloat sym -> SFloat sym -> IO (SymExpr sym BaseBoolType)
    forall sym.
    IsExprBuilder sym =>
    (forall (t :: FloatPrecision).
     sym -> SymFloat sym t -> SymFloat sym t -> IO (Pred sym))
    -> sym -> SFloat sym -> SFloat sym -> IO (Pred sym)
    fpRel sym
    -> SymFloat sym t
    -> SymFloat sym t
    -> IO (SymExpr sym BaseBoolType)
    forall sym (fpp :: FloatPrecision).
    IsExprBuilder sym =>
    sym -> SymFloat sym fpp -> SymFloat sym fpp -> IO (Pred sym)
    forall (t :: FloatPrecision).
    sym
    -> SymFloat sym t
    -> SymFloat sym t
    -> IO (SymExpr sym BaseBoolType)
    floatFpEq

    fpLtIEEE :: IsExprBuilder sym => SFloatRel sym
    fpLtIEEE :: forall sym. IsExprBuilder sym => SFloatRel sym
    fpLtIEEE = (forall (t :: FloatPrecision).
     sym
     -> SymFloat sym t
     -> SymFloat sym t
     -> IO (SymExpr sym BaseBoolType))
    -> sym -> SFloat sym -> SFloat sym -> IO (SymExpr sym BaseBoolType)
    forall sym.
    IsExprBuilder sym =>
    (forall (t :: FloatPrecision).
     sym -> SymFloat sym t -> SymFloat sym t -> IO (Pred sym))
    -> sym -> SFloat sym -> SFloat sym -> IO (Pred sym)
    fpRel sym
    -> SymFloat sym t
    -> SymFloat sym t
    -> IO (SymExpr sym BaseBoolType)
    forall sym (fpp :: FloatPrecision).
    IsExprBuilder sym =>
    sym -> SymFloat sym fpp -> SymFloat sym fpp -> IO (Pred sym)
    forall (t :: FloatPrecision).
    sym
    -> SymFloat sym t
    -> SymFloat sym t
    -> IO (SymExpr sym BaseBoolType)
    floatLt

    fpGtIEEE :: IsExprBuilder sym => SFloatRel sym
    fpGtIEEE :: forall sym. IsExprBuilder sym => SFloatRel sym
    fpGtIEEE = (forall (t :: FloatPrecision).
     sym
     -> SymFloat sym t
     -> SymFloat sym t
     -> IO (SymExpr sym BaseBoolType))
    -> sym -> SFloat sym -> SFloat sym -> IO (SymExpr sym BaseBoolType)
    forall sym.
    IsExprBuilder sym =>
    (forall (t :: FloatPrecision).
     sym -> SymFloat sym t -> SymFloat sym t -> IO (Pred sym))
    -> sym -> SFloat sym -> SFloat sym -> IO (Pred sym)
    fpRel sym
    -> SymFloat sym t
    -> SymFloat sym t
    -> IO (SymExpr sym BaseBoolType)
    forall sym (fpp :: FloatPrecision).
    IsExprBuilder sym =>
    sym -> SymFloat sym fpp -> SymFloat sym fpp -> IO (Pred sym)
    forall (t :: FloatPrecision).
    sym
    -> SymFloat sym t
    -> SymFloat sym t
    -> IO (SymExpr sym BaseBoolType)
    floatGt

    --------------------------------------------------------------------------------
    fpRound ::
      IsExprBuilder sym => sym -> RoundingMode -> SFloat sym -> IO (SFloat sym)
    fpRound :: forall sym.
    IsExprBuilder sym =>
    sym -> RoundingMode -> SFloat sym -> IO (SFloat sym)
    fpRound sym
    sym RoundingMode
    r (SFloat SymFloat sym fpp
    x) = SymFloat sym fpp -> SFloat sym
    forall sym (fpp :: FloatPrecision).
    IsExpr (SymExpr sym) =>
    SymFloat sym fpp -> SFloat sym
    SFloat (SymFloat sym fpp -> SFloat sym)
    -> IO (SymFloat sym fpp) -> IO (SFloat sym)
    forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
    <$> sym -> RoundingMode -> SymFloat sym fpp -> IO (SymFloat sym fpp)
    forall sym (fpp :: FloatPrecision).
    IsExprBuilder sym =>
    sym -> RoundingMode -> SymFloat sym fpp -> IO (SymFloat sym fpp)
    forall (fpp :: FloatPrecision).
    sym -> RoundingMode -> SymFloat sym fpp -> IO (SymFloat sym fpp)
    floatRound sym
    sym RoundingMode
    r SymFloat sym fpp
    x

    -- | This is undefined on "special" values (NaN,infinity)
    fpToReal :: IsExprBuilder sym => sym -> SFloat sym -> IO (SymReal sym)
    fpToReal :: forall sym.
    IsExprBuilder sym =>
    sym -> SFloat sym -> IO (SymReal sym)
    fpToReal sym
    sym (SFloat SymFloat sym fpp
    x) = sym -> SymFloat sym fpp -> IO (SymExpr sym BaseRealType)
    forall sym (fpp :: FloatPrecision).
    IsExprBuilder sym =>
    sym -> SymFloat sym fpp -> IO (SymReal sym)
    forall (fpp :: FloatPrecision).
    sym -> SymFloat sym fpp -> IO (SymExpr sym BaseRealType)
    floatToReal sym
    sym SymFloat sym fpp
    x

    fpFromReal ::
      IsExprBuilder sym =>
      sym -> Integer -> Integer -> RoundingMode -> SymReal sym -> IO (SFloat sym)
    fpFromReal :: forall sym.
    IsExprBuilder sym =>
    sym
    -> Integer
    -> Integer
    -> RoundingMode
    -> SymReal sym
    -> IO (SFloat sym)
    fpFromReal sym
    sym Integer
    e Integer
    p RoundingMode
    r SymReal sym
    x
      | Just (Some FloatPrecisionRepr x
    repr) <- Integer -> Integer -> Maybe (Some FloatPrecisionRepr)
    fpRepr Integer
    e Integer
    p = SymFloat sym x -> SFloat sym
    forall sym (fpp :: FloatPrecision).
    IsExpr (SymExpr sym) =>
    SymFloat sym fpp -> SFloat sym
    SFloat (SymFloat sym x -> SFloat sym)
    -> IO (SymFloat sym x) -> IO (SFloat sym)
    forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
    <$> sym
    -> FloatPrecisionRepr x
    -> RoundingMode
    -> SymReal sym
    -> IO (SymFloat sym x)
    forall sym (fpp :: FloatPrecision).
    IsExprBuilder sym =>
    sym
    -> FloatPrecisionRepr fpp
    -> RoundingMode
    -> SymReal sym
    -> IO (SymFloat sym fpp)
    forall (fpp :: FloatPrecision).
    sym
    -> FloatPrecisionRepr fpp
    -> RoundingMode
    -> SymReal sym
    -> IO (SymFloat sym fpp)
    realToFloat sym
    sym FloatPrecisionRepr x
    repr RoundingMode
    r SymReal sym
    x
      | Bool
    otherwise = String -> Integer -> Integer -> IO (SFloat sym)
    forall a. String -> Integer -> Integer -> IO a
    unsupported String
    "fpFromReal" Integer
    e Integer
    p

    fpFromInteger ::
      IsExprBuilder sym =>
      sym -> Integer -> Integer -> RoundingMode -> SymInteger sym -> IO (SFloat sym)
    fpFromInteger :: forall sym.
    IsExprBuilder sym =>
    sym
    -> Integer
    -> Integer
    -> RoundingMode
    -> SymInteger sym
    -> IO (SFloat sym)
    fpFromInteger sym
    sym Integer
    e Integer
    p RoundingMode
    r SymInteger sym
    x = sym
    -> Integer
    -> Integer
    -> RoundingMode
    -> SymExpr sym BaseRealType
    -> IO (SFloat sym)
    forall sym.
    IsExprBuilder sym =>
    sym
    -> Integer
    -> Integer
    -> RoundingMode
    -> SymReal sym
    -> IO (SFloat sym)
    fpFromReal sym
    sym Integer
    e Integer
    p RoundingMode
    r (SymExpr sym BaseRealType -> IO (SFloat sym))
    -> IO (SymExpr sym BaseRealType) -> IO (SFloat sym)
    forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
    =<< sym -> SymInteger sym -> IO (SymExpr sym BaseRealType)
    forall sym.
    IsExprBuilder sym =>
    sym -> SymInteger sym -> IO (SymReal sym)
    integerToReal sym
    sym SymInteger sym
    x

    fpFromRational ::
      IsExprBuilder sym =>
      sym -> Integer -> Integer -> RoundingMode ->
      SymInteger sym -> SymInteger sym -> IO (SFloat sym)
    fpFromRational :: forall sym.
    IsExprBuilder sym =>
    sym
    -> Integer
    -> Integer
    -> RoundingMode
    -> SymInteger sym
    -> SymInteger sym
    -> IO (SFloat sym)
    fpFromRational sym
    sym Integer
    e Integer
    p RoundingMode
    r SymInteger sym
    x SymInteger sym
    y =
      do SymExpr sym BaseRealType
    num <- sym -> SymInteger sym -> IO (SymExpr sym BaseRealType)
    forall sym.
    IsExprBuilder sym =>
    sym -> SymInteger sym -> IO (SymReal sym)
    integerToReal sym
    sym SymInteger sym
    x
         SymExpr sym BaseRealType
    den <- sym -> SymInteger sym -> IO (SymExpr sym BaseRealType)
    forall sym.
    IsExprBuilder sym =>
    sym -> SymInteger sym -> IO (SymReal sym)
    integerToReal sym
    sym SymInteger sym
    y
         SymExpr sym BaseRealType
    res <- sym
    -> SymExpr sym BaseRealType
    -> SymExpr sym BaseRealType
    -> IO (SymExpr sym BaseRealType)
    forall sym.
    IsExprBuilder sym =>
    sym -> SymReal sym -> SymReal sym -> IO (SymReal sym)
    realDiv sym
    sym SymExpr sym BaseRealType
    num SymExpr sym BaseRealType
    den
         sym
    -> Integer
    -> Integer
    -> RoundingMode
    -> SymExpr sym BaseRealType
    -> IO (SFloat sym)
    forall sym.
    IsExprBuilder sym =>
    sym
    -> Integer
    -> Integer
    -> RoundingMode
    -> SymReal sym
    -> IO (SFloat sym)
    fpFromReal sym
    sym Integer
    e Integer
    p RoundingMode
    r SymExpr sym BaseRealType
    res

    {- | Returns a predicate and two integers, @x@ and @y@.
    If the the predicate holds, then @x / y@ is a rational representing
    the floating point number. Assumes the FP number is not one of the
    special ones that has no real representation. -}
    fpToRational ::
      IsSymExprBuilder sym =>
      sym ->
      SFloat sym ->
      IO (Pred sym, SymInteger sym, SymInteger sym)
    fpToRational :: forall sym.
    IsSymExprBuilder sym =>
    sym -> SFloat sym -> IO (Pred sym, SymInteger sym, SymInteger sym)
    fpToRational sym
    sym SFloat sym
    fp =
      do SymExpr sym BaseRealType
    r    <- sym -> SFloat sym -> IO (SymExpr sym BaseRealType)
    forall sym.
    IsExprBuilder sym =>
    sym -> SFloat sym -> IO (SymReal sym)
    fpToReal sym
    sym SFloat sym
    fp
         SymInteger sym
    x    <- sym
    -> SolverSymbol
    -> BaseTypeRepr 'BaseIntegerType
    -> IO (SymInteger sym)
    forall sym (tp :: BaseType).
    IsSymExprBuilder sym =>
    sym -> SolverSymbol -> BaseTypeRepr tp -> IO (SymExpr sym tp)
    forall (tp :: BaseType).
    sym -> SolverSymbol -> BaseTypeRepr tp -> IO (SymExpr sym tp)
    freshConstant sym
    sym SolverSymbol
    emptySymbol BaseTypeRepr 'BaseIntegerType
    BaseIntegerRepr
         SymInteger sym
    y    <- sym
    -> SolverSymbol
    -> BaseTypeRepr 'BaseIntegerType
    -> IO (SymInteger sym)
    forall sym (tp :: BaseType).
    IsSymExprBuilder sym =>
    sym -> SolverSymbol -> BaseTypeRepr tp -> IO (SymExpr sym tp)
    forall (tp :: BaseType).
    sym -> SolverSymbol -> BaseTypeRepr tp -> IO (SymExpr sym tp)
    freshConstant sym
    sym SolverSymbol
    emptySymbol BaseTypeRepr 'BaseIntegerType
    BaseIntegerRepr
         SymExpr sym BaseRealType
    num  <- sym -> SymInteger sym -> IO (SymExpr sym BaseRealType)
    forall sym.
    IsExprBuilder sym =>
    sym -> SymInteger sym -> IO (SymReal sym)
    integerToReal sym
    sym SymInteger sym
    x
         SymExpr sym BaseRealType
    den  <- sym -> SymInteger sym -> IO (SymExpr sym BaseRealType)
    forall sym.
    IsExprBuilder sym =>
    sym -> SymInteger sym -> IO (SymReal sym)
    integerToReal sym
    sym SymInteger sym
    y
         SymExpr sym BaseRealType
    res  <- sym
    -> SymExpr sym BaseRealType
    -> SymExpr sym BaseRealType
    -> IO (SymExpr sym BaseRealType)
    forall sym.
    IsExprBuilder sym =>
    sym -> SymReal sym -> SymReal sym -> IO (SymReal sym)
    realDiv sym
    sym SymExpr sym BaseRealType
    num SymExpr sym BaseRealType
    den
         Pred sym
    same <- sym
    -> SymExpr sym BaseRealType
    -> SymExpr sym BaseRealType
    -> IO (Pred sym)
    forall sym.
    IsExprBuilder sym =>
    sym -> SymReal sym -> SymReal sym -> IO (Pred sym)
    realEq sym
    sym SymExpr sym BaseRealType
    r SymExpr sym BaseRealType
    res
         (Pred sym, SymInteger sym, SymInteger sym)
    -> IO (Pred sym, SymInteger sym, SymInteger sym)
    forall a. a -> IO a
    forall (f :: Type -> Type) a. Applicative f => a -> f a
    pure (Pred sym
    same, SymInteger sym
    x, SymInteger sym
    y)

    --------------------------------------------------------------------------------
    fpIsInf :: IsExprBuilder sym => sym -> SFloat sym -> IO (Pred sym)
    fpIsInf :: forall sym. IsExprBuilder sym => sym -> SFloat sym -> IO (Pred sym)
    fpIsInf sym
    sym (SFloat SymFloat sym fpp
    x) = sym -> SymFloat sym fpp -> IO (SymExpr sym BaseBoolType)
    forall sym (fpp :: FloatPrecision).
    IsExprBuilder sym =>
    sym -> SymFloat sym fpp -> IO (Pred sym)
    forall (fpp :: FloatPrecision).
    sym -> SymFloat sym fpp -> IO (SymExpr sym BaseBoolType)
    floatIsInf sym
    sym SymFloat sym fpp
    x

    fpIsNaN :: IsExprBuilder sym => sym -> SFloat sym -> IO (Pred sym)
    fpIsNaN :: forall sym. IsExprBuilder sym => sym -> SFloat sym -> IO (Pred sym)
    fpIsNaN sym
    sym (SFloat SymFloat sym fpp
    x) = sym -> SymFloat sym fpp -> IO (SymExpr sym BaseBoolType)
    forall sym (fpp :: FloatPrecision).
    IsExprBuilder sym =>
    sym -> SymFloat sym fpp -> IO (Pred sym)
    forall (fpp :: FloatPrecision).
    sym -> SymFloat sym fpp -> IO (SymExpr sym BaseBoolType)
    floatIsNaN sym
    sym SymFloat sym fpp
    x

    fpIsZero :: IsExprBuilder sym => sym -> SFloat sym -> IO (Pred sym)
    fpIsZero :: forall sym. IsExprBuilder sym => sym -> SFloat sym -> IO (Pred sym)
    fpIsZero sym
    sym (SFloat SymFloat sym fpp
    x) = sym -> SymFloat sym fpp -> IO (SymExpr sym BaseBoolType)
    forall sym (fpp :: FloatPrecision).
    IsExprBuilder sym =>
    sym -> SymFloat sym fpp -> IO (Pred sym)
    forall (fpp :: FloatPrecision).
    sym -> SymFloat sym fpp -> IO (SymExpr sym BaseBoolType)
    floatIsZero sym
    sym SymFloat sym fpp
    x

    fpIsNeg :: IsExprBuilder sym => sym -> SFloat sym -> IO (Pred sym)
    fpIsNeg :: forall sym. IsExprBuilder sym => sym -> SFloat sym -> IO (Pred sym)
    fpIsNeg sym
    sym (SFloat SymFloat sym fpp
    x) = sym -> SymFloat sym fpp -> IO (SymExpr sym BaseBoolType)
    forall sym (fpp :: FloatPrecision).
    IsExprBuilder sym =>
    sym -> SymFloat sym fpp -> IO (Pred sym)
    forall (fpp :: FloatPrecision).
    sym -> SymFloat sym fpp -> IO (SymExpr sym BaseBoolType)
    floatIsNeg sym
    sym SymFloat sym fpp
    x

    fpIsSubnorm :: IsExprBuilder sym => sym -> SFloat sym -> IO (Pred sym)
    fpIsSubnorm :: forall sym. IsExprBuilder sym => sym -> SFloat sym -> IO (Pred sym)
    fpIsSubnorm sym
    sym (SFloat SymFloat sym fpp
    x) = sym -> SymFloat sym fpp -> IO (SymExpr sym BaseBoolType)
    forall sym (fpp :: FloatPrecision).
    IsExprBuilder sym =>
    sym -> SymFloat sym fpp -> IO (Pred sym)
    forall (fpp :: FloatPrecision).
    sym -> SymFloat sym fpp -> IO (SymExpr sym BaseBoolType)
    floatIsSubnorm sym
    sym SymFloat sym fpp
    x

    fpIsNorm :: IsExprBuilder sym => sym -> SFloat sym -> IO (Pred sym)
    fpIsNorm :: forall sym. IsExprBuilder sym => sym -> SFloat sym -> IO (Pred sym)
    fpIsNorm sym
    sym (SFloat SymFloat sym fpp
    x) = sym -> SymFloat sym fpp -> IO (SymExpr sym BaseBoolType)
    forall sym (fpp :: FloatPrecision).
    IsExprBuilder sym =>
    sym -> SymFloat sym fpp -> IO (Pred sym)
    forall (fpp :: FloatPrecision).
    sym -> SymFloat sym fpp -> IO (SymExpr sym BaseBoolType)
    floatIsNorm sym
    sym SymFloat sym fpp
    x