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

    {-# LANGUAGE BangPatterns #-}
    {-# LANGUAGE DeriveGeneric #-}
    {-# LANGUAGE DoAndIfThenElse #-}
    {-# LANGUAGE FlexibleInstances #-}
    {-# LANGUAGE FlexibleContexts #-}
    {-# LANGUAGE ImplicitParams #-}
    {-# LANGUAGE LambdaCase #-}
    {-# LANGUAGE MultiParamTypeClasses #-}
    {-# LANGUAGE PatternGuards #-}
    {-# LANGUAGE ScopedTypeVariables #-}
    {-# LANGUAGE StandaloneDeriving #-}
    {-# LANGUAGE TupleSections #-}
    {-# LANGUAGE TypeFamilies #-}
    {-# LANGUAGE ViewPatterns #-}

    module Cryptol.Backend.WordValue
      ( -- * WordValue
        WordValue
      , wordVal
      , bitmapWordVal
      , asWordList
      , asWordVal
      , asBitsMap
      , joinWordVal
      , takeWordVal
      , dropWordVal
      , extractWordVal
      , wordValLogicOp
      , wordValUnaryOp
      , assertWordValueInBounds
      , enumerateWordValue
      , enumerateWordValueRev
      , enumerateIndexSegments
      , wordValueSize
      , indexWordValue
      , updateWordValue
      , delayWordValue
      , joinWords
      , shiftSeqByWord
      , shiftWordByInteger
      , shiftWordByWord
      , wordValAsLit
      , reverseWordVal
      , forceWordValue
      , wordValueEqualsInteger
      , updateWordByWord

      , mergeWord
      , mergeWord'
      ) where

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

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

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

    -- | Force the evaluation of a word value
    forceWordValue :: Backend sym => WordValue sym -> SEval sym ()
    forceWordValue :: forall sym. Backend sym => WordValue sym -> SEval sym ()
    forceWordValue (WordVal SWord sym
    w)  = SWord sym -> SEval sym () -> SEval sym ()
    forall a b. a -> b -> b
    seq SWord sym
    w (() -> SEval sym ()
    forall a. a -> SEval sym a
    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 ()
    forall a b. a -> b -> b
    seq SWord sym
    w (() -> SEval sym ()
    forall a. a -> SEval sym a
    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
    $cfrom :: forall sym x. WordValue sym -> Rep (WordValue sym) x
    from :: forall x. WordValue sym -> Rep (WordValue sym) x
    $cto :: forall sym x. Rep (WordValue sym) x -> WordValue sym
    to :: forall x. Rep (WordValue sym) x -> WordValue sym
    Generic)

    wordVal :: SWord sym -> WordValue sym
    wordVal :: forall sym. 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 :: forall sym.
    Backend sym =>
    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)
    forall (m :: * -> *) a. Monad m => [m a] -> m [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 :: forall sym.
    Backend sym =>
    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 :: forall sym.
    Backend sym =>
    sym
    -> Integer -> SeqMap sym (SBit sym) -> SEval sym (WordValue sym)
    bitmapWordVal sym
    sym Integer
    sz SeqMap sym (SBit sym)
    bs =
      do SEval sym (SWord sym)
    packed <- 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 a. a -> SEval sym a
    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 :: forall sym.
    Backend sym =>
    sym -> WordValue sym -> WordValue sym -> SEval sym (WordValue sym)
    joinWordVal sym
    sym WordValue sym
    wv1 WordValue sym
    wv2 =
      let fallback :: SEval sym (WordValue sym)
    fallback = 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 a. sym -> SEval sym a -> SEval sym (Maybe a)
    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 a b. SEval sym a -> (a -> SEval sym b) -> SEval sym b
    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 a. sym -> SEval sym a -> SEval sym (Maybe a)
    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 a b. SEval sym a -> (a -> SEval sym b) -> SEval sym b
    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 a. sym -> SEval sym a -> SEval sym (Maybe a)
    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 a b. SEval sym a -> (a -> SEval sym b) -> SEval sym b
    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 a. sym -> SEval sym a -> SEval sym (Maybe a)
    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 a b. SEval sym a -> (a -> SEval sym b) -> SEval sym b
    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 a. sym -> SEval sym a -> SEval sym (Maybe a)
    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 a. sym -> SEval sym a -> SEval sym (Maybe a)
    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 :: forall sym.
    Backend sym =>
    sym -> WordValue sym -> WordValue sym -> SEval sym (WordValue sym)
    fallbackWordJoin sym
    sym WordValue sym
    w1 WordValue sym
    w2 =
      do let n1 :: Integer
    n1 = 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 a. a -> SEval sym a
    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 :: forall sym.
    Backend sym =>
    sym
    -> Integer -> Integer -> WordValue sym -> SEval sym (WordValue sym)
    takeWordVal sym
    sym Integer
    leftWidth Integer
    rigthWidth (WordVal SWord sym
    w) =
      do (SWord sym
    lw, SWord sym
    _rw) <- 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 a. a -> SEval sym a
    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 a. sym -> SEval sym a -> SEval sym (Maybe a)
    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 a b. SEval sym a -> (a -> SEval sym b) -> SEval sym b
    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 a. a -> SEval sym a
    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 a. sym -> SEval sym a -> SEval sym (Maybe a)
    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 a b. SEval sym a -> (a -> SEval sym b) -> SEval sym b
    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 a. a -> SEval sym a
    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 :: forall sym.
    Backend sym =>
    sym
    -> Integer -> Integer -> WordValue sym -> SEval sym (WordValue sym)
    dropWordVal sym
    sym Integer
    leftWidth Integer
    rigthWidth (WordVal SWord sym
    w) =
      do (SWord sym
    _lw, SWord sym
    rw) <- 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 a. a -> SEval sym a
    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 a. sym -> SEval sym a -> SEval sym (Maybe a)
    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 a b. SEval sym a -> (a -> SEval sym b) -> SEval sym b
    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 a. a -> SEval sym a
    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 a. sym -> SEval sym a -> SEval sym (Maybe a)
    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 a b. SEval sym a -> (a -> SEval sym b) -> SEval sym b
    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 a. a -> SEval sym a
    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 :: forall sym.
    Backend sym =>
    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 a. sym -> SEval sym a -> SEval sym (Maybe a)
    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 a b. SEval sym a -> (a -> SEval sym b) -> SEval sym b
    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 a. a -> SEval sym a
    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 a. sym -> SEval sym a -> SEval sym (Maybe a)
    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 a b. SEval sym a -> (a -> SEval sym b) -> SEval sym b
    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 :: forall sym.
    Backend sym =>
    sym
    -> (SBit sym -> SBit sym -> SEval sym (SBit sym))
    -> (SWord sym -> SWord sym -> SEval sym (SWord sym))
    -> WordValue sym
    -> WordValue sym
    -> SEval sym (WordValue sym)
    wordValLogicOp sym
    _sym SBit sym -> SBit sym -> SEval sym (SBit sym)
    _ SWord sym -> SWord sym -> SEval sym (SWord sym)
    wop (WordVal SWord sym
    w1) (WordVal SWord sym
    w2) = 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 a. sym -> SEval sym a -> SEval sym (Maybe a)
    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 a b. SEval sym a -> (a -> SEval sym b) -> SEval sym b
    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 a. sym -> SEval sym a -> SEval sym (Maybe a)
    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 a b. SEval sym a -> (a -> SEval sym b) -> SEval sym b
    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 a. sym -> SEval sym a -> SEval sym (Maybe a)
    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 a. sym -> SEval sym a -> SEval sym (Maybe a)
    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 :: forall sym.
    Backend sym =>
    sym
    -> (SBit sym -> SEval sym (SBit sym))
    -> (SWord sym -> SEval sym (SWord sym))
    -> WordValue sym
    -> SEval sym (WordValue sym)
    wordValUnaryOp sym
    _ SBit sym -> SEval sym (SBit sym)
    _ SWord sym -> SEval sym (SWord sym)
    wop (WordVal SWord sym
    w)  = 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 a. sym -> SEval sym a -> SEval sym (Maybe a)
    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 a b. SEval sym a -> (a -> SEval sym b) -> SEval sym b
    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 :: forall sym.
    Backend sym =>
    sym
    -> Integer
    -> Integer
    -> SeqMap sym (WordValue sym)
    -> SEval sym (WordValue sym)
    joinWords sym
    sym Integer
    nParts Integer
    nEach SeqMap sym (WordValue sym)
    xs | Integer
    nParts 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 a. a -> SEval sym a
    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 :: forall sym.
    Backend sym =>
    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 :: forall sym.
    Backend sym =>
    sym -> WordValue sym -> SEval sym (Maybe Integer)
    wordValAsLit sym
    sym (WordVal SWord sym
    w) = Maybe Integer -> SEval sym (Maybe Integer)
    forall a. a -> SEval sym a
    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 a. sym -> SEval sym a -> SEval sym (Maybe a)
    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 a b. SEval sym a -> (a -> SEval sym b) -> SEval sym b
    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 a. a -> SEval sym a
    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 a. sym -> SEval sym a -> SEval sym (Maybe a)
    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 a b. SEval sym a -> (a -> SEval sym b) -> SEval sym b
    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 a. a -> SEval sym a
    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 a. a -> SEval sym a
    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 :: forall sym.
    Backend sym =>
    sym -> WordValue sym -> SEval sym (SWord sym)
    asWordVal sym
    _   (WordVal SWord sym
    w)            = SWord sym -> SEval sym (SWord sym)
    forall a. a -> SEval sym a
    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 :: forall sym.
    Backend sym =>
    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 a. a -> SEval sym a
    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 a. sym -> SEval sym a -> SEval sym (Maybe a)
    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 a b. SEval sym a -> (a -> SEval sym b) -> SEval sym b
    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)
    forall (m :: * -> *) a. Monad m => [m a] -> m [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 a. a -> SEval sym a
    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 a. a -> SEval sym a
    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 :: forall sym.
    Backend sym =>
    sym -> [WordValue sym] -> SEval sym (Maybe [SWord sym])
    asWordList sym
    sym = ([SWord sym] -> [SWord sym])
    -> [WordValue sym] -> SEval sym (Maybe [SWord sym])
    loop [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 a. a -> SEval sym a
    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 a. sym -> SEval sym a -> SEval sym (Maybe a)
    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 a b. SEval sym a -> (a -> SEval sym b) -> SEval sym b
    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 a. a -> SEval sym a
    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 a. sym -> SEval sym a -> SEval sym (Maybe a)
    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 a b. SEval sym a -> (a -> SEval sym b) -> SEval sym b
    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 a. a -> SEval sym a
    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 :: forall sym.
    Backend sym =>
    sym -> WordValue sym -> SeqMap sym (SBit sym)
    asBitsMap sym
    _   (BitmapVal Integer
    _ SEval sym (SWord sym)
    _ SeqMap sym (SBit sym)
    xs)  = SeqMap sym (SBit sym)
    xs
    asBitsMap sym
    sym (WordVal SWord sym
    w)         = (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 :: forall sym.
    Backend sym =>
    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)
    forall (m :: * -> *) a. Monad m => [m a] -> m [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 :: forall sym.
    Backend sym =>
    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)
    forall (m :: * -> *) a. Monad m => [m a] -> m [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 :: forall sym.
    Backend sym =>
    sym -> WordValue sym -> SEval sym [IndexSegment sym]
    enumerateIndexSegments sym
    _sym (WordVal SWord sym
    w) = [IndexSegment sym] -> SEval sym [IndexSegment sym]
    forall a. a -> SEval sym a
    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 a. sym -> SEval sym a -> SEval sym (Maybe a)
    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 a b. SEval sym a -> (a -> SEval sym b) -> SEval sym b
    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 a. a -> SEval sym a
    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)
    forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> [a] -> f [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 :: forall sym.
    Backend sym =>
    sym -> Integer -> [SBit sym] -> Integer -> SEval sym (SBit sym)
    bitsValueLessThan sym
    sym Integer
    _w [] Integer
    _n = SBit sym -> SEval sym (SBit sym)
    forall a. a -> SEval sym a
    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 :: forall sym.
    Backend sym =>
    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 a. a -> SEval sym a
    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 a. sym -> EvalError -> SEval sym a
    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 a. sym -> SEval sym a -> SEval sym (Maybe a)
    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 a b. SEval sym a -> (a -> SEval sym b) -> SEval sym b
    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)
    forall (m :: * -> *) a. Monad m => [m a] -> m [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 :: forall sym.
    Backend sym =>
    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 a. sym -> SEval sym a -> SEval sym (Maybe a)
    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 a b. SEval sym a -> (a -> SEval sym b) -> SEval sym b
    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 a. a -> SEval sym a
    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 :: forall sym.
    Backend sym =>
    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 a b. SEval sym a -> (a -> SEval sym b) -> SEval sym b
    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 a. a -> SEval sym a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure WordValue sym
    x

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

    shiftWordByInteger :: forall sym.
    Backend sym =>
    sym
    -> (SWord sym -> SWord sym -> SEval sym (SWord sym))
    -> (Integer -> Integer -> Maybe Integer)
    -> WordValue sym
    -> SInteger sym
    -> SEval sym (WordValue sym)
    shiftWordByInteger sym
    sym SWord sym -> SWord sym -> SEval sym (SWord sym)
    wop Integer -> Integer -> Maybe Integer
    reindex WordValue sym
    x SInteger sym
    idx =
      case WordValue sym
    x of
        ThunkWordVal Integer
    w SEval sym (WordValue sym)
    wm ->
          sym
    -> SEval sym (WordValue sym) -> SEval sym (Maybe (WordValue sym))
    forall a. sym -> SEval sym a -> SEval sym (Maybe a)
    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 a b. SEval sym a -> (a -> SEval sym b) -> SEval sym b
    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 a. a -> SEval sym a
    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 a. sym -> SEval sym a -> SEval sym (Maybe a)
    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 a b. SEval sym a -> (a -> SEval sym b) -> SEval sym b
    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 a. a -> SEval sym a
    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 :: forall sym.
    Backend sym =>
    sym
    -> (SWord sym -> SWord sym -> SEval sym (SWord sym))
    -> (Integer -> Integer -> Maybe Integer)
    -> WordValue sym
    -> WordValue sym
    -> SEval sym (WordValue sym)
    shiftWordByWord sym
    sym SWord sym -> SWord sym -> SEval sym (SWord sym)
    wop Integer -> Integer -> Maybe Integer
    reindex WordValue sym
    x WordValue sym
    idx =
      case WordValue sym
    x of
        ThunkWordVal Integer
    w SEval sym (WordValue sym)
    wm ->
          sym
    -> SEval sym (WordValue sym) -> SEval sym (Maybe (WordValue sym))
    forall a. sym -> SEval sym a -> SEval sym (Maybe a)
    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 a b. SEval sym a -> (a -> SEval sym b) -> SEval sym b
    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 a. a -> SEval sym a
    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 a. sym -> SEval sym a -> SEval sym (Maybe a)
    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 a b. SEval sym a -> (a -> SEval sym b) -> SEval sym b
    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 a. a -> SEval sym a
    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 :: forall sym.
    Backend sym =>
    sym
    -> IndexDirection
    -> WordValue sym
    -> WordValue sym
    -> SEval sym (SBit sym)
    -> SEval sym (WordValue sym)
    updateWordByWord sym
    sym IndexDirection
    dir WordValue sym
    w0 WordValue sym
    idx SEval sym (SBit sym)
    bitval =
      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 a b. SEval sym a -> (a -> SEval sym b) -> SEval sym b
    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 a. sym -> SEval sym a -> SEval sym (Maybe a)
    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 a b. SEval sym a -> (a -> SEval sym b) -> SEval sym b
    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 a. sym -> SEval sym a -> SEval sym (Maybe a)
    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 a b. SEval sym a -> (a -> SEval sym b) -> SEval sym b
    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 a.
    sym
    -> (SBit sym -> a -> a -> SEval sym a)
    -> SBit sym
    -> SEval sym a
    -> SEval sym a
    -> SEval sym a
    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 a.
    sym
    -> (SBit sym -> a -> a -> SEval sym a)
    -> SBit sym
    -> SEval sym a
    -> SEval sym a
    -> SEval sym a
    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 :: forall sym a.
    Backend sym =>
    sym
    -> (SBit sym -> a -> a -> SEval sym a)
    -> (Integer -> Integer -> Maybe Integer)
    -> SEval sym a
    -> Nat'
    -> SeqMap sym a
    -> WordValue sym
    -> SEval sym (SeqMap sym a)
    shiftSeqByWord sym
    sym SBit sym -> a -> a -> SEval sym a
    merge Integer -> Integer -> Maybe Integer
    reindex SEval sym a
    zro Nat'
    sz SeqMap sym a
    xs WordValue sym
    idx =
      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 a b. SEval sym a -> (a -> SEval sym b) -> SEval sym b
    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 a. a -> SEval 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 :: forall sym. Backend sym => 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 :: forall sym.
    Backend sym =>
    sym -> WordValue sym -> Integer -> SEval sym (SBit sym)
    indexWordValue sym
    sym (ThunkWordVal Integer
    _ SEval sym (WordValue sym)
    m) Integer
    idx = do WordValue sym
    m' <- SEval sym (WordValue sym)
    m ; 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 :: forall sym.
    Backend sym =>
    sym
    -> WordValue sym
    -> Integer
    -> SEval sym (SBit sym)
    -> SEval sym (WordValue sym)
    updateWordValue sym
    sym WordValue sym
    wv0 Integer
    idx SEval sym (SBit sym)
    b = WordValue sym -> SEval sym (WordValue sym)
    loop WordValue sym
    wv0
      where
        loop :: WordValue sym -> SEval sym (WordValue sym)
    loop (ThunkWordVal Integer
    sz SEval sym (WordValue sym)
    m) =
          sym
    -> SEval sym (WordValue sym) -> SEval sym (Maybe (WordValue sym))
    forall a. sym -> SEval sym a -> SEval sym (Maybe a)
    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 a b. SEval sym a -> (a -> SEval sym b) -> SEval sym b
    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 a. sym -> SEval sym a -> SEval sym (Maybe a)
    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 a b. SEval sym a -> (a -> SEval sym b) -> SEval sym b
    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 a. sym -> SEval sym a -> SEval sym (Maybe a)
    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 a b. SEval sym a -> (a -> SEval sym b) -> SEval sym b
    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 :: forall sym.
    Backend sym =>
    sym
    -> SBit sym
    -> WordValue sym
    -> WordValue sym
    -> SEval sym (WordValue sym)
    mergeWord sym
    sym SBit sym
    c (ThunkWordVal Integer
    _ SEval sym (WordValue sym)
    m1) (ThunkWordVal Integer
    _ SEval sym (WordValue sym)
    m2) =
      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 a. a -> SEval sym a
    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 a. a -> SEval sym a
    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 a. sym -> SEval sym a -> SEval sym (Maybe a)
    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 a b. SEval sym a -> (a -> SEval sym b) -> SEval sym b
    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 a. sym -> SEval sym a -> SEval sym (Maybe a)
    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 a b. SEval sym a -> (a -> SEval sym b) -> SEval sym b
    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 a. sym -> SEval sym a -> SEval sym (Maybe a)
    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 a. sym -> SEval sym a -> SEval sym (Maybe a)
    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 :: forall sym.
    Backend sym =>
    sym
    -> SBit sym
    -> Integer
    -> SeqMap sym (SBit sym)
    -> SeqMap sym (SBit sym)
    -> SEval sym (WordValue sym)
    mergeBitmaps sym
    sym SBit sym
    c Integer
    sz SeqMap sym (SBit sym)
    bs1 SeqMap sym (SBit sym)
    bs2 =
      do SeqMap sym (SBit sym)
    bs <- 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' :: forall sym.
    Backend sym =>
    sym
    -> SBit sym
    -> SEval sym (WordValue sym)
    -> SEval sym (WordValue sym)
    -> SEval sym (WordValue sym)
    mergeWord' sym
    sym SBit sym
    c SEval sym (WordValue sym)
    x SEval sym (WordValue sym)
    y
      | Just Bool
    b <- 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 a.
    sym
    -> (SBit sym -> a -> a -> SEval sym a)
    -> SBit sym
    -> SEval sym a
    -> SEval sym a
    -> SEval sym a
    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