{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
module What4.InterpretedFloatingPoint
(
type FloatInfo
, HalfFloat
, SingleFloat
, DoubleFloat
, QuadFloat
, X86_80Float
, DoubleDoubleFloat
, FloatInfoRepr(..)
, X86_80Val(..)
, fp80ToBits
, fp80ToRational
, FloatInfoToPrecision
, FloatPrecisionToInfo
, floatInfoToPrecisionRepr
, floatPrecisionToInfoRepr
, FloatInfoToBitWidth
, floatInfoToBVTypeRepr
, SymInterpretedFloatType
, SymInterpretedFloat
, 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
data FloatInfo where
HalfFloat :: FloatInfo
SingleFloat :: FloatInfo
DoubleFloat :: FloatInfo
QuadFloat :: FloatInfo
X86_80Float :: FloatInfo
DoubleDoubleFloat :: FloatInfo
type HalfFloat = 'HalfFloat
type SingleFloat = 'SingleFloat
type DoubleFloat = 'DoubleFloat
type QuadFloat = 'QuadFloat
type X86_80Float = 'X86_80Float
type DoubleDoubleFloat = 'DoubleDoubleFloat
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 = 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 = 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 = forall a. Maybe a -> Bool
isJust (forall {k} (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f 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 -> forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
FloatInfoRepr fi
SingleFloatRepr -> forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
FloatInfoRepr fi
DoubleFloatRepr -> forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
FloatInfoRepr fi
QuadFloatRepr -> forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
FloatInfoRepr fi
X86_80FloatRepr -> forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
FloatInfoRepr fi
DoubleDoubleFloatRepr -> 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 <- forall {k} (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality FloatPrecisionRepr fpp
fpp (forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr :: FloatPrecisionRepr Prec16)
= forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
| Just fpp :~: Prec32
Refl <- forall {k} (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality FloatPrecisionRepr fpp
fpp (forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr :: FloatPrecisionRepr Prec32)
= forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
| Just fpp :~: Prec64
Refl <- forall {k} (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality FloatPrecisionRepr fpp
fpp (forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr :: FloatPrecisionRepr Prec64)
= forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
| Just fpp :~: Prec80
Refl <- forall {k} (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality FloatPrecisionRepr fpp
fpp (forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr :: FloatPrecisionRepr Prec80)
= forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
| Just fpp :~: Prec128
Refl <- forall {k} (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality FloatPrecisionRepr fpp
fpp (forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr :: FloatPrecisionRepr Prec128)
= forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
| Bool
otherwise
= forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ String
"unexpected IEEE-754 precision: " forall a. [a] -> [a] -> [a]
++ 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 -> forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
FloatInfoRepr fi
SingleFloatRepr -> forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
FloatInfoRepr fi
DoubleFloatRepr -> forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
FloatInfoRepr fi
QuadFloatRepr -> forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
FloatInfoRepr fi
X86_80FloatRepr -> forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
FloatInfoRepr fi
DoubleDoubleFloatRepr -> forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
data X86_80Val = X86_80Val
Word16
Word64
deriving (Int -> X86_80Val -> ShowS
[X86_80Val] -> ShowS
X86_80Val -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [X86_80Val] -> ShowS
$cshowList :: [X86_80Val] -> ShowS
show :: X86_80Val -> String
$cshow :: X86_80Val -> String
showsPrec :: Int -> X86_80Val -> ShowS
$cshowsPrec :: Int -> X86_80Val -> ShowS
Show, X86_80Val -> X86_80Val -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: X86_80Val -> X86_80Val -> Bool
$c/= :: X86_80Val -> X86_80Val -> Bool
== :: X86_80Val -> X86_80Val -> Bool
$c== :: X86_80Val -> X86_80Val -> Bool
Eq, Eq 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
min :: X86_80Val -> X86_80Val -> X86_80Val
$cmin :: X86_80Val -> X86_80Val -> X86_80Val
max :: X86_80Val -> X86_80Val -> X86_80Val
$cmax :: X86_80Val -> X86_80Val -> X86_80Val
>= :: 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
$c< :: X86_80Val -> X86_80Val -> Bool
compare :: X86_80Val -> X86_80Val -> Ordering
$ccompare :: X86_80Val -> X86_80Val -> Ordering
Ord)
fp80ToBits :: X86_80Val -> Integer
fp80ToBits :: X86_80Val -> Integer
fp80ToBits (X86_80Val Word16
ex Word64
mantissa) =
forall a. Bits a => a -> Int -> a
shiftL (forall a. Integral a => a -> Integer
toInteger Word16
ex) Int
64 forall a. Bits a => a -> a -> a
.|. 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)
| Word16
ex' forall a. Eq a => a -> a -> Bool
== Word16
0x7FFF = forall a. Maybe a
Nothing
| Bool
otherwise = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$! (if Bool
s then forall a. Num a => a -> a
negate else forall a. a -> a
id) (Rational
m forall a. Num a => a -> a -> a
* (Integer
1 forall a. Integral a => a -> a -> Ratio a
% Integer
2forall a b. (Num a, Integral b) => a -> b -> a
^Integer
e))
where
s :: Bool
s = forall a. Bits a => a -> Int -> Bool
testBit Word16
ex Int
15
ex' :: Word16
ex' = Word16
ex forall a. Bits a => a -> a -> a
.&. Word16
0x7FFF
m :: Rational
m = (forall a. Integral a => a -> Integer
toInteger Word64
mantissa) forall a. Integral a => a -> a -> Ratio a
% ((Integer
2::Integer)forall a b. (Num a, Integral b) => a -> b -> a
^(Integer
63::Integer))
e :: Integer
e = Integer
16382 forall a. Num a => a -> a -> a
- forall a. Integral a => a -> Integer
toInteger Word16
ex'
type family SymInterpretedFloatType (sym :: Type) (fi :: FloatInfo) :: BaseType
type SymInterpretedFloat sym fi = SymExpr sym (SymInterpretedFloatType sym fi)
class IsExprBuilder sym => IsInterpretedFloatExprBuilder sym where
iFloatPZero :: sym -> FloatInfoRepr fi -> IO (SymInterpretedFloat sym fi)
iFloatNZero :: sym -> FloatInfoRepr fi -> IO (SymInterpretedFloat sym fi)
iFloatNaN :: sym -> FloatInfoRepr fi -> IO (SymInterpretedFloat sym fi)
iFloatPInf :: sym -> FloatInfoRepr fi -> IO (SymInterpretedFloat sym fi)
iFloatNInf :: sym -> FloatInfoRepr fi -> IO (SymInterpretedFloat sym fi)
iFloatLitRational
:: sym -> FloatInfoRepr fi -> Rational -> IO (SymInterpretedFloat sym fi)
iFloatLitSingle :: sym -> Float -> IO (SymInterpretedFloat sym SingleFloat)
iFloatLitDouble :: sym -> Double -> IO (SymInterpretedFloat sym DoubleFloat)
iFloatLitLongDouble :: sym -> X86_80Val -> IO (SymInterpretedFloat sym X86_80Float)
iFloatNeg
:: sym
-> SymInterpretedFloat sym fi
-> IO (SymInterpretedFloat sym fi)
iFloatAbs
:: sym
-> SymInterpretedFloat sym fi
-> IO (SymInterpretedFloat sym fi)
iFloatSqrt
:: sym
-> RoundingMode
-> SymInterpretedFloat sym fi
-> IO (SymInterpretedFloat sym fi)
iFloatAdd
:: sym
-> RoundingMode
-> SymInterpretedFloat sym fi
-> SymInterpretedFloat sym fi
-> IO (SymInterpretedFloat sym fi)
iFloatSub
:: sym
-> RoundingMode
-> SymInterpretedFloat sym fi
-> SymInterpretedFloat sym fi
-> IO (SymInterpretedFloat sym fi)
iFloatMul
:: sym
-> RoundingMode
-> SymInterpretedFloat sym fi
-> SymInterpretedFloat sym fi
-> IO (SymInterpretedFloat sym fi)
iFloatDiv
:: sym
-> RoundingMode
-> SymInterpretedFloat sym fi
-> SymInterpretedFloat sym fi
-> IO (SymInterpretedFloat sym fi)
iFloatRem
:: sym
-> SymInterpretedFloat sym fi
-> SymInterpretedFloat sym fi
-> IO (SymInterpretedFloat sym fi)
iFloatMin
:: sym
-> SymInterpretedFloat sym fi
-> SymInterpretedFloat sym fi
-> IO (SymInterpretedFloat sym fi)
iFloatMax
:: sym
-> SymInterpretedFloat sym fi
-> SymInterpretedFloat sym fi
-> IO (SymInterpretedFloat sym fi)
iFloatFMA
:: sym
-> RoundingMode
-> SymInterpretedFloat sym fi
-> SymInterpretedFloat sym fi
-> SymInterpretedFloat sym fi
-> IO (SymInterpretedFloat sym fi)
iFloatEq
:: sym
-> SymInterpretedFloat sym fi
-> SymInterpretedFloat sym fi
-> IO (Pred sym)
iFloatNe
:: sym
-> SymInterpretedFloat sym fi
-> SymInterpretedFloat sym fi
-> IO (Pred sym)
iFloatFpEq
:: sym
-> SymInterpretedFloat sym fi
-> SymInterpretedFloat sym fi
-> IO (Pred sym)
iFloatFpApart
:: sym
-> SymInterpretedFloat sym fi
-> SymInterpretedFloat sym fi
-> IO (Pred sym)
iFloatLe
:: sym
-> SymInterpretedFloat sym fi
-> SymInterpretedFloat sym fi
-> IO (Pred sym)
iFloatLt
:: sym
-> SymInterpretedFloat sym fi
-> SymInterpretedFloat sym fi
-> IO (Pred sym)
iFloatGe
:: sym
-> SymInterpretedFloat sym fi
-> SymInterpretedFloat sym fi
-> IO (Pred sym)
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)
iFloatIte
:: sym
-> Pred sym
-> SymInterpretedFloat sym fi
-> SymInterpretedFloat sym fi
-> IO (SymInterpretedFloat sym fi)
iFloatCast
:: sym
-> FloatInfoRepr fi
-> RoundingMode
-> SymInterpretedFloat sym fi'
-> IO (SymInterpretedFloat sym fi)
iFloatRound
:: sym
-> RoundingMode
-> SymInterpretedFloat sym fi
-> IO (SymInterpretedFloat sym fi)
iFloatFromBinary
:: sym
-> FloatInfoRepr fi
-> SymBV sym (FloatInfoToBitWidth fi)
-> IO (SymInterpretedFloat sym fi)
iFloatToBinary
:: sym
-> FloatInfoRepr fi
-> SymInterpretedFloat sym fi
-> IO (SymBV sym (FloatInfoToBitWidth fi))
iBVToFloat
:: (1 <= w)
=> sym
-> FloatInfoRepr fi
-> RoundingMode
-> SymBV sym w
-> IO (SymInterpretedFloat sym fi)
iSBVToFloat
:: (1 <= w) => sym
-> FloatInfoRepr fi
-> RoundingMode
-> SymBV sym w
-> IO (SymInterpretedFloat sym fi)
iRealToFloat
:: sym
-> FloatInfoRepr fi
-> RoundingMode
-> SymReal sym
-> IO (SymInterpretedFloat sym fi)
iFloatToBV
:: (1 <= w)
=> sym
-> NatRepr w
-> RoundingMode
-> SymInterpretedFloat sym fi
-> IO (SymBV sym w)
iFloatToSBV
:: (1 <= w)
=> sym
-> NatRepr w
-> RoundingMode
-> SymInterpretedFloat sym fi
-> IO (SymBV sym w)
iFloatToReal :: sym -> SymInterpretedFloat sym fi -> IO (SymReal sym)
iFloatSpecialFunction
:: sym
-> FloatInfoRepr fi
-> SpecialFunction args
-> Assignment (SpecialFnArg (SymExpr sym) (SymInterpretedFloatType sym fi)) args
-> IO (SymInterpretedFloat sym fi)
iFloatSpecialFunction0
:: sym
-> FloatInfoRepr fi
-> SpecialFunction EmptyCtx
-> IO (SymInterpretedFloat sym fi)
iFloatSpecialFunction0 sym
sym FloatInfoRepr fi
fi SpecialFunction EmptyCtx
fn =
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)
iFloatSpecialFunction sym
sym FloatInfoRepr fi
fi SpecialFunction EmptyCtx
fn forall {k} (ctx :: Ctx k) (f :: k -> Type).
(ctx ~ EmptyCtx) =>
Assignment f ctx
Ctx.Empty
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 =
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)
iFloatSpecialFunction sym
sym FloatInfoRepr fi
fi SpecialFunction (EmptyCtx ::> R)
fn (forall {k} (ctx :: Ctx k) (f :: k -> Type).
(ctx ~ EmptyCtx) =>
Assignment f ctx
Ctx.Empty 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.:> forall {k} (e :: k -> Type) (tp :: k). e tp -> SpecialFnArg e tp R
SpecialFnArg SymInterpretedFloat sym fi
x)
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 =
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)
iFloatSpecialFunction sym
sym FloatInfoRepr fi
fi SpecialFunction ((EmptyCtx ::> R) ::> R)
fn (forall {k} (ctx :: Ctx k) (f :: k -> Type).
(ctx ~ EmptyCtx) =>
Assignment f ctx
Ctx.Empty 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.:> forall {k} (e :: k -> Type) (tp :: k). e tp -> SpecialFnArg e tp R
SpecialFnArg SymInterpretedFloat sym fi
x 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.:> forall {k} (e :: k -> Type) (tp :: k). e tp -> SpecialFnArg e tp R
SpecialFnArg SymInterpretedFloat sym fi
y)
iFloatBaseTypeRepr
:: sym
-> FloatInfoRepr fi
-> BaseTypeRepr (SymInterpretedFloatType sym fi)
class (IsSymExprBuilder sym, IsInterpretedFloatExprBuilder sym) => IsInterpretedFloatSymExprBuilder sym where
freshFloatConstant
:: sym
-> SolverSymbol
-> FloatInfoRepr fi
-> IO (SymExpr sym (SymInterpretedFloatType sym fi))
freshFloatConstant sym
sym SolverSymbol
nm FloatInfoRepr fi
fi = forall sym (tp :: BaseType).
IsSymExprBuilder sym =>
sym -> SolverSymbol -> BaseTypeRepr tp -> IO (SymExpr sym tp)
freshConstant sym
sym SolverSymbol
nm forall a b. (a -> b) -> a -> b
$ forall sym (fi :: FloatInfo).
IsInterpretedFloatExprBuilder sym =>
sym
-> FloatInfoRepr fi
-> BaseTypeRepr (SymInterpretedFloatType sym fi)
iFloatBaseTypeRepr sym
sym FloatInfoRepr fi
fi
freshFloatLatch
:: sym
-> SolverSymbol
-> FloatInfoRepr fi
-> IO (SymExpr sym (SymInterpretedFloatType sym fi))
freshFloatLatch sym
sym SolverSymbol
nm FloatInfoRepr fi
fi = forall sym (tp :: BaseType).
IsSymExprBuilder sym =>
sym -> SolverSymbol -> BaseTypeRepr tp -> IO (SymExpr sym tp)
freshLatch sym
sym SolverSymbol
nm forall a b. (a -> b) -> a -> b
$ forall sym (fi :: FloatInfo).
IsInterpretedFloatExprBuilder sym =>
sym
-> FloatInfoRepr fi
-> BaseTypeRepr (SymInterpretedFloatType sym fi)
iFloatBaseTypeRepr sym
sym FloatInfoRepr fi
fi
freshFloatBoundVar
:: sym
-> SolverSymbol
-> FloatInfoRepr fi
-> IO (BoundVar sym (SymInterpretedFloatType sym fi))
freshFloatBoundVar sym
sym SolverSymbol
nm FloatInfoRepr fi
fi = forall sym (tp :: BaseType).
IsSymExprBuilder sym =>
sym -> SolverSymbol -> BaseTypeRepr tp -> IO (BoundVar sym tp)
freshBoundVar sym
sym SolverSymbol
nm forall a b. (a -> b) -> a -> b
$ forall sym (fi :: FloatInfo).
IsInterpretedFloatExprBuilder sym =>
sym
-> FloatInfoRepr fi
-> BaseTypeRepr (SymInterpretedFloatType sym fi)
iFloatBaseTypeRepr sym
sym FloatInfoRepr fi
fi