{-# LANGUAGE RecordWildCards #-}
{-# LANGUAGE PatternGuards #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE Rank2Types #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE ViewPatterns #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE TypeSynonymInstances #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}
module Cryptol.Symbolic.Prims where
import Control.Monad (unless)
import Data.Bits
import qualified Data.Sequence as Seq
import qualified Data.Foldable as Fold
import Cryptol.Eval.Monad (Eval(..), ready, invalidIndex, cryUserError)
import Cryptol.Eval.Type (finNat', TValue(..))
import Cryptol.Eval.Value (BitWord(..), EvalPrims(..), enumerateSeqMap, SeqMap(..),
reverseSeqMap, wlam, nlam, WordValue(..),
asWordVal, fromWordVal, fromBit,
enumerateWordValue, enumerateWordValueRev,
wordValueSize,
updateWordValue,
updateSeqMap, lookupSeqMap, memoMap )
import Cryptol.Prims.Eval (binary, unary, arithUnary,
arithBinary, Binary, BinArith,
logicBinary, logicUnary, zeroV,
ccatV, splitAtV, joinV, ecSplitV,
reverseV, infFromV, infFromThenV,
fromToV, fromThenToV,
transposeV, indexPrim,
ecToIntegerV, ecFromIntegerV,
ecNumberV, updatePrim, randomV, liftWord,
cmpValue, lg2)
import Cryptol.Symbolic.Value
import Cryptol.TypeCheck.AST (Decl(..))
import Cryptol.TypeCheck.Solver.InfNat (Nat'(..), widthInteger)
import Cryptol.ModuleSystem.Name (asPrim)
import Cryptol.Utils.Ident (Ident,mkIdent)
import qualified Data.SBV as SBV
import qualified Data.SBV.Dynamic as SBV
import qualified Data.Map as Map
import qualified Data.Text as T
import Prelude ()
import Prelude.Compat
import Control.Monad (join)
traverseSnd :: Functor f => (a -> f b) -> (t, a) -> f (t, b)
traverseSnd :: (a -> f b) -> (t, a) -> f (t, b)
traverseSnd f :: a -> f b
f (x :: t
x, y :: a
y) = (,) t
x (b -> (t, b)) -> f b -> f (t, b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> f b
f a
y
instance EvalPrims SBool SWord SInteger where
evalPrim :: Decl -> Maybe (GenValue SBool SBool SBool)
evalPrim Decl { dName :: Decl -> Name
dName = Name
n, .. } =
do Ident
prim <- Name -> Maybe Ident
asPrim Name
n
Ident
-> Map Ident (GenValue SBool SBool SBool)
-> Maybe (GenValue SBool SBool SBool)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Ident
prim Map Ident (GenValue SBool SBool SBool)
primTable
iteValue :: SBool
-> Eval (GenValue SBool SBool SBool)
-> Eval (GenValue SBool SBool SBool)
-> Eval (GenValue SBool SBool SBool)
iteValue b :: SBool
b x1 :: Eval (GenValue SBool SBool SBool)
x1 x2 :: Eval (GenValue SBool SBool SBool)
x2
| Just b' :: Bool
b' <- SBool -> Maybe Bool
SBV.svAsBool SBool
b = if Bool
b' then Eval (GenValue SBool SBool SBool)
x1 else Eval (GenValue SBool SBool SBool)
x2
| Bool
otherwise = do GenValue SBool SBool SBool
v1 <- Eval (GenValue SBool SBool SBool)
x1
GenValue SBool SBool SBool
v2 <- Eval (GenValue SBool SBool SBool)
x2
SBool
-> GenValue SBool SBool SBool
-> GenValue SBool SBool SBool
-> Eval (GenValue SBool SBool SBool)
iteSValue SBool
b GenValue SBool SBool SBool
v1 GenValue SBool SBool SBool
v2
primTable :: Map.Map Ident Value
primTable :: Map Ident (GenValue SBool SBool SBool)
primTable = [(Ident, GenValue SBool SBool SBool)]
-> Map Ident (GenValue SBool SBool SBool)
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ([(Ident, GenValue SBool SBool SBool)]
-> Map Ident (GenValue SBool SBool SBool))
-> [(Ident, GenValue SBool SBool SBool)]
-> Map Ident (GenValue SBool SBool SBool)
forall a b. (a -> b) -> a -> b
$ ((String, GenValue SBool SBool SBool)
-> (Ident, GenValue SBool SBool SBool))
-> [(String, GenValue SBool SBool SBool)]
-> [(Ident, GenValue SBool SBool SBool)]
forall a b. (a -> b) -> [a] -> [b]
map (\(n :: String
n, v :: GenValue SBool SBool SBool
v) -> (Text -> Ident
mkIdent (String -> Text
T.pack String
n), GenValue SBool SBool SBool
v))
[ ("True" , SBool -> GenValue SBool SBool SBool
forall b w i. b -> GenValue b w i
VBit SBool
SBV.svTrue)
, ("False" , SBool -> GenValue SBool SBool SBool
forall b w i. b -> GenValue b w i
VBit SBool
SBV.svFalse)
, ("number" , GenValue SBool SBool SBool
forall b w i. BitWord b w i => GenValue b w i
ecNumberV)
, ("+" , Binary SBool SBool SBool -> GenValue SBool SBool SBool
forall b w i. Binary b w i -> GenValue b w i
binary (BinArith SBool
-> (SBool -> SBool -> Eval SBool)
-> BinArith SBool
-> Binary SBool SBool SBool
forall b w i.
BitWord b w i =>
BinArith w
-> (i -> i -> Eval i)
-> (Integer -> i -> i -> Eval i)
-> Binary b w i
arithBinary ((SBool -> SBool -> SBool) -> BinArith SBool
liftBinArith SBool -> SBool -> SBool
SBV.svPlus) ((SBool -> SBool -> SBool) -> SBool -> SBool -> Eval SBool
forall a b c. (a -> b -> c) -> a -> b -> Eval c
liftBin SBool -> SBool -> SBool
SBV.svPlus)
BinArith SBool
sModAdd))
, ("-" , Binary SBool SBool SBool -> GenValue SBool SBool SBool
forall b w i. Binary b w i -> GenValue b w i
binary (BinArith SBool
-> (SBool -> SBool -> Eval SBool)
-> BinArith SBool
-> Binary SBool SBool SBool
forall b w i.
BitWord b w i =>
BinArith w
-> (i -> i -> Eval i)
-> (Integer -> i -> i -> Eval i)
-> Binary b w i
arithBinary ((SBool -> SBool -> SBool) -> BinArith SBool
liftBinArith SBool -> SBool -> SBool
SBV.svMinus) ((SBool -> SBool -> SBool) -> SBool -> SBool -> Eval SBool
forall a b c. (a -> b -> c) -> a -> b -> Eval c
liftBin SBool -> SBool -> SBool
SBV.svMinus)
BinArith SBool
sModSub))
, ("*" , Binary SBool SBool SBool -> GenValue SBool SBool SBool
forall b w i. Binary b w i -> GenValue b w i
binary (BinArith SBool
-> (SBool -> SBool -> Eval SBool)
-> BinArith SBool
-> Binary SBool SBool SBool
forall b w i.
BitWord b w i =>
BinArith w
-> (i -> i -> Eval i)
-> (Integer -> i -> i -> Eval i)
-> Binary b w i
arithBinary ((SBool -> SBool -> SBool) -> BinArith SBool
liftBinArith SBool -> SBool -> SBool
SBV.svTimes) ((SBool -> SBool -> SBool) -> SBool -> SBool -> Eval SBool
forall a b c. (a -> b -> c) -> a -> b -> Eval c
liftBin SBool -> SBool -> SBool
SBV.svTimes)
BinArith SBool
sModMult))
, ("/" , Binary SBool SBool SBool -> GenValue SBool SBool SBool
forall b w i. Binary b w i -> GenValue b w i
binary (BinArith SBool
-> (SBool -> SBool -> Eval SBool)
-> BinArith SBool
-> Binary SBool SBool SBool
forall b w i.
BitWord b w i =>
BinArith w
-> (i -> i -> Eval i)
-> (Integer -> i -> i -> Eval i)
-> Binary b w i
arithBinary ((SBool -> SBool -> SBool) -> BinArith SBool
liftBinArith SBool -> SBool -> SBool
SBV.svQuot) ((SBool -> SBool -> SBool) -> SBool -> SBool -> Eval SBool
forall a b c. (a -> b -> c) -> a -> b -> Eval c
liftBin SBool -> SBool -> SBool
SBV.svQuot)
((SBool -> SBool -> SBool) -> BinArith SBool
forall a.
(SBool -> SBool -> a) -> Integer -> SBool -> SBool -> Eval a
liftModBin SBool -> SBool -> SBool
SBV.svQuot)))
, ("%" , Binary SBool SBool SBool -> GenValue SBool SBool SBool
forall b w i. Binary b w i -> GenValue b w i
binary (BinArith SBool
-> (SBool -> SBool -> Eval SBool)
-> BinArith SBool
-> Binary SBool SBool SBool
forall b w i.
BitWord b w i =>
BinArith w
-> (i -> i -> Eval i)
-> (Integer -> i -> i -> Eval i)
-> Binary b w i
arithBinary ((SBool -> SBool -> SBool) -> BinArith SBool
liftBinArith SBool -> SBool -> SBool
SBV.svRem) ((SBool -> SBool -> SBool) -> SBool -> SBool -> Eval SBool
forall a b c. (a -> b -> c) -> a -> b -> Eval c
liftBin SBool -> SBool -> SBool
SBV.svRem)
((SBool -> SBool -> SBool) -> BinArith SBool
forall a.
(SBool -> SBool -> a) -> Integer -> SBool -> SBool -> Eval a
liftModBin SBool -> SBool -> SBool
SBV.svRem)))
, ("^^" , Binary SBool SBool SBool -> GenValue SBool SBool SBool
forall b w i. Binary b w i -> GenValue b w i
binary (BinArith SBool
-> (SBool -> SBool -> Eval SBool)
-> BinArith SBool
-> Binary SBool SBool SBool
forall b w i.
BitWord b w i =>
BinArith w
-> (i -> i -> Eval i)
-> (Integer -> i -> i -> Eval i)
-> Binary b w i
arithBinary BinArith SBool
sExp ((SBool -> SBool -> SBool) -> SBool -> SBool -> Eval SBool
forall a b c. (a -> b -> c) -> a -> b -> Eval c
liftBin SBool -> SBool -> SBool
SBV.svExp)
BinArith SBool
sModExp))
, ("lg2" , Unary SBool SBool SBool -> GenValue SBool SBool SBool
forall b w i. Unary b w i -> GenValue b w i
unary (UnaryArith SBool
-> (SBool -> Eval SBool)
-> UnaryArith SBool
-> Unary SBool SBool SBool
forall b w i.
BitWord b w i =>
UnaryArith w
-> (i -> Eval i) -> (Integer -> i -> Eval i) -> Unary b w i
arithUnary UnaryArith SBool
sLg2 SBool -> Eval SBool
svLg2 UnaryArith SBool
svModLg2))
, ("negate" , Unary SBool SBool SBool -> GenValue SBool SBool SBool
forall b w i. Unary b w i -> GenValue b w i
unary (UnaryArith SBool
-> (SBool -> Eval SBool)
-> UnaryArith SBool
-> Unary SBool SBool SBool
forall b w i.
BitWord b w i =>
UnaryArith w
-> (i -> Eval i) -> (Integer -> i -> Eval i) -> Unary b w i
arithUnary (\_ -> SBool -> Eval SBool
forall a. a -> Eval a
ready (SBool -> Eval SBool) -> (SBool -> SBool) -> SBool -> Eval SBool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SBool -> SBool
SBV.svUNeg) (SBool -> Eval SBool
forall a. a -> Eval a
ready (SBool -> Eval SBool) -> (SBool -> SBool) -> SBool -> Eval SBool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SBool -> SBool
SBV.svUNeg)
((SBool -> Eval SBool) -> UnaryArith SBool
forall a b. a -> b -> a
const (SBool -> Eval SBool
forall a. a -> Eval a
ready (SBool -> Eval SBool) -> (SBool -> SBool) -> SBool -> Eval SBool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SBool -> SBool
SBV.svUNeg))))
, ("<" , Binary SBool SBool SBool -> GenValue SBool SBool SBool
forall b w i. Binary b w i -> GenValue b w i
binary ((SBool -> SBool -> Eval SBool -> Eval SBool)
-> (SBool -> SBool -> Eval SBool -> Eval SBool)
-> (SBool -> SBool -> Eval SBool -> Eval SBool)
-> (Integer -> SBool -> SBool -> Eval SBool -> Eval SBool)
-> SBool
-> Binary SBool SBool SBool
cmpBinary SBool -> SBool -> Eval SBool -> Eval SBool
cmpLt SBool -> SBool -> Eval SBool -> Eval SBool
cmpLt SBool -> SBool -> Eval SBool -> Eval SBool
cmpLt ((SBool -> SBool -> Eval SBool -> Eval SBool)
-> Integer -> SBool -> SBool -> Eval SBool -> Eval SBool
cmpMod SBool -> SBool -> Eval SBool -> Eval SBool
cmpLt) SBool
SBV.svFalse))
, (">" , Binary SBool SBool SBool -> GenValue SBool SBool SBool
forall b w i. Binary b w i -> GenValue b w i
binary ((SBool -> SBool -> Eval SBool -> Eval SBool)
-> (SBool -> SBool -> Eval SBool -> Eval SBool)
-> (SBool -> SBool -> Eval SBool -> Eval SBool)
-> (Integer -> SBool -> SBool -> Eval SBool -> Eval SBool)
-> SBool
-> Binary SBool SBool SBool
cmpBinary SBool -> SBool -> Eval SBool -> Eval SBool
cmpGt SBool -> SBool -> Eval SBool -> Eval SBool
cmpGt SBool -> SBool -> Eval SBool -> Eval SBool
cmpGt ((SBool -> SBool -> Eval SBool -> Eval SBool)
-> Integer -> SBool -> SBool -> Eval SBool -> Eval SBool
cmpMod SBool -> SBool -> Eval SBool -> Eval SBool
cmpGt) SBool
SBV.svFalse))
, ("<=" , Binary SBool SBool SBool -> GenValue SBool SBool SBool
forall b w i. Binary b w i -> GenValue b w i
binary ((SBool -> SBool -> Eval SBool -> Eval SBool)
-> (SBool -> SBool -> Eval SBool -> Eval SBool)
-> (SBool -> SBool -> Eval SBool -> Eval SBool)
-> (Integer -> SBool -> SBool -> Eval SBool -> Eval SBool)
-> SBool
-> Binary SBool SBool SBool
cmpBinary SBool -> SBool -> Eval SBool -> Eval SBool
cmpLtEq SBool -> SBool -> Eval SBool -> Eval SBool
cmpLtEq SBool -> SBool -> Eval SBool -> Eval SBool
cmpLtEq ((SBool -> SBool -> Eval SBool -> Eval SBool)
-> Integer -> SBool -> SBool -> Eval SBool -> Eval SBool
cmpMod SBool -> SBool -> Eval SBool -> Eval SBool
cmpLtEq) SBool
SBV.svTrue))
, (">=" , Binary SBool SBool SBool -> GenValue SBool SBool SBool
forall b w i. Binary b w i -> GenValue b w i
binary ((SBool -> SBool -> Eval SBool -> Eval SBool)
-> (SBool -> SBool -> Eval SBool -> Eval SBool)
-> (SBool -> SBool -> Eval SBool -> Eval SBool)
-> (Integer -> SBool -> SBool -> Eval SBool -> Eval SBool)
-> SBool
-> Binary SBool SBool SBool
cmpBinary SBool -> SBool -> Eval SBool -> Eval SBool
cmpGtEq SBool -> SBool -> Eval SBool -> Eval SBool
cmpGtEq SBool -> SBool -> Eval SBool -> Eval SBool
cmpGtEq ((SBool -> SBool -> Eval SBool -> Eval SBool)
-> Integer -> SBool -> SBool -> Eval SBool -> Eval SBool
cmpMod SBool -> SBool -> Eval SBool -> Eval SBool
cmpGtEq) SBool
SBV.svTrue))
, ("==" , Binary SBool SBool SBool -> GenValue SBool SBool SBool
forall b w i. Binary b w i -> GenValue b w i
binary ((SBool -> SBool -> Eval SBool -> Eval SBool)
-> (SBool -> SBool -> Eval SBool -> Eval SBool)
-> (SBool -> SBool -> Eval SBool -> Eval SBool)
-> (Integer -> SBool -> SBool -> Eval SBool -> Eval SBool)
-> SBool
-> Binary SBool SBool SBool
cmpBinary SBool -> SBool -> Eval SBool -> Eval SBool
cmpEq SBool -> SBool -> Eval SBool -> Eval SBool
cmpEq SBool -> SBool -> Eval SBool -> Eval SBool
cmpEq Integer -> SBool -> SBool -> Eval SBool -> Eval SBool
cmpModEq SBool
SBV.svTrue))
, ("!=" , Binary SBool SBool SBool -> GenValue SBool SBool SBool
forall b w i. Binary b w i -> GenValue b w i
binary ((SBool -> SBool -> Eval SBool -> Eval SBool)
-> (SBool -> SBool -> Eval SBool -> Eval SBool)
-> (SBool -> SBool -> Eval SBool -> Eval SBool)
-> (Integer -> SBool -> SBool -> Eval SBool -> Eval SBool)
-> SBool
-> Binary SBool SBool SBool
cmpBinary SBool -> SBool -> Eval SBool -> Eval SBool
cmpNotEq SBool -> SBool -> Eval SBool -> Eval SBool
cmpNotEq SBool -> SBool -> Eval SBool -> Eval SBool
cmpNotEq Integer -> SBool -> SBool -> Eval SBool -> Eval SBool
cmpModNotEq SBool
SBV.svFalse))
, ("<$" , let boolFail :: a
boolFail = String -> [String] -> a
forall a. String -> [String] -> a
evalPanic "<$" ["Attempted signed comparison on bare Bit values"]
intFail :: a
intFail = String -> [String] -> a
forall a. String -> [String] -> a
evalPanic "<$" ["Attempted signed comparison on Integer values"]
in Binary SBool SBool SBool -> GenValue SBool SBool SBool
forall b w i. Binary b w i -> GenValue b w i
binary ((SBool -> SBool -> Eval SBool -> Eval SBool)
-> (SBool -> SBool -> Eval SBool -> Eval SBool)
-> (SBool -> SBool -> Eval SBool -> Eval SBool)
-> (Integer -> SBool -> SBool -> Eval SBool -> Eval SBool)
-> SBool
-> Binary SBool SBool SBool
cmpBinary SBool -> SBool -> Eval SBool -> Eval SBool
forall a. a
boolFail SBool -> SBool -> Eval SBool -> Eval SBool
cmpSignedLt SBool -> SBool -> Eval SBool -> Eval SBool
forall a. a
intFail ((SBool -> SBool -> Eval SBool -> Eval SBool)
-> Integer -> SBool -> SBool -> Eval SBool -> Eval SBool
forall a b. a -> b -> a
const SBool -> SBool -> Eval SBool -> Eval SBool
forall a. a
intFail) SBool
SBV.svFalse))
, ("/$" , Binary SBool SBool SBool -> GenValue SBool SBool SBool
forall b w i. Binary b w i -> GenValue b w i
binary (BinArith SBool
-> (SBool -> SBool -> Eval SBool)
-> BinArith SBool
-> Binary SBool SBool SBool
forall b w i.
BitWord b w i =>
BinArith w
-> (i -> i -> Eval i)
-> (Integer -> i -> i -> Eval i)
-> Binary b w i
arithBinary ((SBool -> SBool -> SBool) -> BinArith SBool
liftBinArith SBool -> SBool -> SBool
signedQuot) ((SBool -> SBool -> SBool) -> SBool -> SBool -> Eval SBool
forall a b c. (a -> b -> c) -> a -> b -> Eval c
liftBin SBool -> SBool -> SBool
SBV.svQuot)
((SBool -> SBool -> SBool) -> BinArith SBool
forall a.
(SBool -> SBool -> a) -> Integer -> SBool -> SBool -> Eval a
liftModBin SBool -> SBool -> SBool
SBV.svQuot)))
, ("%$" , Binary SBool SBool SBool -> GenValue SBool SBool SBool
forall b w i. Binary b w i -> GenValue b w i
binary (BinArith SBool
-> (SBool -> SBool -> Eval SBool)
-> BinArith SBool
-> Binary SBool SBool SBool
forall b w i.
BitWord b w i =>
BinArith w
-> (i -> i -> Eval i)
-> (Integer -> i -> i -> Eval i)
-> Binary b w i
arithBinary ((SBool -> SBool -> SBool) -> BinArith SBool
liftBinArith SBool -> SBool -> SBool
signedRem) ((SBool -> SBool -> SBool) -> SBool -> SBool -> Eval SBool
forall a b c. (a -> b -> c) -> a -> b -> Eval c
liftBin SBool -> SBool -> SBool
SBV.svRem)
((SBool -> SBool -> SBool) -> BinArith SBool
forall a.
(SBool -> SBool -> a) -> Integer -> SBool -> SBool -> Eval a
liftModBin SBool -> SBool -> SBool
SBV.svRem)))
, (">>$" , GenValue SBool SBool SBool
sshrV)
, ("&&" , Binary SBool SBool SBool -> GenValue SBool SBool SBool
forall b w i. Binary b w i -> GenValue b w i
binary ((SBool -> SBool -> SBool)
-> (SBool -> SBool -> SBool) -> Binary SBool SBool SBool
forall b w i.
BitWord b w i =>
(b -> b -> b) -> (w -> w -> w) -> Binary b w i
logicBinary SBool -> SBool -> SBool
SBV.svAnd SBool -> SBool -> SBool
SBV.svAnd))
, ("||" , Binary SBool SBool SBool -> GenValue SBool SBool SBool
forall b w i. Binary b w i -> GenValue b w i
binary ((SBool -> SBool -> SBool)
-> (SBool -> SBool -> SBool) -> Binary SBool SBool SBool
forall b w i.
BitWord b w i =>
(b -> b -> b) -> (w -> w -> w) -> Binary b w i
logicBinary SBool -> SBool -> SBool
SBV.svOr SBool -> SBool -> SBool
SBV.svOr))
, ("^" , Binary SBool SBool SBool -> GenValue SBool SBool SBool
forall b w i. Binary b w i -> GenValue b w i
binary ((SBool -> SBool -> SBool)
-> (SBool -> SBool -> SBool) -> Binary SBool SBool SBool
forall b w i.
BitWord b w i =>
(b -> b -> b) -> (w -> w -> w) -> Binary b w i
logicBinary SBool -> SBool -> SBool
SBV.svXOr SBool -> SBool -> SBool
SBV.svXOr))
, ("complement" , Unary SBool SBool SBool -> GenValue SBool SBool SBool
forall b w i. Unary b w i -> GenValue b w i
unary ((SBool -> SBool) -> (SBool -> SBool) -> Unary SBool SBool SBool
forall b w i. BitWord b w i => (b -> b) -> (w -> w) -> Unary b w i
logicUnary SBool -> SBool
SBV.svNot SBool -> SBool
SBV.svNot))
, ("zero" , (TValue -> GenValue SBool SBool SBool)
-> GenValue SBool SBool SBool
forall b w i. (TValue -> GenValue b w i) -> GenValue b w i
tlam TValue -> GenValue SBool SBool SBool
forall b w i. BitWord b w i => TValue -> GenValue b w i
zeroV)
, ("toInteger" , GenValue SBool SBool SBool
forall b w i. BitWord b w i => GenValue b w i
ecToIntegerV)
, ("fromInteger" , (Integer -> SBool -> SBool) -> GenValue SBool SBool SBool
forall b w i.
BitWord b w i =>
(Integer -> i -> i) -> GenValue b w i
ecFromIntegerV ((SBool -> SBool) -> Integer -> SBool -> SBool
forall a b. a -> b -> a
const SBool -> SBool
forall a. a -> a
id))
, ("fromZ" , (Nat' -> GenValue SBool SBool SBool) -> GenValue SBool SBool SBool
forall b w i. (Nat' -> GenValue b w i) -> GenValue b w i
nlam ((Nat' -> GenValue SBool SBool SBool)
-> GenValue SBool SBool SBool)
-> (Nat' -> GenValue SBool SBool SBool)
-> GenValue SBool SBool SBool
forall a b. (a -> b) -> a -> b
$ \ modulus :: Nat'
modulus ->
(Eval (GenValue SBool SBool SBool)
-> Eval (GenValue SBool SBool SBool))
-> GenValue SBool SBool SBool
forall b w i.
(Eval (GenValue b w i) -> Eval (GenValue b w i)) -> GenValue b w i
lam ((Eval (GenValue SBool SBool SBool)
-> Eval (GenValue SBool SBool SBool))
-> GenValue SBool SBool SBool)
-> (Eval (GenValue SBool SBool SBool)
-> Eval (GenValue SBool SBool SBool))
-> GenValue SBool SBool SBool
forall a b. (a -> b) -> a -> b
$ \ x :: Eval (GenValue SBool SBool SBool)
x -> do
GenValue SBool SBool SBool
val <- Eval (GenValue SBool SBool SBool)
x
case (Nat'
modulus, GenValue SBool SBool SBool
val) of
(Nat n :: Integer
n, VInteger i :: SBool
i) -> GenValue SBool SBool SBool -> Eval (GenValue SBool SBool SBool)
forall (m :: * -> *) a. Monad m => a -> m a
return (GenValue SBool SBool SBool -> Eval (GenValue SBool SBool SBool))
-> GenValue SBool SBool SBool -> Eval (GenValue SBool SBool SBool)
forall a b. (a -> b) -> a -> b
$ SBool -> GenValue SBool SBool SBool
forall b w i. i -> GenValue b w i
VInteger (SBool -> SBool -> SBool
SBV.svRem SBool
i (Integer -> SBool
forall b w i. BitWord b w i => Integer -> i
integerLit Integer
n))
_ -> String -> [String] -> Eval (GenValue SBool SBool SBool)
forall a. String -> [String] -> a
evalPanic "fromZ" ["Invalid arguments"])
, ("<<" , String
-> (SBool -> SBool -> SBool)
-> (Nat' -> Integer -> Integer -> Maybe Integer)
-> GenValue SBool SBool SBool
logicShift "<<"
SBool -> SBool -> SBool
SBV.svShiftLeft
(\sz :: Nat'
sz i :: Integer
i shft :: Integer
shft ->
case Nat'
sz of
Inf -> Integer -> Maybe Integer
forall a. a -> Maybe a
Just (Integer
iInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
+Integer
shft)
Nat n :: Integer
n
| Integer
iInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
+Integer
shft Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= Integer
n -> Maybe Integer
forall a. Maybe a
Nothing
| Bool
otherwise -> Integer -> Maybe Integer
forall a. a -> Maybe a
Just (Integer
iInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
+Integer
shft)))
, (">>" , String
-> (SBool -> SBool -> SBool)
-> (Nat' -> Integer -> Integer -> Maybe Integer)
-> GenValue SBool SBool SBool
logicShift ">>"
SBool -> SBool -> SBool
SBV.svShiftRight
(\_sz :: Nat'
_sz i :: Integer
i shft :: Integer
shft ->
if Integer
iInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
-Integer
shft Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< 0 then Maybe Integer
forall a. Maybe a
Nothing else Integer -> Maybe Integer
forall a. a -> Maybe a
Just (Integer
iInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
-Integer
shft)))
, ("<<<" , String
-> (SBool -> SBool -> SBool)
-> (Nat' -> Integer -> Integer -> Maybe Integer)
-> GenValue SBool SBool SBool
logicShift "<<<"
SBool -> SBool -> SBool
SBV.svRotateLeft
(\sz :: Nat'
sz i :: Integer
i shft :: Integer
shft ->
case Nat'
sz of
Inf -> String -> [String] -> Maybe Integer
forall a. String -> [String] -> a
evalPanic "cannot rotate infinite sequence" []
Nat n :: Integer
n -> Integer -> Maybe Integer
forall a. a -> Maybe a
Just ((Integer
iInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
+Integer
shft) Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`mod` Integer
n)))
, (">>>" , String
-> (SBool -> SBool -> SBool)
-> (Nat' -> Integer -> Integer -> Maybe Integer)
-> GenValue SBool SBool SBool
logicShift ">>>"
SBool -> SBool -> SBool
SBV.svRotateRight
(\sz :: Nat'
sz i :: Integer
i shft :: Integer
shft ->
case Nat'
sz of
Inf -> String -> [String] -> Maybe Integer
forall a. String -> [String] -> a
evalPanic "cannot rotate infinite sequence" []
Nat n :: Integer
n -> Integer -> Maybe Integer
forall a. a -> Maybe a
Just ((Integer
iInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
+Integer
nInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
-Integer
shft) Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`mod` Integer
n)))
, ("carry" , (SBool -> SBool -> Eval (GenValue SBool SBool SBool))
-> GenValue SBool SBool SBool
forall b w i.
BitWord b w i =>
(w -> w -> Eval (GenValue b w i)) -> GenValue b w i
liftWord SBool -> SBool -> Eval (GenValue SBool SBool SBool)
carry)
, ("scarry" , (SBool -> SBool -> Eval (GenValue SBool SBool SBool))
-> GenValue SBool SBool SBool
forall b w i.
BitWord b w i =>
(w -> w -> Eval (GenValue b w i)) -> GenValue b w i
liftWord SBool -> SBool -> Eval (GenValue SBool SBool SBool)
scarry)
, ("#" ,
(Nat' -> GenValue SBool SBool SBool) -> GenValue SBool SBool SBool
forall b w i. (Nat' -> GenValue b w i) -> GenValue b w i
nlam ((Nat' -> GenValue SBool SBool SBool)
-> GenValue SBool SBool SBool)
-> (Nat' -> GenValue SBool SBool SBool)
-> GenValue SBool SBool SBool
forall a b. (a -> b) -> a -> b
$ \ front :: Nat'
front ->
(Nat' -> GenValue SBool SBool SBool) -> GenValue SBool SBool SBool
forall b w i. (Nat' -> GenValue b w i) -> GenValue b w i
nlam ((Nat' -> GenValue SBool SBool SBool)
-> GenValue SBool SBool SBool)
-> (Nat' -> GenValue SBool SBool SBool)
-> GenValue SBool SBool SBool
forall a b. (a -> b) -> a -> b
$ \ back :: Nat'
back ->
(TValue -> GenValue SBool SBool SBool)
-> GenValue SBool SBool SBool
forall b w i. (TValue -> GenValue b w i) -> GenValue b w i
tlam ((TValue -> GenValue SBool SBool SBool)
-> GenValue SBool SBool SBool)
-> (TValue -> GenValue SBool SBool SBool)
-> GenValue SBool SBool SBool
forall a b. (a -> b) -> a -> b
$ \ elty :: TValue
elty ->
(Eval (GenValue SBool SBool SBool)
-> Eval (GenValue SBool SBool SBool))
-> GenValue SBool SBool SBool
forall b w i.
(Eval (GenValue b w i) -> Eval (GenValue b w i)) -> GenValue b w i
lam ((Eval (GenValue SBool SBool SBool)
-> Eval (GenValue SBool SBool SBool))
-> GenValue SBool SBool SBool)
-> (Eval (GenValue SBool SBool SBool)
-> Eval (GenValue SBool SBool SBool))
-> GenValue SBool SBool SBool
forall a b. (a -> b) -> a -> b
$ \ l :: Eval (GenValue SBool SBool SBool)
l -> GenValue SBool SBool SBool -> Eval (GenValue SBool SBool SBool)
forall (m :: * -> *) a. Monad m => a -> m a
return (GenValue SBool SBool SBool -> Eval (GenValue SBool SBool SBool))
-> GenValue SBool SBool SBool -> Eval (GenValue SBool SBool SBool)
forall a b. (a -> b) -> a -> b
$
(Eval (GenValue SBool SBool SBool)
-> Eval (GenValue SBool SBool SBool))
-> GenValue SBool SBool SBool
forall b w i.
(Eval (GenValue b w i) -> Eval (GenValue b w i)) -> GenValue b w i
lam ((Eval (GenValue SBool SBool SBool)
-> Eval (GenValue SBool SBool SBool))
-> GenValue SBool SBool SBool)
-> (Eval (GenValue SBool SBool SBool)
-> Eval (GenValue SBool SBool SBool))
-> GenValue SBool SBool SBool
forall a b. (a -> b) -> a -> b
$ \ r :: Eval (GenValue SBool SBool SBool)
r -> Eval (Eval (GenValue SBool SBool SBool))
-> Eval (GenValue SBool SBool SBool)
forall (m :: * -> *) a. Monad m => m (m a) -> m a
join (Nat' -> Nat' -> Binary SBool SBool SBool
forall b w i.
(Show b, Show w, BitWord b w i) =>
Nat'
-> Nat'
-> TValue
-> GenValue b w i
-> GenValue b w i
-> Eval (GenValue b w i)
ccatV Nat'
front Nat'
back TValue
elty (GenValue SBool SBool SBool
-> GenValue SBool SBool SBool -> Eval (GenValue SBool SBool SBool))
-> Eval (GenValue SBool SBool SBool)
-> Eval
(GenValue SBool SBool SBool -> Eval (GenValue SBool SBool SBool))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Eval (GenValue SBool SBool SBool)
l Eval
(GenValue SBool SBool SBool -> Eval (GenValue SBool SBool SBool))
-> Eval (GenValue SBool SBool SBool)
-> Eval (Eval (GenValue SBool SBool SBool))
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Eval (GenValue SBool SBool SBool)
r))
, ("splitAt" ,
(Nat' -> GenValue SBool SBool SBool) -> GenValue SBool SBool SBool
forall b w i. (Nat' -> GenValue b w i) -> GenValue b w i
nlam ((Nat' -> GenValue SBool SBool SBool)
-> GenValue SBool SBool SBool)
-> (Nat' -> GenValue SBool SBool SBool)
-> GenValue SBool SBool SBool
forall a b. (a -> b) -> a -> b
$ \ front :: Nat'
front ->
(Nat' -> GenValue SBool SBool SBool) -> GenValue SBool SBool SBool
forall b w i. (Nat' -> GenValue b w i) -> GenValue b w i
nlam ((Nat' -> GenValue SBool SBool SBool)
-> GenValue SBool SBool SBool)
-> (Nat' -> GenValue SBool SBool SBool)
-> GenValue SBool SBool SBool
forall a b. (a -> b) -> a -> b
$ \ back :: Nat'
back ->
(TValue -> GenValue SBool SBool SBool)
-> GenValue SBool SBool SBool
forall b w i. (TValue -> GenValue b w i) -> GenValue b w i
tlam ((TValue -> GenValue SBool SBool SBool)
-> GenValue SBool SBool SBool)
-> (TValue -> GenValue SBool SBool SBool)
-> GenValue SBool SBool SBool
forall a b. (a -> b) -> a -> b
$ \ a :: TValue
a ->
(Eval (GenValue SBool SBool SBool)
-> Eval (GenValue SBool SBool SBool))
-> GenValue SBool SBool SBool
forall b w i.
(Eval (GenValue b w i) -> Eval (GenValue b w i)) -> GenValue b w i
lam ((Eval (GenValue SBool SBool SBool)
-> Eval (GenValue SBool SBool SBool))
-> GenValue SBool SBool SBool)
-> (Eval (GenValue SBool SBool SBool)
-> Eval (GenValue SBool SBool SBool))
-> GenValue SBool SBool SBool
forall a b. (a -> b) -> a -> b
$ \ x :: Eval (GenValue SBool SBool SBool)
x ->
Nat' -> Nat' -> Unary SBool SBool SBool
forall b w i.
BitWord b w i =>
Nat' -> Nat' -> TValue -> GenValue b w i -> Eval (GenValue b w i)
splitAtV Nat'
front Nat'
back TValue
a (GenValue SBool SBool SBool -> Eval (GenValue SBool SBool SBool))
-> Eval (GenValue SBool SBool SBool)
-> Eval (GenValue SBool SBool SBool)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Eval (GenValue SBool SBool SBool)
x)
, ("join" ,
(Nat' -> GenValue SBool SBool SBool) -> GenValue SBool SBool SBool
forall b w i. (Nat' -> GenValue b w i) -> GenValue b w i
nlam ((Nat' -> GenValue SBool SBool SBool)
-> GenValue SBool SBool SBool)
-> (Nat' -> GenValue SBool SBool SBool)
-> GenValue SBool SBool SBool
forall a b. (a -> b) -> a -> b
$ \ parts :: Nat'
parts ->
(Nat' -> GenValue SBool SBool SBool) -> GenValue SBool SBool SBool
forall b w i. (Nat' -> GenValue b w i) -> GenValue b w i
nlam ((Nat' -> GenValue SBool SBool SBool)
-> GenValue SBool SBool SBool)
-> (Nat' -> GenValue SBool SBool SBool)
-> GenValue SBool SBool SBool
forall a b. (a -> b) -> a -> b
$ \ (Nat' -> Integer
finNat' -> Integer
each) ->
(TValue -> GenValue SBool SBool SBool)
-> GenValue SBool SBool SBool
forall b w i. (TValue -> GenValue b w i) -> GenValue b w i
tlam ((TValue -> GenValue SBool SBool SBool)
-> GenValue SBool SBool SBool)
-> (TValue -> GenValue SBool SBool SBool)
-> GenValue SBool SBool SBool
forall a b. (a -> b) -> a -> b
$ \ a :: TValue
a ->
(Eval (GenValue SBool SBool SBool)
-> Eval (GenValue SBool SBool SBool))
-> GenValue SBool SBool SBool
forall b w i.
(Eval (GenValue b w i) -> Eval (GenValue b w i)) -> GenValue b w i
lam ((Eval (GenValue SBool SBool SBool)
-> Eval (GenValue SBool SBool SBool))
-> GenValue SBool SBool SBool)
-> (Eval (GenValue SBool SBool SBool)
-> Eval (GenValue SBool SBool SBool))
-> GenValue SBool SBool SBool
forall a b. (a -> b) -> a -> b
$ \ x :: Eval (GenValue SBool SBool SBool)
x ->
Nat' -> Integer -> Unary SBool SBool SBool
forall b w i.
BitWord b w i =>
Nat'
-> Integer -> TValue -> GenValue b w i -> Eval (GenValue b w i)
joinV Nat'
parts Integer
each TValue
a (GenValue SBool SBool SBool -> Eval (GenValue SBool SBool SBool))
-> Eval (GenValue SBool SBool SBool)
-> Eval (GenValue SBool SBool SBool)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Eval (GenValue SBool SBool SBool)
x)
, ("split" , GenValue SBool SBool SBool
forall b w i. BitWord b w i => GenValue b w i
ecSplitV)
, ("reverse" , (Nat' -> GenValue SBool SBool SBool) -> GenValue SBool SBool SBool
forall b w i. (Nat' -> GenValue b w i) -> GenValue b w i
nlam ((Nat' -> GenValue SBool SBool SBool)
-> GenValue SBool SBool SBool)
-> (Nat' -> GenValue SBool SBool SBool)
-> GenValue SBool SBool SBool
forall a b. (a -> b) -> a -> b
$ \_a :: Nat'
_a ->
(TValue -> GenValue SBool SBool SBool)
-> GenValue SBool SBool SBool
forall b w i. (TValue -> GenValue b w i) -> GenValue b w i
tlam ((TValue -> GenValue SBool SBool SBool)
-> GenValue SBool SBool SBool)
-> (TValue -> GenValue SBool SBool SBool)
-> GenValue SBool SBool SBool
forall a b. (a -> b) -> a -> b
$ \_b :: TValue
_b ->
(Eval (GenValue SBool SBool SBool)
-> Eval (GenValue SBool SBool SBool))
-> GenValue SBool SBool SBool
forall b w i.
(Eval (GenValue b w i) -> Eval (GenValue b w i)) -> GenValue b w i
lam ((Eval (GenValue SBool SBool SBool)
-> Eval (GenValue SBool SBool SBool))
-> GenValue SBool SBool SBool)
-> (Eval (GenValue SBool SBool SBool)
-> Eval (GenValue SBool SBool SBool))
-> GenValue SBool SBool SBool
forall a b. (a -> b) -> a -> b
$ \xs :: Eval (GenValue SBool SBool SBool)
xs -> GenValue SBool SBool SBool -> Eval (GenValue SBool SBool SBool)
forall b w i.
BitWord b w i =>
GenValue b w i -> Eval (GenValue b w i)
reverseV (GenValue SBool SBool SBool -> Eval (GenValue SBool SBool SBool))
-> Eval (GenValue SBool SBool SBool)
-> Eval (GenValue SBool SBool SBool)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Eval (GenValue SBool SBool SBool)
xs)
, ("transpose" , (Nat' -> GenValue SBool SBool SBool) -> GenValue SBool SBool SBool
forall b w i. (Nat' -> GenValue b w i) -> GenValue b w i
nlam ((Nat' -> GenValue SBool SBool SBool)
-> GenValue SBool SBool SBool)
-> (Nat' -> GenValue SBool SBool SBool)
-> GenValue SBool SBool SBool
forall a b. (a -> b) -> a -> b
$ \a :: Nat'
a ->
(Nat' -> GenValue SBool SBool SBool) -> GenValue SBool SBool SBool
forall b w i. (Nat' -> GenValue b w i) -> GenValue b w i
nlam ((Nat' -> GenValue SBool SBool SBool)
-> GenValue SBool SBool SBool)
-> (Nat' -> GenValue SBool SBool SBool)
-> GenValue SBool SBool SBool
forall a b. (a -> b) -> a -> b
$ \b :: Nat'
b ->
(TValue -> GenValue SBool SBool SBool)
-> GenValue SBool SBool SBool
forall b w i. (TValue -> GenValue b w i) -> GenValue b w i
tlam ((TValue -> GenValue SBool SBool SBool)
-> GenValue SBool SBool SBool)
-> (TValue -> GenValue SBool SBool SBool)
-> GenValue SBool SBool SBool
forall a b. (a -> b) -> a -> b
$ \c :: TValue
c ->
(Eval (GenValue SBool SBool SBool)
-> Eval (GenValue SBool SBool SBool))
-> GenValue SBool SBool SBool
forall b w i.
(Eval (GenValue b w i) -> Eval (GenValue b w i)) -> GenValue b w i
lam ((Eval (GenValue SBool SBool SBool)
-> Eval (GenValue SBool SBool SBool))
-> GenValue SBool SBool SBool)
-> (Eval (GenValue SBool SBool SBool)
-> Eval (GenValue SBool SBool SBool))
-> GenValue SBool SBool SBool
forall a b. (a -> b) -> a -> b
$ \xs :: Eval (GenValue SBool SBool SBool)
xs -> Nat' -> Nat' -> Unary SBool SBool SBool
forall b w i.
BitWord b w i =>
Nat' -> Nat' -> TValue -> GenValue b w i -> Eval (GenValue b w i)
transposeV Nat'
a Nat'
b TValue
c (GenValue SBool SBool SBool -> Eval (GenValue SBool SBool SBool))
-> Eval (GenValue SBool SBool SBool)
-> Eval (GenValue SBool SBool SBool)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Eval (GenValue SBool SBool SBool)
xs)
, ("fromTo" , GenValue SBool SBool SBool
forall b w i. BitWord b w i => GenValue b w i
fromToV)
, ("fromThenTo" , GenValue SBool SBool SBool
forall b w i. BitWord b w i => GenValue b w i
fromThenToV)
, ("infFrom" , GenValue SBool SBool SBool
forall b w i. BitWord b w i => GenValue b w i
infFromV)
, ("infFromThen" , GenValue SBool SBool SBool
forall b w i. BitWord b w i => GenValue b w i
infFromThenV)
, ("@" , (Maybe Integer
-> TValue
-> SeqMap SBool SBool SBool
-> Seq SBool
-> Eval (GenValue SBool SBool SBool))
-> (Maybe Integer
-> TValue
-> SeqMap SBool SBool SBool
-> SBool
-> Eval (GenValue SBool SBool SBool))
-> GenValue SBool SBool SBool
forall b w i.
BitWord b w i =>
(Maybe Integer
-> TValue -> SeqMap b w i -> Seq b -> Eval (GenValue b w i))
-> (Maybe Integer
-> TValue -> SeqMap b w i -> w -> Eval (GenValue b w i))
-> GenValue b w i
indexPrim Maybe Integer
-> TValue
-> SeqMap SBool SBool SBool
-> Seq SBool
-> Eval (GenValue SBool SBool SBool)
indexFront_bits Maybe Integer
-> TValue
-> SeqMap SBool SBool SBool
-> SBool
-> Eval (GenValue SBool SBool SBool)
indexFront)
, ("!" , (Maybe Integer
-> TValue
-> SeqMap SBool SBool SBool
-> Seq SBool
-> Eval (GenValue SBool SBool SBool))
-> (Maybe Integer
-> TValue
-> SeqMap SBool SBool SBool
-> SBool
-> Eval (GenValue SBool SBool SBool))
-> GenValue SBool SBool SBool
forall b w i.
BitWord b w i =>
(Maybe Integer
-> TValue -> SeqMap b w i -> Seq b -> Eval (GenValue b w i))
-> (Maybe Integer
-> TValue -> SeqMap b w i -> w -> Eval (GenValue b w i))
-> GenValue b w i
indexPrim Maybe Integer
-> TValue
-> SeqMap SBool SBool SBool
-> Seq SBool
-> Eval (GenValue SBool SBool SBool)
indexBack_bits Maybe Integer
-> TValue
-> SeqMap SBool SBool SBool
-> SBool
-> Eval (GenValue SBool SBool SBool)
indexBack)
, ("update" , (Nat'
-> TValue
-> WordValue SBool SBool SBool
-> WordValue SBool SBool SBool
-> Eval (GenValue SBool SBool SBool)
-> Eval (WordValue SBool SBool SBool))
-> (Nat'
-> TValue
-> SeqMap SBool SBool SBool
-> WordValue SBool SBool SBool
-> Eval (GenValue SBool SBool SBool)
-> Eval (SeqMap SBool SBool SBool))
-> GenValue SBool SBool SBool
forall b w i.
BitWord b w i =>
(Nat'
-> TValue
-> WordValue b w i
-> WordValue b w i
-> Eval (GenValue b w i)
-> Eval (WordValue b w i))
-> (Nat'
-> TValue
-> SeqMap b w i
-> WordValue b w i
-> Eval (GenValue b w i)
-> Eval (SeqMap b w i))
-> GenValue b w i
updatePrim Nat'
-> TValue
-> WordValue SBool SBool SBool
-> WordValue SBool SBool SBool
-> Eval (GenValue SBool SBool SBool)
-> Eval (WordValue SBool SBool SBool)
updateFrontSym_word Nat'
-> TValue
-> SeqMap SBool SBool SBool
-> WordValue SBool SBool SBool
-> Eval (GenValue SBool SBool SBool)
-> Eval (SeqMap SBool SBool SBool)
updateFrontSym)
, ("updateEnd" , (Nat'
-> TValue
-> WordValue SBool SBool SBool
-> WordValue SBool SBool SBool
-> Eval (GenValue SBool SBool SBool)
-> Eval (WordValue SBool SBool SBool))
-> (Nat'
-> TValue
-> SeqMap SBool SBool SBool
-> WordValue SBool SBool SBool
-> Eval (GenValue SBool SBool SBool)
-> Eval (SeqMap SBool SBool SBool))
-> GenValue SBool SBool SBool
forall b w i.
BitWord b w i =>
(Nat'
-> TValue
-> WordValue b w i
-> WordValue b w i
-> Eval (GenValue b w i)
-> Eval (WordValue b w i))
-> (Nat'
-> TValue
-> SeqMap b w i
-> WordValue b w i
-> Eval (GenValue b w i)
-> Eval (SeqMap b w i))
-> GenValue b w i
updatePrim Nat'
-> TValue
-> WordValue SBool SBool SBool
-> WordValue SBool SBool SBool
-> Eval (GenValue SBool SBool SBool)
-> Eval (WordValue SBool SBool SBool)
updateBackSym_word Nat'
-> TValue
-> SeqMap SBool SBool SBool
-> WordValue SBool SBool SBool
-> Eval (GenValue SBool SBool SBool)
-> Eval (SeqMap SBool SBool SBool)
updateBackSym)
, ("error" ,
(TValue -> GenValue SBool SBool SBool)
-> GenValue SBool SBool SBool
forall b w i. (TValue -> GenValue b w i) -> GenValue b w i
tlam ((TValue -> GenValue SBool SBool SBool)
-> GenValue SBool SBool SBool)
-> (TValue -> GenValue SBool SBool SBool)
-> GenValue SBool SBool SBool
forall a b. (a -> b) -> a -> b
$ \at :: TValue
at ->
(Nat' -> GenValue SBool SBool SBool) -> GenValue SBool SBool SBool
forall b w i. (Nat' -> GenValue b w i) -> GenValue b w i
nlam ((Nat' -> GenValue SBool SBool SBool)
-> GenValue SBool SBool SBool)
-> (Nat' -> GenValue SBool SBool SBool)
-> GenValue SBool SBool SBool
forall a b. (a -> b) -> a -> b
$ \(Nat' -> Integer
finNat' -> Integer
_len) ->
(Eval (GenValue SBool SBool SBool)
-> Eval (GenValue SBool SBool SBool))
-> GenValue SBool SBool SBool
forall b w i.
(Eval (GenValue b w i) -> Eval (GenValue b w i)) -> GenValue b w i
VFun ((Eval (GenValue SBool SBool SBool)
-> Eval (GenValue SBool SBool SBool))
-> GenValue SBool SBool SBool)
-> (Eval (GenValue SBool SBool SBool)
-> Eval (GenValue SBool SBool SBool))
-> GenValue SBool SBool SBool
forall a b. (a -> b) -> a -> b
$ \_msg :: Eval (GenValue SBool SBool SBool)
_msg ->
GenValue SBool SBool SBool -> Eval (GenValue SBool SBool SBool)
forall (m :: * -> *) a. Monad m => a -> m a
return (GenValue SBool SBool SBool -> Eval (GenValue SBool SBool SBool))
-> GenValue SBool SBool SBool -> Eval (GenValue SBool SBool SBool)
forall a b. (a -> b) -> a -> b
$ TValue -> GenValue SBool SBool SBool
forall b w i. BitWord b w i => TValue -> GenValue b w i
zeroV TValue
at)
, ("random" ,
(TValue -> GenValue SBool SBool SBool)
-> GenValue SBool SBool SBool
forall b w i. (TValue -> GenValue b w i) -> GenValue b w i
tlam ((TValue -> GenValue SBool SBool SBool)
-> GenValue SBool SBool SBool)
-> (TValue -> GenValue SBool SBool SBool)
-> GenValue SBool SBool SBool
forall a b. (a -> b) -> a -> b
$ \a :: TValue
a ->
(SBool -> Eval (GenValue SBool SBool SBool))
-> GenValue SBool SBool SBool
forall b w i.
BitWord b w i =>
(w -> Eval (GenValue b w i)) -> GenValue b w i
wlam ((SBool -> Eval (GenValue SBool SBool SBool))
-> GenValue SBool SBool SBool)
-> (SBool -> Eval (GenValue SBool SBool SBool))
-> GenValue SBool SBool SBool
forall a b. (a -> b) -> a -> b
$ \x :: SBool
x ->
case SBool -> Maybe Integer
SBV.svAsInteger SBool
x of
Just i :: Integer
i -> GenValue SBool SBool SBool -> Eval (GenValue SBool SBool SBool)
forall (m :: * -> *) a. Monad m => a -> m a
return (GenValue SBool SBool SBool -> Eval (GenValue SBool SBool SBool))
-> GenValue SBool SBool SBool -> Eval (GenValue SBool SBool SBool)
forall a b. (a -> b) -> a -> b
$ TValue -> Integer -> GenValue SBool SBool SBool
forall b w i. BitWord b w i => TValue -> Integer -> GenValue b w i
randomV TValue
a Integer
i
Nothing -> String -> Eval (GenValue SBool SBool SBool)
forall a. String -> Eval a
cryUserError "cannot evaluate 'random' with symbolic inputs")
, ("trace",
(Nat' -> GenValue SBool SBool SBool) -> GenValue SBool SBool SBool
forall b w i. (Nat' -> GenValue b w i) -> GenValue b w i
nlam ((Nat' -> GenValue SBool SBool SBool)
-> GenValue SBool SBool SBool)
-> (Nat' -> GenValue SBool SBool SBool)
-> GenValue SBool SBool SBool
forall a b. (a -> b) -> a -> b
$ \_n :: Nat'
_n ->
(TValue -> GenValue SBool SBool SBool)
-> GenValue SBool SBool SBool
forall b w i. (TValue -> GenValue b w i) -> GenValue b w i
tlam ((TValue -> GenValue SBool SBool SBool)
-> GenValue SBool SBool SBool)
-> (TValue -> GenValue SBool SBool SBool)
-> GenValue SBool SBool SBool
forall a b. (a -> b) -> a -> b
$ \_a :: TValue
_a ->
(TValue -> GenValue SBool SBool SBool)
-> GenValue SBool SBool SBool
forall b w i. (TValue -> GenValue b w i) -> GenValue b w i
tlam ((TValue -> GenValue SBool SBool SBool)
-> GenValue SBool SBool SBool)
-> (TValue -> GenValue SBool SBool SBool)
-> GenValue SBool SBool SBool
forall a b. (a -> b) -> a -> b
$ \_b :: TValue
_b ->
(Eval (GenValue SBool SBool SBool)
-> Eval (GenValue SBool SBool SBool))
-> GenValue SBool SBool SBool
forall b w i.
(Eval (GenValue b w i) -> Eval (GenValue b w i)) -> GenValue b w i
lam ((Eval (GenValue SBool SBool SBool)
-> Eval (GenValue SBool SBool SBool))
-> GenValue SBool SBool SBool)
-> (Eval (GenValue SBool SBool SBool)
-> Eval (GenValue SBool SBool SBool))
-> GenValue SBool SBool SBool
forall a b. (a -> b) -> a -> b
$ \s :: Eval (GenValue SBool SBool SBool)
s -> GenValue SBool SBool SBool -> Eval (GenValue SBool SBool SBool)
forall (m :: * -> *) a. Monad m => a -> m a
return (GenValue SBool SBool SBool -> Eval (GenValue SBool SBool SBool))
-> GenValue SBool SBool SBool -> Eval (GenValue SBool SBool SBool)
forall a b. (a -> b) -> a -> b
$
(Eval (GenValue SBool SBool SBool)
-> Eval (GenValue SBool SBool SBool))
-> GenValue SBool SBool SBool
forall b w i.
(Eval (GenValue b w i) -> Eval (GenValue b w i)) -> GenValue b w i
lam ((Eval (GenValue SBool SBool SBool)
-> Eval (GenValue SBool SBool SBool))
-> GenValue SBool SBool SBool)
-> (Eval (GenValue SBool SBool SBool)
-> Eval (GenValue SBool SBool SBool))
-> GenValue SBool SBool SBool
forall a b. (a -> b) -> a -> b
$ \x :: Eval (GenValue SBool SBool SBool)
x -> GenValue SBool SBool SBool -> Eval (GenValue SBool SBool SBool)
forall (m :: * -> *) a. Monad m => a -> m a
return (GenValue SBool SBool SBool -> Eval (GenValue SBool SBool SBool))
-> GenValue SBool SBool SBool -> Eval (GenValue SBool SBool SBool)
forall a b. (a -> b) -> a -> b
$
(Eval (GenValue SBool SBool SBool)
-> Eval (GenValue SBool SBool SBool))
-> GenValue SBool SBool SBool
forall b w i.
(Eval (GenValue b w i) -> Eval (GenValue b w i)) -> GenValue b w i
lam ((Eval (GenValue SBool SBool SBool)
-> Eval (GenValue SBool SBool SBool))
-> GenValue SBool SBool SBool)
-> (Eval (GenValue SBool SBool SBool)
-> Eval (GenValue SBool SBool SBool))
-> GenValue SBool SBool SBool
forall a b. (a -> b) -> a -> b
$ \y :: Eval (GenValue SBool SBool SBool)
y -> do
GenValue SBool SBool SBool
_ <- Eval (GenValue SBool SBool SBool)
s
GenValue SBool SBool SBool
_ <- Eval (GenValue SBool SBool SBool)
x
Eval (GenValue SBool SBool SBool)
y)
]
shifter :: Monad m => (SBool -> a -> a -> a) -> (a -> Integer -> m a) -> a -> [SBool] -> m a
shifter :: (SBool -> a -> a -> a)
-> (a -> Integer -> m a) -> a -> [SBool] -> m a
shifter mux :: SBool -> a -> a -> a
mux op :: a -> Integer -> m a
op = a -> [SBool] -> m a
go
where
go :: a -> [SBool] -> m a
go x :: a
x [] = a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return a
x
go x :: a
x (b :: SBool
b : bs :: [SBool]
bs) = do
a
x' <- a -> Integer -> m a
op a
x (2 Integer -> Int -> Integer
forall a b. (Num a, Integral b) => a -> b -> a
^ [SBool] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [SBool]
bs)
a -> [SBool] -> m a
go (SBool -> a -> a -> a
mux SBool
b a
x' a
x) [SBool]
bs
logicShift :: String
-> (SWord -> SWord -> SWord)
-> (Nat' -> Integer -> Integer -> Maybe Integer)
-> Value
logicShift :: String
-> (SBool -> SBool -> SBool)
-> (Nat' -> Integer -> Integer -> Maybe Integer)
-> GenValue SBool SBool SBool
logicShift nm :: String
nm wop :: SBool -> SBool -> SBool
wop reindex :: Nat' -> Integer -> Integer -> Maybe Integer
reindex =
(Nat' -> GenValue SBool SBool SBool) -> GenValue SBool SBool SBool
forall b w i. (Nat' -> GenValue b w i) -> GenValue b w i
nlam ((Nat' -> GenValue SBool SBool SBool)
-> GenValue SBool SBool SBool)
-> (Nat' -> GenValue SBool SBool SBool)
-> GenValue SBool SBool SBool
forall a b. (a -> b) -> a -> b
$ \_m :: Nat'
_m ->
(Nat' -> GenValue SBool SBool SBool) -> GenValue SBool SBool SBool
forall b w i. (Nat' -> GenValue b w i) -> GenValue b w i
nlam ((Nat' -> GenValue SBool SBool SBool)
-> GenValue SBool SBool SBool)
-> (Nat' -> GenValue SBool SBool SBool)
-> GenValue SBool SBool SBool
forall a b. (a -> b) -> a -> b
$ \_n :: Nat'
_n ->
(TValue -> GenValue SBool SBool SBool)
-> GenValue SBool SBool SBool
forall b w i. (TValue -> GenValue b w i) -> GenValue b w i
tlam ((TValue -> GenValue SBool SBool SBool)
-> GenValue SBool SBool SBool)
-> (TValue -> GenValue SBool SBool SBool)
-> GenValue SBool SBool SBool
forall a b. (a -> b) -> a -> b
$ \a :: TValue
a ->
(Eval (GenValue SBool SBool SBool)
-> Eval (GenValue SBool SBool SBool))
-> GenValue SBool SBool SBool
forall b w i.
(Eval (GenValue b w i) -> Eval (GenValue b w i)) -> GenValue b w i
VFun ((Eval (GenValue SBool SBool SBool)
-> Eval (GenValue SBool SBool SBool))
-> GenValue SBool SBool SBool)
-> (Eval (GenValue SBool SBool SBool)
-> Eval (GenValue SBool SBool SBool))
-> GenValue SBool SBool SBool
forall a b. (a -> b) -> a -> b
$ \xs :: Eval (GenValue SBool SBool SBool)
xs -> GenValue SBool SBool SBool -> Eval (GenValue SBool SBool SBool)
forall (m :: * -> *) a. Monad m => a -> m a
return (GenValue SBool SBool SBool -> Eval (GenValue SBool SBool SBool))
-> GenValue SBool SBool SBool -> Eval (GenValue SBool SBool SBool)
forall a b. (a -> b) -> a -> b
$
(Eval (GenValue SBool SBool SBool)
-> Eval (GenValue SBool SBool SBool))
-> GenValue SBool SBool SBool
forall b w i.
(Eval (GenValue b w i) -> Eval (GenValue b w i)) -> GenValue b w i
VFun ((Eval (GenValue SBool SBool SBool)
-> Eval (GenValue SBool SBool SBool))
-> GenValue SBool SBool SBool)
-> (Eval (GenValue SBool SBool SBool)
-> Eval (GenValue SBool SBool SBool))
-> GenValue SBool SBool SBool
forall a b. (a -> b) -> a -> b
$ \y :: Eval (GenValue SBool SBool SBool)
y -> do
WordValue SBool SBool SBool
idx <- String
-> GenValue SBool SBool SBool -> Eval (WordValue SBool SBool SBool)
forall b w i. String -> GenValue b w i -> Eval (WordValue b w i)
fromWordVal "logicShift" (GenValue SBool SBool SBool -> Eval (WordValue SBool SBool SBool))
-> Eval (GenValue SBool SBool SBool)
-> Eval (WordValue SBool SBool SBool)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Eval (GenValue SBool SBool SBool)
y
Eval (GenValue SBool SBool SBool)
xs Eval (GenValue SBool SBool SBool)
-> (GenValue SBool SBool SBool
-> Eval (GenValue SBool SBool SBool))
-> Eval (GenValue SBool SBool SBool)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
VWord w :: Integer
w x :: Eval (WordValue SBool SBool SBool)
x ->
GenValue SBool SBool SBool -> Eval (GenValue SBool SBool SBool)
forall (m :: * -> *) a. Monad m => a -> m a
return (GenValue SBool SBool SBool -> Eval (GenValue SBool SBool SBool))
-> GenValue SBool SBool SBool -> Eval (GenValue SBool SBool SBool)
forall a b. (a -> b) -> a -> b
$ Integer
-> Eval (WordValue SBool SBool SBool) -> GenValue SBool SBool SBool
forall b w i. Integer -> Eval (WordValue b w i) -> GenValue b w i
VWord Integer
w (Eval (WordValue SBool SBool SBool) -> GenValue SBool SBool SBool)
-> Eval (WordValue SBool SBool SBool) -> GenValue SBool SBool SBool
forall a b. (a -> b) -> a -> b
$ do
Eval (WordValue SBool SBool SBool)
x Eval (WordValue SBool SBool SBool)
-> (WordValue SBool SBool SBool
-> Eval (WordValue SBool SBool SBool))
-> Eval (WordValue SBool SBool SBool)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
WordVal x' :: SBool
x' -> SBool -> WordValue SBool SBool SBool
forall b w i. w -> WordValue b w i
WordVal (SBool -> WordValue SBool SBool SBool)
-> (SBool -> SBool) -> SBool -> WordValue SBool SBool SBool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SBool -> SBool -> SBool
wop SBool
x' (SBool -> WordValue SBool SBool SBool)
-> Eval SBool -> Eval (WordValue SBool SBool SBool)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> WordValue SBool SBool SBool -> Eval SBool
forall b w i. BitWord b w i => WordValue b w i -> Eval w
asWordVal WordValue SBool SBool SBool
idx
BitsVal bs0 :: Seq (Eval SBool)
bs0 ->
do [SBool]
idx_bits <- WordValue SBool SBool SBool -> Eval [SBool]
forall b w i. BitWord b w i => WordValue b w i -> Eval [b]
enumerateWordValue WordValue SBool SBool SBool
idx
let op :: Seq (m a) -> Integer -> m (Seq (m a))
op bs :: Seq (m a)
bs shft :: Integer
shft = Seq (m a) -> m (Seq (m a))
forall (m :: * -> *) a. Monad m => a -> m a
return (Seq (m a) -> m (Seq (m a))) -> Seq (m a) -> m (Seq (m a))
forall a b. (a -> b) -> a -> b
$ Int -> (Int -> m a) -> Seq (m a)
forall a. Int -> (Int -> a) -> Seq a
Seq.fromFunction (Seq (m a) -> Int
forall a. Seq a -> Int
Seq.length Seq (m a)
bs) ((Int -> m a) -> Seq (m a)) -> (Int -> m a) -> Seq (m a)
forall a b. (a -> b) -> a -> b
$ \i :: Int
i ->
case Nat' -> Integer -> Integer -> Maybe Integer
reindex (Integer -> Nat'
Nat Integer
w) (Int -> Integer
forall a. Integral a => a -> Integer
toInteger Int
i) Integer
shft of
Nothing -> a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (a -> m a) -> a -> m a
forall a b. (a -> b) -> a -> b
$ Bool -> a
forall b w i. BitWord b w i => Bool -> b
bitLit Bool
False
Just i' :: Integer
i' -> Seq (m a) -> Int -> m a
forall a. Seq a -> Int -> a
Seq.index Seq (m a)
bs (Integer -> Int
forall a. Num a => Integer -> a
fromInteger Integer
i')
Seq (Eval SBool) -> WordValue SBool SBool SBool
forall b w i. Seq (Eval b) -> WordValue b w i
BitsVal (Seq (Eval SBool) -> WordValue SBool SBool SBool)
-> Eval (Seq (Eval SBool)) -> Eval (WordValue SBool SBool SBool)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (SBool -> Seq (Eval SBool) -> Seq (Eval SBool) -> Seq (Eval SBool))
-> (Seq (Eval SBool) -> Integer -> Eval (Seq (Eval SBool)))
-> Seq (Eval SBool)
-> [SBool]
-> Eval (Seq (Eval SBool))
forall (m :: * -> *) a.
Monad m =>
(SBool -> a -> a -> a)
-> (a -> Integer -> m a) -> a -> [SBool] -> m a
shifter (Bool
-> SBool
-> Seq (Eval SBool)
-> Seq (Eval SBool)
-> Seq (Eval SBool)
mergeBits Bool
True) Seq (Eval SBool) -> Integer -> Eval (Seq (Eval SBool))
forall (m :: * -> *) (m :: * -> *) a w i.
(Monad m, Monad m, BitWord a w i) =>
Seq (m a) -> Integer -> m (Seq (m a))
op Seq (Eval SBool)
bs0 [SBool]
idx_bits
LargeBitsVal n :: Integer
n bs0 :: SeqMap SBool SBool SBool
bs0 ->
do [SBool]
idx_bits <- WordValue SBool SBool SBool -> Eval [SBool]
forall b w i. BitWord b w i => WordValue b w i -> Eval [b]
enumerateWordValue WordValue SBool SBool SBool
idx
let op :: SeqMap b w i -> Integer -> Eval (SeqMap b w i)
op bs :: SeqMap b w i
bs shft :: Integer
shft = SeqMap b w i -> Eval (SeqMap b w i)
forall b w i. SeqMap b w i -> Eval (SeqMap b w i)
memoMap (SeqMap b w i -> Eval (SeqMap b w i))
-> SeqMap b w i -> Eval (SeqMap b w i)
forall a b. (a -> b) -> a -> b
$ (Integer -> Eval (GenValue b w i)) -> SeqMap b w i
forall b w i. (Integer -> Eval (GenValue b w i)) -> SeqMap b w i
IndexSeqMap ((Integer -> Eval (GenValue b w i)) -> SeqMap b w i)
-> (Integer -> Eval (GenValue b w i)) -> SeqMap b w i
forall a b. (a -> b) -> a -> b
$ \i :: Integer
i ->
case Nat' -> Integer -> Integer -> Maybe Integer
reindex (Integer -> Nat'
Nat Integer
w) Integer
i Integer
shft of
Nothing -> GenValue b w i -> Eval (GenValue b w i)
forall (m :: * -> *) a. Monad m => a -> m a
return (GenValue b w i -> Eval (GenValue b w i))
-> GenValue b w i -> Eval (GenValue b w i)
forall a b. (a -> b) -> a -> b
$ b -> GenValue b w i
forall b w i. b -> GenValue b w i
VBit (b -> GenValue b w i) -> b -> GenValue b w i
forall a b. (a -> b) -> a -> b
$ Bool -> b
forall b w i. BitWord b w i => Bool -> b
bitLit Bool
False
Just i' :: Integer
i' -> SeqMap b w i -> Integer -> Eval (GenValue b w i)
forall b w i. SeqMap b w i -> Integer -> Eval (GenValue b w i)
lookupSeqMap SeqMap b w i
bs Integer
i'
Integer -> SeqMap SBool SBool SBool -> WordValue SBool SBool SBool
forall b w i. Integer -> SeqMap b w i -> WordValue b w i
LargeBitsVal Integer
n (SeqMap SBool SBool SBool -> WordValue SBool SBool SBool)
-> Eval (SeqMap SBool SBool SBool)
-> Eval (WordValue SBool SBool SBool)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (SBool
-> SeqMap SBool SBool SBool
-> SeqMap SBool SBool SBool
-> SeqMap SBool SBool SBool)
-> (SeqMap SBool SBool SBool
-> Integer -> Eval (SeqMap SBool SBool SBool))
-> SeqMap SBool SBool SBool
-> [SBool]
-> Eval (SeqMap SBool SBool SBool)
forall (m :: * -> *) a.
Monad m =>
(SBool -> a -> a -> a)
-> (a -> Integer -> m a) -> a -> [SBool] -> m a
shifter (Bool
-> SBool
-> SeqMap SBool SBool SBool
-> SeqMap SBool SBool SBool
-> SeqMap SBool SBool SBool
mergeSeqMap Bool
True) SeqMap SBool SBool SBool
-> Integer -> Eval (SeqMap SBool SBool SBool)
forall b w i w i.
BitWord b w i =>
SeqMap b w i -> Integer -> Eval (SeqMap b w i)
op SeqMap SBool SBool SBool
bs0 [SBool]
idx_bits
VSeq w :: Integer
w vs0 :: SeqMap SBool SBool SBool
vs0 ->
do [SBool]
idx_bits <- WordValue SBool SBool SBool -> Eval [SBool]
forall b w i. BitWord b w i => WordValue b w i -> Eval [b]
enumerateWordValue WordValue SBool SBool SBool
idx
let op :: SeqMap b w i -> Integer -> Eval (SeqMap b w i)
op vs :: SeqMap b w i
vs shft :: Integer
shft = SeqMap b w i -> Eval (SeqMap b w i)
forall b w i. SeqMap b w i -> Eval (SeqMap b w i)
memoMap (SeqMap b w i -> Eval (SeqMap b w i))
-> SeqMap b w i -> Eval (SeqMap b w i)
forall a b. (a -> b) -> a -> b
$ (Integer -> Eval (GenValue b w i)) -> SeqMap b w i
forall b w i. (Integer -> Eval (GenValue b w i)) -> SeqMap b w i
IndexSeqMap ((Integer -> Eval (GenValue b w i)) -> SeqMap b w i)
-> (Integer -> Eval (GenValue b w i)) -> SeqMap b w i
forall a b. (a -> b) -> a -> b
$ \i :: Integer
i ->
case Nat' -> Integer -> Integer -> Maybe Integer
reindex (Integer -> Nat'
Nat Integer
w) Integer
i Integer
shft of
Nothing -> GenValue b w i -> Eval (GenValue b w i)
forall (m :: * -> *) a. Monad m => a -> m a
return (GenValue b w i -> Eval (GenValue b w i))
-> GenValue b w i -> Eval (GenValue b w i)
forall a b. (a -> b) -> a -> b
$ TValue -> GenValue b w i
forall b w i. BitWord b w i => TValue -> GenValue b w i
zeroV TValue
a
Just i' :: Integer
i' -> SeqMap b w i -> Integer -> Eval (GenValue b w i)
forall b w i. SeqMap b w i -> Integer -> Eval (GenValue b w i)
lookupSeqMap SeqMap b w i
vs Integer
i'
Integer -> SeqMap SBool SBool SBool -> GenValue SBool SBool SBool
forall b w i. Integer -> SeqMap b w i -> GenValue b w i
VSeq Integer
w (SeqMap SBool SBool SBool -> GenValue SBool SBool SBool)
-> Eval (SeqMap SBool SBool SBool)
-> Eval (GenValue SBool SBool SBool)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (SBool
-> SeqMap SBool SBool SBool
-> SeqMap SBool SBool SBool
-> SeqMap SBool SBool SBool)
-> (SeqMap SBool SBool SBool
-> Integer -> Eval (SeqMap SBool SBool SBool))
-> SeqMap SBool SBool SBool
-> [SBool]
-> Eval (SeqMap SBool SBool SBool)
forall (m :: * -> *) a.
Monad m =>
(SBool -> a -> a -> a)
-> (a -> Integer -> m a) -> a -> [SBool] -> m a
shifter (Bool
-> SBool
-> SeqMap SBool SBool SBool
-> SeqMap SBool SBool SBool
-> SeqMap SBool SBool SBool
mergeSeqMap Bool
True) SeqMap SBool SBool SBool
-> Integer -> Eval (SeqMap SBool SBool SBool)
forall b w i.
BitWord b w i =>
SeqMap b w i -> Integer -> Eval (SeqMap b w i)
op SeqMap SBool SBool SBool
vs0 [SBool]
idx_bits
VStream vs0 :: SeqMap SBool SBool SBool
vs0 ->
do [SBool]
idx_bits <- WordValue SBool SBool SBool -> Eval [SBool]
forall b w i. BitWord b w i => WordValue b w i -> Eval [b]
enumerateWordValue WordValue SBool SBool SBool
idx
let op :: SeqMap b w i -> Integer -> Eval (SeqMap b w i)
op vs :: SeqMap b w i
vs shft :: Integer
shft = SeqMap b w i -> Eval (SeqMap b w i)
forall b w i. SeqMap b w i -> Eval (SeqMap b w i)
memoMap (SeqMap b w i -> Eval (SeqMap b w i))
-> SeqMap b w i -> Eval (SeqMap b w i)
forall a b. (a -> b) -> a -> b
$ (Integer -> Eval (GenValue b w i)) -> SeqMap b w i
forall b w i. (Integer -> Eval (GenValue b w i)) -> SeqMap b w i
IndexSeqMap ((Integer -> Eval (GenValue b w i)) -> SeqMap b w i)
-> (Integer -> Eval (GenValue b w i)) -> SeqMap b w i
forall a b. (a -> b) -> a -> b
$ \i :: Integer
i ->
case Nat' -> Integer -> Integer -> Maybe Integer
reindex Nat'
Inf Integer
i Integer
shft of
Nothing -> GenValue b w i -> Eval (GenValue b w i)
forall (m :: * -> *) a. Monad m => a -> m a
return (GenValue b w i -> Eval (GenValue b w i))
-> GenValue b w i -> Eval (GenValue b w i)
forall a b. (a -> b) -> a -> b
$ TValue -> GenValue b w i
forall b w i. BitWord b w i => TValue -> GenValue b w i
zeroV TValue
a
Just i' :: Integer
i' -> SeqMap b w i -> Integer -> Eval (GenValue b w i)
forall b w i. SeqMap b w i -> Integer -> Eval (GenValue b w i)
lookupSeqMap SeqMap b w i
vs Integer
i'
SeqMap SBool SBool SBool -> GenValue SBool SBool SBool
forall b w i. SeqMap b w i -> GenValue b w i
VStream (SeqMap SBool SBool SBool -> GenValue SBool SBool SBool)
-> Eval (SeqMap SBool SBool SBool)
-> Eval (GenValue SBool SBool SBool)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (SBool
-> SeqMap SBool SBool SBool
-> SeqMap SBool SBool SBool
-> SeqMap SBool SBool SBool)
-> (SeqMap SBool SBool SBool
-> Integer -> Eval (SeqMap SBool SBool SBool))
-> SeqMap SBool SBool SBool
-> [SBool]
-> Eval (SeqMap SBool SBool SBool)
forall (m :: * -> *) a.
Monad m =>
(SBool -> a -> a -> a)
-> (a -> Integer -> m a) -> a -> [SBool] -> m a
shifter (Bool
-> SBool
-> SeqMap SBool SBool SBool
-> SeqMap SBool SBool SBool
-> SeqMap SBool SBool SBool
mergeSeqMap Bool
True) SeqMap SBool SBool SBool
-> Integer -> Eval (SeqMap SBool SBool SBool)
forall b w i.
BitWord b w i =>
SeqMap b w i -> Integer -> Eval (SeqMap b w i)
op SeqMap SBool SBool SBool
vs0 [SBool]
idx_bits
_ -> String -> [String] -> Eval (GenValue SBool SBool SBool)
forall a. String -> [String] -> a
evalPanic "expected sequence value in shift operation" [String
nm]
indexFront :: Maybe Integer
-> TValue
-> SeqMap SBool SWord SInteger
-> SWord
-> Eval Value
indexFront :: Maybe Integer
-> TValue
-> SeqMap SBool SBool SBool
-> SBool
-> Eval (GenValue SBool SBool SBool)
indexFront mblen :: Maybe Integer
mblen a :: TValue
a xs :: SeqMap SBool SBool SBool
xs idx :: SBool
idx
| Just i :: Integer
i <- SBool -> Maybe Integer
SBV.svAsInteger SBool
idx
= SeqMap SBool SBool SBool
-> Integer -> Eval (GenValue SBool SBool SBool)
forall b w i. SeqMap b w i -> Integer -> Eval (GenValue b w i)
lookupSeqMap SeqMap SBool SBool SBool
xs Integer
i
| Just n :: Integer
n <- Maybe Integer
mblen
, TVSeq wlen :: Integer
wlen TVBit <- TValue
a
= do [WordValue SBool SBool SBool]
wvs <- (Eval (GenValue SBool SBool SBool)
-> Eval (WordValue SBool SBool SBool))
-> [Eval (GenValue SBool SBool SBool)]
-> Eval [WordValue SBool SBool SBool]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (String
-> GenValue SBool SBool SBool -> Eval (WordValue SBool SBool SBool)
forall b w i. String -> GenValue b w i -> Eval (WordValue b w i)
fromWordVal "indexFront" (GenValue SBool SBool SBool -> Eval (WordValue SBool SBool SBool))
-> Eval (GenValue SBool SBool SBool)
-> Eval (WordValue SBool SBool SBool)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<<) (Integer
-> SeqMap SBool SBool SBool -> [Eval (GenValue SBool SBool SBool)]
forall n b w i.
Integral n =>
n -> SeqMap b w i -> [Eval (GenValue b w i)]
enumerateSeqMap Integer
n SeqMap SBool SBool SBool
xs)
case [WordValue SBool SBool SBool] -> Maybe [SBool]
asWordList [WordValue SBool SBool SBool]
wvs of
Just ws :: [SBool]
ws ->
GenValue SBool SBool SBool -> Eval (GenValue SBool SBool SBool)
forall (m :: * -> *) a. Monad m => a -> m a
return (GenValue SBool SBool SBool -> Eval (GenValue SBool SBool SBool))
-> GenValue SBool SBool SBool -> Eval (GenValue SBool SBool SBool)
forall a b. (a -> b) -> a -> b
$ Integer
-> Eval (WordValue SBool SBool SBool) -> GenValue SBool SBool SBool
forall b w i. Integer -> Eval (WordValue b w i) -> GenValue b w i
VWord Integer
wlen (Eval (WordValue SBool SBool SBool) -> GenValue SBool SBool SBool)
-> Eval (WordValue SBool SBool SBool) -> GenValue SBool SBool SBool
forall a b. (a -> b) -> a -> b
$ WordValue SBool SBool SBool -> Eval (WordValue SBool SBool SBool)
forall a. a -> Eval a
ready (WordValue SBool SBool SBool -> Eval (WordValue SBool SBool SBool))
-> WordValue SBool SBool SBool
-> Eval (WordValue SBool SBool SBool)
forall a b. (a -> b) -> a -> b
$ SBool -> WordValue SBool SBool SBool
forall b w i. w -> WordValue b w i
WordVal (SBool -> WordValue SBool SBool SBool)
-> SBool -> WordValue SBool SBool SBool
forall a b. (a -> b) -> a -> b
$ [SBool] -> SBool -> SBool -> SBool
SBV.svSelect [SBool]
ws (Integer -> Integer -> SBool
forall b w i. BitWord b w i => Integer -> Integer -> w
wordLit Integer
wlen 0) SBool
idx
Nothing -> (Integer
-> Eval (GenValue SBool SBool SBool)
-> Eval (GenValue SBool SBool SBool))
-> Eval (GenValue SBool SBool SBool)
-> [Integer]
-> Eval (GenValue SBool SBool SBool)
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Integer
-> Eval (GenValue SBool SBool SBool)
-> Eval (GenValue SBool SBool SBool)
f Eval (GenValue SBool SBool SBool)
def [Integer]
idxs
| Bool
otherwise
= (Integer
-> Eval (GenValue SBool SBool SBool)
-> Eval (GenValue SBool SBool SBool))
-> Eval (GenValue SBool SBool SBool)
-> [Integer]
-> Eval (GenValue SBool SBool SBool)
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Integer
-> Eval (GenValue SBool SBool SBool)
-> Eval (GenValue SBool SBool SBool)
f Eval (GenValue SBool SBool SBool)
def [Integer]
idxs
where
k :: Kind
k = SBool -> Kind
forall a. HasKind a => a -> Kind
SBV.kindOf SBool
idx
w :: Int
w = SBool -> Int
forall a. HasKind a => a -> Int
SBV.intSizeOf SBool
idx
def :: Eval (GenValue SBool SBool SBool)
def = GenValue SBool SBool SBool -> Eval (GenValue SBool SBool SBool)
forall a. a -> Eval a
ready (GenValue SBool SBool SBool -> Eval (GenValue SBool SBool SBool))
-> GenValue SBool SBool SBool -> Eval (GenValue SBool SBool SBool)
forall a b. (a -> b) -> a -> b
$ TValue -> GenValue SBool SBool SBool
forall b w i. BitWord b w i => TValue -> GenValue b w i
zeroV TValue
a
f :: Integer
-> Eval (GenValue SBool SBool SBool)
-> Eval (GenValue SBool SBool SBool)
f n :: Integer
n y :: Eval (GenValue SBool SBool SBool)
y = SBool
-> Eval (GenValue SBool SBool SBool)
-> Eval (GenValue SBool SBool SBool)
-> Eval (GenValue SBool SBool SBool)
forall b w i.
EvalPrims b w i =>
b
-> Eval (GenValue b w i)
-> Eval (GenValue b w i)
-> Eval (GenValue b w i)
iteValue (SBool -> SBool -> SBool
SBV.svEqual SBool
idx (Kind -> Integer -> SBool
SBV.svInteger Kind
k Integer
n)) (SeqMap SBool SBool SBool
-> Integer -> Eval (GenValue SBool SBool SBool)
forall b w i. SeqMap b w i -> Integer -> Eval (GenValue b w i)
lookupSeqMap SeqMap SBool SBool SBool
xs Integer
n) Eval (GenValue SBool SBool SBool)
y
idxs :: [Integer]
idxs = case Maybe Integer
mblen of
Just n :: Integer
n | Integer
n Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< 2Integer -> Int -> Integer
forall a b. (Num a, Integral b) => a -> b -> a
^Int
w -> [0 .. Integer
nInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
-1]
_ -> [0 .. 2Integer -> Int -> Integer
forall a b. (Num a, Integral b) => a -> b -> a
^Int
w Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- 1]
indexBack :: Maybe Integer
-> TValue
-> SeqMap SBool SWord SInteger
-> SWord
-> Eval Value
indexBack :: Maybe Integer
-> TValue
-> SeqMap SBool SBool SBool
-> SBool
-> Eval (GenValue SBool SBool SBool)
indexBack (Just n :: Integer
n) a :: TValue
a xs :: SeqMap SBool SBool SBool
xs idx :: SBool
idx = Maybe Integer
-> TValue
-> SeqMap SBool SBool SBool
-> SBool
-> Eval (GenValue SBool SBool SBool)
indexFront (Integer -> Maybe Integer
forall a. a -> Maybe a
Just Integer
n) TValue
a (Integer -> SeqMap SBool SBool SBool -> SeqMap SBool SBool SBool
forall b w i. Integer -> SeqMap b w i -> SeqMap b w i
reverseSeqMap Integer
n SeqMap SBool SBool SBool
xs) SBool
idx
indexBack Nothing _ _ _ = String -> [String] -> Eval (GenValue SBool SBool SBool)
forall a. String -> [String] -> a
evalPanic "Expected finite sequence" ["indexBack"]
indexFront_bits :: Maybe Integer
-> TValue
-> SeqMap SBool SWord SInteger
-> Seq.Seq SBool
-> Eval Value
indexFront_bits :: Maybe Integer
-> TValue
-> SeqMap SBool SBool SBool
-> Seq SBool
-> Eval (GenValue SBool SBool SBool)
indexFront_bits mblen :: Maybe Integer
mblen a :: TValue
a xs :: SeqMap SBool SBool SBool
xs bits0 :: Seq SBool
bits0 = Integer -> Int -> [SBool] -> Eval (GenValue SBool SBool SBool)
go 0 (Seq SBool -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length Seq SBool
bits0) (Seq SBool -> [SBool]
forall (t :: * -> *) a. Foldable t => t a -> [a]
Fold.toList Seq SBool
bits0)
where
go :: Integer -> Int -> [SBool] -> Eval Value
go :: Integer -> Int -> [SBool] -> Eval (GenValue SBool SBool SBool)
go i :: Integer
i _k :: Int
_k []
| Just n :: Integer
n <- Maybe Integer
mblen
, Integer
i Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= Integer
n
= GenValue SBool SBool SBool -> Eval (GenValue SBool SBool SBool)
forall (m :: * -> *) a. Monad m => a -> m a
return (GenValue SBool SBool SBool -> Eval (GenValue SBool SBool SBool))
-> GenValue SBool SBool SBool -> Eval (GenValue SBool SBool SBool)
forall a b. (a -> b) -> a -> b
$ TValue -> GenValue SBool SBool SBool
forall b w i. BitWord b w i => TValue -> GenValue b w i
zeroV TValue
a
| Bool
otherwise
= SeqMap SBool SBool SBool
-> Integer -> Eval (GenValue SBool SBool SBool)
forall b w i. SeqMap b w i -> Integer -> Eval (GenValue b w i)
lookupSeqMap SeqMap SBool SBool SBool
xs Integer
i
go i :: Integer
i k :: Int
k (b :: SBool
b:bs :: [SBool]
bs)
| Just n :: Integer
n <- Maybe Integer
mblen
, (Integer
i Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
`shiftL` Int
k) Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= Integer
n
= GenValue SBool SBool SBool -> Eval (GenValue SBool SBool SBool)
forall (m :: * -> *) a. Monad m => a -> m a
return (GenValue SBool SBool SBool -> Eval (GenValue SBool SBool SBool))
-> GenValue SBool SBool SBool -> Eval (GenValue SBool SBool SBool)
forall a b. (a -> b) -> a -> b
$ TValue -> GenValue SBool SBool SBool
forall b w i. BitWord b w i => TValue -> GenValue b w i
zeroV TValue
a
| Bool
otherwise
= SBool
-> Eval (GenValue SBool SBool SBool)
-> Eval (GenValue SBool SBool SBool)
-> Eval (GenValue SBool SBool SBool)
forall b w i.
EvalPrims b w i =>
b
-> Eval (GenValue b w i)
-> Eval (GenValue b w i)
-> Eval (GenValue b w i)
iteValue SBool
b (Integer -> Int -> [SBool] -> Eval (GenValue SBool SBool SBool)
go ((Integer
i Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
`shiftL` 1) Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ 1) (Int
kInt -> Int -> Int
forall a. Num a => a -> a -> a
-1) [SBool]
bs)
(Integer -> Int -> [SBool] -> Eval (GenValue SBool SBool SBool)
go (Integer
i Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
`shiftL` 1) (Int
kInt -> Int -> Int
forall a. Num a => a -> a -> a
-1) [SBool]
bs)
indexBack_bits :: Maybe Integer
-> TValue
-> SeqMap SBool SWord SInteger
-> Seq.Seq SBool
-> Eval Value
indexBack_bits :: Maybe Integer
-> TValue
-> SeqMap SBool SBool SBool
-> Seq SBool
-> Eval (GenValue SBool SBool SBool)
indexBack_bits (Just n :: Integer
n) a :: TValue
a xs :: SeqMap SBool SBool SBool
xs idx :: Seq SBool
idx = Maybe Integer
-> TValue
-> SeqMap SBool SBool SBool
-> Seq SBool
-> Eval (GenValue SBool SBool SBool)
indexFront_bits (Integer -> Maybe Integer
forall a. a -> Maybe a
Just Integer
n) TValue
a (Integer -> SeqMap SBool SBool SBool -> SeqMap SBool SBool SBool
forall b w i. Integer -> SeqMap b w i -> SeqMap b w i
reverseSeqMap Integer
n SeqMap SBool SBool SBool
xs) Seq SBool
idx
indexBack_bits Nothing _ _ _ = String -> [String] -> Eval (GenValue SBool SBool SBool)
forall a. String -> [String] -> a
evalPanic "Expected finite sequence" ["indexBack_bits"]
wordValueEqualsInteger :: WordValue SBool SWord SInteger -> Integer -> Eval SBool
wordValueEqualsInteger :: WordValue SBool SBool SBool -> Integer -> Eval SBool
wordValueEqualsInteger wv :: WordValue SBool SBool SBool
wv i :: Integer
i
| WordValue SBool SBool SBool -> Integer
forall b w i. BitWord b w i => WordValue b w i -> Integer
wordValueSize WordValue SBool SBool SBool
wv Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer -> Integer
widthInteger Integer
i = SBool -> Eval SBool
forall (m :: * -> *) a. Monad m => a -> m a
return SBool
SBV.svFalse
| Bool
otherwise =
case WordValue SBool SBool SBool
wv of
WordVal w :: SBool
w -> SBool -> Eval SBool
forall (m :: * -> *) a. Monad m => a -> m a
return (SBool -> Eval SBool) -> SBool -> Eval SBool
forall a b. (a -> b) -> a -> b
$ SBool -> SBool -> SBool
SBV.svEqual SBool
w (Int -> Integer -> SBool
literalSWord (SBool -> Int
forall a. HasKind a => a -> Int
SBV.intSizeOf SBool
w) Integer
i)
_ -> Integer -> [SBool] -> SBool
bitsAre Integer
i ([SBool] -> SBool) -> Eval [SBool] -> Eval SBool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> WordValue SBool SBool SBool -> Eval [SBool]
forall b w i. BitWord b w i => WordValue b w i -> Eval [b]
enumerateWordValueRev WordValue SBool SBool SBool
wv
where
bitsAre :: Integer -> [SBool] -> SBool
bitsAre :: Integer -> [SBool] -> SBool
bitsAre n :: Integer
n [] = Bool -> SBool
SBV.svBool (Integer
n Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== 0)
bitsAre n :: Integer
n (b :: SBool
b : bs :: [SBool]
bs) = SBool -> SBool -> SBool
SBV.svAnd (Bool -> SBool -> SBool
bitIs (Integer -> Bool
forall a. Integral a => a -> Bool
odd Integer
n) SBool
b) (Integer -> [SBool] -> SBool
bitsAre (Integer
n Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`div` 2) [SBool]
bs)
bitIs :: Bool -> SBool -> SBool
bitIs :: Bool -> SBool -> SBool
bitIs b :: Bool
b x :: SBool
x = if Bool
b then SBool
x else SBool -> SBool
SBV.svNot SBool
x
lazyMergeBit :: SBool -> Eval SBool -> Eval SBool -> Eval SBool
lazyMergeBit :: SBool -> Eval SBool -> Eval SBool -> Eval SBool
lazyMergeBit c :: SBool
c x :: Eval SBool
x y :: Eval SBool
y =
case SBool -> Maybe Bool
SBV.svAsBool SBool
c of
Just True -> Eval SBool
x
Just False -> Eval SBool
y
Nothing -> Bool -> SBool -> SBool -> SBool -> SBool
mergeBit Bool
False SBool
c (SBool -> SBool -> SBool) -> Eval SBool -> Eval (SBool -> SBool)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Eval SBool
x Eval (SBool -> SBool) -> Eval SBool -> Eval SBool
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Eval SBool
y
updateFrontSym
:: Nat'
-> TValue
-> SeqMap SBool SWord SInteger
-> WordValue SBool SWord SInteger
-> Eval (GenValue SBool SWord SInteger)
-> Eval (SeqMap SBool SWord SInteger)
updateFrontSym :: Nat'
-> TValue
-> SeqMap SBool SBool SBool
-> WordValue SBool SBool SBool
-> Eval (GenValue SBool SBool SBool)
-> Eval (SeqMap SBool SBool SBool)
updateFrontSym len :: Nat'
len _eltTy :: TValue
_eltTy vs :: SeqMap SBool SBool SBool
vs wv :: WordValue SBool SBool SBool
wv val :: Eval (GenValue SBool SBool SBool)
val =
case WordValue SBool SBool SBool
wv of
WordVal w :: SBool
w | Just j :: Integer
j <- SBool -> Maybe Integer
SBV.svAsInteger SBool
w ->
do case Nat'
len of
Inf -> () -> Eval ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
Nat n :: Integer
n -> Bool -> Eval () -> Eval ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Integer
j Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
n) (Integer -> Eval ()
forall a. Integer -> Eval a
invalidIndex Integer
j)
SeqMap SBool SBool SBool -> Eval (SeqMap SBool SBool SBool)
forall (m :: * -> *) a. Monad m => a -> m a
return (SeqMap SBool SBool SBool -> Eval (SeqMap SBool SBool SBool))
-> SeqMap SBool SBool SBool -> Eval (SeqMap SBool SBool SBool)
forall a b. (a -> b) -> a -> b
$ SeqMap SBool SBool SBool
-> Integer
-> Eval (GenValue SBool SBool SBool)
-> SeqMap SBool SBool SBool
forall b w i.
SeqMap b w i -> Integer -> Eval (GenValue b w i) -> SeqMap b w i
updateSeqMap SeqMap SBool SBool SBool
vs Integer
j Eval (GenValue SBool SBool SBool)
val
_ ->
SeqMap SBool SBool SBool -> Eval (SeqMap SBool SBool SBool)
forall (m :: * -> *) a. Monad m => a -> m a
return (SeqMap SBool SBool SBool -> Eval (SeqMap SBool SBool SBool))
-> SeqMap SBool SBool SBool -> Eval (SeqMap SBool SBool SBool)
forall a b. (a -> b) -> a -> b
$ (Integer -> Eval (GenValue SBool SBool SBool))
-> SeqMap SBool SBool SBool
forall b w i. (Integer -> Eval (GenValue b w i)) -> SeqMap b w i
IndexSeqMap ((Integer -> Eval (GenValue SBool SBool SBool))
-> SeqMap SBool SBool SBool)
-> (Integer -> Eval (GenValue SBool SBool SBool))
-> SeqMap SBool SBool SBool
forall a b. (a -> b) -> a -> b
$ \i :: Integer
i ->
do SBool
b <- WordValue SBool SBool SBool -> Integer -> Eval SBool
wordValueEqualsInteger WordValue SBool SBool SBool
wv Integer
i
SBool
-> Eval (GenValue SBool SBool SBool)
-> Eval (GenValue SBool SBool SBool)
-> Eval (GenValue SBool SBool SBool)
forall b w i.
EvalPrims b w i =>
b
-> Eval (GenValue b w i)
-> Eval (GenValue b w i)
-> Eval (GenValue b w i)
iteValue SBool
b Eval (GenValue SBool SBool SBool)
val (SeqMap SBool SBool SBool
-> Integer -> Eval (GenValue SBool SBool SBool)
forall b w i. SeqMap b w i -> Integer -> Eval (GenValue b w i)
lookupSeqMap SeqMap SBool SBool SBool
vs Integer
i)
updateFrontSym_word
:: Nat'
-> TValue
-> WordValue SBool SWord SInteger
-> WordValue SBool SWord SInteger
-> Eval (GenValue SBool SWord SInteger)
-> Eval (WordValue SBool SWord SInteger)
updateFrontSym_word :: Nat'
-> TValue
-> WordValue SBool SBool SBool
-> WordValue SBool SBool SBool
-> Eval (GenValue SBool SBool SBool)
-> Eval (WordValue SBool SBool SBool)
updateFrontSym_word Inf _ _ _ _ = String -> [String] -> Eval (WordValue SBool SBool SBool)
forall a. String -> [String] -> a
evalPanic "Expected finite sequence" ["updateFrontSym_bits"]
updateFrontSym_word (Nat n :: Integer
n) eltTy :: TValue
eltTy bv :: WordValue SBool SBool SBool
bv wv :: WordValue SBool SBool SBool
wv val :: Eval (GenValue SBool SBool SBool)
val =
case WordValue SBool SBool SBool
wv of
WordVal w :: SBool
w | Just j :: Integer
j <- SBool -> Maybe Integer
SBV.svAsInteger SBool
w ->
do Bool -> Eval () -> Eval ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Integer
j Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
n) (Integer -> Eval ()
forall a. Integer -> Eval a
invalidIndex Integer
j)
WordValue SBool SBool SBool
-> Integer -> Eval SBool -> Eval (WordValue SBool SBool SBool)
forall b w i.
BitWord b w i =>
WordValue b w i -> Integer -> Eval b -> Eval (WordValue b w i)
updateWordValue WordValue SBool SBool SBool
bv Integer
j (GenValue SBool SBool SBool -> SBool
forall b w i. GenValue b w i -> b
fromVBit (GenValue SBool SBool SBool -> SBool)
-> Eval (GenValue SBool SBool SBool) -> Eval SBool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Eval (GenValue SBool SBool SBool)
val)
_ ->
case WordValue SBool SBool SBool
bv of
WordVal bw :: SBool
bw -> WordValue SBool SBool SBool -> Eval (WordValue SBool SBool SBool)
forall (m :: * -> *) a. Monad m => a -> m a
return (WordValue SBool SBool SBool -> Eval (WordValue SBool SBool SBool))
-> WordValue SBool SBool SBool
-> Eval (WordValue SBool SBool SBool)
forall a b. (a -> b) -> a -> b
$ Seq (Eval SBool) -> WordValue SBool SBool SBool
forall b w i. Seq (Eval b) -> WordValue b w i
BitsVal (Seq (Eval SBool) -> WordValue SBool SBool SBool)
-> Seq (Eval SBool) -> WordValue SBool SBool SBool
forall a b. (a -> b) -> a -> b
$ (Int -> Eval SBool -> Eval SBool)
-> Seq (Eval SBool) -> Seq (Eval SBool)
forall a b. (Int -> a -> b) -> Seq a -> Seq b
Seq.mapWithIndex Int -> Eval SBool -> Eval SBool
f Seq (Eval SBool)
bs
where bs :: Seq (Eval SBool)
bs = (SBool -> Eval SBool) -> Seq SBool -> Seq (Eval SBool)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap SBool -> Eval SBool
forall (m :: * -> *) a. Monad m => a -> m a
return (Seq SBool -> Seq (Eval SBool)) -> Seq SBool -> Seq (Eval SBool)
forall a b. (a -> b) -> a -> b
$ [SBool] -> Seq SBool
forall a. [a] -> Seq a
Seq.fromList ([SBool] -> Seq SBool) -> [SBool] -> Seq SBool
forall a b. (a -> b) -> a -> b
$ SBool -> [SBool]
forall b w i. BitWord b w i => w -> [b]
unpackWord SBool
bw
BitsVal bs :: Seq (Eval SBool)
bs -> WordValue SBool SBool SBool -> Eval (WordValue SBool SBool SBool)
forall (m :: * -> *) a. Monad m => a -> m a
return (WordValue SBool SBool SBool -> Eval (WordValue SBool SBool SBool))
-> WordValue SBool SBool SBool
-> Eval (WordValue SBool SBool SBool)
forall a b. (a -> b) -> a -> b
$ Seq (Eval SBool) -> WordValue SBool SBool SBool
forall b w i. Seq (Eval b) -> WordValue b w i
BitsVal (Seq (Eval SBool) -> WordValue SBool SBool SBool)
-> Seq (Eval SBool) -> WordValue SBool SBool SBool
forall a b. (a -> b) -> a -> b
$ (Int -> Eval SBool -> Eval SBool)
-> Seq (Eval SBool) -> Seq (Eval SBool)
forall a b. (Int -> a -> b) -> Seq a -> Seq b
Seq.mapWithIndex Int -> Eval SBool -> Eval SBool
f Seq (Eval SBool)
bs
LargeBitsVal l :: Integer
l vs :: SeqMap SBool SBool SBool
vs -> Integer -> SeqMap SBool SBool SBool -> WordValue SBool SBool SBool
forall b w i. Integer -> SeqMap b w i -> WordValue b w i
LargeBitsVal Integer
l (SeqMap SBool SBool SBool -> WordValue SBool SBool SBool)
-> Eval (SeqMap SBool SBool SBool)
-> Eval (WordValue SBool SBool SBool)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Nat'
-> TValue
-> SeqMap SBool SBool SBool
-> WordValue SBool SBool SBool
-> Eval (GenValue SBool SBool SBool)
-> Eval (SeqMap SBool SBool SBool)
updateFrontSym (Integer -> Nat'
Nat Integer
n) TValue
eltTy SeqMap SBool SBool SBool
vs WordValue SBool SBool SBool
wv Eval (GenValue SBool SBool SBool)
val
where
f :: Int -> Eval SBool -> Eval SBool
f :: Int -> Eval SBool -> Eval SBool
f i :: Int
i x :: Eval SBool
x = do SBool
c <- WordValue SBool SBool SBool -> Integer -> Eval SBool
wordValueEqualsInteger WordValue SBool SBool SBool
wv (Int -> Integer
forall a. Integral a => a -> Integer
toInteger Int
i)
SBool -> Eval SBool -> Eval SBool -> Eval SBool
lazyMergeBit SBool
c (GenValue SBool SBool SBool -> Eval SBool
forall b w i. GenValue b w i -> Eval b
fromBit (GenValue SBool SBool SBool -> Eval SBool)
-> Eval (GenValue SBool SBool SBool) -> Eval SBool
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Eval (GenValue SBool SBool SBool)
val) Eval SBool
x
updateBackSym
:: Nat'
-> TValue
-> SeqMap SBool SWord SInteger
-> WordValue SBool SWord SInteger
-> Eval (GenValue SBool SWord SInteger)
-> Eval (SeqMap SBool SWord SInteger)
updateBackSym :: Nat'
-> TValue
-> SeqMap SBool SBool SBool
-> WordValue SBool SBool SBool
-> Eval (GenValue SBool SBool SBool)
-> Eval (SeqMap SBool SBool SBool)
updateBackSym Inf _ _ _ _ = String -> [String] -> Eval (SeqMap SBool SBool SBool)
forall a. String -> [String] -> a
evalPanic "Expected finite sequence" ["updateBackSym"]
updateBackSym (Nat n :: Integer
n) _eltTy :: TValue
_eltTy vs :: SeqMap SBool SBool SBool
vs wv :: WordValue SBool SBool SBool
wv val :: Eval (GenValue SBool SBool SBool)
val =
case WordValue SBool SBool SBool
wv of
WordVal w :: SBool
w | Just j :: Integer
j <- SBool -> Maybe Integer
SBV.svAsInteger SBool
w ->
do Bool -> Eval () -> Eval ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Integer
j Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
n) (Integer -> Eval ()
forall a. Integer -> Eval a
invalidIndex Integer
j)
SeqMap SBool SBool SBool -> Eval (SeqMap SBool SBool SBool)
forall (m :: * -> *) a. Monad m => a -> m a
return (SeqMap SBool SBool SBool -> Eval (SeqMap SBool SBool SBool))
-> SeqMap SBool SBool SBool -> Eval (SeqMap SBool SBool SBool)
forall a b. (a -> b) -> a -> b
$ SeqMap SBool SBool SBool
-> Integer
-> Eval (GenValue SBool SBool SBool)
-> SeqMap SBool SBool SBool
forall b w i.
SeqMap b w i -> Integer -> Eval (GenValue b w i) -> SeqMap b w i
updateSeqMap SeqMap SBool SBool SBool
vs (Integer
n Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- 1 Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
j) Eval (GenValue SBool SBool SBool)
val
_ ->
SeqMap SBool SBool SBool -> Eval (SeqMap SBool SBool SBool)
forall (m :: * -> *) a. Monad m => a -> m a
return (SeqMap SBool SBool SBool -> Eval (SeqMap SBool SBool SBool))
-> SeqMap SBool SBool SBool -> Eval (SeqMap SBool SBool SBool)
forall a b. (a -> b) -> a -> b
$ (Integer -> Eval (GenValue SBool SBool SBool))
-> SeqMap SBool SBool SBool
forall b w i. (Integer -> Eval (GenValue b w i)) -> SeqMap b w i
IndexSeqMap ((Integer -> Eval (GenValue SBool SBool SBool))
-> SeqMap SBool SBool SBool)
-> (Integer -> Eval (GenValue SBool SBool SBool))
-> SeqMap SBool SBool SBool
forall a b. (a -> b) -> a -> b
$ \i :: Integer
i ->
do SBool
b <- WordValue SBool SBool SBool -> Integer -> Eval SBool
wordValueEqualsInteger WordValue SBool SBool SBool
wv (Integer
n Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- 1 Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
i)
SBool
-> Eval (GenValue SBool SBool SBool)
-> Eval (GenValue SBool SBool SBool)
-> Eval (GenValue SBool SBool SBool)
forall b w i.
EvalPrims b w i =>
b
-> Eval (GenValue b w i)
-> Eval (GenValue b w i)
-> Eval (GenValue b w i)
iteValue SBool
b Eval (GenValue SBool SBool SBool)
val (SeqMap SBool SBool SBool
-> Integer -> Eval (GenValue SBool SBool SBool)
forall b w i. SeqMap b w i -> Integer -> Eval (GenValue b w i)
lookupSeqMap SeqMap SBool SBool SBool
vs Integer
i)
updateBackSym_word
:: Nat'
-> TValue
-> WordValue SBool SWord SInteger
-> WordValue SBool SWord SInteger
-> Eval (GenValue SBool SWord SInteger)
-> Eval (WordValue SBool SWord SInteger)
updateBackSym_word :: Nat'
-> TValue
-> WordValue SBool SBool SBool
-> WordValue SBool SBool SBool
-> Eval (GenValue SBool SBool SBool)
-> Eval (WordValue SBool SBool SBool)
updateBackSym_word Inf _ _ _ _ = String -> [String] -> Eval (WordValue SBool SBool SBool)
forall a. String -> [String] -> a
evalPanic "Expected finite sequence" ["updateBackSym_bits"]
updateBackSym_word (Nat n :: Integer
n) eltTy :: TValue
eltTy bv :: WordValue SBool SBool SBool
bv wv :: WordValue SBool SBool SBool
wv val :: Eval (GenValue SBool SBool SBool)
val = do
case WordValue SBool SBool SBool
wv of
WordVal w :: SBool
w | Just j :: Integer
j <- SBool -> Maybe Integer
SBV.svAsInteger SBool
w ->
do Bool -> Eval () -> Eval ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Integer
j Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
n) (Integer -> Eval ()
forall a. Integer -> Eval a
invalidIndex Integer
j)
WordValue SBool SBool SBool
-> Integer -> Eval SBool -> Eval (WordValue SBool SBool SBool)
forall b w i.
BitWord b w i =>
WordValue b w i -> Integer -> Eval b -> Eval (WordValue b w i)
updateWordValue WordValue SBool SBool SBool
bv (Integer
n Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- 1 Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
j) (GenValue SBool SBool SBool -> SBool
forall b w i. GenValue b w i -> b
fromVBit (GenValue SBool SBool SBool -> SBool)
-> Eval (GenValue SBool SBool SBool) -> Eval SBool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Eval (GenValue SBool SBool SBool)
val)
_ ->
case WordValue SBool SBool SBool
bv of
WordVal bw :: SBool
bw -> WordValue SBool SBool SBool -> Eval (WordValue SBool SBool SBool)
forall (m :: * -> *) a. Monad m => a -> m a
return (WordValue SBool SBool SBool -> Eval (WordValue SBool SBool SBool))
-> WordValue SBool SBool SBool
-> Eval (WordValue SBool SBool SBool)
forall a b. (a -> b) -> a -> b
$ Seq (Eval SBool) -> WordValue SBool SBool SBool
forall b w i. Seq (Eval b) -> WordValue b w i
BitsVal (Seq (Eval SBool) -> WordValue SBool SBool SBool)
-> Seq (Eval SBool) -> WordValue SBool SBool SBool
forall a b. (a -> b) -> a -> b
$ (Int -> Eval SBool -> Eval SBool)
-> Seq (Eval SBool) -> Seq (Eval SBool)
forall a b. (Int -> a -> b) -> Seq a -> Seq b
Seq.mapWithIndex Int -> Eval SBool -> Eval SBool
f Seq (Eval SBool)
bs
where bs :: Seq (Eval SBool)
bs = (SBool -> Eval SBool) -> Seq SBool -> Seq (Eval SBool)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap SBool -> Eval SBool
forall (m :: * -> *) a. Monad m => a -> m a
return (Seq SBool -> Seq (Eval SBool)) -> Seq SBool -> Seq (Eval SBool)
forall a b. (a -> b) -> a -> b
$ [SBool] -> Seq SBool
forall a. [a] -> Seq a
Seq.fromList ([SBool] -> Seq SBool) -> [SBool] -> Seq SBool
forall a b. (a -> b) -> a -> b
$ SBool -> [SBool]
forall b w i. BitWord b w i => w -> [b]
unpackWord SBool
bw
BitsVal bs :: Seq (Eval SBool)
bs -> WordValue SBool SBool SBool -> Eval (WordValue SBool SBool SBool)
forall (m :: * -> *) a. Monad m => a -> m a
return (WordValue SBool SBool SBool -> Eval (WordValue SBool SBool SBool))
-> WordValue SBool SBool SBool
-> Eval (WordValue SBool SBool SBool)
forall a b. (a -> b) -> a -> b
$ Seq (Eval SBool) -> WordValue SBool SBool SBool
forall b w i. Seq (Eval b) -> WordValue b w i
BitsVal (Seq (Eval SBool) -> WordValue SBool SBool SBool)
-> Seq (Eval SBool) -> WordValue SBool SBool SBool
forall a b. (a -> b) -> a -> b
$ (Int -> Eval SBool -> Eval SBool)
-> Seq (Eval SBool) -> Seq (Eval SBool)
forall a b. (Int -> a -> b) -> Seq a -> Seq b
Seq.mapWithIndex Int -> Eval SBool -> Eval SBool
f Seq (Eval SBool)
bs
LargeBitsVal l :: Integer
l vs :: SeqMap SBool SBool SBool
vs -> Integer -> SeqMap SBool SBool SBool -> WordValue SBool SBool SBool
forall b w i. Integer -> SeqMap b w i -> WordValue b w i
LargeBitsVal Integer
l (SeqMap SBool SBool SBool -> WordValue SBool SBool SBool)
-> Eval (SeqMap SBool SBool SBool)
-> Eval (WordValue SBool SBool SBool)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Nat'
-> TValue
-> SeqMap SBool SBool SBool
-> WordValue SBool SBool SBool
-> Eval (GenValue SBool SBool SBool)
-> Eval (SeqMap SBool SBool SBool)
updateBackSym (Integer -> Nat'
Nat Integer
n) TValue
eltTy SeqMap SBool SBool SBool
vs WordValue SBool SBool SBool
wv Eval (GenValue SBool SBool SBool)
val
where
f :: Int -> Eval SBool -> Eval SBool
f :: Int -> Eval SBool -> Eval SBool
f i :: Int
i x :: Eval SBool
x = do SBool
c <- WordValue SBool SBool SBool -> Integer -> Eval SBool
wordValueEqualsInteger WordValue SBool SBool SBool
wv (Integer
n Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- 1 Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Int -> Integer
forall a. Integral a => a -> Integer
toInteger Int
i)
SBool -> Eval SBool -> Eval SBool -> Eval SBool
lazyMergeBit SBool
c (GenValue SBool SBool SBool -> Eval SBool
forall b w i. GenValue b w i -> Eval b
fromBit (GenValue SBool SBool SBool -> Eval SBool)
-> Eval (GenValue SBool SBool SBool) -> Eval SBool
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Eval (GenValue SBool SBool SBool)
val) Eval SBool
x
asBitList :: [Eval SBool] -> Maybe [SBool]
asBitList :: [Eval SBool] -> Maybe [SBool]
asBitList = ([SBool] -> [SBool]) -> [Eval SBool] -> Maybe [SBool]
go [SBool] -> [SBool]
forall a. a -> a
id
where go :: ([SBool] -> [SBool]) -> [Eval SBool] -> Maybe [SBool]
go :: ([SBool] -> [SBool]) -> [Eval SBool] -> Maybe [SBool]
go f :: [SBool] -> [SBool]
f [] = [SBool] -> Maybe [SBool]
forall a. a -> Maybe a
Just ([SBool] -> [SBool]
f [])
go f :: [SBool] -> [SBool]
f (Ready b :: SBool
b:vs :: [Eval SBool]
vs) = ([SBool] -> [SBool]) -> [Eval SBool] -> Maybe [SBool]
go ([SBool] -> [SBool]
f ([SBool] -> [SBool]) -> ([SBool] -> [SBool]) -> [SBool] -> [SBool]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (SBool
bSBool -> [SBool] -> [SBool]
forall a. a -> [a] -> [a]
:)) [Eval SBool]
vs
go _ _ = Maybe [SBool]
forall a. Maybe a
Nothing
asWordList :: [WordValue SBool SWord SInteger] -> Maybe [SWord]
asWordList :: [WordValue SBool SBool SBool] -> Maybe [SBool]
asWordList = ([SBool] -> [SBool])
-> [WordValue SBool SBool SBool] -> Maybe [SBool]
go [SBool] -> [SBool]
forall a. a -> a
id
where go :: ([SWord] -> [SWord]) -> [WordValue SBool SWord SInteger] -> Maybe [SWord]
go :: ([SBool] -> [SBool])
-> [WordValue SBool SBool SBool] -> Maybe [SBool]
go f :: [SBool] -> [SBool]
f [] = [SBool] -> Maybe [SBool]
forall a. a -> Maybe a
Just ([SBool] -> [SBool]
f [])
go f :: [SBool] -> [SBool]
f (WordVal x :: SBool
x :vs :: [WordValue SBool SBool SBool]
vs) = ([SBool] -> [SBool])
-> [WordValue SBool SBool SBool] -> Maybe [SBool]
go ([SBool] -> [SBool]
f ([SBool] -> [SBool]) -> ([SBool] -> [SBool]) -> [SBool] -> [SBool]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (SBool
xSBool -> [SBool] -> [SBool]
forall a. a -> [a] -> [a]
:)) [WordValue SBool SBool SBool]
vs
go f :: [SBool] -> [SBool]
f (BitsVal bs :: Seq (Eval SBool)
bs:vs :: [WordValue SBool SBool SBool]
vs) =
case [Eval SBool] -> Maybe [SBool]
asBitList (Seq (Eval SBool) -> [Eval SBool]
forall (t :: * -> *) a. Foldable t => t a -> [a]
Fold.toList Seq (Eval SBool)
bs) of
Just xs :: [SBool]
xs -> ([SBool] -> [SBool])
-> [WordValue SBool SBool SBool] -> Maybe [SBool]
go ([SBool] -> [SBool]
f ([SBool] -> [SBool]) -> ([SBool] -> [SBool]) -> [SBool] -> [SBool]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([SBool] -> SBool
forall b w i. BitWord b w i => [b] -> w
packWord [SBool]
xsSBool -> [SBool] -> [SBool]
forall a. a -> [a] -> [a]
:)) [WordValue SBool SBool SBool]
vs
Nothing -> Maybe [SBool]
forall a. Maybe a
Nothing
go _f :: [SBool] -> [SBool]
_f (LargeBitsVal _ _ : _) = Maybe [SBool]
forall a. Maybe a
Nothing
liftBinArith :: (SWord -> SWord -> SWord) -> BinArith SWord
liftBinArith :: (SBool -> SBool -> SBool) -> BinArith SBool
liftBinArith op :: SBool -> SBool -> SBool
op _ x :: SBool
x y :: SBool
y = SBool -> Eval SBool
forall a. a -> Eval a
ready (SBool -> Eval SBool) -> SBool -> Eval SBool
forall a b. (a -> b) -> a -> b
$ SBool -> SBool -> SBool
op SBool
x SBool
y
liftBin :: (a -> b -> c) -> a -> b -> Eval c
liftBin :: (a -> b -> c) -> a -> b -> Eval c
liftBin op :: a -> b -> c
op x :: a
x y :: b
y = c -> Eval c
forall a. a -> Eval a
ready (c -> Eval c) -> c -> Eval c
forall a b. (a -> b) -> a -> b
$ a -> b -> c
op a
x b
y
liftModBin :: (SInteger -> SInteger -> a) -> Integer -> SInteger -> SInteger -> Eval a
liftModBin :: (SBool -> SBool -> a) -> Integer -> SBool -> SBool -> Eval a
liftModBin op :: SBool -> SBool -> a
op modulus :: Integer
modulus x :: SBool
x y :: SBool
y = a -> Eval a
forall a. a -> Eval a
ready (a -> Eval a) -> a -> Eval a
forall a b. (a -> b) -> a -> b
$ SBool -> SBool -> a
op (SBool -> SBool -> SBool
SBV.svRem SBool
x SBool
m) (SBool -> SBool -> SBool
SBV.svRem SBool
y SBool
m)
where m :: SBool
m = Integer -> SBool
forall b w i. BitWord b w i => Integer -> i
integerLit Integer
modulus
sExp :: Integer -> SWord -> SWord -> Eval SWord
sExp :: BinArith SBool
sExp _w :: Integer
_w x :: SBool
x y :: SBool
y = SBool -> Eval SBool
forall a. a -> Eval a
ready (SBool -> Eval SBool) -> SBool -> Eval SBool
forall a b. (a -> b) -> a -> b
$ [SBool] -> SBool
go ([SBool] -> [SBool]
forall a. [a] -> [a]
reverse (SBool -> [SBool]
forall b w i. BitWord b w i => w -> [b]
unpackWord SBool
y))
where go :: [SBool] -> SBool
go [] = Int -> Integer -> SBool
literalSWord (SBool -> Int
forall a. HasKind a => a -> Int
SBV.intSizeOf SBool
x) 1
go (b :: SBool
b : bs :: [SBool]
bs) = SBool -> SBool -> SBool -> SBool
SBV.svIte SBool
b (SBool -> SBool -> SBool
SBV.svTimes SBool
x SBool
s) SBool
s
where a :: SBool
a = [SBool] -> SBool
go [SBool]
bs
s :: SBool
s = SBool -> SBool -> SBool
SBV.svTimes SBool
a SBool
a
sModAdd :: Integer -> SInteger -> SInteger -> Eval SInteger
sModAdd :: BinArith SBool
sModAdd modulus :: Integer
modulus x :: SBool
x y :: SBool
y =
case (SBool -> Maybe Integer
SBV.svAsInteger SBool
x, SBool -> Maybe Integer
SBV.svAsInteger SBool
y) of
(Just i :: Integer
i, Just j :: Integer
j) -> SBool -> Eval SBool
forall a. a -> Eval a
ready (SBool -> Eval SBool) -> SBool -> Eval SBool
forall a b. (a -> b) -> a -> b
$ Integer -> SBool
forall b w i. BitWord b w i => Integer -> i
integerLit ((Integer
i Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
j) Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`mod` Integer
modulus)
_ -> SBool -> Eval SBool
forall a. a -> Eval a
ready (SBool -> Eval SBool) -> SBool -> Eval SBool
forall a b. (a -> b) -> a -> b
$ SBool -> SBool -> SBool
SBV.svPlus SBool
x SBool
y
sModSub :: Integer -> SInteger -> SInteger -> Eval SInteger
sModSub :: BinArith SBool
sModSub modulus :: Integer
modulus x :: SBool
x y :: SBool
y =
case (SBool -> Maybe Integer
SBV.svAsInteger SBool
x, SBool -> Maybe Integer
SBV.svAsInteger SBool
y) of
(Just i :: Integer
i, Just j :: Integer
j) -> SBool -> Eval SBool
forall a. a -> Eval a
ready (SBool -> Eval SBool) -> SBool -> Eval SBool
forall a b. (a -> b) -> a -> b
$ Integer -> SBool
forall b w i. BitWord b w i => Integer -> i
integerLit ((Integer
i Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
j) Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`mod` Integer
modulus)
_ -> SBool -> Eval SBool
forall a. a -> Eval a
ready (SBool -> Eval SBool) -> SBool -> Eval SBool
forall a b. (a -> b) -> a -> b
$ SBool -> SBool -> SBool
SBV.svMinus SBool
x SBool
y
sModMult :: Integer -> SInteger -> SInteger -> Eval SInteger
sModMult :: BinArith SBool
sModMult modulus :: Integer
modulus x :: SBool
x y :: SBool
y =
case (SBool -> Maybe Integer
SBV.svAsInteger SBool
x, SBool -> Maybe Integer
SBV.svAsInteger SBool
y) of
(Just i :: Integer
i, Just j :: Integer
j) -> SBool -> Eval SBool
forall a. a -> Eval a
ready (SBool -> Eval SBool) -> SBool -> Eval SBool
forall a b. (a -> b) -> a -> b
$ Integer -> SBool
forall b w i. BitWord b w i => Integer -> i
integerLit ((Integer
i Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* Integer
j) Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`mod` Integer
modulus)
_ -> SBool -> Eval SBool
forall a. a -> Eval a
ready (SBool -> Eval SBool) -> SBool -> Eval SBool
forall a b. (a -> b) -> a -> b
$ SBool -> SBool -> SBool
SBV.svTimes SBool
x SBool
y
sModExp :: Integer -> SInteger -> SInteger -> Eval SInteger
sModExp :: BinArith SBool
sModExp modulus :: Integer
modulus x :: SBool
x y :: SBool
y = SBool -> Eval SBool
forall a. a -> Eval a
ready (SBool -> Eval SBool) -> SBool -> Eval SBool
forall a b. (a -> b) -> a -> b
$ SBool -> SBool -> SBool
SBV.svExp SBool
x (SBool -> SBool -> SBool
SBV.svRem SBool
y SBool
m)
where m :: SBool
m = Integer -> SBool
forall b w i. BitWord b w i => Integer -> i
integerLit Integer
modulus
sLg2 :: Integer -> SWord -> Eval SWord
sLg2 :: UnaryArith SBool
sLg2 _w :: Integer
_w x :: SBool
x = SBool -> Eval SBool
forall a. a -> Eval a
ready (SBool -> Eval SBool) -> SBool -> Eval SBool
forall a b. (a -> b) -> a -> b
$ Int -> SBool
go 0
where
lit :: Integer -> SBool
lit n :: Integer
n = Int -> Integer -> SBool
literalSWord (SBool -> Int
forall a. HasKind a => a -> Int
SBV.intSizeOf SBool
x) Integer
n
go :: Int -> SBool
go i :: Int
i | Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< SBool -> Int
forall a. HasKind a => a -> Int
SBV.intSizeOf SBool
x = SBool -> SBool -> SBool -> SBool
SBV.svIte (SBool -> SBool -> SBool
SBV.svLessEq SBool
x (Integer -> SBool
lit (2Integer -> Int -> Integer
forall a b. (Num a, Integral b) => a -> b -> a
^Int
i))) (Integer -> SBool
lit (Int -> Integer
forall a. Integral a => a -> Integer
toInteger Int
i)) (Int -> SBool
go (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 1))
| Bool
otherwise = Integer -> SBool
lit (Int -> Integer
forall a. Integral a => a -> Integer
toInteger Int
i)
svLg2 :: SInteger -> Eval SInteger
svLg2 :: SBool -> Eval SBool
svLg2 x :: SBool
x =
case SBool -> Maybe Integer
SBV.svAsInteger SBool
x of
Just n :: Integer
n -> SBool -> Eval SBool
forall a. a -> Eval a
ready (SBool -> Eval SBool) -> SBool -> Eval SBool
forall a b. (a -> b) -> a -> b
$ Kind -> Integer -> SBool
SBV.svInteger Kind
SBV.KUnbounded (Integer -> Integer
lg2 Integer
n)
Nothing -> String -> [String] -> Eval SBool
forall a. String -> [String] -> a
evalPanic "cannot compute lg2 of symbolic unbounded integer" []
svModLg2 :: Integer -> SInteger -> Eval SInteger
svModLg2 :: UnaryArith SBool
svModLg2 modulus :: Integer
modulus x :: SBool
x = SBool -> Eval SBool
svLg2 (SBool -> SBool -> SBool
SBV.svRem SBool
x SBool
m)
where m :: SBool
m = Integer -> SBool
forall b w i. BitWord b w i => Integer -> i
integerLit Integer
modulus
cmpEq :: SWord -> SWord -> Eval SBool -> Eval SBool
cmpEq :: SBool -> SBool -> Eval SBool -> Eval SBool
cmpEq x :: SBool
x y :: SBool
y k :: Eval SBool
k = SBool -> SBool -> SBool
SBV.svAnd (SBool -> SBool -> SBool
SBV.svEqual SBool
x SBool
y) (SBool -> SBool) -> Eval SBool -> Eval SBool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Eval SBool
k
cmpNotEq :: SWord -> SWord -> Eval SBool -> Eval SBool
cmpNotEq :: SBool -> SBool -> Eval SBool -> Eval SBool
cmpNotEq x :: SBool
x y :: SBool
y k :: Eval SBool
k = SBool -> SBool -> SBool
SBV.svOr (SBool -> SBool -> SBool
SBV.svNotEqual SBool
x SBool
y) (SBool -> SBool) -> Eval SBool -> Eval SBool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Eval SBool
k
cmpSignedLt :: SWord -> SWord -> Eval SBool -> Eval SBool
cmpSignedLt :: SBool -> SBool -> Eval SBool -> Eval SBool
cmpSignedLt x :: SBool
x y :: SBool
y k :: Eval SBool
k = SBool -> SBool -> SBool
SBV.svOr (SBool -> SBool -> SBool
SBV.svLessThan SBool
sx SBool
sy) (SBool -> SBool) -> Eval SBool -> Eval SBool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (SBool -> SBool -> Eval SBool -> Eval SBool
cmpEq SBool
sx SBool
sy Eval SBool
k)
where sx :: SBool
sx = SBool -> SBool
SBV.svSign SBool
x
sy :: SBool
sy = SBool -> SBool
SBV.svSign SBool
y
cmpLt, cmpGt :: SWord -> SWord -> Eval SBool -> Eval SBool
cmpLt :: SBool -> SBool -> Eval SBool -> Eval SBool
cmpLt x :: SBool
x y :: SBool
y k :: Eval SBool
k = SBool -> SBool -> SBool
SBV.svOr (SBool -> SBool -> SBool
SBV.svLessThan SBool
x SBool
y) (SBool -> SBool) -> Eval SBool -> Eval SBool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (SBool -> SBool -> Eval SBool -> Eval SBool
cmpEq SBool
x SBool
y Eval SBool
k)
cmpGt :: SBool -> SBool -> Eval SBool -> Eval SBool
cmpGt x :: SBool
x y :: SBool
y k :: Eval SBool
k = SBool -> SBool -> SBool
SBV.svOr (SBool -> SBool -> SBool
SBV.svGreaterThan SBool
x SBool
y) (SBool -> SBool) -> Eval SBool -> Eval SBool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (SBool -> SBool -> Eval SBool -> Eval SBool
cmpEq SBool
x SBool
y Eval SBool
k)
cmpLtEq, cmpGtEq :: SWord -> SWord -> Eval SBool -> Eval SBool
cmpLtEq :: SBool -> SBool -> Eval SBool -> Eval SBool
cmpLtEq x :: SBool
x y :: SBool
y k :: Eval SBool
k = SBool -> SBool -> SBool
SBV.svAnd (SBool -> SBool -> SBool
SBV.svLessEq SBool
x SBool
y) (SBool -> SBool) -> Eval SBool -> Eval SBool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (SBool -> SBool -> Eval SBool -> Eval SBool
cmpNotEq SBool
x SBool
y Eval SBool
k)
cmpGtEq :: SBool -> SBool -> Eval SBool -> Eval SBool
cmpGtEq x :: SBool
x y :: SBool
y k :: Eval SBool
k = SBool -> SBool -> SBool
SBV.svAnd (SBool -> SBool -> SBool
SBV.svGreaterEq SBool
x SBool
y) (SBool -> SBool) -> Eval SBool -> Eval SBool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (SBool -> SBool -> Eval SBool -> Eval SBool
cmpNotEq SBool
x SBool
y Eval SBool
k)
cmpMod ::
(SInteger -> SInteger -> Eval SBool -> Eval SBool) ->
(Integer -> SInteger -> SInteger -> Eval SBool -> Eval SBool)
cmpMod :: (SBool -> SBool -> Eval SBool -> Eval SBool)
-> Integer -> SBool -> SBool -> Eval SBool -> Eval SBool
cmpMod cmp :: SBool -> SBool -> Eval SBool -> Eval SBool
cmp modulus :: Integer
modulus x :: SBool
x y :: SBool
y k :: Eval SBool
k = SBool -> SBool -> Eval SBool -> Eval SBool
cmp (SBool -> SBool -> SBool
SBV.svRem SBool
x SBool
m) (SBool -> SBool -> SBool
SBV.svRem SBool
y SBool
m) Eval SBool
k
where m :: SBool
m = Integer -> SBool
forall b w i. BitWord b w i => Integer -> i
integerLit Integer
modulus
cmpModEq :: Integer -> SInteger -> SInteger -> Eval SBool -> Eval SBool
cmpModEq :: Integer -> SBool -> SBool -> Eval SBool -> Eval SBool
cmpModEq m :: Integer
m x :: SBool
x y :: SBool
y k :: Eval SBool
k = SBool -> SBool -> SBool
SBV.svAnd (Integer -> SBool -> SBool
svDivisible Integer
m (SBool -> SBool -> SBool
SBV.svMinus SBool
x SBool
y)) (SBool -> SBool) -> Eval SBool -> Eval SBool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Eval SBool
k
cmpModNotEq :: Integer -> SInteger -> SInteger -> Eval SBool -> Eval SBool
cmpModNotEq :: Integer -> SBool -> SBool -> Eval SBool -> Eval SBool
cmpModNotEq m :: Integer
m x :: SBool
x y :: SBool
y k :: Eval SBool
k = SBool -> SBool -> SBool
SBV.svOr (SBool -> SBool
SBV.svNot (Integer -> SBool -> SBool
svDivisible Integer
m (SBool -> SBool -> SBool
SBV.svMinus SBool
x SBool
y))) (SBool -> SBool) -> Eval SBool -> Eval SBool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Eval SBool
k
svDivisible :: Integer -> SInteger -> SBool
svDivisible :: Integer -> SBool -> SBool
svDivisible m :: Integer
m x :: SBool
x = SBool -> SBool -> SBool
SBV.svEqual (SBool -> SBool -> SBool
SBV.svRem SBool
x (Integer -> SBool
forall b w i. BitWord b w i => Integer -> i
integerLit Integer
m)) (Integer -> SBool
forall b w i. BitWord b w i => Integer -> i
integerLit 0)
cmpBinary :: (SBool -> SBool -> Eval SBool -> Eval SBool)
-> (SWord -> SWord -> Eval SBool -> Eval SBool)
-> (SInteger -> SInteger -> Eval SBool -> Eval SBool)
-> (Integer -> SInteger -> SInteger -> Eval SBool -> Eval SBool)
-> SBool -> Binary SBool SWord SInteger
cmpBinary :: (SBool -> SBool -> Eval SBool -> Eval SBool)
-> (SBool -> SBool -> Eval SBool -> Eval SBool)
-> (SBool -> SBool -> Eval SBool -> Eval SBool)
-> (Integer -> SBool -> SBool -> Eval SBool -> Eval SBool)
-> SBool
-> Binary SBool SBool SBool
cmpBinary fb :: SBool -> SBool -> Eval SBool -> Eval SBool
fb fw :: SBool -> SBool -> Eval SBool -> Eval SBool
fw fi :: SBool -> SBool -> Eval SBool -> Eval SBool
fi fz :: Integer -> SBool -> SBool -> Eval SBool -> Eval SBool
fz b :: SBool
b ty :: TValue
ty v1 :: GenValue SBool SBool SBool
v1 v2 :: GenValue SBool SBool SBool
v2 = SBool -> GenValue SBool SBool SBool
forall b w i. b -> GenValue b w i
VBit (SBool -> GenValue SBool SBool SBool)
-> Eval SBool -> Eval (GenValue SBool SBool SBool)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (SBool -> SBool -> Eval SBool -> Eval SBool)
-> (SBool -> SBool -> Eval SBool -> Eval SBool)
-> (SBool -> SBool -> Eval SBool -> Eval SBool)
-> (Integer -> SBool -> SBool -> Eval SBool -> Eval SBool)
-> TValue
-> GenValue SBool SBool SBool
-> GenValue SBool SBool SBool
-> Eval SBool
-> Eval SBool
forall b w i a.
BitWord b w i =>
(b -> b -> Eval a -> Eval a)
-> (w -> w -> Eval a -> Eval a)
-> (i -> i -> Eval a -> Eval a)
-> (Integer -> i -> i -> Eval a -> Eval a)
-> TValue
-> GenValue b w i
-> GenValue b w i
-> Eval a
-> Eval a
cmpValue SBool -> SBool -> Eval SBool -> Eval SBool
fb SBool -> SBool -> Eval SBool -> Eval SBool
fw SBool -> SBool -> Eval SBool -> Eval SBool
fi Integer -> SBool -> SBool -> Eval SBool -> Eval SBool
fz TValue
ty GenValue SBool SBool SBool
v1 GenValue SBool SBool SBool
v2 (SBool -> Eval SBool
forall (m :: * -> *) a. Monad m => a -> m a
return SBool
b)
signedQuot :: SWord -> SWord -> SWord
signedQuot :: SBool -> SBool -> SBool
signedQuot x :: SBool
x y :: SBool
y = SBool -> SBool
SBV.svUnsign (SBool -> SBool -> SBool
SBV.svQuot (SBool -> SBool
SBV.svSign SBool
x) (SBool -> SBool
SBV.svSign SBool
y))
signedRem :: SWord -> SWord -> SWord
signedRem :: SBool -> SBool -> SBool
signedRem x :: SBool
x y :: SBool
y = SBool -> SBool
SBV.svUnsign (SBool -> SBool -> SBool
SBV.svRem (SBool -> SBool
SBV.svSign SBool
x) (SBool -> SBool
SBV.svSign SBool
y))
sshrV :: Value
sshrV :: GenValue SBool SBool SBool
sshrV =
(Nat' -> GenValue SBool SBool SBool) -> GenValue SBool SBool SBool
forall b w i. (Nat' -> GenValue b w i) -> GenValue b w i
nlam ((Nat' -> GenValue SBool SBool SBool)
-> GenValue SBool SBool SBool)
-> (Nat' -> GenValue SBool SBool SBool)
-> GenValue SBool SBool SBool
forall a b. (a -> b) -> a -> b
$ \_n :: Nat'
_n ->
(Nat' -> GenValue SBool SBool SBool) -> GenValue SBool SBool SBool
forall b w i. (Nat' -> GenValue b w i) -> GenValue b w i
nlam ((Nat' -> GenValue SBool SBool SBool)
-> GenValue SBool SBool SBool)
-> (Nat' -> GenValue SBool SBool SBool)
-> GenValue SBool SBool SBool
forall a b. (a -> b) -> a -> b
$ \_k :: Nat'
_k ->
(SBool -> Eval (GenValue SBool SBool SBool))
-> GenValue SBool SBool SBool
forall b w i.
BitWord b w i =>
(w -> Eval (GenValue b w i)) -> GenValue b w i
wlam ((SBool -> Eval (GenValue SBool SBool SBool))
-> GenValue SBool SBool SBool)
-> (SBool -> Eval (GenValue SBool SBool SBool))
-> GenValue SBool SBool SBool
forall a b. (a -> b) -> a -> b
$ \x :: SBool
x -> GenValue SBool SBool SBool -> Eval (GenValue SBool SBool SBool)
forall (m :: * -> *) a. Monad m => a -> m a
return (GenValue SBool SBool SBool -> Eval (GenValue SBool SBool SBool))
-> GenValue SBool SBool SBool -> Eval (GenValue SBool SBool SBool)
forall a b. (a -> b) -> a -> b
$
(SBool -> Eval (GenValue SBool SBool SBool))
-> GenValue SBool SBool SBool
forall b w i.
BitWord b w i =>
(w -> Eval (GenValue b w i)) -> GenValue b w i
wlam ((SBool -> Eval (GenValue SBool SBool SBool))
-> GenValue SBool SBool SBool)
-> (SBool -> Eval (GenValue SBool SBool SBool))
-> GenValue SBool SBool SBool
forall a b. (a -> b) -> a -> b
$ \y :: SBool
y ->
case SBool -> Maybe Integer
SBV.svAsInteger SBool
y of
Just i :: Integer
i ->
let z :: SBool
z = SBool -> SBool
SBV.svUnsign (SBool -> Int -> SBool
SBV.svShr (SBool -> SBool
SBV.svSign SBool
x) (Integer -> Int
forall a. Num a => Integer -> a
fromInteger Integer
i))
in GenValue SBool SBool SBool -> Eval (GenValue SBool SBool SBool)
forall (m :: * -> *) a. Monad m => a -> m a
return (GenValue SBool SBool SBool -> Eval (GenValue SBool SBool SBool))
-> (SBool -> GenValue SBool SBool SBool)
-> SBool
-> Eval (GenValue SBool SBool SBool)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer
-> Eval (WordValue SBool SBool SBool) -> GenValue SBool SBool SBool
forall b w i. Integer -> Eval (WordValue b w i) -> GenValue b w i
VWord (Int -> Integer
forall a. Integral a => a -> Integer
toInteger (SBool -> Int
forall a. HasKind a => a -> Int
SBV.intSizeOf SBool
x)) (Eval (WordValue SBool SBool SBool) -> GenValue SBool SBool SBool)
-> (SBool -> Eval (WordValue SBool SBool SBool))
-> SBool
-> GenValue SBool SBool SBool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. WordValue SBool SBool SBool -> Eval (WordValue SBool SBool SBool)
forall a. a -> Eval a
ready (WordValue SBool SBool SBool -> Eval (WordValue SBool SBool SBool))
-> (SBool -> WordValue SBool SBool SBool)
-> SBool
-> Eval (WordValue SBool SBool SBool)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SBool -> WordValue SBool SBool SBool
forall b w i. w -> WordValue b w i
WordVal (SBool -> Eval (GenValue SBool SBool SBool))
-> SBool -> Eval (GenValue SBool SBool SBool)
forall a b. (a -> b) -> a -> b
$ SBool
z
Nothing ->
let z :: SBool
z = SBool -> SBool
SBV.svUnsign (SBool -> SBool -> SBool
SBV.svShiftRight (SBool -> SBool
SBV.svSign SBool
x) SBool
y)
in GenValue SBool SBool SBool -> Eval (GenValue SBool SBool SBool)
forall (m :: * -> *) a. Monad m => a -> m a
return (GenValue SBool SBool SBool -> Eval (GenValue SBool SBool SBool))
-> (SBool -> GenValue SBool SBool SBool)
-> SBool
-> Eval (GenValue SBool SBool SBool)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer
-> Eval (WordValue SBool SBool SBool) -> GenValue SBool SBool SBool
forall b w i. Integer -> Eval (WordValue b w i) -> GenValue b w i
VWord (Int -> Integer
forall a. Integral a => a -> Integer
toInteger (SBool -> Int
forall a. HasKind a => a -> Int
SBV.intSizeOf SBool
x)) (Eval (WordValue SBool SBool SBool) -> GenValue SBool SBool SBool)
-> (SBool -> Eval (WordValue SBool SBool SBool))
-> SBool
-> GenValue SBool SBool SBool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. WordValue SBool SBool SBool -> Eval (WordValue SBool SBool SBool)
forall a. a -> Eval a
ready (WordValue SBool SBool SBool -> Eval (WordValue SBool SBool SBool))
-> (SBool -> WordValue SBool SBool SBool)
-> SBool
-> Eval (WordValue SBool SBool SBool)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SBool -> WordValue SBool SBool SBool
forall b w i. w -> WordValue b w i
WordVal (SBool -> Eval (GenValue SBool SBool SBool))
-> SBool -> Eval (GenValue SBool SBool SBool)
forall a b. (a -> b) -> a -> b
$ SBool
z
carry :: SWord -> SWord -> Eval Value
carry :: SBool -> SBool -> Eval (GenValue SBool SBool SBool)
carry x :: SBool
x y :: SBool
y = GenValue SBool SBool SBool -> Eval (GenValue SBool SBool SBool)
forall (m :: * -> *) a. Monad m => a -> m a
return (GenValue SBool SBool SBool -> Eval (GenValue SBool SBool SBool))
-> GenValue SBool SBool SBool -> Eval (GenValue SBool SBool SBool)
forall a b. (a -> b) -> a -> b
$ SBool -> GenValue SBool SBool SBool
forall b w i. b -> GenValue b w i
VBit SBool
c
where
c :: SBool
c = SBool -> SBool -> SBool
SBV.svLessThan (SBool -> SBool -> SBool
SBV.svPlus SBool
x SBool
y) SBool
x
scarry :: SWord -> SWord -> Eval Value
scarry :: SBool -> SBool -> Eval (GenValue SBool SBool SBool)
scarry x :: SBool
x y :: SBool
y = GenValue SBool SBool SBool -> Eval (GenValue SBool SBool SBool)
forall (m :: * -> *) a. Monad m => a -> m a
return (GenValue SBool SBool SBool -> Eval (GenValue SBool SBool SBool))
-> GenValue SBool SBool SBool -> Eval (GenValue SBool SBool SBool)
forall a b. (a -> b) -> a -> b
$ SBool -> GenValue SBool SBool SBool
forall b w i. b -> GenValue b w i
VBit SBool
sc
where
n :: Int
n = SBool -> Int
forall a. HasKind a => a -> Int
SBV.intSizeOf SBool
x
z :: SBool
z = SBool -> SBool -> SBool
SBV.svPlus (SBool -> SBool
SBV.svSign SBool
x) (SBool -> SBool
SBV.svSign SBool
y)
xsign :: SBool
xsign = SBool -> Int -> SBool
SBV.svTestBit SBool
x (Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
-1)
ysign :: SBool
ysign = SBool -> Int -> SBool
SBV.svTestBit SBool
y (Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
-1)
zsign :: SBool
zsign = SBool -> Int -> SBool
SBV.svTestBit SBool
z (Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
-1)
sc :: SBool
sc = SBool -> SBool -> SBool
SBV.svAnd (SBool -> SBool -> SBool
SBV.svEqual SBool
xsign SBool
ysign) (SBool -> SBool -> SBool
SBV.svNotEqual SBool
xsign SBool
zsign)