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

{-# LANGUAGE BangPatterns #-}
{-# 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.WordValue
  ( -- * WordValue
    WordValue
  , wordVal
  , bitmapWordVal
  , asWordList
  , asWordVal
  , asBitsMap
  , joinWordVal
  , takeWordVal
  , dropWordVal
  , extractWordVal
  , wordValLogicOp
  , wordValUnaryOp
  , assertWordValueInBounds
  , enumerateWordValue
  , enumerateWordValueRev
  , enumerateIndexSegments
  , wordValueSize
  , indexWordValue
  , updateWordValue
  , delayWordValue
  , joinWords
  , shiftSeqByWord
  , shiftWordByInteger
  , shiftWordByWord
  , wordValAsLit
  , reverseWordVal
  , forceWordValue
  , wordValueEqualsInteger
  , updateWordByWord

  , mergeWord
  , mergeWord'
  ) where

import Control.Monad (unless)
import Data.Bits
import GHC.Generics (Generic)

import Cryptol.Backend
import Cryptol.Backend.Concrete (Concrete(..))
import Cryptol.Backend.Monad (EvalError(..))
import Cryptol.Backend.SeqMap

import Cryptol.TypeCheck.Solver.InfNat(widthInteger, Nat'(..))

-- | Force the evaluation of a word value
forceWordValue :: Backend sym => WordValue sym -> SEval sym ()
forceWordValue :: forall sym. Backend sym => WordValue sym -> SEval sym ()
forceWordValue (WordVal SWord sym
w)  = seq :: forall a b. a -> b -> b
seq SWord sym
w (forall (m :: * -> *) a. Monad m => a -> m a
return ())
forceWordValue (ThunkWordVal Integer
_ SEval sym (WordValue sym)
m)  = forall sym. Backend sym => WordValue sym -> SEval sym ()
forceWordValue forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< SEval sym (WordValue sym)
m
forceWordValue (BitmapVal Integer
_n SEval sym (SWord sym)
packed SeqMap sym (SBit sym)
_) = do SWord sym
w <- SEval sym (SWord sym)
packed; seq :: forall a b. a -> b -> b
seq SWord sym
w (forall (m :: * -> *) a. Monad m => a -> m a
return ())

-- | An arbitrarily-chosen number of elements where we switch from a dense
--   sequence representation of bit-level words to 'SeqMap' representation.
largeBitSize :: Integer
largeBitSize :: Integer
largeBitSize = forall a. Bits a => Int -> a
bit Int
32

-- | For efficiency reasons, we handle finite sequences of bits as special cases
--   in the evaluator.  In cases where we know it is safe to do so, we prefer to
--   used a "packed word" representation of bit sequences.  This allows us to rely
--   directly on Integer types (in the concrete evaluator) and SBV's Word types (in
--   the symbolic simulator).
--
--   However, if we cannot be sure all the bits of the sequence
--   will eventually be forced, we must instead rely on an explicit sequence of bits
--   representation.
data WordValue sym
  = ThunkWordVal Integer !(SEval sym (WordValue sym))
  | WordVal !(SWord sym)                      -- ^ Packed word representation for bit sequences.
  | BitmapVal
       !Integer -- ^ Length of the word
       !(SEval sym (SWord sym)) -- ^ Thunk for packing the word
       !(SeqMap sym (SBit sym)) -- ^
 deriving (forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall sym x. Rep (WordValue sym) x -> WordValue sym
forall sym x. WordValue sym -> Rep (WordValue sym) x
$cto :: forall sym x. Rep (WordValue sym) x -> WordValue sym
$cfrom :: forall sym x. WordValue sym -> Rep (WordValue sym) x
Generic)

wordVal :: SWord sym -> WordValue sym
wordVal :: forall sym. SWord sym -> WordValue sym
wordVal = forall sym. SWord sym -> WordValue sym
WordVal

packBitmap :: Backend sym => sym -> Integer -> SeqMap sym (SBit sym) -> SEval sym (SWord sym)
packBitmap :: forall sym.
Backend sym =>
sym -> Integer -> SeqMap sym (SBit sym) -> SEval sym (SWord sym)
packBitmap sym
sym Integer
sz SeqMap sym (SBit sym)
bs = forall sym.
Backend sym =>
sym -> [SBit sym] -> SEval sym (SWord sym)
packWord sym
sym forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence (forall sym n a.
(Backend sym, Integral n) =>
n -> SeqMap sym a -> [SEval sym a]
enumerateSeqMap Integer
sz SeqMap sym (SBit sym)
bs)

unpackBitmap :: Backend sym => sym -> SWord sym -> SeqMap sym (SBit sym)
unpackBitmap :: forall sym.
Backend sym =>
sym -> SWord sym -> SeqMap sym (SBit sym)
unpackBitmap sym
sym SWord sym
w = forall sym a. (Integer -> SEval sym a) -> SeqMap sym a
indexSeqMap forall a b. (a -> b) -> a -> b
$ \Integer
i -> forall sym.
Backend sym =>
sym -> SWord sym -> Integer -> SEval sym (SBit sym)
wordBit sym
sym SWord sym
w Integer
i

bitmapWordVal :: Backend sym => sym -> Integer -> SeqMap sym (SBit sym) -> SEval sym (WordValue sym)
bitmapWordVal :: forall sym.
Backend sym =>
sym
-> Integer -> SeqMap sym (SBit sym) -> SEval sym (WordValue sym)
bitmapWordVal sym
sym Integer
sz SeqMap sym (SBit sym)
bs =
  do SEval sym (SWord sym)
packed <- forall sym a.
Backend sym =>
sym -> SEval sym a -> SEval sym (SEval sym a)
sDelay sym
sym (forall sym.
Backend sym =>
sym -> Integer -> SeqMap sym (SBit sym) -> SEval sym (SWord sym)
packBitmap sym
sym Integer
sz SeqMap sym (SBit sym)
bs)
     forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall sym.
Integer
-> SEval sym (SWord sym) -> SeqMap sym (SBit sym) -> WordValue sym
BitmapVal Integer
sz SEval sym (SWord sym)
packed SeqMap sym (SBit sym)
bs)

{-# INLINE joinWordVal #-}
joinWordVal :: Backend sym => sym -> WordValue sym -> WordValue sym -> SEval sym (WordValue sym)
joinWordVal :: forall sym.
Backend sym =>
sym -> WordValue sym -> WordValue sym -> SEval sym (WordValue sym)
joinWordVal sym
sym WordValue sym
wv1 WordValue sym
wv2 =
  let fallback :: SEval sym (WordValue sym)
fallback = forall sym.
Backend sym =>
sym -> WordValue sym -> WordValue sym -> SEval sym (WordValue sym)
fallbackWordJoin sym
sym WordValue sym
wv1 WordValue sym
wv2 in
  case (WordValue sym
wv1, WordValue sym
wv2) of
    (WordVal SWord sym
w1, WordVal SWord sym
w2) ->
      forall sym. SWord sym -> WordValue sym
WordVal forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym.
Backend sym =>
sym -> SWord sym -> SWord sym -> SEval sym (SWord sym)
joinWord sym
sym SWord sym
w1 SWord sym
w2

    (ThunkWordVal Integer
_ SEval sym (WordValue sym)
m1, WordValue sym
_) ->
      forall sym a.
Backend sym =>
sym -> SEval sym a -> SEval sym (Maybe a)
isReady sym
sym SEval sym (WordValue sym)
m1 forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
        Just WordValue sym
x -> forall sym.
Backend sym =>
sym -> WordValue sym -> WordValue sym -> SEval sym (WordValue sym)
joinWordVal sym
sym WordValue sym
x WordValue sym
wv2
        Maybe (WordValue sym)
Nothing -> SEval sym (WordValue sym)
fallback

    (WordValue sym
_,ThunkWordVal Integer
_ SEval sym (WordValue sym)
m2) ->
      forall sym a.
Backend sym =>
sym -> SEval sym a -> SEval sym (Maybe a)
isReady sym
sym SEval sym (WordValue sym)
m2 forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
        Just WordValue sym
x   -> forall sym.
Backend sym =>
sym -> WordValue sym -> WordValue sym -> SEval sym (WordValue sym)
joinWordVal sym
sym WordValue sym
wv1 WordValue sym
x
        Maybe (WordValue sym)
Nothing  -> SEval sym (WordValue sym)
fallback

    (WordVal SWord sym
w1, BitmapVal Integer
_ SEval sym (SWord sym)
packed2 SeqMap sym (SBit sym)
_) ->
      forall sym a.
Backend sym =>
sym -> SEval sym a -> SEval sym (Maybe a)
isReady sym
sym SEval sym (SWord sym)
packed2 forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
        Just SWord sym
w2 -> forall sym. SWord sym -> WordValue sym
WordVal forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym.
Backend sym =>
sym -> SWord sym -> SWord sym -> SEval sym (SWord sym)
joinWord sym
sym SWord sym
w1 SWord sym
w2
        Maybe (SWord sym)
Nothing  -> SEval sym (WordValue sym)
fallback

    (BitmapVal Integer
_ SEval sym (SWord sym)
packed1 SeqMap sym (SBit sym)
_, WordVal SWord sym
w2) ->
      forall sym a.
Backend sym =>
sym -> SEval sym a -> SEval sym (Maybe a)
isReady sym
sym SEval sym (SWord sym)
packed1 forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
        Just SWord sym
w1 -> forall sym. SWord sym -> WordValue sym
WordVal forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym.
Backend sym =>
sym -> SWord sym -> SWord sym -> SEval sym (SWord sym)
joinWord sym
sym SWord sym
w1 SWord sym
w2
        Maybe (SWord sym)
Nothing -> SEval sym (WordValue sym)
fallback

    (BitmapVal Integer
_ SEval sym (SWord sym)
packed1 SeqMap sym (SBit sym)
_, BitmapVal Integer
_ SEval sym (SWord sym)
packed2 SeqMap sym (SBit sym)
_) ->
      do Maybe (SWord sym)
r1 <- forall sym a.
Backend sym =>
sym -> SEval sym a -> SEval sym (Maybe a)
isReady sym
sym SEval sym (SWord sym)
packed1
         Maybe (SWord sym)
r2 <- forall sym a.
Backend sym =>
sym -> SEval sym a -> SEval sym (Maybe a)
isReady sym
sym SEval sym (SWord sym)
packed2
         case (Maybe (SWord sym)
r1,Maybe (SWord sym)
r2) of
           (Just SWord sym
w1, Just SWord sym
w2) -> forall sym. SWord sym -> WordValue sym
WordVal forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym.
Backend sym =>
sym -> SWord sym -> SWord sym -> SEval sym (SWord sym)
joinWord sym
sym SWord sym
w1 SWord sym
w2
           (Maybe (SWord sym), Maybe (SWord sym))
_ -> SEval sym (WordValue sym)
fallback

{-# INLINE fallbackWordJoin #-}
fallbackWordJoin :: Backend sym => sym -> WordValue sym -> WordValue sym -> SEval sym (WordValue sym)
fallbackWordJoin :: forall sym.
Backend sym =>
sym -> WordValue sym -> WordValue sym -> SEval sym (WordValue sym)
fallbackWordJoin sym
sym WordValue sym
w1 WordValue sym
w2 =
  do let n1 :: Integer
n1 = forall sym. Backend sym => sym -> WordValue sym -> Integer
wordValueSize sym
sym WordValue sym
w1
     let n2 :: Integer
n2 = forall sym. Backend sym => sym -> WordValue sym -> Integer
wordValueSize sym
sym WordValue sym
w2
     let len :: Integer
len = Integer
n1 forall a. Num a => a -> a -> a
+ Integer
n2
     SEval sym (SWord sym)
packed <- forall sym a.
Backend sym =>
sym -> SEval sym a -> SEval sym (SEval sym a)
sDelay sym
sym
                 (do SWord sym
a <- forall sym.
Backend sym =>
sym -> WordValue sym -> SEval sym (SWord sym)
asWordVal sym
sym WordValue sym
w1
                     SWord sym
b <- forall sym.
Backend sym =>
sym -> WordValue sym -> SEval sym (SWord sym)
asWordVal sym
sym WordValue sym
w2
                     forall sym.
Backend sym =>
sym -> SWord sym -> SWord sym -> SEval sym (SWord sym)
joinWord sym
sym SWord sym
a SWord sym
b)
     let bs :: SeqMap sym (SBit sym)
bs = forall sym a.
Backend sym =>
Integer -> SeqMap sym a -> SeqMap sym a -> SeqMap sym a
concatSeqMap Integer
n1 (forall sym.
Backend sym =>
sym -> WordValue sym -> SeqMap sym (SBit sym)
asBitsMap sym
sym WordValue sym
w1) (forall sym.
Backend sym =>
sym -> WordValue sym -> SeqMap sym (SBit sym)
asBitsMap sym
sym WordValue sym
w2)
     forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall sym.
Integer
-> SEval sym (SWord sym) -> SeqMap sym (SBit sym) -> WordValue sym
BitmapVal Integer
len SEval sym (SWord sym)
packed SeqMap sym (SBit sym)
bs)


{-# INLINE takeWordVal #-}
takeWordVal ::
  Backend sym =>
  sym ->
  Integer ->
  Integer ->
  WordValue sym ->
  SEval sym (WordValue sym)
takeWordVal :: forall sym.
Backend sym =>
sym
-> Integer -> Integer -> WordValue sym -> SEval sym (WordValue sym)
takeWordVal sym
sym Integer
leftWidth Integer
rigthWidth (WordVal SWord sym
w) =
  do (SWord sym
lw, SWord sym
_rw) <- forall sym.
Backend sym =>
sym
-> Integer
-> Integer
-> SWord sym
-> SEval sym (SWord sym, SWord sym)
splitWord sym
sym Integer
leftWidth Integer
rigthWidth SWord sym
w
     forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall sym. SWord sym -> WordValue sym
WordVal SWord sym
lw)

takeWordVal sym
sym Integer
leftWidth Integer
rightWidth (ThunkWordVal Integer
_ SEval sym (WordValue sym)
m) =
  forall sym a.
Backend sym =>
sym -> SEval sym a -> SEval sym (Maybe a)
isReady sym
sym SEval sym (WordValue sym)
m forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
    Just WordValue sym
w -> forall sym.
Backend sym =>
sym
-> Integer -> Integer -> WordValue sym -> SEval sym (WordValue sym)
takeWordVal sym
sym Integer
leftWidth Integer
rightWidth WordValue sym
w
    Maybe (WordValue sym)
Nothing ->
      do SEval sym (WordValue sym)
m' <- forall sym a.
Backend sym =>
sym -> SEval sym a -> SEval sym (SEval sym a)
sDelay sym
sym (forall sym.
Backend sym =>
sym
-> Integer -> Integer -> WordValue sym -> SEval sym (WordValue sym)
takeWordVal sym
sym Integer
leftWidth Integer
rightWidth forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< SEval sym (WordValue sym)
m)
         forall (m :: * -> *) a. Monad m => a -> m a
return (forall sym. Integer -> SEval sym (WordValue sym) -> WordValue sym
ThunkWordVal Integer
leftWidth SEval sym (WordValue sym)
m')

takeWordVal sym
sym Integer
leftWidth Integer
rightWidth (BitmapVal Integer
_n SEval sym (SWord sym)
packed SeqMap sym (SBit sym)
xs) =
  forall sym a.
Backend sym =>
sym -> SEval sym a -> SEval sym (Maybe a)
isReady sym
sym SEval sym (SWord sym)
packed forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
    Just SWord sym
w -> do (SWord sym
lw, SWord sym
_rw) <- forall sym.
Backend sym =>
sym
-> Integer
-> Integer
-> SWord sym
-> SEval sym (SWord sym, SWord sym)
splitWord sym
sym Integer
leftWidth Integer
rightWidth SWord sym
w
                 forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall sym. SWord sym -> WordValue sym
WordVal SWord sym
lw)
    Maybe (SWord sym)
Nothing -> forall sym.
Backend sym =>
sym
-> Integer -> SeqMap sym (SBit sym) -> SEval sym (WordValue sym)
bitmapWordVal sym
sym Integer
leftWidth SeqMap sym (SBit sym)
xs

{-# INLINE dropWordVal #-}
dropWordVal ::
  Backend sym =>
  sym ->
  Integer ->
  Integer ->
  WordValue sym ->
  SEval sym (WordValue sym)
dropWordVal :: forall sym.
Backend sym =>
sym
-> Integer -> Integer -> WordValue sym -> SEval sym (WordValue sym)
dropWordVal sym
sym Integer
leftWidth Integer
rigthWidth (WordVal SWord sym
w) =
  do (SWord sym
_lw, SWord sym
rw) <- forall sym.
Backend sym =>
sym
-> Integer
-> Integer
-> SWord sym
-> SEval sym (SWord sym, SWord sym)
splitWord sym
sym Integer
leftWidth Integer
rigthWidth SWord sym
w
     forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall sym. SWord sym -> WordValue sym
WordVal SWord sym
rw)

dropWordVal sym
sym Integer
leftWidth Integer
rightWidth (ThunkWordVal Integer
_ SEval sym (WordValue sym)
m) =
  forall sym a.
Backend sym =>
sym -> SEval sym a -> SEval sym (Maybe a)
isReady sym
sym SEval sym (WordValue sym)
m forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
    Just WordValue sym
w -> forall sym.
Backend sym =>
sym
-> Integer -> Integer -> WordValue sym -> SEval sym (WordValue sym)
dropWordVal sym
sym Integer
leftWidth Integer
rightWidth WordValue sym
w
    Maybe (WordValue sym)
Nothing ->
      do SEval sym (WordValue sym)
m' <- forall sym a.
Backend sym =>
sym -> SEval sym a -> SEval sym (SEval sym a)
sDelay sym
sym (forall sym.
Backend sym =>
sym
-> Integer -> Integer -> WordValue sym -> SEval sym (WordValue sym)
dropWordVal sym
sym Integer
leftWidth Integer
rightWidth forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< SEval sym (WordValue sym)
m)
         forall (m :: * -> *) a. Monad m => a -> m a
return (forall sym. Integer -> SEval sym (WordValue sym) -> WordValue sym
ThunkWordVal Integer
rightWidth SEval sym (WordValue sym)
m')

dropWordVal sym
sym Integer
leftWidth Integer
rightWidth (BitmapVal Integer
_n SEval sym (SWord sym)
packed SeqMap sym (SBit sym)
xs) =
  forall sym a.
Backend sym =>
sym -> SEval sym a -> SEval sym (Maybe a)
isReady sym
sym SEval sym (SWord sym)
packed forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
    Just SWord sym
w -> do (SWord sym
_lw, SWord sym
rw) <- forall sym.
Backend sym =>
sym
-> Integer
-> Integer
-> SWord sym
-> SEval sym (SWord sym, SWord sym)
splitWord sym
sym Integer
leftWidth Integer
rightWidth SWord sym
w
                 forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall sym. SWord sym -> WordValue sym
WordVal SWord sym
rw)
    Maybe (SWord sym)
Nothing ->
      do let rxs :: SeqMap sym (SBit sym)
rxs = forall sym a.
Backend sym =>
Integer -> SeqMap sym a -> SeqMap sym a
dropSeqMap Integer
leftWidth SeqMap sym (SBit sym)
xs
         forall sym.
Backend sym =>
sym
-> Integer -> SeqMap sym (SBit sym) -> SEval sym (WordValue sym)
bitmapWordVal sym
sym Integer
rightWidth SeqMap sym (SBit sym)
rxs

{-# INLINE extractWordVal #-}

-- | Extract a subsequence of bits from a @WordValue@.
--   The first integer argument is the number of bits in the
--   resulting word.  The second integer argument is the
--   number of less-significant digits to discard.  Stated another
--   way, the operation `extractWordVal n i w` is equivalent to
--   first shifting `w` right by `i` bits, and then truncating to
--   `n` bits.
extractWordVal ::
  Backend sym =>
  sym ->
  Integer ->
  Integer ->
  WordValue sym ->
  SEval sym (WordValue sym)
extractWordVal :: forall sym.
Backend sym =>
sym
-> Integer -> Integer -> WordValue sym -> SEval sym (WordValue sym)
extractWordVal sym
sym Integer
len Integer
start (WordVal SWord sym
w) =
   forall sym. SWord sym -> WordValue sym
WordVal forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym.
Backend sym =>
sym -> Integer -> Integer -> SWord sym -> SEval sym (SWord sym)
extractWord sym
sym Integer
len Integer
start SWord sym
w
extractWordVal sym
sym Integer
len Integer
start (ThunkWordVal Integer
_n SEval sym (WordValue sym)
m) =
  forall sym a.
Backend sym =>
sym -> SEval sym a -> SEval sym (Maybe a)
isReady sym
sym SEval sym (WordValue sym)
m forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
    Just WordValue sym
w -> forall sym.
Backend sym =>
sym
-> Integer -> Integer -> WordValue sym -> SEval sym (WordValue sym)
extractWordVal sym
sym Integer
len Integer
start WordValue sym
w
    Maybe (WordValue sym)
Nothing ->
      do SEval sym (WordValue sym)
m' <- forall sym a.
Backend sym =>
sym -> SEval sym a -> SEval sym (SEval sym a)
sDelay sym
sym (forall sym.
Backend sym =>
sym
-> Integer -> Integer -> WordValue sym -> SEval sym (WordValue sym)
extractWordVal sym
sym Integer
len Integer
start forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< SEval sym (WordValue sym)
m)
         forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall sym. Integer -> SEval sym (WordValue sym) -> WordValue sym
ThunkWordVal Integer
len SEval sym (WordValue sym)
m')
extractWordVal sym
sym Integer
len Integer
start (BitmapVal Integer
n SEval sym (SWord sym)
packed SeqMap sym (SBit sym)
xs) =
  forall sym a.
Backend sym =>
sym -> SEval sym a -> SEval sym (Maybe a)
isReady sym
sym SEval sym (SWord sym)
packed forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
    Just SWord sym
w -> forall sym. SWord sym -> WordValue sym
WordVal forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym.
Backend sym =>
sym -> Integer -> Integer -> SWord sym -> SEval sym (SWord sym)
extractWord sym
sym Integer
len Integer
start SWord sym
w
    Maybe (SWord sym)
Nothing ->
      do let xs' :: SeqMap sym (SBit sym)
xs' = forall sym a.
Backend sym =>
Integer -> SeqMap sym a -> SeqMap sym a
dropSeqMap (Integer
n forall a. Num a => a -> a -> a
- Integer
start forall a. Num a => a -> a -> a
- Integer
len) SeqMap sym (SBit sym)
xs
         forall sym.
Backend sym =>
sym
-> Integer -> SeqMap sym (SBit sym) -> SEval sym (WordValue sym)
bitmapWordVal sym
sym Integer
len SeqMap sym (SBit sym)
xs'

{-# INLINE wordValLogicOp #-}

wordValLogicOp ::
  Backend sym =>
  sym ->
  (SBit sym -> SBit sym -> SEval sym (SBit sym)) ->
  (SWord sym -> SWord sym -> SEval sym (SWord sym)) ->
  WordValue sym ->
  WordValue sym ->
  SEval sym (WordValue sym)
wordValLogicOp :: forall sym.
Backend sym =>
sym
-> (SBit sym -> SBit sym -> SEval sym (SBit sym))
-> (SWord sym -> SWord sym -> SEval sym (SWord sym))
-> WordValue sym
-> WordValue sym
-> SEval sym (WordValue sym)
wordValLogicOp sym
_sym SBit sym -> SBit sym -> SEval sym (SBit sym)
_ SWord sym -> SWord sym -> SEval sym (SWord sym)
wop (WordVal SWord sym
w1) (WordVal SWord sym
w2) = forall sym. SWord sym -> WordValue sym
WordVal forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SWord sym -> SWord sym -> SEval sym (SWord sym)
wop SWord sym
w1 SWord sym
w2

wordValLogicOp sym
sym SBit sym -> SBit sym -> SEval sym (SBit sym)
bop SWord sym -> SWord sym -> SEval sym (SWord sym)
wop (WordVal SWord sym
w1) (BitmapVal Integer
n2 SEval sym (SWord sym)
packed2 SeqMap sym (SBit sym)
bs2) =
  forall sym a.
Backend sym =>
sym -> SEval sym a -> SEval sym (Maybe a)
isReady sym
sym SEval sym (SWord sym)
packed2 forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
    Just SWord sym
w2 -> forall sym. SWord sym -> WordValue sym
WordVal forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SWord sym -> SWord sym -> SEval sym (SWord sym)
wop SWord sym
w1 SWord sym
w2
    Maybe (SWord sym)
Nothing -> forall sym.
Backend sym =>
sym
-> Integer -> SeqMap sym (SBit sym) -> SEval sym (WordValue sym)
bitmapWordVal sym
sym Integer
n2 forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< 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 SBit sym -> SBit sym -> SEval sym (SBit sym)
bop (Integer -> Nat'
Nat Integer
n2) (forall sym.
Backend sym =>
sym -> SWord sym -> SeqMap sym (SBit sym)
unpackBitmap sym
sym SWord sym
w1) SeqMap sym (SBit sym)
bs2

wordValLogicOp sym
sym SBit sym -> SBit sym -> SEval sym (SBit sym)
bop SWord sym -> SWord sym -> SEval sym (SWord sym)
wop (BitmapVal Integer
n1 SEval sym (SWord sym)
packed1 SeqMap sym (SBit sym)
bs1) (WordVal SWord sym
w2) =
  forall sym a.
Backend sym =>
sym -> SEval sym a -> SEval sym (Maybe a)
isReady sym
sym SEval sym (SWord sym)
packed1 forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
    Just SWord sym
w1 -> forall sym. SWord sym -> WordValue sym
WordVal forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SWord sym -> SWord sym -> SEval sym (SWord sym)
wop SWord sym
w1 SWord sym
w2
    Maybe (SWord sym)
Nothing -> forall sym.
Backend sym =>
sym
-> Integer -> SeqMap sym (SBit sym) -> SEval sym (WordValue sym)
bitmapWordVal sym
sym Integer
n1 forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< 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 SBit sym -> SBit sym -> SEval sym (SBit sym)
bop (Integer -> Nat'
Nat Integer
n1) SeqMap sym (SBit sym)
bs1 (forall sym.
Backend sym =>
sym -> SWord sym -> SeqMap sym (SBit sym)
unpackBitmap sym
sym SWord sym
w2)

wordValLogicOp sym
sym SBit sym -> SBit sym -> SEval sym (SBit sym)
bop SWord sym -> SWord sym -> SEval sym (SWord sym)
wop (BitmapVal Integer
n1 SEval sym (SWord sym)
packed1 SeqMap sym (SBit sym)
bs1) (BitmapVal Integer
_n2 SEval sym (SWord sym)
packed2 SeqMap sym (SBit sym)
bs2) =
  do Maybe (SWord sym)
r1 <- forall sym a.
Backend sym =>
sym -> SEval sym a -> SEval sym (Maybe a)
isReady sym
sym SEval sym (SWord sym)
packed1
     Maybe (SWord sym)
r2 <- forall sym a.
Backend sym =>
sym -> SEval sym a -> SEval sym (Maybe a)
isReady sym
sym SEval sym (SWord sym)
packed2
     case (Maybe (SWord sym)
r1,Maybe (SWord sym)
r2) of
       (Just SWord sym
w1, Just SWord sym
w2) -> forall sym. SWord sym -> WordValue sym
WordVal forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SWord sym -> SWord sym -> SEval sym (SWord sym)
wop SWord sym
w1 SWord sym
w2
       (Maybe (SWord sym), Maybe (SWord sym))
_ -> forall sym.
Backend sym =>
sym
-> Integer -> SeqMap sym (SBit sym) -> SEval sym (WordValue sym)
bitmapWordVal sym
sym Integer
n1 forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< 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 SBit sym -> SBit sym -> SEval sym (SBit sym)
bop (Integer -> Nat'
Nat Integer
n1) SeqMap sym (SBit sym)
bs1 SeqMap sym (SBit sym)
bs2

wordValLogicOp sym
sym SBit sym -> SBit sym -> SEval sym (SBit sym)
bop SWord sym -> SWord sym -> SEval sym (SWord sym)
wop (ThunkWordVal Integer
_ SEval sym (WordValue sym)
m1) WordValue sym
w2 =
  do WordValue sym
w1 <- SEval sym (WordValue sym)
m1
     forall sym.
Backend sym =>
sym
-> (SBit sym -> SBit sym -> SEval sym (SBit sym))
-> (SWord sym -> SWord sym -> SEval sym (SWord sym))
-> WordValue sym
-> WordValue sym
-> SEval sym (WordValue sym)
wordValLogicOp sym
sym SBit sym -> SBit sym -> SEval sym (SBit sym)
bop SWord sym -> SWord sym -> SEval sym (SWord sym)
wop WordValue sym
w1 WordValue sym
w2

wordValLogicOp sym
sym SBit sym -> SBit sym -> SEval sym (SBit sym)
bop SWord sym -> SWord sym -> SEval sym (SWord sym)
wop WordValue sym
w1 (ThunkWordVal Integer
_ SEval sym (WordValue sym)
m2) =
  do WordValue sym
w2 <- SEval sym (WordValue sym)
m2
     forall sym.
Backend sym =>
sym
-> (SBit sym -> SBit sym -> SEval sym (SBit sym))
-> (SWord sym -> SWord sym -> SEval sym (SWord sym))
-> WordValue sym
-> WordValue sym
-> SEval sym (WordValue sym)
wordValLogicOp sym
sym SBit sym -> SBit sym -> SEval sym (SBit sym)
bop SWord sym -> SWord sym -> SEval sym (SWord sym)
wop WordValue sym
w1 WordValue sym
w2

{-# INLINE wordValUnaryOp #-}
wordValUnaryOp ::
  Backend sym =>
  sym ->
  (SBit sym -> SEval sym (SBit sym)) ->
  (SWord sym -> SEval sym (SWord sym)) ->
  WordValue sym ->
  SEval sym (WordValue sym)
wordValUnaryOp :: forall sym.
Backend sym =>
sym
-> (SBit sym -> SEval sym (SBit sym))
-> (SWord sym -> SEval sym (SWord sym))
-> WordValue sym
-> SEval sym (WordValue sym)
wordValUnaryOp sym
_ SBit sym -> SEval sym (SBit sym)
_ SWord sym -> SEval sym (SWord sym)
wop (WordVal SWord sym
w)  = forall sym. SWord sym -> WordValue sym
WordVal forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SWord sym -> SEval sym (SWord sym)
wop SWord sym
w
wordValUnaryOp sym
sym SBit sym -> SEval sym (SBit sym)
bop SWord sym -> SEval sym (SWord sym)
wop (ThunkWordVal Integer
_ SEval sym (WordValue sym)
m) = forall sym.
Backend sym =>
sym
-> (SBit sym -> SEval sym (SBit sym))
-> (SWord sym -> SEval sym (SWord sym))
-> WordValue sym
-> SEval sym (WordValue sym)
wordValUnaryOp sym
sym SBit sym -> SEval sym (SBit sym)
bop SWord sym -> SEval sym (SWord sym)
wop forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< SEval sym (WordValue sym)
m
wordValUnaryOp sym
sym SBit sym -> SEval sym (SBit sym)
bop SWord sym -> SEval sym (SWord sym)
wop (BitmapVal Integer
n SEval sym (SWord sym)
packed SeqMap sym (SBit sym)
xs) =
  forall sym a.
Backend sym =>
sym -> SEval sym a -> SEval sym (Maybe a)
isReady sym
sym SEval sym (SWord sym)
packed forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
    Just SWord sym
w  -> forall sym. SWord sym -> WordValue sym
WordVal forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SWord sym -> SEval sym (SWord sym)
wop SWord sym
w
    Maybe (SWord sym)
Nothing -> forall sym.
Backend sym =>
sym
-> Integer -> SeqMap sym (SBit sym) -> SEval sym (WordValue sym)
bitmapWordVal sym
sym Integer
n forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall sym a.
Backend sym =>
sym
-> (a -> SEval sym a)
-> Nat'
-> SeqMap sym a
-> SEval sym (SeqMap sym a)
mapSeqMap sym
sym SBit sym -> SEval sym (SBit sym)
bop (Integer -> Nat'
Nat Integer
n) SeqMap sym (SBit sym)
xs

{-# SPECIALIZE joinWords ::
  Concrete ->
  Integer ->
  Integer ->
  SeqMap Concrete (WordValue Concrete)->
  SEval Concrete (WordValue Concrete)
  #-}
joinWords :: forall sym.
  Backend sym =>
  sym ->
  Integer ->
  Integer ->
  SeqMap sym (WordValue sym) ->
  SEval sym (WordValue sym)

-- small enough to pack
joinWords :: forall sym.
Backend sym =>
sym
-> Integer
-> Integer
-> SeqMap sym (WordValue sym)
-> SEval sym (WordValue sym)
joinWords sym
sym Integer
nParts Integer
nEach SeqMap sym (WordValue sym)
xs | Integer
nParts forall a. Num a => a -> a -> a
* Integer
nEach forall a. Ord a => a -> a -> Bool
< Integer
largeBitSize =
  do SWord sym
z <- forall sym.
Backend sym =>
sym -> Integer -> Integer -> SEval sym (SWord sym)
wordLit sym
sym Integer
0 Integer
0
     WordValue sym
-> [SEval sym (WordValue sym)] -> SEval sym (WordValue sym)
loop (forall sym. SWord sym -> WordValue sym
wordVal SWord sym
z) (forall sym n a.
(Backend sym, Integral n) =>
n -> SeqMap sym a -> [SEval sym a]
enumerateSeqMap Integer
nParts SeqMap sym (WordValue sym)
xs)

 where
 loop :: WordValue sym -> [SEval sym (WordValue sym)] -> SEval sym (WordValue sym)
 loop :: WordValue sym
-> [SEval sym (WordValue sym)] -> SEval sym (WordValue sym)
loop !WordValue sym
wv [] = forall (f :: * -> *) a. Applicative f => a -> f a
pure WordValue sym
wv
 loop !WordValue sym
wv (SEval sym (WordValue sym)
w : [SEval sym (WordValue sym)]
ws) =
    do WordValue sym
w'  <- forall sym.
Backend sym =>
sym
-> Integer
-> SEval sym (WordValue sym)
-> SEval sym (WordValue sym)
delayWordValue sym
sym Integer
nEach SEval sym (WordValue sym)
w
       WordValue sym
wv' <- forall sym.
Backend sym =>
sym -> WordValue sym -> WordValue sym -> SEval sym (WordValue sym)
joinWordVal sym
sym WordValue sym
wv WordValue sym
w'
       WordValue sym
-> [SEval sym (WordValue sym)] -> SEval sym (WordValue sym)
loop WordValue sym
wv' [SEval sym (WordValue sym)]
ws

-- too large to pack
joinWords sym
sym Integer
nParts Integer
nEach SeqMap sym (WordValue sym)
xs = forall sym.
Backend sym =>
sym
-> Integer -> SeqMap sym (SBit sym) -> SEval sym (WordValue sym)
bitmapWordVal sym
sym (Integer
nParts forall a. Num a => a -> a -> a
* Integer
nEach) SeqMap sym (SBit sym)
zs
  where
    zs :: SeqMap sym (SBit sym)
zs = forall sym a. (Integer -> SEval sym a) -> SeqMap sym a
indexSeqMap forall a b. (a -> b) -> a -> b
$ \Integer
i ->
            do let (Integer
q,Integer
r) = forall a. Integral a => a -> a -> (a, a)
divMod Integer
i Integer
nEach
               WordValue sym
ys <- forall sym a. Backend sym => SeqMap sym a -> Integer -> SEval sym a
lookupSeqMap SeqMap sym (WordValue sym)
xs Integer
q
               forall sym.
Backend sym =>
sym -> WordValue sym -> Integer -> SEval sym (SBit sym)
indexWordValue sym
sym WordValue sym
ys Integer
r

reverseWordVal :: Backend sym => sym -> WordValue sym -> SEval sym (WordValue sym)
reverseWordVal :: forall sym.
Backend sym =>
sym -> WordValue sym -> SEval sym (WordValue sym)
reverseWordVal sym
sym WordValue sym
w =
  let m :: Integer
m = forall sym. Backend sym => sym -> WordValue sym -> Integer
wordValueSize sym
sym WordValue sym
w in
  forall sym.
Backend sym =>
sym
-> Integer -> SeqMap sym (SBit sym) -> SEval sym (WordValue sym)
bitmapWordVal sym
sym Integer
m forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym a.
Backend sym =>
Integer -> SeqMap sym a -> SeqMap sym a
reverseSeqMap Integer
m forall a b. (a -> b) -> a -> b
$ forall sym.
Backend sym =>
sym -> WordValue sym -> SeqMap sym (SBit sym)
asBitsMap sym
sym WordValue sym
w

wordValAsLit :: Backend sym => sym -> WordValue sym -> SEval sym (Maybe Integer)
wordValAsLit :: forall sym.
Backend sym =>
sym -> WordValue sym -> SEval sym (Maybe Integer)
wordValAsLit sym
sym (WordVal SWord sym
w) = forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall a b. (a, b) -> b
snd forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym.
Backend sym =>
sym -> SWord sym -> Maybe (Integer, Integer)
wordAsLit sym
sym SWord sym
w)
wordValAsLit sym
sym (ThunkWordVal Integer
_ SEval sym (WordValue sym)
m) =
  forall sym a.
Backend sym =>
sym -> SEval sym a -> SEval sym (Maybe a)
isReady sym
sym SEval sym (WordValue sym)
m forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
    Just WordValue sym
v  -> forall sym.
Backend sym =>
sym -> WordValue sym -> SEval sym (Maybe Integer)
wordValAsLit sym
sym WordValue sym
v
    Maybe (WordValue sym)
Nothing -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a. Maybe a
Nothing
wordValAsLit sym
sym (BitmapVal Integer
_ SEval sym (SWord sym)
packed SeqMap sym (SBit sym)
_) =
  forall sym a.
Backend sym =>
sym -> SEval sym a -> SEval sym (Maybe a)
isReady sym
sym SEval sym (SWord sym)
packed forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
    Just SWord sym
w  -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall a b. (a, b) -> b
snd forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym.
Backend sym =>
sym -> SWord sym -> Maybe (Integer, Integer)
wordAsLit sym
sym SWord sym
w)
    Maybe (SWord sym)
Nothing -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a. Maybe a
Nothing

-- | Force a word value into packed word form
asWordVal :: Backend sym => sym -> WordValue sym -> SEval sym (SWord sym)
asWordVal :: forall sym.
Backend sym =>
sym -> WordValue sym -> SEval sym (SWord sym)
asWordVal sym
_   (WordVal SWord sym
w)            = forall (m :: * -> *) a. Monad m => a -> m a
return SWord sym
w
asWordVal sym
sym (ThunkWordVal Integer
_ SEval sym (WordValue sym)
m)     = forall sym.
Backend sym =>
sym -> WordValue sym -> SEval sym (SWord sym)
asWordVal sym
sym forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< SEval sym (WordValue sym)
m
asWordVal sym
_   (BitmapVal Integer
_ SEval sym (SWord sym)
packed SeqMap sym (SBit sym)
_) = SEval sym (SWord sym)
packed

wordValueEqualsInteger :: forall sym. Backend sym =>
  sym ->
  WordValue sym ->
  Integer ->
  SEval sym (SBit sym)
wordValueEqualsInteger :: forall sym.
Backend sym =>
sym -> WordValue sym -> Integer -> SEval sym (SBit sym)
wordValueEqualsInteger sym
sym WordValue sym
wv Integer
i
  | forall sym. Backend sym => sym -> WordValue sym -> Integer
wordValueSize sym
sym WordValue sym
wv forall a. Ord a => a -> a -> Bool
< Integer -> Integer
widthInteger Integer
i = forall (m :: * -> *) a. Monad m => a -> m a
return (forall sym. Backend sym => sym -> Bool -> SBit sym
bitLit sym
sym Bool
False)
  | Bool
otherwise = WordValue sym -> SEval sym (SBit sym)
loop WordValue sym
wv

 where
   loop :: WordValue sym -> SEval sym (SBit sym)
loop (ThunkWordVal Integer
_ SEval sym (WordValue sym)
m) = WordValue sym -> SEval sym (SBit sym)
loop forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< SEval sym (WordValue sym)
m
   loop (WordVal SWord sym
w) = forall sym.
Backend sym =>
sym -> SWord sym -> SWord sym -> SEval sym (SBit sym)
wordEq sym
sym SWord sym
w forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall sym.
Backend sym =>
sym -> Integer -> Integer -> SEval sym (SWord sym)
wordLit sym
sym (forall sym. Backend sym => sym -> SWord sym -> Integer
wordLen sym
sym SWord sym
w) Integer
i
   loop (BitmapVal Integer
n SEval sym (SWord sym)
packed SeqMap sym (SBit sym)
bs) =
     forall sym a.
Backend sym =>
sym -> SEval sym a -> SEval sym (Maybe a)
isReady sym
sym SEval sym (SWord sym)
packed forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
       Just SWord sym
w  -> WordValue sym -> SEval sym (SBit sym)
loop (forall sym. SWord sym -> WordValue sym
WordVal SWord sym
w)
       Maybe (SWord sym)
Nothing -> Integer -> [SBit sym] -> SEval sym (SBit sym)
bitsAre Integer
i forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence (forall sym n a.
(Backend sym, Integral n) =>
n -> SeqMap sym a -> [SEval sym a]
enumerateSeqMap Integer
n (forall sym a.
Backend sym =>
Integer -> SeqMap sym a -> SeqMap sym a
reverseSeqMap Integer
n SeqMap sym (SBit sym)
bs))

   -- NB little-endian sequence of bits
   bitsAre :: Integer -> [SBit sym] -> SEval sym (SBit sym)
   bitsAre :: Integer -> [SBit sym] -> SEval sym (SBit sym)
bitsAre !Integer
n [] = forall (m :: * -> *) a. Monad m => a -> m a
return (forall sym. Backend sym => sym -> Bool -> SBit sym
bitLit sym
sym (Integer
n forall a. Eq a => a -> a -> Bool
== Integer
0))
   bitsAre !Integer
n (SBit sym
b:[SBit sym]
bs) =
     do SBit sym
pb  <- Bool -> SBit sym -> SEval sym (SBit sym)
bitIs (forall a. Bits a => a -> Int -> Bool
testBit Integer
n Int
0) SBit sym
b
        SBit sym
pbs <- Integer -> [SBit sym] -> SEval sym (SBit sym)
bitsAre (Integer
n forall a. Bits a => a -> Int -> a
`shiftR` Int
1) [SBit sym]
bs
        forall sym.
Backend sym =>
sym -> SBit sym -> SBit sym -> SEval sym (SBit sym)
bitAnd sym
sym SBit sym
pb SBit sym
pbs

   bitIs :: Bool -> SBit sym -> SEval sym (SBit sym)
   bitIs :: Bool -> SBit sym -> SEval sym (SBit sym)
bitIs Bool
b SBit sym
x = if Bool
b then forall (f :: * -> *) a. Applicative f => a -> f a
pure SBit sym
x else forall sym. Backend sym => sym -> SBit sym -> SEval sym (SBit sym)
bitComplement sym
sym SBit sym
x

asWordList :: forall sym. Backend sym => sym -> [WordValue sym] -> SEval sym (Maybe [SWord sym])
asWordList :: forall sym.
Backend sym =>
sym -> [WordValue sym] -> SEval sym (Maybe [SWord sym])
asWordList sym
sym = ([SWord sym] -> [SWord sym])
-> [WordValue sym] -> SEval sym (Maybe [SWord sym])
loop forall a. a -> a
id
 where
   loop :: ([SWord sym] -> [SWord sym]) -> [WordValue sym] -> SEval sym (Maybe [SWord sym])
   loop :: ([SWord sym] -> [SWord sym])
-> [WordValue sym] -> SEval sym (Maybe [SWord sym])
loop [SWord sym] -> [SWord sym]
f [] = forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall a. a -> Maybe a
Just ([SWord sym] -> [SWord sym]
f []))
   loop [SWord sym] -> [SWord sym]
f (WordVal SWord sym
x : [WordValue sym]
vs) = ([SWord sym] -> [SWord sym])
-> [WordValue sym] -> SEval sym (Maybe [SWord sym])
loop ([SWord sym] -> [SWord sym]
f forall b c a. (b -> c) -> (a -> b) -> a -> c
. (SWord sym
xforall a. a -> [a] -> [a]
:)) [WordValue sym]
vs
   loop [SWord sym] -> [SWord sym]
f (ThunkWordVal Integer
_ SEval sym (WordValue sym)
m : [WordValue sym]
vs) =
     forall sym a.
Backend sym =>
sym -> SEval sym a -> SEval sym (Maybe a)
isReady sym
sym SEval sym (WordValue sym)
m forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
       Just WordValue sym
m' -> ([SWord sym] -> [SWord sym])
-> [WordValue sym] -> SEval sym (Maybe [SWord sym])
loop [SWord sym] -> [SWord sym]
f (WordValue sym
m' forall a. a -> [a] -> [a]
: [WordValue sym]
vs)
       Maybe (WordValue sym)
Nothing -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a. Maybe a
Nothing
   loop [SWord sym] -> [SWord sym]
f (BitmapVal Integer
_ SEval sym (SWord sym)
packed SeqMap sym (SBit sym)
_ : [WordValue sym]
vs) =
     forall sym a.
Backend sym =>
sym -> SEval sym a -> SEval sym (Maybe a)
isReady sym
sym SEval sym (SWord sym)
packed forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
       Just SWord sym
x -> ([SWord sym] -> [SWord sym])
-> [WordValue sym] -> SEval sym (Maybe [SWord sym])
loop ([SWord sym] -> [SWord sym]
f forall b c a. (b -> c) -> (a -> b) -> a -> c
. (SWord sym
xforall a. a -> [a] -> [a]
:)) [WordValue sym]
vs
       Maybe (SWord sym)
Nothing -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a. Maybe a
Nothing

-- | Force a word value into a sequence of bits
asBitsMap :: Backend sym => sym -> WordValue sym -> SeqMap sym (SBit sym)
asBitsMap :: forall sym.
Backend sym =>
sym -> WordValue sym -> SeqMap sym (SBit sym)
asBitsMap sym
_   (BitmapVal Integer
_ SEval sym (SWord sym)
_ SeqMap sym (SBit sym)
xs)  = SeqMap sym (SBit sym)
xs
asBitsMap sym
sym (WordVal SWord sym
w)         = forall sym a. (Integer -> SEval sym a) -> SeqMap sym a
indexSeqMap forall a b. (a -> b) -> a -> b
$ \Integer
i -> forall sym.
Backend sym =>
sym -> SWord sym -> Integer -> SEval sym (SBit sym)
wordBit sym
sym SWord sym
w Integer
i
asBitsMap sym
sym (ThunkWordVal Integer
_ SEval sym (WordValue sym)
m)  =
  forall sym a. (Integer -> SEval sym a) -> SeqMap sym a
indexSeqMap forall a b. (a -> b) -> a -> b
$ \Integer
i ->
    do SeqMap sym (SBit sym)
mp <- forall sym.
Backend sym =>
sym -> WordValue sym -> SeqMap sym (SBit sym)
asBitsMap sym
sym forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall sym.
Backend sym =>
SEval sym (WordValue sym) -> SEval sym (WordValue sym)
unwindThunks SEval sym (WordValue sym)
m)
       forall sym a. Backend sym => SeqMap sym a -> Integer -> SEval sym a
lookupSeqMap SeqMap sym (SBit sym)
mp Integer
i

-- | Turn a word value into a sequence of bits, forcing each bit.
--   The sequence is returned in big-endian order.
enumerateWordValue :: Backend sym => sym -> WordValue sym -> SEval sym [SBit sym]
enumerateWordValue :: forall sym.
Backend sym =>
sym -> WordValue sym -> SEval sym [SBit sym]
enumerateWordValue sym
sym (WordVal SWord sym
w) = forall sym. Backend sym => sym -> SWord sym -> SEval sym [SBit sym]
unpackWord sym
sym SWord sym
w
enumerateWordValue sym
sym (ThunkWordVal Integer
_ SEval sym (WordValue sym)
m) = forall sym.
Backend sym =>
sym -> WordValue sym -> SEval sym [SBit sym]
enumerateWordValue sym
sym forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< SEval sym (WordValue sym)
m
  -- TODO? used the packed value if it is ready?
enumerateWordValue sym
_ (BitmapVal Integer
n SEval sym (SWord sym)
_ SeqMap sym (SBit sym)
xs) = forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence (forall sym n a.
(Backend sym, Integral n) =>
n -> SeqMap sym a -> [SEval sym a]
enumerateSeqMap Integer
n SeqMap sym (SBit sym)
xs)

-- | Turn a word value into a sequence of bits, forcing each bit.
--   The sequence is returned in reverse of the usual order, which is little-endian order.
enumerateWordValueRev :: Backend sym => sym -> WordValue sym -> SEval sym [SBit sym]
enumerateWordValueRev :: forall sym.
Backend sym =>
sym -> WordValue sym -> SEval sym [SBit sym]
enumerateWordValueRev sym
sym (WordVal SWord sym
w)  = forall a. [a] -> [a]
reverse forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym. Backend sym => sym -> SWord sym -> SEval sym [SBit sym]
unpackWord sym
sym SWord sym
w
enumerateWordValueRev sym
sym (ThunkWordVal Integer
_ SEval sym (WordValue sym)
m)  = forall sym.
Backend sym =>
sym -> WordValue sym -> SEval sym [SBit sym]
enumerateWordValueRev sym
sym forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< SEval sym (WordValue sym)
m
  -- TODO? used the packed value if it is ready?
enumerateWordValueRev sym
_   (BitmapVal Integer
n SEval sym (SWord sym)
_ SeqMap sym (SBit sym)
xs) = forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence (forall sym n a.
(Backend sym, Integral n) =>
n -> SeqMap sym a -> [SEval sym a]
enumerateSeqMap Integer
n (forall sym a.
Backend sym =>
Integer -> SeqMap sym a -> SeqMap sym a
reverseSeqMap Integer
n SeqMap sym (SBit sym)
xs))


enumerateIndexSegments :: Backend sym => sym -> WordValue sym -> SEval sym [IndexSegment sym]
enumerateIndexSegments :: forall sym.
Backend sym =>
sym -> WordValue sym -> SEval sym [IndexSegment sym]
enumerateIndexSegments sym
_sym (WordVal SWord sym
w) = forall (f :: * -> *) a. Applicative f => a -> f a
pure [forall sym. SWord sym -> IndexSegment sym
WordIndexSegment SWord sym
w]
enumerateIndexSegments sym
sym (ThunkWordVal Integer
_ SEval sym (WordValue sym)
m) = forall sym.
Backend sym =>
sym -> WordValue sym -> SEval sym [IndexSegment sym]
enumerateIndexSegments sym
sym forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< SEval sym (WordValue sym)
m
enumerateIndexSegments sym
sym (BitmapVal Integer
n SEval sym (SWord sym)
packed SeqMap sym (SBit sym)
xs) =
  forall sym a.
Backend sym =>
sym -> SEval sym a -> SEval sym (Maybe a)
isReady sym
sym SEval sym (SWord sym)
packed forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
    Just SWord sym
w  -> forall (f :: * -> *) a. Applicative f => a -> f a
pure [forall sym. SWord sym -> IndexSegment sym
WordIndexSegment SWord sym
w]
    Maybe (SWord sym)
Nothing -> forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (forall sym. SBit sym -> IndexSegment sym
BitIndexSegment forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>) (forall sym n a.
(Backend sym, Integral n) =>
n -> SeqMap sym a -> [SEval sym a]
enumerateSeqMap Integer
n SeqMap sym (SBit sym)
xs)

{-# SPECIALIZE bitsValueLessThan ::
  Concrete ->
  Integer ->
  [SBit Concrete] ->
  Integer ->
  SEval Concrete (SBit Concrete)
  #-}
bitsValueLessThan ::
  Backend sym =>
  sym ->
  Integer {- ^ bit-width -} ->
  [SBit sym] {- ^ big-endian list of index bits -} ->
  Integer {- ^ Upper bound to test against -} ->
  SEval sym (SBit sym)
bitsValueLessThan :: forall sym.
Backend sym =>
sym -> Integer -> [SBit sym] -> Integer -> SEval sym (SBit sym)
bitsValueLessThan sym
sym Integer
_w [] Integer
_n = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall sym. Backend sym => sym -> Bool -> SBit sym
bitLit sym
sym Bool
False
bitsValueLessThan sym
sym Integer
w (SBit sym
b:[SBit sym]
bs) Integer
n
  | Bool
nbit =
      do SBit sym
notb <- forall sym. Backend sym => sym -> SBit sym -> SEval sym (SBit sym)
bitComplement sym
sym SBit sym
b
         forall sym.
Backend sym =>
sym -> SBit sym -> SBit sym -> SEval sym (SBit sym)
bitOr sym
sym SBit sym
notb forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall sym.
Backend sym =>
sym -> Integer -> [SBit sym] -> Integer -> SEval sym (SBit sym)
bitsValueLessThan sym
sym (Integer
wforall a. Num a => a -> a -> a
-Integer
1) [SBit sym]
bs Integer
n
  | Bool
otherwise =
      do SBit sym
notb <- forall sym. Backend sym => sym -> SBit sym -> SEval sym (SBit sym)
bitComplement sym
sym SBit sym
b
         forall sym.
Backend sym =>
sym -> SBit sym -> SBit sym -> SEval sym (SBit sym)
bitAnd sym
sym SBit sym
notb forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall sym.
Backend sym =>
sym -> Integer -> [SBit sym] -> Integer -> SEval sym (SBit sym)
bitsValueLessThan sym
sym (Integer
wforall a. Num a => a -> a -> a
-Integer
1) [SBit sym]
bs Integer
n
 where
 nbit :: Bool
nbit = forall a. Bits a => a -> Int -> Bool
testBit Integer
n (forall a. Num a => Integer -> a
fromInteger (Integer
wforall a. Num a => a -> a -> a
-Integer
1))


assertWordValueInBounds ::
  Backend sym => sym -> Integer -> WordValue sym -> SEval sym ()

-- Can't index out of bounds for a sequence that is
-- longer than the expressible index values
assertWordValueInBounds :: forall sym.
Backend sym =>
sym -> Integer -> WordValue sym -> SEval sym ()
assertWordValueInBounds sym
sym Integer
n WordValue sym
idx
  | Integer
n forall a. Ord a => a -> a -> Bool
>= Integer
2forall a b. (Num a, Integral b) => a -> b -> a
^(forall sym. Backend sym => sym -> WordValue sym -> Integer
wordValueSize sym
sym WordValue sym
idx)
  = forall (m :: * -> *) a. Monad m => a -> m a
return ()

assertWordValueInBounds sym
sym Integer
n (WordVal SWord sym
idx)
  | Just (Integer
_w,Integer
i) <- forall sym.
Backend sym =>
sym -> SWord sym -> Maybe (Integer, Integer)
wordAsLit sym
sym SWord sym
idx
  = forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Integer
i forall a. Ord a => a -> a -> Bool
< Integer
n) (forall sym a. Backend sym => sym -> EvalError -> SEval sym a
raiseError sym
sym (Maybe Integer -> EvalError
InvalidIndex (forall a. a -> Maybe a
Just Integer
i)))

-- If the index is a packed word, test that it
-- is less than the concrete value of n, which
-- fits into w bits because of the above test.
assertWordValueInBounds sym
sym Integer
n (WordVal SWord sym
idx) =
  do SWord sym
n' <- forall sym.
Backend sym =>
sym -> Integer -> Integer -> SEval sym (SWord sym)
wordLit sym
sym (forall sym. Backend sym => sym -> SWord sym -> Integer
wordLen sym
sym SWord sym
idx) Integer
n
     SBit sym
p <- forall sym.
Backend sym =>
sym -> SWord sym -> SWord sym -> SEval sym (SBit sym)
wordLessThan sym
sym SWord sym
idx SWord sym
n'
     forall sym.
Backend sym =>
sym -> SBit sym -> EvalError -> SEval sym ()
assertSideCondition sym
sym SBit sym
p (Maybe Integer -> EvalError
InvalidIndex forall a. Maybe a
Nothing)

-- Force thunks
assertWordValueInBounds sym
sym Integer
n (ThunkWordVal Integer
_ SEval sym (WordValue sym)
m) =
  forall sym.
Backend sym =>
sym -> Integer -> WordValue sym -> SEval sym ()
assertWordValueInBounds sym
sym Integer
n forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< SEval sym (WordValue sym)
m

-- If the index is an unpacked word, force all the bits
-- and compute the unsigned less-than test directly.
assertWordValueInBounds sym
sym Integer
n (BitmapVal Integer
sz SEval sym (SWord sym)
packed SeqMap sym (SBit sym)
bits) =
  forall sym a.
Backend sym =>
sym -> SEval sym a -> SEval sym (Maybe a)
isReady sym
sym SEval sym (SWord sym)
packed forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
    Just SWord sym
w -> forall sym.
Backend sym =>
sym -> Integer -> WordValue sym -> SEval sym ()
assertWordValueInBounds sym
sym Integer
n (forall sym. SWord sym -> WordValue sym
WordVal SWord sym
w)
    Maybe (SWord sym)
Nothing ->
      do [SBit sym]
bitsList <- forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence (forall sym n a.
(Backend sym, Integral n) =>
n -> SeqMap sym a -> [SEval sym a]
enumerateSeqMap Integer
sz SeqMap sym (SBit sym)
bits)
         SBit sym
p <- forall sym.
Backend sym =>
sym -> Integer -> [SBit sym] -> Integer -> SEval sym (SBit sym)
bitsValueLessThan sym
sym Integer
sz [SBit sym]
bitsList Integer
n
         forall sym.
Backend sym =>
sym -> SBit sym -> EvalError -> SEval sym ()
assertSideCondition sym
sym SBit sym
p (Maybe Integer -> EvalError
InvalidIndex forall a. Maybe a
Nothing)

delayWordValue :: Backend sym => sym -> Integer -> SEval sym (WordValue sym) -> SEval sym (WordValue sym)
delayWordValue :: forall sym.
Backend sym =>
sym
-> Integer
-> SEval sym (WordValue sym)
-> SEval sym (WordValue sym)
delayWordValue sym
sym Integer
sz SEval sym (WordValue sym)
m =
  forall sym a.
Backend sym =>
sym -> SEval sym a -> SEval sym (Maybe a)
isReady sym
sym SEval sym (WordValue sym)
m forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
    Just WordValue sym
w  -> forall (f :: * -> *) a. Applicative f => a -> f a
pure WordValue sym
w
    Maybe (WordValue sym)
Nothing -> forall sym. Integer -> SEval sym (WordValue sym) -> WordValue sym
ThunkWordVal Integer
sz forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym a.
Backend sym =>
sym -> SEval sym a -> SEval sym (SEval sym a)
sDelay sym
sym (forall sym.
Backend sym =>
SEval sym (WordValue sym) -> SEval sym (WordValue sym)
unwindThunks SEval sym (WordValue sym)
m)

-- If we are calling this, we know the spine of the word value has been
-- demanded, so we unwind any chains of `ThunkWordValue` that may have built up.
unwindThunks :: Backend sym => SEval sym (WordValue sym) -> SEval sym (WordValue sym)
unwindThunks :: forall sym.
Backend sym =>
SEval sym (WordValue sym) -> SEval sym (WordValue sym)
unwindThunks SEval sym (WordValue sym)
m =
  SEval sym (WordValue sym)
m forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
    ThunkWordVal Integer
_ SEval sym (WordValue sym)
m' -> forall sym.
Backend sym =>
SEval sym (WordValue sym) -> SEval sym (WordValue sym)
unwindThunks SEval sym (WordValue sym)
m'
    WordValue sym
x -> forall (f :: * -> *) a. Applicative f => a -> f a
pure WordValue sym
x

{-# INLINE shiftWordByInteger #-}
shiftWordByInteger ::
  Backend sym =>
  sym ->
  (SWord sym -> SWord sym -> SEval sym (SWord sym)) 
    {- ^ operation on word values -} ->
  (Integer -> Integer -> Maybe Integer)
    {- ^ reindexing operation -} ->
  WordValue sym {- ^ word value to shift -} ->
  SInteger sym {- ^ shift amount, assumed to be in range [0,len] -} ->
  SEval sym (WordValue sym)

shiftWordByInteger :: forall sym.
Backend sym =>
sym
-> (SWord sym -> SWord sym -> SEval sym (SWord sym))
-> (Integer -> Integer -> Maybe Integer)
-> WordValue sym
-> SInteger sym
-> SEval sym (WordValue sym)
shiftWordByInteger sym
sym SWord sym -> SWord sym -> SEval sym (SWord sym)
wop Integer -> Integer -> Maybe Integer
reindex WordValue sym
x SInteger sym
idx =
  case WordValue sym
x of
    ThunkWordVal Integer
w SEval sym (WordValue sym)
wm ->
      forall sym a.
Backend sym =>
sym -> SEval sym a -> SEval sym (Maybe a)
isReady sym
sym SEval sym (WordValue sym)
wm forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
        Just WordValue sym
x' -> forall sym.
Backend sym =>
sym
-> (SWord sym -> SWord sym -> SEval sym (SWord sym))
-> (Integer -> Integer -> Maybe Integer)
-> WordValue sym
-> SInteger sym
-> SEval sym (WordValue sym)
shiftWordByInteger sym
sym SWord sym -> SWord sym -> SEval sym (SWord sym)
wop Integer -> Integer -> Maybe Integer
reindex WordValue sym
x' SInteger sym
idx
        Maybe (WordValue sym)
Nothing ->
         do SEval sym (WordValue sym)
m' <- forall sym a.
Backend sym =>
sym -> SEval sym a -> SEval sym (SEval sym a)
sDelay sym
sym
                     (do WordValue sym
x' <- SEval sym (WordValue sym)
wm
                         forall sym.
Backend sym =>
sym
-> (SWord sym -> SWord sym -> SEval sym (SWord sym))
-> (Integer -> Integer -> Maybe Integer)
-> WordValue sym
-> SInteger sym
-> SEval sym (WordValue sym)
shiftWordByInteger sym
sym SWord sym -> SWord sym -> SEval sym (SWord sym)
wop Integer -> Integer -> Maybe Integer
reindex WordValue sym
x' SInteger sym
idx)
            forall (m :: * -> *) a. Monad m => a -> m a
return (forall sym. Integer -> SEval sym (WordValue sym) -> WordValue sym
ThunkWordVal Integer
w SEval sym (WordValue sym)
m')

    WordVal SWord sym
x' -> forall sym. SWord sym -> WordValue sym
WordVal forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (SWord sym -> SWord sym -> SEval sym (SWord sym)
wop SWord sym
x' forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall sym.
Backend sym =>
sym -> Integer -> SInteger sym -> SEval sym (SWord sym)
wordFromInt sym
sym (forall sym. Backend sym => sym -> SWord sym -> Integer
wordLen sym
sym SWord sym
x') SInteger sym
idx)

    BitmapVal Integer
n SEval sym (SWord sym)
packed SeqMap sym (SBit sym)
bs0 ->
      forall sym a.
Backend sym =>
sym -> SEval sym a -> SEval sym (Maybe a)
isReady sym
sym SEval sym (SWord sym)
packed forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
        Just SWord sym
w -> forall sym.
Backend sym =>
sym
-> (SWord sym -> SWord sym -> SEval sym (SWord sym))
-> (Integer -> Integer -> Maybe Integer)
-> WordValue sym
-> SInteger sym
-> SEval sym (WordValue sym)
shiftWordByInteger sym
sym SWord sym -> SWord sym -> SEval sym (SWord sym)
wop Integer -> Integer -> Maybe Integer
reindex (forall sym. SWord sym -> WordValue sym
WordVal SWord sym
w) SInteger sym
idx
        Maybe (SWord sym)
Nothing ->
          forall sym.
Backend sym =>
sym
-> Integer -> SeqMap sym (SBit sym) -> SEval sym (WordValue sym)
bitmapWordVal sym
sym Integer
n forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<<
            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 (forall sym.
Backend sym =>
sym -> SBit sym -> SBit sym -> SBit sym -> SEval sym (SBit sym)
iteBit sym
sym) Integer -> Integer -> Maybe Integer
reindex (forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall sym. Backend sym => sym -> Bool -> SBit sym
bitLit sym
sym Bool
False)) (Integer -> Nat'
Nat Integer
n) SeqMap sym (SBit sym)
bs0 SInteger sym
idx


{-# INLINE shiftWordByWord #-}
shiftWordByWord ::
  Backend sym =>
  sym ->
  (SWord sym -> SWord sym -> SEval sym (SWord sym))
    {- ^ operation on word values -} ->
  (Integer -> Integer -> Maybe Integer)
    {- ^ reindexing operation -} ->
  WordValue sym {- ^ value to shift -} ->
  WordValue sym {- ^ amount to shift -} ->
  SEval sym (WordValue sym)
shiftWordByWord :: forall sym.
Backend sym =>
sym
-> (SWord sym -> SWord sym -> SEval sym (SWord sym))
-> (Integer -> Integer -> Maybe Integer)
-> WordValue sym
-> WordValue sym
-> SEval sym (WordValue sym)
shiftWordByWord sym
sym SWord sym -> SWord sym -> SEval sym (SWord sym)
wop Integer -> Integer -> Maybe Integer
reindex WordValue sym
x WordValue sym
idx =
  case WordValue sym
x of
    ThunkWordVal Integer
w SEval sym (WordValue sym)
wm ->
      forall sym a.
Backend sym =>
sym -> SEval sym a -> SEval sym (Maybe a)
isReady sym
sym SEval sym (WordValue sym)
wm forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
        Just WordValue sym
wm' -> forall sym.
Backend sym =>
sym
-> (SWord sym -> SWord sym -> SEval sym (SWord sym))
-> (Integer -> Integer -> Maybe Integer)
-> WordValue sym
-> WordValue sym
-> SEval sym (WordValue sym)
shiftWordByWord sym
sym SWord sym -> SWord sym -> SEval sym (SWord sym)
wop Integer -> Integer -> Maybe Integer
reindex WordValue sym
wm' WordValue sym
idx
        Maybe (WordValue sym)
Nothing ->
         do SEval sym (WordValue sym)
m' <- forall sym a.
Backend sym =>
sym -> SEval sym a -> SEval sym (SEval sym a)
sDelay sym
sym (do WordValue sym
wm' <- SEval sym (WordValue sym)
wm
                                 forall sym.
Backend sym =>
sym
-> (SWord sym -> SWord sym -> SEval sym (SWord sym))
-> (Integer -> Integer -> Maybe Integer)
-> WordValue sym
-> WordValue sym
-> SEval sym (WordValue sym)
shiftWordByWord sym
sym SWord sym -> SWord sym -> SEval sym (SWord sym)
wop Integer -> Integer -> Maybe Integer
reindex WordValue sym
wm' WordValue sym
idx)
            forall (m :: * -> *) a. Monad m => a -> m a
return (forall sym. Integer -> SEval sym (WordValue sym) -> WordValue sym
ThunkWordVal Integer
w SEval sym (WordValue sym)
m')

    WordVal SWord sym
x' -> forall sym. SWord sym -> WordValue sym
WordVal forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (SWord sym -> SWord sym -> SEval sym (SWord sym)
wop SWord sym
x' forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall sym.
Backend sym =>
sym -> WordValue sym -> SEval sym (SWord sym)
asWordVal sym
sym WordValue sym
idx)

    BitmapVal Integer
n SEval sym (SWord sym)
packed SeqMap sym (SBit sym)
bs0 ->
      forall sym a.
Backend sym =>
sym -> SEval sym a -> SEval sym (Maybe a)
isReady sym
sym SEval sym (SWord sym)
packed forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
        Just SWord sym
w -> forall sym.
Backend sym =>
sym
-> (SWord sym -> SWord sym -> SEval sym (SWord sym))
-> (Integer -> Integer -> Maybe Integer)
-> WordValue sym
-> WordValue sym
-> SEval sym (WordValue sym)
shiftWordByWord sym
sym SWord sym -> SWord sym -> SEval sym (SWord sym)
wop Integer -> Integer -> Maybe Integer
reindex (forall sym. SWord sym -> WordValue sym
WordVal SWord sym
w) WordValue sym
idx
        Maybe (SWord sym)
Nothing ->
          forall sym.
Backend sym =>
sym
-> Integer -> SeqMap sym (SBit sym) -> SEval sym (WordValue sym)
bitmapWordVal sym
sym Integer
n forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<<
            forall sym a.
Backend sym =>
sym
-> (SBit sym -> a -> a -> SEval sym a)
-> (Integer -> Integer -> Maybe Integer)
-> SEval sym a
-> Nat'
-> SeqMap sym a
-> WordValue sym
-> SEval sym (SeqMap sym a)
shiftSeqByWord sym
sym (forall sym.
Backend sym =>
sym -> SBit sym -> SBit sym -> SBit sym -> SEval sym (SBit sym)
iteBit sym
sym) Integer -> Integer -> Maybe Integer
reindex (forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall sym. Backend sym => sym -> Bool -> SBit sym
bitLit sym
sym Bool
False)) (Integer -> Nat'
Nat Integer
n) SeqMap sym (SBit sym)
bs0 WordValue sym
idx


{-# INLINE updateWordByWord #-}
updateWordByWord ::
  Backend sym =>
  sym ->
  IndexDirection ->
  WordValue sym {- ^ value to update -} ->
  WordValue sym {- ^ index to update at -} ->
  SEval sym (SBit sym) {- ^ fresh bit -} ->
  SEval sym (WordValue sym)
updateWordByWord :: forall sym.
Backend sym =>
sym
-> IndexDirection
-> WordValue sym
-> WordValue sym
-> SEval sym (SBit sym)
-> SEval sym (WordValue sym)
updateWordByWord sym
sym IndexDirection
dir WordValue sym
w0 WordValue sym
idx SEval sym (SBit sym)
bitval =
  forall sym.
Backend sym =>
sym -> WordValue sym -> SEval sym (Maybe Integer)
wordValAsLit sym
sym WordValue sym
idx forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
    Just Integer
j ->
      let sz :: Integer
sz = forall sym. Backend sym => sym -> WordValue sym -> Integer
wordValueSize sym
sym WordValue sym
w0 in
      case IndexDirection
dir of
        IndexDirection
IndexForward  -> forall sym.
Backend sym =>
sym
-> WordValue sym
-> Integer
-> SEval sym (SBit sym)
-> SEval sym (WordValue sym)
updateWordValue sym
sym WordValue sym
w0 Integer
j SEval sym (SBit sym)
bitval
        IndexDirection
IndexBackward -> forall sym.
Backend sym =>
sym
-> WordValue sym
-> Integer
-> SEval sym (SBit sym)
-> SEval sym (WordValue sym)
updateWordValue sym
sym WordValue sym
w0 (Integer
sz forall a. Num a => a -> a -> a
- Integer
j forall a. Num a => a -> a -> a
- Integer
1) SEval sym (SBit sym)
bitval
    Maybe Integer
Nothing -> WordValue sym -> SEval sym (WordValue sym)
loop WordValue sym
w0

 where
   loop :: WordValue sym -> SEval sym (WordValue sym)
loop (ThunkWordVal Integer
sz SEval sym (WordValue sym)
m) =
     forall sym a.
Backend sym =>
sym -> SEval sym a -> SEval sym (Maybe a)
isReady sym
sym SEval sym (WordValue sym)
m forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
       Just WordValue sym
w' -> WordValue sym -> SEval sym (WordValue sym)
loop WordValue sym
w'
       Maybe (WordValue sym)
Nothing -> forall sym.
Backend sym =>
sym
-> Integer
-> SEval sym (WordValue sym)
-> SEval sym (WordValue sym)
delayWordValue sym
sym Integer
sz (WordValue sym -> SEval sym (WordValue sym)
loop forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< SEval sym (WordValue sym)
m)

   loop (BitmapVal Integer
sz SEval sym (SWord sym)
packed SeqMap sym (SBit sym)
bs) =
     forall sym a.
Backend sym =>
sym -> SEval sym a -> SEval sym (Maybe a)
isReady sym
sym SEval sym (SWord sym)
packed forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
       Just SWord sym
w -> WordValue sym -> SEval sym (WordValue sym)
loop (forall sym. SWord sym -> WordValue sym
WordVal SWord sym
w)
       Maybe (SWord sym)
Nothing ->
         case IndexDirection
dir of
           IndexDirection
IndexForward ->
             forall sym.
Backend sym =>
sym
-> Integer -> SeqMap sym (SBit sym) -> SEval sym (WordValue sym)
bitmapWordVal sym
sym Integer
sz 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 SBit sym
b <- forall sym.
Backend sym =>
sym -> WordValue sym -> Integer -> SEval sym (SBit sym)
wordValueEqualsInteger sym
sym WordValue sym
idx 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 (forall sym.
Backend sym =>
sym -> SBit sym -> SBit sym -> SBit sym -> SEval sym (SBit sym)
iteBit sym
sym) SBit sym
b SEval sym (SBit sym)
bitval (forall sym a. Backend sym => SeqMap sym a -> Integer -> SEval sym a
lookupSeqMap SeqMap sym (SBit sym)
bs Integer
i)
           IndexDirection
IndexBackward ->
             forall sym.
Backend sym =>
sym
-> Integer -> SeqMap sym (SBit sym) -> SEval sym (WordValue sym)
bitmapWordVal sym
sym Integer
sz 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 SBit sym
b <- forall sym.
Backend sym =>
sym -> WordValue sym -> Integer -> SEval sym (SBit sym)
wordValueEqualsInteger sym
sym WordValue sym
idx (Integer
sz forall a. Num a => a -> a -> a
- Integer
i forall a. Num a => a -> a -> a
- Integer
1)
                  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 (forall sym.
Backend sym =>
sym -> SBit sym -> SBit sym -> SBit sym -> SEval sym (SBit sym)
iteBit sym
sym) SBit sym
b SEval sym (SBit sym)
bitval (forall sym a. Backend sym => SeqMap sym a -> Integer -> SEval sym a
lookupSeqMap SeqMap sym (SBit sym)
bs Integer
i)

   loop (WordVal SWord sym
wv) = forall sym. SWord sym -> WordValue sym
WordVal forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
      -- TODO, this is too strict in bit
      do let sz :: Integer
sz = forall sym. Backend sym => sym -> SWord sym -> Integer
wordLen sym
sym SWord sym
wv
         SBit sym
b <- SEval sym (SBit sym)
bitval
         SWord sym
msk <- case IndexDirection
dir of
                  IndexDirection
IndexForward ->
                    do SWord sym
highbit <- forall sym.
Backend sym =>
sym -> Integer -> Integer -> SEval sym (SWord sym)
wordLit sym
sym Integer
sz (forall a. Bits a => Int -> a
bit (forall a. Num a => Integer -> a
fromInteger (Integer
szforall a. Num a => a -> a -> a
-Integer
1)))
                       forall sym.
Backend sym =>
sym -> SWord sym -> SWord sym -> SEval sym (SWord sym)
wordShiftRight sym
sym SWord sym
highbit forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall sym.
Backend sym =>
sym -> WordValue sym -> SEval sym (SWord sym)
asWordVal sym
sym WordValue sym
idx
                  IndexDirection
IndexBackward ->
                    do SWord sym
lowbit <- forall sym.
Backend sym =>
sym -> Integer -> Integer -> SEval sym (SWord sym)
wordLit sym
sym Integer
sz Integer
1
                       forall sym.
Backend sym =>
sym -> SWord sym -> SWord sym -> SEval sym (SWord sym)
wordShiftLeft sym
sym SWord sym
lowbit forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall sym.
Backend sym =>
sym -> WordValue sym -> SEval sym (SWord sym)
asWordVal sym
sym WordValue sym
idx
         case forall sym. Backend sym => sym -> SBit sym -> Maybe Bool
bitAsLit sym
sym SBit sym
b of
           Just Bool
True  -> forall sym.
Backend sym =>
sym -> SWord sym -> SWord sym -> SEval sym (SWord sym)
wordOr  sym
sym SWord sym
wv SWord sym
msk
           Just Bool
False -> forall sym.
Backend sym =>
sym -> SWord sym -> SWord sym -> SEval sym (SWord sym)
wordAnd sym
sym SWord sym
wv forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall sym.
Backend sym =>
sym -> SWord sym -> SEval sym (SWord sym)
wordComplement sym
sym SWord sym
msk
           Maybe Bool
Nothing ->
             do SWord sym
zro <- forall sym.
Backend sym =>
sym -> Integer -> Integer -> SEval sym (SWord sym)
wordLit sym
sym Integer
sz Integer
0
                SWord sym
one <- forall sym.
Backend sym =>
sym -> SWord sym -> SEval sym (SWord sym)
wordComplement sym
sym SWord sym
zro
                SWord sym
q   <- forall sym.
Backend sym =>
sym -> SBit sym -> SWord sym -> SWord sym -> SEval sym (SWord sym)
iteWord sym
sym SBit sym
b SWord sym
one SWord sym
zro
                SWord sym
w'  <- forall sym.
Backend sym =>
sym -> SWord sym -> SWord sym -> SEval sym (SWord sym)
wordAnd sym
sym SWord sym
wv forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall sym.
Backend sym =>
sym -> SWord sym -> SEval sym (SWord sym)
wordComplement sym
sym SWord sym
msk
                forall sym.
Backend sym =>
sym -> SWord sym -> SWord sym -> SEval sym (SWord sym)
wordXor sym
sym SWord sym
w' forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall sym.
Backend sym =>
sym -> SWord sym -> SWord sym -> SEval sym (SWord sym)
wordAnd sym
sym SWord sym
msk SWord sym
q


{-# INLINE shiftSeqByWord #-}
shiftSeqByWord  ::
  Backend sym =>
  sym ->
  (SBit sym -> a -> a -> SEval sym a)
     {- ^ if/then/else operation of values -} ->
  (Integer -> Integer -> Maybe Integer)
     {- ^ reindexing operation -} ->
  SEval sym a  {- ^ zero value -} ->
  Nat' {- ^ size of the sequence -} ->
  SeqMap sym a {- ^ sequence to shift -} ->
  WordValue sym {- ^ shift amount -} ->
  SEval sym (SeqMap sym a)
shiftSeqByWord :: forall sym a.
Backend sym =>
sym
-> (SBit sym -> a -> a -> SEval sym a)
-> (Integer -> Integer -> Maybe Integer)
-> SEval sym a
-> Nat'
-> SeqMap sym a
-> WordValue sym
-> SEval sym (SeqMap sym a)
shiftSeqByWord sym
sym SBit sym -> a -> a -> SEval sym a
merge Integer -> Integer -> Maybe Integer
reindex SEval sym a
zro Nat'
sz SeqMap sym a
xs WordValue sym
idx =
  forall sym.
Backend sym =>
sym -> WordValue sym -> SEval sym (Maybe Integer)
wordValAsLit sym
sym WordValue sym
idx forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
    Just Integer
j -> SeqMap sym a -> Integer -> SEval sym (SeqMap sym a)
shiftOp SeqMap sym a
xs Integer
j
    Maybe Integer
Nothing ->
      do [IndexSegment sym]
idx_segs <- forall sym.
Backend sym =>
sym -> WordValue sym -> SEval sym [IndexSegment sym]
enumerateIndexSegments sym
sym WordValue 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'
sz SeqMap sym a
xs Integer
idx_bits [IndexSegment sym]
idx_segs
  where
   idx_bits :: Integer
idx_bits = forall sym. Backend sym => sym -> WordValue sym -> Integer
wordValueSize sym
sym WordValue sym
idx

   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'

-- | Compute the size of a word value
-- TODO, can we get rid of this? If feels like it should be
--  unnecessary.
wordValueSize :: Backend sym => sym -> WordValue sym -> Integer
wordValueSize :: forall sym. Backend sym => sym -> WordValue sym -> Integer
wordValueSize sym
sym (WordVal SWord sym
w)  = forall sym. Backend sym => sym -> SWord sym -> Integer
wordLen sym
sym SWord sym
w
wordValueSize sym
_ (ThunkWordVal Integer
n SEval sym (WordValue sym)
_) = Integer
n
wordValueSize sym
_ (BitmapVal Integer
n SEval sym (SWord sym)
_ SeqMap sym (SBit sym)
_) = Integer
n

-- | Select an individual bit from a word value
indexWordValue :: Backend sym => sym -> WordValue sym -> Integer -> SEval sym (SBit sym)
indexWordValue :: forall sym.
Backend sym =>
sym -> WordValue sym -> Integer -> SEval sym (SBit sym)
indexWordValue sym
sym (ThunkWordVal Integer
_ SEval sym (WordValue sym)
m) Integer
idx = do WordValue sym
m' <- SEval sym (WordValue sym)
m ; forall sym.
Backend sym =>
sym -> WordValue sym -> Integer -> SEval sym (SBit sym)
indexWordValue sym
sym WordValue sym
m' Integer
idx
indexWordValue sym
sym (WordVal SWord sym
w) Integer
idx
   | Integer
0 forall a. Ord a => a -> a -> Bool
<= Integer
idx Bool -> Bool -> Bool
&& Integer
idx forall a. Ord a => a -> a -> Bool
< forall sym. Backend sym => sym -> SWord sym -> Integer
wordLen sym
sym SWord sym
w = forall sym.
Backend sym =>
sym -> SWord sym -> Integer -> SEval sym (SBit sym)
wordBit sym
sym SWord sym
w Integer
idx
   | Bool
otherwise = forall sym a. Backend sym => sym -> Integer -> SEval sym a
invalidIndex sym
sym Integer
idx
indexWordValue sym
sym (BitmapVal Integer
n SEval sym (SWord sym)
_packed SeqMap sym (SBit sym)
xs) Integer
idx
   | Integer
0 forall a. Ord a => a -> a -> Bool
<= Integer
idx Bool -> Bool -> Bool
&& Integer
idx forall a. Ord a => a -> a -> Bool
< Integer
n = forall sym a. Backend sym => SeqMap sym a -> Integer -> SEval sym a
lookupSeqMap SeqMap sym (SBit sym)
xs Integer
idx
   | Bool
otherwise = forall sym a. Backend sym => sym -> Integer -> SEval sym a
invalidIndex sym
sym Integer
idx

-- | Produce a new 'WordValue' from the one given by updating the @i@th bit with the
--   given bit value.
updateWordValue :: Backend sym =>
  sym -> WordValue sym -> Integer -> SEval sym (SBit sym) -> SEval sym (WordValue sym)
updateWordValue :: forall sym.
Backend sym =>
sym
-> WordValue sym
-> Integer
-> SEval sym (SBit sym)
-> SEval sym (WordValue sym)
updateWordValue sym
sym WordValue sym
wv0 Integer
idx SEval sym (SBit sym)
b = WordValue sym -> SEval sym (WordValue sym)
loop WordValue sym
wv0
  where
    loop :: WordValue sym -> SEval sym (WordValue sym)
loop (ThunkWordVal Integer
sz SEval sym (WordValue sym)
m) =
      forall sym a.
Backend sym =>
sym -> SEval sym a -> SEval sym (Maybe a)
isReady sym
sym SEval sym (WordValue sym)
m forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
        Just WordValue sym
w  -> WordValue sym -> SEval sym (WordValue sym)
loop WordValue sym
w
        Maybe (WordValue sym)
Nothing -> forall sym.
Backend sym =>
sym
-> Integer
-> SEval sym (WordValue sym)
-> SEval sym (WordValue sym)
delayWordValue sym
sym Integer
sz (WordValue sym -> SEval sym (WordValue sym)
loop forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< SEval sym (WordValue sym)
m)

    loop (WordVal SWord sym
w)
      | Integer
idx forall a. Ord a => a -> a -> Bool
< Integer
0 Bool -> Bool -> Bool
|| Integer
idx forall a. Ord a => a -> a -> Bool
>= forall sym. Backend sym => sym -> SWord sym -> Integer
wordLen sym
sym SWord sym
w = forall sym a. Backend sym => sym -> Integer -> SEval sym a
invalidIndex sym
sym Integer
idx
      | Bool
otherwise =
          forall sym a.
Backend sym =>
sym -> SEval sym a -> SEval sym (Maybe a)
isReady sym
sym SEval sym (SBit sym)
b forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
            Just SBit sym
b' -> forall sym. SWord sym -> WordValue sym
WordVal forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym.
Backend sym =>
sym -> SWord sym -> Integer -> SBit sym -> SEval sym (SWord sym)
wordUpdate sym
sym SWord sym
w Integer
idx SBit sym
b'
            Maybe (SBit sym)
Nothing ->
              do let bs :: SeqMap sym (SBit sym)
bs = forall sym.
Backend sym =>
sym -> SWord sym -> SeqMap sym (SBit sym)
unpackBitmap sym
sym SWord sym
w
                 forall sym.
Backend sym =>
sym
-> Integer -> SeqMap sym (SBit sym) -> SEval sym (WordValue sym)
bitmapWordVal sym
sym (forall sym. Backend sym => sym -> SWord sym -> Integer
wordLen sym
sym SWord sym
w) forall a b. (a -> b) -> a -> b
$ forall sym a.
SeqMap sym a -> Integer -> SEval sym a -> SeqMap sym a
updateSeqMap SeqMap sym (SBit sym)
bs Integer
idx SEval sym (SBit sym)
b

    loop (BitmapVal Integer
sz SEval sym (SWord sym)
packed SeqMap sym (SBit sym)
bs)
      | Integer
0 forall a. Ord a => a -> a -> Bool
<= Integer
idx Bool -> Bool -> Bool
&& Integer
idx forall a. Ord a => a -> a -> Bool
< Integer
sz =
          forall sym a.
Backend sym =>
sym -> SEval sym a -> SEval sym (Maybe a)
isReady sym
sym SEval sym (SWord sym)
packed forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
            Just SWord sym
w  -> WordValue sym -> SEval sym (WordValue sym)
loop (forall sym. SWord sym -> WordValue sym
WordVal SWord sym
w)
            Maybe (SWord sym)
Nothing -> forall sym.
Backend sym =>
sym
-> Integer -> SeqMap sym (SBit sym) -> SEval sym (WordValue sym)
bitmapWordVal sym
sym Integer
sz forall a b. (a -> b) -> a -> b
$ forall sym a.
SeqMap sym a -> Integer -> SEval sym a -> SeqMap sym a
updateSeqMap SeqMap sym (SBit sym)
bs Integer
idx SEval sym (SBit sym)
b
      | Bool
otherwise = forall sym a. Backend sym => sym -> Integer -> SEval sym a
invalidIndex sym
sym Integer
idx

{-# INLINE mergeWord #-}
mergeWord :: Backend sym =>
  sym ->
  SBit sym ->
  WordValue sym ->
  WordValue sym ->
  SEval sym (WordValue sym)
mergeWord :: forall sym.
Backend sym =>
sym
-> SBit sym
-> WordValue sym
-> WordValue sym
-> SEval sym (WordValue sym)
mergeWord sym
sym SBit sym
c (ThunkWordVal Integer
_ SEval sym (WordValue sym)
m1) (ThunkWordVal Integer
_ SEval sym (WordValue sym)
m2) =
  forall sym.
Backend sym =>
sym
-> SBit sym
-> SEval sym (WordValue sym)
-> SEval sym (WordValue sym)
-> SEval sym (WordValue sym)
mergeWord' sym
sym SBit sym
c (forall sym.
Backend sym =>
SEval sym (WordValue sym) -> SEval sym (WordValue sym)
unwindThunks SEval sym (WordValue sym)
m1) (forall sym.
Backend sym =>
SEval sym (WordValue sym) -> SEval sym (WordValue sym)
unwindThunks SEval sym (WordValue sym)
m2)
mergeWord sym
sym SBit sym
c (ThunkWordVal Integer
_ SEval sym (WordValue sym)
m1) WordValue sym
w2 =
  forall sym.
Backend sym =>
sym
-> SBit sym
-> SEval sym (WordValue sym)
-> SEval sym (WordValue sym)
-> SEval sym (WordValue sym)
mergeWord' sym
sym SBit sym
c (forall sym.
Backend sym =>
SEval sym (WordValue sym) -> SEval sym (WordValue sym)
unwindThunks SEval sym (WordValue sym)
m1) (forall (f :: * -> *) a. Applicative f => a -> f a
pure WordValue sym
w2)
mergeWord sym
sym SBit sym
c WordValue sym
w1 (ThunkWordVal Integer
_ SEval sym (WordValue sym)
m2) =
  forall sym.
Backend sym =>
sym
-> SBit sym
-> SEval sym (WordValue sym)
-> SEval sym (WordValue sym)
-> SEval sym (WordValue sym)
mergeWord' sym
sym SBit sym
c (forall (f :: * -> *) a. Applicative f => a -> f a
pure WordValue sym
w1) (forall sym.
Backend sym =>
SEval sym (WordValue sym) -> SEval sym (WordValue sym)
unwindThunks SEval sym (WordValue sym)
m2)

mergeWord sym
sym SBit sym
c (WordVal SWord sym
w1) (WordVal SWord sym
w2) =
  forall sym. SWord sym -> WordValue sym
WordVal forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym.
Backend sym =>
sym -> SBit sym -> SWord sym -> SWord sym -> SEval sym (SWord sym)
iteWord sym
sym SBit sym
c SWord sym
w1 SWord sym
w2

mergeWord sym
sym SBit sym
c (BitmapVal Integer
n1 SEval sym (SWord sym)
packed1 SeqMap sym (SBit sym)
bs1) (WordVal SWord sym
w2) =
  forall sym a.
Backend sym =>
sym -> SEval sym a -> SEval sym (Maybe a)
isReady sym
sym SEval sym (SWord sym)
packed1 forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
    Just SWord sym
w1 -> forall sym. SWord sym -> WordValue sym
WordVal forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym.
Backend sym =>
sym -> SBit sym -> SWord sym -> SWord sym -> SEval sym (SWord sym)
iteWord sym
sym SBit sym
c SWord sym
w1 SWord sym
w2
    Maybe (SWord sym)
Nothing -> forall sym.
Backend sym =>
sym
-> SBit sym
-> Integer
-> SeqMap sym (SBit sym)
-> SeqMap sym (SBit sym)
-> SEval sym (WordValue sym)
mergeBitmaps sym
sym SBit sym
c Integer
n1 SeqMap sym (SBit sym)
bs1 (forall sym.
Backend sym =>
sym -> SWord sym -> SeqMap sym (SBit sym)
unpackBitmap sym
sym SWord sym
w2)

mergeWord sym
sym SBit sym
c (WordVal SWord sym
w1) (BitmapVal Integer
n2 SEval sym (SWord sym)
packed2 SeqMap sym (SBit sym)
bs2) =
  forall sym a.
Backend sym =>
sym -> SEval sym a -> SEval sym (Maybe a)
isReady sym
sym SEval sym (SWord sym)
packed2 forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
    Just SWord sym
w2 -> forall sym. SWord sym -> WordValue sym
WordVal forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym.
Backend sym =>
sym -> SBit sym -> SWord sym -> SWord sym -> SEval sym (SWord sym)
iteWord sym
sym SBit sym
c SWord sym
w1 SWord sym
w2
    Maybe (SWord sym)
Nothing -> forall sym.
Backend sym =>
sym
-> SBit sym
-> Integer
-> SeqMap sym (SBit sym)
-> SeqMap sym (SBit sym)
-> SEval sym (WordValue sym)
mergeBitmaps sym
sym SBit sym
c Integer
n2 (forall sym.
Backend sym =>
sym -> SWord sym -> SeqMap sym (SBit sym)
unpackBitmap sym
sym SWord sym
w1) SeqMap sym (SBit sym)
bs2

mergeWord sym
sym SBit sym
c (BitmapVal Integer
n1 SEval sym (SWord sym)
packed1 SeqMap sym (SBit sym)
bs1) (BitmapVal Integer
_n2 SEval sym (SWord sym)
packed2 SeqMap sym (SBit sym)
bs2) =
  do Maybe (SWord sym)
r1 <- forall sym a.
Backend sym =>
sym -> SEval sym a -> SEval sym (Maybe a)
isReady sym
sym SEval sym (SWord sym)
packed1
     Maybe (SWord sym)
r2 <- forall sym a.
Backend sym =>
sym -> SEval sym a -> SEval sym (Maybe a)
isReady sym
sym SEval sym (SWord sym)
packed2
     case (Maybe (SWord sym)
r1,Maybe (SWord sym)
r2) of
       (Just SWord sym
w1, Just SWord sym
w2) -> forall sym. SWord sym -> WordValue sym
WordVal forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym.
Backend sym =>
sym -> SBit sym -> SWord sym -> SWord sym -> SEval sym (SWord sym)
iteWord sym
sym SBit sym
c SWord sym
w1 SWord sym
w2
       (Maybe (SWord sym), Maybe (SWord sym))
_ -> forall sym.
Backend sym =>
sym
-> SBit sym
-> Integer
-> SeqMap sym (SBit sym)
-> SeqMap sym (SBit sym)
-> SEval sym (WordValue sym)
mergeBitmaps sym
sym SBit sym
c Integer
n1 SeqMap sym (SBit sym)
bs1 SeqMap sym (SBit sym)
bs2

mergeBitmaps :: Backend sym =>
  sym ->
  SBit sym ->
  Integer ->
  SeqMap sym (SBit sym) ->
  SeqMap sym (SBit sym) ->
  SEval sym (WordValue sym)
mergeBitmaps :: forall sym.
Backend sym =>
sym
-> SBit sym
-> Integer
-> SeqMap sym (SBit sym)
-> SeqMap sym (SBit sym)
-> SEval sym (WordValue sym)
mergeBitmaps sym
sym SBit sym
c Integer
sz SeqMap sym (SBit sym)
bs1 SeqMap sym (SBit sym)
bs2 =
  do SeqMap sym (SBit sym)
bs <- forall sym a.
Backend sym =>
sym -> Nat' -> SeqMap sym a -> SEval sym (SeqMap sym a)
memoMap sym
sym (Integer -> Nat'
Nat Integer
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 (forall sym.
Backend sym =>
sym -> SBit sym -> SBit sym -> SBit sym -> SEval sym (SBit sym)
iteBit sym
sym) SBit sym
c SeqMap sym (SBit sym)
bs1 SeqMap sym (SBit sym)
bs2)
     forall sym.
Backend sym =>
sym
-> Integer -> SeqMap sym (SBit sym) -> SEval sym (WordValue sym)
bitmapWordVal sym
sym Integer
sz SeqMap sym (SBit sym)
bs

{-# INLINE mergeWord' #-}
mergeWord' :: Backend sym =>
  sym ->
  SBit sym ->
  SEval sym (WordValue sym) ->
  SEval sym (WordValue sym) ->
  SEval sym (WordValue sym)
mergeWord' :: forall sym.
Backend sym =>
sym
-> SBit sym
-> SEval sym (WordValue sym)
-> SEval sym (WordValue sym)
-> SEval sym (WordValue sym)
mergeWord' sym
sym SBit sym
c SEval sym (WordValue sym)
x SEval sym (WordValue sym)
y
  | Just Bool
b <- forall sym. Backend sym => sym -> SBit sym -> Maybe Bool
bitAsLit sym
sym SBit sym
c = if Bool
b then SEval sym (WordValue sym)
x else SEval sym (WordValue sym)
y
  | Bool
otherwise = 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 (forall sym.
Backend sym =>
sym
-> SBit sym
-> WordValue sym
-> WordValue sym
-> SEval sym (WordValue sym)
mergeWord sym
sym) SBit sym
c SEval sym (WordValue sym)
x SEval sym (WordValue sym)
y