-- |
-- 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 Numeric (showIntAtBase)
import qualified LibBF as FP
import qualified GHC.Integer.GMP.Internals 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
(Int -> Concrete -> ShowS)
-> (Concrete -> String) -> ([Concrete] -> ShowS) -> Show Concrete
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 = Integer -> String
forall a. Show a => a -> String
show (Integer -> String) -> (BV -> Integer) -> BV -> String
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 :: (Integer -> Integer -> Integer) -> BV -> BV -> m BV
binBV Integer -> Integer -> Integer
f (BV Integer
w Integer
x) (BV Integer
_ Integer
y) = BV -> m BV
forall (f :: * -> *) a. Applicative f => a -> f a
pure (BV -> m BV) -> BV -> m BV
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 (Integer -> BV) -> Integer -> BV
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 Integer -> Int -> Bool
forall a. Bits a => a -> Int -> Bool
testBit Integer
x (Integer -> Int
forall a. Num a => Integer -> a
fromInteger (Integer
iInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
-Integer
1)) then Integer
x Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- (Int -> Integer
forall a. Bits a => Int -> a
bit (Integer -> Int
forall a. Num a => Integer -> a
fromInteger Integer
i)) else Integer
x

integerToChar :: Integer -> Char
integerToChar :: Integer -> Char
integerToChar = Int -> Char
forall a. Enum a => Int -> a
toEnum (Int -> Char) -> (Integer -> Int) -> Integer -> Char
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> Int
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' Integer -> Integer -> Integer
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 Int -> Int -> Bool
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 (Char -> String
forall a. Show a => a -> String
show (Int -> Char
forall a. Enum a => Int -> a
toEnum (Integer -> Int
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 (Int -> Char -> String
forall a. Int -> a -> [a]
replicate Int
padLen Char
'0')
    where
    padLen :: Int
padLen | Int
m Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
0     = Int
d Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1
           | Bool
otherwise = Int
d

    (Int
d,Int
m) = (Integer -> Int
forall a. Num a => Integer -> a
fromInteger Integer
width Int -> Int -> Int
forall a. Num a => a -> a -> a
- (String -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length String
value Int -> Int -> Int
forall a. Num a => a -> a -> a
* Int
bitsPerDigit))
                   Int -> Int -> (Int, Int)
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 -> Doc
empty
    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  = Integer -> (Int -> Char) -> Integer -> ShowS
forall a. (Integral a, Show a) => a -> (Int -> Char) -> a -> ShowS
showIntAtBase (Int -> Integer
forall a. Integral a => a -> Integer
toInteger Int
base) (String
digits String -> Int -> Char
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 Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= Integer
Arch.maxBigIntWidth = Integer -> Integer
forall a. Integer -> a
wordTooWide Integer
w
         | Bool
otherwise                = Integer
i Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.&. (Int -> Integer
forall a. Bits a => Int -> a
bit (Integer -> Int
forall a. Num a => Integer -> a
fromInteger Integer
w) Integer -> Integer -> Integer
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 :: Concrete -> EvalError -> SEval Concrete a
raiseError Concrete
_ EvalError
err = IO a -> Eval a
forall a. IO a -> Eval a
io (EvalError -> IO a
forall e a. Exception e => e -> IO a
X.throwIO EvalError
err)

  assertSideCondition :: Concrete -> SBit Concrete -> EvalError -> SEval Concrete ()
assertSideCondition Concrete
_ SBit Concrete
True EvalError
_ = () -> Eval ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
  assertSideCondition Concrete
_ SBit Concrete
False EvalError
err = IO () -> Eval ()
forall a. IO a -> Eval a
io (EvalError -> IO ()
forall e a. Exception e => e -> IO a
X.throwIO EvalError
err)

  wordLen :: Concrete -> SWord Concrete -> Integer
wordLen Concrete
_ (BV w _) = Integer
w
  wordAsChar :: Concrete -> SWord Concrete -> Maybe Char
wordAsChar Concrete
_ (BV _ x) = Char -> Maybe Char
forall a. a -> Maybe a
Just (Char -> Maybe Char) -> Char -> Maybe Char
forall a b. (a -> b) -> a -> b
$! Integer -> Char
integerToChar Integer
x

  wordBit :: Concrete
-> SWord Concrete -> Integer -> SEval Concrete (SBit Concrete)
wordBit Concrete
_ (BV w x) Integer
idx = Bool -> Eval Bool
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Bool -> Eval Bool) -> Bool -> Eval Bool
forall a b. (a -> b) -> a -> b
$! Integer -> Int -> Bool
forall a. Bits a => a -> Int -> Bool
testBit Integer
x (Integer -> Int
forall a. Num a => Integer -> a
fromInteger (Integer
w Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
1 Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
idx))

  wordUpdate :: Concrete
-> SWord Concrete
-> Integer
-> SBit Concrete
-> SEval Concrete (SWord Concrete)
wordUpdate Concrete
_ (BV w x) Integer
idx SBit Concrete
True  = BV -> Eval BV
forall (f :: * -> *) a. Applicative f => a -> f a
pure (BV -> Eval BV) -> BV -> Eval BV
forall a b. (a -> b) -> a -> b
$! Integer -> Integer -> BV
BV Integer
w (Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
setBit   Integer
x (Integer -> Int
forall a. Num a => Integer -> a
fromInteger (Integer
w Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
1 Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
idx)))
  wordUpdate Concrete
_ (BV w x) Integer
idx SBit Concrete
False = BV -> Eval BV
forall (f :: * -> *) a. Applicative f => a -> f a
pure (BV -> Eval BV) -> BV -> Eval BV
forall a b. (a -> b) -> a -> b
$! Integer -> Integer -> BV
BV Integer
w (Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
clearBit Integer
x (Integer -> Int
forall a. Num a => Integer -> a
fromInteger (Integer
w Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
1 Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
idx)))

  isReady :: Concrete -> SEval Concrete a -> Bool
isReady Concrete
_ (Ready _) = Bool
True
  isReady Concrete
_ SEval Concrete a
_ = Bool
False

  mergeEval :: 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 <- Eval a
SEval Concrete a
mx
       a
y <- Eval a
SEval Concrete a
my
       SBit Concrete -> a -> a -> SEval Concrete a
f SBit Concrete
c a
x a
y

  sDeclareHole :: Concrete
-> String
-> SEval
     Concrete (SEval Concrete a, SEval Concrete a -> SEval Concrete ())
sDeclareHole Concrete
_ = String
-> SEval
     Concrete (SEval Concrete a, SEval Concrete a -> SEval Concrete ())
forall a. String -> Eval (Eval a, Eval a -> Eval ())
blackhole
  sDelayFill :: Concrete
-> SEval Concrete a
-> SEval Concrete a
-> SEval Concrete (SEval Concrete a)
sDelayFill Concrete
_ = SEval Concrete a
-> SEval Concrete a -> SEval Concrete (SEval Concrete a)
forall a. Eval a -> Eval a -> Eval (Eval a)
delayFill
  sSpark :: Concrete -> SEval Concrete a -> SEval Concrete (SEval Concrete a)
sSpark Concrete
_ = SEval Concrete a -> SEval Concrete (SEval Concrete a)
forall a. Eval a -> Eval (Eval a)
evalSpark

  ppBit :: Concrete -> SBit Concrete -> Doc
ppBit Concrete
_ SBit Concrete
b | Bool
SBit Concrete
b         = String -> Doc
text String
"True"
            | Bool
otherwise = String -> Doc
text String
"False"

  ppWord :: Concrete -> PPOpts -> SWord Concrete -> Doc
ppWord Concrete
_ = PPOpts -> SWord Concrete -> Doc
PPOpts -> BV -> Doc
ppBV

  ppInteger :: Concrete -> PPOpts -> SInteger Concrete -> Doc
ppInteger Concrete
_ PPOpts
_opts SInteger Concrete
i = Integer -> Doc
integer Integer
SInteger Concrete
i

  ppFloat :: Concrete -> PPOpts -> SFloat Concrete -> Doc
ppFloat Concrete
_ = PPOpts -> BF -> Doc
PPOpts -> SFloat Concrete -> Doc
FP.fpPP

  bitLit :: Concrete -> Bool -> SBit Concrete
bitLit Concrete
_ Bool
b = Bool
SBit Concrete
b
  bitAsLit :: Concrete -> SBit Concrete -> Maybe Bool
bitAsLit Concrete
_ SBit Concrete
b = Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
SBit Concrete
b

  bitEq :: Concrete
-> SBit Concrete -> SBit Concrete -> SEval Concrete (SBit Concrete)
bitEq Concrete
_  SBit Concrete
x SBit Concrete
y = Bool -> Eval Bool
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Bool -> Eval Bool) -> Bool -> Eval Bool
forall a b. (a -> b) -> a -> b
$! Bool
SBit Concrete
x Bool -> Bool -> Bool
forall a. Eq a => a -> a -> Bool
== Bool
SBit Concrete
y
  bitOr :: Concrete
-> SBit Concrete -> SBit Concrete -> SEval Concrete (SBit Concrete)
bitOr Concrete
_  SBit Concrete
x SBit Concrete
y = Bool -> Eval Bool
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Bool -> Eval Bool) -> Bool -> Eval Bool
forall a b. (a -> b) -> a -> b
$! Bool
SBit Concrete
x Bool -> Bool -> Bool
forall a. Bits a => a -> a -> a
.|. Bool
SBit Concrete
y
  bitAnd :: Concrete
-> SBit Concrete -> SBit Concrete -> SEval Concrete (SBit Concrete)
bitAnd Concrete
_ SBit Concrete
x SBit Concrete
y = Bool -> Eval Bool
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Bool -> Eval Bool) -> Bool -> Eval Bool
forall a b. (a -> b) -> a -> b
$! Bool
SBit Concrete
x Bool -> Bool -> Bool
forall a. Bits a => a -> a -> a
.&. Bool
SBit Concrete
y
  bitXor :: Concrete
-> SBit Concrete -> SBit Concrete -> SEval Concrete (SBit Concrete)
bitXor Concrete
_ SBit Concrete
x SBit Concrete
y = Bool -> Eval Bool
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Bool -> Eval Bool) -> Bool -> Eval Bool
forall a b. (a -> b) -> a -> b
$! Bool
SBit Concrete
x Bool -> Bool -> Bool
forall a. Bits a => a -> a -> a
`xor` Bool
SBit Concrete
y
  bitComplement :: Concrete -> SBit Concrete -> SEval Concrete (SBit Concrete)
