-- |
-- Module      :  Cryptol.Backend.Concrete
-- Copyright   :  (c) 2013-2020 Galois, Inc.
-- License     :  BSD3
-- Maintainer  :  cryptol@galois.com
-- Stability   :  provisional
-- Portability :  portable

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

-- | Concrete bitvector values: width, value
-- Invariant: The value must be within the range 0 .. 2^width-1
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

-- | Apply an integer function to the values of bitvectors.
--   This function assumes both bitvectors are the same width.
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 #-}

-- | Apply an integer function to the values of a bitvector.
--   This function assumes the function will not require masking.
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 #-}

-- | Smart constructor for 'BV's that checks for the width limit
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 -- not sure how to rule this out
  | 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"

-- Concrete Big-endian Words ------------------------------------------------------------

mask ::
  Integer  {- ^ Bit-width -} ->
  Integer  {- ^ Value -} ->
  Integer  {- ^ Masked result -}
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

  -- NB: requires we maintain the invariant that
  --     Z_n is in reduced form
  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

  -- NB: under the precondition that `m` is prime,
  -- the only values for which no inverse exists are
  -- congruent to 0 modulo m.
  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

  ------------------------------------------------------------------------
  -- Floating Point
  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  {- ^ Rouding mode -} ->
  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 {- ^ Rounding mode -} ->
  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