{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE DoAndIfThenElse #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE ImplicitParams #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PatternGuards #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TupleSections #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE ViewPatterns #-}
module Cryptol.Backend.SeqMap
(
SeqMap
, indexSeqMap
, lookupSeqMap
, finiteSeqMap
, infiniteSeqMap
, enumerateSeqMap
, streamSeqMap
, reverseSeqMap
, updateSeqMap
, dropSeqMap
, concatSeqMap
, splitSeqMap
, memoMap
, delaySeqMap
, zipSeqMap
, mapSeqMap
, mergeSeqMap
, barrelShifter
, shiftSeqByInteger
, IndexSegment(..)
) where
import qualified Control.Exception as X
import Control.Monad
import Control.Monad.IO.Class
import Data.Bits
import Data.List
import Data.IORef
import Data.Map.Strict (Map)
import qualified Data.Map.Strict as Map
import Cryptol.Backend
import Cryptol.Backend.Concrete (Concrete)
import Cryptol.Backend.Monad (Unsupported(..))
import Cryptol.TypeCheck.Solver.InfNat(Nat'(..))
import Cryptol.Utils.Panic
data SeqMap sym a
= IndexSeqMap !(Integer -> SEval sym a)
| UpdateSeqMap !(Map Integer (SEval sym a))
!(SeqMap sym a)
| MemoSeqMap
!Nat'
!(IORef (Map Integer a))
!(IORef (Integer -> SEval sym a))
indexSeqMap :: (Integer -> SEval sym a) -> SeqMap sym a
indexSeqMap :: forall sym a. (Integer -> SEval sym a) -> SeqMap sym a
indexSeqMap = forall sym a. (Integer -> SEval sym a) -> SeqMap sym a
IndexSeqMap
lookupSeqMap :: Backend sym => SeqMap sym a -> Integer -> SEval sym a
lookupSeqMap :: forall sym a. Backend sym => SeqMap sym a -> Integer -> SEval sym a
lookupSeqMap (IndexSeqMap Integer -> SEval sym a
f) Integer
i = Integer -> SEval sym a
f Integer
i
lookupSeqMap (UpdateSeqMap Map Integer (SEval sym a)
m SeqMap sym a
xs) Integer
i =
case forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Integer
i Map Integer (SEval sym a)
m of
Just SEval sym a
x -> SEval sym a
x
Maybe (SEval sym a)
Nothing -> forall sym a. Backend sym => SeqMap sym a -> Integer -> SEval sym a
lookupSeqMap SeqMap sym a
xs Integer
i
lookupSeqMap (MemoSeqMap Nat'
sz IORef (Map Integer a)
cache IORef (Integer -> SEval sym a)
eval) Integer
i =
do Maybe a
mz <- forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Integer
i forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. IORef a -> IO a
readIORef IORef (Map Integer a)
cache)
case Maybe a
mz of
Just a
z -> forall (m :: * -> *) a. Monad m => a -> m a
return a
z
Maybe a
Nothing ->
do Integer -> SEval sym a
f <- forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (forall a. IORef a -> IO a
readIORef IORef (Integer -> SEval sym a)
eval)
a
v <- Integer -> SEval sym a
f Integer
i
Int
msz <- forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ forall a b. IORef a -> (a -> (a, b)) -> IO b
atomicModifyIORef' IORef (Map Integer a)
cache (\Map Integer a
m ->
let m' :: Map Integer a
m' = forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Integer
i a
v Map Integer a
m in (Map Integer a
m', forall k a. Map k a -> Int
Map.size Map Integer a
m'))
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (case Nat'
sz of Nat'
Inf -> Bool
False; Nat Integer
sz' -> forall a. Integral a => a -> Integer
toInteger Int
msz forall a. Ord a => a -> a -> Bool
>= Integer
sz')
(forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (forall a. IORef a -> a -> IO ()
writeIORef IORef (Integer -> SEval sym a)
eval
(\Integer
j -> forall a. HasCallStack => String -> [String] -> a
panic String
"lookupSeqMap" [String
"Messed up size accounting", forall a. Show a => a -> String
show Nat'
sz, forall a. Show a => a -> String
show Integer
j])))
forall (m :: * -> *) a. Monad m => a -> m a
return a
v
instance Backend sym => Functor (SeqMap sym) where
fmap :: forall a b. (a -> b) -> SeqMap sym a -> SeqMap sym b
fmap a -> b
f SeqMap sym a
xs = forall sym a. (Integer -> SEval sym a) -> SeqMap sym a
IndexSeqMap (\Integer
i -> a -> b
f forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym a. Backend sym => SeqMap sym a -> Integer -> SEval sym a
lookupSeqMap SeqMap sym a
xs Integer
i)
finiteSeqMap :: Backend sym => sym -> [SEval sym a] -> SeqMap sym a
finiteSeqMap :: forall sym a. Backend sym => sym -> [SEval sym a] -> SeqMap sym a
finiteSeqMap sym
sym [SEval sym a]
xs =
forall sym a.
Map Integer (SEval sym a) -> SeqMap sym a -> SeqMap sym a
UpdateSeqMap
(forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList (forall a b. [a] -> [b] -> [(a, b)]
zip [Integer
0..] [SEval sym a]
xs))
(forall sym a. (Integer -> SEval sym a) -> SeqMap sym a
IndexSeqMap (\Integer
i -> forall sym a. Backend sym => sym -> Integer -> SEval sym a
invalidIndex sym
sym Integer
i))
infiniteSeqMap :: Backend sym => sym -> [SEval sym a] -> SEval sym (SeqMap sym a)
infiniteSeqMap :: forall sym a.
Backend sym =>
sym -> [SEval sym a] -> SEval sym (SeqMap sym a)
infiniteSeqMap sym
sym [SEval sym a]
xs =
forall sym a.
Backend sym =>
sym -> Nat' -> SeqMap sym a -> SEval sym (SeqMap sym a)
memoMap sym
sym Nat'
Inf (forall sym a. (Integer -> SEval sym a) -> SeqMap sym a
IndexSeqMap forall a b. (a -> b) -> a -> b
$ \Integer
i -> forall i a. Integral i => [a] -> i -> a
genericIndex [SEval sym a]
xs Integer
i)
enumerateSeqMap :: (Backend sym, Integral n) => n -> SeqMap sym a -> [SEval sym a]
enumerateSeqMap :: forall sym n a.
(Backend sym, Integral n) =>
n -> SeqMap sym a -> [SEval sym a]
enumerateSeqMap n
n SeqMap sym a
m = [ forall sym a. Backend sym => SeqMap sym a -> Integer -> SEval sym a
lookupSeqMap SeqMap sym a
m Integer
i | Integer
i <- [Integer
0 .. (forall a. Integral a => a -> Integer
toInteger n
n)forall a. Num a => a -> a -> a
-Integer
1] ]
streamSeqMap :: Backend sym => SeqMap sym a -> [SEval sym a]
streamSeqMap :: forall sym a. Backend sym => SeqMap sym a -> [SEval sym a]
streamSeqMap SeqMap sym a
m = [ forall sym a. Backend sym => SeqMap sym a -> Integer -> SEval sym a
lookupSeqMap SeqMap sym a
m Integer
i | Integer
i <- [Integer
0..] ]
reverseSeqMap :: Backend sym =>
Integer ->
SeqMap sym a ->
SeqMap sym a
reverseSeqMap :: forall sym a.
Backend sym =>
Integer -> SeqMap sym a -> SeqMap sym a
reverseSeqMap Integer
n SeqMap sym a
vals = forall sym a. (Integer -> SEval sym a) -> SeqMap sym a
IndexSeqMap forall a b. (a -> b) -> a -> b
$ \Integer
i -> forall sym a. Backend sym => SeqMap sym a -> Integer -> SEval sym a
lookupSeqMap SeqMap sym a
vals (Integer
n forall a. Num a => a -> a -> a
- Integer
1 forall a. Num a => a -> a -> a
- Integer
i)
updateSeqMap :: SeqMap sym a -> Integer -> SEval sym a -> SeqMap sym a
updateSeqMap :: forall sym a.
SeqMap sym a -> Integer -> SEval sym a -> SeqMap sym a
updateSeqMap (UpdateSeqMap Map Integer (SEval sym a)
m SeqMap sym a
sm) Integer
i SEval sym a
x = forall sym a.
Map Integer (SEval sym a) -> SeqMap sym a -> SeqMap sym a
UpdateSeqMap (forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Integer
i SEval sym a
x Map Integer (SEval sym a)
m) SeqMap sym a
sm
updateSeqMap SeqMap sym a
xs Integer
i SEval sym a
x = forall sym a.
Map Integer (SEval sym a) -> SeqMap sym a -> SeqMap sym a
UpdateSeqMap (forall k a. k -> a -> Map k a
Map.singleton Integer
i SEval sym a
x) SeqMap sym a
xs
concatSeqMap :: Backend sym => Integer -> SeqMap sym a -> SeqMap sym a -> SeqMap sym a
concatSeqMap :: forall sym a.
Backend sym =>
Integer -> SeqMap sym a -> SeqMap sym a -> SeqMap sym a
concatSeqMap Integer
n SeqMap sym a
x SeqMap sym a
y =
forall sym a. (Integer -> SEval sym a) -> SeqMap sym a
IndexSeqMap forall a b. (a -> b) -> a -> b
$ \Integer
i ->
if Integer
i forall a. Ord a => a -> a -> Bool
< Integer
n
then forall sym a. Backend sym => SeqMap sym a -> Integer -> SEval sym a
lookupSeqMap SeqMap sym a
x Integer
i
else forall sym a. Backend sym => SeqMap sym a -> Integer -> SEval sym a
lookupSeqMap SeqMap sym a
y (Integer
iforall a. Num a => a -> a -> a
-Integer
n)
splitSeqMap :: Backend sym => Integer -> SeqMap sym a -> (SeqMap sym a, SeqMap sym a)
splitSeqMap :: forall sym a.
Backend sym =>
Integer -> SeqMap sym a -> (SeqMap sym a, SeqMap sym a)
splitSeqMap Integer
n SeqMap sym a
xs = (SeqMap sym a
hd,SeqMap sym a
tl)
where
hd :: SeqMap sym a
hd = SeqMap sym a
xs
tl :: SeqMap sym a
tl = forall sym a. (Integer -> SEval sym a) -> SeqMap sym a
IndexSeqMap forall a b. (a -> b) -> a -> b
$ \Integer
i -> forall sym a. Backend sym => SeqMap sym a -> Integer -> SEval sym a
lookupSeqMap SeqMap sym a
xs (Integer
iforall a. Num a => a -> a -> a
+Integer
n)
dropSeqMap :: Backend sym => Integer -> SeqMap sym a -> SeqMap sym a
dropSeqMap :: forall sym a.
Backend sym =>
Integer -> SeqMap sym a -> SeqMap sym a
dropSeqMap Integer
0 SeqMap sym a
xs = SeqMap sym a
xs
dropSeqMap Integer
n SeqMap sym a
xs = forall sym a. (Integer -> SEval sym a) -> SeqMap sym a
IndexSeqMap forall a b. (a -> b) -> a -> b
$ \Integer
i -> forall sym a. Backend sym => SeqMap sym a -> Integer -> SEval sym a
lookupSeqMap SeqMap sym a
xs (Integer
iforall a. Num a => a -> a -> a
+Integer
n)
delaySeqMap :: Backend sym => sym -> SEval sym (SeqMap sym a) -> SEval sym (SeqMap sym a)
delaySeqMap :: forall sym a.
Backend sym =>
sym -> SEval sym (SeqMap sym a) -> SEval sym (SeqMap sym a)
delaySeqMap sym
sym SEval sym (SeqMap sym a)
xs =
do SEval sym (SeqMap sym a)
xs' <- forall sym a.
Backend sym =>
sym -> SEval sym a -> SEval sym (SEval sym a)
sDelay sym
sym SEval sym (SeqMap sym a)
xs
forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall sym a. (Integer -> SEval sym a) -> SeqMap sym a
IndexSeqMap forall a b. (a -> b) -> a -> b
$ \Integer
i -> do SeqMap sym a
m <- SEval sym (SeqMap sym a)
xs'; forall sym a. Backend sym => SeqMap sym a -> Integer -> SEval sym a
lookupSeqMap SeqMap sym a
m Integer
i
memoMap :: Backend sym => sym -> Nat' -> SeqMap sym a -> SEval sym (SeqMap sym a)
memoMap :: forall sym a.
Backend sym =>
sym -> Nat' -> SeqMap sym a -> SEval sym (SeqMap sym a)
memoMap sym
_sym Nat'
_sz x :: SeqMap sym a
x@(MemoSeqMap{}) = forall (f :: * -> *) a. Applicative f => a -> f a
pure SeqMap sym a
x
memoMap sym
sym Nat'
sz SeqMap sym a
x = do
CallStack
stk <- forall sym. Backend sym => sym -> SEval sym CallStack
sGetCallStack sym
sym
IORef (Map Integer a)
cache <- forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ forall a. a -> IO (IORef a)
newIORef forall a b. (a -> b) -> a -> b
$ forall k a. Map k a
Map.empty
IORef (Integer -> SEval sym a)
evalRef <- forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ forall a. a -> IO (IORef a)
newIORef forall a b. (a -> b) -> a -> b
$ CallStack -> Integer -> SEval sym a
eval CallStack
stk
forall (m :: * -> *) a. Monad m => a -> m a
return (forall sym a.
Nat'
-> IORef (Map Integer a)
-> IORef (Integer -> SEval sym a)
-> SeqMap sym a
MemoSeqMap Nat'
sz IORef (Map Integer a)
cache IORef (Integer -> SEval sym a)
evalRef)
where
eval :: CallStack -> Integer -> SEval sym a
eval CallStack
stk Integer
i = forall sym a.
Backend sym =>
sym -> CallStack -> SEval sym a -> SEval sym a
sWithCallStack sym
sym CallStack
stk (forall sym a. Backend sym => SeqMap sym a -> Integer -> SEval sym a
lookupSeqMap SeqMap sym a
x Integer
i)
zipSeqMap ::
Backend sym =>
sym ->
(a -> a -> SEval sym a) ->
Nat' ->
SeqMap sym a ->
SeqMap sym a ->
SEval sym (SeqMap sym a)
zipSeqMap :: forall sym a.
Backend sym =>
sym
-> (a -> a -> SEval sym a)
-> Nat'
-> SeqMap sym a
-> SeqMap sym a
-> SEval sym (SeqMap sym a)
zipSeqMap sym
sym a -> a -> SEval sym a
f Nat'
sz SeqMap sym a
x SeqMap sym a
y =
forall sym a.
Backend sym =>
sym -> Nat' -> SeqMap sym a -> SEval sym (SeqMap sym a)
memoMap sym
sym Nat'
sz (forall sym a. (Integer -> SEval sym a) -> SeqMap sym a
IndexSeqMap forall a b. (a -> b) -> a -> b
$ \Integer
i -> forall (m :: * -> *) a. Monad m => m (m a) -> m a
join (a -> a -> SEval sym a
f forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym a. Backend sym => SeqMap sym a -> Integer -> SEval sym a
lookupSeqMap SeqMap sym a
x Integer
i forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall sym a. Backend sym => SeqMap sym a -> Integer -> SEval sym a
lookupSeqMap SeqMap sym a
y Integer
i))
mapSeqMap ::
Backend sym =>
sym ->
(a -> SEval sym a) ->
Nat' ->
SeqMap sym a ->
SEval sym (SeqMap sym a)
mapSeqMap :: forall sym a.
Backend sym =>
sym
-> (a -> SEval sym a)
-> Nat'
-> SeqMap sym a
-> SEval sym (SeqMap sym a)
mapSeqMap sym
sym a -> SEval sym a
f Nat'
sz SeqMap sym a
x =
forall sym a.
Backend sym =>
sym -> Nat' -> SeqMap sym a -> SEval sym (SeqMap sym a)
memoMap sym
sym Nat'
sz (forall sym a. (Integer -> SEval sym a) -> SeqMap sym a
IndexSeqMap forall a b. (a -> b) -> a -> b
$ \Integer
i -> a -> SEval sym a
f forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall sym a. Backend sym => SeqMap sym a -> Integer -> SEval sym a
lookupSeqMap SeqMap sym a
x Integer
i)
{-# INLINE mergeSeqMap #-}
mergeSeqMap :: Backend sym =>
sym ->
(SBit sym -> a -> a -> SEval sym a) ->
SBit sym ->
SeqMap sym a ->
SeqMap sym a ->
SeqMap sym a
mergeSeqMap :: forall sym a.
Backend sym =>
sym
-> (SBit sym -> a -> a -> SEval sym a)
-> SBit sym
-> SeqMap sym a
-> SeqMap sym a
-> SeqMap sym a
mergeSeqMap sym
sym SBit sym -> a -> a -> SEval sym a
f SBit sym
c SeqMap sym a
x SeqMap sym a
y =
forall sym a. (Integer -> SEval sym a) -> SeqMap sym a
IndexSeqMap forall a b. (a -> b) -> a -> b
$ \Integer
i -> forall sym a.
Backend sym =>
sym
-> (SBit sym -> a -> a -> SEval sym a)
-> SBit sym
-> SEval sym a
-> SEval sym a
-> SEval sym a
mergeEval sym
sym SBit sym -> a -> a -> SEval sym a
f SBit sym
c (forall sym a. Backend sym => SeqMap sym a -> Integer -> SEval sym a
lookupSeqMap SeqMap sym a
x Integer
i) (forall sym a. Backend sym => SeqMap sym a -> Integer -> SEval sym a
lookupSeqMap SeqMap sym a
y Integer
i)
{-# INLINE shiftSeqByInteger #-}
shiftSeqByInteger :: Backend sym =>
sym ->
(SBit sym -> a -> a -> SEval sym a)
->
(Integer -> Integer -> Maybe Integer)
->
SEval sym a ->
Nat' ->
SeqMap sym a ->
SInteger sym ->
SEval sym (SeqMap sym a)
shiftSeqByInteger :: forall sym a.
Backend sym =>
sym
-> (SBit sym -> a -> a -> SEval sym a)
-> (Integer -> Integer -> Maybe Integer)
-> SEval sym a
-> Nat'
-> SeqMap sym a
-> SInteger sym
-> SEval sym (SeqMap sym a)
shiftSeqByInteger sym
sym SBit sym -> a -> a -> SEval sym a
merge Integer -> Integer -> Maybe Integer
reindex SEval sym a
zro Nat'
m SeqMap sym a
xs SInteger sym
idx
| Just Integer
j <- forall sym. Backend sym => sym -> SInteger sym -> Maybe Integer
integerAsLit sym
sym SInteger sym
idx = SeqMap sym a -> Integer -> SEval sym (SeqMap sym a)
shiftOp SeqMap sym a
xs Integer
j
| Bool
otherwise =
do (Integer
n, [SBit sym]
idx_bits) <- forall sym.
Backend sym =>
sym -> Nat' -> SInteger sym -> SEval sym (Integer, [SBit sym])
enumerateIntBits sym
sym Nat'
m SInteger sym
idx
forall sym a.
Backend sym =>
sym
-> (SBit sym -> a -> a -> SEval sym a)
-> (SeqMap sym a -> Integer -> SEval sym (SeqMap sym a))
-> Nat'
-> SeqMap sym a
-> Integer
-> [IndexSegment sym]
-> SEval sym (SeqMap sym a)
barrelShifter sym
sym SBit sym -> a -> a -> SEval sym a
merge SeqMap sym a -> Integer -> SEval sym (SeqMap sym a)
shiftOp Nat'
m SeqMap sym a
xs Integer
n (forall a b. (a -> b) -> [a] -> [b]
map forall sym. SBit sym -> IndexSegment sym
BitIndexSegment [SBit sym]
idx_bits)
where
shiftOp :: SeqMap sym a -> Integer -> SEval sym (SeqMap sym a)
shiftOp SeqMap sym a
vs Integer
shft =
forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall sym a. (Integer -> SEval sym a) -> SeqMap sym a
indexSeqMap forall a b. (a -> b) -> a -> b
$ \Integer
i ->
case Integer -> Integer -> Maybe Integer
reindex Integer
i Integer
shft of
Maybe Integer
Nothing -> SEval sym a
zro
Just Integer
i' -> forall sym a. Backend sym => SeqMap sym a -> Integer -> SEval sym a
lookupSeqMap SeqMap sym a
vs Integer
i'
data IndexSegment sym
= BitIndexSegment (SBit sym)
| WordIndexSegment (SWord sym)
{-# SPECIALIZE
barrelShifter ::
Concrete ->
(SBit Concrete -> a -> a -> SEval Concrete a) ->
(SeqMap Concrete a -> Integer -> SEval Concrete (SeqMap Concrete a)) ->
Nat' ->
SeqMap Concrete a ->
Integer ->
[IndexSegment Concrete] ->
SEval Concrete (SeqMap Concrete a)
#-}
barrelShifter :: Backend sym =>
sym ->
(SBit sym -> a -> a -> SEval sym a)
->
(SeqMap sym a -> Integer -> SEval sym (SeqMap sym a))
->
Nat' ->
SeqMap sym a ->
Integer ->
[IndexSegment sym] ->
SEval sym (SeqMap sym a)
barrelShifter :: forall sym a.
Backend sym =>
sym
-> (SBit sym -> a -> a -> SEval sym a)
-> (SeqMap sym a -> Integer -> SEval sym (SeqMap sym a))
-> Nat'
-> SeqMap sym a
-> Integer
-> [IndexSegment sym]
-> SEval sym (SeqMap sym a)
barrelShifter sym
sym SBit sym -> a -> a -> SEval sym a
mux SeqMap sym a -> Integer -> SEval sym (SeqMap sym a)
shift_op Nat'
sz SeqMap sym a
x0 Integer
n0 [IndexSegment sym]
bs0
| Integer
n0 forall a. Ord a => a -> a -> Bool
>= forall a. Integral a => a -> Integer
toInteger (forall a. Bounded a => a
maxBound :: Int) =
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (forall a e. Exception e => e -> a
X.throw (String -> Unsupported
UnsupportedSymbolicOp (String
"Barrel shifter with too many bits in shift amount: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Integer
n0)))
| Bool
otherwise = SeqMap sym a
-> Int -> [IndexSegment sym] -> SEval sym (SeqMap sym a)
go SeqMap sym a
x0 (forall a. Num a => Integer -> a
fromInteger Integer
n0) [IndexSegment sym]
bs0
where
go :: SeqMap sym a
-> Int -> [IndexSegment sym] -> SEval sym (SeqMap sym a)
go SeqMap sym a
x !Int
_n [] = forall (m :: * -> *) a. Monad m => a -> m a
return SeqMap sym a
x
go SeqMap sym a
x !Int
n (WordIndexSegment SWord sym
w:[IndexSegment sym]
bs) =
let n' :: Int
n' = Int
n forall a. Num a => a -> a -> a
- forall a. Num a => Integer -> a
fromInteger (forall sym. Backend sym => sym -> SWord sym -> Integer
wordLen sym
sym SWord sym
w) in
case forall sym.
Backend sym =>
sym -> SWord sym -> Maybe (Integer, Integer)
wordAsLit sym
sym SWord sym
w of
Just (Integer
_,Integer
0) -> SeqMap sym a
-> Int -> [IndexSegment sym] -> SEval sym (SeqMap sym a)
go SeqMap sym a
x Int
n' [IndexSegment sym]
bs
Just (Integer
_,Integer
j) ->
do SeqMap sym a
x_shft <- SeqMap sym a -> Integer -> SEval sym (SeqMap sym a)
shift_op SeqMap sym a
x (Integer
j forall a. Num a => a -> a -> a
* forall a. Bits a => Int -> a
bit Int
n')
SeqMap sym a
-> Int -> [IndexSegment sym] -> SEval sym (SeqMap sym a)
go SeqMap sym a
x_shft Int
n' [IndexSegment sym]
bs
Maybe (Integer, Integer)
Nothing ->
do [SBit sym]
wbs <- forall sym. Backend sym => sym -> SWord sym -> SEval sym [SBit sym]
unpackWord sym
sym SWord sym
w
SeqMap sym a
-> Int -> [IndexSegment sym] -> SEval sym (SeqMap sym a)
go SeqMap sym a
x Int
n (forall a b. (a -> b) -> [a] -> [b]
map forall sym. SBit sym -> IndexSegment sym
BitIndexSegment [SBit sym]
wbs forall a. [a] -> [a] -> [a]
++ [IndexSegment sym]
bs)
go SeqMap sym a
x !Int
n (BitIndexSegment SBit sym
b:[IndexSegment sym]
bs) =
let n' :: Int
n' = Int
n forall a. Num a => a -> a -> a
- Int
1 in
case forall sym. Backend sym => sym -> SBit sym -> Maybe Bool
bitAsLit sym
sym SBit sym
b of
Just Bool
False -> SeqMap sym a
-> Int -> [IndexSegment sym] -> SEval sym (SeqMap sym a)
go SeqMap sym a
x Int
n' [IndexSegment sym]
bs
Just Bool
True ->
do SeqMap sym a
x_shft <- SeqMap sym a -> Integer -> SEval sym (SeqMap sym a)
shift_op SeqMap sym a
x (forall a. Bits a => Int -> a
bit Int
n')
SeqMap sym a
-> Int -> [IndexSegment sym] -> SEval sym (SeqMap sym a)
go SeqMap sym a
x_shft Int
n' [IndexSegment sym]
bs
Maybe Bool
Nothing ->
do SeqMap sym a
x_shft <- SeqMap sym a -> Integer -> SEval sym (SeqMap sym a)
shift_op SeqMap sym a
x (forall a. Bits a => Int -> a
bit Int
n')
SeqMap sym a
x' <- forall sym a.
Backend sym =>
sym -> Nat' -> SeqMap sym a -> SEval sym (SeqMap sym a)
memoMap sym
sym Nat'
sz (forall sym a.
Backend sym =>
sym
-> (SBit sym -> a -> a -> SEval sym a)
-> SBit sym
-> SeqMap sym a
-> SeqMap sym a
-> SeqMap sym a
mergeSeqMap sym
sym SBit sym -> a -> a -> SEval sym a
mux SBit sym
b SeqMap sym a
x_shft SeqMap sym a
x)
SeqMap sym a
-> Int -> [IndexSegment sym] -> SEval sym (SeqMap sym a)
go SeqMap sym a
x' Int
n' [IndexSegment sym]
bs