bitComplement Concrete
_ SBit Concrete
x = Bool -> Eval Bool
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Bool -> Eval Bool) -> Bool -> Eval Bool
forall a b. (a -> b) -> a -> b
$! Bool -> Bool
forall a. Bits a => a -> a
complement Bool
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  = Bool -> Eval Bool
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Bool -> Eval Bool) -> Bool -> Eval Bool
forall a b. (a -> b) -> a -> b
$! if Bool
SBit Concrete
b then Bool
SBit Concrete
x else Bool
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 = BV -> Eval BV
forall (f :: * -> *) a. Applicative f => a -> f a
pure (BV -> Eval BV) -> BV -> Eval BV
forall a b. (a -> b) -> a -> b
$! if Bool
SBit Concrete
b then SWord Concrete
BV
x else SWord Concrete
BV
y
  iteInteger :: Concrete
-> SBit Concrete
-> SInteger Concrete
-> SInteger Concrete
-> SEval Concrete (SInteger Concrete)
iteInteger Concrete
_ SBit Concrete
b SInteger Concrete
x SInteger Concrete
y = Integer -> Eval Integer
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Integer -> Eval Integer) -> Integer -> Eval Integer
forall a b. (a -> b) -> a -> b
$! if Bool
SBit Concrete
b then Integer
SInteger Concrete
x else Integer
SInteger Concrete
y

  wordLit :: Concrete -> Integer -> Integer -> SEval Concrete (SWord Concrete)
