WordValue.hs

-- |
-- 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
  , wordValWidth
  , 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 Data.Proxy(Proxy(..))
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 (WordVal w)  = seq w (return ())
forceWordValue (ThunkWordVal _ m)  = forceWordValue =<< m
forceWordValue (BitmapVal _n packed _) = do w <- packed; seq w (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 = bit 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 (Generic)

wordValWidth :: forall sym. Backend sym => WordValue sym -> Integer
wordValWidth val =
  case val of
    ThunkWordVal n _ -> n
    WordVal sv -> wordLen' (Proxy :: Proxy sym) sv
    BitmapVal n _ _ -> n
{-# INLINE wordValWidth #-}

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

packBitmap :: Backend sym => sym -> Integer -> SeqMap sym (SBit sym) -> SEval sym (SWord sym)
packBitmap sym sz bs = packWord sym =<< sequence (enumerateSeqMap sz bs)

unpackBitmap :: Backend sym => sym -> SWord sym -> SeqMap sym (SBit sym)
unpackBitmap sym w = indexSeqMap $ \i -> wordBit sym w i

bitmapWordVal :: Backend sym => sym -> Integer -> SeqMap sym (SBit sym) -> SEval sym (WordValue sym)
bitmapWordVal sym sz bs =
  do packed <- sDelay sym (packBitmap sym sz bs)
     pure (BitmapVal sz packed bs)

{-# INLINE joinWordVal #-}
joinWordVal :: Backend sym => sym -> WordValue sym -> WordValue sym -> SEval sym (WordValue sym)
joinWordVal sym wv1 wv2 =
  let fallback = fallbackWordJoin sym wv1 wv2 in
  case (wv1, wv2) of
    (WordVal w1, WordVal w2) ->
      WordVal <$> joinWord sym w1 w2

    (ThunkWordVal _ m1, _) ->
      isReady sym m1 >>= \case
        Just x -> joinWordVal sym x wv2
        Nothing -> fallback

    (_,ThunkWordVal _ m2) ->
      isReady sym m2 >>= \case
        Just x   -> joinWordVal sym wv1 x
        Nothing  -> fallback

    (WordVal w1, BitmapVal _ packed2 _) ->
      isReady sym packed2 >>= \case
        Just w2 -> WordVal <$> joinWord sym w1 w2
        Nothing  -> fallback

    (BitmapVal _ packed1 _, WordVal w2) ->
      isReady sym packed1 >>= \case
        Just w1 -> WordVal <$> joinWord sym w1 w2
        Nothing -> fallback

    (BitmapVal _ packed1 _, BitmapVal _ packed2 _) ->
      do r1 <- isReady sym packed1
         r2 <- isReady sym packed2
         case (r1,r2) of
           (Just w1, Just w2) -> WordVal <$> joinWord sym w1 w2
           _ -> fallback

{-# INLINE fallbackWordJoin #-}
fallbackWordJoin :: Backend sym => sym -> WordValue sym -> WordValue sym -> SEval sym (WordValue sym)
fallbackWordJoin sym w1 w2 =
  do let n1 = wordValueSize sym w1
     let n2 = wordValueSize sym w2
     let len = n1 + n2
     packed <- sDelay sym
                 (do a <- asWordVal sym w1
                     b <- asWordVal sym w2
                     joinWord sym a b)
     let bs = concatSeqMap n1 (asBitsMap sym w1) (asBitsMap sym w2)
     pure (BitmapVal len packed bs)


{-# INLINE takeWordVal #-}
takeWordVal ::
  Backend sym =>
  sym ->
  Integer ->
  Integer ->
  WordValue sym ->
  SEval sym (WordValue sym)
takeWordVal sym leftWidth rigthWidth (WordVal w) =
  do (lw, _rw) <- splitWord sym leftWidth rigthWidth w
     pure (WordVal lw)

takeWordVal sym leftWidth rightWidth (ThunkWordVal _ m) =
  isReady sym m >>= \case
    Just w -> takeWordVal sym leftWidth rightWidth w
    Nothing ->
      do m' <- sDelay sym (takeWordVal sym leftWidth rightWidth =<< m)
         return (ThunkWordVal leftWidth m')

takeWordVal sym leftWidth rightWidth (BitmapVal _n packed xs) =
  isReady sym packed >>= \case
    Just w -> do (lw, _rw) <- splitWord sym leftWidth rightWidth w
                 pure (WordVal lw)
    Nothing -> bitmapWordVal sym leftWidth xs

{-# INLINE dropWordVal #-}
dropWordVal ::
  Backend sym =>
  sym ->
  Integer ->
  Integer ->
  WordValue sym ->
  SEval sym (WordValue sym)
dropWordVal sym leftWidth rigthWidth (WordVal w) =
  do (_lw, rw) <- splitWord sym leftWidth rigthWidth w
     pure (WordVal rw)

dropWordVal sym leftWidth rightWidth (ThunkWordVal _ m) =
  isReady sym m >>= \case
    Just w -> dropWordVal sym leftWidth rightWidth w
    Nothing ->
      do m' <- sDelay sym (dropWordVal sym leftWidth rightWidth =<< m)
         return (ThunkWordVal rightWidth m')

dropWordVal sym leftWidth rightWidth (BitmapVal _n packed xs) =
  isReady sym packed >>= \case
    Just w -> do (_lw, rw) <- splitWord sym leftWidth rightWidth w
                 pure (WordVal rw)
    Nothing ->
      do let rxs = dropSeqMap leftWidth xs
         bitmapWordVal sym rightWidth 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 len start (WordVal w) =
   WordVal <$> extractWord sym len start w
extractWordVal sym len start (ThunkWordVal _n m) =
  isReady sym m >>= \case
    Just w -> extractWordVal sym len start w
    Nothing ->
      do m' <- sDelay sym (extractWordVal sym len start =<< m)
         pure (ThunkWordVal len m')
extractWordVal sym len start (BitmapVal n packed xs) =
  isReady sym packed >>= \case
    Just w -> WordVal <$> extractWord sym len start w
    Nothing ->
      do let xs' = dropSeqMap (n - start - len) xs
         bitmapWordVal sym len 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 _ wop (WordVal w1) (WordVal w2) = WordVal <$> wop w1 w2

wordValLogicOp sym bop wop (WordVal w1) (BitmapVal n2 packed2 bs2) =
  isReady sym packed2 >>= \case
    Just w2 -> WordVal <$> wop w1 w2
    Nothing -> bitmapWordVal sym n2 =<< zipSeqMap sym bop (Nat n2) (unpackBitmap sym w1) bs2

wordValLogicOp sym bop wop (BitmapVal n1 packed1 bs1) (WordVal w2) =
  isReady sym packed1 >>= \case
    Just w1 -> WordVal <$> wop w1 w2
    Nothing -> bitmapWordVal sym n1 =<< zipSeqMap sym bop (Nat n1) bs1 (unpackBitmap sym w2)

wordValLogicOp sym bop wop (BitmapVal n1 packed1 bs1) (BitmapVal _n2 packed2 bs2) =
  do r1 <- isReady sym packed1
     r2 <- isReady sym packed2
     case (r1,r2) of
       (Just w1, Just w2) -> WordVal <$> wop w1 w2
       _ -> bitmapWordVal sym n1 =<< zipSeqMap sym bop (Nat n1) bs1 bs2

wordValLogicOp sym bop wop (ThunkWordVal _ m1) w2 =
  do w1 <- m1
     wordValLogicOp sym bop wop w1 w2

wordValLogicOp sym bop wop w1 (ThunkWordVal _ m2) =
  do w2 <- m2
     wordValLogicOp sym bop wop w1 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 _ _ wop (WordVal w)  = WordVal <$> wop w
wordValUnaryOp sym bop wop (ThunkWordVal _ m) = wordValUnaryOp sym bop wop =<< m
wordValUnaryOp sym bop wop (BitmapVal n packed xs) =
  isReady sym packed >>= \case
    Just w  -> WordVal <$> wop w
    Nothing -> bitmapWordVal sym n =<< mapSeqMap sym bop (Nat n) 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 nParts nEach xs | nParts * nEach < largeBitSize =
  do z <- wordLit sym 0 0
     loop (wordVal z) (enumerateSeqMap nParts xs)

 where
 loop :: WordValue sym -> [SEval sym (WordValue sym)] -> SEval sym (WordValue sym)
 loop !wv [] = pure wv
 loop !wv (w : ws) =
    do w'  <- delayWordValue sym nEach w
       wv' <- joinWordVal sym wv w'
       loop wv' ws

-- too large to pack
joinWords sym nParts nEach xs = bitmapWordVal sym (nParts * nEach) zs
  where
    zs = indexSeqMap $ \i ->
            do let (q,r) = divMod i nEach
               ys <- lookupSeqMap xs q
               indexWordValue sym ys r

reverseWordVal :: Backend sym => sym -> WordValue sym -> SEval sym (WordValue sym)
reverseWordVal sym w =
  let m = wordValueSize sym w in
  bitmapWordVal sym m <$> reverseSeqMap m $ asBitsMap sym w

wordValAsLit :: Backend sym => sym -> WordValue sym -> SEval sym (Maybe Integer)
wordValAsLit sym (WordVal w) = pure (snd <$> wordAsLit sym w)
wordValAsLit sym (ThunkWordVal _ m) =
  isReady sym m >>= \case
    Just v  -> wordValAsLit sym v
    Nothing -> pure Nothing
wordValAsLit sym (BitmapVal _ packed _) =
  isReady sym packed >>= \case
    Just w  -> pure (snd <$> wordAsLit sym w)
    Nothing -> pure Nothing

-- | Force a word value into packed word form
asWordVal :: Backend sym => sym -> WordValue sym -> SEval sym (SWord sym)
asWordVal _   (WordVal w)            = return w
asWordVal sym (ThunkWordVal _ m)     = asWordVal sym =<< m
asWordVal _   (BitmapVal _ packed _) = packed

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

 where
   loop (ThunkWordVal _ m) = loop =<< m
   loop (WordVal w) = wordEq sym w =<< wordLit sym (wordLen sym w) i
   loop (BitmapVal n packed bs) =
     isReady sym packed >>= \case
       Just w  -> loop (WordVal w)
       Nothing -> bitsAre i =<< sequence (enumerateSeqMap n (reverseSeqMap n bs))

   -- NB little-endian sequence of bits
   bitsAre :: Integer -> [SBit sym] -> SEval sym (SBit sym)
   bitsAre !n [] = return (bitLit sym (n == 0))
   bitsAre !n (b:bs) =
     do pb  <- bitIs (testBit n 0) b
        pbs <- bitsAre (n `shiftR` 1) bs
        bitAnd sym pb pbs

   bitIs :: Bool -> SBit sym -> SEval sym (SBit sym)
   bitIs b x = if b then pure x else bitComplement sym x

asWordList :: forall sym. Backend sym => sym -> [WordValue sym] -> SEval sym (Maybe [SWord sym])
asWordList sym = loop id
 where
   loop :: ([SWord sym] -> [SWord sym]) -> [WordValue sym] -> SEval sym (Maybe [SWord sym])
   loop f [] = pure (Just (f []))
   loop f (WordVal x : vs) = loop (f . (x:)) vs
   loop f (ThunkWordVal _ m : vs) =
     isReady sym m >>= \case
       Just m' -> loop f (m' : vs)
       Nothing -> pure Nothing
   loop f (BitmapVal _ packed _ : vs) =
     isReady sym packed >>= \case
       Just x -> loop (f . (x:)) vs
       Nothing -> pure Nothing

-- | Force a word value into a sequence of bits
asBitsMap :: Backend sym => sym -> WordValue sym -> SeqMap sym (SBit sym)
asBitsMap _   (BitmapVal _ _ xs)  = xs
asBitsMap sym (WordVal w)         = indexSeqMap $ \i -> wordBit sym w i
asBitsMap sym (ThunkWordVal _ m)  =
  indexSeqMap $ \i ->
    do mp <- asBitsMap sym <$> (unwindThunks m)
       lookupSeqMap mp 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 (WordVal w) = unpackWord sym w
enumerateWordValue sym (ThunkWordVal _ m) = enumerateWordValue sym =<< m
  -- TODO? used the packed value if it is ready?
enumerateWordValue _ (BitmapVal n _ xs) = sequence (enumerateSeqMap n 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 (WordVal w)  = reverse <$> unpackWord sym w
enumerateWordValueRev sym (ThunkWordVal _ m)  = enumerateWordValueRev sym =<< m
  -- TODO? used the packed value if it is ready?
enumerateWordValueRev _   (BitmapVal n _ xs) = sequence (enumerateSeqMap n (reverseSeqMap n xs))


enumerateIndexSegments :: Backend sym => sym -> WordValue sym -> SEval sym [IndexSegment sym]
enumerateIndexSegments _sym (WordVal w) = pure [WordIndexSegment w]
enumerateIndexSegments sym (ThunkWordVal _ m) = enumerateIndexSegments sym =<< m
enumerateIndexSegments sym (BitmapVal n packed xs) =
  isReady sym packed >>= \case
    Just w  -> pure [WordIndexSegment w]
    Nothing -> traverse (BitIndexSegment <$>) (enumerateSeqMap n 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 _w [] _n = pure $ bitLit sym False
bitsValueLessThan sym w (b:bs) n
  | nbit =
      do notb <- bitComplement sym b
         bitOr sym notb =<< bitsValueLessThan sym (w-1) bs n
  | otherwise =
      do notb <- bitComplement sym b
         bitAnd sym notb =<< bitsValueLessThan sym (w-1) bs n
 where
 nbit = testBit n (fromInteger (w-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 n idx
  | n >= 2^(wordValueSize sym idx)
  = return ()

assertWordValueInBounds sym n (WordVal idx)
  | Just (_w,i) <- wordAsLit sym idx
  = unless (i < n) (raiseError sym (InvalidIndex (Just 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 n (WordVal idx) =
  do n' <- wordLit sym (wordLen sym idx) n
     p <- wordLessThan sym idx n'
     assertSideCondition sym p (InvalidIndex Nothing)

-- Force thunks
assertWordValueInBounds sym n (ThunkWordVal _ m) =
  assertWordValueInBounds sym n =<< m

-- If the index is an unpacked word, force all the bits
-- and compute the unsigned less-than test directly.
assertWordValueInBounds sym n (BitmapVal sz packed bits) =
  isReady sym packed >>= \case
    Just w -> assertWordValueInBounds sym n (WordVal w)
    Nothing ->
      do bitsList <- sequence (enumerateSeqMap sz bits)
         p <- bitsValueLessThan sym sz bitsList n
         assertSideCondition sym p (InvalidIndex Nothing)

delayWordValue :: Backend sym => sym -> Integer -> SEval sym (WordValue sym) -> SEval sym (WordValue sym)
delayWordValue sym sz m =
  isReady sym m >>= \case
    Just w  -> pure w
    Nothing -> ThunkWordVal sz <$> sDelay sym (unwindThunks 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 m =
  m >>= \case
    ThunkWordVal _ m' -> unwindThunks m'
    x -> pure 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 wop reindex x idx =
  case x of
    ThunkWordVal w wm ->
      isReady sym wm >>= \case
        Just x' -> shiftWordByInteger sym wop reindex x' idx
        Nothing ->
         do m' <- sDelay sym
                     (do x' <- wm
                         shiftWordByInteger sym wop reindex x' idx)
            return (ThunkWordVal w m')

    WordVal x' -> WordVal <$> (wop x' =<< wordFromInt sym (wordLen sym x') idx)

    BitmapVal n packed bs0 ->
      isReady sym packed >>= \case
        Just w -> shiftWordByInteger sym wop reindex (WordVal w) idx
        Nothing ->
          bitmapWordVal sym n =<<
            shiftSeqByInteger sym (iteBit sym) reindex (pure (bitLit sym False)) (Nat n) bs0 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 wop reindex x idx =
  case x of
    ThunkWordVal w wm ->
      isReady sym wm >>= \case
        Just wm' -> shiftWordByWord sym wop reindex wm' idx
        Nothing ->
         do m' <- sDelay sym (do wm' <- wm
                                 shiftWordByWord sym wop reindex wm' idx)
            return (ThunkWordVal w m')

    WordVal x' -> WordVal <$> (wop x' =<< asWordVal sym idx)

    BitmapVal n packed bs0 ->
      isReady sym packed >>= \case
        Just w -> shiftWordByWord sym wop reindex (WordVal w) idx
        Nothing ->
          bitmapWordVal sym n =<<
            shiftSeqByWord sym (iteBit sym) reindex (pure (bitLit sym False)) (Nat n) bs0 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 dir w0 idx bitval =
  wordValAsLit sym idx >>= \case
    Just j ->
      let sz = wordValueSize sym w0 in
      case dir of
        IndexForward  -> updateWordValue sym w0 j bitval
        IndexBackward -> updateWordValue sym w0 (sz - j - 1) bitval
    Nothing -> loop w0

 where
   loop (ThunkWordVal sz m) =
     isReady sym m >>= \case
       Just w' -> loop w'
       Nothing -> delayWordValue sym sz (loop =<< m)

   loop (BitmapVal sz packed bs) =
     isReady sym packed >>= \case
       Just w -> loop (WordVal w)
       Nothing ->
         case dir of
           IndexForward ->
             bitmapWordVal sym sz $ indexSeqMap $ \i ->
               do b <- wordValueEqualsInteger sym idx i
                  mergeEval sym (iteBit sym) b bitval (lookupSeqMap bs i)
           IndexBackward ->
             bitmapWordVal sym sz $ indexSeqMap $ \i ->
               do b <- wordValueEqualsInteger sym idx (sz - i - 1)
                  mergeEval sym (iteBit sym) b bitval (lookupSeqMap bs i)

   loop (WordVal wv) = WordVal <$>
      -- TODO, this is too strict in bit
      do let sz = wordLen sym wv
         b <- bitval
         msk <- case dir of
                  IndexForward ->
                    do highbit <- wordLit sym sz (bit (fromInteger (sz-1)))
                       wordShiftRight sym highbit =<< asWordVal sym idx
                  IndexBackward ->
                    do lowbit <- wordLit sym sz 1
                       wordShiftLeft sym lowbit =<< asWordVal sym idx
         case bitAsLit sym b of
           Just True  -> wordOr  sym wv msk
           Just False -> wordAnd sym wv =<< wordComplement sym msk
           Nothing ->
             do zro <- wordLit sym sz 0
                one <- wordComplement sym zro
                q   <- iteWord sym b one zro
                w'  <- wordAnd sym wv =<< wordComplement sym msk
                wordXor sym w' =<< wordAnd sym msk 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 merge reindex zro sz xs idx =
  wordValAsLit sym idx >>= \case
    Just j -> shiftOp xs j
    Nothing ->
      do idx_segs <- enumerateIndexSegments sym idx
         barrelShifter sym merge shiftOp sz xs idx_bits idx_segs
  where
   idx_bits = wordValueSize sym idx

   shiftOp vs shft =
     pure $ indexSeqMap $ \i ->
       case reindex i shft of
         Nothing -> zro
         Just i' -> lookupSeqMap vs 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 (WordVal w)  = wordLen sym w
wordValueSize _ (ThunkWordVal n _) = n
wordValueSize _ (BitmapVal n _ _) = n

-- | Select an individual bit from a word value
indexWordValue :: Backend sym => sym -> WordValue sym -> Integer -> SEval sym (SBit sym)
indexWordValue sym (ThunkWordVal _ m) idx = do m' <- m ; indexWordValue sym m' idx
indexWordValue sym (WordVal w) idx
   | 0 <= idx && idx < wordLen sym w = wordBit sym w idx
   | otherwise = invalidIndex sym idx
indexWordValue sym (BitmapVal n _packed xs) idx
   | 0 <= idx && idx < n = lookupSeqMap xs idx
   | otherwise = invalidIndex sym 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 wv0 idx b = loop wv0
  where
    loop (ThunkWordVal sz m) =
      isReady sym m >>= \case
        Just w  -> loop w
        Nothing -> delayWordValue sym sz (loop =<< m)

    loop (WordVal w)
      | idx < 0 || idx >= wordLen sym w = invalidIndex sym idx
      | otherwise =
          isReady sym b >>= \case
            Just b' -> WordVal <$> wordUpdate sym w idx b'
            Nothing ->
              do let bs = unpackBitmap sym w
                 bitmapWordVal sym (wordLen sym w) $ updateSeqMap bs idx b

    loop (BitmapVal sz packed bs)
      | 0 <= idx && idx < sz =
          isReady sym packed >>= \case
            Just w  -> loop (WordVal w)
            Nothing -> bitmapWordVal sym sz $ updateSeqMap bs idx b
      | otherwise = invalidIndex sym idx

{-# INLINE mergeWord #-}
mergeWord :: Backend sym =>
  sym ->
  SBit sym ->
  WordValue sym ->
  WordValue sym ->
  SEval sym (WordValue sym)
mergeWord sym c (ThunkWordVal _ m1) (ThunkWordVal _ m2) =
  mergeWord' sym c (unwindThunks m1) (unwindThunks m2)
mergeWord sym c (ThunkWordVal _ m1) w2 =
  mergeWord' sym c (unwindThunks m1) (pure w2)
mergeWord sym c w1 (ThunkWordVal _ m2) =
  mergeWord' sym c (pure w1) (unwindThunks m2)

mergeWord sym c (WordVal w1) (WordVal w2) =
  WordVal <$> iteWord sym c w1 w2

mergeWord sym c (BitmapVal n1 packed1 bs1) (WordVal w2) =
  isReady sym packed1 >>= \case
    Just w1 -> WordVal <$> iteWord sym c w1 w2
    Nothing -> mergeBitmaps sym c n1 bs1 (unpackBitmap sym w2)

mergeWord sym c (WordVal w1) (BitmapVal n2 packed2 bs2) =
  isReady sym packed2 >>= \case
    Just w2 -> WordVal <$> iteWord sym c w1 w2
    Nothing -> mergeBitmaps sym c n2 (unpackBitmap sym w1) bs2

mergeWord sym c (BitmapVal n1 packed1 bs1) (BitmapVal _n2 packed2 bs2) =
  do r1 <- isReady sym packed1
     r2 <- isReady sym packed2
     case (r1,r2) of
       (Just w1, Just w2) -> WordVal <$> iteWord sym c w1 w2
       _ -> mergeBitmaps sym c n1 bs1 bs2

mergeBitmaps :: Backend sym =>
  sym ->
  SBit sym ->
  Integer ->
  SeqMap sym (SBit sym) ->
  SeqMap sym (SBit sym) ->
  SEval sym (WordValue sym)
mergeBitmaps sym c sz bs1 bs2 =
  do bs <- memoMap sym (Nat sz) (mergeSeqMap sym (iteBit sym) c bs1 bs2)
     bitmapWordVal sym sz bs

{-# INLINE mergeWord' #-}
mergeWord' :: Backend sym =>
  sym ->
  SBit sym ->
  SEval sym (WordValue sym) ->
  SEval sym (WordValue sym) ->
  SEval sym (WordValue sym)
mergeWord' sym c x y
  | Just b <- bitAsLit sym c = if b then x else y
  | otherwise = mergeEval sym (mergeWord sym) c x y