-- |
-- 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 :: WordValue sym -> SEval sym ()
forceWordValue (WordVal SWord sym
w)  = SWord sym -> SEval sym () -> SEval sym ()
seq SWord sym
w (() -> SEval sym ()
forall (m :: * -> *) a. Monad m => a -> m a
return ())
forceWordValue (ThunkWordVal Integer
_ SEval sym (WordValue sym)
m)  = WordValue sym -> SEval sym ()
forall sym. Backend sym => WordValue sym -> SEval sym ()
forceWordValue (WordValue sym -> SEval sym ())
-> SEval sym (WordValue sym) -> SEval sym ()
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; SWord sym -> SEval sym () -> SEval sym ()
seq SWord sym
w (() -> SEval sym ()
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 = Int -> Integer
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 x. WordValue sym -> Rep (WordValue sym) x)
-> (forall x. Rep (WordValue sym) x -> WordValue sym)
-> Generic (WordValue sym)
forall x. Rep (WordValue sym) x -> WordValue sym
forall x. WordValue sym -> Rep (WordValue sym) x
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 :: SWord sym -> WordValue sym
wordVal = SWord sym -> WordValue sym
forall sym. SWord sym -> WordValue sym
WordVal

packBitmap :: Backend sym => sym -> Integer -> SeqMap sym (SBit sym) -> SEval sym (SWord sym)
packBitmap :: sym -> Integer -> SeqMap sym (SBit sym) -> SEval sym (SWord sym)
packBitmap sym
sym Integer
sz SeqMap sym (SBit sym)
bs = sym -> [SBit sym] -> SEval sym (SWord sym)
forall sym.
Backend sym =>
sym -> [SBit sym] -> SEval sym (SWord sym)
packWord sym
sym ([SBit sym] -> SEval sym (SWord sym))
-> SEval sym [SBit sym] -> SEval sym (SWord sym)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< [SEval sym (SBit sym)] -> SEval sym [SBit sym]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence (Integer -> SeqMap sym (SBit sym) -> [SEval sym (SBit sym)]
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 :: sym -> SWord sym -> SeqMap sym (SBit sym)
unpackBitmap sym
sym SWord sym
w = (Integer -> SEval sym (SBit sym)) -> SeqMap sym (SBit sym)
forall sym a. (Integer -> SEval sym a) -> SeqMap sym a
indexSeqMap ((Integer -> SEval sym (SBit sym)) -> SeqMap sym (SBit sym))
-> (Integer -> SEval sym (SBit sym)) -> SeqMap sym (SBit sym)
forall a b. (a -> b) -> a -> b
$ \Integer
i -> sym -> SWord sym -> Integer -> SEval sym (SBit sym)
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 :: 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 <- sym -> SEval sym (SWord sym) -> SEval sym (SEval sym (SWord sym))
forall sym a.
Backend sym =>
sym -> SEval sym a -> SEval sym (SEval sym a)
sDelay sym
sym (sym -> Integer -> SeqMap sym (SBit sym) -> SEval sym (SWord 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)
     WordValue sym -> SEval sym (WordValue sym)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Integer
-> SEval sym (SWord sym) -> SeqMap sym (SBit sym) -> WordValue sym
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 :: 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 = sym -> WordValue sym -> WordValue sym -> SEval sym (WordValue sym)
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) ->
      SWord sym -> WordValue sym
forall sym. SWord sym -> WordValue sym
WordVal (SWord sym -> WordValue sym)
-> SEval sym (SWord sym) -> SEval sym (WordValue sym)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> sym -> SWord sym -> SWord sym -> SEval sym (SWord sym)
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
_) ->
      sym
-> SEval sym (WordValue sym) -> SEval sym (Maybe (WordValue sym))
forall sym a.
Backend sym =>
sym -> SEval sym a -> SEval sym (Maybe a)
isReady sym
sym SEval sym (WordValue sym)
m1 SEval sym (Maybe (WordValue sym))
-> (Maybe (WordValue sym) -> SEval sym (WordValue sym))
-> SEval sym (WordValue sym)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
        Just WordValue sym
x -> sym -> WordValue sym -> WordValue sym -> SEval sym (WordValue sym)
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) ->
      sym
-> SEval sym (WordValue sym) -> SEval sym (Maybe (WordValue sym))
forall sym a.
Backend sym =>
sym -> SEval sym a -> SEval sym (Maybe a)
isReady sym
sym SEval sym (WordValue sym)
m2 SEval sym (Maybe (WordValue sym))
-> (Maybe (WordValue sym) -> SEval sym (WordValue sym))
-> SEval sym (WordValue sym)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
        Just WordValue sym
x   -> sym -> WordValue sym -> WordValue sym -> SEval sym (WordValue sym)
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)
_) ->
      sym -> SEval sym (SWord sym) -> SEval sym (Maybe (SWord sym))
forall sym a.
Backend sym =>
sym -> SEval sym a -> SEval sym (Maybe a)
isReady sym
sym SEval sym (SWord sym)
packed2 SEval sym (Maybe (SWord sym))
-> (Maybe (SWord sym) -> SEval sym (WordValue sym))
-> SEval sym (WordValue sym)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
        Just SWord sym
w2 -> SWord sym -> WordValue sym
forall sym. SWord sym -> WordValue sym
WordVal (SWord sym -> WordValue sym)
-> SEval sym (SWord sym) -> SEval sym (WordValue sym)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> sym -> SWord sym -> SWord sym -> SEval sym (SWord sym)
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) ->
      sym -> SEval sym (SWord sym) -> SEval sym (Maybe (SWord sym))
forall sym a.
Backend sym =>
sym -> SEval sym a -> SEval sym (Maybe a)
isReady sym
sym SEval sym (SWord sym)
packed1 SEval sym (Maybe (SWord sym))
-> (Maybe (SWord sym) -> SEval sym (WordValue sym))
-> SEval sym (WordValue sym)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
        Just SWord sym
w1 -> SWord sym -> WordValue sym
forall sym. SWord sym -> WordValue sym
WordVal (SWord sym -> WordValue sym)
-> SEval sym (SWord sym) -> SEval sym (WordValue sym)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> sym -> SWord sym -> SWord sym -> SEval sym (SWord sym)
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 <- sym -> SEval sym (SWord sym) -> SEval sym (Maybe (SWord sym))
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 <- sym -> SEval sym (SWord sym) -> SEval sym (Maybe (SWord sym))
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) -> SWord sym -> WordValue sym
forall sym. SWord sym -> WordValue sym
WordVal (SWord sym -> WordValue sym)
-> SEval sym (SWord sym) -> SEval sym (WordValue sym)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> sym -> SWord sym -> SWord sym -> SEval sym (SWord sym)
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 :: sym -> WordValue sym -> WordValue sym -> SEval sym (WordValue sym)
fallbackWordJoin sym
sym WordValue sym
w1 WordValue sym
w2 =
  do let n1 :: Integer
n1 = sym -> WordValue sym -> Integer
forall sym. Backend sym => sym -> WordValue sym -> Integer
wordValueSize sym
sym WordValue sym
w1
     let n2 :: Integer
n2 = sym -> WordValue sym -> Integer
forall sym. Backend sym => sym -> WordValue sym -> Integer
wordValueSize sym
sym WordValue sym
w2
     let len :: Integer
len = Integer
n1 Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
n2
     SEval sym (SWord sym)
packed <- sym -> SEval sym (SWord sym) -> SEval sym (SEval sym (SWord sym))
forall sym a.
Backend sym =>
sym -> SEval sym a -> SEval sym (SEval sym a)
sDelay sym
sym
                 (do SWord sym
a <- sym -> WordValue sym -> SEval sym (SWord sym)
forall sym.
Backend sym =>
sym -> WordValue sym -> SEval sym (SWord sym)
asWordVal sym
sym WordValue sym
w1
                     SWord sym
b <- sym -> WordValue sym -> SEval sym (SWord sym)
forall sym.
Backend sym =>
sym -> WordValue sym -> SEval sym (SWord sym)
asWordVal sym
sym WordValue sym
w2
                     sym -> SWord sym -> SWord sym -> SEval sym (SWord sym)
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 = Integer
-> SeqMap sym (SBit sym)
-> SeqMap sym (SBit sym)
-> SeqMap sym (SBit sym)
forall sym a.
Backend sym =>
Integer -> SeqMap sym a -> SeqMap sym a -> SeqMap sym a
concatSeqMap Integer
n1 (sym -> WordValue sym -> SeqMap sym (SBit sym)
forall sym.
Backend sym =>
sym -> WordValue sym -> SeqMap sym (SBit sym)
asBitsMap sym
sym WordValue sym
w1) (sym -> WordValue sym -> SeqMap sym (SBit sym)
forall sym.
Backend sym =>
sym -> WordValue sym -> SeqMap sym (SBit sym)
asBitsMap sym
sym WordValue sym
w2)
     WordValue sym -> SEval sym (WordValue sym)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Integer
-> SEval sym (SWord sym) -> SeqMap sym (SBit sym) -> WordValue sym
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 :: 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) <- sym
-> Integer
-> Integer
-> SWord sym
-> SEval sym (SWord sym, SWord sym)
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
     WordValue sym -> SEval sym (WordValue sym)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SWord sym -> WordValue sym
forall sym. SWord sym -> WordValue sym
WordVal SWord sym
lw)

takeWordVal sym
sym Integer
leftWidth Integer
rightWidth (ThunkWordVal Integer
_ SEval sym (WordValue sym)
m) =
  sym
-> SEval sym (WordValue sym) -> SEval sym (Maybe (WordValue sym))
forall sym a.
Backend sym =>
sym -> SEval sym a -> SEval sym (Maybe a)
isReady sym
sym SEval sym (WordValue sym)
m SEval sym (Maybe (WordValue sym))
-> (Maybe (WordValue sym) -> SEval sym (WordValue sym))
-> SEval sym (WordValue sym)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
    Just WordValue sym
