{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE BlockArguments #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE NamedFieldPuns #-}
{-# LANGUAGE PatternGuards #-}
{-# LANGUAGE Rank2Types #-}
{-# LANGUAGE RecordWildCards #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TupleSections #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE ViewPatterns #-}
module Cryptol.Backend.Concrete
( BV(..)
, binBV
, unaryBV
, bvVal
, ppBV
, mkBv
, mask
, signedBV
, signedValue
, integerToChar
, lg2
, Concrete(..)
, liftBinIntMod
, fpBinArith
, fpRoundMode
) where
import qualified Control.Exception as X
import Data.Bits
import Data.Ratio
import Numeric (showIntAtBase)
import qualified LibBF as FP
import qualified GHC.Num.Compat as Integer
import qualified Cryptol.Backend.Arch as Arch
import qualified Cryptol.Backend.FloatHelpers as FP
import Cryptol.Backend
import Cryptol.Backend.Monad
import Cryptol.TypeCheck.Solver.InfNat (genLog)
import Cryptol.Utils.Panic (panic)
import Cryptol.Utils.PP
data Concrete = Concrete deriving Int -> Concrete -> ShowS
[Concrete] -> ShowS
Concrete -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Concrete] -> ShowS
$cshowList :: [Concrete] -> ShowS
show :: Concrete -> String
$cshow :: Concrete -> String
showsPrec :: Int -> Concrete -> ShowS
$cshowsPrec :: Int -> Concrete -> ShowS
Show
data BV = BV !Integer !Integer
instance Show BV where
show :: BV -> String
show = forall a. Show a => a -> String
show forall b c a. (b -> c) -> (a -> b) -> a -> c
. BV -> Integer
bvVal
binBV :: Applicative m => (Integer -> Integer -> Integer) -> BV -> BV -> m BV
binBV :: forall (m :: * -> *).
Applicative m =>
(Integer -> Integer -> Integer) -> BV -> BV -> m BV
binBV Integer -> Integer -> Integer
f (BV Integer
w Integer
x) (BV Integer
_ Integer
y) = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$! Integer -> Integer -> BV
mkBv Integer
w (Integer -> Integer -> Integer
f Integer
x Integer
y)
{-# INLINE binBV #-}
unaryBV :: (Integer -> Integer) -> BV -> BV
unaryBV :: (Integer -> Integer) -> BV -> BV
unaryBV Integer -> Integer
f (BV Integer
w Integer
x) = Integer -> Integer -> BV
mkBv Integer
w forall a b. (a -> b) -> a -> b
$! Integer -> Integer
f Integer
x
{-# INLINE unaryBV #-}
bvVal :: BV -> Integer
bvVal :: BV -> Integer
bvVal (BV Integer
_w Integer
x) = Integer
x
{-# INLINE bvVal #-}
mkBv :: Integer -> Integer -> BV
mkBv :: Integer -> Integer -> BV
mkBv Integer
w Integer
i = Integer -> Integer -> BV
BV Integer
w (Integer -> Integer -> Integer
mask Integer
w Integer
i)
signedBV :: BV -> Integer
signedBV :: BV -> Integer
signedBV (BV Integer
i Integer
x) = Integer -> Integer -> Integer
signedValue Integer
i Integer
x
signedValue :: Integer -> Integer -> Integer
signedValue :: Integer -> Integer -> Integer
signedValue Integer
i Integer
x = if forall a. Bits a => a -> Int -> Bool
testBit Integer
x (forall a. Num a => Integer -> a
fromInteger (Integer
iforall a. Num a => a -> a -> a
-Integer
1)) then Integer
x forall a. Num a => a -> a -> a
- (forall a. Bits a => Int -> a
bit (forall a. Num a => Integer -> a
fromInteger Integer
i)) else Integer
x
integerToChar :: Integer -> Char
integerToChar :: Integer -> Char
integerToChar = forall a. Enum a => Int -> a
toEnum forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Num a => Integer -> a
fromInteger
lg2 :: Integer -> Integer
lg2 :: Integer -> Integer
lg2 Integer
i = case Integer -> Integer -> Maybe (Integer, Bool)
genLog Integer
i Integer
2 of
Just (Integer
i',Bool
isExact) | Bool
isExact -> Integer
i'
| Bool
otherwise -> Integer
i' forall a. Num a => a -> a -> a
+ Integer
1
Maybe (Integer, Bool)
Nothing -> Integer
0
ppBV :: PPOpts -> BV -> Doc
ppBV :: PPOpts -> BV -> Doc
ppBV PPOpts
opts (BV Integer
width Integer
i)
| Int
base forall a. Ord a => a -> a -> Bool
> Int
36 = Integer -> Doc
integer Integer
i
| PPOpts -> Integer -> Bool
asciiMode PPOpts
opts Integer
width = String -> Doc
text (forall a. Show a => a -> String
show (forall a. Enum a => Int -> a
toEnum (forall a. Num a => Integer -> a
fromInteger Integer
i) :: Char))
| Bool
otherwise = Doc
prefix Doc -> Doc -> Doc
<.> String -> Doc
text String
value
where
base :: Int
base = PPOpts -> Int
useBase PPOpts
opts
padding :: Int -> Doc
padding Int
bitsPerDigit = String -> Doc
text (forall a. Int -> a -> [a]
replicate Int
padLen Char
'0')
where
padLen :: Int
padLen | Int
m forall a. Ord a => a -> a -> Bool
> Int
0 = Int
d forall a. Num a => a -> a -> a
+ Int
1
| Bool
otherwise = Int
d
(Int
d,Int
m) = (forall a. Num a => Integer -> a
fromInteger Integer
width forall a. Num a => a -> a -> a
- (forall (t :: * -> *) a. Foldable t => t a -> Int
length String
value forall a. Num a => a -> a -> a
* Int
bitsPerDigit))
forall a. Integral a => a -> a -> (a, a)
`divMod` Int
bitsPerDigit
prefix :: Doc
prefix = case Int
base of
Int
2 -> String -> Doc
text String
"0b" Doc -> Doc -> Doc
<.> Int -> Doc
padding Int
1
Int
8 -> String -> Doc
text String
"0o" Doc -> Doc -> Doc
<.> Int -> Doc
padding Int
3
Int
10 -> forall a. Monoid a => a
mempty
Int
16 -> String -> Doc
text String
"0x" Doc -> Doc -> Doc
<.> Int -> Doc
padding Int
4
Int
_ -> String -> Doc
text String
"0" Doc -> Doc -> Doc
<.> Char -> Doc
char Char
'<' Doc -> Doc -> Doc
<.> Int -> Doc
int Int
base Doc -> Doc -> Doc
<.> Char -> Doc
char Char
'>'
value :: String
value = forall a. (Integral a, Show a) => a -> (Int -> Char) -> a -> ShowS
showIntAtBase (forall a. Integral a => a -> Integer
toInteger Int
base) (String
digits forall a. [a] -> Int -> a
!!) Integer
i String
""
digits :: String
digits = String
"0123456789abcdefghijklmnopqrstuvwxyz"
mask ::
Integer ->
Integer ->
Integer
mask :: Integer -> Integer -> Integer
mask Integer
w Integer
i | Integer
w forall a. Ord a => a -> a -> Bool
>= Integer
Arch.maxBigIntWidth = forall a. Integer -> a
wordTooWide Integer
w
| Bool
otherwise = Integer
i forall a. Bits a => a -> a -> a
.&. (forall a. Bits a => Int -> a
bit (forall a. Num a => Integer -> a
fromInteger Integer
w) forall a. Num a => a -> a -> a
- Integer
1)
instance Backend Concrete where
type SBit Concrete = Bool
type SWord Concrete = BV
type SInteger Concrete = Integer
type SFloat Concrete = FP.BF
type SEval Concrete = Eval
raiseError :: forall a. Concrete -> EvalError -> SEval Concrete a
raiseError Concrete
_ EvalError
err =
do CallStack
stk <- Eval CallStack
getCallStack
forall a. IO a -> Eval a
io (forall e a. Exception e => e -> IO a
X.throwIO (CallStack -> EvalError -> EvalErrorEx
EvalErrorEx CallStack
stk EvalError
err))
assertSideCondition :: Concrete -> SBit Concrete -> EvalError -> SEval Concrete ()
assertSideCondition Concrete
_ Bool
SBit Concrete
True EvalError
_ = forall (m :: * -> *) a. Monad m => a -> m a
return ()
assertSideCondition Concrete
sym Bool
SBit Concrete
False EvalError
err = forall sym a. Backend sym => sym -> EvalError -> SEval sym a
raiseError Concrete
sym EvalError
err
wordLen :: Concrete -> SWord Concrete -> Integer
wordLen Concrete
_ (BV Integer
w Integer
_) = Integer
w
wordAsChar :: Concrete -> SWord Concrete -> Maybe Char
wordAsChar Concrete
_ (BV Integer
_ Integer
x) = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$! Integer -> Char
integerToChar Integer
x
wordBit :: Concrete
-> SWord Concrete -> Integer -> SEval Concrete (SBit Concrete)
wordBit Concrete
_ (BV Integer
w Integer
x) Integer
idx = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$! forall a. Bits a => a -> Int -> Bool
testBit Integer
x (forall a. Num a => Integer -> a
fromInteger (Integer
w forall a. Num a => a -> a -> a
- Integer
1 forall a. Num a => a -> a -> a
- Integer
idx))
wordUpdate :: Concrete
-> SWord Concrete
-> Integer
-> SBit Concrete
-> SEval Concrete (SWord Concrete)
wordUpdate Concrete
_ (BV Integer
w Integer
x) Integer
idx Bool
SBit Concrete
True = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$! Integer -> Integer -> BV
BV Integer
w (forall a. Bits a => a -> Int -> a
setBit Integer
x (forall a. Num a => Integer -> a
fromInteger (Integer
w forall a. Num a => a -> a -> a
- Integer
1 forall a. Num a => a -> a -> a
- Integer
idx)))
wordUpdate Concrete
_ (BV Integer
w Integer
x) Integer
idx Bool
SBit Concrete
False = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$! Integer -> Integer -> BV
BV Integer
w (forall a. Bits a => a -> Int -> a
clearBit Integer
x (forall a. Num a => Integer -> a
fromInteger (Integer
w forall a. Num a => a -> a -> a
- Integer
1 forall a. Num a => a -> a -> a
- Integer
idx)))
isReady :: forall a. Concrete -> SEval Concrete a -> SEval Concrete (Maybe a)
isReady Concrete
_ = forall a. Eval a -> Eval (Maybe a)
maybeReady
mergeEval :: forall a.
Concrete
-> (SBit Concrete -> a -> a -> SEval Concrete a)
-> SBit Concrete
-> SEval Concrete a
-> SEval Concrete a
-> SEval Concrete a
mergeEval Concrete
_sym SBit Concrete -> a -> a -> SEval Concrete a
f SBit Concrete
c SEval Concrete a
mx SEval Concrete a
my =
do a
x <- SEval Concrete a
mx
a
y <- SEval Concrete a
my
SBit Concrete -> a -> a -> SEval Concrete a
f SBit Concrete
c a
x a
y
sDeclareHole :: forall a.
Concrete
-> String
-> SEval
Concrete (SEval Concrete a, SEval Concrete a -> SEval Concrete ())
sDeclareHole Concrete
_ = forall a. String -> Eval (Eval a, Eval a -> Eval ())
blackhole
sDelayFill :: forall a.
Concrete
-> SEval Concrete a
-> Maybe (SEval Concrete a)
-> String
-> SEval Concrete (SEval Concrete a)
sDelayFill Concrete
_ = forall a. Eval a -> Maybe (Eval a) -> String -> Eval (Eval a)
delayFill
sSpark :: forall a.
Concrete -> SEval Concrete a -> SEval Concrete (SEval Concrete a)
sSpark Concrete
_ = forall a. Eval a -> Eval (Eval a)
evalSpark
sModifyCallStack :: forall a.
Concrete
-> (CallStack -> CallStack) -> SEval Concrete a -> SEval Concrete a
sModifyCallStack Concrete
_ CallStack -> CallStack
f SEval Concrete a
m = forall a. (CallStack -> CallStack) -> Eval a -> Eval a
modifyCallStack CallStack -> CallStack
f SEval Concrete a
m
sGetCallStack :: Concrete -> SEval Concrete CallStack
sGetCallStack Concrete
_ = Eval CallStack
getCallStack
bitLit :: Concrete -> Bool -> SBit Concrete
bitLit Concrete
_ Bool
b = Bool
b
bitAsLit :: Concrete -> SBit Concrete -> Maybe Bool
bitAsLit Concrete
_ SBit Concrete
b = forall a. a -> Maybe a
Just SBit Concrete
b
bitEq :: Concrete
-> SBit Concrete -> SBit Concrete -> SEval Concrete (SBit Concrete)
bitEq Concrete
_ SBit Concrete
x SBit Concrete
y = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$! SBit Concrete
x forall a. Eq a => a -> a -> Bool
== SBit Concrete
y
bitOr :: Concrete
-> SBit Concrete -> SBit Concrete -> SEval Concrete (SBit Concrete)
bitOr Concrete
_ SBit Concrete
x SBit Concrete
y = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$! SBit Concrete
x forall a. Bits a => a -> a -> a
.|. SBit Concrete
y
bitAnd :: Concrete
-> SBit Concrete -> SBit Concrete -> SEval Concrete (SBit Concrete)
bitAnd Concrete
_ SBit Concrete
x SBit Concrete
y = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$! SBit Concrete
x forall a. Bits a => a -> a -> a
.&. SBit Concrete
y
bitXor :: Concrete
-> SBit Concrete -> SBit Concrete -> SEval Concrete (SBit Concrete)
bitXor Concrete
_ SBit Concrete
x SBit Concrete
y = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$! SBit Concrete
x forall a. Bits a => a -> a -> a
`xor` SBit Concrete
y
bitComplement :: Concrete -> SBit Concrete -> SEval Concrete (SBit Concrete)
bitComplement Concrete
_ SBit Concrete
x = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$! forall a. Bits a => a -> a
complement SBit Concrete
x
iteBit :: Concrete
-> SBit Concrete
-> SBit Concrete
-> SBit Concrete
-> SEval Concrete (SBit Concrete)
iteBit Concrete
_ SBit Concrete
b SBit Concrete
x SBit Concrete
y = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$! if SBit Concrete
b then SBit Concrete
x else SBit Concrete
y
iteWord :: Concrete
-> SBit Concrete
-> SWord Concrete
-> SWord Concrete
-> SEval Concrete (SWord Concrete)
iteWord Concrete
_ SBit Concrete
b SWord Concrete
x SWord Concrete
y = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$! if SBit Concrete
b then SWord Concrete
x else SWord Concrete
y
iteInteger :: Concrete
-> SBit Concrete
-> SInteger Concrete
-> SInteger Concrete
-> SEval Concrete (SInteger Concrete)
iteInteger Concrete
_ SBit Concrete
b SInteger Concrete
x SInteger Concrete
y = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$! if SBit Concrete
b then SInteger Concrete
x else SInteger Concrete
y
iteFloat :: Concrete
-> SBit Concrete
-> SFloat Concrete
-> SFloat Concrete
-> SEval Concrete (SFloat Concrete)
iteFloat Concrete
_ SBit Concrete
b SFloat Concrete
x SFloat Concrete
y = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$! if SBit Concrete
b then SFloat Concrete
x else SFloat Concrete
y
wordLit :: Concrete -> Integer -> Integer -> SEval Concrete (SWord Concrete)
wordLit Concrete
_ Integer
w Integer
i = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$! Integer -> Integer -> BV
mkBv Integer
w Integer
i
wordAsLit :: Concrete -> SWord Concrete -> Maybe (Integer, Integer)
wordAsLit Concrete
_ (BV Integer
w Integer
i) = forall a. a -> Maybe a
Just (Integer
w,Integer
i)
integerLit :: Concrete -> Integer -> SEval Concrete (SInteger Concrete)
integerLit Concrete
_ Integer
i = forall (f :: * -> *) a. Applicative f => a -> f a
pure Integer
i
integerAsLit :: Concrete -> SInteger Concrete -> Maybe Integer
integerAsLit Concrete
_ = forall a. a -> Maybe a
Just
wordToInt :: Concrete -> SWord Concrete -> SEval Concrete (SInteger Concrete)
wordToInt Concrete
_ (BV Integer
_ Integer
x) = forall (f :: * -> *) a. Applicative f => a -> f a
pure Integer
x
wordToSignedInt :: Concrete -> SWord Concrete -> SEval Concrete (SInteger Concrete)
wordToSignedInt Concrete
_ (BV Integer
w Integer
x) = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$! Integer -> Integer -> Integer
signedValue Integer
w Integer
x
wordFromInt :: Concrete
-> Integer -> SInteger Concrete -> SEval Concrete (SWord Concrete)
wordFromInt Concrete
_ Integer
w SInteger Concrete
x = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$! Integer -> Integer -> BV
mkBv Integer
w SInteger Concrete
x
packWord :: Concrete -> [SBit Concrete] -> SEval Concrete (SWord Concrete)
packWord Concrete
_ [SBit Concrete]
bits = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$! Integer -> Integer -> BV
BV (forall a. Integral a => a -> Integer
toInteger Int
w) Integer
a
where
w :: Int
w = case forall (t :: * -> *) a. Foldable t => t a -> Int
length [SBit Concrete]
bits of
Int
len | forall a. Integral a => a -> Integer
toInteger Int
len forall a. Ord a => a -> a -> Bool
>= Integer
Arch.maxBigIntWidth -> forall a. Integer -> a
wordTooWide (forall a. Integral a => a -> Integer
toInteger Int
len)
| Bool
otherwise -> Int
len
a :: Integer
a = forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl forall {a}. Bits a => a -> (Int, Bool) -> a
setb Integer
0 (forall a b. [a] -> [b] -> [(a, b)]
zip [Int
w forall a. Num a => a -> a -> a
- Int
1, Int
w forall a. Num a => a -> a -> a
- Int
2 .. Int
0] [SBit Concrete]
bits)
setb :: a -> (Int, Bool) -> a
setb a
acc (Int
n,Bool
b) | Bool
b = forall a. Bits a => a -> Int -> a
setBit a
acc Int
n
| Bool
otherwise = a
acc
unpackWord :: Concrete -> SWord Concrete -> SEval Concrete [SBit Concrete]
unpackWord Concrete
_ (BV Integer
w Integer
a) = forall (f :: * -> *) a. Applicative f => a -> f a
pure [ forall a. Bits a => a -> Int -> Bool
testBit Integer
a Int
n | Int
n <- [Int
w' forall a. Num a => a -> a -> a
- Int
1, Int
w' forall a. Num a => a -> a -> a
- Int
2 .. Int
0] ]
where
w' :: Int
w' = forall a. Num a => Integer -> a
fromInteger Integer
w
joinWord :: Concrete
-> SWord Concrete
-> SWord Concrete
-> SEval Concrete (SWord Concrete)
joinWord Concrete
_ (BV Integer
i Integer
x) (BV Integer
j Integer
y) =
forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$! Integer -> Integer -> BV
BV (Integer
i forall a. Num a => a -> a -> a
+ Integer
j) (forall a. Bits a => a -> Int -> a
shiftL Integer
x (forall a. Num a => Integer -> a
fromInteger Integer
j) forall a. Num a => a -> a -> a
+ Integer
y)
splitWord :: Concrete
-> Integer
-> Integer
-> SWord Concrete
-> SEval Concrete (SWord Concrete, SWord Concrete)
splitWord Concrete
_ Integer
leftW Integer
rightW (BV Integer
_ Integer
x) =
forall (f :: * -> *) a. Applicative f => a -> f a
pure ( Integer -> Integer -> BV
BV Integer
leftW (Integer
x forall a. Bits a => a -> Int -> a
`shiftR` (forall a. Num a => Integer -> a
fromInteger Integer
rightW)), Integer -> Integer -> BV
mkBv Integer
rightW Integer
x )
extractWord :: Concrete
-> Integer
-> Integer
-> SWord Concrete
-> SEval Concrete (SWord Concrete)
extractWord Concrete
_ Integer
n Integer
i (BV Integer
_ Integer
x) = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$! Integer -> Integer -> BV
mkBv Integer
n (Integer
x forall a. Bits a => a -> Int -> a
`shiftR` (forall a. Num a => Integer -> a
fromInteger Integer
i))
wordEq :: Concrete
-> SWord Concrete
-> SWord Concrete
-> SEval Concrete (SBit Concrete)
wordEq Concrete
_ (BV Integer
i Integer
x) (BV Integer
j Integer
y)
| Integer
i forall a. Eq a => a -> a -> Bool
== Integer
j = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$! Integer
x forall a. Eq a => a -> a -> Bool
== Integer
y
| Bool
otherwise = forall a. HasCallStack => String -> [String] -> a
panic String
"Attempt to compare words of different sizes: wordEq" [forall a. Show a => a -> String
show Integer
i, forall a. Show a => a -> String
show Integer
j]
wordSignedLessThan :: Concrete
-> SWord Concrete
-> SWord Concrete
-> SEval Concrete (SBit Concrete)
wordSignedLessThan Concrete
_ (BV Integer
i Integer
x) (BV Integer
j Integer
y)
| Integer
i forall a. Eq a => a -> a -> Bool
== Integer
j = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$! Integer -> Integer -> Integer
signedValue Integer
i Integer
x forall a. Ord a => a -> a -> Bool
< Integer -> Integer -> Integer
signedValue Integer
i Integer
y
| Bool
otherwise = forall a. HasCallStack => String -> [String] -> a
panic String
"Attempt to compare words of different sizes: wordSignedLessThan" [forall a. Show a => a -> String
show Integer
i, forall a. Show a => a -> String
show Integer
j]
wordLessThan :: Concrete
-> SWord Concrete
-> SWord Concrete
-> SEval Concrete (SBit Concrete)
wordLessThan Concrete
_ (BV Integer
i Integer
x) (BV Integer
j Integer
y)
| Integer
i forall a. Eq a => a -> a -> Bool
== Integer
j = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$! Integer
x forall a. Ord a => a -> a -> Bool
< Integer
y
| Bool
otherwise = forall a. HasCallStack => String -> [String] -> a
panic String
"Attempt to compare words of different sizes: wordLessThan" [forall a. Show a => a -> String
show Integer
i, forall a. Show a => a -> String
show Integer
j]
wordGreaterThan :: Concrete
-> SWord Concrete
-> SWord Concrete
-> SEval Concrete (SBit Concrete)
wordGreaterThan Concrete
_ (BV Integer
i Integer
x) (BV Integer
j Integer
y)
| Integer
i forall a. Eq a => a -> a -> Bool
== Integer
j = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$! Integer
x forall a. Ord a => a -> a -> Bool
> Integer
y
| Bool
otherwise = forall a. HasCallStack => String -> [String] -> a
panic String
"Attempt to compare words of different sizes: wordGreaterThan" [forall a. Show a => a -> String
show Integer
i, forall a. Show a => a -> String
show Integer
j]
wordAnd :: Concrete
-> SWord Concrete
-> SWord Concrete
-> SEval Concrete (SWord Concrete)
wordAnd Concrete
_ (BV Integer
i Integer
x) (BV Integer
j Integer
y)
| Integer
i forall a. Eq a => a -> a -> Bool
== Integer
j = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$! Integer -> Integer -> BV
mkBv Integer
i (Integer
x forall a. Bits a => a -> a -> a
.&. Integer
y)
| Bool
otherwise = forall a. HasCallStack => String -> [String] -> a
panic String
"Attempt to AND words of different sizes: wordPlus" [forall a. Show a => a -> String
show Integer
i, forall a. Show a => a -> String
show Integer
j]
wordOr :: Concrete
-> SWord Concrete
-> SWord Concrete
-> SEval Concrete (SWord Concrete)
wordOr Concrete
_ (BV Integer
i Integer
x) (BV Integer
j Integer
y)
| Integer
i forall a. Eq a => a -> a -> Bool
== Integer
j = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$! Integer -> Integer -> BV
mkBv Integer
i (Integer
x forall a. Bits a => a -> a -> a
.|. Integer
y)
| Bool
otherwise = forall a. HasCallStack => String -> [String] -> a
panic String
"Attempt to OR words of different sizes: wordPlus" [forall a. Show a => a -> String
show Integer
i, forall a. Show a => a -> String
show Integer
j]
wordXor :: Concrete
-> SWord Concrete
-> SWord Concrete
-> SEval Concrete (SWord Concrete)
wordXor Concrete
_ (BV Integer
i Integer
x) (BV Integer
j Integer
y)
| Integer
i forall a. Eq a => a -> a -> Bool
== Integer
j = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$! Integer -> Integer -> BV
mkBv Integer
i (Integer
x forall a. Bits a => a -> a -> a
`xor` Integer
y)
| Bool
otherwise = forall a. HasCallStack => String -> [String] -> a
panic String
"Attempt to XOR words of different sizes: wordPlus" [forall a. Show a => a -> String
show Integer
i, forall a. Show a => a -> String
show Integer
j]
wordComplement :: Concrete -> SWord Concrete -> SEval Concrete (SWord Concrete)
wordComplement Concrete
_ (BV Integer
i Integer
x) = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$! Integer -> Integer -> BV
mkBv Integer
i (forall a. Bits a => a -> a
complement Integer
x)
wordPlus :: Concrete
-> SWord Concrete
-> SWord Concrete
-> SEval Concrete (SWord Concrete)
wordPlus Concrete
_ (BV Integer
i Integer
x) (BV Integer
j Integer
y)
| Integer
i forall a. Eq a => a -> a -> Bool
== Integer
j = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$! Integer -> Integer -> BV
mkBv Integer
i (Integer
xforall a. Num a => a -> a -> a
+Integer
y)
| Bool
otherwise = forall a. HasCallStack => String -> [String] -> a
panic String
"Attempt to add words of different sizes: wordPlus" [forall a. Show a => a -> String
show Integer
i, forall a. Show a => a -> String
show Integer
j]
wordNegate :: Concrete -> SWord Concrete -> SEval Concrete (SWord Concrete)
wordNegate Concrete
_ (BV Integer
i Integer
x) = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$! Integer -> Integer -> BV
mkBv Integer
i (forall a. Num a => a -> a
negate Integer
x)
wordMinus :: Concrete
-> SWord Concrete
-> SWord Concrete
-> SEval Concrete (SWord Concrete)
wordMinus Concrete
_ (BV Integer
i Integer
x) (BV Integer
j Integer
y)
| Integer
i forall a. Eq a => a -> a -> Bool
== Integer
j = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$! Integer -> Integer -> BV
mkBv Integer
i (Integer
xforall a. Num a => a -> a -> a
-Integer
y)
| Bool
otherwise = forall a. HasCallStack => String -> [String] -> a
panic String
"Attempt to subtract words of different sizes: wordMinus" [forall a. Show a => a -> String
show Integer
i, forall a. Show a => a -> String
show Integer
j]
wordMult :: Concrete
-> SWord Concrete
-> SWord Concrete
-> SEval Concrete (SWord Concrete)
wordMult Concrete
_ (BV Integer
i Integer
x) (BV Integer
j Integer
y)
| Integer
i forall a. Eq a => a -> a -> Bool
== Integer
j = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$! Integer -> Integer -> BV
mkBv Integer
i (Integer
xforall a. Num a => a -> a -> a
*Integer
y)
| Bool
otherwise = forall a. HasCallStack => String -> [String] -> a
panic String
"Attempt to multiply words of different sizes: wordMult" [forall a. Show a => a -> String
show Integer
i, forall a. Show a => a -> String
show Integer
j]
wordDiv :: Concrete
-> SWord Concrete
-> SWord Concrete
-> SEval Concrete (SWord Concrete)
wordDiv Concrete
sym (BV Integer
i Integer
x) (BV Integer
j Integer
y)
| Integer
i forall a. Eq a => a -> a -> Bool
== Integer
0 Bool -> Bool -> Bool
&& Integer
j forall a. Eq a => a -> a -> Bool
== Integer
0 = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$! Integer -> Integer -> BV
mkBv Integer
0 Integer
0
| Integer
i forall a. Eq a => a -> a -> Bool
== Integer
j =
do forall sym.
Backend sym =>
sym -> SBit sym -> EvalError -> SEval sym ()
assertSideCondition Concrete
sym (Integer
y forall a. Eq a => a -> a -> Bool
/= Integer
0) EvalError
DivideByZero
forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$! Integer -> Integer -> BV
mkBv Integer
i (Integer
x forall a. Integral a => a -> a -> a
`div` Integer
y)
| Bool
otherwise = forall a. HasCallStack => String -> [String] -> a
panic String
"Attempt to divide words of different sizes: wordDiv" [forall a. Show a => a -> String
show Integer
i, forall a. Show a => a -> String
show Integer
j]
wordMod :: Concrete
-> SWord Concrete
-> SWord Concrete
-> SEval Concrete (SWord Concrete)
wordMod Concrete
sym (BV Integer
i Integer
x) (BV Integer
j Integer
y)
| Integer
i forall a. Eq a => a -> a -> Bool
== Integer
0 Bool -> Bool -> Bool
&& Integer
j forall a. Eq a => a -> a -> Bool
== Integer
0 = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$! Integer -> Integer -> BV
mkBv Integer
0 Integer
0
| Integer
i forall a. Eq a => a -> a -> Bool
== Integer
j =
do forall sym.
Backend sym =>
sym -> SBit sym -> EvalError -> SEval sym ()
assertSideCondition Concrete
sym (Integer
y forall a. Eq a => a -> a -> Bool
/= Integer
0) EvalError
DivideByZero
forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$! Integer -> Integer -> BV
mkBv Integer
i (Integer
x forall a. Integral a => a -> a -> a
`mod` Integer
y)
| Bool
otherwise = forall a. HasCallStack => String -> [String] -> a
panic String
"Attempt to mod words of different sizes: wordMod" [forall a. Show a => a -> String
show Integer
i, forall a. Show a => a -> String
show Integer
j]
wordSignedDiv :: Concrete
-> SWord Concrete
-> SWord Concrete
-> SEval Concrete (SWord Concrete)
wordSignedDiv Concrete
sym (BV Integer
i Integer
x) (BV Integer
j Integer
y)
| Integer
i forall a. Eq a => a -> a -> Bool
== Integer
0 Bool -> Bool -> Bool
&& Integer
j forall a. Eq a => a -> a -> Bool
== Integer
0 = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$! Integer -> Integer -> BV
mkBv Integer
0 Integer
0
| Integer
i forall a. Eq a => a -> a -> Bool
== Integer
j =
do forall sym.
Backend sym =>
sym -> SBit sym -> EvalError -> SEval sym ()
assertSideCondition Concrete
sym (Integer
y forall a. Eq a => a -> a -> Bool
/= Integer
0) EvalError
DivideByZero
let sx :: Integer
sx = Integer -> Integer -> Integer
signedValue Integer
i Integer
x
sy :: Integer
sy = Integer -> Integer -> Integer
signedValue Integer
i Integer
y
forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$! Integer -> Integer -> BV
mkBv Integer
i (Integer
sx forall a. Integral a => a -> a -> a
`quot` Integer
sy)
| Bool
otherwise = forall a. HasCallStack => String -> [String] -> a
panic String
"Attempt to divide words of different sizes: wordSignedDiv" [forall a. Show a => a -> String
show Integer
i, forall a. Show a => a -> String
show Integer
j]
wordSignedMod :: Concrete
-> SWord Concrete
-> SWord Concrete
-> SEval Concrete (SWord Concrete)
wordSignedMod Concrete
sym (BV Integer
i Integer
x) (BV Integer
j Integer
y)
| Integer
i forall a. Eq a => a -> a -> Bool
== Integer
0 Bool -> Bool -> Bool
&& Integer
j forall a. Eq a => a -> a -> Bool
== Integer
0 = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$! Integer -> Integer -> BV
mkBv Integer
0 Integer
0
| Integer
i forall a. Eq a => a -> a -> Bool
== Integer
j =
do forall sym.
Backend sym =>
sym -> SBit sym -> EvalError -> SEval sym ()
assertSideCondition Concrete
sym (Integer
y forall a. Eq a => a -> a -> Bool
/= Integer
0) EvalError
DivideByZero
let sx :: Integer
sx = Integer -> Integer -> Integer
signedValue Integer
i Integer
x
sy :: Integer
sy = Integer -> Integer -> Integer
signedValue Integer
i Integer
y
forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$! Integer -> Integer -> BV
mkBv Integer
i (Integer
sx forall a. Integral a => a -> a -> a
`rem` Integer
sy)
| Bool
otherwise = forall a. HasCallStack => String -> [String] -> a
panic String
"Attempt to mod words of different sizes: wordSignedMod" [forall a. Show a => a -> String
show Integer
i, forall a. Show a => a -> String
show Integer
j]
wordShiftLeft :: Concrete
-> SWord Concrete
-> SWord Concrete
-> SEval Concrete (SWord Concrete)
wordShiftLeft Concrete
_sym (BV Integer
w Integer
ival) (BV Integer
_ Integer
by)
| Integer
by forall a. Ord a => a -> a -> Bool
>= Integer
w = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$! Integer -> Integer -> BV
BV Integer
w Integer
0
| Integer
by forall a. Ord a => a -> a -> Bool
> forall a. Integral a => a -> Integer
toInteger (forall a. Bounded a => a
maxBound :: Int) = forall a. HasCallStack => String -> [String] -> a
panic String
"shl" [String
"Shift amount too large", forall a. Show a => a -> String
show Integer
by]
| Bool
otherwise = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$! Integer -> Integer -> BV
mkBv Integer
w (forall a. Bits a => a -> Int -> a
shiftL Integer
ival (forall a. Num a => Integer -> a
fromInteger Integer
by))
wordShiftRight :: Concrete
-> SWord Concrete
-> SWord Concrete
-> SEval Concrete (SWord Concrete)
wordShiftRight Concrete
_sym (BV Integer
w Integer
ival) (BV Integer
_ Integer
by)
| Integer
by forall a. Ord a => a -> a -> Bool
>= Integer
w = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$! Integer -> Integer -> BV
BV Integer
w Integer
0
| Integer
by forall a. Ord a => a -> a -> Bool
> forall a. Integral a => a -> Integer
toInteger (forall a. Bounded a => a
maxBound :: Int) = forall a. HasCallStack => String -> [String] -> a
panic String
"lshr" [String
"Shift amount too large", forall a. Show a => a -> String
show Integer
by]
| Bool
otherwise = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$! Integer -> Integer -> BV
BV Integer
w (forall a. Bits a => a -> Int -> a
shiftR Integer
ival (forall a. Num a => Integer -> a
fromInteger Integer
by))
wordSignedShiftRight :: Concrete
-> SWord Concrete
-> SWord Concrete
-> SEval Concrete (SWord Concrete)
wordSignedShiftRight Concrete
_sym (BV Integer
w Integer
ival) (BV Integer
_ Integer
by) =
let by' :: Integer
by' = forall a. Ord a => a -> a -> a
min Integer
w Integer
by in
if Integer
by' forall a. Ord a => a -> a -> Bool
> forall a. Integral a => a -> Integer
toInteger (forall a. Bounded a => a
maxBound :: Int) then
forall a. HasCallStack => String -> [String] -> a
panic String
"wordSignedShiftRight" [String
"Shift amount too large", forall a. Show a => a -> String
show Integer
by]
else
forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$! Integer -> Integer -> BV
mkBv Integer
w (forall a. Bits a => a -> Int -> a
shiftR (Integer -> Integer -> Integer
signedValue Integer
w Integer
ival) (forall a. Num a => Integer -> a
fromInteger Integer
by'))
wordRotateRight :: Concrete
-> SWord Concrete
-> SWord Concrete
-> SEval Concrete (SWord Concrete)
wordRotateRight Concrete
_sym (BV Integer
0 Integer
i) SWord Concrete
_ = forall (f :: * -> *) a. Applicative f => a -> f a
pure (Integer -> Integer -> BV
BV Integer
0 Integer
i)
wordRotateRight Concrete
_sym (BV Integer
w Integer
i) (BV Integer
_ Integer
by) =
forall (f :: * -> *) a. Applicative f => a -> f a
pure forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> Integer -> BV
mkBv Integer
w forall a b. (a -> b) -> a -> b
$! (Integer
i forall a. Bits a => a -> Int -> a
`shiftR` Int
b) forall a. Bits a => a -> a -> a
.|. (Integer
i forall a. Bits a => a -> Int -> a
`shiftL` (forall a. Num a => Integer -> a
fromInteger Integer
w forall a. Num a => a -> a -> a
- Int
b))
where b :: Int
b = forall a. Num a => Integer -> a
fromInteger (Integer
by forall a. Integral a => a -> a -> a
`mod` Integer
w)
wordRotateLeft :: Concrete
-> SWord Concrete
-> SWord Concrete
-> SEval Concrete (SWord Concrete)
wordRotateLeft Concrete
_sym (BV Integer
0 Integer
i) SWord Concrete
_ = forall (f :: * -> *) a. Applicative f => a -> f a
pure (Integer -> Integer -> BV
BV Integer
0 Integer
i)
wordRotateLeft Concrete
_sym (BV Integer
w Integer
i) (BV Integer
_ Integer
by) =
forall (f :: * -> *) a. Applicative f => a -> f a
pure forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> Integer -> BV
mkBv Integer
w forall a b. (a -> b) -> a -> b
$! (Integer
i forall a. Bits a => a -> Int -> a
`shiftL` Int
b) forall a. Bits a => a -> a -> a
.|. (Integer
i forall a. Bits a => a -> Int -> a
`shiftR` (forall a. Num a => Integer -> a
fromInteger Integer
w forall a. Num a => a -> a -> a
- Int
b))
where b :: Int
b = forall a. Num a => Integer -> a
fromInteger (Integer
by forall a. Integral a => a -> a -> a
`mod` Integer
w)
wordLg2 :: Concrete -> SWord Concrete -> SEval Concrete (SWord Concrete)
wordLg2 Concrete
_ (BV Integer
i Integer
x) = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$! Integer -> Integer -> BV
mkBv Integer
i (Integer -> Integer
lg2 Integer
x)
intEq :: Concrete
-> SInteger Concrete
-> SInteger Concrete
-> SEval Concrete (SBit Concrete)
intEq Concrete
_ SInteger Concrete
x SInteger Concrete
y = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$! SInteger Concrete
x forall a. Eq a => a -> a -> Bool
== SInteger Concrete
y
intLessThan :: Concrete
-> SInteger Concrete
-> SInteger Concrete
-> SEval Concrete (SBit Concrete)
intLessThan Concrete
_ SInteger Concrete
x SInteger Concrete
y = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$! SInteger Concrete
x forall a. Ord a => a -> a -> Bool
< SInteger Concrete
y
intGreaterThan :: Concrete
-> SInteger Concrete
-> SInteger Concrete
-> SEval Concrete (SBit Concrete)
intGreaterThan Concrete
_ SInteger Concrete
x SInteger Concrete
y = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$! SInteger Concrete
x forall a. Ord a => a -> a -> Bool
> SInteger Concrete
y
intPlus :: Concrete
-> SInteger Concrete
-> SInteger Concrete
-> SEval Concrete (SInteger Concrete)
intPlus Concrete
_ SInteger Concrete
x SInteger Concrete
y = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$! SInteger Concrete
x forall a. Num a => a -> a -> a
+ SInteger Concrete
y
intMinus :: Concrete
-> SInteger Concrete
-> SInteger Concrete
-> SEval Concrete (SInteger Concrete)
intMinus Concrete
_ SInteger Concrete
x SInteger Concrete
y = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$! SInteger Concrete
x forall a. Num a => a -> a -> a
- SInteger Concrete
y
intNegate :: Concrete -> SInteger Concrete -> SEval Concrete (SInteger Concrete)
intNegate Concrete
_ SInteger Concrete
x = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$! forall a. Num a => a -> a
negate SInteger Concrete
x
intMult :: Concrete
-> SInteger Concrete
-> SInteger Concrete
-> SEval Concrete (SInteger Concrete)
intMult Concrete
_ SInteger Concrete
x SInteger Concrete
y = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$! SInteger Concrete
x forall a. Num a => a -> a -> a
* SInteger Concrete
y
intDiv :: Concrete
-> SInteger Concrete
-> SInteger Concrete
-> SEval Concrete (SInteger Concrete)
intDiv Concrete
sym SInteger Concrete
x SInteger Concrete
y =
do forall sym.
Backend sym =>
sym -> SBit sym -> EvalError -> SEval sym ()
assertSideCondition Concrete
sym (SInteger Concrete
y forall a. Eq a => a -> a -> Bool
/= Integer
0) EvalError
DivideByZero
forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$! SInteger Concrete
x forall a. Integral a => a -> a -> a
`div` SInteger Concrete
y
intMod :: Concrete
-> SInteger Concrete
-> SInteger Concrete
-> SEval Concrete (SInteger Concrete)
intMod Concrete
sym SInteger Concrete
x SInteger Concrete
y =
do forall sym.
Backend sym =>
sym -> SBit sym -> EvalError -> SEval sym ()
assertSideCondition Concrete
sym (SInteger Concrete
y forall a. Eq a => a -> a -> Bool
/= Integer
0) EvalError
DivideByZero
forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$! SInteger Concrete
x forall a. Integral a => a -> a -> a
`mod` SInteger Concrete
y
intToZn :: Concrete
-> Integer
-> SInteger Concrete
-> SEval Concrete (SInteger Concrete)
intToZn Concrete
_ Integer
0 SInteger Concrete
_ = forall a. HasCallStack => String -> [String] -> a
evalPanic String
"intToZn" [String
"0 modulus not allowed"]
intToZn Concrete
_ Integer
m SInteger Concrete
x = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$! SInteger Concrete
x forall a. Integral a => a -> a -> a
`mod` Integer
m
znToInt :: Concrete
-> Integer
-> SInteger Concrete
-> SEval Concrete (SInteger Concrete)
znToInt Concrete
_ Integer
_m SInteger Concrete
x = forall (f :: * -> *) a. Applicative f => a -> f a
pure SInteger Concrete
x
znEq :: Concrete
-> Integer
-> SInteger Concrete
-> SInteger Concrete
-> SEval Concrete (SBit Concrete)
znEq Concrete
_ Integer
_m SInteger Concrete
x SInteger Concrete
y = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$! SInteger Concrete
x forall a. Eq a => a -> a -> Bool
== SInteger Concrete
y
znRecip :: Concrete
-> Integer
-> SInteger Concrete
-> SEval Concrete (SInteger Concrete)
znRecip Concrete
sym Integer
m SInteger Concrete
x =
case Integer -> Integer -> Maybe Integer
Integer.integerRecipMod SInteger Concrete
x Integer
m of
Just Integer
r -> forall sym.
Backend sym =>
sym -> Integer -> SEval sym (SInteger sym)
integerLit Concrete
sym Integer
r
Maybe Integer
Nothing -> forall sym a. Backend sym => sym -> EvalError -> SEval sym a
raiseError Concrete
sym EvalError
DivideByZero
znPlus :: Concrete
-> Integer
-> SInteger Concrete
-> SInteger Concrete
-> SEval Concrete (SInteger Concrete)
znPlus Concrete
_ = forall (m :: * -> *).
Monad m =>
(Integer -> Integer -> Integer)
-> Integer -> Integer -> Integer -> m Integer
liftBinIntMod forall a. Num a => a -> a -> a
(+)
znMinus :: Concrete
-> Integer
-> SInteger Concrete
-> SInteger Concrete
-> SEval Concrete (SInteger Concrete)
znMinus Concrete
_ = forall (m :: * -> *).
Monad m =>
(Integer -> Integer -> Integer)
-> Integer -> Integer -> Integer -> m Integer
liftBinIntMod (-)
znMult :: Concrete
-> Integer
-> SInteger Concrete
-> SInteger Concrete
-> SEval Concrete (SInteger Concrete)
znMult Concrete
_ = forall (m :: * -> *).
Monad m =>
(Integer -> Integer -> Integer)
-> Integer -> Integer -> Integer -> m Integer
liftBinIntMod forall a. Num a => a -> a -> a
(*)
znNegate :: Concrete
-> Integer
-> SInteger Concrete
-> SEval Concrete (SInteger Concrete)
znNegate Concrete
_ Integer
0 SInteger Concrete
_ = forall a. HasCallStack => String -> [String] -> a
evalPanic String
"znNegate" [String
"0 modulus not allowed"]
znNegate Concrete
_ Integer
m SInteger Concrete
x = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$! (forall a. Num a => a -> a
negate SInteger Concrete
x) forall a. Integral a => a -> a -> a
`mod` Integer
m
fpLit :: Concrete
-> Integer
-> Integer
-> Rational
-> SEval Concrete (SFloat Concrete)
fpLit Concrete
_sym Integer
e Integer
p Rational
rat = forall (f :: * -> *) a. Applicative f => a -> f a
pure (Integer -> Integer -> Rational -> BF
FP.fpLit Integer
e Integer
p Rational
rat)
fpNaN :: Concrete -> Integer -> Integer -> SEval Concrete (SFloat Concrete)
fpNaN Concrete
_sym Integer
e Integer
p = forall (f :: * -> *) a. Applicative f => a -> f a
pure (Integer -> Integer -> BigFloat -> BF
FP.BF Integer
e Integer
p BigFloat
FP.bfNaN)
fpPosInf :: Concrete -> Integer -> Integer -> SEval Concrete (SFloat Concrete)
fpPosInf Concrete
_sym Integer
e Integer
p = forall (f :: * -> *) a. Applicative f => a -> f a
pure (Integer -> Integer -> BigFloat -> BF
FP.BF Integer
e Integer
p BigFloat
FP.bfPosInf)
fpAsLit :: Concrete -> SFloat Concrete -> Maybe BF
fpAsLit Concrete
_ SFloat Concrete
f = forall a. a -> Maybe a
Just SFloat Concrete
f
fpExactLit :: Concrete -> BF -> SEval Concrete (SFloat Concrete)
fpExactLit Concrete
_sym BF
bf = forall (f :: * -> *) a. Applicative f => a -> f a
pure BF
bf
fpEq :: Concrete
-> SFloat Concrete
-> SFloat Concrete
-> SEval Concrete (SBit Concrete)
fpEq Concrete
_sym SFloat Concrete
x SFloat Concrete
y = forall (f :: * -> *) a. Applicative f => a -> f a
pure (BF -> BigFloat
FP.bfValue SFloat Concrete
x forall a. Eq a => a -> a -> Bool
== BF -> BigFloat
FP.bfValue SFloat Concrete
y)
fpLogicalEq :: Concrete
-> SFloat Concrete
-> SFloat Concrete
-> SEval Concrete (SBit Concrete)
fpLogicalEq Concrete
_sym SFloat Concrete
x SFloat Concrete
y = forall (f :: * -> *) a. Applicative f => a -> f a
pure (BigFloat -> BigFloat -> Ordering
FP.bfCompare (BF -> BigFloat
FP.bfValue SFloat Concrete
x) (BF -> BigFloat
FP.bfValue SFloat Concrete
y) forall a. Eq a => a -> a -> Bool
== Ordering
EQ)
fpLessThan :: Concrete
-> SFloat Concrete
-> SFloat Concrete
-> SEval Concrete (SBit Concrete)
fpLessThan Concrete
_sym SFloat Concrete
x SFloat Concrete
y = forall (f :: * -> *) a. Applicative f => a -> f a
pure (BF -> BigFloat
FP.bfValue SFloat Concrete
x forall a. Ord a => a -> a -> Bool
< BF -> BigFloat
FP.bfValue SFloat Concrete
y)
fpGreaterThan :: Concrete
-> SFloat Concrete
-> SFloat Concrete
-> SEval Concrete (SBit Concrete)
fpGreaterThan Concrete
_sym SFloat Concrete
x SFloat Concrete
y = forall (f :: * -> *) a. Applicative f => a -> f a
pure (BF -> BigFloat
FP.bfValue SFloat Concrete
x forall a. Ord a => a -> a -> Bool
> BF -> BigFloat
FP.bfValue SFloat Concrete
y)
fpPlus :: FPArith2 Concrete
fpPlus = (BFOpts -> BigFloat -> BigFloat -> (BigFloat, Status))
-> FPArith2 Concrete
fpBinArith BFOpts -> BigFloat -> BigFloat -> (BigFloat, Status)
FP.bfAdd
fpMinus :: FPArith2 Concrete
fpMinus = (BFOpts -> BigFloat -> BigFloat -> (BigFloat, Status))
-> FPArith2 Concrete
fpBinArith BFOpts -> BigFloat -> BigFloat -> (BigFloat, Status)
FP.bfSub
fpMult :: FPArith2 Concrete
fpMult = (BFOpts -> BigFloat -> BigFloat -> (BigFloat, Status))
-> FPArith2 Concrete
fpBinArith BFOpts -> BigFloat -> BigFloat -> (BigFloat, Status)
FP.bfMul
fpDiv :: FPArith2 Concrete
fpDiv = (BFOpts -> BigFloat -> BigFloat -> (BigFloat, Status))
-> FPArith2 Concrete
fpBinArith BFOpts -> BigFloat -> BigFloat -> (BigFloat, Status)
FP.bfDiv
fpNeg :: Concrete -> SFloat Concrete -> SEval Concrete (SFloat Concrete)
fpNeg Concrete
_ SFloat Concrete
x = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$! SFloat Concrete
x { bfValue :: BigFloat
FP.bfValue = BigFloat -> BigFloat
FP.bfNeg (BF -> BigFloat
FP.bfValue SFloat Concrete
x) }
fpAbs :: Concrete -> SFloat Concrete -> SEval Concrete (SFloat Concrete)
fpAbs Concrete
_ SFloat Concrete
x = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$! SFloat Concrete
x { bfValue :: BigFloat
FP.bfValue = BigFloat -> BigFloat
FP.bfAbs (BF -> BigFloat
FP.bfValue SFloat Concrete
x) }
fpSqrt :: Concrete
-> SWord Concrete
-> SFloat Concrete
-> SEval Concrete (SFloat Concrete)
fpSqrt Concrete
sym SWord Concrete
r SFloat Concrete
x =
do RoundMode
r' <- Concrete -> SWord Concrete -> SEval Concrete RoundMode
fpRoundMode Concrete
sym SWord Concrete
r
let opts :: BFOpts
opts = Integer -> Integer -> RoundMode -> BFOpts
FP.fpOpts (BF -> Integer
FP.bfExpWidth SFloat Concrete
x) (BF -> Integer
FP.bfPrecWidth SFloat Concrete
x) RoundMode
r'
forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$! SFloat Concrete
x{ bfValue :: BigFloat
FP.bfValue = (BigFloat, Status) -> BigFloat
FP.fpCheckStatus (BFOpts -> BigFloat -> (BigFloat, Status)
FP.bfSqrt BFOpts
opts (BF -> BigFloat
FP.bfValue SFloat Concrete
x)) }
fpFMA :: Concrete
-> SWord Concrete
-> SFloat Concrete
-> SFloat Concrete
-> SFloat Concrete
-> SEval Concrete (SFloat Concrete)
fpFMA Concrete
sym SWord Concrete
r SFloat Concrete
x SFloat Concrete
y SFloat Concrete
z =
do RoundMode
r' <- Concrete -> SWord Concrete -> SEval Concrete RoundMode
fpRoundMode Concrete
sym SWord Concrete
r
let opts :: BFOpts
opts = Integer -> Integer -> RoundMode -> BFOpts
FP.fpOpts (BF -> Integer
FP.bfExpWidth SFloat Concrete
x) (BF -> Integer
FP.bfPrecWidth SFloat Concrete
x) RoundMode
r'
forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$! SFloat Concrete
x { bfValue :: BigFloat
FP.bfValue = (BigFloat, Status) -> BigFloat
FP.fpCheckStatus (BFOpts -> BigFloat -> BigFloat -> BigFloat -> (BigFloat, Status)
FP.bfFMA BFOpts
opts (BF -> BigFloat
FP.bfValue SFloat Concrete
x) (BF -> BigFloat
FP.bfValue SFloat Concrete
y) (BF -> BigFloat
FP.bfValue SFloat Concrete
z)) }
fpIsZero :: Concrete -> SFloat Concrete -> SEval Concrete (SBit Concrete)
fpIsZero Concrete
_ SFloat Concrete
x = forall (f :: * -> *) a. Applicative f => a -> f a
pure (BigFloat -> Bool
FP.bfIsZero (BF -> BigFloat
FP.bfValue SFloat Concrete
x))
fpIsNeg :: Concrete -> SFloat Concrete -> SEval Concrete (SBit Concrete)
fpIsNeg Concrete
_ SFloat Concrete
x = forall (f :: * -> *) a. Applicative f => a -> f a
pure (BigFloat -> Bool
FP.bfIsNeg (BF -> BigFloat
FP.bfValue SFloat Concrete
x))
fpIsNaN :: Concrete -> SFloat Concrete -> SEval Concrete (SBit Concrete)
fpIsNaN Concrete
_ SFloat Concrete
x = forall (f :: * -> *) a. Applicative f => a -> f a
pure (BigFloat -> Bool
FP.bfIsNaN (BF -> BigFloat
FP.bfValue SFloat Concrete
x))
fpIsInf :: Concrete -> SFloat Concrete -> SEval Concrete (SBit Concrete)
fpIsInf Concrete
_ SFloat Concrete
x = forall (f :: * -> *) a. Applicative f => a -> f a
pure (BigFloat -> Bool
FP.bfIsInf (BF -> BigFloat
FP.bfValue SFloat Concrete
x))
fpIsNorm :: Concrete -> SFloat Concrete -> SEval Concrete (SBit Concrete)
fpIsNorm Concrete
_ SFloat Concrete
x =
let opts :: BFOpts
opts = Integer -> Integer -> RoundMode -> BFOpts
FP.fpOpts (BF -> Integer
FP.bfExpWidth SFloat Concrete
x) (BF -> Integer
FP.bfPrecWidth SFloat Concrete
x) RoundMode
FP.NearEven
in forall (f :: * -> *) a. Applicative f => a -> f a
pure (BFOpts -> BigFloat -> Bool
FP.bfIsNormal BFOpts
opts (BF -> BigFloat
FP.bfValue SFloat Concrete
x))
fpIsSubnorm :: Concrete -> SFloat Concrete -> SEval Concrete (SBit Concrete)
fpIsSubnorm Concrete
_ SFloat Concrete
x =
let opts :: BFOpts
opts = Integer -> Integer -> RoundMode -> BFOpts
FP.fpOpts (BF -> Integer
FP.bfExpWidth SFloat Concrete
x) (BF -> Integer
FP.bfPrecWidth SFloat Concrete
x) RoundMode
FP.NearEven
in forall (f :: * -> *) a. Applicative f => a -> f a
pure (BFOpts -> BigFloat -> Bool
FP.bfIsSubnormal BFOpts
opts (BF -> BigFloat
FP.bfValue SFloat Concrete
x))
fpFromBits :: Concrete
-> Integer
-> Integer
-> SWord Concrete
-> SEval Concrete (SFloat Concrete)
fpFromBits Concrete
_sym Integer
e Integer
p SWord Concrete
bv = forall (f :: * -> *) a. Applicative f => a -> f a
pure (Integer -> Integer -> Integer -> BF
FP.floatFromBits Integer
e Integer
p (BV -> Integer
bvVal SWord Concrete
bv))
fpToBits :: Concrete -> SFloat Concrete -> SEval Concrete (SWord Concrete)
fpToBits Concrete
_sym (FP.BF Integer
e Integer
p BigFloat
v) = forall (f :: * -> *) a. Applicative f => a -> f a
pure (Integer -> Integer -> BV
mkBv (Integer
eforall a. Num a => a -> a -> a
+Integer
p) (Integer -> Integer -> BigFloat -> Integer
FP.floatToBits Integer
e Integer
p BigFloat
v))
fpFromInteger :: Concrete
-> Integer
-> Integer
-> SWord Concrete
-> SInteger Concrete
-> SEval Concrete (SFloat Concrete)
fpFromInteger Concrete
sym Integer
e Integer
p SWord Concrete
r SInteger Concrete
x =
do RoundMode
r' <- Concrete -> SWord Concrete -> SEval Concrete RoundMode
fpRoundMode Concrete
sym SWord Concrete
r
forall (f :: * -> *) a. Applicative f => a -> f a
pure FP.BF { bfExpWidth :: Integer
FP.bfExpWidth = Integer
e
, bfPrecWidth :: Integer
FP.bfPrecWidth = Integer
p
, bfValue :: BigFloat
FP.bfValue = (BigFloat, Status) -> BigFloat
FP.fpCheckStatus forall a b. (a -> b) -> a -> b
$
RoundMode -> BigFloat -> (BigFloat, Status)
FP.bfRoundInt RoundMode
r' (Integer -> BigFloat
FP.bfFromInteger SInteger Concrete
x)
}
fpToInteger :: Concrete
-> String
-> SWord Concrete
-> SFloat Concrete
-> SEval Concrete (SInteger Concrete)
fpToInteger = Concrete
-> String
-> SWord Concrete
-> SFloat Concrete
-> SEval Concrete (SInteger Concrete)
fpCvtToInteger
fpFromRational :: Concrete
-> Integer
-> Integer
-> SWord Concrete
-> SRational Concrete
-> SEval Concrete (SFloat Concrete)
fpFromRational Concrete
sym Integer
e Integer
p SWord Concrete
r SRational Concrete
x =
do RoundMode
mode <- Concrete -> SWord Concrete -> SEval Concrete RoundMode
fpRoundMode Concrete
sym SWord Concrete
r
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Integer -> Integer -> RoundMode -> Rational -> BF
FP.floatFromRational Integer
e Integer
p RoundMode
mode (forall sym. SRational sym -> SInteger sym
sNum SRational Concrete
x forall a. Integral a => a -> a -> Ratio a
% forall sym. SRational sym -> SInteger sym
sDenom SRational Concrete
x))
fpToRational :: Concrete -> SFloat Concrete -> SEval Concrete (SRational Concrete)
fpToRational Concrete
sym SFloat Concrete
fp =
case String -> BF -> Either EvalError Rational
FP.floatToRational String
"fpToRational" SFloat Concrete
fp of
Left EvalError
err -> forall sym a. Backend sym => sym -> EvalError -> SEval sym a
raiseError Concrete
sym EvalError
err
Right Rational
r -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ SRational { sNum :: SInteger Concrete
sNum = forall a. Ratio a -> a
numerator Rational
r, sDenom :: SInteger Concrete
sDenom = forall a. Ratio a -> a
denominator Rational
r }
{-# INLINE liftBinIntMod #-}
liftBinIntMod :: Monad m =>
(Integer -> Integer -> Integer) -> Integer -> Integer -> Integer -> m Integer
liftBinIntMod :: forall (m :: * -> *).
Monad m =>
(Integer -> Integer -> Integer)
-> Integer -> Integer -> Integer -> m Integer
liftBinIntMod Integer -> Integer -> Integer
op Integer
m Integer
x Integer
y
| Integer
m forall a. Eq a => a -> a -> Bool
== Integer
0 = forall a. HasCallStack => String -> [String] -> a
evalPanic String
"znArithmetic" [String
"0 modulus not allowed"]
| Bool
otherwise = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ (Integer -> Integer -> Integer
op Integer
x Integer
y) forall a. Integral a => a -> a -> a
`mod` Integer
m
{-# INLINE fpBinArith #-}
fpBinArith ::
(FP.BFOpts -> FP.BigFloat -> FP.BigFloat -> (FP.BigFloat, FP.Status)) ->
Concrete ->
SWord Concrete ->
SFloat Concrete ->
SFloat Concrete ->
SEval Concrete (SFloat Concrete)
fpBinArith :: (BFOpts -> BigFloat -> BigFloat -> (BigFloat, Status))
-> FPArith2 Concrete
fpBinArith BFOpts -> BigFloat -> BigFloat -> (BigFloat, Status)
fun = \Concrete
sym SWord Concrete
r SFloat Concrete
x SFloat Concrete
y ->
do BFOpts
opts <- Integer -> Integer -> RoundMode -> BFOpts
FP.fpOpts (BF -> Integer
FP.bfExpWidth SFloat Concrete
x) (BF -> Integer
FP.bfPrecWidth SFloat Concrete
x)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Concrete -> SWord Concrete -> SEval Concrete RoundMode
fpRoundMode Concrete
sym SWord Concrete
r
forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$! SFloat Concrete
x { bfValue :: BigFloat
FP.bfValue = (BigFloat, Status) -> BigFloat
FP.fpCheckStatus
(BFOpts -> BigFloat -> BigFloat -> (BigFloat, Status)
fun BFOpts
opts (BF -> BigFloat
FP.bfValue SFloat Concrete
x) (BF -> BigFloat
FP.bfValue SFloat Concrete
y)) }
fpCvtToInteger ::
Concrete ->
String ->
SWord Concrete ->
SFloat Concrete ->
SEval Concrete (SInteger Concrete)
fpCvtToInteger :: Concrete
-> String
-> SWord Concrete
-> SFloat Concrete
-> SEval Concrete (SInteger Concrete)
fpCvtToInteger Concrete
sym String
fun SWord Concrete
rnd SFloat Concrete
flt =
do RoundMode
mode <- Concrete -> SWord Concrete -> SEval Concrete RoundMode
fpRoundMode Concrete
sym SWord Concrete
rnd
case String -> RoundMode -> BF -> Either EvalError Integer
FP.floatToInteger String
fun RoundMode
mode SFloat Concrete
flt of
Right Integer
i -> forall (f :: * -> *) a. Applicative f => a -> f a
pure Integer
i
Left EvalError
err -> forall sym a. Backend sym => sym -> EvalError -> SEval sym a
raiseError Concrete
sym EvalError
err
fpRoundMode :: Concrete -> SWord Concrete -> SEval Concrete FP.RoundMode
fpRoundMode :: Concrete -> SWord Concrete -> SEval Concrete RoundMode
fpRoundMode Concrete
sym SWord Concrete
w =
case Integer -> Either EvalError RoundMode
FP.fpRound (BV -> Integer
bvVal SWord Concrete
w) of
Left EvalError
err -> forall sym a. Backend sym => sym -> EvalError -> SEval sym a
raiseError Concrete
sym EvalError
err
Right RoundMode
a -> forall (f :: * -> *) a. Applicative f => a -> f a
pure RoundMode
a