wordLit Concrete
_ Integer
w Integer
i = BV -> Eval BV
forall (f :: * -> *) a. Applicative f => a -> f a
pure (BV -> Eval BV) -> BV -> Eval BV
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 w i) = (Integer, Integer) -> Maybe (Integer, Integer)
forall a. a -> Maybe a
Just (Integer
w,Integer
i)
  integerLit :: Concrete -> Integer -> SEval Concrete (SInteger Concrete)
integerLit Concrete
_ Integer
i = Integer -> Eval Integer
forall (f :: * -> *) a. Applicative f => a -> f a
pure Integer
i
  integerAsLit :: Concrete -> SInteger Concrete -> Maybe Integer
integerAsLit Concrete
_ = SInteger Concrete -> Maybe Integer
forall a. a -> Maybe a
Just

  wordToInt :: Concrete -> SWord Concrete -> SEval Concrete (SInteger Concrete)
wordToInt Concrete
_ (BV _ x) = Integer -> Eval Integer
forall (f :: * -> *) a. Applicative f => a -> f a
pure Integer
x
  wordFromInt :: Concrete
-> Integer -> SInteger Concrete -> SEval Concrete (SWord Concrete)
wordFromInt Concrete
_ Integer
w SInteger Concrete
x = BV -> Eval BV
forall (f :: * -> *) a. Applicative f => a -> f a
pure (BV -> Eval BV) -> BV -> Eval BV
forall a b. (a -> b) -> a -> b
$! Integer -> Integer -> BV
mkBv Integer
w Integer
SInteger Concrete
x

  packWord :: Concrete -> [SBit Concrete] -> SEval Concrete (SWord Concrete)
packWord Concrete
_ [SBit Concrete]
bits = BV -> Eval BV
forall (f :: * -> *) a. Applicative f => a -> f a
pure (BV -> Eval BV) -> BV -> Eval BV
forall a b. (a -> b) -> a -> b
$! Integer -> Integer -> BV
BV (Int -> Integer
forall a. Integral a => a -> Integer
toInteger Int
w) Integer
a
    where
      w :: Int
w = case [Bool] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Bool]
[SBit Concrete]
bits of
            Int
len | Int -> Integer
forall a. Integral a => a -> Integer
toInteger Int
len Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= Integer
Arch.maxBigIntWidth -> Integer -> Int
forall a. Integer -> a
wordTooWide (Int -> Integer
forall a. Integral a => a -> Integer
toInteger Int
len)
                | Bool
otherwise                  -> Int
len
      a :: Integer
a = (Integer -> (Int, Bool) -> Integer)
-> Integer -> [(Int, Bool)] -> Integer
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl Integer -> (Int, Bool) -> Integer
forall p. Bits p => p -> (Int, Bool) -> p
setb Integer
0 ([Int] -> [Bool] -> [(Int, Bool)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Int
w Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1, Int
w Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
2 .. Int
0] [Bool]
[SBit Concrete]
bits)
      setb :: p -> (Int, Bool) -> p
setb p
acc (Int
n,Bool
b) | Bool
b         = p -> Int -> p
forall a. Bits a => a -> Int -> a
setBit p
acc Int
n
                     | Bool
otherwise = p
acc

  unpackWord :: Concrete -> SWord Concrete -> SEval Concrete [SBit Concrete]
unpackWord Concrete
_ (BV w a) = [Bool] -> Eval [Bool]
forall (f :: * -> *) a. Applicative f => a -> f a
pure [ Integer -> Int -> Bool
forall a. Bits a => a -> Int -> Bool
testBit Integer
a Int
n | Int
n <- [Int
w' Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1, Int
w' Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
2 .. Int
0] ]
    where
      w' :: Int
w' = Integer -> Int
forall a. Num a => Integer -> a
fromInteger Integer
w

  joinWord :: Concrete
-> SWord Concrete
-> SWord Concrete
-> SEval Concrete (SWord Concrete)
joinWord Concrete
_ (BV i x) (BV j y) =
    BV -> Eval BV
forall (f :: * -> *) a. Applicative f => a -> f a
pure (BV -> Eval BV) -> BV -> Eval BV
forall a b. (a -> b) -> a -> b
$! Integer -> Integer -> BV
BV (Integer
i Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
j) (Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
shiftL Integer
x (Integer -> Int
forall a. Num a => Integer -> a
fromInteger Integer
j) Integer -> Integer -> Integer
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 _ x) =
    (BV, BV) -> Eval (BV, BV)