w -> sym
-> Integer -> Integer -> WordValue sym -> SEval sym (WordValue sym)
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' <- sym
-> SEval sym (WordValue sym)
-> SEval sym (SEval sym (WordValue sym))
forall sym a.
Backend sym =>
sym -> SEval sym a -> SEval sym (SEval sym a)
sDelay sym
sym (sym
-> Integer -> Integer -> WordValue sym -> SEval sym (WordValue sym)
forall sym.
Backend sym =>
sym
-> Integer -> Integer -> WordValue sym -> SEval sym (WordValue sym)
takeWordVal sym
sym Integer
leftWidth Integer
rightWidth (WordValue sym -> SEval sym (WordValue sym))
-> SEval sym (WordValue sym) -> SEval sym (WordValue sym)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< SEval sym (WordValue sym)
m)
         WordValue sym -> SEval sym (WordValue sym)
forall (m :: * -> *) a. Monad m => a -> m a
return (Integer -> SEval sym (WordValue sym) -> WordValue sym
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) =
  sym -> SEval sym (SWord sym) -> SEval sym (Maybe (SWord sym))
forall sym a.
Backend sym =>
sym -> SEval sym a -> SEval sym (Maybe a)
isReady sym
sym SEval sym (SWord sym)
packed SEval sym (Maybe (SWord sym))
-> (Maybe (SWord sym) -> SEval sym (WordValue sym))
-> SEval sym (WordValue sym)
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) <- sym
-> Integer
-> Integer
-> SWord sym
-> SEval sym (SWord sym, SWord sym)
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
                 WordValue sym -> SEval sym (WordValue sym)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SWord sym -> WordValue sym
forall sym. SWord sym -> WordValue sym
WordVal SWord sym
lw)
    Maybe (SWord sym)
Nothing -> sym
-> Integer -> SeqMap sym (SBit sym) -> SEval sym (WordValue sym)
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 :: 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) <- sym
-> Integer
-> Integer
-> SWord sym
-> SEval sym (SWord sym, SWord sym)
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
     WordValue sym -> SEval sym (WordValue sym)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SWord sym -> WordValue sym
forall sym. SWord sym -> WordValue sym
WordVal SWord sym
rw)

dropWordVal sym
sym Integer
leftWidth Integer
rightWidth (ThunkWordVal Integer
_ SEval sym (WordValue sym)
m) =
  sym
-> SEval sym (WordValue sym) -> SEval sym (Maybe (WordValue sym))
forall sym a.
Backend sym =>
sym -> SEval sym a -> SEval sym (Maybe a)
isReady sym
sym SEval sym (WordValue sym)
m SEval sym (Maybe (WordValue sym))
-> (Maybe (WordValue sym) -> SEval sym (WordValue sym))
-> SEval sym (WordValue sym)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
    Just WordValue sym
w -> sym
-> Integer -> Integer -> WordValue sym -> SEval sym (WordValue sym)
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' <- sym
-> SEval sym (WordValue sym)
-> SEval sym (SEval sym (WordValue sym))
forall sym a.
Backend sym =>
sym -> SEval sym a -> SEval sym (SEval sym a)
sDelay sym
sym (sym
-> Integer -> Integer -> WordValue sym -> SEval sym (WordValue sym)
forall sym.
Backend sym =>
sym
-> Integer -> Integer -> WordValue sym -> SEval sym (WordValue sym)
dropWordVal sym
sym Integer
leftWidth Integer
rightWidth (WordValue sym -> SEval sym (WordValue sym))
-> SEval sym (WordValue sym) -> SEval sym (WordValue sym)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< SEval sym (WordValue sym)
m)
         WordValue sym -> SEval sym (WordValue sym)
forall (m :: * -> *) a. Monad m => a -> m a
return (Integer -> SEval sym (WordValue sym) -> WordValue sym
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) =
  sym -> SEval sym (SWord sym) -> SEval sym (Maybe (SWord sym))
forall sym a.
Backend sym =>
sym -> SEval sym a -> SEval sym (Maybe a)
isReady sym
sym SEval sym (SWord sym)
packed SEval sym (Maybe (SWord sym))
-> (Maybe (SWord sym) -> SEval sym (WordValue sym))
-> SEval sym (WordValue sym)
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) <- sym
-> Integer
-> Integer
-> SWord sym
-> SEval sym (SWord sym, SWord sym)
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
                 WordValue sym -> SEval sym (WordValue sym)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SWord sym -> WordValue sym
forall sym. SWord sym -> WordValue sym
WordVal SWord sym
rw)
    Maybe (SWord sym)
Nothing ->
      do let rxs :: SeqMap sym (SBit sym)
rxs = Integer -> SeqMap sym (SBit sym) -> SeqMap sym (SBit sym)
forall sym a.
Backend sym =>
Integer -> SeqMap sym a -> SeqMap sym a
dropSeqMap Integer
leftWidth SeqMap sym (SBit sym)
xs
         sym
-> Integer -> SeqMap sym (SBit sym) -> SEval sym (WordValue sym)
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 :: sym
-> Integer -> Integer -> WordValue sym -> SEval sym (WordValue sym)
extractWordVal sym
sym Integer
len Integer
start (WordVal SWord sym
w) =
   SWord sym -> WordValue sym
forall sym. SWord sym -> WordValue sym
WordVal (SWord sym -> WordValue sym)
-> SEval sym (SWord sym) -> SEval sym (WordValue sym)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> sym -> Integer -> Integer -> SWord sym -> SEval sym (SWord sym)
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) =
  sym
-> SEval sym (WordValue sym) -> SEval sym (Maybe (WordValue sym))
forall sym a.
Backend sym =>
sym -> SEval sym a -> SEval sym (Maybe a)
isReady sym
sym SEval sym (WordValue sym)
m SEval sym (Maybe (WordValue sym))
-> (Maybe (WordValue sym) -> SEval sym (WordValue sym))
-> SEval sym (WordValue sym)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
    Just WordValue sym
w -> sym
-> Integer -> Integer -> WordValue sym -> SEval sym (WordValue sym)
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' <- sym
-> SEval sym (WordValue sym)
-> SEval sym (SEval sym (WordValue sym))
forall sym a.
Backend sym =>
sym -> SEval sym a -> SEval sym (SEval sym a)
sDelay sym
sym (sym
-> Integer -> Integer -> WordValue sym -> SEval sym (WordValue sym)
forall sym.
Backend sym =>
sym
-> Integer -> Integer -> WordValue sym -> SEval sym (WordValue sym)
extractWordVal sym
sym Integer
len Integer
start (WordValue sym -> SEval sym (WordValue sym))
-> SEval sym (WordValue sym) -> SEval sym (WordValue sym)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< SEval sym (WordValue sym)
m)
         WordValue sym -> SEval sym (WordValue sym)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Integer -> SEval sym (WordValue sym) -> WordValue sym
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) =
  sym -> SEval sym (SWord sym) -> SEval sym (Maybe (SWord sym))
forall sym a.
Backend sym =>
sym -> SEval sym a -> SEval sym (Maybe a)
isReady sym
sym SEval sym (SWord sym)
packed SEval sym (Maybe (SWord sym))
-> (Maybe (SWord sym) -> SEval sym (WordValue sym))
-> SEval sym (WordValue sym)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
    Just SWord sym
w -> SWord sym -> WordValue sym
forall sym. SWord sym -> WordValue sym
WordVal (SWord sym -> WordValue sym)
-> SEval sym (SWord sym) -> SEval sym (WordValue sym)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> sym -> Integer -> Integer -> SWord sym -> SEval sym (SWord sym)
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' = Integer -> SeqMap sym (SBit sym) -> SeqMap sym (SBit sym)
forall sym a.
Backend sym =>
Integer -> SeqMap sym a -> SeqMap sym a
dropSeqMap (Integer
n Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
start Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
len) SeqMap sym (SBit sym)
xs
         sym
-> Integer -> SeqMap sym (SBit sym) -> SEval sym (WordValue sym)
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 :: 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) = SWord sym -> WordValue sym
forall sym. SWord sym -> WordValue sym
WordVal (SWord sym -> WordValue sym)
-> SEval sym (SWord sym) -> SEval sym (WordValue sym)
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) =
  sym -> SEval sym (SWord sym) -> SEval sym (Maybe (SWord sym))
forall sym a.
Backend sym =>
sym -> SEval sym a -> SEval sym (Maybe a)
isReady sym
sym SEval sym (SWord sym)
packed2 SEval sym (Maybe (SWord sym))
-> (Maybe (SWord sym) -> SEval sym (WordValue sym))
-> SEval sym (WordValue sym)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
    Just SWord sym
w2 -> SWord sym -> WordValue sym
forall sym. SWord sym -> WordValue sym
WordVal (SWord sym -> WordValue sym)
-> SEval sym (SWord sym) -> SEval sym (WordValue sym)
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 -> sym
-> Integer -> SeqMap sym (SBit sym) -> SEval sym (WordValue sym)
forall sym.
Backend sym =>
sym
-> Integer -> SeqMap sym (SBit sym) -> SEval sym (WordValue sym)
bitmapWordVal sym
sym Integer
n2 (SeqMap sym (SBit sym) -> SEval sym (WordValue sym))
-> SEval sym (SeqMap sym (SBit sym)) -> SEval sym (WordValue sym)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< sym
-> (SBit sym -> SBit sym -> SEval sym (SBit sym))
-> Nat'
-> SeqMap sym (SBit sym)
-> SeqMap sym (SBit sym)
-> SEval sym (SeqMap sym (SBit sym))
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) (sym -> SWord sym -> SeqMap sym (SBit sym)
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) =
  sym -> SEval sym (SWord sym) -> SEval sym (Maybe (SWord sym))
