    {-# LANGUAGE AllowAmbiguousTypes #-}
    {-# LANGUAGE DataKinds #-}
    {-# LANGUAGE FlexibleInstances #-}
    {-# LANGUAGE GADTs #-}
    {-# LANGUAGE LambdaCase #-}
    {-# LANGUAGE MultiParamTypeClasses #-}
    {-# LANGUAGE TemplateHaskell #-}
    {-# LANGUAGE TypeFamilies #-}
    {-# LANGUAGE TypeOperators #-}

    module What4.InterpretedFloatingPoint
      ( -- * FloatInfo data kind
        type FloatInfo
        -- ** Constructors for kind FloatInfo
      , HalfFloat
      , SingleFloat
      , DoubleFloat
      , QuadFloat
      , X86_80Float
      , DoubleDoubleFloat
        -- ** Representations of FloatInfo types
      , FloatInfoRepr(..)
        -- ** extended 80 bit float values ("long double")
      , X86_80Val(..)
      , fp80ToBits
      , fp80ToRational
        -- ** FloatInfo to/from FloatPrecision
      , FloatInfoToPrecision
      , FloatPrecisionToInfo
      , floatInfoToPrecisionRepr
      , floatPrecisionToInfoRepr
        -- ** Bit-width type family
      , FloatInfoToBitWidth
      , floatInfoToBVTypeRepr
        -- * Interface classes
        -- ** Interpretation type family
      , SymInterpretedFloatType
        -- ** Type alias
      , SymInterpretedFloat
        -- ** IsInterpretedFloatExprBuilder
      , IsInterpretedFloatExprBuilder(..)
      , IsInterpretedFloatSymExprBuilder(..)
      ) where

    import Data.Bits
    import Data.Hashable
    import Data.Kind
    import Data.Parameterized.Classes
    import Data.Parameterized.Context (Assignment, EmptyCtx, (::>))
    import qualified Data.Parameterized.Context as Ctx
    import Data.Parameterized.TH.GADT
    import Data.Ratio
    import Data.Word ( Word16, Word64 )
    import GHC.TypeNats
    import Prettyprinter

    import What4.BaseTypes
    import What4.Interface
    import What4.SpecialFunctions

    -- | This data kind describes the types of floating-point formats.
    -- This consist of the standard IEEE 754-2008 binary floating point formats,
    -- as well as the X86 extended 80-bit format and the double-double format.
    data FloatInfo where
      HalfFloat         :: FloatInfo  --  16 bit binary IEEE754
      SingleFloat       :: FloatInfo  --  32 bit binary IEEE754
      DoubleFloat       :: FloatInfo  --  64 bit binary IEEE754
      QuadFloat         :: FloatInfo  -- 128 bit binary IEEE754
      X86_80Float       :: FloatInfo  -- X86 80-bit extended floats
      DoubleDoubleFloat :: FloatInfo  -- two 64-bit floats fused in the "double-double" style

    type HalfFloat         = 'HalfFloat         -- ^  16 bit binary IEEE754.
    type SingleFloat       = 'SingleFloat       -- ^  32 bit binary IEEE754.
    type DoubleFloat       = 'DoubleFloat       -- ^  64 bit binary IEEE754.
    type QuadFloat         = 'QuadFloat         -- ^ 128 bit binary IEEE754.
    type X86_80Float       = 'X86_80Float       -- ^ X86 80-bit extended floats.
    type DoubleDoubleFloat = 'DoubleDoubleFloat -- ^ Two 64-bit floats fused in the "double-double" style.

    -- | A family of value-level representatives for floating-point types.
    data FloatInfoRepr (fi :: FloatInfo) where
      HalfFloatRepr         :: FloatInfoRepr HalfFloat
      SingleFloatRepr       :: FloatInfoRepr SingleFloat
      DoubleFloatRepr       :: FloatInfoRepr DoubleFloat
      QuadFloatRepr         :: FloatInfoRepr QuadFloat
      X86_80FloatRepr       :: FloatInfoRepr X86_80Float
      DoubleDoubleFloatRepr :: FloatInfoRepr DoubleDoubleFloat

    instance KnownRepr FloatInfoRepr HalfFloat         where knownRepr :: FloatInfoRepr HalfFloat
    knownRepr = FloatInfoRepr HalfFloat
    HalfFloatRepr
    instance KnownRepr FloatInfoRepr SingleFloat       where knownRepr :: FloatInfoRepr SingleFloat
    knownRepr = FloatInfoRepr SingleFloat
    SingleFloatRepr
    instance KnownRepr FloatInfoRepr DoubleFloat       where knownRepr :: FloatInfoRepr DoubleFloat
    knownRepr = FloatInfoRepr DoubleFloat
    DoubleFloatRepr
    instance KnownRepr FloatInfoRepr QuadFloat         where knownRepr :: FloatInfoRepr QuadFloat
    knownRepr = FloatInfoRepr QuadFloat
    QuadFloatRepr
    instance KnownRepr FloatInfoRepr X86_80Float       where knownRepr :: FloatInfoRepr X86_80Float
    knownRepr = FloatInfoRepr X86_80Float
    X86_80FloatRepr
    instance KnownRepr FloatInfoRepr DoubleDoubleFloat where knownRepr :: FloatInfoRepr DoubleDoubleFloat
    knownRepr = FloatInfoRepr DoubleDoubleFloat
    DoubleDoubleFloatRepr

    $(return [])

    instance HashableF FloatInfoRepr where
      hashWithSaltF :: forall (tp :: FloatInfo). Int -> FloatInfoRepr tp -> Int
    hashWithSaltF = Int -> FloatInfoRepr tp -> Int
    forall a. Hashable a => Int -> a -> Int
    hashWithSalt
    instance Hashable (FloatInfoRepr fi) where
      hashWithSalt :: Int -> FloatInfoRepr fi -> Int
    hashWithSalt = $(structuralHashWithSalt [t|FloatInfoRepr|] [])

    instance Pretty (FloatInfoRepr fi) where
      pretty :: forall ann. FloatInfoRepr fi -> Doc ann
    pretty = FloatInfoRepr fi -> Doc ann
    forall a ann. Show a => a -> Doc ann
    viaShow
    instance Show (FloatInfoRepr fi) where
      showsPrec :: Int -> FloatInfoRepr fi -> ShowS
    showsPrec = $(structuralShowsPrec [t|FloatInfoRepr|])
    instance ShowF FloatInfoRepr

    instance TestEquality FloatInfoRepr where
      testEquality :: forall (a :: FloatInfo) (b :: FloatInfo).
    FloatInfoRepr a -> FloatInfoRepr b -> Maybe (a :~: b)
    testEquality = $(structuralTypeEquality [t|FloatInfoRepr|] [])
    instance Eq (FloatInfoRepr fi) where
      FloatInfoRepr fi
    x == :: FloatInfoRepr fi -> FloatInfoRepr fi -> Bool
    == FloatInfoRepr fi
    y = Maybe (fi :~: fi) -> Bool
    forall a. Maybe a -> Bool
    isJust (FloatInfoRepr fi -> FloatInfoRepr fi -> Maybe (fi :~: fi)
    forall {k} (f :: k -> Type) (a :: k) (b :: k).
    TestEquality f =>
    f a -> f b -> Maybe (a :~: b)
    forall (a :: FloatInfo) (b :: FloatInfo).
    FloatInfoRepr a -> FloatInfoRepr b -> Maybe (a :~: b)
    testEquality FloatInfoRepr fi
    x FloatInfoRepr fi
    y)
    instance OrdF FloatInfoRepr where
      compareF :: forall (x :: FloatInfo) (y :: FloatInfo).
    FloatInfoRepr x -> FloatInfoRepr y -> OrderingF x y
    compareF = $(structuralTypeOrd [t|FloatInfoRepr|] [])

    type family FloatInfoToPrecision (fi :: FloatInfo) :: FloatPrecision where
      FloatInfoToPrecision HalfFloat   = Prec16
      FloatInfoToPrecision SingleFloat = Prec32
      FloatInfoToPrecision DoubleFloat = Prec64
      FloatInfoToPrecision X86_80Float = Prec80
      FloatInfoToPrecision QuadFloat   = Prec128

    type family FloatPrecisionToInfo (fpp :: FloatPrecision) :: FloatInfo where
      FloatPrecisionToInfo Prec16  = HalfFloat
      FloatPrecisionToInfo Prec32  = SingleFloat
      FloatPrecisionToInfo Prec64  = DoubleFloat
      FloatPrecisionToInfo Prec80  = X86_80Float
      FloatPrecisionToInfo Prec128 = QuadFloat

    type family FloatInfoToBitWidth (fi :: FloatInfo) :: GHC.TypeNats.Nat where
      FloatInfoToBitWidth HalfFloat         = 16
      FloatInfoToBitWidth SingleFloat       = 32
      FloatInfoToBitWidth DoubleFloat       = 64
      FloatInfoToBitWidth X86_80Float       = 80
      FloatInfoToBitWidth QuadFloat         = 128
      FloatInfoToBitWidth DoubleDoubleFloat = 128

    floatInfoToPrecisionRepr
      :: FloatInfoRepr fi -> FloatPrecisionRepr (FloatInfoToPrecision fi)
    floatInfoToPrecisionRepr :: forall (fi :: FloatInfo).
    FloatInfoRepr fi -> FloatPrecisionRepr (FloatInfoToPrecision fi)
    floatInfoToPrecisionRepr = \case
      FloatInfoRepr fi
    HalfFloatRepr         -> FloatPrecisionRepr Prec16
    FloatPrecisionRepr (FloatInfoToPrecision fi)
    forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
    knownRepr
      FloatInfoRepr fi
    SingleFloatRepr       -> FloatPrecisionRepr Prec32
    FloatPrecisionRepr (FloatInfoToPrecision fi)
    forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
    knownRepr
      FloatInfoRepr fi
    DoubleFloatRepr       -> FloatPrecisionRepr Prec64
    FloatPrecisionRepr (FloatInfoToPrecision fi)
    forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
    knownRepr
      FloatInfoRepr fi
    QuadFloatRepr         -> FloatPrecisionRepr Prec128
    FloatPrecisionRepr (FloatInfoToPrecision fi)
    forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
    knownRepr
      FloatInfoRepr fi
    X86_80FloatRepr       -> FloatPrecisionRepr Prec80
    FloatPrecisionRepr (FloatInfoToPrecision fi)
    forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
    knownRepr -- n.b. semantics TBD, not technically an IEEE-754 format.
      FloatInfoRepr fi
    DoubleDoubleFloatRepr -> String
    -> FloatPrecisionRepr (FloatInfoToPrecision DoubleDoubleFloat)
    forall a. HasCallStack => String -> a
    error String
    "double-double is not an IEEE-754 format."

    floatPrecisionToInfoRepr
      :: FloatPrecisionRepr fpp -> FloatInfoRepr (FloatPrecisionToInfo fpp)
    floatPrecisionToInfoRepr :: forall (fpp :: FloatPrecision).
    FloatPrecisionRepr fpp -> FloatInfoRepr (FloatPrecisionToInfo fpp)
    floatPrecisionToInfoRepr FloatPrecisionRepr fpp
    fpp
      | Just fpp :~: Prec16
    Refl <- FloatPrecisionRepr fpp
    -> FloatPrecisionRepr Prec16 -> Maybe (fpp :~: Prec16)
    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
    fpp (FloatPrecisionRepr Prec16
    forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
    knownRepr :: FloatPrecisionRepr Prec16)
      = FloatInfoRepr HalfFloat
    FloatInfoRepr (FloatPrecisionToInfo fpp)
    forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
    knownRepr
      | Just fpp :~: Prec32
    Refl <- FloatPrecisionRepr fpp
    -> FloatPrecisionRepr Prec32 -> Maybe (fpp :~: Prec32)
    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
    fpp (FloatPrecisionRepr Prec32
    forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
    knownRepr :: FloatPrecisionRepr Prec32)
      = FloatInfoRepr SingleFloat
    FloatInfoRepr (FloatPrecisionToInfo fpp)
    forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
    knownRepr
      | Just fpp :~: Prec64
    Refl <- FloatPrecisionRepr fpp
    -> FloatPrecisionRepr Prec64 -> Maybe (fpp :~: Prec64)
    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
    fpp (FloatPrecisionRepr Prec64
    forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
    knownRepr :: FloatPrecisionRepr Prec64)
      = FloatInfoRepr DoubleFloat
    FloatInfoRepr (FloatPrecisionToInfo fpp)
    forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
    knownRepr
      | Just fpp :~: Prec80
    Refl <- FloatPrecisionRepr fpp
    -> FloatPrecisionRepr Prec80 -> Maybe (fpp :~: Prec80)
    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
    fpp (FloatPrecisionRepr Prec80
    forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
    knownRepr :: FloatPrecisionRepr Prec80)
      = FloatInfoRepr X86_80Float
    FloatInfoRepr (FloatPrecisionToInfo fpp)
    forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
    knownRepr
      | Just fpp :~: Prec128
    Refl <- FloatPrecisionRepr fpp
    -> FloatPrecisionRepr Prec128 -> Maybe (fpp :~: Prec128)
    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
    fpp (FloatPrecisionRepr Prec128
    forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
    knownRepr :: FloatPrecisionRepr Prec128)
      = FloatInfoRepr QuadFloat
    FloatInfoRepr (FloatPrecisionToInfo fpp)
    forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
    knownRepr
      | Bool
    otherwise
      = String -> FloatInfoRepr (FloatPrecisionToInfo fpp)
    forall a. HasCallStack => String -> a
    error (String -> FloatInfoRepr (FloatPrecisionToInfo fpp))
    -> String -> FloatInfoRepr (FloatPrecisionToInfo fpp)
    forall a b. (a -> b) -> a -> b
    $ String
    "unexpected IEEE-754 precision: " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ FloatPrecisionRepr fpp -> String
    forall a. Show a => a -> String
    show FloatPrecisionRepr fpp
    fpp

    floatInfoToBVTypeRepr
      :: FloatInfoRepr fi -> BaseTypeRepr (BaseBVType (FloatInfoToBitWidth fi))
    floatInfoToBVTypeRepr :: forall (fi :: FloatInfo).
    FloatInfoRepr fi
    -> BaseTypeRepr (BaseBVType (FloatInfoToBitWidth fi))
    floatInfoToBVTypeRepr = \case
      FloatInfoRepr fi
    HalfFloatRepr         -> BaseTypeRepr (BaseBVType 16)
    BaseTypeRepr (BaseBVType (FloatInfoToBitWidth fi))
    forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
    knownRepr
      FloatInfoRepr fi
    SingleFloatRepr       -> BaseTypeRepr (BaseBVType 32)
    BaseTypeRepr (BaseBVType (FloatInfoToBitWidth fi))
    forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
    knownRepr
      FloatInfoRepr fi
    DoubleFloatRepr       -> BaseTypeRepr (BaseBVType 64)
    BaseTypeRepr (BaseBVType (FloatInfoToBitWidth fi))
    forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
    knownRepr
      FloatInfoRepr fi
    QuadFloatRepr         -> BaseTypeRepr (BaseBVType 128)
    BaseTypeRepr (BaseBVType (FloatInfoToBitWidth fi))
    forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
    knownRepr
      FloatInfoRepr fi
    X86_80FloatRepr       -> BaseTypeRepr (BaseBVType 80)
    BaseTypeRepr (BaseBVType (FloatInfoToBitWidth fi))
    forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
    knownRepr
      FloatInfoRepr fi
    DoubleDoubleFloatRepr -> BaseTypeRepr (BaseBVType 128)
    BaseTypeRepr (BaseBVType (FloatInfoToBitWidth fi))
    forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
    knownRepr

    -- | Representation of 80-bit floating values, since there's no native
    -- Haskell type for these.
    data X86_80Val = X86_80Val
                     Word16 -- exponent
                     Word64 -- significand
                   deriving (Int -> X86_80Val -> ShowS
    [X86_80Val] -> ShowS
    X86_80Val -> String
    (Int -> X86_80Val -> ShowS)
    -> (X86_80Val -> String)
    -> ([X86_80Val] -> ShowS)
    -> Show X86_80Val
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: Int -> X86_80Val -> ShowS
    showsPrec :: Int -> X86_80Val -> ShowS
    $cshow :: X86_80Val -> String
    show :: X86_80Val -> String
    $cshowList :: [X86_80Val] -> ShowS
    showList :: [X86_80Val] -> ShowS
    Show, X86_80Val -> X86_80Val -> Bool
    (X86_80Val -> X86_80Val -> Bool)
    -> (X86_80Val -> X86_80Val -> Bool) -> Eq X86_80Val
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    $c== :: X86_80Val -> X86_80Val -> Bool
    == :: X86_80Val -> X86_80Val -> Bool
    $c/= :: X86_80Val -> X86_80Val -> Bool
    /= :: X86_80Val -> X86_80Val -> Bool
    Eq, Eq X86_80Val
    Eq X86_80Val
    -> (X86_80Val -> X86_80Val -> Ordering)
    -> (X86_80Val -> X86_80Val -> Bool)
    -> (X86_80Val -> X86_80Val -> Bool)
    -> (X86_80Val -> X86_80Val -> Bool)
    -> (X86_80Val -> X86_80Val -> Bool)
    -> (X86_80Val -> X86_80Val -> X86_80Val)
    -> (X86_80Val -> X86_80Val -> X86_80Val)
    -> Ord X86_80Val
    X86_80Val -> X86_80Val -> Bool
    X86_80Val -> X86_80Val -> Ordering
    X86_80Val -> X86_80Val -> X86_80Val
    forall a.
    Eq a
    -> (a -> a -> Ordering)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> a)
    -> (a -> a -> a)
    -> Ord a
    $ccompare :: X86_80Val -> X86_80Val -> Ordering
    compare :: X86_80Val -> X86_80Val -> Ordering
    $c< :: X86_80Val -> X86_80Val -> Bool
    < :: X86_80Val -> X86_80Val -> Bool
    $c<= :: X86_80Val -> X86_80Val -> Bool
    <= :: X86_80Val -> X86_80Val -> Bool
    $c> :: X86_80Val -> X86_80Val -> Bool
    > :: X86_80Val -> X86_80Val -> Bool
    $c>= :: X86_80Val -> X86_80Val -> Bool
    >= :: X86_80Val -> X86_80Val -> Bool
    $cmax :: X86_80Val -> X86_80Val -> X86_80Val
    max :: X86_80Val -> X86_80Val -> X86_80Val
    $cmin :: X86_80Val -> X86_80Val -> X86_80Val
    min :: X86_80Val -> X86_80Val -> X86_80Val
    Ord)

    fp80ToBits :: X86_80Val -> Integer
    fp80ToBits :: X86_80Val -> Integer
    fp80ToBits (X86_80Val Word16
    ex Word64
    mantissa) =
      Integer -> Int -> Integer
    forall a. Bits a => a -> Int -> a
    shiftL (Word16 -> Integer
    forall a. Integral a => a -> Integer
    toInteger Word16
    ex) Int
    64 Integer -> Integer -> Integer
    forall a. Bits a => a -> a -> a
    .|. Word64 -> Integer
    forall a. Integral a => a -> Integer
    toInteger Word64
    mantissa

    fp80ToRational :: X86_80Val -> Maybe Rational
    fp80ToRational :: X86_80Val -> Maybe Rational
    fp80ToRational (X86_80Val Word16
    ex Word64
    mantissa)
        -- infinities/NaN/etc
      | Word16
    ex' Word16 -> Word16 -> Bool
    forall a. Eq a => a -> a -> Bool
    == Word16
    0x7FFF = Maybe Rational
    forall a. Maybe a
    Nothing

        -- denormal/pseudo-denormal/normal/unnormal numbers
      | Bool
    otherwise = Rational -> Maybe Rational
    forall a. a -> Maybe a
    Just (Rational -> Maybe Rational) -> Rational -> Maybe Rational
    forall a b. (a -> b) -> a -> b
    $! (if Bool
    s then Rational -> Rational
    forall a. Num a => a -> a
    negate else Rational -> Rational
    forall a. a -> a
    id) (Rational
    m Rational -> Rational -> Rational
    forall a. Num a => a -> a -> a
    * (Integer
    1 Integer -> Integer -> Rational
    forall a. Integral a => a -> a -> Ratio a
    % Integer
    2Integer -> Integer -> Integer
    forall a b. (Num a, Integral b) => a -> b -> a
    ^Integer
    e))

      where
      s :: Bool
    s   = Word16 -> Int -> Bool
    forall a. Bits a => a -> Int -> Bool
    testBit Word16
    ex Int
    15
      ex' :: Word16
    ex' = Word16
    ex Word16 -> Word16 -> Word16
    forall a. Bits a => a -> a -> a
    .&. Word16
    0x7FFF
      m :: Rational
    m   = (Word64 -> Integer
    forall a. Integral a => a -> Integer
    toInteger Word64
    mantissa) Integer -> Integer -> Rational
    forall a. Integral a => a -> a -> Ratio a
    % ((Integer
    2::Integer)Integer -> Integer -> Integer
    forall a b. (Num a, Integral b) => a -> b -> a
    ^(Integer
    63::Integer))
      e :: Integer
    e   = Integer
    16382 Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    - Word16 -> Integer
    forall a. Integral a => a -> Integer
    toInteger Word16
    ex'

    -- Note that the long-double package also provides a representation
    -- for 80-bit floating point values but that package includes
    -- significant FFI compatibility elements which may not be necessary
    -- here; in the future that could be used by defining 'type X86_80Val
    -- = LongDouble'.

    -- | Interpretation of the floating point type.
    type family SymInterpretedFloatType (sym :: Type) (fi :: FloatInfo) :: BaseType

    -- | Symbolic floating point numbers.
    type SymInterpretedFloat sym fi = SymExpr sym (SymInterpretedFloatType sym fi)

    -- | Abstact floating point operations.
    class IsExprBuilder sym => IsInterpretedFloatExprBuilder sym where
      -- | Return floating point number @+0@.
      iFloatPZero :: sym -> FloatInfoRepr fi -> IO (SymInterpretedFloat sym fi)

      -- | Return floating point number @-0@.
      iFloatNZero :: sym -> FloatInfoRepr fi -> IO (SymInterpretedFloat sym fi)

      -- |  Return floating point NaN.
      iFloatNaN :: sym -> FloatInfoRepr fi -> IO (SymInterpretedFloat sym fi)

      -- | Return floating point @+infinity@.
      iFloatPInf :: sym -> FloatInfoRepr fi -> IO (SymInterpretedFloat sym fi)

      -- | Return floating point @-infinity@.
      iFloatNInf :: sym -> FloatInfoRepr fi -> IO (SymInterpretedFloat sym fi)

      -- | Create a floating point literal from a rational literal.
      iFloatLitRational
        :: sym -> FloatInfoRepr fi -> Rational -> IO (SymInterpretedFloat sym fi)

      -- | Create a (single precision) floating point literal.
      iFloatLitSingle :: sym -> Float -> IO (SymInterpretedFloat sym SingleFloat)
      -- | Create a (double precision) floating point literal.
      iFloatLitDouble :: sym -> Double -> IO (SymInterpretedFloat sym DoubleFloat)
      -- | Create an (extended double precision) floating point literal.
      iFloatLitLongDouble :: sym -> X86_80Val -> IO (SymInterpretedFloat sym X86_80Float)

      -- | Negate a floating point number.
      iFloatNeg
        :: sym
        -> SymInterpretedFloat sym fi
        -> IO (SymInterpretedFloat sym fi)

      -- | Return the absolute value of a floating point number.
      iFloatAbs
        :: sym
        -> SymInterpretedFloat sym fi
        -> IO (SymInterpretedFloat sym fi)

      -- | Compute the square root of a floating point number.
      iFloatSqrt
        :: sym
        -> RoundingMode
        -> SymInterpretedFloat sym fi
        -> IO (SymInterpretedFloat sym fi)

      -- | Add two floating point numbers.
      iFloatAdd
        :: sym
        -> RoundingMode
        -> SymInterpretedFloat sym fi
        -> SymInterpretedFloat sym fi
        -> IO (SymInterpretedFloat sym fi)

      -- | Subtract two floating point numbers.
      iFloatSub
        :: sym
        -> RoundingMode
        -> SymInterpretedFloat sym fi
        -> SymInterpretedFloat sym fi
        -> IO (SymInterpretedFloat sym fi)

      -- | Multiply two floating point numbers.
      iFloatMul
        :: sym
        -> RoundingMode
        -> SymInterpretedFloat sym fi
        -> SymInterpretedFloat sym fi
        -> IO (SymInterpretedFloat sym fi)

      -- | Divide two floating point numbers.
      iFloatDiv
        :: sym
        -> RoundingMode
        -> SymInterpretedFloat sym fi
        -> SymInterpretedFloat sym fi
        -> IO (SymInterpretedFloat sym fi)

      -- | Compute the reminder: @x - y * n@, where @n@ in Z is nearest to @x / y@.
      iFloatRem
        :: sym
        -> SymInterpretedFloat sym fi
        -> SymInterpretedFloat sym fi
        -> IO (SymInterpretedFloat sym fi)

      -- | Return the min of two floating point numbers.
      iFloatMin
        :: sym
        -> SymInterpretedFloat sym fi
        -> SymInterpretedFloat sym fi
        -> IO (SymInterpretedFloat sym fi)

      -- | Return the max of two floating point numbers.
      iFloatMax
        :: sym
        -> SymInterpretedFloat sym fi
        -> SymInterpretedFloat sym fi
        -> IO (SymInterpretedFloat sym fi)

      -- | Compute the fused multiplication and addition: @(x * y) + z@.
      iFloatFMA
        :: sym
        -> RoundingMode
        -> SymInterpretedFloat sym fi
        -> SymInterpretedFloat sym fi
        -> SymInterpretedFloat sym fi
        -> IO (SymInterpretedFloat sym fi)

      -- | Check logical equality of two floating point numbers.
      iFloatEq
        :: sym
        -> SymInterpretedFloat sym fi
        -> SymInterpretedFloat sym fi
        -> IO (Pred sym)

      -- | Check logical non-equality of two floating point numbers.
      iFloatNe
        :: sym
        -> SymInterpretedFloat sym fi
        -> SymInterpretedFloat sym fi
        -> IO (Pred sym)

      -- | Check IEEE equality of two floating point numbers.
      iFloatFpEq
        :: sym
        -> SymInterpretedFloat sym fi
        -> SymInterpretedFloat sym fi
        -> IO (Pred sym)

      -- | Check IEEE apartness of two floating point numbers.
      iFloatFpApart
        :: sym
        -> SymInterpretedFloat sym fi
        -> SymInterpretedFloat sym fi
        -> IO (Pred sym)

      -- | Check @<=@ on two floating point numbers.
      iFloatLe
        :: sym
        -> SymInterpretedFloat sym fi
        -> SymInterpretedFloat sym fi
        -> IO (Pred sym)

      -- | Check @<@ on two floating point numbers.
      iFloatLt
        :: sym
        -> SymInterpretedFloat sym fi
        -> SymInterpretedFloat sym fi
        -> IO (Pred sym)

      -- | Check @>=@ on two floating point numbers.
      iFloatGe
        :: sym
        -> SymInterpretedFloat sym fi
        -> SymInterpretedFloat sym fi
        -> IO (Pred sym)

      -- | Check @>@ on two floating point numbers.
      iFloatGt
        :: sym
        -> SymInterpretedFloat sym fi
        -> SymInterpretedFloat sym fi
        -> IO (Pred sym)

      iFloatIsNaN :: sym -> SymInterpretedFloat sym fi -> IO (Pred sym)
      iFloatIsInf :: sym -> SymInterpretedFloat sym fi -> IO (Pred sym)
      iFloatIsZero :: sym -> SymInterpretedFloat sym fi -> IO (Pred sym)
      iFloatIsPos :: sym -> SymInterpretedFloat sym fi -> IO (Pred sym)
      iFloatIsNeg :: sym -> SymInterpretedFloat sym fi -> IO (Pred sym)
      iFloatIsSubnorm :: sym -> SymInterpretedFloat sym fi -> IO (Pred sym)
      iFloatIsNorm :: sym -> SymInterpretedFloat sym fi -> IO (Pred sym)

      -- | If-then-else on floating point numbers.
      iFloatIte
        :: sym
        -> Pred sym
        -> SymInterpretedFloat sym fi
        -> SymInterpretedFloat sym fi
        -> IO (SymInterpretedFloat sym fi)

      -- | Change the precision of a floating point number.
      iFloatCast
        :: sym
        -> FloatInfoRepr fi
        -> RoundingMode
        -> SymInterpretedFloat sym fi'
        -> IO (SymInterpretedFloat sym fi)
      -- | Round a floating point number to an integral value.
      iFloatRound
        :: sym
        -> RoundingMode
        -> SymInterpretedFloat sym fi
        -> IO (SymInterpretedFloat sym fi)
      -- | Convert from binary representation in IEEE 754-2008 format to
      --   floating point.
      iFloatFromBinary
        :: sym
        -> FloatInfoRepr fi
        -> SymBV sym (FloatInfoToBitWidth fi)
        -> IO (SymInterpretedFloat sym fi)
      -- | Convert from floating point from to the binary representation in
      --   IEEE 754-2008 format.
      iFloatToBinary
        :: sym
        -> FloatInfoRepr fi
        -> SymInterpretedFloat sym fi
        -> IO (SymBV sym (FloatInfoToBitWidth fi))
      -- | Convert a unsigned bitvector to a floating point number.
      iBVToFloat
        :: (1 <= w)
        => sym
        -> FloatInfoRepr fi
        -> RoundingMode
        -> SymBV sym w
        -> IO (SymInterpretedFloat sym fi)
      -- | Convert a signed bitvector to a floating point number.
      iSBVToFloat
        :: (1 <= w) => sym
        -> FloatInfoRepr fi
        -> RoundingMode
        -> SymBV sym w
        -> IO (SymInterpretedFloat sym fi)
      -- | Convert a real number to a floating point number.
      iRealToFloat
        :: sym
        -> FloatInfoRepr fi
        -> RoundingMode
        -> SymReal sym
        -> IO (SymInterpretedFloat sym fi)
      -- | Convert a floating point number to a unsigned bitvector.
      iFloatToBV
        :: (1 <= w)
        => sym
        -> NatRepr w
        -> RoundingMode
        -> SymInterpretedFloat sym fi
        -> IO (SymBV sym w)
      -- | Convert a floating point number to a signed bitvector.
      iFloatToSBV
        :: (1 <= w)
        => sym
        -> NatRepr w
        -> RoundingMode
        -> SymInterpretedFloat sym fi
        -> IO (SymBV sym w)
      -- | Convert a floating point number to a real number.
      iFloatToReal :: sym -> SymInterpretedFloat sym fi -> IO (SymReal sym)

      -- | Apply a special function to floating-point arguments
      iFloatSpecialFunction
        :: sym
        -> FloatInfoRepr fi
        -> SpecialFunction args
        -> Assignment (SpecialFnArg (SymExpr sym) (SymInterpretedFloatType sym fi)) args
        -> IO (SymInterpretedFloat sym fi)

      -- | Access a 0-arity special function constant
      iFloatSpecialFunction0
        :: sym
        -> FloatInfoRepr fi
        -> SpecialFunction EmptyCtx
        -> IO (SymInterpretedFloat sym fi)
      iFloatSpecialFunction0 sym
    sym FloatInfoRepr fi
    fi SpecialFunction EmptyCtx
    fn =
        sym
    -> FloatInfoRepr fi
    -> SpecialFunction EmptyCtx
    -> Assignment
         (SpecialFnArg (SymExpr sym) (SymInterpretedFloatType sym fi))
         EmptyCtx
    -> IO (SymExpr sym (SymInterpretedFloatType sym fi))
    forall sym (fi :: FloatInfo) (args :: Ctx Type).
    IsInterpretedFloatExprBuilder sym =>
    sym
    -> FloatInfoRepr fi
    -> SpecialFunction args
    -> Assignment
         (SpecialFnArg (SymExpr sym) (SymInterpretedFloatType sym fi)) args
    -> IO (SymInterpretedFloat sym fi)
    forall (fi :: FloatInfo) (args :: Ctx Type).
    sym
    -> FloatInfoRepr fi
    -> SpecialFunction args
    -> Assignment
         (SpecialFnArg (SymExpr sym) (SymInterpretedFloatType sym fi)) args
    -> IO (SymInterpretedFloat sym fi)
    iFloatSpecialFunction sym
    sym FloatInfoRepr fi
    fi SpecialFunction EmptyCtx
    fn Assignment
      (SpecialFnArg (SymExpr sym) (SymInterpretedFloatType sym fi))
      EmptyCtx
    forall {k} (ctx :: Ctx k) (f :: k -> Type).
    (ctx ~ EmptyCtx) =>
    Assignment f ctx
    Ctx.Empty

      -- | Apply a 1-argument special function
      iFloatSpecialFunction1
        :: sym
        -> FloatInfoRepr fi
        -> SpecialFunction (EmptyCtx ::> R)
        -> SymInterpretedFloat sym fi
        -> IO (SymInterpretedFloat sym fi)
      iFloatSpecialFunction1 sym
    sym FloatInfoRepr fi
    fi SpecialFunction (EmptyCtx ::> R)
    fn SymInterpretedFloat sym fi
    x =
        sym
    -> FloatInfoRepr fi
    -> SpecialFunction (EmptyCtx ::> R)
    -> Assignment
         (SpecialFnArg (SymExpr sym) (SymInterpretedFloatType sym fi))
         (EmptyCtx ::> R)
    -> IO (SymInterpretedFloat sym fi)
    forall sym (fi :: FloatInfo) (args :: Ctx Type).
    IsInterpretedFloatExprBuilder sym =>
    sym
    -> FloatInfoRepr fi
    -> SpecialFunction args
    -> Assignment
         (SpecialFnArg (SymExpr sym) (SymInterpretedFloatType sym fi)) args
    -> IO (SymInterpretedFloat sym fi)
    forall (fi :: FloatInfo) (args :: Ctx Type).
    sym
    -> FloatInfoRepr fi
    -> SpecialFunction args
    -> Assignment
         (SpecialFnArg (SymExpr sym) (SymInterpretedFloatType sym fi)) args
    -> IO (SymInterpretedFloat sym fi)
    iFloatSpecialFunction sym
    sym FloatInfoRepr fi
    fi SpecialFunction (EmptyCtx ::> R)
    fn (Assignment
      (SpecialFnArg (SymExpr sym) (SymInterpretedFloatType sym fi))
      EmptyCtx
    forall {k} (ctx :: Ctx k) (f :: k -> Type).
    (ctx ~ EmptyCtx) =>
    Assignment f ctx
    Ctx.Empty Assignment
      (SpecialFnArg (SymExpr sym) (SymInterpretedFloatType sym fi))
      EmptyCtx
    -> SpecialFnArg (SymExpr sym) (SymInterpretedFloatType sym fi) R
    -> Assignment
         (SpecialFnArg (SymExpr sym) (SymInterpretedFloatType sym fi))
         (EmptyCtx ::> R)
    forall {k} (ctx' :: Ctx k) (f :: k -> Type) (ctx :: Ctx k)
           (tp :: k).
    (ctx' ~ (ctx ::> tp)) =>
    Assignment f ctx -> f tp -> Assignment f ctx'
    Ctx.:> SymInterpretedFloat sym fi
    -> SpecialFnArg (SymExpr sym) (SymInterpretedFloatType sym fi) R
    forall {k} (e :: k -> Type) (tp :: k). e tp -> SpecialFnArg e tp R
    SpecialFnArg SymInterpretedFloat sym fi
    x)

      -- | Apply a 2-argument special function
      iFloatSpecialFunction2
        :: sym
        -> FloatInfoRepr fi
        -> SpecialFunction (EmptyCtx ::> R ::> R)
        -> SymInterpretedFloat sym fi
        -> SymInterpretedFloat sym fi
        -> IO (SymInterpretedFloat sym fi)
      iFloatSpecialFunction2 sym
    sym FloatInfoRepr fi
    fi SpecialFunction ((EmptyCtx ::> R) ::> R)
    fn SymInterpretedFloat sym fi
    x SymInterpretedFloat sym fi
    y =
        sym
    -> FloatInfoRepr fi
    -> SpecialFunction ((EmptyCtx ::> R) ::> R)
    -> Assignment
         (SpecialFnArg (SymExpr sym) (SymInterpretedFloatType sym fi))
         ((EmptyCtx ::> R) ::> R)
    -> IO (SymInterpretedFloat sym fi)
    forall sym (fi :: FloatInfo) (args :: Ctx Type).
    IsInterpretedFloatExprBuilder sym =>
    sym
    -> FloatInfoRepr fi
    -> SpecialFunction args
    -> Assignment
         (SpecialFnArg (SymExpr sym) (SymInterpretedFloatType sym fi)) args
    -> IO (SymInterpretedFloat sym fi)
    forall (fi :: FloatInfo) (args :: Ctx Type).
    sym
    -> FloatInfoRepr fi
    -> SpecialFunction args
    -> Assignment
         (SpecialFnArg (SymExpr sym) (SymInterpretedFloatType sym fi)) args
    -> IO (SymInterpretedFloat sym fi)
    iFloatSpecialFunction sym
    sym FloatInfoRepr fi
    fi SpecialFunction ((EmptyCtx ::> R) ::> R)
    fn (Assignment
      (SpecialFnArg (SymExpr sym) (SymInterpretedFloatType sym fi))
      EmptyCtx
    forall {k} (ctx :: Ctx k) (f :: k -> Type).
    (ctx ~ EmptyCtx) =>
    Assignment f ctx
    Ctx.Empty Assignment
      (SpecialFnArg (SymExpr sym) (SymInterpretedFloatType sym fi))
      EmptyCtx
    -> SpecialFnArg (SymExpr sym) (SymInterpretedFloatType sym fi) R
    -> Assignment
         (SpecialFnArg (SymExpr sym) (SymInterpretedFloatType sym fi))
         (EmptyCtx ::> R)
    forall {k} (ctx' :: Ctx k) (f :: k -> Type) (ctx :: Ctx k)
           (tp :: k).
    (ctx' ~ (ctx ::> tp)) =>
    Assignment f ctx -> f tp -> Assignment f ctx'
    Ctx.:> SymInterpretedFloat sym fi
    -> SpecialFnArg (SymExpr sym) (SymInterpretedFloatType sym fi) R
    forall {k} (e :: k -> Type) (tp :: k). e tp -> SpecialFnArg e tp R
    SpecialFnArg SymInterpretedFloat sym fi
    x Assignment
      (SpecialFnArg (SymExpr sym) (SymInterpretedFloatType sym fi))
      (EmptyCtx ::> R)
    -> SpecialFnArg (SymExpr sym) (SymInterpretedFloatType sym fi) R
    -> Assignment
         (SpecialFnArg (SymExpr sym) (SymInterpretedFloatType sym fi))
         ((EmptyCtx ::> R) ::> R)
    forall {k} (ctx' :: Ctx k) (f :: k -> Type) (ctx :: Ctx k)
           (tp :: k).
    (ctx' ~ (ctx ::> tp)) =>
    Assignment f ctx -> f tp -> Assignment f ctx'
    Ctx.:> SymInterpretedFloat sym fi
    -> SpecialFnArg (SymExpr sym) (SymInterpretedFloatType sym fi) R
    forall {k} (e :: k -> Type) (tp :: k). e tp -> SpecialFnArg e tp R
    SpecialFnArg SymInterpretedFloat sym fi
    y)

      -- | The associated BaseType representative of the floating point
      -- interpretation for each format.
      iFloatBaseTypeRepr
        :: sym
        -> FloatInfoRepr fi
        -> BaseTypeRepr (SymInterpretedFloatType sym fi)

    -- | Helper interface for creating new symbolic floating-point constants and
    --   variables.
    class (IsSymExprBuilder sym, IsInterpretedFloatExprBuilder sym) => IsInterpretedFloatSymExprBuilder sym where
      -- | Create a fresh top-level floating-point uninterpreted constant.
      freshFloatConstant
        :: sym
        -> SolverSymbol
        -> FloatInfoRepr fi
        -> IO (SymExpr sym (SymInterpretedFloatType sym fi))
      freshFloatConstant sym
    sym SolverSymbol
    nm FloatInfoRepr fi
    fi = sym
    -> SolverSymbol
    -> BaseTypeRepr (SymInterpretedFloatType sym fi)
    -> IO (SymExpr sym (SymInterpretedFloatType sym fi))
    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
    nm (BaseTypeRepr (SymInterpretedFloatType sym fi)
     -> IO (SymExpr sym (SymInterpretedFloatType sym fi)))
    -> BaseTypeRepr (SymInterpretedFloatType sym fi)
    -> IO (SymExpr sym (SymInterpretedFloatType sym fi))
    forall a b. (a -> b) -> a -> b
    $ sym
    -> FloatInfoRepr fi
    -> BaseTypeRepr (SymInterpretedFloatType sym fi)
    forall sym (fi :: FloatInfo).
    IsInterpretedFloatExprBuilder sym =>
    sym
    -> FloatInfoRepr fi
    -> BaseTypeRepr (SymInterpretedFloatType sym fi)
    forall (fi :: FloatInfo).
    sym
    -> FloatInfoRepr fi
    -> BaseTypeRepr (SymInterpretedFloatType sym fi)
    iFloatBaseTypeRepr sym
    sym FloatInfoRepr fi
    fi

      -- | Create a fresh floating-point latch variable.
      freshFloatLatch
        :: sym
        -> SolverSymbol
        -> FloatInfoRepr fi
        -> IO (SymExpr sym (SymInterpretedFloatType sym fi))
      freshFloatLatch sym
    sym SolverSymbol
    nm FloatInfoRepr fi
    fi = sym
    -> SolverSymbol
    -> BaseTypeRepr (SymInterpretedFloatType sym fi)
    -> IO (SymExpr sym (SymInterpretedFloatType sym fi))
    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)
    freshLatch sym
    sym SolverSymbol
    nm (BaseTypeRepr (SymInterpretedFloatType sym fi)
     -> IO (SymExpr sym (SymInterpretedFloatType sym fi)))
    -> BaseTypeRepr (SymInterpretedFloatType sym fi)
    -> IO (SymExpr sym (SymInterpretedFloatType sym fi))
    forall a b. (a -> b) -> a -> b
    $ sym
    -> FloatInfoRepr fi
    -> BaseTypeRepr (SymInterpretedFloatType sym fi)
    forall sym (fi :: FloatInfo).
    IsInterpretedFloatExprBuilder sym =>
    sym
    -> FloatInfoRepr fi
    -> BaseTypeRepr (SymInterpretedFloatType sym fi)
    forall (fi :: FloatInfo).
    sym
    -> FloatInfoRepr fi
    -> BaseTypeRepr (SymInterpretedFloatType sym fi)
    iFloatBaseTypeRepr sym
    sym FloatInfoRepr fi
    fi

      -- | Creates a floating-point bound variable.
      freshFloatBoundVar
        :: sym
        -> SolverSymbol
        -> FloatInfoRepr fi
        -> IO (BoundVar sym (SymInterpretedFloatType sym fi))
      freshFloatBoundVar sym
    sym SolverSymbol
    nm FloatInfoRepr fi
    fi = sym
    -> SolverSymbol
    -> BaseTypeRepr (SymInterpretedFloatType sym fi)
    -> IO (BoundVar sym (SymInterpretedFloatType sym fi))
    forall sym (tp :: BaseType).
    IsSymExprBuilder sym =>
    sym -> SolverSymbol -> BaseTypeRepr tp -> IO (BoundVar sym tp)
    forall (tp :: BaseType).
    sym -> SolverSymbol -> BaseTypeRepr tp -> IO (BoundVar sym tp)
    freshBoundVar sym
    sym SolverSymbol
    nm (BaseTypeRepr (SymInterpretedFloatType sym fi)
     -> IO (BoundVar sym (SymInterpretedFloatType sym fi)))
    -> BaseTypeRepr (SymInterpretedFloatType sym fi)
    -> IO (BoundVar sym (SymInterpretedFloatType sym fi))
    forall a b. (a -> b) -> a -> b
    $ sym
    -> FloatInfoRepr fi
    -> BaseTypeRepr (SymInterpretedFloatType sym fi)
    forall sym (fi :: FloatInfo).
    IsInterpretedFloatExprBuilder sym =>
    sym
    -> FloatInfoRepr fi
    -> BaseTypeRepr (SymInterpretedFloatType sym fi)
    forall (fi :: FloatInfo).
    sym
    -> FloatInfoRepr fi
    -> BaseTypeRepr (SymInterpretedFloatType sym fi)
    iFloatBaseTypeRepr sym
    sym FloatInfoRepr fi
    fi