forall (f :: * -> *) a. Applicative f => a -> f a
pure ( Integer -> Integer -> BV
BV Integer
leftW (Integer
x Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
`shiftR` (Integer -> Int
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 _ x) = BV -> Eval BV
forall (f :: * -> *) a. Applicative f => a -> f a
pure (BV -> Eval BV) -> BV -> Eval BV
forall a b. (a -> b) -> a -> b
$! Integer -> Integer -> BV
mkBv Integer
n (Integer
x Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
`shiftR` (Integer -> Int
forall a. Num a => Integer -> a
fromInteger Integer
i))

  wordEq :: Concrete
-> SWord Concrete
-> SWord Concrete
-> SEval Concrete (SBit Concrete)
wordEq Concrete
_ (BV i x) (BV j y)
    | Integer
i Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
j = Bool -> Eval Bool
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Bool -> Eval Bool) -> Bool -> Eval Bool
forall a b. (a -> b) -> a -> b
$! Integer
x Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
y
    | Bool
otherwise = String -> [String] -> Eval Bool
forall a. HasCallStack => String -> [String] -> a
panic String
"Attempt to compare words of different sizes: wordEq" [Integer -> String
forall a. Show a => a -> String
show Integer
i, Integer -> String
forall a. Show a => a -> String
show Integer
j]

  wordSignedLessThan :: Concrete
-> SWord Concrete
-> SWord Concrete
-> SEval Concrete (SBit Concrete)
wordSignedLessThan Concrete
_ (BV i x) (BV j y)
    | Integer
i Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
j = Bool -> Eval Bool
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Bool -> Eval Bool) -> Bool -> Eval Bool
forall a b. (a -> b) -> a -> b
$! Integer -> Integer -> Integer
signedValue Integer
i Integer
x Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer -> Integer -> Integer
signedValue Integer
i Integer
y
    | Bool
otherwise = String -> [String] -> Eval Bool
forall a. HasCallStack => String -> [String] -> a
panic String
"Attempt to compare words of different sizes: wordSignedLessThan" [Integer -> String
forall a. Show a => a -> String
show Integer
i, Integer -> String
forall a. Show a => a -> String
show Integer
j]

  wordLessThan :: Concrete
-> SWord Concrete
-> SWord Concrete
-> SEval Concrete (SBit Concrete)
wordLessThan Concrete
_ (BV i x) (BV j y)
    | Integer
i Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
j = Bool -> Eval Bool
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Bool -> Eval Bool) -> Bool -> Eval Bool
forall a b. (a -> b) -> a -> b
$! Integer
x Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
y
    | Bool
otherwise = String -> [String] -> Eval Bool
forall a. HasCallStack => String -> [String] -> a
panic String
"Attempt to compare words of different sizes: wordLessThan" [Integer -> String
forall a. Show a => a -> String
show Integer
i, Integer -> String
forall a. Show a => a -> String
show Integer
j]

  wordGreaterThan :: Concrete
-> SWord Concrete
-> SWord Concrete
-> SEval Concrete (SBit Concrete)
wordGreaterThan Concrete
_ (BV i x) (BV j y)
    | Integer
i Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
j = Bool -> Eval Bool
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Bool -> Eval Bool) -> Bool -> Eval Bool
forall a b. (a -> b) -> a -> b
$! Integer
x Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
> Integer
y
    | Bool
otherwise = String -> [String] -> Eval Bool
forall a. HasCallStack => String -> [String] -> a
panic String
"Attempt to compare words of different sizes: wordGreaterThan" [Integer -> String
forall a. Show a => a -> String
show Integer
i, Integer -> String
forall a. Show a => a -> String
show Integer
j]

  wordAnd :: Concrete
-> SWord Concrete
-> SWord Concrete
-> SEval Concrete (SWord Concrete)
wordAnd Concrete
_ (BV i x) (BV j y)
    | Integer
i Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
j = BV -> Eval BV
forall (f :: * -> *) a. Applicative f => a -> f a
pure (BV -> Eval BV) -> BV -> Eval BV
forall a b. (a -> b) -> a -> b
$! Integer -> Integer -> BV
mkBv Integer
i (Integer
x Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.&. Integer
y)
    | Bool
otherwise = String -> [String] -> Eval BV
forall a. HasCallStack => String -> [String] -> a
panic String
"Attempt to AND words of different sizes: wordPlus" [Integer -> String
forall a. Show a => a -> String
show Integer
i, Integer -> String
forall a. Show a => a -> String
show Integer
j]

  wordOr :: Concrete
-> SWord Concrete
-> SWord Concrete
-> SEval Concrete (SWord Concrete)
wordOr Concrete
_ (BV i x) (BV j y)
    | Integer
i Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
j = BV -> Eval BV
forall (f :: * -> *) a. Applicative f => a -> f a
pure (BV -> Eval BV) -> BV -> Eval BV
forall a b. (a -> b) -> a -> b
$! Integer -> Integer -> BV
mkBv Integer
i (Integer
x Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.|. Integer
y)
    | Bool
otherwise = String -> [String] -> Eval BV
forall a. HasCallStack => String -> [String] -> a
panic String
"Attempt to OR words of different sizes: wordPlus" [Integer -> String
forall a. Show a => a -> String
show Integer
i, Integer -> String
forall a. Show a => a -> String
show Integer
j]

  wordXor :: Concrete
-> SWord Concrete
-> SWord Concrete
-> SEval Concrete (SWord Concrete)
wordXor Concrete
_ (BV i x) (BV j y)
    | Integer
i Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
j = BV -> Eval BV
forall (f :: * -> *) a. Applicative f => a -> f a
pure (BV -> Eval BV) -> BV -> Eval BV
forall a b. (a -> b) -> a -> b
$! Integer -> Integer -> BV
mkBv Integer
i (Integer
x Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
`xor` Integer
y)
    | Bool
otherwise = String -> [String] -> Eval BV
forall a. HasCallStack => String -> [String] -> a
panic String
"Attempt to XOR words of different sizes: wordPlus" [Integer -> String
forall a. Show a => a -> String
show Integer
i, Integer -> String
forall a. Show a => a -> String
show Integer
j]

  wordComplement :: Concrete -> SWord Concrete -> SEval Concrete (SWord Concrete)
wordComplement Concrete
_ (BV i x) = BV -> Eval BV
forall (f :: * -> *) a. Applicative f => a -> f a
pure (BV -> Eval BV) -> BV -> Eval BV
forall a b. (a -> b) -> a -> b
$! Integer -> Integer -> BV
mkBv Integer
i (Integer -> Integer
forall a. Bits a => a -> a
complement Integer
x)

  wordPlus :: Concrete