forall sym a.
Backend sym =>
sym -> SEval sym a -> SEval sym (Maybe a)
isReady sym
sym SEval sym (SWord sym)
packed1 SEval sym (Maybe (SWord sym))
-> (Maybe (SWord sym) -> SEval sym (WordValue sym))
-> SEval sym (WordValue sym)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
    Just SWord sym
w1 -> SWord sym -> WordValue sym
forall sym. SWord sym -> WordValue sym
WordVal (SWord sym -> WordValue sym)
-> SEval sym (SWord sym) -> SEval sym (WordValue sym)
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 -> sym
-> Integer -> SeqMap sym (SBit sym) -> SEval sym (WordValue sym)
forall sym.
Backend sym =>
sym
-> Integer -> SeqMap sym (SBit sym) -> SEval sym (WordValue sym)
bitmapWordVal sym
sym Integer
n1 (SeqMap sym (SBit sym) -> SEval sym (WordValue sym))
-> SEval sym (SeqMap sym (SBit sym)) -> SEval sym (WordValue sym)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< sym
-> (SBit sym -> SBit sym -> SEval sym (SBit sym))
-> Nat'
-> SeqMap sym (SBit sym)
-> SeqMap sym (SBit sym)
-> SEval sym (SeqMap sym (SBit sym))
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 (sym -> SWord sym -> SeqMap sym (SBit sym)
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 <- sym -> SEval sym (SWord sym) -> SEval sym (Maybe (SWord sym))
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 <- sym -> SEval sym (SWord sym) -> SEval sym (Maybe (SWord sym))
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) -> SWord sym -> WordValue sym
forall sym. SWord sym -> WordValue sym
WordVal (SWord sym -> WordValue sym)
-> SEval sym (SWord sym) -> SEval sym (WordValue sym)
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))
_ -> sym
-> Integer -> SeqMap sym (SBit sym) -> SEval sym (WordValue sym)
forall sym.
Backend sym =>
sym
-> Integer -> SeqMap sym (SBit sym) -> SEval sym (WordValue sym)
bitmapWordVal sym
sym Integer
n1 (SeqMap sym (SBit sym) -> SEval sym (WordValue sym))
-> SEval sym (SeqMap sym (SBit sym)) -> SEval sym (WordValue sym)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< sym
-> (SBit sym -> SBit sym -> SEval sym (SBit sym))
-> Nat'
-> SeqMap sym (SBit sym)
-> SeqMap sym (SBit sym)
-> SEval sym (SeqMap sym (SBit sym))
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
     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)
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
     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)
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 :: 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)  = SWord sym -> WordValue sym
forall sym. SWord sym -> WordValue sym
WordVal (SWord sym -> WordValue sym)
-> SEval sym (SWord sym) -> SEval sym (WordValue sym)
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) = sym
-> (SBit sym -> SEval sym (SBit sym))
-> (SWord sym -> SEval sym (SWord sym))
-> WordValue sym
-> SEval sym (WordValue sym)
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 (WordValue sym -> SEval sym (WordValue sym))
-> SEval sym (WordValue sym) -> SEval sym (WordValue sym)
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) =
  sym -> SEval sym (SWord sym) -> SEval sym (Maybe (SWord sym))
forall sym a.
Backend sym =>
sym -> SEval sym a -> SEval sym (Maybe a)
isReady sym
sym SEval sym (SWord sym)
packed SEval sym (Maybe (SWord sym))
-> (Maybe (SWord sym) -> SEval sym (WordValue sym))
-> SEval sym (WordValue sym)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
    Just SWord sym
w  -> SWord sym -> WordValue sym
forall sym. SWord sym -> WordValue sym
WordVal (SWord sym -> WordValue sym)
-> SEval sym (SWord sym) -> SEval sym (WordValue sym)
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 -> sym
-> Integer -> SeqMap sym (SBit sym) -> SEval sym (WordValue sym)
forall sym.
Backend sym =>
sym
-> Integer -> SeqMap sym (SBit sym) -> SEval sym (WordValue sym)
bitmapWordVal sym
sym Integer
n (SeqMap sym (SBit sym) -> SEval sym (WordValue sym))
-> SEval sym (SeqMap sym (SBit sym)) -> SEval sym (WordValue sym)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< sym
-> (SBit sym -> SEval sym (SBit sym))
-> Nat'
-> SeqMap sym (SBit sym)
-> SEval sym (SeqMap sym (SBit sym))
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 :: 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 Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* Integer
nEach Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
largeBitSize =
  do SWord sym
