{-# 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