-> SWord Concrete
-> SWord Concrete
-> SEval Concrete (SWord Concrete)
wordPlus Concrete
_ (BV i x) (BV j y)
    | Integer
i Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
j = BV -> Eval BV
forall (f :: * -> *) a. Applicative f => a -> f a
pure (BV -> Eval BV) -> BV -> Eval BV
forall a b. (a -> b) -> a -> b
$! Integer -> Integer -> BV
mkBv Integer
i (Integer
xInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
+Integer
y)
    | Bool
otherwise = String -> [String] -> Eval BV
forall a. HasCallStack => String -> [String] -> a
panic String
"Attempt to add words of different sizes: wordPlus" [Integer -> String
forall a. Show a => a -> String
show Integer
i, Integer -> String
forall a. Show a => a -> String
show Integer
j]

  wordNegate :: Concrete -> SWord Concrete -> SEval Concrete (SWord Concrete)
wordNegate Concrete
_ (BV i x) = BV -> Eval BV
forall (f :: * -> *) a. Applicative f => a -> f a
pure (BV -> Eval BV) -> BV -> Eval BV
forall a b. (a -> b) -> a -> b
$! Integer -> Integer -> BV
mkBv Integer
i (Integer -> Integer
forall a. Num a => a -> a
negate Integer
x)

  wordMinus :: Concrete
-> SWord Concrete
-> SWord Concrete
-> SEval Concrete (SWord Concrete)
wordMinus Concrete
_ (BV i x) (BV j y)
    | Integer
i Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
j = BV -> Eval BV
forall (f :: * -> *) a. Applicative f => a -> f a
pure (BV -> Eval BV) -> BV -> Eval BV
forall a b. (a -> b) -> a -> b
$! Integer -> Integer -> BV
mkBv Integer
i (Integer
xInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
-Integer
y)
    | Bool
otherwise = String -> [String] -> Eval BV
forall a. HasCallStack => String -> [String] -> a
panic String
"Attempt to subtract words of different sizes: wordMinus" [Integer -> String
forall a. Show a => a -> String
show Integer
i, Integer -> String
forall a. Show a => a -> String
show Integer
j]

  wordMult :: Concrete
-> SWord Concrete
-> SWord Concrete
-> SEval Concrete (SWord Concrete)
wordMult Concrete
_ (BV i x) (BV j y)
    | Integer
i Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
j = BV -> Eval BV
forall (f :: * -> *) a. Applicative f => a -> f a
pure (BV -> Eval BV) -> BV -> Eval BV
forall a b. (a -> b) -> a -> b
$! Integer -> Integer -> BV
mkBv Integer
i (Integer
xInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
*Integer
y)
    | Bool
otherwise = String -> [String] -> Eval BV
forall a. HasCallStack => String -> [String] -> a
panic String
"Attempt to multiply words of different sizes: wordMult" [Integer -> String
forall a. Show a => a -> String
show Integer
i, Integer -> String
forall a. Show a => a -> String
show Integer
j]

  wordDiv :: Concrete
-> SWord Concrete
-> SWord Concrete
-> SEval Concrete (SWord Concrete)
wordDiv Concrete
sym (BV i x) (BV j y)
    | Integer
i Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
0 Bool -> Bool -> Bool
&& Integer
j Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
0 = BV -> Eval BV
forall (f :: * -> *) a. Applicative f => a -> f a
pure (BV -> Eval BV) -> BV -> Eval BV
forall a b. (a -> b) -> a -> b
$! Integer -> Integer -> BV
mkBv Integer
0 Integer
0
    | Integer
i Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
j =
        do Concrete -> SBit Concrete -> EvalError -> SEval Concrete ()
forall sym.
Backend sym =>
sym -> SBit sym -> EvalError -> SEval sym ()
assertSideCondition Concrete
sym (Integer
y Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
/= Integer
0) EvalError
DivideByZero
           BV -> Eval BV
forall (f :: * -> *) a. Applicative f => a -> f a
pure (BV -> Eval BV) -> BV -> Eval BV
forall a b. (a -> b) -> a -> b
$! Integer -> Integer -> BV
mkBv Integer
i (Integer
x Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`div` Integer
y)
    | Bool
otherwise = String -> [String] -> Eval BV
forall a. HasCallStack => String -> [String] -> a
panic String
"Attempt to divide words of different sizes: wordDiv" [Integer -> String
forall a. Show a => a -> String
show Integer
i, Integer -> String
forall a. Show a => a -> String
show Integer
j]

  wordMod :: Concrete
-> SWord Concrete
-> SWord Concrete
-> SEval Concrete (SWord Concrete)
wordMod Concrete
sym (BV i x) (BV j y)
    | Integer
i Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
0 Bool -> Bool -> Bool
&& Integer
j Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
0 = BV -> Eval BV
forall (f :: * -> *) a. Applicative f => a -> f a
pure (BV -> Eval BV) -> BV -> Eval BV
forall a b. (a -> b) -> a -> b
$! Integer -> Integer -> BV
mkBv Integer
0 Integer
0
    | Integer
i Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
j =
        do Concrete -> SBit Concrete -> EvalError -> SEval Concrete ()
forall sym.
Backend sym =>
sym -> SBit sym -> EvalError -> SEval sym ()
assertSideCondition Concrete
sym (Integer
y Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
/= Integer
0) EvalError
DivideByZero
           BV -> Eval BV
forall (f :: * -> *) a. Applicative f => a -> f a
pure (BV -> Eval BV) -> BV -> Eval BV
forall a b. (a -> b) -> a -> b
$! Integer -> Integer -> BV
mkBv Integer
i (Integer
x Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`mod` Integer
y)
    | Bool