z <- sym -> Integer -> Integer -> SEval sym (SWord sym)
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 (SWord sym -> WordValue sym
forall sym. SWord sym -> WordValue sym
wordVal SWord sym
z) (Integer
-> SeqMap sym (WordValue sym) -> [SEval sym (WordValue sym)]
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 [] = WordValue sym -> SEval sym (WordValue sym)
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'  <- sym
-> Integer
-> SEval sym (WordValue sym)
-> SEval sym (WordValue sym)
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' <- sym -> WordValue sym -> WordValue sym -> SEval sym (WordValue sym)
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 = sym
-> Integer -> SeqMap sym (SBit sym) -> SEval sym (WordValue sym)
forall sym.
Backend sym =>
sym
-> Integer -> SeqMap sym (SBit sym) -> SEval sym (WordValue sym)
bitmapWordVal sym
sym (Integer
nParts Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* Integer
nEach) SeqMap sym (SBit sym)
zs
  where
    zs :: SeqMap sym (SBit sym)
zs = (Integer -> SEval sym (SBit sym)) -> SeqMap sym (SBit sym)
forall sym a. (Integer -> SEval sym a) -> SeqMap sym a
indexSeqMap ((Integer -> SEval sym (SBit sym)) -> SeqMap sym (SBit sym))
-> (Integer -> SEval sym (SBit sym)) -> SeqMap sym (SBit sym)
forall a b. (a -> b) -> a -> b
$ \Integer
i ->
            do let (Integer
q,Integer
r) = Integer -> Integer -> (Integer, Integer)
forall a. Integral a => a -> a -> (a, a)
divMod Integer
i Integer
nEach
               WordValue sym
ys <- SeqMap sym (WordValue sym) -> Integer -> SEval sym (WordValue sym)
forall sym a. Backend sym => SeqMap sym a -> Integer -> SEval sym a
lookupSeqMap SeqMap sym (WordValue sym)
xs Integer
q
               sym -> WordValue sym -> Integer -> SEval sym (SBit sym)
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 :: sym -> WordValue sym -> SEval sym (WordValue sym)
reverseWordVal sym
sym WordValue sym
w =
  let m :: Integer
m = sym -> WordValue sym -> Integer
forall sym. Backend sym => sym -> WordValue sym -> Integer
wordValueSize sym
sym WordValue sym
w in
  sym
-> Integer -> SeqMap sym (SBit sym) -> SEval sym (WordValue sym)
forall sym.
Backend sym =>
sym
-> Integer -> SeqMap sym (SBit sym) -> SEval sym (WordValue sym)
bitmapWordVal sym
sym Integer
m (SeqMap sym (SBit sym) -> SEval sym (WordValue sym))
-> (SeqMap sym (SBit sym) -> SeqMap sym (SBit sym))
-> SeqMap sym (SBit sym)
-> SEval sym (WordValue sym)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Integer -> SeqMap sym (SBit sym) -> SeqMap sym (SBit sym)
forall sym a.
Backend sym =>
Integer -> SeqMap sym a -> SeqMap sym a
reverseSeqMap Integer
m (SeqMap sym (SBit sym) -> SEval sym (WordValue sym))
-> SeqMap sym (SBit sym) -> SEval sym (WordValue sym)
forall a b. (a -> b) -> a -> b
$ sym -> WordValue sym -> SeqMap sym (SBit sym)
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 :: sym -> WordValue sym -> SEval sym (Maybe Integer)
wordValAsLit sym
sym (WordVal SWord sym
w) = Maybe Integer -> SEval sym (Maybe Integer)
forall (f :: * -> *) a. Applicative f => a -> f a
pure ((Integer, Integer) -> Integer
forall a b. (a, b) -> b
snd ((Integer, Integer) -> Integer)
-> Maybe (Integer, Integer) -> Maybe Integer
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> sym -> SWord sym -> Maybe (Integer, Integer)
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) =
  sym
-> SEval sym (WordValue sym) -> SEval sym (Maybe (WordValue sym))
forall sym a.
Backend sym =>
sym -> SEval sym a -> SEval sym (Maybe a)
isReady sym
sym SEval sym (WordValue sym)
m SEval sym (Maybe (WordValue sym))
-> (Maybe (WordValue sym) -> SEval sym (Maybe Integer))
-> SEval sym (Maybe Integer)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
    Just WordValue sym
v  -> sym -> WordValue sym -> SEval sym (Maybe Integer)
forall sym.
Backend sym =>
sym -> WordValue sym -> SEval sym (Maybe Integer)
wordValAsLit sym
sym WordValue sym
v
    Maybe (WordValue sym)
Nothing -> Maybe Integer -> SEval sym (Maybe Integer)
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe Integer
forall a. Maybe a
Nothing
wordValAsLit sym
sym (BitmapVal Integer
_ SEval sym (SWord sym)
packed SeqMap sym (SBit sym)
_) =
  sym -> SEval sym (SWord sym) -> SEval sym (Maybe (SWord sym))
forall sym a.
Backend sym =>
sym -> SEval sym a -> SEval sym (Maybe a)
isReady sym
sym SEval sym (SWord sym)
packed SEval sym (Maybe (SWord sym))
-> (Maybe (SWord sym) -> SEval sym (Maybe Integer))
-> SEval sym (Maybe Integer)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
    Just SWord sym
w  -> Maybe Integer -> SEval sym (Maybe Integer)
forall (f :: * -> *) a. Applicative f => a -> f a
pure ((Integer, Integer) -> Integer
forall a b. (a, b) -> b
snd ((Integer, Integer) -> Integer)
-> Maybe (Integer, Integer) -> Maybe Integer
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> sym -> SWord sym -> Maybe (Integer, Integer)
forall sym.
Backend sym =>
sym -> SWord sym -> Maybe (Integer, Integer)
wordAsLit sym
sym SWord sym
w)
    Maybe (SWord sym)
Nothing -> Maybe Integer -> SEval sym (Maybe Integer)
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe Integer
forall a. Maybe a
Nothing

-- | Force a word value into packed word form
asWordVal :: Backend sym => sym -> WordValue sym -> SEval sym (SWord sym)
asWordVal :: sym -> WordValue sym -> SEval sym (SWord sym)
asWordVal sym
_   (WordVal SWord sym
w)            = SWord sym -> SEval sym (SWord sym)
forall (m :: * -> *) a. Monad m => a -> m a
return SWord sym
w
asWordVal sym
sym (ThunkWordVal Integer
_ SEval sym (WordValue sym)
m)     = sym -> WordValue sym -> SEval sym (SWord sym)
forall sym.
Backend sym =>
sym -> WordValue sym -> SEval sym (SWord sym)
asWordVal sym
sym (WordValue sym -> SEval sym (SWord sym))
-> SEval sym (WordValue sym) -> SEval sym (SWord 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 :: sym -> WordValue sym -> Integer -> SEval sym (SBit sym)
wordValueEqualsInteger sym
sym WordValue sym
wv Integer
i
  | sym -> WordValue sym -> Integer
forall sym. Backend sym => sym -> WordValue sym -> Integer
wordValueSize sym
sym WordValue sym
wv Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer -> Integer
widthInteger Integer
i = SBit sym -> SEval sym (SBit sym)
forall (m :: * -> *) a. Monad m => a -> m a
return (sym -> Bool -> SBit sym
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 (WordValue sym -> SEval sym (SBit sym))
-> SEval sym (WordValue sym) -> SEval sym (SBit sym)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< SEval sym (WordValue sym)
m
   loop (WordVal SWord sym
w) = sym -> SWord sym -> SWord sym -> SEval sym (SBit sym)
forall sym.
Backend sym =>
sym -> SWord sym -> SWord sym -> SEval sym (SBit sym)
wordEq sym
sym SWord sym
w (SWord sym -> SEval sym (SBit sym))
-> SEval sym (SWord sym) -> SEval sym (SBit sym)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< sym -> Integer -> Integer -> SEval sym (SWord sym)
forall sym.
Backend sym =>
sym -> Integer -> Integer -> SEval sym (SWord sym)
wordLit sym
sym (sym -> SWord sym -> Integer
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) =
     sym -> SEval sym (SWord sym) -> SEval sym (Maybe (SWord sym))
forall sym a.
Backend sym =>
sym -> SEval sym a -> SEval sym (Maybe a)
isReady sym
sym SEval sym (SWord sym)
packed SEval sym (Maybe (SWord sym))
-> (Maybe (SWord sym) -> SEval sym (SBit sym))
-> SEval sym (SBit sym)
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 (SWord sym -> WordValue sym
forall sym. SWord sym -> WordValue sym
WordVal SWord sym
w)
       Maybe (SWord sym)
Nothing -> Integer -> [SBit sym] -> SEval sym (SBit sym)
bitsAre Integer
i ([SBit sym] -> SEval sym (SBit sym))
-> SEval sym [SBit sym] -> SEval sym (SBit sym)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< [SEval sym (SBit sym)] -> SEval sym [SBit sym]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence (Integer -> SeqMap sym (SBit sym) -> [SEval sym (SBit sym)]
forall sym n a.
(Backend sym, Integral n) =>
n -> SeqMap sym a -> [SEval sym a]
enumerateSeqMap Integer
n (Integer -> SeqMap sym (SBit sym) -> SeqMap sym (SBit sym)
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 [] = SBit sym -> SEval sym (SBit sym)
forall (m :: * -> *) a. Monad m => a -> m a
return (sym -> Bool -> SBit sym
forall sym. Backend sym => sym -> Bool -> SBit sym
bitLit sym
sym (Integer
n Integer -> Integer -> Bool
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 (Integer -> Int -> Bool
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 Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
`shiftR` Int
1) [SBit sym]
bs
        sym -> SBit sym -> SBit sym -> SEval sym (SBit sym)
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 SBit sym -> SEval sym (SBit sym)
forall (f :: * -> *) a. Applicative f => a -> f a
pure SBit sym
x else sym -> SBit sym -> SEval sym (SBit sym)
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 :: sym -> [WordValue sym] -> SEval sym (Maybe [SWord sym])
asWordList sym
sym = ([SWord sym] -> [SWord sym])
-> [WordValue sym] -> SEval sym (Maybe [SWord sym])
loop [SWord sym] -> [SWord sym]
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 [] = Maybe [SWord sym] -> SEval sym (Maybe [SWord sym])
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([SWord sym] -> Maybe [SWord sym]
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 ([SWord sym] -> [SWord sym])
-> ([SWord sym] -> [SWord sym]) -> [SWord sym] -> [SWord sym]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (SWord sym
xSWord sym -> [SWord sym] -> [SWord sym]
forall a. a -> [a] -> [a]
:)) [WordValue sym]
vs
   loop [SWord sym] -> [SWord sym]
f (ThunkWordVal Integer
_ SEval sym (WordValue sym)
m : [WordValue sym]
vs) =
     sym
-> SEval sym (WordValue sym) -> SEval sym (Maybe (WordValue sym))
forall sym a.
Backend sym =>
sym -> SEval sym a -> SEval sym (Maybe a)
isReady sym
sym SEval sym (WordValue sym)
m SEval sym (Maybe (WordValue sym))
-> (Maybe (WordValue sym) -> SEval sym (Maybe [SWord sym]))
-> SEval sym (Maybe [SWord sym])
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' WordValue sym -> [WordValue sym] -> [WordValue sym]
forall a. a -> [a] -> [a]
: [WordValue sym]
vs)
       Maybe (WordValue sym)
Nothing -> Maybe [SWord sym] -> SEval sym (Maybe [SWord sym])
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe [SWord sym]
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) =
     sym -> SEval sym (SWord sym) -> SEval sym (Maybe (SWord sym))
forall sym a.
Backend sym =>
sym -> SEval sym a -> SEval sym (Maybe a)
isReady sym
sym SEval sym (SWord sym)
packed SEval sym (Maybe (SWord sym))
-> (Maybe (SWord sym) -> SEval sym (Maybe [SWord sym]))
-> SEval sym (Maybe [SWord sym])
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 ([SWord sym] -> [SWord sym])
-> ([SWord sym] -> [SWord sym]) -> [SWord sym] -> [SWord sym]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (SWord sym
xSWord sym -> [SWord sym] -> [SWord sym]
forall a. a -> [a] -> [a]
:)) [WordValue sym]
vs
       Maybe (SWord sym)
Nothing -> Maybe [SWord sym] -> SEval sym (Maybe [SWord sym])
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe [SWord sym]
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 :: 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)         = (Integer -> SEval sym (SBit sym)) -> SeqMap sym (SBit sym)
forall sym a. (Integer -> SEval sym a) -> SeqMap sym a
indexSeqMap ((Integer -> SEval sym (SBit sym)) -> SeqMap sym (SBit sym))
-> (Integer -> SEval sym (SBit sym)) -> SeqMap sym (SBit sym)
forall a b. (a -> b) -> a -> b
$ \Integer
i -> sym -> SWord sym -> Integer -> SEval sym (SBit sym)
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)  =
  (Integer -> SEval sym (SBit sym)) -> SeqMap sym (SBit sym)
forall sym a. (Integer -> SEval sym a) -> SeqMap sym a
indexSeqMap ((Integer -> SEval sym (SBit sym)) -> SeqMap sym (SBit sym))
-> (Integer -> SEval sym (SBit sym)) -> SeqMap sym (SBit sym)
forall a b. (a -> b) -> a -> b
$ \Integer
i ->
    do SeqMap sym (SBit sym)
mp <- sym -> WordValue sym -> SeqMap sym (SBit sym)
forall sym.
Backend sym =>
sym -> WordValue sym -> SeqMap sym (SBit sym)
asBitsMap sym
sym (WordValue sym -> SeqMap sym (SBit sym))
-> SEval sym (WordValue sym) -> SEval sym (SeqMap sym (SBit sym))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (SEval sym (WordValue sym) -> SEval sym (WordValue sym)
forall sym.
Backend sym =>
SEval sym (WordValue sym) -> SEval sym (WordValue sym)
unwindThunks SEval sym (WordValue sym)
m)
       SeqMap sym (SBit sym) -> Integer -> SEval sym (SBit sym)
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 :: sym -> WordValue sym -> SEval sym [SBit sym]
enumerateWordValue sym
sym (WordVal SWord sym
w) = sym -> SWord sym -> SEval sym [SBit sym]
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) = sym -> WordValue sym -> SEval sym [SBit sym]
forall sym.
Backend sym =>
sym -> WordValue sym -> SEval sym [SBit sym]
enumerateWordValue sym
sym (WordValue sym -> SEval sym [SBit sym])
-> SEval sym (WordValue sym) -> SEval sym [SBit 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) = [SEval sym (SBit sym)] -> SEval sym [SBit sym]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence (Integer -> SeqMap sym (SBit sym) -> [SEval sym (SBit sym)]
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 :: sym -> WordValue sym -> SEval sym [SBit sym]
enumerateWordValueRev sym
sym (WordVal SWord sym
w)  = [SBit sym] -> [SBit sym]
forall a. [a] -> [a]
reverse ([SBit sym] -> [SBit sym])
-> SEval sym [SBit sym] -> SEval sym [SBit sym]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> sym -> SWord sym -> SEval sym [SBit sym]
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)  = sym -> WordValue sym -> SEval sym [SBit sym]
forall sym.
Backend sym =>
sym -> WordValue sym -> SEval sym [SBit sym]
enumerateWordValueRev sym
sym (WordValue sym -> SEval sym [SBit sym])
-> SEval sym (WordValue sym) -> SEval sym [SBit 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) = [SEval sym (SBit sym)] -> SEval sym [SBit sym]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence (Integer -> SeqMap sym (SBit sym) -> [SEval sym (SBit sym)]
forall sym n a.
(Backend sym, Integral n) =>
n -> SeqMap sym a -> [SEval sym a]
enumerateSeqMap Integer
n (Integer -> SeqMap sym (SBit sym) -> SeqMap sym (SBit sym)
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 :: sym -> WordValue sym -> SEval sym [IndexSegment sym]
enumerateIndexSegments sym
_sym (WordVal SWord sym
w) = [IndexSegment sym] -> SEval sym [IndexSegment sym]
forall (f :: * -> *) a. Applicative f => a -> f a
pure [SWord sym -> IndexSegment sym
forall sym. SWord sym -> IndexSegment sym
WordIndexSegment SWord sym
w]
enumerateIndexSegments sym
sym (ThunkWordVal Integer
_ SEval sym (WordValue sym)
m) = sym -> WordValue sym -> SEval sym [IndexSegment sym]
forall sym.
Backend sym =>
sym -> WordValue sym -> SEval sym [IndexSegment sym]
enumerateIndexSegments sym
sym (WordValue sym -> SEval sym [IndexSegment sym])
-> SEval sym (WordValue sym) -> SEval sym [IndexSegment 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) =
  sym -> SEval sym (SWord sym) -> SEval sym (Maybe (SWord sym))
forall sym a.
Backend sym =>
sym -> SEval sym a -> SEval sym (Maybe a)
isReady sym
sym SEval sym (SWord sym)
packed SEval sym (Maybe (SWord sym))
-> (Maybe (SWord sym) -> SEval sym [IndexSegment sym])
-> SEval sym [IndexSegment sym]
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
    Just SWord sym
w  -> [IndexSegment sym] -> SEval sym [IndexSegment sym]
forall (f :: * -> *) a. Applicative f => a -> f a
pure [SWord sym -> IndexSegment sym
forall sym. SWord sym -> IndexSegment sym
WordIndexSegment SWord sym
w]
    Maybe (SWord sym)
Nothing -> (SEval sym (SBit sym) -> SEval sym (IndexSegment sym))
-> [SEval sym (SBit sym)] -> SEval sym [IndexSegment sym]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (SBit sym -> IndexSegment sym
forall sym. SBit sym -> IndexSegment sym
BitIndexSegment (SBit sym -> IndexSegment sym)
-> SEval sym (SBit sym) -> SEval sym (IndexSegment sym)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>) (Integer -> SeqMap sym (SBit sym) -> [SEval sym (SBit sym)]
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 :: sym -> Integer -> [SBit sym] -> Integer -> SEval sym (SBit sym)
bitsValueLessThan sym
sym Integer
_w [] Integer
_n = SBit sym -> SEval sym (SBit sym)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SBit sym -> SEval sym (SBit sym))
-> SBit sym -> SEval sym (SBit sym)
forall a b. (a -> b) -> a -> b
$ sym -> Bool -> SBit sym
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 <- sym -> SBit sym -> SEval sym (SBit sym)
forall sym. Backend sym => sym -> SBit sym -> SEval sym (SBit sym)
bitComplement sym
sym SBit sym
b
         sym -> SBit sym -> SBit sym -> SEval sym (SBit sym)
forall sym.
Backend sym =>
sym -> SBit sym -> SBit sym -> SEval sym (SBit sym)
bitOr sym
sym SBit sym
notb (SBit sym -> SEval sym (SBit sym))
-> SEval sym (SBit sym) -> SEval sym (SBit sym)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< sym -> Integer -> [SBit sym] -> Integer -> SEval sym (SBit sym)
forall sym.
Backend sym =>
sym -> Integer -> [SBit sym] -> Integer -> SEval sym (SBit sym)
bitsValueLessThan sym
sym (Integer
wInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
-Integer
1) [SBit sym]
bs Integer
n
  | Bool
otherwise =
      do SBit sym
notb <- sym -> SBit sym -> SEval sym (SBit sym)
forall sym. Backend sym => sym -> SBit sym -> SEval sym (SBit sym)
bitComplement sym
sym SBit sym
b
         sym -> SBit sym -> SBit sym -> SEval sym (SBit sym)
forall sym.
Backend sym =>
sym -> SBit sym -> SBit sym -> SEval sym (SBit sym)
bitAnd sym
sym SBit sym
notb (SBit sym -> SEval sym (SBit sym))
-> SEval sym (SBit sym) -> SEval sym (SBit sym)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< sym -> Integer -> [SBit sym] -> Integer -> SEval sym (SBit sym)
forall sym.
Backend sym =>
sym -> Integer -> [SBit sym] -> Integer -> SEval sym (SBit sym)
bitsValueLessThan sym
sym (Integer
wInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
-Integer
1) [SBit sym]
bs Integer
n
 where
 nbit :: Bool
nbit = Integer -> Int -> Bool
forall a. Bits a => a -> Int -> Bool
testBit Integer
n (Integer -> Int
forall a. Num a => Integer -> a
fromInteger (Integer
wInteger -> Integer -> Integer
forall 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 :: sym -> Integer -> WordValue sym -> SEval sym ()
assertWordValueInBounds sym
sym Integer
n WordValue sym
idx
  | Integer
n Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= Integer
2Integer -> Integer -> Integer
forall a b. (Num a, Integral b) => a -> b -> a
^(sym -> WordValue sym -> Integer
forall sym. Backend sym => sym -> WordValue sym -> Integer
wordValueSize sym
sym WordValue sym
idx)
  = () -> SEval sym ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()

assertWordValueInBounds sym
sym Integer
n (WordVal SWord sym
idx)
  | Just (Integer
_w,Integer
i) <- sym -> SWord sym -> Maybe (Integer, Integer)
forall sym.
Backend sym =>
sym -> SWord sym -> Maybe (Integer, Integer)
wordAsLit sym
sym SWord sym
idx
  = Bool -> SEval sym () -> SEval sym ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Integer
i Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
n) (sym -> EvalError -> SEval sym ()
forall sym a. Backend sym => sym -> EvalError -> SEval sym a
raiseError sym
sym (Maybe Integer -> EvalError
InvalidIndex (Integer -> Maybe Integer
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' <- sym -> Integer -> Integer -> SEval sym (SWord sym)
forall sym.
Backend sym =>
sym -> Integer -> Integer -> SEval sym (SWord sym)
wordLit sym
sym (sym -> SWord sym -> Integer
forall sym. Backend sym => sym -> SWord sym -> Integer
wordLen sym
sym SWord sym
idx) Integer
n
     SBit sym
p <- sym -> SWord sym -> SWord sym -> SEval sym (SBit sym)
forall sym.
Backend sym =>
sym -> SWord sym -> SWord sym -> SEval sym (SBit sym)
wordLessThan sym
sym SWord sym
idx SWord sym
n'
     sym -> SBit sym -> EvalError -> SEval sym ()
forall sym.
Backend sym =>
sym -> SBit sym -> EvalError -> SEval sym ()
assertSideCondition sym
sym SBit sym
p (Maybe Integer -> EvalError
InvalidIndex Maybe Integer
forall a. Maybe a
Nothing)

-- Force thunks
assertWordValueInBounds sym
sym Integer
n (ThunkWordVal Integer
_ SEval sym (WordValue sym)
m) =
  sym -> Integer -> WordValue sym -> SEval sym ()
forall sym.
Backend sym =>
sym -> Integer -> WordValue sym -> SEval sym ()
assertWordValueInBounds sym
sym Integer
n (WordValue sym -> SEval sym ())
-> SEval sym (WordValue sym) -> SEval sym ()
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) =
  sym -> SEval sym (SWord sym) -> SEval sym (Maybe (SWord sym))
forall sym a.
Backend sym =>
sym -> SEval sym a -> SEval sym (Maybe a)
isReady sym
sym SEval sym (SWord sym)
packed SEval sym (Maybe (SWord sym))
-> (Maybe (SWord sym) -> SEval sym ()) -> SEval sym ()
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
    Just SWord sym
w -> sym -> Integer -> WordValue sym -> SEval sym ()
forall sym.
Backend sym =>
sym -> Integer -> WordValue sym -> SEval sym ()
assertWordValueInBounds sym
sym Integer
n (SWord sym -> WordValue sym
forall sym. SWord sym -> WordValue sym
WordVal SWord sym
w)
    Maybe (SWord sym)
Nothing ->
      do [SBit sym]
bitsList <- [SEval sym (SBit sym)] -> SEval sym [SBit sym]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence (Integer -> SeqMap sym (SBit sym) -> [SEval sym (SBit sym)]
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 <- sym -> Integer -> [SBit sym] -> Integer -> SEval sym (SBit sym)
forall sym.
Backend sym =>
sym -> Integer -> [SBit sym] -> Integer -> SEval sym (SBit sym)
bitsValueLessThan sym
sym Integer
sz [SBit sym]
bitsList Integer
n
         sym -> SBit sym -> EvalError -> SEval sym ()
forall sym.
Backend sym =>
sym -> SBit sym -> EvalError -> SEval sym ()
assertSideCondition sym
sym SBit sym
p (Maybe Integer -> EvalError
InvalidIndex Maybe Integer
forall a. Maybe a
Nothing)

delayWordValue :: Backend sym => sym -> Integer -> SEval sym (WordValue sym) -> SEval sym (WordValue sym)
delayWordValue :: sym
-> Integer
-> SEval sym (WordValue sym)
-> SEval sym (WordValue sym)
delayWordValue sym
sym Integer
sz SEval sym (WordValue sym)
m =
  sym
-> SEval sym (WordValue sym) -> SEval sym (Maybe (WordValue sym))
forall sym a.
Backend sym =>
sym -> SEval sym a -> SEval sym (Maybe a)
isReady sym
sym SEval sym (WordValue sym)
m SEval sym (Maybe (WordValue sym))
-> (Maybe (WordValue sym) -> SEval sym (WordValue sym))
-> SEval sym (WordValue sym)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
    Just WordValue sym
w  -> WordValue sym -> SEval sym (WordValue sym)
forall (f :: * -> *) a. Applicative f => a -> f a
pure WordValue sym
w
    Maybe (WordValue sym)
Nothing -> Integer -> SEval sym (WordValue sym) -> WordValue sym
forall sym. Integer -> SEval sym (WordValue sym) -> WordValue sym
ThunkWordVal Integer
sz (SEval sym (WordValue sym) -> WordValue sym)
-> SEval sym (SEval sym (WordValue sym))
-> SEval sym (WordValue sym)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> sym
-> SEval sym (WordValue sym)
-> SEval sym (SEval sym (WordValue sym))
forall sym a.
Backend sym =>
sym -> SEval sym a -> SEval sym (SEval sym a)
sDelay sym
sym (SEval sym (WordValue sym) -> SEval sym (WordValue 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 :: SEval sym (WordValue sym) -> SEval sym (WordValue sym)
unwindThunks SEval sym (WordValue sym)
m =
  SEval sym (WordValue sym)
m SEval sym (WordValue sym)
-> (WordValue sym -> SEval sym (WordValue sym))
-> SEval sym (WordValue sym)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
    ThunkWordVal Integer
_ SEval sym (WordValue sym)
m' -> SEval sym (WordValue sym) -> SEval sym (WordValue sym)
forall sym.
Backend sym =>
SEval sym (WordValue sym) -> SEval sym (WordValue sym)
unwindThunks SEval sym (WordValue sym)
m'
    WordValue sym
x -> WordValue sym -> SEval sym (WordValue sym)
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 :: 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 ->
      sym
-> SEval sym (WordValue sym) -> SEval sym (Maybe (WordValue sym))
forall sym a.
Backend sym =>
sym -> SEval sym a -> SEval sym (Maybe a)
isReady sym
sym SEval sym (WordValue sym)
wm SEval sym (Maybe (WordValue sym))
-> (Maybe (WordValue sym) -> SEval sym (WordValue sym))
-> SEval sym (WordValue sym)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
        Just WordValue sym
x' -> sym
-> (SWord sym -> SWord sym -> SEval sym (SWord sym))
-> (Integer -> Integer -> Maybe Integer)
-> WordValue sym
-> SInteger sym
-> SEval sym (WordValue sym)
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' <- sym
-> SEval sym (WordValue sym)
-> SEval sym (SEval sym (WordValue sym))
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
                         sym
-> (SWord sym -> SWord sym -> SEval sym (SWord sym))
-> (Integer -> Integer -> Maybe Integer)
-> WordValue sym
-> SInteger sym
-> SEval sym (WordValue sym)
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)
            WordValue sym -> SEval sym (WordValue sym)
forall (m :: * -> *) a. Monad m => a -> m a
return (Integer -> SEval sym (WordValue sym) -> WordValue sym
forall sym. Integer -> SEval sym (WordValue sym) -> WordValue sym
ThunkWordVal Integer
w SEval sym (WordValue sym)
m')

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

    WordVal SWord sym
x' -> SWord sym -> WordValue sym
forall sym. SWord sym -> WordValue sym
WordVal (SWord sym -> WordValue sym)
-> SEval sym (SWord sym) -> SEval sym (WordValue sym)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (SWord sym -> SWord sym -> SEval sym (SWord sym)
wop SWord sym
x' (SWord sym -> SEval sym (SWord sym))
-> SEval sym (SWord sym) -> SEval sym (SWord sym)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< sym -> WordValue sym -> SEval sym (SWord sym)
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 ->
      sym -> SEval sym (SWord sym) -> SEval sym (Maybe (SWord sym))
forall sym a.
Backend sym =>
sym -> SEval sym a -> SEval sym (Maybe a)
isReady sym
sym SEval sym (SWord sym)
packed SEval sym (Maybe (SWord sym))
-> (Maybe (SWord sym) -> SEval sym (WordValue sym))
-> SEval sym (WordValue sym)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
        Just SWord sym
w -> sym
-> (SWord sym -> SWord sym -> SEval sym (SWord sym))
-> (Integer -> Integer -> Maybe Integer)
-> WordValue sym
-> WordValue sym
-> SEval sym (WordValue sym)
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 (SWord sym -> WordValue sym
forall sym. SWord sym -> WordValue sym
WordVal SWord sym
w) WordValue sym
idx
        Maybe (SWord sym)
Nothing ->
          sym
-> Integer -> SeqMap sym (SBit sym) -> SEval sym (WordValue sym)
forall sym.
Backend sym =>
sym
-> Integer -> SeqMap sym (SBit sym) -> SEval sym (WordValue sym)
bitmapWordVal sym
sym Integer
n (SeqMap sym (SBit sym) -> SEval sym (WordValue sym))
-> SEval sym (SeqMap sym (SBit sym)) -> SEval sym (WordValue sym)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<<
            sym
-> (SBit sym -> SBit sym -> SBit sym -> SEval sym (SBit sym))
-> (Integer -> Integer -> Maybe Integer)
-> SEval sym (SBit sym)
-> Nat'
-> SeqMap sym (SBit sym)
-> WordValue sym
-> SEval sym (SeqMap sym (SBit sym))
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 (sym -> SBit sym -> SBit sym -> SBit sym -> SEval sym (SBit sym)
forall sym.
Backend sym =>
sym -> SBit sym -> SBit sym -> SBit sym -> SEval sym (SBit sym)
iteBit sym
sym) Integer -> Integer -> Maybe Integer
reindex (SBit sym -> SEval sym (SBit sym)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (sym -> Bool -> SBit sym
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 :: 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 =
  sym -> WordValue sym -> SEval sym (Maybe Integer)
forall sym.
Backend sym =>
sym -> WordValue sym -> SEval sym (Maybe Integer)
wordValAsLit sym
sym WordValue sym
idx SEval sym (Maybe Integer)
-> (Maybe Integer -> SEval sym (WordValue sym))
-> SEval sym (WordValue sym)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
    Just Integer
j ->
      let sz :: Integer
sz = sym -> WordValue sym -> Integer
forall sym. Backend sym => sym -> WordValue sym -> Integer
wordValueSize sym
sym WordValue sym
w0 in
      case IndexDirection
dir of
        IndexDirection
IndexForward  -> sym
-> WordValue sym
-> Integer
-> SEval sym (SBit sym)
-> SEval sym (WordValue sym)
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 -> sym
-> WordValue sym
-> Integer
-> SEval sym (SBit sym)
-> SEval sym (WordValue sym)
forall sym.
Backend sym =>
sym
-> WordValue sym
-> Integer
-> SEval sym (SBit sym)
-> SEval sym (WordValue sym)
updateWordValue sym
sym WordValue sym
w0 (Integer
sz Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
j Integer -> Integer -> Integer
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) =
     sym
-> SEval sym (WordValue sym) -> SEval sym (Maybe (WordValue sym))
forall sym a.
Backend sym =>
sym -> SEval sym a -> SEval sym (Maybe a)
isReady sym
sym SEval sym (WordValue sym)
m SEval sym (Maybe (WordValue sym))
-> (Maybe (WordValue sym) -> SEval sym (WordValue sym))
-> SEval sym (WordValue sym)
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 -> sym
-> Integer
-> SEval sym (WordValue sym)
-> SEval sym (WordValue sym)
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 (WordValue sym -> SEval sym (WordValue sym))
-> SEval sym (WordValue sym) -> SEval sym (WordValue sym)
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) =
     sym -> SEval sym (SWord sym) -> SEval sym (Maybe (SWord sym))
forall sym a.
Backend sym =>
sym -> SEval sym a -> SEval sym (Maybe a)
isReady sym
sym SEval sym (SWord sym)
packed SEval sym (Maybe (SWord sym))
-> (Maybe (SWord sym) -> SEval sym (WordValue sym))
-> SEval sym (WordValue sym)
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 (SWord sym -> WordValue sym
forall sym. SWord sym -> WordValue sym
WordVal SWord sym
w)
       Maybe (SWord sym)
Nothing ->
         case IndexDirection
dir of
           IndexDirection
IndexForward ->
             sym
-> Integer -> SeqMap sym (SBit sym) -> SEval sym (WordValue sym)
forall sym.
Backend sym =>
sym
-> Integer -> SeqMap sym (SBit sym) -> SEval sym (WordValue sym)
bitmapWordVal sym
sym Integer
sz (SeqMap sym (SBit sym) -> SEval sym (WordValue sym))
-> SeqMap sym (SBit sym) -> SEval sym (WordValue sym)
forall a b. (a -> b) -> a -> b
$ (Integer -> SEval sym (SBit sym)) -> SeqMap sym (SBit sym)
forall sym a. (Integer -> SEval sym a) -> SeqMap sym a
indexSeqMap ((Integer -> SEval sym (SBit sym)) -> SeqMap sym (SBit sym))
-> (Integer -> SEval sym (SBit sym)) -> SeqMap sym (SBit sym)
forall a b. (a -> b) -> a -> b
$ \Integer
i ->
               do SBit sym
b <- sym -> WordValue sym -> Integer -> SEval sym (SBit sym)
forall sym.
Backend sym =>
sym -> WordValue sym -> Integer -> SEval sym (SBit sym)
wordValueEqualsInteger sym
sym WordValue sym
idx Integer
i
                  sym
-> (SBit sym -> SBit sym -> SBit sym -> SEval sym (SBit sym))
-> SBit sym
-> SEval sym (SBit sym)
-> SEval sym (SBit sym)
-> SEval sym (SBit sym)
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 (sym -> SBit sym -> SBit sym -> SBit sym -> SEval sym (SBit 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 (SeqMap sym (SBit sym) -> Integer -> SEval sym (SBit sym)
forall sym a. Backend sym => SeqMap sym a -> Integer -> SEval sym a
lookupSeqMap SeqMap sym (SBit sym)
bs Integer
i)
           IndexDirection
IndexBackward ->
             sym
-> Integer -> SeqMap sym (SBit sym) -> SEval sym (WordValue sym)
forall sym.
Backend sym =>
sym
-> Integer -> SeqMap sym (SBit sym) -> SEval sym (WordValue sym)
bitmapWordVal sym
sym Integer
sz (SeqMap sym (SBit sym) -> SEval sym (WordValue sym))
-> SeqMap sym (SBit sym) -> SEval sym (WordValue sym)
forall a b. (a -> b) -> a -> b
$ (Integer -> SEval sym (SBit sym)) -> SeqMap sym (SBit sym)
forall sym a. (Integer -> SEval sym a) -> SeqMap sym a
indexSeqMap ((Integer -> SEval sym (SBit sym)) -> SeqMap sym (SBit sym))
-> (Integer -> SEval sym (SBit sym)) -> SeqMap sym (SBit sym)
forall a b. (a -> b) -> a -> b
$ \Integer
i ->
               do SBit sym
b <- sym -> WordValue sym -> Integer -> SEval sym (SBit sym)
forall sym.
Backend sym =>
sym -> WordValue sym -> Integer -> SEval sym (SBit sym)
wordValueEqualsInteger sym
sym WordValue sym
idx (Integer
sz Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
i Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
1)
                  sym
-> (SBit sym -> SBit sym -> SBit sym -> SEval sym (SBit sym))
-> SBit sym
-> SEval sym (SBit sym)
-> SEval sym (SBit sym)
-> SEval sym (SBit sym)
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 (sym -> SBit sym -> SBit sym -> SBit sym -> SEval sym (SBit 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 (SeqMap sym (SBit sym) -> Integer -> SEval sym (SBit sym)
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) = SWord sym -> WordValue sym
forall sym. SWord sym -> WordValue sym
WordVal (SWord sym -> WordValue sym)
-> SEval sym (SWord sym) -> SEval sym (WordValue sym)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
      -- TODO, this is too strict in bit
      do let sz :: Integer
sz = sym -> SWord sym -> Integer
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 <- sym -> Integer -> Integer -> SEval sym (SWord sym)
forall sym.
Backend sym =>
sym -> Integer -> Integer -> SEval sym (SWord sym)
wordLit sym
sym Integer
sz (Int -> Integer
forall a. Bits a => Int -> a
bit (Integer -> Int
forall a. Num a => Integer -> a
fromInteger (Integer
szInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
-Integer
1)))
                       sym -> SWord sym -> SWord sym -> SEval sym (SWord sym)
forall sym.
Backend sym =>
sym -> SWord sym -> SWord sym -> SEval sym (SWord sym)
wordShiftRight sym
sym SWord sym
highbit (SWord sym -> SEval sym (SWord sym))
-> SEval sym (SWord sym) -> SEval sym (SWord sym)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< sym -> WordValue sym -> SEval sym (SWord sym)
forall sym.
Backend sym =>
sym -> WordValue sym -> SEval sym (SWord sym)
asWordVal sym
sym WordValue sym
idx
                  IndexDirection
IndexBackward ->
                    do SWord sym
lowbit <- sym -> Integer -> Integer -> SEval sym (SWord sym)
forall sym.
Backend sym =>
sym -> Integer -> Integer -> SEval sym (SWord sym)
wordLit sym
sym Integer
sz Integer
1
                       sym -> SWord sym -> SWord sym -> SEval sym (SWord sym)
forall sym.
Backend sym =>
sym -> SWord sym -> SWord sym -> SEval sym (SWord sym)
wordShiftLeft sym
sym SWord sym
lowbit (SWord sym -> SEval sym (SWord sym))
-> SEval sym (SWord sym) -> SEval sym (SWord sym)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< sym -> WordValue sym -> SEval sym (SWord sym)
forall sym.
Backend sym =>
sym -> WordValue sym -> SEval sym (SWord sym)
asWordVal sym
sym WordValue sym
idx
         case sym -> SBit sym -> Maybe Bool
forall sym. Backend sym => sym -> SBit sym -> Maybe Bool
bitAsLit sym
sym SBit sym
b of
           Just Bool
True  -> sym -> SWord sym -> SWord sym -> SEval sym (SWord sym)
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 -> sym -> SWord sym -> SWord sym -> SEval sym (SWord sym)
forall sym.
Backend sym =>
sym -> SWord sym -> SWord sym -> SEval sym (SWord sym)
wordAnd sym
sym SWord sym
wv (SWord sym -> SEval sym (SWord sym))
-> SEval sym (SWord sym) -> SEval sym (SWord sym)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< sym -> SWord sym -> SEval sym (SWord sym)
forall sym.
Backend sym =>
sym -> SWord sym -> SEval sym (SWord sym)
wordComplement sym
sym SWord sym
msk
           Maybe Bool
Nothing ->
             do SWord sym
zro <- sym -> Integer -> Integer -> SEval sym (SWord sym)
forall sym.
Backend sym =>
sym -> Integer -> Integer -> SEval sym (SWord sym)
wordLit sym
sym Integer
sz Integer
0
                SWord sym
one <- sym -> SWord sym -> SEval sym (SWord sym)
forall sym.
Backend sym =>
sym -> SWord sym -> SEval sym (SWord sym)
wordComplement sym
sym SWord sym
zro
                SWord sym
q   <- sym -> SBit sym -> SWord sym -> SWord sym -> SEval sym (SWord sym)
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'  <- sym -> SWord sym -> SWord sym -> SEval sym (SWord sym)
forall sym.
Backend sym =>
sym -> SWord sym -> SWord sym -> SEval sym (SWord sym)
wordAnd sym
sym SWord sym
wv (SWord sym -> SEval sym (SWord sym))
-> SEval sym (SWord sym) -> SEval sym (SWord sym)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< sym -> SWord sym -> SEval sym (SWord sym)
forall sym.
Backend sym =>
sym -> SWord sym -> SEval sym (SWord sym)
wordComplement sym
sym SWord sym
msk
                sym -> SWord sym -> SWord sym -> SEval sym (SWord sym)
forall sym.
Backend sym =>
sym -> SWord sym -> SWord sym -> SEval sym (SWord sym)
wordXor sym
sym SWord sym
w' (SWord sym -> SEval sym (SWord sym))
-> SEval sym (SWord sym) -> SEval sym (SWord sym)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< sym -> SWord sym -> SWord sym -> SEval sym (SWord sym)
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 :: 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 =
  sym -> WordValue sym -> SEval sym (Maybe Integer)
forall sym.
Backend sym =>
sym -> WordValue sym -> SEval sym (Maybe Integer)
wordValAsLit sym
sym WordValue sym
idx SEval sym (Maybe Integer)
-> (Maybe Integer -> SEval sym (SeqMap sym a))
-> SEval sym (SeqMap sym a)
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 <- sym -> WordValue sym -> SEval sym [IndexSegment sym]
forall sym.
Backend sym =>
sym -> WordValue sym -> SEval sym [IndexSegment sym]
enumerateIndexSegments sym
sym WordValue sym
idx
         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)
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 = sym -> WordValue sym -> Integer
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 =
     SeqMap sym a -> SEval sym (SeqMap sym a)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SeqMap sym a -> SEval sym (SeqMap sym a))
-> SeqMap sym a -> SEval sym (SeqMap sym a)
forall a b. (a -> b) -> a -> b
$ (Integer -> SEval sym a) -> SeqMap sym a
forall sym a. (Integer -> SEval sym a) -> SeqMap sym a
indexSeqMap ((Integer -> SEval sym a) -> SeqMap sym a)
-> (Integer -> SEval sym a) -> SeqMap sym a
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' -> SeqMap sym a -> Integer -> SEval sym a
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 :: sym -> WordValue sym -> Integer
wordValueSize sym
sym (WordVal SWord sym
w)  = sym -> SWord sym -> Integer
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 :: 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 ; sym -> WordValue sym -> Integer -> SEval sym (SBit sym)
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 Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
<= Integer
idx Bool -> Bool -> Bool
&& Integer
idx Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< sym -> SWord sym -> Integer
forall sym. Backend sym => sym -> SWord sym -> Integer
wordLen sym
sym SWord sym
w = sym -> SWord sym -> Integer -> SEval sym (SBit sym)
forall sym.
Backend sym =>
sym -> SWord sym -> Integer -> SEval sym (SBit sym)
wordBit sym
sym SWord sym
w Integer
idx
   | Bool
otherwise = sym -> Integer -> SEval sym (SBit sym)
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 Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
<= Integer
idx Bool -> Bool -> Bool
&& Integer
idx Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
n = SeqMap sym (SBit sym) -> Integer -> SEval sym (SBit sym)
forall sym a. Backend sym => SeqMap sym a -> Integer -> SEval sym a
lookupSeqMap SeqMap sym (SBit sym)
xs Integer
idx
   | Bool
otherwise = sym -> Integer -> SEval sym (SBit sym)
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 :: 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) =
      sym
-> SEval sym (WordValue sym) -> SEval sym (Maybe (WordValue sym))
forall sym a.
Backend sym =>
sym -> SEval sym a -> SEval sym (Maybe a)
isReady sym
sym SEval sym (WordValue sym)
m SEval sym (Maybe (WordValue sym))
-> (Maybe (WordValue sym) -> SEval sym (WordValue sym))
-> SEval sym (WordValue sym)
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 -> sym
-> Integer
-> SEval sym (WordValue sym)
-> SEval sym (WordValue sym)
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 (WordValue sym -> SEval sym (WordValue sym))
-> SEval sym (WordValue sym) -> SEval sym (WordValue sym)
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 Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
0 Bool -> Bool -> Bool
|| Integer
idx Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= sym -> SWord sym -> Integer
forall sym. Backend sym => sym -> SWord sym -> Integer
wordLen sym
sym SWord sym
w = sym -> Integer -> SEval sym (WordValue sym)
forall sym a. Backend sym => sym -> Integer -> SEval sym a
invalidIndex sym
sym Integer
idx
      | Bool
otherwise =
          sym -> SEval sym (SBit sym) -> SEval sym (Maybe (SBit sym))
forall sym a.
Backend sym =>
sym -> SEval sym a -> SEval sym (Maybe a)
isReady sym
sym SEval sym (SBit sym)
b SEval sym (Maybe (SBit sym))
-> (Maybe (SBit sym) -> SEval sym (WordValue sym))
-> SEval sym (WordValue sym)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
            Just SBit sym
b' -> SWord sym -> WordValue sym
forall sym. SWord sym -> WordValue sym
WordVal (SWord sym -> WordValue sym)
-> SEval sym (SWord sym) -> SEval sym (WordValue sym)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> sym -> SWord sym -> Integer -> SBit sym -> SEval sym (SWord sym)
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 = sym -> SWord sym -> SeqMap sym (SBit sym)
forall sym.
Backend sym =>
sym -> SWord sym -> SeqMap sym (SBit sym)
unpackBitmap sym
sym SWord sym
w
                 sym
-> Integer -> SeqMap sym (SBit sym) -> SEval sym (WordValue sym)
forall sym.
Backend sym =>
sym
-> Integer -> SeqMap sym (SBit sym) -> SEval sym (WordValue sym)
bitmapWordVal sym
sym (sym -> SWord sym -> Integer
forall sym. Backend sym => sym -> SWord sym -> Integer
wordLen sym
sym SWord sym
w) (SeqMap sym (SBit sym) -> SEval sym (WordValue sym))
-> SeqMap sym (SBit sym) -> SEval sym (WordValue sym)
forall a b. (a -> b) -> a -> b
$ SeqMap sym (SBit sym)
-> Integer -> SEval sym (SBit sym) -> SeqMap sym (SBit sym)
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 Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
<= Integer
idx Bool -> Bool -> Bool
&& Integer
idx Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
sz =
          sym -> SEval sym (SWord sym) -> SEval sym (Maybe (SWord sym))
forall sym a.
Backend sym =>
sym -> SEval sym a -> SEval sym (Maybe a)
isReady sym
sym SEval sym (SWord sym)
packed SEval sym (Maybe (SWord sym))
-> (Maybe (SWord sym) -> SEval sym (WordValue sym))
-> SEval sym (WordValue sym)
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 (SWord sym -> WordValue sym
forall sym. SWord sym -> WordValue sym
WordVal SWord sym
w)
            Maybe (SWord sym)
Nothing -> sym
-> Integer -> SeqMap sym (SBit sym) -> SEval sym (WordValue sym)
forall sym.
Backend sym =>
sym
-> Integer -> SeqMap sym (SBit sym) -> SEval sym (WordValue sym)
bitmapWordVal sym
sym Integer
sz (SeqMap sym (SBit sym) -> SEval sym (WordValue sym))
-> SeqMap sym (SBit sym) -> SEval sym (WordValue sym)
forall a b. (a -> b) -> a -> b
$ SeqMap sym (SBit sym)
-> Integer -> SEval sym (SBit sym) -> SeqMap sym (SBit sym)
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 = sym -> Integer -> SEval sym (WordValue sym)
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 :: 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) =
  sym
-> SBit sym
-> SEval sym (WordValue sym)
-> SEval sym (WordValue sym)
-> SEval sym (WordValue sym)
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) -> SEval sym (WordValue sym)
forall sym.
Backend sym =>
SEval sym (WordValue sym) -> SEval sym (WordValue sym)
unwindThunks SEval sym (WordValue sym)
m1) (SEval sym (WordValue sym) -> SEval sym (WordValue sym)
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 =
  sym
-> SBit sym
-> SEval sym (WordValue sym)
-> SEval sym (WordValue sym)
-> SEval sym (WordValue sym)
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) -> SEval sym (WordValue sym)
forall sym.
Backend sym =>
SEval sym (WordValue sym) -> SEval sym (WordValue sym)
unwindThunks SEval sym (WordValue sym)
m1) (WordValue sym -> SEval sym (WordValue sym)
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) =
  sym
-> SBit sym
-> SEval sym (WordValue sym)
-> SEval sym (WordValue sym)
-> SEval sym (WordValue sym)
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 (WordValue sym -> SEval sym (WordValue sym)
forall (f :: * -> *) a. Applicative f => a -> f a
pure WordValue sym
w1) (SEval sym (WordValue sym) -> SEval sym (WordValue sym)
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) =
  SWord sym -> WordValue sym
forall sym. SWord sym -> WordValue sym
WordVal (SWord sym -> WordValue sym)
-> SEval sym (SWord sym) -> SEval sym (WordValue sym)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> sym -> SBit sym -> SWord sym -> SWord sym -> SEval sym (SWord sym)
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) =
  sym -> SEval sym (SWord sym) -> SEval sym (Maybe (SWord sym))
forall sym a.
Backend sym =>
sym -> SEval sym a -> SEval sym (Maybe a)
isReady sym
sym SEval sym (SWord sym)
packed1 SEval sym (Maybe (SWord sym))
-> (Maybe (SWord sym) -> SEval sym (WordValue sym))
-> SEval sym (WordValue sym)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
    Just SWord sym
w1 -> SWord sym -> WordValue sym
forall sym. SWord sym -> WordValue sym
WordVal (SWord sym -> WordValue sym)
-> SEval sym (SWord sym) -> SEval sym (WordValue sym)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> sym -> SBit sym -> SWord sym -> SWord sym -> SEval sym (SWord sym)
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 -> sym
-> SBit sym
-> Integer
-> SeqMap sym (SBit sym)
-> SeqMap sym (SBit sym)
-> SEval sym (WordValue 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 (sym -> SWord sym -> SeqMap sym (SBit sym)
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) =
  sym -> SEval sym (SWord sym) -> SEval sym (Maybe (SWord sym))
forall sym a.
Backend sym =>
sym -> SEval sym a -> SEval sym (Maybe a)
isReady sym
sym SEval sym (SWord sym)
packed2 SEval sym (Maybe (SWord sym))
-> (Maybe (SWord sym) -> SEval sym (WordValue sym))
-> SEval sym (WordValue sym)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
    Just SWord sym
w2 -> SWord sym -> WordValue sym
forall sym. SWord sym -> WordValue sym
WordVal (SWord sym -> WordValue sym)
-> SEval sym (SWord sym) -> SEval sym (WordValue sym)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> sym -> SBit sym -> SWord sym -> SWord sym -> SEval sym (SWord sym)
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 -> sym
-> SBit sym
-> Integer
-> SeqMap sym (SBit sym)
-> SeqMap sym (SBit sym)
-> SEval sym (WordValue 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
n2 (sym -> SWord sym -> SeqMap sym (SBit sym)
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 <- sym -> SEval sym (SWord sym) -> SEval sym (Maybe (SWord sym))
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 <- sym -> SEval sym (SWord sym) -> SEval sym (Maybe (SWord sym))
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) -> SWord sym -> WordValue sym
forall sym. SWord sym -> WordValue sym
WordVal (SWord sym -> WordValue sym)
-> SEval sym (SWord sym) -> SEval sym (WordValue sym)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> sym -> SBit sym -> SWord sym -> SWord sym -> SEval sym (SWord sym)
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))
_ -> sym
-> SBit sym
-> Integer
-> SeqMap sym (SBit sym)
-> SeqMap sym (SBit sym)
-> SEval sym (WordValue 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 :: 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 <- sym
-> Nat'
-> SeqMap sym (SBit sym)
-> SEval sym (SeqMap sym (SBit sym))
forall sym a.
Backend sym =>
sym -> Nat' -> SeqMap sym a -> SEval sym (SeqMap sym a)
memoMap sym
sym (Integer -> Nat'
Nat Integer
sz) (sym
-> (SBit sym -> SBit sym -> SBit sym -> SEval sym (SBit sym))
-> SBit sym
-> SeqMap sym (SBit sym)
-> SeqMap sym (SBit sym)
-> SeqMap sym (SBit sym)
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 (sym -> SBit sym -> SBit sym -> SBit sym -> SEval sym (SBit 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)
     sym
-> Integer -> SeqMap sym (SBit sym) -> SEval sym (WordValue sym)
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' :: 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 <- sym -> SBit sym -> Maybe Bool
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 = sym
-> (SBit sym
    -> WordValue sym -> WordValue sym -> SEval sym (WordValue sym))
-> SBit sym
-> SEval sym (WordValue sym)
-> SEval sym (WordValue sym)
-> SEval sym (WordValue sym)
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 (sym
-> SBit sym
-> WordValue sym
-> WordValue sym
-> SEval sym (WordValue 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