diff --git a/cryptol.cabal b/cryptol.cabal
index 1414b127..bbad094c 100644
--- a/cryptol.cabal
+++ b/cryptol.cabal
@@ -164,6 +164,7 @@ library
                        Cryptol.Backend.Concrete,
                        Cryptol.Backend.FloatHelpers,
                        Cryptol.Backend.Monad,
+                       Cryptol.Backend.SeqMap,
                        Cryptol.Backend.SBV,
                        Cryptol.Backend.What4,
 
diff --git a/src/Cryptol/Backend/SeqMap.hs b/src/Cryptol/Backend/SeqMap.hs
new file mode 100644
index 00000000..26e482a2
--- /dev/null
+++ b/src/Cryptol/Backend/SeqMap.hs
@@ -0,0 +1,163 @@
+-- |
+-- Module      :  Cryptol.Backend.SeqMap
+-- Copyright   :  (c) 2013-2021 Galois, Inc.
+-- License     :  BSD3
+-- Maintainer  :  cryptol@galois.com
+-- Stability   :  provisional
+-- Portability :  portable
+
+{-# LANGUAGE DeriveAnyClass #-}
+{-# LANGUAGE DeriveFunctor #-}
+{-# LANGUAGE DeriveGeneric #-}
+{-# LANGUAGE DoAndIfThenElse #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE ImplicitParams #-}
+{-# LANGUAGE LambdaCase #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE PatternGuards #-}
+{-# LANGUAGE Safe #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE StandaloneDeriving #-}
+{-# LANGUAGE TupleSections #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE ViewPatterns #-}
+
+module Cryptol.Backend.SeqMap 
+  ( -- * Sequence Maps
+    SeqMap (..)
+  , lookupSeqMap
+  , finiteSeqMap
+  , infiniteSeqMap
+  , enumerateSeqMap
+  , streamSeqMap
+  , reverseSeqMap
+  , updateSeqMap
+  , dropSeqMap
+  , concatSeqMap
+  , splitSeqMap
+  , memoMap
+  , zipSeqMap
+  , mapSeqMap
+  ) where
+
+import Control.Monad
+import Control.Monad.IO.Class
+import Data.List
+import Data.IORef
+import Data.Map.Strict (Map)
+import qualified Data.Map.Strict as Map
+
+import Cryptol.Backend
+import Cryptol.Utils.Panic(panic)
+
+-- | A sequence map represents a mapping from nonnegative integer indices
+--   to values.  These are used to represent both finite and infinite sequences.
+data SeqMap sym a
+  = IndexSeqMap  !(Integer -> SEval sym a)
+  | UpdateSeqMap !(Map Integer (SEval sym a))
+                 !(Integer -> SEval sym a)
+
+lookupSeqMap :: SeqMap sym a -> Integer -> SEval sym a
+lookupSeqMap (IndexSeqMap f) i = f i
+lookupSeqMap (UpdateSeqMap m f) i =
+  case Map.lookup i m of
+    Just x  -> x
+    Nothing -> f i
+
+
+-- | Generate a finite sequence map from a list of values
+finiteSeqMap :: [SEval sym a] -> SeqMap sym a
+finiteSeqMap xs =
+   UpdateSeqMap
+      (Map.fromList (zip [0..] xs))
+      (\i -> panic "finiteSeqMap" ["Out of bounds access of finite seq map", "length: " ++ show (length xs), show i])
+
+-- | Generate an infinite sequence map from a stream of values
+infiniteSeqMap :: Backend sym => sym -> [SEval sym a] -> SEval sym (SeqMap sym a)
+infiniteSeqMap sym xs =
+   -- TODO: use an int-trie?
+   memoMap sym (IndexSeqMap $ \i -> genericIndex xs i)
+
+-- | Create a finite list of length @n@ of the values from @[0..n-1]@ in
+--   the given the sequence emap.
+enumerateSeqMap :: (Integral n) => n -> SeqMap sym a -> [SEval sym a]
+enumerateSeqMap n m = [ lookupSeqMap m  i | i <- [0 .. (toInteger n)-1] ]
+
+-- | Create an infinite stream of all the values in a sequence map
+streamSeqMap :: SeqMap sym a -> [SEval sym a]
+streamSeqMap m = [ lookupSeqMap m i | i <- [0..] ]
+
+-- | Reverse the order of a finite sequence map
+reverseSeqMap :: Integer     -- ^ Size of the sequence map
+              -> SeqMap sym a
+              -> SeqMap sym a
+reverseSeqMap n vals = IndexSeqMap $ \i -> lookupSeqMap vals (n - 1 - i)
+
+updateSeqMap :: SeqMap sym a -> Integer -> SEval sym a -> SeqMap sym a
+updateSeqMap (UpdateSeqMap m sm) i x = UpdateSeqMap (Map.insert i x m) sm
+updateSeqMap (IndexSeqMap f) i x = UpdateSeqMap (Map.singleton i x) f
+
+-- | Concatenate the first @n@ values of the first sequence map onto the
+--   beginning of the second sequence map.
+concatSeqMap :: Integer -> SeqMap sym a -> SeqMap sym a -> SeqMap sym a
+concatSeqMap n x y =
+    IndexSeqMap $ \i ->
+       if i < n
+         then lookupSeqMap x i
+         else lookupSeqMap y (i-n)
+
+-- | Given a number @n@ and a sequence map, return two new sequence maps:
+--   the first containing the values from @[0..n-1]@ and the next containing
+--   the values from @n@ onward.
+splitSeqMap :: Integer -> SeqMap sym a -> (SeqMap sym a, SeqMap sym a)
+splitSeqMap n xs = (hd,tl)
+  where
+  hd = xs
+  tl = IndexSeqMap $ \i -> lookupSeqMap xs (i+n)
+
+-- | Drop the first @n@ elements of the given 'SeqMap'.
+dropSeqMap :: Integer -> SeqMap sym a -> SeqMap sym a
+dropSeqMap 0 xs = xs
+dropSeqMap n xs = IndexSeqMap $ \i -> lookupSeqMap xs (i+n)
+
+-- | Given a sequence map, return a new sequence map that is memoized using
+--   a finite map memo table.
+memoMap :: Backend sym => sym -> SeqMap sym a -> SEval sym (SeqMap sym a)
+memoMap sym x = do
+  stk <- sGetCallStack sym
+  cache <- liftIO $ newIORef $ Map.empty
+  return $ IndexSeqMap (memo cache stk)
+
+  where
+  memo cache stk i = do
+    mz <- liftIO (Map.lookup i <$> readIORef cache)
+    case mz of
+      Just z  -> return z
+      Nothing -> sWithCallStack sym stk (doEval cache i)
+
+  doEval cache i = do
+    v <- lookupSeqMap x i
+    liftIO $ atomicModifyIORef' cache (\m -> (Map.insert i v m, ()))
+    return v
+
+-- | Apply the given evaluation function pointwise to the two given
+--   sequence maps.
+zipSeqMap ::
+  Backend sym =>
+  sym ->
+  (a -> a -> SEval sym a) ->
+  SeqMap sym a ->
+  SeqMap sym a ->
+  SEval sym (SeqMap sym a)
+zipSeqMap sym f x y =
+  memoMap sym (IndexSeqMap $ \i -> join (f <$> lookupSeqMap x i <*> lookupSeqMap y i))
+
+-- | Apply the given function to each value in the given sequence map
+mapSeqMap ::
+  Backend sym =>
+  sym ->
+  (a -> SEval sym a) ->
+  SeqMap sym a -> SEval sym (SeqMap sym a)
+mapSeqMap sym f x =
+  memoMap sym (IndexSeqMap $ \i -> f =<< lookupSeqMap x i)
diff --git a/src/Cryptol/Eval/Concrete.hs b/src/Cryptol/Eval/Concrete.hs
index 963f693c..14904949 100644
--- a/src/Cryptol/Eval/Concrete.hs
+++ b/src/Cryptol/Eval/Concrete.hs
@@ -466,7 +466,7 @@ sshrV =
 logicShift :: (Integer -> Integer -> Integer -> Integer)
               -- ^ The function may assume its arguments are masked.
               -- It is responsible for masking its result if needed.
-           -> (Nat' -> TValue -> SeqMap Concrete -> Integer -> SeqMap Concrete)
+           -> (Nat' -> TValue -> SeqMap Concrete (GenValue Concrete) -> Integer -> SeqMap Concrete (GenValue Concrete))
            -> Prim Concrete
 logicShift opW opS =
   PNumPoly \a ->
@@ -513,7 +513,7 @@ signedShiftRW w ival by
      else
        shiftR (signedValue w ival) (fromInteger by')
 
-shiftLS :: Nat' -> TValue -> SeqMap Concrete -> Integer -> SeqMap Concrete
+shiftLS :: Nat' -> TValue -> SeqMap Concrete (GenValue Concrete) -> Integer -> SeqMap Concrete (GenValue Concrete)
 shiftLS w ety vs by
   | by < 0 = shiftRS w ety vs (negate by)
 
@@ -525,7 +525,7 @@ shiftLS w ety vs by = IndexSeqMap $ \i ->
       | otherwise  -> evalPanic "shiftLS" ["Index out of bounds"]
     Inf            -> lookupSeqMap vs (i+by)
 
-shiftRS :: Nat' -> TValue -> SeqMap Concrete -> Integer -> SeqMap Concrete
+shiftRS :: Nat' -> TValue -> SeqMap Concrete (GenValue Concrete) -> Integer -> SeqMap Concrete (GenValue Concrete)
 shiftRS w ety vs by
   | by < 0 = shiftLS w ety vs (negate by)
 
@@ -546,7 +546,7 @@ rotateLW 0 i _  = i
 rotateLW w i by = mask w $ (i `shiftL` b) .|. (i `shiftR` (fromInteger w - b))
   where b = fromInteger (by `mod` w)
 
-rotateLS :: Nat' -> TValue -> SeqMap Concrete -> Integer -> SeqMap Concrete
+rotateLS :: Nat' -> TValue -> SeqMap Concrete (GenValue Concrete) -> Integer -> SeqMap Concrete (GenValue Concrete)
 rotateLS w _ vs by = IndexSeqMap $ \i ->
   case w of
     Nat len -> lookupSeqMap vs ((by + i) `mod` len)
@@ -558,7 +558,7 @@ rotateRW 0 i _  = i
 rotateRW w i by = mask w $ (i `shiftR` b) .|. (i `shiftL` (fromInteger w - b))
   where b = fromInteger (by `mod` w)
 
-rotateRS :: Nat' -> TValue -> SeqMap Concrete -> Integer -> SeqMap Concrete
+rotateRS :: Nat' -> TValue -> SeqMap Concrete (GenValue Concrete) -> Integer -> SeqMap Concrete (GenValue Concrete)
 rotateRS w _ vs by = IndexSeqMap $ \i ->
   case w of
     Nat len -> lookupSeqMap vs ((len - by + i) `mod` len)
@@ -567,22 +567,22 @@ rotateRS w _ vs by = IndexSeqMap $ \i ->
 
 -- Sequence Primitives ---------------------------------------------------------
 
-indexFront :: Nat' -> TValue -> SeqMap Concrete -> TValue -> BV -> Eval Value
+indexFront :: Nat' -> TValue -> SeqMap Concrete (GenValue Concrete) -> TValue -> BV -> Eval Value
 indexFront _mblen _a vs _ix (bvVal -> ix) = lookupSeqMap vs ix
 
-indexFront_bits :: Nat' -> TValue -> SeqMap Concrete -> TValue -> [Bool] -> Eval Value
+indexFront_bits :: Nat' -> TValue -> SeqMap Concrete (GenValue Concrete) -> TValue -> [Bool] -> Eval Value
 indexFront_bits mblen a vs ix bs = indexFront mblen a vs ix =<< packWord Concrete bs
 
-indexFront_int :: Nat' -> TValue -> SeqMap Concrete -> TValue -> Integer -> Eval Value
+indexFront_int :: Nat' -> TValue -> SeqMap Concrete (GenValue Concrete) -> TValue -> Integer -> Eval Value
 indexFront_int _mblen _a vs _ix idx = lookupSeqMap vs idx
 
-indexBack :: Nat' -> TValue -> SeqMap Concrete -> TValue -> BV -> Eval Value
+indexBack :: Nat' -> TValue -> SeqMap Concrete (GenValue Concrete) -> TValue -> BV -> Eval Value
 indexBack mblen a vs ix (bvVal -> idx) = indexBack_int mblen a vs ix idx
 
-indexBack_bits :: Nat' -> TValue -> SeqMap Concrete -> TValue -> [Bool] -> Eval Value
+indexBack_bits :: Nat' -> TValue -> SeqMap Concrete (GenValue Concrete) -> TValue -> [Bool] -> Eval Value
 indexBack_bits mblen a vs ix bs = indexBack mblen a vs ix =<< packWord Concrete bs
 
-indexBack_int :: Nat' -> TValue -> SeqMap Concrete -> TValue -> Integer -> Eval Value
+indexBack_int :: Nat' -> TValue -> SeqMap Concrete (GenValue Concrete) -> TValue -> Integer -> Eval Value
 indexBack_int mblen _a vs _ix idx =
   case mblen of
     Nat len -> lookupSeqMap vs (len - idx - 1)
@@ -591,10 +591,10 @@ indexBack_int mblen _a vs _ix idx =
 updateFront ::
   Nat'               {- ^ length of the sequence -} ->
   TValue             {- ^ type of values in the sequence -} ->
-  SeqMap Concrete    {- ^ sequence to update -} ->
+  SeqMap Concrete (GenValue Concrete) {- ^ sequence to update -} ->
   Either Integer (WordValue Concrete) {- ^ index -} ->
   Eval Value         {- ^ new value at index -} ->
-  Eval (SeqMap Concrete)
+  Eval (SeqMap Concrete (GenValue Concrete))
 updateFront _len _eltTy vs (Left idx) val = do
   return $ updateSeqMap vs idx val
 
@@ -619,10 +619,10 @@ updateFront_word _len _eltTy bs (Right w) val = do
 updateBack ::
   Nat'               {- ^ length of the sequence -} ->
   TValue             {- ^ type of values in the sequence -} ->
-  SeqMap Concrete    {- ^ sequence to update -} ->
+  SeqMap Concrete (GenValue Concrete) {- ^ sequence to update -} ->
   Either Integer (WordValue Concrete) {- ^ index -} ->
   Eval Value         {- ^ new value at index -} ->
-  Eval (SeqMap Concrete)
+  Eval (SeqMap Concrete (GenValue Concrete))
 updateBack Inf _eltTy _vs _w _val =
   evalPanic "Unexpected infinite sequence in updateEnd" []
 updateBack (Nat n) _eltTy vs (Left idx) val = do
diff --git a/src/Cryptol/Eval/Generic.hs b/src/Cryptol/Eval/Generic.hs
index 4af134b9..2fc8f59b 100644
--- a/src/Cryptol/Eval/Generic.hs
+++ b/src/Cryptol/Eval/Generic.hs
@@ -969,7 +969,7 @@ joinWordVal sym w1 w2
   Concrete ->
   Integer ->
   Integer ->
-  SeqMap Concrete ->
+  SeqMap Concrete (GenValue Concrete)->
   SEval Concrete (GenValue Concrete)
   #-}
 joinWords :: forall sym.
@@ -977,7 +977,7 @@ joinWords :: forall sym.
   sym ->
   Integer ->
   Integer ->
-  SeqMap sym ->
+  SeqMap sym (GenValue sym) ->
   SEval sym (GenValue sym)
 joinWords sym nParts nEach xs =
   loop (WordVal <$> wordLit sym 0 0) (enumerateSeqMap nParts xs)
@@ -999,7 +999,7 @@ joinWords sym nParts nEach xs =
   Nat' ->
   Integer ->
   TValue ->
-  SeqMap Concrete ->
+  SeqMap Concrete (GenValue Concrete) ->
   SEval Concrete (GenValue Concrete)
   #-}
 joinSeq ::
@@ -1008,7 +1008,7 @@ joinSeq ::
   Nat' ->
   Integer ->
   TValue ->
-  SeqMap sym ->
+  SeqMap sym (GenValue sym) ->
   SEval sym (GenValue sym)
 
 -- Special case for 0 length inner sequences.
@@ -1568,9 +1568,9 @@ assertIndexInBounds sym (Nat n) (Right (LargeBitsVal w bits)) =
 indexPrim ::
   Backend sym =>
   sym ->
-  (Nat' -> TValue -> SeqMap sym -> TValue -> SInteger sym -> SEval sym (GenValue sym)) ->
-  (Nat' -> TValue -> SeqMap sym -> TValue -> [SBit sym] -> SEval sym (GenValue sym)) ->
-  (Nat' -> TValue -> SeqMap sym -> TValue -> SWord sym -> SEval sym (GenValue sym)) ->
+  (Nat' -> TValue -> SeqMap sym (GenValue sym) -> TValue -> SInteger sym -> SEval sym (GenValue sym)) ->
+  (Nat' -> TValue -> SeqMap sym (GenValue sym) -> TValue -> [SBit sym] -> SEval sym (GenValue sym)) ->
+  (Nat' -> TValue -> SeqMap sym (GenValue sym) -> TValue -> SWord sym -> SEval sym (GenValue sym)) ->
   Prim sym
 indexPrim sym int_op bits_op word_op =
   PNumPoly \len ->
@@ -1599,7 +1599,7 @@ updatePrim ::
   Backend sym =>
   sym ->
   (Nat' -> TValue -> WordValue sym -> Either (SInteger sym) (WordValue sym) -> SEval sym (GenValue sym) -> SEval sym (WordValue sym)) ->
-  (Nat' -> TValue -> SeqMap sym    -> Either (SInteger sym) (WordValue sym) -> SEval sym (GenValue sym) -> SEval sym (SeqMap sym)) ->
+  (Nat' -> TValue -> SeqMap sym (GenValue sym) -> Either (SInteger sym) (WordValue sym) -> SEval sym (GenValue sym) -> SEval sym (SeqMap sym (GenValue sym))) ->
   Prim sym
 updatePrim sym updateWord updateSeq =
   PNumPoly \len ->
@@ -1700,11 +1700,11 @@ infFromThenV sym =
 
 barrelShifter :: Backend sym =>
   sym ->
-  (SeqMap sym -> Integer -> SEval sym (SeqMap sym))
+  (SeqMap sym (GenValue sym) -> Integer -> SEval sym (SeqMap sym (GenValue sym)))
      {- ^ concrete shifting operation -} ->
-  SeqMap sym  {- ^ initial value -} ->
+  SeqMap sym (GenValue sym) {- ^ initial value -} ->
   [SBit sym]  {- ^ bits of shift amount, in big-endian order -} ->
-  SEval sym (SeqMap sym)
+  SEval sym (SeqMap sym (GenValue sym))
 barrelShifter sym shift_op = go
   where
   go x [] = return x
@@ -2059,9 +2059,9 @@ mergeValue sym c v1 v2 =
 mergeSeqMap :: Backend sym =>
   sym ->
   SBit sym ->
-  SeqMap sym ->
-  SeqMap sym ->
-  SeqMap sym
+  SeqMap sym (GenValue sym)->
+  SeqMap sym (GenValue sym)->
+  SeqMap sym (GenValue sym)
 mergeSeqMap sym c x y =
   IndexSeqMap $ \i ->
     iteValue sym c (lookupSeqMap x i) (lookupSeqMap y i)
@@ -2169,8 +2169,8 @@ sparkParMap ::
   sym ->
   (SEval sym (GenValue sym) -> SEval sym (GenValue sym)) ->
   Integer ->
-  SeqMap sym ->
-  SEval sym (SeqMap sym)
+  SeqMap sym (GenValue sym) ->
+  SEval sym (SeqMap sym (GenValue sym))
 sparkParMap sym f n m =
   finiteSeqMap <$> mapM (sSpark sym . g) (enumerateSeqMap n m)
  where
diff --git a/src/Cryptol/Eval/SBV.hs b/src/Cryptol/Eval/SBV.hs
index 9bdc56e5..be3c83e4 100644
--- a/src/Cryptol/Eval/SBV.hs
+++ b/src/Cryptol/Eval/SBV.hs
@@ -92,7 +92,7 @@ indexFront ::
   SBV ->
   Nat' ->
   TValue ->
-  SeqMap SBV ->
+  SeqMap SBV (GenValue SBV) ->
   TValue ->
   SVal ->
   SEval SBV Value
@@ -131,7 +131,7 @@ indexBack ::
   SBV ->
   Nat' ->
   TValue ->
-  SeqMap SBV ->
+  SeqMap SBV (GenValue SBV) ->
   TValue ->
   SWord SBV ->
   SEval SBV Value
@@ -142,7 +142,7 @@ indexFront_bits ::
   SBV ->
   Nat' ->
   TValue ->
-  SeqMap SBV ->
+  SeqMap SBV (GenValue SBV) ->
   TValue ->
   [SBit SBV] ->
   SEval SBV Value
@@ -175,7 +175,7 @@ indexBack_bits ::
   SBV ->
   Nat' ->
   TValue ->
-  SeqMap SBV ->
+  SeqMap SBV (GenValue SBV) ->
   TValue ->
   [SBit SBV] ->
   SEval SBV Value
@@ -204,10 +204,10 @@ updateFrontSym ::
   SBV ->
   Nat' ->
   TValue ->
-  SeqMap SBV ->
+  SeqMap SBV (GenValue SBV) ->
   Either (SInteger SBV) (WordValue SBV) ->
   SEval SBV (GenValue SBV) ->
-  SEval SBV (SeqMap SBV)
+  SEval SBV (SeqMap SBV (GenValue SBV))
 updateFrontSym sym _len _eltTy vs (Left idx) val =
   case SBV.svAsInteger idx of
     Just i -> return $ updateSeqMap vs i val
@@ -275,10 +275,10 @@ updateBackSym ::
   SBV ->
   Nat' ->
   TValue ->
-  SeqMap SBV ->
+  SeqMap SBV (GenValue SBV) ->
   Either (SInteger SBV) (WordValue SBV) ->
   SEval SBV (GenValue SBV) ->
-  SEval SBV (SeqMap SBV)
+  SEval SBV (SeqMap SBV (GenValue SBV))
 updateBackSym _ Inf _ _ _ _ = evalPanic "Expected finite sequence" ["updateBackSym"]
 
 updateBackSym sym (Nat n) _eltTy vs (Left idx) val =
diff --git a/src/Cryptol/Eval/Value.hs b/src/Cryptol/Eval/Value.hs
index 0d254bee..14b623bd 100644
--- a/src/Cryptol/Eval/Value.hs
+++ b/src/Cryptol/Eval/Value.hs
@@ -89,16 +89,12 @@ module Cryptol.Eval.Value
   , updateWordValue
   ) where
 
-import Control.Monad.IO.Class
 import Data.Bits
-import Data.IORef
-import Data.Map.Strict (Map)
 import Data.Ratio
-import qualified Data.Map.Strict as Map
-import MonadLib
 import Numeric (showIntAtBase)
 
 import Cryptol.Backend
+import Cryptol.Backend.SeqMap
 import qualified Cryptol.Backend.Arch as Arch
 import Cryptol.Backend.Monad
   ( evalPanic, wordTooWide, CallStack, combineCallStacks )
@@ -112,8 +108,6 @@ import Cryptol.Utils.Panic(panic)
 import Cryptol.Utils.PP
 import Cryptol.Utils.RecordMap
 
-import Data.List(genericIndex)
-
 import GHC.Generics (Generic)
 
 -- | Some options for evalutaion
@@ -124,121 +118,11 @@ data EvalOpts = EvalOpts
 
 -- Values ----------------------------------------------------------------------
 
--- | A sequence map represents a mapping from nonnegative integer indices
---   to values.  These are used to represent both finite and infinite sequences.
-data SeqMap sym
-  = IndexSeqMap  !(Integer -> SEval sym (GenValue sym))
-  | UpdateSeqMap !(Map Integer (SEval sym (GenValue sym)))
-                 !(Integer -> SEval sym (GenValue sym))
-
-lookupSeqMap :: SeqMap sym -> Integer -> SEval sym (GenValue sym)
-lookupSeqMap (IndexSeqMap f) i = f i
-lookupSeqMap (UpdateSeqMap m f) i =
-  case Map.lookup i m of
-    Just x  -> x
-    Nothing -> f i
-
 -- | An arbitrarily-chosen number of elements where we switch from a dense
 --   sequence representation of bit-level words to 'SeqMap' representation.
 largeBitSize :: Integer
 largeBitSize = 1 `shiftL` 48
 
--- | Generate a finite sequence map from a list of values
-finiteSeqMap :: [SEval sym (GenValue sym)] -> SeqMap sym
-finiteSeqMap xs =
-   UpdateSeqMap
-      (Map.fromList (zip [0..] xs))
-      (\i -> panic "finiteSeqMap" ["Out of bounds access of finite seq map", "length: " ++ show (length xs), show i])
-
--- | Generate an infinite sequence map from a stream of values
-infiniteSeqMap :: Backend sym => sym -> [SEval sym (GenValue sym)] -> SEval sym (SeqMap sym)
-infiniteSeqMap sym xs =
-   -- TODO: use an int-trie?
-   memoMap sym (IndexSeqMap $ \i -> genericIndex xs i)
-
--- | Create a finite list of length @n@ of the values from @[0..n-1]@ in
---   the given the sequence emap.
-enumerateSeqMap :: (Integral n) => n -> SeqMap sym -> [SEval sym (GenValue sym)]
-enumerateSeqMap n m = [ lookupSeqMap m  i | i <- [0 .. (toInteger n)-1] ]
-
--- | Create an infinite stream of all the values in a sequence map
-streamSeqMap :: SeqMap sym -> [SEval sym (GenValue sym)]
-streamSeqMap m = [ lookupSeqMap m i | i <- [0..] ]
-
--- | Reverse the order of a finite sequence map
-reverseSeqMap :: Integer     -- ^ Size of the sequence map
-              -> SeqMap sym
-              -> SeqMap sym
-reverseSeqMap n vals = IndexSeqMap $ \i -> lookupSeqMap vals (n - 1 - i)
-
-updateSeqMap :: SeqMap sym -> Integer -> SEval sym (GenValue sym) -> SeqMap sym
-updateSeqMap (UpdateSeqMap m sm) i x = UpdateSeqMap (Map.insert i x m) sm
-updateSeqMap (IndexSeqMap f) i x = UpdateSeqMap (Map.singleton i x) f
-
--- | Concatenate the first @n@ values of the first sequence map onto the
---   beginning of the second sequence map.
-concatSeqMap :: Integer -> SeqMap sym -> SeqMap sym -> SeqMap sym
-concatSeqMap n x y =
-    IndexSeqMap $ \i ->
-       if i < n
-         then lookupSeqMap x i
-         else lookupSeqMap y (i-n)
-
--- | Given a number @n@ and a sequence map, return two new sequence maps:
---   the first containing the values from @[0..n-1]@ and the next containing
---   the values from @n@ onward.
-splitSeqMap :: Integer -> SeqMap sym -> (SeqMap sym, SeqMap sym)
-splitSeqMap n xs = (hd,tl)
-  where
-  hd = xs
-  tl = IndexSeqMap $ \i -> lookupSeqMap xs (i+n)
-
--- | Drop the first @n@ elements of the given 'SeqMap'.
-dropSeqMap :: Integer -> SeqMap sym -> SeqMap sym
-dropSeqMap 0 xs = xs
-dropSeqMap n xs = IndexSeqMap $ \i -> lookupSeqMap xs (i+n)
-
--- | Given a sequence map, return a new sequence map that is memoized using
---   a finite map memo table.
-memoMap :: Backend sym => sym -> SeqMap sym -> SEval sym (SeqMap sym)
-memoMap sym x = do
-  stk <- sGetCallStack sym
-  cache <- liftIO $ newIORef $ Map.empty
-  return $ IndexSeqMap (memo cache stk)
-
-  where
-  memo cache stk i = do
-    mz <- liftIO (Map.lookup i <$> readIORef cache)
-    case mz of
-      Just z  -> return z
-      Nothing -> sWithCallStack sym stk (doEval cache i)
-
-  doEval cache i = do
-    v <- lookupSeqMap x i
-    liftIO $ atomicModifyIORef' cache (\m -> (Map.insert i v m, ()))
-    return v
-
--- | Apply the given evaluation function pointwise to the two given
---   sequence maps.
-zipSeqMap ::
-  Backend sym =>
-  sym ->
-  (GenValue sym -> GenValue sym -> SEval sym (GenValue sym)) ->
-  SeqMap sym ->
-  SeqMap sym ->
-  SEval sym (SeqMap sym)
-zipSeqMap sym f x y =
-  memoMap sym (IndexSeqMap $ \i -> join (f <$> lookupSeqMap x i <*> lookupSeqMap y i))
-
--- | Apply the given function to each value in the given sequence map
-mapSeqMap ::
-  Backend sym =>
-  sym ->
-  (GenValue sym -> SEval sym (GenValue sym)) ->
-  SeqMap sym -> SEval sym (SeqMap sym)
-mapSeqMap sym f x =
-  memoMap sym (IndexSeqMap $ \i -> f =<< lookupSeqMap x i)
-
 -- | 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
@@ -251,7 +135,8 @@ mapSeqMap sym f x =
 data WordValue sym
   = ThunkWordVal Integer !(SEval sym (WordValue sym))
   | WordVal !(SWord sym)                      -- ^ Packed word representation for bit sequences.
-  | LargeBitsVal !Integer !(SeqMap sym)       -- ^ A large bitvector sequence, represented as a
+  | LargeBitsVal !Integer !(SeqMap sym (GenValue sym))
+                                              -- ^ A large bitvector sequence, represented as a
                                               --   'SeqMap' of bits.
  deriving (Generic)
 
@@ -262,8 +147,8 @@ asWordVal sym (ThunkWordVal _ m)  = asWordVal sym =<< m
 asWordVal sym (LargeBitsVal n xs) = packWord sym =<< traverse (fromVBit <$>) (enumerateSeqMap n xs)
 
 -- | Force a word value into a sequence of bits
-asBitsMap :: Backend sym => sym -> WordValue sym -> SeqMap sym
-asBitsMap sym (WordVal w)         = IndexSeqMap $ \i -> VBit <$> (wordBit sym w i)
+asBitsMap :: Backend sym => sym -> WordValue sym -> SeqMap sym (GenValue sym)
+asBitsMap sym (WordVal w)         = IndexSeqMap $ \i -> VBit <$> wordBit sym w i
 asBitsMap sym (ThunkWordVal _ m)  = IndexSeqMap $ \i -> do mp <- asBitsMap sym <$> m; lookupSeqMap mp i
 asBitsMap _   (LargeBitsVal _ xs) = xs
 
@@ -272,7 +157,7 @@ asBitsMap _   (LargeBitsVal _ xs) = xs
 enumerateWordValue :: Backend sym => sym -> WordValue sym -> SEval sym [SBit sym]
 enumerateWordValue sym (WordVal w) = unpackWord sym w
 enumerateWordValue sym (ThunkWordVal _ m) = enumerateWordValue sym =<< m
-enumerateWordValue _ (LargeBitsVal n xs) = traverse (fromVBit <$>) (enumerateSeqMap n xs)
+enumerateWordValue _ (LargeBitsVal n xs)  = traverse (fromVBit <$>) (enumerateSeqMap n xs)
 
 -- | Turn a word value into a sequence of bits, forcing each bit.
 --   The sequence is returned in reverse of the usual order, which is little-endian order.
@@ -326,10 +211,10 @@ data GenValue sym
   | VInteger !(SInteger sym)                   -- ^ @ Integer @ or @ Z n @
   | VRational !(SRational sym)                 -- ^ @ Rational @
   | VFloat !(SFloat sym)
-  | VSeq !Integer !(SeqMap sym)                -- ^ @ [n]a   @
+  | VSeq !Integer !(SeqMap sym (GenValue sym)) -- ^ @ [n]a   @
                                                --   Invariant: VSeq is never a sequence of bits
   | VWord !Integer !(WordValue sym)            -- ^ @ [n]Bit @
-  | VStream !(SeqMap sym)                      -- ^ @ [inf]a @
+  | VStream !(SeqMap sym (GenValue sym))       -- ^ @ [inf]a @
   | VFun  CallStack (SEval sym (GenValue sym) -> SEval sym (GenValue sym)) -- ^ functions
   | VPoly CallStack (TValue -> SEval sym (GenValue sym))   -- ^ polymorphic values (kind *)
   | VNumPoly CallStack (Nat' -> SEval sym (GenValue sym))  -- ^ polymorphic values (kind #)
@@ -412,7 +297,7 @@ ppValue x opts = loop
   ppWordVal :: WordValue sym -> SEval sym Doc
   ppWordVal w = ppSWord x opts =<< asWordVal x w
 
-  ppWordSeq :: Integer -> SeqMap sym -> SEval sym Doc
+  ppWordSeq :: Integer -> SeqMap sym (GenValue sym) -> SEval sym Doc
   ppWordSeq sz vals = do
     ws <- sequence (enumerateSeqMap sz vals)
     case ws of
@@ -553,7 +438,7 @@ ilam sym f =
 
 -- | Construct either a finite sequence, or a stream.  In the finite case,
 -- record whether or not the elements were bits, to aid pretty-printing.
-mkSeq :: Backend sym => Nat' -> TValue -> SeqMap sym -> GenValue sym
+mkSeq :: Backend sym => Nat' -> TValue -> SeqMap sym (GenValue sym) -> GenValue sym
 mkSeq len elty vals = case len of
   Nat n
     | isTBit elty -> VWord n $ LargeBitsVal n vals
@@ -582,13 +467,13 @@ fromVRational val = case val of
   _      -> evalPanic "fromVRational" ["not a Rational"]
 
 -- | Extract a finite sequence value.
-fromVSeq :: GenValue sym -> SeqMap sym
+fromVSeq :: GenValue sym -> SeqMap sym (GenValue sym)
 fromVSeq val = case val of
   VSeq _ vs -> vs
   _         -> evalPanic "fromVSeq" ["not a sequence"]
 
 -- | Extract a sequence.
-fromSeq :: Backend sym => String -> GenValue sym -> SEval sym (SeqMap sym)
+fromSeq :: Backend sym => String -> GenValue sym -> SEval sym (SeqMap sym (GenValue sym))
 fromSeq msg val = case val of
   VSeq _ vs   -> return vs
   VStream vs  -> return vs
diff --git a/src/Cryptol/Eval/What4.hs b/src/Cryptol/Eval/What4.hs
index 99edb859..339e0656 100644
--- a/src/Cryptol/Eval/What4.hs
+++ b/src/Cryptol/Eval/What4.hs
@@ -459,7 +459,7 @@ getUninterpFn sym funNm args ret =
                            ]
 
 toWord32 :: W4.IsSymExprBuilder sym =>
-  What4 sym -> String -> SeqMap (What4 sym) -> Integer -> SEval (What4 sym) (W4.SymBV sym 32)
+  What4 sym -> String -> SeqMap (What4 sym) (GenValue (What4 sym)) -> Integer -> SEval (What4 sym) (W4.SymBV sym 32)
 toWord32 sym nm ss i =
   do x <- fromVWord sym nm =<< lookupSeqMap ss i
      case x of
@@ -470,7 +470,7 @@ fromWord32 :: W4.IsSymExprBuilder sym => W4.SymBV sym 32 -> SEval (What4 sym) (V
 fromWord32 = pure . VWord 32 . WordVal . SW.DBV
 
 toWord64 :: W4.IsSymExprBuilder sym =>
-  What4 sym -> String -> SeqMap (What4 sym) -> Integer -> SEval (What4 sym) (W4.SymBV sym 64)
+  What4 sym -> String -> SeqMap (What4 sym) (GenValue (What4 sym)) -> Integer -> SEval (What4 sym) (W4.SymBV sym 64)
 toWord64 sym nm ss i =
   do x <- fromVWord sym nm =<< lookupSeqMap ss i
      case x of
@@ -537,7 +537,7 @@ indexFront_int ::
   What4 sym ->
   Nat' ->
   TValue ->
-  SeqMap (What4 sym) ->
+  SeqMap (What4 sym) (GenValue (What4 sym)) ->
   TValue ->
   SInteger (What4 sym) ->
   SEval (What4 sym) (Value sym)
@@ -586,7 +586,7 @@ indexBack_int ::
   What4 sym ->
   Nat' ->
   TValue ->
-  SeqMap (What4 sym) ->
+  SeqMap (What4 sym) (GenValue (What4 sym)) ->
   TValue ->
   SInteger (What4 sym) ->
   SEval (What4 sym) (Value sym)
@@ -598,7 +598,7 @@ indexFront_word ::
   What4 sym ->
   Nat' ->
   TValue ->
-  SeqMap (What4 sym) ->
+  SeqMap (What4 sym) (GenValue (What4 sym)) ->
   TValue ->
   SWord (What4 sym) ->
   SEval (What4 sym) (Value sym)
@@ -639,7 +639,7 @@ indexBack_word ::
   What4 sym ->
   Nat' ->
   TValue ->
-  SeqMap (What4 sym) ->
+  SeqMap (What4 sym) (GenValue (What4 sym)) ->
   TValue ->
   SWord (What4 sym) ->
   SEval (What4 sym) (Value sym)
@@ -651,7 +651,7 @@ indexFront_bits :: forall sym.
   What4 sym ->
   Nat' ->
   TValue ->
-  SeqMap (What4 sym) ->
+  SeqMap (What4 sym) (GenValue (What4 sym)) ->
   TValue ->
   [SBit (What4 sym)] ->
   SEval (What4 sym) (Value sym)
@@ -684,7 +684,7 @@ indexBack_bits ::
   What4 sym ->
   Nat' ->
   TValue ->
-  SeqMap (What4 sym) ->
+  SeqMap (What4 sym) (GenValue (What4 sym)) ->
   TValue ->
   [SBit (What4 sym)] ->
   SEval (What4 sym) (Value sym)
@@ -723,10 +723,10 @@ updateFrontSym ::
   What4 sym ->
   Nat' ->
   TValue ->
-  SeqMap (What4 sym) ->
+  SeqMap (What4 sym) (GenValue (What4 sym)) ->
   Either (SInteger (What4 sym)) (WordValue (What4 sym)) ->
   SEval (What4 sym) (Value sym) ->
-  SEval (What4 sym) (SeqMap (What4 sym))
+  SEval (What4 sym) (SeqMap (What4 sym) (GenValue (What4 sym)))
 updateFrontSym sym _len _eltTy vs (Left idx) val =
   case W4.asInteger idx of
     Just i -> return $ updateSeqMap vs i val
@@ -748,10 +748,10 @@ updateBackSym ::
   What4 sym ->
   Nat' ->
   TValue ->
-  SeqMap (What4 sym) ->
+  SeqMap (What4 sym) (GenValue (What4 sym)) ->
   Either (SInteger (What4 sym)) (WordValue (What4 sym)) ->
   SEval (What4 sym) (Value sym) ->
-  SEval (What4 sym) (SeqMap (What4 sym))
+  SEval (What4 sym) (SeqMap (What4 sym) (GenValue (What4 sym)))
 updateBackSym _ Inf _ _ _ _ = evalPanic "Expected finite sequence" ["updateBackSym"]
 
 updateBackSym sym (Nat n) _eltTy vs (Left idx) val =