otherwise = String -> [String] -> Eval BV
forall a. HasCallStack => String -> [String] -> a
panic String
"Attempt to mod words of different sizes: wordMod" [Integer -> String
forall a. Show a => a -> String
show Integer
i, Integer -> String
forall a. Show a => a -> String
show Integer
j]

  wordSignedDiv :: Concrete
-> SWord Concrete
-> SWord Concrete
-> SEval Concrete (SWord Concrete)
wordSignedDiv Concrete
sym (BV i x) (BV j y)
    | Integer
i Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
0 Bool -> Bool -> Bool
&& Integer
j Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
0 = BV -> Eval BV
forall (f :: * -> *) a. Applicative f => a -> f a
pure (BV -> Eval BV) -> BV -> Eval BV
forall a b. (a -> b) -> a -> b
$! Integer -> Integer -> BV
mkBv Integer
0 Integer
0
    | Integer
i Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
j =
        do Concrete -> SBit Concrete -> EvalError -> SEval Concrete ()
forall sym.
Backend sym =>
sym -> SBit sym -> EvalError -> SEval sym ()
assertSideCondition Concrete
sym (Integer
y Integer -> Integer -> Bool
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
           BV -> Eval BV
forall (f :: * -> *) a. Applicative f => a -> f a
pure (BV -> Eval BV) -> BV -> Eval BV
forall a b. (a -> b) -> a -> b
$! Integer -> Integer -> BV
mkBv Integer
i (Integer
sx Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`quot` Integer
sy)
    | Bool
otherwise = String -> [String] -> Eval BV
forall a. HasCallStack => String -> [String] -> a
panic String
"Attempt to divide words of different sizes: wordSignedDiv" [Integer -> String
forall a. Show a => a -> String
show Integer
i, Integer -> String
forall a. Show a => a -> String
show Integer
j]

  wordSignedMod :: Concrete
-> SWord Concrete
-> SWord Concrete
-> SEval Concrete (SWord Concrete)
wordSignedMod Concrete
sym (BV i x) (BV j y)
    | Integer
i Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
0 Bool -> Bool -> Bool
&& Integer
j Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
0 = BV -> Eval BV
forall (f :: * -> *) a. Applicative f => a -> f a
pure (BV -> Eval BV) -> BV -> Eval BV
forall a b. (a -> b) -> a -> b
$! Integer -> Integer -> BV
mkBv Integer
0 Integer
0
    | Integer
i Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
j =
        do Concrete -> SBit Concrete -> EvalError -> SEval Concrete ()
forall sym.
Backend sym =>
sym -> SBit sym -> EvalError -> SEval sym ()
assertSideCondition Concrete
sym (Integer
y Integer -> Integer -> Bool
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
           BV -> Eval BV
forall (f :: * -> *) a. Applicative f => a -> f a
pure (BV -> Eval BV) -> BV -> Eval BV
forall a b. (a -> b) -> a -> b
$! Integer -> Integer -> BV
mkBv Integer
i (Integer
sx Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`rem` Integer
sy)
    | Bool
otherwise = String -> [String] -> Eval BV
forall a. HasCallStack => String -> [String] -> a
panic String
"Attempt to mod words of different sizes: wordSignedMod" [Integer -> String
forall a. Show a => a -> String
show Integer
i, Integer -> String
forall a. Show a => a -> String
show Integer
j]

  wordLg2 :: Concrete -> SWord Concrete -> SEval Concrete (SWord Concrete)
wordLg2 Concrete
_ (BV i x) = BV -> Eval BV
forall (f :: * -> *) a. Applicative f => a -> f a
pure (BV -> Eval BV) -> BV -> Eval BV
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 = Bool -> Eval Bool
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Bool -> Eval Bool) -> Bool -> Eval Bool
forall a b. (a -> b) -> a -> b
$! Integer
SInteger Concrete
x Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
SInteger Concrete
y
  intLessThan :: Concrete
-> SInteger Concrete
-> SInteger Concrete
-> SEval Concrete (SBit Concrete)
intLessThan Concrete
_ SInteger Concrete
x SInteger Concrete
y = Bool -> Eval Bool
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Bool -> Eval Bool) -> Bool -> Eval Bool
forall a b. (a -> b) -> a -> b
$! Integer
SInteger Concrete
x Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
SInteger Concrete
y
  intGreaterThan :: Concrete
-> SInteger Concrete
-> SInteger Concrete
-> SEval Concrete (SBit Concrete)
intGreaterThan Concrete
_ SInteger Concrete
x SInteger Concrete
y = Bool -> Eval Bool
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Bool -> Eval Bool) -> Bool -> Eval Bool
forall a b. (a -> b) -> a -> b
$! Integer
SInteger Concrete
x Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
> Integer
SInteger Concrete
y

  intPlus :: Concrete
-> SInteger Concrete
-> SInteger Concrete
-> SEval Concrete (SInteger Concrete)
intPlus  Concrete
_ SInteger Concrete
x SInteger Concrete
y = Integer -> Eval Integer
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Integer -> Eval Integer) -> Integer -> Eval Integer
forall a b. (a -> b) -> a -> b
$! Integer
SInteger Concrete
x Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
SInteger Concrete
y
  intMinus :: Concrete
-> SInteger Concrete
-> SInteger Concrete
-> SEval Concrete (SInteger Concrete)
intMinus Concrete
_ SInteger Concrete
x SInteger Concrete
y = Integer -> Eval Integer
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Integer -> Eval Integer) -> Integer -> Eval Integer
forall a b. (a -> b) -> a -> b
$! Integer
SInteger Concrete
x Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
SInteger Concrete
y
  intNegate :: Concrete -> SInteger Concrete -> SEval Concrete (SInteger Concrete)
intNegate Concrete
_ SInteger Concrete
x  = Integer -> Eval Integer
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Integer -> Eval Integer) -> Integer -> Eval Integer
forall a b. (a -> b) -> a -> b
$! Integer -> Integer
forall a. Num a => a -> a
negate Integer
SInteger Concrete
x
  intMult :: Concrete
