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

    {-# LANGUAGE LambdaCase #-}
    {-# LANGUAGE Trustworthy #-}
    {-# LANGUAGE TupleSections #-}
    {-# LANGUAGE MultiParamTypeClasses #-}
    {-# LANGUAGE RecordWildCards #-}
    {-# LANGUAGE NamedFieldPuns #-}
    {-# LANGUAGE Rank2Types #-}
    {-# LANGUAGE PatternGuards #-}
    {-# LANGUAGE ScopedTypeVariables #-}
    {-# LANGUAGE ViewPatterns #-}
    {-# LANGUAGE BangPatterns #-}
    {-# OPTIONS_GHC -fno-warn-orphans #-}
    module Cryptol.Prims.Eval where

    import Control.Monad (join, unless)

    import Cryptol.TypeCheck.AST
    import Cryptol.TypeCheck.Solver.InfNat (Nat'(..),fromNat,genLog, nMul)
    import qualified Cryptol.Eval.Arch as Arch
    import Cryptol.Eval.Monad
    import Cryptol.Eval.Type
    import Cryptol.Eval.Value
    import Cryptol.Testing.Random (randomValue)
    import Cryptol.Utils.Panic (panic)
    import Cryptol.ModuleSystem.Name (asPrim)
    import Cryptol.Utils.Ident (Ident,mkIdent)
    import Cryptol.Utils.PP
    import Cryptol.Utils.Logger(logPrint)

    import qualified Data.Foldable as Fold
    import Data.List (sortBy)
    import qualified Data.Sequence as Seq
    import Data.Ord (comparing)
    import Data.Bits (Bits(..))

    import qualified Data.Map.Strict as Map
    import qualified Data.Text as T

    import System.Random.TF.Gen (seedTFGen)

    -- Primitives ------------------------------------------------------------------

    instance EvalPrims Bool BV Integer where
      evalPrim Decl { dName = n, .. }
        | Just prim <- asPrim n, Just val <- Map.lookup prim primTable = val

      evalPrim Decl { .. } =
          panic "Eval" [ "Unimplemented primitive", show dName ]

      iteValue b t f = if b then t else f

    primTable :: Map.Map Ident Value
    primTable = Map.fromList $ map (\(n, v) -> (mkIdent (T.pack n), v))
      [ ("+"          , {-# SCC "Prelude::(+)" #-}
                        binary (arithBinary (liftBinArith (+)) (liftBinInteger (+))
                                (liftBinIntMod (+))))
      , ("-"          , {-# SCC "Prelude::(-)" #-}
                        binary (arithBinary (liftBinArith (-)) (liftBinInteger (-))
                                (liftBinIntMod (-))))
      , ("*"          , {-# SCC "Prelude::(*)" #-}
                        binary (arithBinary (liftBinArith (*)) (liftBinInteger (*))
                                (liftBinIntMod (*))))
      , ("/"          , {-# SCC "Prelude::(/)" #-}
                        binary (arithBinary (liftDivArith div) (liftDivInteger div)
                                (const (liftDivInteger div))))
      , ("%"          , {-# SCC "Prelude::(%)" #-}
                        binary (arithBinary (liftDivArith mod) (liftDivInteger mod)
                                (const (liftDivInteger mod))))
      , ("^^"         , {-# SCC "Prelude::(^^)" #-}
                        binary (arithBinary modExp integerExp intModExp))
      , ("lg2"        , {-# SCC "Prelude::lg2" #-}
                        unary  (arithUnary (liftUnaryArith lg2) integerLg2 (const integerLg2)))
      , ("negate"     , {-# SCC "Prelude::negate" #-}
                        unary  (arithUnary (liftUnaryArith negate) integerNeg intModNeg))
      , ("<"          , {-# SCC "Prelude::(<)" #-}
                        binary (cmpOrder "<"  (\o -> o == LT           )))
      , (">"          , {-# SCC "Prelude::(>)" #-}
                        binary (cmpOrder ">"  (\o -> o == GT           )))
      , ("<="         , {-# SCC "Prelude::(<=)" #-}
                        binary (cmpOrder "<=" (\o -> o == LT || o == EQ)))
      , (">="         , {-# SCC "Prelude::(>=)" #-}
                        binary (cmpOrder ">=" (\o -> o == GT || o == EQ)))
      , ("=="         , {-# SCC "Prelude::(==)" #-}
                        binary (cmpOrder "==" (\o ->            o == EQ)))
      , ("!="         , {-# SCC "Prelude::(!=)" #-}
                        binary (cmpOrder "!=" (\o ->            o /= EQ)))
      , ("<$"         , {-# SCC "Prelude::(<$)" #-}
                        binary (signedCmpOrder "<$" (\o -> o == LT)))
      , ("/$"         , {-# SCC "Prelude::(/$)" #-}
                        binary (arithBinary (liftSigned bvSdiv) (liftDivInteger div)
                                (const (liftDivInteger div))))
      , ("%$"         , {-# SCC "Prelude::(%$)" #-}
                        binary (arithBinary (liftSigned bvSrem) (liftDivInteger mod)
                                (const (liftDivInteger mod))))
      , (">>$"        , {-# SCC "Prelude::(>>$)" #-}
                        sshrV)
      , ("&&"         , {-# SCC "Prelude::(&&)" #-}
                        binary (logicBinary (.&.) (binBV (.&.))))
      , ("||"         , {-# SCC "Prelude::(||)" #-}
                        binary (logicBinary (.|.) (binBV (.|.))))
      , ("^"          , {-# SCC "Prelude::(^)" #-}
                        binary (logicBinary xor (binBV xor)))
      , ("complement" , {-# SCC "Prelude::complement" #-}
                        unary  (logicUnary complement (unaryBV complement)))
      , ("toInteger"  , ecToIntegerV)
      , ("fromInteger", ecFromIntegerV (flip mod))
      , ("fromZ"      , {-# SCC "Prelude::fromZ" #-}
                        nlam $ \ _modulus ->
                        lam  $ \ x -> x)
      , ("<<"         , {-# SCC "Prelude::(<<)" #-}
                        logicShift shiftLW shiftLB shiftLS)
      , (">>"         , {-# SCC "Prelude::(>>)" #-}
                        logicShift shiftRW shiftRB shiftRS)
      , ("<<<"        , {-# SCC "Prelude::(<<<)" #-}
                        logicShift rotateLW rotateLB rotateLS)
      , (">>>"        , {-# SCC "Prelude::(>>>)" #-}
                        logicShift rotateRW rotateRB rotateRS)
      , ("True"       , VBit True)
      , ("False"      , VBit False)

      , ("carry"      , {-# SCC "Prelude::carry" #-}
                        carryV)
      , ("scarry"     , {-# SCC "Prelude::scarry" #-}
                        scarryV)
      , ("number"     , {-# SCC "Prelude::number" #-}
                        ecNumberV)

      , ("#"          , {-# SCC "Prelude::(#)" #-}
                        nlam $ \ front ->
                        nlam $ \ back  ->
                        tlam $ \ elty  ->
                        lam  $ \ l     -> return $
                        lam  $ \ r     -> join (ccatV front back elty <$> l <*> r))

      , ("@"          , {-# SCC "Prelude::(@)" #-}
                        indexPrim indexFront_bits indexFront)
      , ("!"          , {-# SCC "Prelude::(!)" #-}
                        indexPrim indexBack_bits indexBack)

      , ("update"     , {-# SCC "Prelude::update" #-}
                        updatePrim updateFront_word updateFront)

      , ("updateEnd"  , {-# SCC "Prelude::updateEnd" #-}
                        updatePrim updateBack_word updateBack)

      , ("zero"       , {-# SCC "Prelude::zero" #-}
                        tlam zeroV)

      , ("join"       , {-# SCC "Prelude::join" #-}
                        nlam $ \ parts ->
                        nlam $ \ (finNat' -> each)  ->
                        tlam $ \ a     ->
                        lam  $ \ x     ->
                          joinV parts each a =<< x)

      , ("split"      , {-# SCC "Prelude::split" #-}
                        ecSplitV)

      , ("splitAt"    , {-# SCC "Prelude::splitAt" #-}
                        nlam $ \ front ->
                        nlam $ \ back  ->
                        tlam $ \ a     ->
                        lam  $ \ x     ->
                           splitAtV front back a =<< x)

      , ("fromThen"   , {-# SCC "Prelude::fromThen" #-}
                        fromThenV)
      , ("fromTo"     , {-# SCC "Prelude::fromTo" #-}
                        fromToV)
      , ("fromThenTo" , {-# SCC "Prelude::fromThenTo" #-}
                        fromThenToV)
      , ("infFrom"    , {-# SCC "Prelude::infFrom" #-}
                        infFromV)
      , ("infFromThen", {-# SCC "Prelude::infFromThen" #-}
                        infFromThenV)

      , ("error"      , {-# SCC "Prelude::error" #-}
                          tlam $ \a ->
                          nlam $ \_ ->
                           lam $ \s -> errorV a =<< (fromStr =<< s))

      , ("reverse"    , {-# SCC "Prelude::reverse" #-}
                        nlam $ \_a ->
                        tlam $ \_b ->
                         lam $ \xs -> reverseV =<< xs)

      , ("transpose"  , {-# SCC "Prelude::transpose" #-}
                        nlam $ \a ->
                        nlam $ \b ->
                        tlam $ \c ->
                         lam $ \xs -> transposeV a b c =<< xs)

      , ("random"      , {-# SCC "Prelude::random" #-}
                         tlam $ \a ->
                         wlam $ \(bvVal -> x) -> return $ randomV a x)
      , ("trace"       , {-# SCC "Prelude::trace" #-}
                         nlam $ \_n ->
                         tlam $ \_a ->
                         tlam $ \_b ->
                          lam $ \s -> return $
                          lam $ \x -> return $
                          lam $ \y -> do
                             msg <- fromStr =<< s
                             EvalOpts { evalPPOpts, evalLogger } <- getEvalOpts
                             doc <- ppValue evalPPOpts =<< x
                             yv <- y
                             io $ logPrint evalLogger
                                 $ if null msg then doc else text msg <+> doc
                             return yv)
      ]

    -- | Make a numeric literal value at the given type.
    mkLit :: BitWord b w i => TValue -> Integer -> GenValue b w i
    mkLit ty =
      case ty of
        TVInteger                    -> VInteger . integerLit
        TVIntMod _                   -> VInteger . integerLit
        TVSeq w TVBit
          | w >= Arch.maxBigIntWidth -> wordTooWide w
          | otherwise                -> word w
        _                            -> evalPanic "Cryptol.Eval.Prim.evalConst"
                                        [ "Invalid type for number" ]

    -- | Make a numeric constant.
    ecNumberV :: BitWord b w i => GenValue b w i
    ecNumberV = nlam $ \valT ->
                tlam $ \ty ->
                case valT of
                  Nat v -> mkLit ty v
                  _ -> evalPanic "Cryptol.Eval.Prim.evalConst"
                           ["Unexpected Inf in constant."
                           , show valT
                           , show ty
                           ]

    -- | Convert a word to a non-negative integer.
    ecToIntegerV :: BitWord b w i => GenValue b w i
    ecToIntegerV =
      nlam $ \ _ ->
      wlam $ \ w -> return $ VInteger (wordToInt w)

    -- | Convert an unbounded integer to a packed bitvector.
    ecFromIntegerV :: BitWord b w i => (Integer -> i -> i) -> GenValue b w i
    ecFromIntegerV opz =
      tlam $ \ a ->
      lam  $ \ x ->
      do i <- fromVInteger <$> x
         return $ arithNullary (flip wordFromInt i) i (flip opz i) a

    --------------------------------------------------------------------------------

    -- | Create a packed word
    modExp :: Integer -- ^ bit size of the resulting word
           -> BV      -- ^ base
           -> BV      -- ^ exponent
           -> Eval BV
    modExp bits (BV _ base) (BV _ e)
      | bits == 0            = ready $ BV bits 0
      | base < 0 || bits < 0 = evalPanic "modExp"
                                 [ "bad args: "
                                 , "  base = " ++ show base
                                 , "  e    = " ++ show e
                                 , "  bits = " ++ show modulus
                                 ]
      | otherwise            = ready $ mkBv bits $ doubleAndAdd base e modulus
      where
      modulus = 0 `setBit` fromInteger bits

    intModExp :: Integer -> Integer -> Integer -> Eval Integer
    intModExp modulus base e
      | modulus > 0  = ready $ doubleAndAdd base e modulus
      | modulus == 0 = integerExp base e
      | otherwise    = evalPanic "intModExp" [ "negative modulus: " ++ show modulus ]

    integerExp :: Integer -> Integer -> Eval Integer
    integerExp x y
      | y < 0     = negativeExponent
      | otherwise = ready $ x ^ y

    integerLg2 :: Integer -> Eval Integer
    integerLg2 x
      | x < 0     = logNegative
      | otherwise = ready $ lg2 x

    integerNeg :: Integer -> Eval Integer
    integerNeg x = ready $ negate x

    intModNeg :: Integer -> Integer -> Eval Integer
    intModNeg modulus x = ready $ negate x `mod` modulus

    doubleAndAdd :: Integer -- ^ base
                 -> Integer -- ^ exponent mask
                 -> Integer -- ^ modulus
                 -> Integer
    doubleAndAdd base0 expMask modulus = go 1 base0 expMask
      where
      go acc base k
        | k > 0     = acc' `seq` base' `seq` go acc' base' (k `shiftR` 1)
        | otherwise = acc
        where
        acc' | k `testBit` 0 = acc `modMul` base
             | otherwise     = acc

        base' = base `modMul` base

        modMul x y = (x * y) `mod` modulus

    -- Operation Lifting -----------------------------------------------------------

    type Binary b w i = TValue -> GenValue b w i -> GenValue b w i -> Eval (GenValue b w i)

    binary :: Binary b w i -> GenValue b w i
    binary f = tlam $ \ ty ->
                lam $ \ a  -> return $
                lam $ \ b  -> do
                   --io $ putStrLn "Entering a binary function"
                   join (f ty <$> a <*> b)

    type Unary b w i = TValue -> GenValue b w i -> Eval (GenValue b w i)

    unary :: Unary b w i -> GenValue b w i
    unary f = tlam $ \ ty ->
               lam $ \ a  -> f ty =<< a

    -- Arith -----------------------------------------------------------------------

    -- | Turn a normal binop on Integers into one that can also deal with a bitsize.
    --   However, if the bitvector size is 0, always return the 0
    --   bitvector.
    liftBinArith :: (Integer -> Integer -> Integer) -> BinArith BV
    liftBinArith _  0 _        _        = ready $ mkBv 0 0
    liftBinArith op w (BV _ x) (BV _ y) = ready $ mkBv w $ op x y

    -- | Turn a normal binop on Integers into one that can also deal with a bitsize.
    --   Generate a thunk that throws a divide by 0 error when forced if the second
    --   argument is 0.  However, if the bitvector size is 0, always return the 0
    --   bitvector.
    liftDivArith :: (Integer -> Integer -> Integer) -> BinArith BV
    liftDivArith _  0 _        _        = ready $ mkBv 0 0
    liftDivArith _  _ _        (BV _ 0) = divideByZero
    liftDivArith op w (BV _ x) (BV _ y) = ready $ mkBv w $ op x y

    type BinArith w = Integer -> w -> w -> Eval w

    liftBinInteger :: (Integer -> Integer -> Integer) -> Integer -> Integer -> Eval Integer
    liftBinInteger op x y = ready $ op x y

    liftBinIntMod ::
      (Integer -> Integer -> Integer) -> Integer -> Integer -> Integer -> Eval Integer
    liftBinIntMod op m x y
      | m == 0    = ready $ op x y
      | otherwise = ready $ (op x y) `mod` m

    liftDivInteger :: (Integer -> Integer -> Integer) -> Integer -> Integer -> Eval Integer
    liftDivInteger _  _ 0 = divideByZero
    liftDivInteger op x y = ready $ op x y

    modWrap :: Integral a => a -> a -> Eval a
    modWrap _ 0 = divideByZero
    modWrap x y = return (x `mod` y)

    arithBinary :: forall b w i
                 . BitWord b w i
                => BinArith w
                -> (i -> i -> Eval i)
                -> (Integer -> i -> i -> Eval i)
                -> Binary b w i
    arithBinary opw opi opz = loop
      where
      loop' :: TValue
            -> Eval (GenValue b w i)
            -> Eval (GenValue b w i)
            -> Eval (GenValue b w i)
      loop' ty l r = join (loop ty <$> l <*> r)

      loop :: TValue
           -> GenValue b w i
           -> GenValue b w i
           -> Eval (GenValue b w i)
      loop ty l r = case ty of
        TVBit ->
          evalPanic "arithBinary" ["Bit not in class Arith"]

        TVInteger ->
          VInteger <$> opi (fromVInteger l) (fromVInteger r)

        TVIntMod n ->
          VInteger <$> opz n (fromVInteger l) (fromVInteger r)

        TVSeq w a
          -- words and finite sequences
          | isTBit a -> do
                      lw <- fromVWord "arithLeft" l
                      rw <- fromVWord "arithRight" r
                      return $ VWord w (WordVal <$> opw w lw rw)
          | otherwise -> VSeq w <$> (join (zipSeqMap (loop a) <$>
                                          (fromSeq "arithBinary left" l) <*>
                                          (fromSeq "arithBinary right" r)))

        TVStream a ->
          -- streams
          VStream <$> (join (zipSeqMap (loop a) <$>
                                 (fromSeq "arithBinary left" l) <*>
                                 (fromSeq "arithBinary right" r)))

        -- functions
        TVFun _ ety ->
          return $ lam $ \ x -> loop' ety (fromVFun l x) (fromVFun r x)

        -- tuples
        TVTuple tys ->
          do ls <- mapM (delay Nothing) (fromVTuple l)
             rs <- mapM (delay Nothing) (fromVTuple r)
             return $ VTuple (zipWith3 loop' tys ls rs)

        -- records
        TVRec fs ->
          do fs' <- sequence
                     [ (f,) <$> delay Nothing (loop' fty (lookupRecord f l) (lookupRecord f r))
                     | (f,fty) <- fs
                     ]
             return $ VRecord fs'

    type UnaryArith w = Integer -> w -> Eval w

    liftUnaryArith :: (Integer -> Integer) -> UnaryArith BV
    liftUnaryArith op w (BV _ x) = ready $ mkBv w $ op x

    arithUnary :: forall b w i
                . BitWord b w i
               => UnaryArith w
               -> (i -> Eval i)
               -> (Integer -> i -> Eval i)
               -> Unary b w i
    arithUnary opw opi opz = loop
      where
      loop' :: TValue -> Eval (GenValue b w i) -> Eval (GenValue b w i)
      loop' ty x = loop ty =<< x

      loop :: TValue -> GenValue b w i -> Eval (GenValue b w i)
      loop ty x = case ty of

        TVBit ->
          evalPanic "arithUnary" ["Bit not in class Arith"]

        TVInteger ->
          VInteger <$> opi (fromVInteger x)

        TVIntMod n ->
          VInteger <$> opz n (fromVInteger x)

        TVSeq w a
          -- words and finite sequences
          | isTBit a -> do
                  wx <- fromVWord "arithUnary" x
                  return $ VWord w (WordVal <$> opw w wx)
          | otherwise -> VSeq w <$> (mapSeqMap (loop a) =<< fromSeq "arithUnary" x)

        TVStream a ->
          VStream <$> (mapSeqMap (loop a) =<< fromSeq "arithUnary" x)

        -- functions
        TVFun _ ety ->
          return $ lam $ \ y -> loop' ety (fromVFun x y)

        -- tuples
        TVTuple tys ->
          do as <- mapM (delay Nothing) (fromVTuple x)
             return $ VTuple (zipWith loop' tys as)

        -- records
        TVRec fs ->
          do fs' <- sequence
                     [ (f,) <$> delay Nothing (loop' fty (lookupRecord f x))
                     | (f,fty) <- fs
                     ]
             return $ VRecord fs'

    arithNullary ::
      forall b w i.
      BitWord b w i =>
      (Integer -> w) ->
      i ->
      (Integer -> i) ->
      TValue -> GenValue b w i
    arithNullary opw opi opz = loop
      where
        loop :: TValue -> GenValue b w i
        loop ty =
          case ty of
            TVBit -> evalPanic "arithNullary" ["Bit not in class Arith"]

            TVInteger -> VInteger opi

            TVIntMod n -> VInteger (opz n)

            TVSeq w a
              -- words and finite sequences
              | isTBit a -> VWord w $ ready $ WordVal $ opw w
              | otherwise -> VSeq w $ IndexSeqMap $ const $ ready $ loop a

            TVStream a -> VStream $ IndexSeqMap $ const $ ready $ loop a

            TVFun _ b -> lam $ const $ ready $ loop b

            TVTuple tys -> VTuple $ map (ready . loop) tys

            TVRec fs -> VRecord [ (f, ready (loop a)) | (f, a) <- fs ]

    lg2 :: Integer -> Integer
    lg2 i = case genLog i 2 of
      Just (i',isExact) | isExact   -> i'
                        | otherwise -> i' + 1
      Nothing                       -> 0

    addV :: BitWord b w i => Binary b w i
    addV = arithBinary opw opi opz
      where
        opw _w x y = ready $ wordPlus x y
        opi x y = ready $ intPlus x y
        opz m x y = ready $ intModPlus m x y

    subV :: BitWord b w i => Binary b w i
    subV = arithBinary opw opi opz
      where
        opw _w x y = ready $ wordMinus x y
        opi x y = ready $ intMinus x y
        opz m x y = ready $ intModMinus m x y

    mulV :: BitWord b w i => Binary b w i
    mulV = arithBinary opw opi opz
      where
        opw _w x y = ready $ wordMult x y
        opi x y = ready $ intMult x y
        opz m x y = ready $ intModMult m x y

    intV :: BitWord b w i => i -> TValue -> GenValue b w i
    intV i = arithNullary (flip wordFromInt i) i (const i)

    -- Cmp -------------------------------------------------------------------------

    cmpValue :: BitWord b w i
             => (b -> b -> Eval a -> Eval a)
             -> (w -> w -> Eval a -> Eval a)
             -> (i -> i -> Eval a -> Eval a)
             -> (Integer -> i -> i -> Eval a -> Eval a)
             -> (TValue -> GenValue b w i -> GenValue b w i -> Eval a -> Eval a)
    cmpValue fb fw fi fz = cmp
      where
        cmp ty v1 v2 k =
          case ty of
            TVBit         -> fb (fromVBit v1) (fromVBit v2) k
            TVInteger     -> fi (fromVInteger v1) (fromVInteger v2) k
            TVIntMod n    -> fz n (fromVInteger v1) (fromVInteger v2) k
            TVSeq n t
              | isTBit t  -> do w1 <- fromVWord "cmpValue" v1
                                w2 <- fromVWord "cmpValue" v2
                                fw w1 w2 k
              | otherwise -> cmpValues (repeat t)
                             (enumerateSeqMap n (fromVSeq v1))
                             (enumerateSeqMap n (fromVSeq v2)) k
            TVStream _    -> panic "Cryptol.Prims.Value.cmpValue"
                             [ "Infinite streams are not comparable" ]
            TVFun _ _     -> panic "Cryptol.Prims.Value.cmpValue"
                             [ "Functions are not comparable" ]
            TVTuple tys   -> cmpValues tys (fromVTuple v1) (fromVTuple v2) k
            TVRec fields  -> do let vals = map snd . sortBy (comparing fst)
                                let tys = vals fields
                                cmpValues tys
                                  (vals (fromVRecord v1))
                                  (vals (fromVRecord v2)) k

        cmpValues (t : ts) (x1 : xs1) (x2 : xs2) k =
          do x1' <- x1
             x2' <- x2
             cmp t x1' x2' (cmpValues ts xs1 xs2 k)
        cmpValues _ _ _ k = k

    lexCompare :: TValue -> Value -> Value -> Eval Ordering
    lexCompare ty a b = cmpValue op opw op (const op) ty a b (return EQ)
     where
       opw :: BV -> BV -> Eval Ordering -> Eval Ordering
       opw x y k = op (bvVal x) (bvVal y) k

       op :: Ord a => a -> a -> Eval Ordering -> Eval Ordering
       op x y k = case compare x y of
                         EQ  -> k
                         cmp -> return cmp

    signedLexCompare :: TValue -> Value -> Value -> Eval Ordering
    signedLexCompare ty a b = cmpValue opb opw opi (const opi) ty a b (return EQ)
     where
       opb :: Bool -> Bool -> Eval Ordering -> Eval Ordering
       opb _x _y _k = panic "signedLexCompare"
                        ["Attempted to perform signed comparisons on bare Bit type"]

       opw :: BV -> BV -> Eval Ordering -> Eval Ordering
       opw x y k = case compare (signedBV x) (signedBV y) of
                         EQ  -> k
                         cmp -> return cmp

       opi :: Integer -> Integer -> Eval Ordering -> Eval Ordering
       opi _x _y _k = panic "signedLexCompare"
                        ["Attempted to perform signed comparisons on Integer type"]

    -- | Process two elements based on their lexicographic ordering.
    cmpOrder :: String -> (Ordering -> Bool) -> Binary Bool BV Integer
    cmpOrder _nm op ty l r = VBit . op <$> lexCompare ty l r

    -- | Process two elements based on their lexicographic ordering, using signed comparisons
    signedCmpOrder :: String -> (Ordering -> Bool) -> Binary Bool BV Integer
    signedCmpOrder _nm op ty l r = VBit . op <$> signedLexCompare ty l r

    -- Signed arithmetic -----------------------------------------------------------

    -- | Lifted operation on finite bitsequences.  Used
    --   for signed comparisons and arithemtic.
    liftWord :: BitWord b w i
             => (w -> w -> Eval (GenValue b w i))
             -> GenValue b w i
    liftWord op =
      nlam $ \_n ->
      wlam $ \w1 -> return $
      wlam $ \w2 -> op w1 w2

    liftSigned :: (Integer -> Integer -> Integer -> Eval BV)
               -> BinArith BV
    liftSigned _  0    = \_ _ -> return $ mkBv 0 0
    liftSigned op size = f
     where
     f (BV i x) (BV j y)
       | i == j && size == i = op size sx sy
       | otherwise = evalPanic "liftSigned" ["Attempt to compute with words of different sizes"]
       where sx = signedValue i x
             sy = signedValue j y

    signedBV :: BV -> Integer
    signedBV (BV i x) = signedValue i x

    signedValue :: Integer -> Integer -> Integer
    signedValue i x = if testBit x (fromIntegral (i-1)) then x - (1 `shiftL` (fromIntegral i)) else x

    bvSlt :: Integer -> Integer -> Integer -> Eval Value
    bvSlt _sz x y = return . VBit $! (x < y)

    bvSdiv :: Integer -> Integer -> Integer -> Eval BV
    bvSdiv  _ _ 0 = divideByZero
    bvSdiv sz x y = return $! mkBv sz (x `quot` y)

    bvSrem :: Integer -> Integer -> Integer -> Eval BV
    bvSrem  _ _ 0 = divideByZero
    bvSrem sz x y = return $! mkBv sz (x `rem` y)

    sshrV :: Value
    sshrV =
      nlam $ \_n ->
      nlam $ \_k ->
      wlam $ \(BV i x) -> return $
      wlam $ \y ->
       let signx = testBit x (fromIntegral (i-1))
           amt   = fromInteger (bvVal y)
           negv  = (((-1) `shiftL` amt) .|. x) `shiftR` amt
           posv  = x `shiftR` amt
        in return . VWord i . ready . WordVal . mkBv i $! if signx then negv else posv

    -- | Signed carry bit.
    scarryV :: Value
    scarryV =
      nlam $ \_n ->
      wlam $ \(BV i x) -> return $
      wlam $ \(BV j y) ->
        if i == j
          then let z     = x + y
                   xsign = testBit x (fromInteger i - 1)
                   ysign = testBit y (fromInteger i - 1)
                   zsign = testBit z (fromInteger i - 1)
                   sc    = (xsign == ysign) && (xsign /= zsign)
                in return $ VBit sc
          else evalPanic "scarryV" ["Attempted to compute with words of different sizes"]

    -- | Unsigned carry bit.
    carryV :: Value
    carryV =
      nlam $ \_n ->
      wlam $ \(BV i x) -> return $
      wlam $ \(BV j y) ->
        if i == j
          then return . VBit $! testBit (x + y) (fromInteger i)
          else evalPanic "carryV" ["Attempted to compute with words of different sizes"]

    -- Logic -----------------------------------------------------------------------

    zeroV :: forall b w i
           . BitWord b w i
          => TValue
          -> GenValue b w i
    zeroV ty = case ty of

      -- bits
      TVBit ->
        VBit (bitLit False)

      -- integers
      TVInteger ->
        VInteger (integerLit 0)

      -- integers mod n
      TVIntMod _ ->
        VInteger (integerLit 0)

      -- sequences
      TVSeq w ety
          | isTBit ety -> word w 0
          | otherwise  -> VSeq w (IndexSeqMap $ \_ -> ready $ zeroV ety)

      TVStream ety ->
        VStream (IndexSeqMap $ \_ -> ready $ zeroV ety)

      -- functions
      TVFun _ bty ->
        lam (\ _ -> ready (zeroV bty))

      -- tuples
      TVTuple tys ->
        VTuple (map (ready . zeroV) tys)

      -- records
      TVRec fields ->
        VRecord [ (f,ready $ zeroV fty) | (f,fty) <- fields ]

    --  | otherwise = evalPanic "zeroV" ["invalid type for zero"]

    joinWordVal :: BitWord b w i =>
                WordValue b w i -> WordValue b w i -> WordValue b w i
    joinWordVal (WordVal w1) (WordVal w2)
      | wordLen w1 + wordLen w2 < largeBitSize
      = WordVal $ joinWord w1 w2
    joinWordVal (BitsVal xs) (WordVal w2)
      | toInteger (Seq.length xs) + wordLen w2 < largeBitSize
      = BitsVal (xs Seq.>< Seq.fromList (map ready $ unpackWord w2))
    joinWordVal (WordVal w1) (BitsVal ys)
      | wordLen w1 + toInteger (Seq.length ys) < largeBitSize
      = BitsVal (Seq.fromList (map ready $ unpackWord w1) Seq.>< ys)
    joinWordVal (BitsVal xs) (BitsVal ys)
      | toInteger (Seq.length xs) + toInteger (Seq.length ys) < largeBitSize
      = BitsVal (xs Seq.>< ys)
    joinWordVal w1 w2
      = LargeBitsVal (n1+n2) (concatSeqMap n1 (asBitsMap w1) (asBitsMap w2))
     where n1 = wordValueSize w1
           n2 = wordValueSize w2

    joinWords :: forall b w i
               . BitWord b w i
              => Integer
              -> Integer
              -> SeqMap b w i
              -> Eval (GenValue b w i)
    joinWords nParts nEach xs =
      loop (ready $ WordVal (wordLit 0 0)) (enumerateSeqMap nParts xs)

     where
     loop :: Eval (WordValue b w i) -> [Eval (GenValue b w i)] -> Eval (GenValue b w i)
     loop !wv [] = return $ VWord (nParts * nEach) wv
     loop !wv (w : ws) = do
        w >>= \case
          VWord _ w' -> loop (joinWordVal <$> wv <*> w') ws
          _ -> evalPanic "joinWords: expected word value" []

    joinSeq :: BitWord b w i
            => Nat'
            -> Integer
            -> TValue
            -> SeqMap b w i
            -> Eval (GenValue b w i)

    -- Special case for 0 length inner sequences.
    joinSeq _parts 0 a _xs
      = return $ zeroV (TVSeq 0 a)

    -- finite sequence of words
    joinSeq (Nat parts) each TVBit xs
      | parts * each < largeBitSize
      = joinWords parts each xs
      | otherwise
      = do let zs = IndexSeqMap $ \i ->
                      do let (q,r) = divMod i each
                         ys <- fromWordVal "join seq" =<< lookupSeqMap xs q
                         VBit <$> indexWordValue ys (fromInteger r)
           return $ VWord (parts * each) $ ready $ LargeBitsVal (parts * each) zs

    -- infinite sequence of words
    joinSeq Inf each TVBit xs
      = return $ VStream $ IndexSeqMap $ \i ->
          do let (q,r) = divMod i each
             ys <- fromWordVal "join seq" =<< lookupSeqMap xs q
             VBit <$> indexWordValue ys (fromInteger r)

    -- finite or infinite sequence of non-words
    joinSeq parts each _a xs
      = return $ vSeq $ IndexSeqMap $ \i -> do
          let (q,r) = divMod i each
          ys <- fromSeq "join seq" =<< lookupSeqMap xs q
          lookupSeqMap ys r
      where
      len = parts `nMul` (Nat each)
      vSeq = case len of
               Inf    -> VStream
               Nat n  -> VSeq n

    -- | Join a sequence of sequences into a single sequence.
    joinV :: BitWord b w i
          => Nat'
          -> Integer
          -> TValue
          -> GenValue b w i
          -> Eval (GenValue b w i)
    joinV parts each a val = joinSeq parts each a =<< fromSeq "joinV" val

    splitWordVal :: BitWord b w i
                 => Integer
                 -> Integer
                 -> WordValue b w i
                 -> (WordValue b w i, WordValue b w i)
    splitWordVal leftWidth rightWidth (WordVal w) =
      let (lw, rw) = splitWord leftWidth rightWidth w
       in (WordVal lw, WordVal rw)
    splitWordVal leftWidth _rightWidth (BitsVal bs) =
      let (lbs, rbs) = Seq.splitAt (fromInteger leftWidth) bs
       in (BitsVal lbs, BitsVal rbs)
    splitWordVal leftWidth rightWidth (LargeBitsVal _n xs) =
      let (lxs, rxs) = splitSeqMap leftWidth xs
       in (LargeBitsVal leftWidth lxs, LargeBitsVal rightWidth rxs)

    splitAtV :: BitWord b w i
             => Nat'
             -> Nat'
             -> TValue
             -> GenValue b w i
             -> Eval (GenValue b w i)
    splitAtV front back a val =
      case back of

        Nat rightWidth | aBit -> do
              ws <- delay Nothing (splitWordVal leftWidth rightWidth <$> fromWordVal "splitAtV" val)
              return $ VTuple
                       [ VWord leftWidth  . ready . fst <$> ws
                       , VWord rightWidth . ready . snd <$> ws
                       ]

        Inf | aBit -> do
           vs <- delay Nothing (fromSeq "splitAtV" val)
           ls <- delay Nothing (do m <- fst . splitSeqMap leftWidth <$> vs
                                   let ms = map (fromVBit <$>) (enumerateSeqMap leftWidth m)
                                   return $ Seq.fromList $ ms)
           rs <- delay Nothing (snd . splitSeqMap leftWidth <$> vs)
           return $ VTuple [ return $ VWord leftWidth (BitsVal <$> ls)
                           , VStream <$> rs
                           ]

        _ -> do
           vs <- delay Nothing (fromSeq "splitAtV" val)
           ls <- delay Nothing (fst . splitSeqMap leftWidth <$> vs)
           rs <- delay Nothing (snd . splitSeqMap leftWidth <$> vs)
           return $ VTuple [ VSeq leftWidth <$> ls
                           , mkSeq back a <$> rs
                           ]

      where
      aBit = isTBit a

      leftWidth = case front of
        Nat n -> n
        _     -> evalPanic "splitAtV" ["invalid `front` len"]

      -- | 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 :: BitWord b w i
                   => Integer
                   -> Integer
                   -> WordValue b w i
                   -> WordValue b w i
    extractWordVal len start (WordVal w) =
       WordVal $ extractWord len start w
    extractWordVal len start (BitsVal bs) =
       BitsVal $ Seq.take (fromInteger len) $
         Seq.drop (Seq.length bs - fromInteger start - fromInteger len) bs
    extractWordVal len start (LargeBitsVal n xs) =
       let xs' = dropSeqMap (n - start - len) xs
        in LargeBitsVal len xs'

    -- | Split implementation.
    ecSplitV :: BitWord b w i
             => GenValue b w i
    ecSplitV =
      nlam $ \ parts ->
      nlam $ \ each  ->
      tlam $ \ a     ->
      lam  $ \ val ->
        case (parts, each) of
           (Nat p, Nat e) | isTBit a -> do
              ~(VWord _ val') <- val
              return $ VSeq p $ IndexSeqMap $ \i -> do
                return $ VWord e (extractWordVal e ((p-i-1)*e) <$> val')
           (Inf, Nat e) | isTBit a -> do
              val' <- delay Nothing (fromSeq "ecSplitV" =<< val)
              return $ VStream $ IndexSeqMap $ \i ->
                return $ VWord e $ return $ BitsVal $ Seq.fromFunction (fromInteger e) $ \j ->
                  let idx = i*e + toInteger j
                   in idx `seq` do
                          xs <- val'
                          fromVBit <$> lookupSeqMap xs idx
           (Nat p, Nat e) -> do
              val' <- delay Nothing (fromSeq "ecSplitV" =<< val)
              return $ VSeq p $ IndexSeqMap $ \i ->
                return $ VSeq e $ IndexSeqMap $ \j -> do
                  xs <- val'
                  lookupSeqMap xs (e * i + j)
           (Inf  , Nat e) -> do
              val' <- delay Nothing (fromSeq "ecSplitV" =<< val)
              return $ VStream $ IndexSeqMap $ \i ->
                return $ VSeq e $ IndexSeqMap $ \j -> do
                  xs <- val'
                  lookupSeqMap xs (e * i + j)
           _              -> evalPanic "splitV" ["invalid type arguments to split"]

    reverseV :: forall b w i
              . BitWord b w i
             => GenValue b w i
             -> Eval (GenValue b w i)
    reverseV (VSeq n xs) =
      return $ VSeq n $ reverseSeqMap n xs
    reverseV (VWord n wv) = return (VWord n (revword <$> wv))
     where
     revword (WordVal w)         = BitsVal $ Seq.reverse $ Seq.fromList $ map ready $ unpackWord w
     revword (BitsVal bs)        = BitsVal $ Seq.reverse bs
     revword (LargeBitsVal m xs) = LargeBitsVal m $ reverseSeqMap m xs
    reverseV _ =
      evalPanic "reverseV" ["Not a finite sequence"]

    transposeV :: BitWord b w i
               => Nat'
               -> Nat'
               -> TValue
               -> GenValue b w i
               -> Eval (GenValue b w i)
    transposeV a b c xs
      | isTBit c, Nat na <- a = -- Fin a => [a][b]Bit -> [b][a]Bit
          return $ bseq $ IndexSeqMap $ \bi ->
            return $ VWord na $ return $ BitsVal $
              Seq.fromFunction (fromInteger na) $ \ai -> do
                ys <- flip lookupSeqMap (toInteger ai) =<< fromSeq "transposeV" xs
                case ys of
                  VStream ys' -> fromVBit <$> lookupSeqMap ys' bi
                  VWord _ wv  -> flip indexWordValue bi =<< wv
                  _ -> evalPanic "transpose" ["expected sequence of bits"]

      | isTBit c, Inf <- a = -- [inf][b]Bit -> [b][inf]Bit
          return $ bseq $ IndexSeqMap $ \bi ->
            return $ VStream $ IndexSeqMap $ \ai ->
             do ys <- flip lookupSeqMap ai =<< fromSeq "transposeV" xs
                case ys of
                  VStream ys' -> VBit . fromVBit <$> lookupSeqMap ys' bi
                  VWord _ wv  -> VBit <$> (flip indexWordValue bi =<< wv)
                  _ -> evalPanic "transpose" ["expected sequence of bits"]

      | otherwise = -- [a][b]c -> [b][a]c
          return $ bseq $ IndexSeqMap $ \bi ->
            return $ aseq $ IndexSeqMap $ \ai -> do
              ys  <- flip lookupSeqMap ai =<< fromSeq "transposeV 1" xs
              z   <- flip lookupSeqMap bi =<< fromSeq "transposeV 2" ys
              return z

     where
      bseq =
            case b of
              Nat nb -> VSeq nb
              Inf    -> VStream
      aseq =
            case a of
              Nat na -> VSeq na
              Inf    -> VStream

    ccatV :: (Show b, Show w, BitWord b w i)
          => Nat'
          -> Nat'
          -> TValue
          -> (GenValue b w i)
          -> (GenValue b w i)
          -> Eval (GenValue b w i)

    ccatV _front _back _elty (VWord m l) (VWord n r) =
      return $ VWord (m+n) (joinWordVal <$> l <*> r)

    ccatV _front _back _elty (VWord m l) (VStream r) = do
      l' <- delay Nothing l
      return $ VStream $ IndexSeqMap $ \i ->
        if i < m then
          VBit <$> (flip indexWordValue i =<< l')
        else
          lookupSeqMap r (i-m)

    ccatV front back elty l r = do
           l'' <- delay Nothing (fromSeq "ccatV left" l)
           r'' <- delay Nothing (fromSeq "ccatV right" r)
           let Nat n = front
           mkSeq (evalTF TCAdd [front,back]) elty <$> return (IndexSeqMap $ \i ->
            if i < n then do
             ls <- l''
             lookupSeqMap ls i
            else do
             rs <- r''
             lookupSeqMap rs (i-n))

    wordValLogicOp :: BitWord b w i
                   => (b -> b -> b)
                   -> (w -> w -> w)
                   -> WordValue b w i
                   -> WordValue b w i
                   -> Eval (WordValue b w i)
    wordValLogicOp _ wop (WordVal w1) (WordVal w2) = return $ WordVal (wop w1 w2)
    wordValLogicOp bop _ (BitsVal xs) (BitsVal ys) =
      BitsVal <$> sequence (Seq.zipWith (\x y -> delay Nothing (bop <$> x <*> y)) xs ys)
    wordValLogicOp bop _ (WordVal w1) (BitsVal ys) =
      ready $ BitsVal $ Seq.zipWith (\x y -> bop <$> x <*> y) (Seq.fromList $ map ready $ unpackWord w1) ys
    wordValLogicOp bop _ (BitsVal xs) (WordVal w2) =
      ready $ BitsVal $ Seq.zipWith (\x y -> bop <$> x <*> y) xs (Seq.fromList $ map ready $ unpackWord w2)
    wordValLogicOp bop _ w1 w2 = LargeBitsVal (wordValueSize w1) <$> zs
         where zs = memoMap $ IndexSeqMap $ \i -> op <$> (lookupSeqMap xs i) <*> (lookupSeqMap ys i)
               xs = asBitsMap w1
               ys = asBitsMap w2
               op x y = VBit (bop (fromVBit x) (fromVBit y))

    -- | Merge two values given a binop.  This is used for and, or and xor.
    logicBinary :: forall b w i
                 . BitWord b w i
                => (b -> b -> b)
                -> (w -> w -> w)
                -> Binary b w i
    logicBinary opb opw = loop
      where
      loop' :: TValue
            -> Eval (GenValue b w i)
            -> Eval (GenValue b w i)
            -> Eval (GenValue b w i)
      loop' ty l r = join (loop ty <$> l <*> r)

      loop :: TValue
            -> GenValue b w i
            -> GenValue b w i
            -> Eval (GenValue b w i)

      loop ty l r = case ty of
        TVBit -> return $ VBit (opb (fromVBit l) (fromVBit r))
        TVInteger -> evalPanic "logicBinary" ["Integer not in class Logic"]
        TVIntMod _ -> evalPanic "logicBinary" ["Z not in class Logic"]
        TVSeq w aty
             -- words
             | isTBit aty
                  -> do v <- delay Nothing $ join
                                (wordValLogicOp opb opw <$>
                                        fromWordVal "logicBinary l" l <*>
                                        fromWordVal "logicBinary r" r)
                        return $ VWord w v

             -- finite sequences
             | otherwise -> VSeq w <$>
                               (join (zipSeqMap (loop aty) <$>
                                        (fromSeq "logicBinary left" l)
                                        <*> (fromSeq "logicBinary right" r)))

        TVStream aty ->
            VStream <$> (join (zipSeqMap (loop aty) <$>
                              (fromSeq "logicBinary left" l) <*>
                              (fromSeq "logicBinary right" r)))

        TVTuple etys -> do
            ls <- mapM (delay Nothing) (fromVTuple l)
            rs <- mapM (delay Nothing) (fromVTuple r)
            return $ VTuple $ zipWith3 loop' etys ls rs

        TVFun _ bty ->
            return $ lam $ \ a -> loop' bty (fromVFun l a) (fromVFun r a)

        TVRec fields ->
            do fs <- sequence
                       [ (f,) <$> delay Nothing (loop' fty a b)
                       | (f,fty) <- fields
                       , let a = lookupRecord f l
                             b = lookupRecord f r
                       ]
               return $ VRecord fs

    wordValUnaryOp :: BitWord b w i
                   => (b -> b)
                   -> (w -> w)
                   -> WordValue b w i
                   -> Eval (WordValue b w i)
    wordValUnaryOp _ wop (WordVal w)  = return $ WordVal (wop w)
    wordValUnaryOp bop _ (BitsVal bs) = return $ BitsVal (fmap (bop <$>) bs)
    wordValUnaryOp bop _ (LargeBitsVal n xs) = LargeBitsVal n <$> mapSeqMap f xs
      where f x = VBit . bop <$> fromBit x

    logicUnary :: forall b w i
                . BitWord b w i
               => (b -> b)
               -> (w -> w)
               -> Unary b w i
    logicUnary opb opw = loop
      where
      loop' :: TValue -> Eval (GenValue b w i) -> Eval (GenValue b w i)
      loop' ty val = loop ty =<< val

      loop :: TValue -> GenValue b w i -> Eval (GenValue b w i)
      loop ty val = case ty of
        TVBit -> return . VBit . opb $ fromVBit val

        TVInteger -> evalPanic "logicUnary" ["Integer not in class Logic"]
        TVIntMod _ -> evalPanic "logicUnary" ["Z not in class Logic"]

        TVSeq w ety
             -- words
             | isTBit ety
                  -> do v <- delay Nothing (wordValUnaryOp opb opw =<< fromWordVal "logicUnary" val)
                        return $ VWord w v

             -- finite sequences
             | otherwise
                  -> VSeq w <$> (mapSeqMap (loop ety) =<< fromSeq "logicUnary" val)

             -- streams
        TVStream ety ->
             VStream <$> (mapSeqMap (loop ety) =<< fromSeq "logicUnary" val)

        TVTuple etys ->
          do as <- mapM (delay Nothing) (fromVTuple val)
             return $ VTuple (zipWith loop' etys as)

        TVFun _ bty ->
          return $ lam $ \ a -> loop' bty (fromVFun val a)

        TVRec fields ->
          do fs <- sequence
                     [ (f,) <$> delay Nothing (loop' fty a)
                     | (f,fty) <- fields, let a = lookupRecord f val
                     ]
             return $ VRecord fs

    logicShift :: (Integer -> Integer -> Integer -> Integer)
                  -- ^ The function may assume its arguments are masked.
                  -- It is responsible for masking its result if needed.
               -> (Integer -> Seq.Seq (Eval Bool) -> Integer -> Seq.Seq (Eval Bool))
               -> (Nat' -> TValue -> SeqValMap -> Integer -> SeqValMap)
               -> Value
    logicShift opW obB opS
      = nlam $ \ a ->
        nlam $ \ _ ->
        tlam $ \ c ->
         lam  $ \ l -> return $
         lam  $ \ r -> do
            BV _ i <- fromVWord "logicShift amount" =<< r
            l >>= \case
              VWord w wv -> return $ VWord w $ wv >>= \case
                              WordVal (BV _ x) -> return $ WordVal (BV w (opW w x i))
                              BitsVal bs -> return $ BitsVal (obB w bs i)
                              LargeBitsVal n xs -> return $ LargeBitsVal n $ opS (Nat n) c xs i

              _ -> mkSeq a c <$> (opS a c <$> (fromSeq "logicShift" =<< l) <*> return i)

    -- Left shift for words.
    shiftLW :: Integer -> Integer -> Integer -> Integer
    shiftLW w ival by
      | by >= w   = 0
      | otherwise = mask w (shiftL ival (fromInteger by))

    shiftLB :: Integer -> Seq.Seq (Eval Bool) -> Integer -> Seq.Seq (Eval Bool)
    shiftLB w bs by =
      Seq.drop (fromInteger (min w by)) bs
      Seq.><
      Seq.replicate (fromInteger (min w by)) (ready False)

    shiftLS :: Nat' -> TValue -> SeqValMap -> Integer -> SeqValMap
    shiftLS w ety vs by = IndexSeqMap $ \i ->
      case w of
        Nat len
          | i+by < len -> lookupSeqMap vs (i+by)
          | i    < len -> return $ zeroV ety
          | otherwise  -> evalPanic "shiftLS" ["Index out of bounds"]
        Inf            -> lookupSeqMap vs (i+by)

    shiftRW :: Integer -> Integer -> Integer -> Integer
    shiftRW w i by
      | by >= w   = 0
      | otherwise = shiftR i (fromInteger by)

    shiftRB :: Integer -> Seq.Seq (Eval Bool) -> Integer -> Seq.Seq (Eval Bool)
    shiftRB w bs by =
      Seq.replicate (fromInteger (min w by)) (ready False)
      Seq.><
      Seq.take (fromInteger (w - min w by)) bs

    shiftRS :: Nat' -> TValue -> SeqValMap -> Integer -> SeqValMap
    shiftRS w ety vs by = IndexSeqMap $ \i ->
      case w of
        Nat len
          | i >= by   -> lookupSeqMap vs (i-by)
          | i < len   -> return $ zeroV ety
          | otherwise -> evalPanic "shiftLS" ["Index out of bounds"]
        Inf
          | i >= by   -> lookupSeqMap vs (i-by)
          | otherwise -> return $ zeroV ety

    -- XXX integer doesn't implement rotateL, as there's no bit bound
    rotateLW :: Integer -> Integer -> Integer -> Integer
    rotateLW 0 i _  = i
    rotateLW w i by = mask w $ (i `shiftL` b) .|. (i `shiftR` (fromInteger w - b))
      where b = fromInteger (by `mod` w)

    rotateLB :: Integer -> Seq.Seq (Eval Bool) -> Integer -> Seq.Seq (Eval Bool)
    rotateLB w bs by =
      let (hd,tl) = Seq.splitAt (fromInteger (by `mod` w)) bs
       in tl Seq.>< hd

    rotateLS :: Nat' -> TValue -> SeqValMap -> Integer -> SeqValMap
    rotateLS w _ vs by = IndexSeqMap $ \i ->
      case w of
        Nat len -> lookupSeqMap vs ((by + i) `mod` len)
        _ -> panic "Cryptol.Eval.Prim.rotateLS" [ "unexpected infinite sequence" ]

    -- XXX integer doesn't implement rotateR, as there's no bit bound
    rotateRW :: Integer -> Integer -> Integer -> Integer
    rotateRW 0 i _  = i
    rotateRW w i by = mask w $ (i `shiftR` b) .|. (i `shiftL` (fromInteger w - b))
      where b = fromInteger (by `mod` w)

    rotateRB :: Integer -> Seq.Seq (Eval Bool) -> Integer -> Seq.Seq (Eval Bool)
    rotateRB w bs by =
      let (hd,tl) = Seq.splitAt (fromInteger (w - (by `mod` w))) bs
       in tl Seq.>< hd

    rotateRS :: Nat' -> TValue -> SeqValMap -> Integer -> SeqValMap
    rotateRS w _ vs by = IndexSeqMap $ \i ->
      case w of
        Nat len -> lookupSeqMap vs ((len - by + i) `mod` len)
        _ -> panic "Cryptol.Eval.Prim.rotateRS" [ "unexpected infinite sequence" ]

    -- Sequence Primitives ---------------------------------------------------------

    -- | Indexing operations.
    indexPrim :: BitWord b w i
              => (Maybe Integer -> TValue -> SeqMap b w i -> Seq.Seq b -> Eval (GenValue b w i))
              -> (Maybe Integer -> TValue -> SeqMap b w i -> w -> Eval (GenValue b w i))
              -> GenValue b w i
    indexPrim bits_op word_op =
      nlam $ \ n  ->
      tlam $ \ a ->
      nlam $ \ _i ->
       lam $ \ l  -> return $
       lam $ \ r  -> do
          vs <- l >>= \case
                   VWord _ w  -> w >>= \w' -> return $ IndexSeqMap (\i -> VBit <$> indexWordValue w' i)
                   VSeq _ vs  -> return vs
                   VStream vs -> return vs
                   _ -> evalPanic "Expected sequence value" ["indexPrim"]
          r >>= \case
             VWord _ w -> w >>= \case
               WordVal w' -> word_op (fromNat n) a vs w'
               BitsVal bs -> bits_op (fromNat n) a vs =<< sequence bs
               LargeBitsVal m xs -> bits_op (fromNat n) a vs . Seq.fromList =<< traverse (fromBit =<<) (enumerateSeqMap m xs)
             _ -> evalPanic "Expected word value" ["indexPrim"]

    indexFront :: Maybe Integer -> TValue -> SeqValMap -> BV -> Eval Value
    indexFront mblen _a vs (bvVal -> ix) =
      case mblen of
        Just len | len <= ix -> invalidIndex ix
        _                    -> lookupSeqMap vs ix

    indexFront_bits :: Maybe Integer -> TValue -> SeqValMap -> Seq.Seq Bool -> Eval Value
    indexFront_bits mblen a vs = indexFront mblen a vs . packWord . Fold.toList

    indexBack :: Maybe Integer -> TValue -> SeqValMap -> BV -> Eval Value
    indexBack mblen _a vs (bvVal -> ix) =
      case mblen of
        Just len | len > ix  -> lookupSeqMap vs (len - ix - 1)
                 | otherwise -> invalidIndex ix
        Nothing              -> evalPanic "indexBack"
                                ["unexpected infinite sequence"]

    indexBack_bits :: Maybe Integer -> TValue -> SeqValMap -> Seq.Seq Bool -> Eval Value
    indexBack_bits mblen a vs = indexBack mblen a vs . packWord . Fold.toList

    updateFront
      :: Nat'
      -> TValue
      -> SeqMap Bool BV Integer
      -> WordValue Bool BV Integer
      -> Eval (GenValue Bool BV Integer)
      -> Eval (SeqMap Bool BV Integer)
    updateFront len _eltTy vs w val = do
      idx <- bvVal <$> asWordVal w
      case len of
        Inf -> return ()
        Nat n -> unless (idx < n) (invalidIndex idx)
      return $ updateSeqMap vs idx val

    updateFront_word
     :: Nat'
     -> TValue
     -> WordValue Bool BV Integer
     -> WordValue Bool BV Integer
     -> Eval (GenValue Bool BV Integer)
     -> Eval (WordValue Bool BV Integer)
    updateFront_word _len _eltTy bs w val = do
      idx <- bvVal <$> asWordVal w
      updateWordValue bs idx (fromBit =<< val)

    updateBack
      :: Nat'
      -> TValue
      -> SeqMap Bool BV Integer
      -> WordValue Bool BV Integer
      -> Eval (GenValue Bool BV Integer)
      -> Eval (SeqMap Bool BV Integer)
    updateBack Inf _eltTy _vs _w _val =
      evalPanic "Unexpected infinite sequence in updateEnd" []
    updateBack (Nat n) _eltTy vs w val = do
      idx <- bvVal <$> asWordVal w
      unless (idx < n) (invalidIndex idx)
      return $ updateSeqMap vs (n - idx - 1) val

    updateBack_word
     :: Nat'
     -> TValue
     -> WordValue Bool BV Integer
     -> WordValue Bool BV Integer
     -> Eval (GenValue Bool BV Integer)
     -> Eval (WordValue Bool BV Integer)
    updateBack_word Inf _eltTy _bs _w _val =
      evalPanic "Unexpected infinite sequence in updateEnd" []
    updateBack_word (Nat n) _eltTy bs w val = do
      idx <- bvVal <$> asWordVal w
      updateWordValue bs (n - idx - 1) (fromBit =<< val)

    {-
      idx <- bvVal <$> asWordVal w
      unless (idx < n) (invalidIndex idx)
      let idx' = n - idx - 1
      return $! Seq.update (fromInteger idx') (fromVBit <$> val) bs
    -}

    updatePrim
         :: BitWord b w i
         => (Nat' -> TValue -> WordValue b w i -> WordValue b w i -> Eval (GenValue b w i) -> Eval (WordValue b w i))
         -> (Nat' -> TValue -> SeqMap b w i    -> WordValue b w i -> Eval (GenValue b w i) -> Eval (SeqMap b w i))
         -> GenValue b w i
    updatePrim updateWord updateSeq =
      nlam $ \len ->
      tlam $ \eltTy ->
      nlam $ \_idxLen ->
      lam $ \xs  -> return $
      lam $ \idx -> return $
      lam $ \val -> do
        idx' <- fromWordVal "update" =<< idx
        xs >>= \case
          VWord l w  -> do w' <- delay Nothing w
                           return $ VWord l (w' >>= \w'' -> updateWord len eltTy w'' idx' val)
          VSeq l vs  -> VSeq l  <$> updateSeq len eltTy vs idx' val
          VStream vs -> VStream <$> updateSeq len eltTy vs idx' val
          _ -> evalPanic "Expected sequence value" ["updatePrim"]

    -- @[ 0, 1 .. ]@
    fromThenV :: BitWord b w i
              => GenValue b w i
    fromThenV  =
      nlam $ \ first ->
      nlam $ \ next  ->
      nlam $ \ bits  ->
      nlam $ \ len   ->
        case (first, next, len, bits) of
          (_         , _        , _       , Nat bits')
            | bits' >= Arch.maxBigIntWidth -> wordTooWide bits'
          (Nat first', Nat next', Nat len', Nat bits') ->
            let diff = next' - first'
             in VSeq len' $ IndexSeqMap $ \i ->
                    ready $ VWord bits' $ return $
                      WordVal $ wordLit bits' (first' + i*diff)
          _ -> evalPanic "fromThenV" ["invalid arguments"]

    -- @[ 0 .. 10 ]@
    fromToV :: BitWord b w i
            => GenValue b w i
    fromToV  =
      nlam $ \ first ->
      nlam $ \ lst   ->
      tlam $ \ ty    ->
        let !f = mkLit ty in
        case (first, lst) of
          (Nat first', Nat lst') ->
            let len = 1 + (lst' - first')
            in VSeq len $ IndexSeqMap $ \i -> ready $ f (first' + i)
          _ -> evalPanic "fromToV" ["invalid arguments"]

    -- @[ 0, 1 .. 10 ]@
    fromThenToV :: BitWord b w i
                => GenValue b w i
    fromThenToV  =
      nlam $ \ first ->
      nlam $ \ next  ->
      nlam $ \ lst   ->
      tlam $ \ ty    ->
      nlam $ \ len   ->
        let !f = mkLit ty in
        case (first, next, lst, len) of
          (Nat first', Nat next', Nat _lst', Nat len') ->
            let diff = next' - first'
            in VSeq len' $ IndexSeqMap $ \i -> ready $ f (first' + i*diff)
          _ -> evalPanic "fromThenToV" ["invalid arguments"]

    infFromV :: BitWord b w i => GenValue b w i
    infFromV =
      tlam $ \ ty ->
      lam  $ \ x' ->
      return $ VStream $ IndexSeqMap $ \i ->
      do x <- x'
         addV ty x (intV (integerLit i) ty)

    infFromThenV :: BitWord b w i => GenValue b w i
    infFromThenV =
      tlam $ \ ty ->
      lam $ \ first -> return $
      lam $ \ next ->
      do x <- first
         y <- next
         d <- subV ty y x
         return $ VStream $ IndexSeqMap $ \i ->
           addV ty x =<< mulV ty d (intV (integerLit i) ty)

    -- Random Values ---------------------------------------------------------------

    -- | Produce a random value with the given seed. If we do not support
    -- making values of the given type, return zero of that type.
    -- TODO: do better than returning zero
    randomV :: BitWord b w i => TValue -> Integer -> GenValue b w i
    randomV ty seed =
      case randomValue (tValTy ty) of
        Nothing -> zeroV ty
        Just gen ->
          -- unpack the seed into four Word64s
          let mask64 = 0xFFFFFFFFFFFFFFFF
              unpack s = fromIntegral (s .&. mask64) : unpack (s `shiftR` 64)
              [a, b, c, d] = take 4 (unpack seed)
          in fst $ gen 100 $ seedTFGen (a, b, c, d)

    -- Miscellaneous ---------------------------------------------------------------

    errorV :: forall b w i
           . BitWord b w i
          => TValue
          -> String
          -> Eval (GenValue b w i)
    errorV ty msg = case ty of
      -- bits
      TVBit -> cryUserError msg
      TVInteger -> cryUserError msg
      TVIntMod _ -> cryUserError msg

      -- sequences
      TVSeq w ety
         | isTBit ety -> return $ VWord w $ return $ BitsVal $
                             Seq.replicate (fromInteger w) (cryUserError msg)
         | otherwise  -> return $ VSeq w (IndexSeqMap $ \_ -> errorV ety msg)

      TVStream ety ->
        return $ VStream (IndexSeqMap $ \_ -> errorV ety msg)

      -- functions
      TVFun _ bty ->
        return $ lam (\ _ -> errorV bty msg)

      -- tuples
      TVTuple tys ->
        return $ VTuple (map (flip errorV msg) tys)

      -- records
      TVRec fields ->
        return $ VRecord [ (f,errorV fty msg) | (f,fty) <- fields ]