-> SInteger Concrete
-> SInteger Concrete
-> SEval Concrete (SInteger Concrete)
intMult  Concrete
_ SInteger Concrete
x SInteger Concrete
y = Integer -> Eval Integer
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Integer -> Eval Integer) -> Integer -> Eval Integer
forall a b. (a -> b) -> a -> b
$! Integer
SInteger Concrete
x Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* Integer
SInteger Concrete
y
  intDiv :: Concrete
-> SInteger Concrete
-> SInteger Concrete
-> SEval Concrete (SInteger Concrete)
intDiv Concrete
sym SInteger Concrete
x SInteger Concrete
y =
    do Concrete -> SBit Concrete -> EvalError -> SEval Concrete ()
forall sym.
Backend sym =>
sym -> SBit sym -> EvalError -> SEval sym ()
assertSideCondition Concrete
sym (Integer
SInteger Concrete
y Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
/= Integer
0) EvalError
DivideByZero
       Integer -> Eval Integer
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Integer -> Eval Integer) -> Integer -> Eval Integer
forall a b. (a -> b) -> a -> b
$! Integer
SInteger Concrete
x Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`div` Integer
SInteger Concrete
y
  intMod :: Concrete
-> SInteger Concrete
-> SInteger Concrete
-> SEval Concrete (SInteger Concrete)
intMod Concrete
sym SInteger Concrete
x SInteger Concrete
y =
    do Concrete -> SBit Concrete -> EvalError -> SEval Concrete ()
forall sym.
Backend sym =>
sym -> SBit sym -> EvalError -> SEval sym ()
assertSideCondition Concrete
sym (Integer
SInteger Concrete
y Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
/= Integer
0) EvalError
DivideByZero
       Integer -> Eval Integer
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Integer -> Eval Integer) -> Integer -> Eval Integer
forall a b. (a -> b) -> a -> b
$! Integer
SInteger Concrete
x Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`mod` Integer
SInteger Concrete
y

  intToZn :: Concrete
-> Integer
-> SInteger Concrete
-> SEval Concrete (SInteger Concrete)
intToZn Concrete
_ Integer
0 SInteger Concrete
_ = String -> [String] -> Eval Integer
forall a. HasCallStack => String -> [String] -> a
evalPanic String
"intToZn" [String
"0 modulus not allowed"]
  intToZn Concrete
_ Integer
m SInteger Concrete
x = Integer -> Eval Integer
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Integer -> Eval Integer) -> Integer -> Eval Integer
forall a b. (a -> b) -> a -> b
$! Integer
SInteger Concrete
x Integer -> Integer -> Integer
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 = Integer -> Eval Integer
forall (f :: * -> *) a. Applicative f => a -> f a
pure Integer
SInteger Concrete
x
  znEq :: Concrete
-> Integer
-> SInteger Concrete
-> SInteger Concrete
-> SEval Concrete (SBit Concrete)
znEq Concrete
_ Integer
_m SInteger Concrete
x SInteger Concrete
y = Bool -> Eval Bool
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Bool -> Eval Bool) -> Bool -> Eval Bool
forall a b. (a -> b) -> a -> b
$! Integer
SInteger Concrete
x Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
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
    | Integer
r Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
0    = Concrete -> EvalError -> SEval Concrete Integer
forall sym a. Backend sym => sym -> EvalError -> SEval sym a
raiseError Concrete
sym EvalError
DivideByZero
    | Bool
otherwise = Integer -> Eval Integer
forall (f :: * -> *) a. Applicative f => a -> f a
pure Integer
r
   where
     r :: Integer
r = Integer -> Integer -> Integer
Integer.recipModInteger Integer
SInteger Concrete
x Integer
m

  znPlus :: Concrete
-> Integer
-> SInteger Concrete
-> SInteger Concrete
-> SEval Concrete (SInteger Concrete)
znPlus  Concrete
_ = (Integer -> Integer -> Integer)
-> Integer -> Integer -> Integer -> Eval Integer
forall (m :: * -> *).
Monad m =>
(Integer -> Integer -> Integer)
-> Integer -> Integer -> Integer -> m Integer
liftBinIntMod Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
(+)
  znMinus :: Concrete
-> Integer
-> SInteger Concrete
-> SInteger Concrete
-> SEval Concrete (SInteger Concrete)
znMinus Concrete
_ = (Integer -> Integer -> Integer)
-> Integer -> Integer -> Integer -> Eval Integer
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
_ = (Integer -> Integer -> Integer)
-> Integer -> Integer -> Integer -> Eval Integer
forall (m :: * -> *).
Monad m =>
(Integer -> Integer -> Integer)
-> Integer -> Integer -> Integer -> m Integer
liftBinIntMod Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
(*)
  znNegate :: Concrete
-> Integer
-> SInteger Concrete
-> SEval Concrete (SInteger Concrete)
znNegate Concrete
_ Integer
0 SInteger Concrete
_ = String -> [String] -> Eval Integer
forall a. HasCallStack => String -> [String] -> a
evalPanic String
"znNegate" [String
"0 modulus not allowed"]
  znNegate Concrete
_ Integer
m SInteger Concrete
x = Integer -> Eval Integer
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Integer -> Eval Integer) -> Integer -> Eval Integer
forall a b. (a -> b) -> a -> b
$! (Integer -> Integer
forall a. Num a => a -> a
negate Integer
SInteger Concrete
x) Integer -> Integer -> Integer
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     = BF -> Eval BF
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Integer -> Integer -> Rational -> BF
FP.fpLit Integer
e Integer
p Rational
rat)
  fpExactLit :: Concrete -> BF -> SEval Concrete (SFloat Concrete)
fpExactLit Concrete
_sym BF
bf     = BF -> Eval 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          = Bool -> Eval Bool
forall (f :: * -> *) a. Applicative f => a -> f a
pure (BF -> BigFloat
FP.bfValue BF
SFloat Concrete
x BigFloat -> BigFloat -> Bool
forall a. Eq a => a -> a -> Bool
== BF -> BigFloat
FP.bfValue BF
SFloat Concrete
y)
  fpLogicalEq :: Concrete
-> SFloat Concrete
-> SFloat Concrete
-> SEval Concrete (SBit Concrete)
fpLogicalEq Concrete
_sym SFloat Concrete
x SFloat Concrete
y   = Bool -> Eval Bool
forall (f :: * -> *) a. Applicative f => a -> f a
pure (BigFloat -> BigFloat -> Ordering
FP.bfCompare (BF -> BigFloat
FP.bfValue BF
SFloat Concrete
x) (BF -> BigFloat
FP.bfValue BF
SFloat Concrete
y) Ordering -> Ordering -> Bool
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    = Bool -> Eval Bool
forall (f :: * -> *) a. Applicative f => a -> f a
pure (BF -> BigFloat
FP.bfValue BF
SFloat Concrete
x BigFloat -> BigFloat -> Bool
forall a. Ord a => a -> a -> Bool
<  BF -> BigFloat
FP.bfValue BF
SFloat Concrete
y)
  fpGreaterThan :: Concrete
-> SFloat Concrete
-> SFloat Concrete
-> SEval Concrete (SBit Concrete)
fpGreaterThan Concrete
_sym SFloat Concrete
x SFloat Concrete
y = Bool -> Eval Bool
forall (f :: * -> *) a. Applicative f => a -> f a
pure (BF -> BigFloat
FP.bfValue BF
SFloat Concrete
x BigFloat -> BigFloat -> Bool
forall a. Ord a => a -> a -> Bool
>  BF -> BigFloat
FP.bfValue BF
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 = BF -> Eval BF
forall (f :: * -> *) a. Applicative f => a -> f a
pure BF
SFloat Concrete
x { bfValue :: BigFloat
FP.bfValue = BigFloat -> BigFloat
FP.bfNeg (BF -> BigFloat
FP.bfValue BF
SFloat Concrete
x) }
  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 BFOpts
opts <- Integer -> Integer -> RoundMode -> BFOpts
FP.fpOpts Integer
e Integer
p (RoundMode -> BFOpts) -> Eval RoundMode -> Eval BFOpts
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Concrete -> SWord Concrete -> SEval Concrete RoundMode
fpRoundMode Concrete
sym SWord Concrete
r
       BF -> Eval BF
forall (f :: * -> *) a. Applicative f => a -> f a
pure BF :: Integer -> Integer -> BigFloat -> BF
FP.BF { bfExpWidth :: Integer
FP.bfExpWidth = Integer
e
                  , bfPrecWidth :: Integer
FP.bfPrecWidth = Integer
p
                  , bfValue :: BigFloat
FP.bfValue = (BigFloat, Status) -> BigFloat
FP.fpCheckStatus ((BigFloat, Status) -> BigFloat) -> (BigFloat, Status) -> BigFloat
forall a b. (a -> b) -> a -> b
$
                                 BFOpts -> BigFloat -> (BigFloat, Status)
FP.bfRoundInt BFOpts
opts (Integer -> BigFloat
FP.bfFromInteger Integer
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


{-# INLINE liftBinIntMod #-}
liftBinIntMod :: Monad m =>
  (Integer -> Integer -> Integer) -> Integer -> Integer -> Integer -> m Integer
liftBinIntMod :: (Integer -> Integer -> Integer)
-> Integer -> Integer -> Integer -> m Integer
liftBinIntMod Integer -> Integer -> Integer
op Integer
m Integer
x Integer
y
  | Integer
m Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
0    = String -> [String] -> m Integer
forall a. HasCallStack => String -> [String] -> a
evalPanic String
"znArithmetic" [String
"0 modulus not allowed"]
  | Bool
otherwise = Integer -> m Integer
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Integer -> m Integer) -> Integer -> m Integer
forall a b. (a -> b) -> a -> b
$ (Integer -> Integer -> Integer
op Integer
x Integer
y) Integer -> Integer -> Integer
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 BF
SFloat Concrete
x) (BF -> Integer
FP.bfPrecWidth BF
SFloat Concrete
x)
                                                  (RoundMode -> BFOpts) -> Eval RoundMode -> Eval BFOpts
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Concrete -> SWord Concrete -> SEval Concrete RoundMode
fpRoundMode Concrete
sym SWord Concrete
r
     BF -> Eval BF
forall (f :: * -> *) a. Applicative f => a -> f a
pure BF
SFloat Concrete
x { bfValue :: BigFloat
FP.bfValue = (BigFloat, Status) -> BigFloat
FP.fpCheckStatus
                                (BFOpts -> BigFloat -> BigFloat -> (BigFloat, Status)
fun BFOpts
opts (BF -> BigFloat
FP.bfValue BF
SFloat Concrete
x) (BF -> BigFloat
FP.bfValue BF
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 BF
SFloat Concrete
flt of
       Right Integer
i -> Integer -> Eval Integer
forall (f :: * -> *) a. Applicative f => a -> f a
pure Integer
i
       Left EvalError
err -> Concrete -> EvalError -> SEval Concrete Integer
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
BV
w) of
    Left EvalError
err -> Concrete -> EvalError -> SEval Concrete RoundMode
forall sym a. Backend sym => sym -> EvalError -> SEval sym a
raiseError Concrete
sym EvalError
err
    Right RoundMode
a  -> RoundMode -> Eval RoundMode
forall (f :: * -> *) a. Applicative f => a -> f a
pure RoundMode
a