WIP. New monadic Cryptol interpreter.

The concrete evaluator now seems to be working correctly, but seems to suffer from major performace problems.
2024-11-30 23:45:23 +03:00 · 2016-05-12 18:44:06 -07:00 · 2016-05-12 18:44:06 -07:00 · 7e968d2d18
commit 7e968d2d18
parent 9d11fd4485
24 changed files with 1033 additions and 523 deletions
--- a/cryptol.cabal
+++ b/cryptol.cabal
@ -146,7 +146,7 @@ library
                       Cryptol.Eval,
                       Cryptol.Eval.Arch,
                       Cryptol.Eval.Env,
-                       Cryptol.Eval.Error,
+                       Cryptol.Eval.Monad,
                       Cryptol.Eval.Type,
                       Cryptol.Eval.Value,

--- a/lib/Cryptol.cry
+++ b/lib/Cryptol.cry
@ -212,7 +212,6 @@ primitive (#) : {front, back, a} (fin front) => [front]a -> [back]a
 */
 primitive splitAt : {front, back, a} (fin front) => [front + back]a
                                                 -> ([front]a, [back]a)
-
 /**
 * Joins sequences.
 */
@ -333,3 +332,12 @@ groupBy = split`{parts=parts}
 * Define the base 2 logarithm function in terms of width
 */
 type lg2 n = width (max n 1 - 1)
+
+/**
+ * Debugging function for tracing values.  The value of the 
+ * first argument is printed before returning the second value.
+ */
+primitive trace : {n, a, b} [n][8] -> a -> b -> b
+
+traceVal : {n, a, b} [n][8] -> a -> a
+traceVal msg x = trace msg x x
--- a/src/Cryptol/Eval.hs
+++ b/src/Cryptol/Eval.hs
@ -6,6 +6,8 @@
 -- Stability   :  provisional
 -- Portability :  portable

+{-# LANGUAGE DoAndIfThenElse #-}
+{-# LANGUAGE LambdaCase #-}
 {-# LANGUAGE Safe #-}
 {-# LANGUAGE PatternGuards #-}

@ -16,19 +18,25 @@ module Cryptol.Eval (
  , evalExpr
  , evalDecls
  , EvalError(..)
-  , WithBase(..)
+--  , WithBase(..)
  ) where

-import Cryptol.Eval.Error
 import Cryptol.Eval.Env
+import Cryptol.Eval.Monad
 import Cryptol.Eval.Type
 import Cryptol.Eval.Value
 import Cryptol.ModuleSystem.Name
 import Cryptol.TypeCheck.AST
+import Cryptol.TypeCheck.Solver.InfNat(Nat'(..))
+import Cryptol.Utils.Ident (Ident)
 import Cryptol.Utils.Panic (panic)
 import Cryptol.Utils.PP
 import Cryptol.Prims.Eval

+import           Control.Monad
+import           Control.Monad.Fix
+import           Data.IORef
+import           Data.List
 import qualified Data.Map as Map

 import Prelude ()
@ -36,46 +44,66 @@ import Prelude.Compat

 -- Expression Evaluation -------------------------------------------------------

-moduleEnv :: Module -> EvalEnv -> EvalEnv
-moduleEnv m env = evalDecls (mDecls m) (evalNewtypes (mNewtypes m) env)
+moduleEnv :: Module -> EvalEnv -> Eval EvalEnv
+moduleEnv m env = evalDecls (mDecls m) =<< evalNewtypes (mNewtypes m) env

-evalExpr :: EvalEnv -> Expr -> Value
+evalExpr :: EvalEnv -> Expr -> Eval Value
 evalExpr env expr = case expr of

-  EList es ty -> VSeq (isTBit (evalType env ty)) (map (evalExpr env) es)
+  EList es ty ->
+    VSeq (genericLength es) (isTBit (evalType env ty))
+       <$> finiteSeqMap (map (evalExpr env) es)

-  ETuple es -> VTuple (map eval es)
+  ETuple es -> return $ VTuple (map eval es)

-  ERec fields -> VRecord [ (f,eval e) | (f,e) <- fields ]
+  ERec fields -> return $ VRecord [ (f,eval e) | (f,e) <- fields ]

-  ESel e sel -> evalSel env e sel
+  ESel e sel -> eval e >>= \e' -> evalSel e' sel

-  EIf c t f | fromVBit (eval c) -> eval t
-            | otherwise         -> eval f
+  EIf c t f -> do
+     b <- fromVBit <$> eval c
+     if b then
+       eval t
+     else
+       eval f

-  EComp l h gs -> evalComp env (evalType env l) h gs
+  EComp n t h gs -> do
+      --io $ putStrLn $ "Eval comp"
+      let len  = evalType env n
+      let elty = evalType env t
+      --io $ putStrLn $ "at type: " ++ show (pp (tSeq (tValTy len) (tValTy elty)))
+      z <- evalComp env len elty h gs
+      --io $ putStrLn $ "Done with comp eval"
+      return z

-  EVar n -> case lookupVar n env of
-    Just val -> val
-    Nothing  -> panic "[Eval] evalExpr"
+  EVar n -> do
+    case lookupVar n env of
+      Just val -> val
+      Nothing  -> do
+        envdoc <- ppEnv defaultPPOpts env
+        panic "[Eval] evalExpr"
                     ["var `" ++ show (pp n) ++ "` is not defined"
-                     , pretty (WithBase defaultPPOpts env)
+                     , show envdoc
                     ]

-  ETAbs tv b -> VPoly $ \ty -> evalExpr (bindType (tpVar tv) ty env) b
+  ETAbs tv b -> return $ VPoly $ \ty -> evalExpr (bindType (tpVar tv) ty env) b

-  ETApp e ty -> case eval e of
-    VPoly f -> f (evalType env ty)
-    val     -> panic "[Eval] evalExpr"
-                    ["expected a polymorphic value"
-                    , show (ppV val), show e, show ty
-                    ]
+  ETApp e ty -> do
+    eval e >>= \case
+      VPoly f -> f $ (evalType env ty)
+      val     -> do vdoc <- ppV val
+                    panic "[Eval] evalExpr"
+                      ["expected a polymorphic value"
+                      , show vdoc, show e, show ty
+                      ]

-  EApp f x -> case eval f of
-    VFun f' -> f' (eval x)
-    it       -> panic "[Eval] evalExpr" ["not a function", show (ppV it) ]
+  EApp f x -> do
+    eval f >>= \case
+      VFun f' -> f' (eval x)
+      it      -> do itdoc <- ppV it
+                    panic "[Eval] evalExpr" ["not a function", show itdoc ]

-  EAbs n _ty b -> VFun (\ val -> evalExpr (bindVar n val env) b )
+  EAbs n _ty b -> return $ VFun (\val -> bindVar n val env >>= \env' -> evalExpr env' b )

  -- XXX these will likely change once there is an evidence value
  EProofAbs _ e -> evalExpr env e
@ -83,7 +111,9 @@ evalExpr env expr = case expr of

  ECast e _ty -> evalExpr env e

-  EWhere e ds -> evalExpr (evalDecls ds env) e
+  EWhere e ds -> do
+     env' <- evalDecls ds env
+     evalExpr env' e

  where

@ -94,12 +124,12 @@ evalExpr env expr = case expr of

 -- Newtypes --------------------------------------------------------------------

-evalNewtypes :: Map.Map Name Newtype -> EvalEnv -> EvalEnv
-evalNewtypes nts env = Map.foldl (flip evalNewtype) env nts
+evalNewtypes :: Map.Map Name Newtype -> EvalEnv -> Eval EvalEnv
+evalNewtypes nts env = foldM (flip evalNewtype) env $ Map.elems nts

 -- | Introduce the constructor function for a newtype.
-evalNewtype :: Newtype -> EvalEnv -> EvalEnv
-evalNewtype nt = bindVar (ntName nt) (foldr tabs con (ntParams nt))
+evalNewtype :: Newtype -> EvalEnv -> Eval EvalEnv
+evalNewtype nt = bindVar (ntName nt) (return (foldr tabs con (ntParams nt)))
  where
  tabs _tp body = tlam (\ _ -> body)
  con           = VFun id
@ -107,58 +137,88 @@ evalNewtype nt = bindVar (ntName nt) (foldr tabs con (ntParams nt))

 -- Declarations ----------------------------------------------------------------

-evalDecls :: [DeclGroup] -> EvalEnv -> EvalEnv
-evalDecls dgs env = foldl (flip evalDeclGroup) env dgs
+evalDecls :: [DeclGroup] -> EvalEnv -> Eval EvalEnv
+evalDecls dgs env = foldM (flip evalDeclGroup) env dgs

-evalDeclGroup :: DeclGroup -> EvalEnv -> EvalEnv
-evalDeclGroup dg env = env'
-  where
-  -- the final environment is passed in for each declaration, to permit
-  -- recursive values.
-  env' = case dg of
-    Recursive ds   -> foldr (evalDecl env') env ds
-    NonRecursive d -> evalDecl env d env
+evalDeclGroup :: DeclGroup -> EvalEnv -> Eval EvalEnv
+evalDeclGroup dg env = do
+  --io $ putStrLn $ "evalDeclGroup"
+  case dg of
+    Recursive ds   -> do
+      --io $ putStrLn "recursive decl group"
+      holes <- mapM declHole ds
+      let holeEnv = Map.fromList $ [ (nm,h) | (nm,h,_) <- holes ]
+      let env' = env `mappend` emptyEnv{ envVars = holeEnv }
+      --io $ putStrLn "evaluating defns"
+      env'' <- foldM (flip (evalDecl env')) env ds
+      mapM_ (fillHole env'') holes
+      --io $ putStrLn $ "Finish recursive decl group"
+      return env'

-evalDecl :: ReadEnv -> Decl -> EvalEnv -> EvalEnv
+    NonRecursive d -> do
+      evalDecl env d env
+
+fillHole :: EvalEnv -> (Name, Eval Value, Eval Value -> Eval ()) -> Eval ()
+fillHole env (nm, _, fill) = do
+  case lookupVar nm env of
+    Nothing -> evalPanic "fillHole" ["Recursive definition not completed", show (ppLocName nm)]
+    Just x  -> fill =<< delay (Just (show (ppLocName nm))) x
+
+declHole :: Decl -> Eval (Name, Eval Value, Eval Value -> Eval ())
+declHole d =
+  case dDefinition d of
+    DPrim   -> evalPanic "Unexpected primitive declaration in recursive group" [show (ppLocName nm)]
+    DExpr e -> do
+      (hole, fill) <- blackhole msg
+      return (nm, hole, fill)
+ where
+ nm = dName d
+ msg = unwords ["<<loop>> while evaluating", show (pp nm)]
+  
+
+evalDecl :: ReadEnv -> Decl -> EvalEnv -> Eval EvalEnv
 evalDecl renv d =
  bindVar (dName d) $
    case dDefinition d of
-      DPrim   -> evalPrim d
+      DPrim   -> return $ evalPrim d
      DExpr e -> evalExpr renv e


 -- Selectors -------------------------------------------------------------------

-evalSel :: ReadEnv -> Expr -> Selector -> Value
-evalSel env e sel = case sel of
+evalSel :: Value -> Selector -> Eval Value
+evalSel val sel = case sel of

  TupleSel n _  -> tupleSel n val
  RecordSel n _ -> recordSel n val
-  ListSel ix _  -> fromSeq val !! ix
+  ListSel ix _  -> do xs <- fromSeq val
+                      lookupSeqMap xs (toInteger ix)

  where

-  val = evalExpr env e
-
+  tupleSel :: Int -> Value -> Eval Value
  tupleSel n v =
    case v of
-      VTuple vs     -> vs !! n
-      VSeq False vs -> VSeq False [ tupleSel n v1 | v1 <- vs ]
-      VStream vs    -> VStream [ tupleSel n v1 | v1 <- vs ]
-      VFun f        -> VFun (\x -> tupleSel n (f x))
-      _             -> evalPanic "Cryptol.Eval.evalSel"
-                          [ "Unexpected value in tuple selection"
-                          , show (ppValue defaultPPOpts v) ]
+      VTuple vs       -> vs !! n
+      VSeq w False vs -> VSeq w False <$> mapSeqMap (tupleSel n) vs
+      VStream vs      -> VStream <$> mapSeqMap (tupleSel n) vs
+      VFun f          -> return $ VFun (\x -> tupleSel n =<< f x)
+      _               -> do vdoc <- ppValue defaultPPOpts v
+                            evalPanic "Cryptol.Eval.evalSel"
+                             [ "Unexpected value in tuple selection"
+                             , show vdoc ]

+  recordSel :: Ident -> Value -> Eval Value
  recordSel n v =
    case v of
-      VRecord {}    -> lookupRecord n v
-      VSeq False vs -> VSeq False [ recordSel n v1 | v1 <- vs ]
-      VStream vs    -> VStream [recordSel n v1 | v1 <- vs ]
-      VFun f        -> VFun (\x -> recordSel n (f x))
-      _             -> evalPanic "Cryptol.Eval.evalSel"
-                          [ "Unexpected value in record selection"
-                          , show (ppValue defaultPPOpts v) ]
+      VRecord {}      -> lookupRecord n v
+      VSeq w False vs -> VSeq w False <$> mapSeqMap (recordSel n) vs
+      VStream vs      -> VStream <$> mapSeqMap (recordSel n) vs
+      VFun f          -> return $ VFun (\x -> recordSel n =<< f x)
+      _               -> do vdoc <- ppValue defaultPPOpts v
+                            evalPanic "Cryptol.Eval.evalSel"
+                             [ "Unexpected value in record selection"
+                             , show vdoc ]



@ -173,28 +233,28 @@ evalSel env e sel = case sel of
 -- different values at different positions in the list, while the
 -- @Pure@ constructor is for bindings originating outside the list
 -- comprehension, which have the same value for all list positions.
-data ZList a = Pure a | Zip [a]
+data ZList a = Pure a | Zip (Integer -> a)

-getZList :: ZList a -> [a]
-getZList (Pure x) = repeat x
+getZList :: ZList a -> Integer -> a
+getZList (Pure x) = \_ -> x
 getZList (Zip xs) = xs

 instance Functor ZList where
  fmap f (Pure x) = Pure (f x)
-  fmap f (Zip xs) = Zip (map f xs)
+  fmap f (Zip xs) = Zip (f . xs)

 instance Applicative ZList where
  pure x = Pure x
  Pure f <*> Pure x = Pure (f x)
-  Pure f <*> Zip xs = Zip (map f xs)
-  Zip fs <*> Pure x = Zip (map ($ x) fs)
-  Zip fs <*> Zip xs = Zip (zipWith ($) fs xs)
+  Pure f <*> Zip xs = Zip (\i -> f (xs i))
+  Zip fs <*> Pure x = Zip (\i -> fs i x)
+  Zip fs <*> Zip xs = Zip (\i -> fs i (xs i))

 -- | Evaluation environments for list comprehensions: Each variable
 -- name is bound to a list of values, one for each element in the list
 -- comprehension.
 data ListEnv = ListEnv
-  { leVars :: Map.Map Name (ZList Value)
+  { leVars  :: Map.Map Name (ZList (Eval Value))
  , leTypes :: Map.Map TVar TValue
  }

@ -212,7 +272,7 @@ instance Monoid ListEnv where
 toListEnv :: EvalEnv -> ListEnv
 toListEnv e =
  ListEnv
-  { leVars = fmap Pure (envVars e)
+  { leVars  = fmap Pure (envVars e)
  , leTypes = envTypes e
  }

@ -220,57 +280,84 @@ toListEnv e =
 -- bound to longer lists of values (e.g. if they come from a different
 -- parallel branch of a comprehension) then the last elements will be
 -- dropped as the lists are zipped together.
-zipListEnv :: ListEnv -> [EvalEnv]
-zipListEnv (ListEnv vm tm) =
-  [ EvalEnv { envVars = v, envTypes = tm }
-  | v <- getZList (sequenceA vm) ]
+zipListEnv :: ListEnv -> Integer -> EvalEnv
+zipListEnv (ListEnv vm tm) i =
+  let v = getZList (sequenceA vm) i
+   in EvalEnv { envVars = v, envTypes = tm }

-bindVarList :: Name -> [Value] -> ListEnv -> ListEnv
+bindVarList :: Name -> (Integer -> Eval Value) -> ListEnv -> ListEnv
 bindVarList n vs lenv = lenv { leVars = Map.insert n (Zip vs) (leVars lenv) }


 -- List Comprehensions ---------------------------------------------------------

 -- | Evaluate a comprehension.
-evalComp :: ReadEnv -> TValue -> Expr -> [[Match]] -> Value
-evalComp env seqty body ms
-  | Just (len,el) <- isTSeq seqty = toSeq len el [ evalExpr e body | e <- envs ]
-  | otherwise = evalPanic "Cryptol.Eval" [ "evalComp given a non sequence"
-                                         , show seqty
-                                         ]
+evalComp :: ReadEnv -> TValue -> TValue -> Expr -> [[Match]] -> Eval Value
+evalComp env len elty body ms =
+       do envMap <- mkEnvMap
+          seq <- memoMap $ SeqMap $ \i -> do
+              env' <- envMap i
+              evalExpr env' body
+          return $ mkSeq len elty $ seq

-  -- XXX we could potentially print this as a number if the type was available.
  where
-  -- generate a new environment for each iteration of each parallel branch
-  benvs :: [ListEnv]
-  benvs = map (branchEnvs (toListEnv env)) ms
-
-  -- join environments to produce environments at each step through the process.
-  envs :: [EvalEnv]
-  envs = zipListEnv (mconcat benvs)
+  mkEnvMap :: Eval (Integer -> Eval EvalEnv)
+  mkEnvMap = do
+    r <- io $ newIORef Map.empty
+    benvs <- mconcat <$> mapM (branchEnvs (toListEnv env)) ms
+    return $ \i -> do
+      m <- io $ readIORef r
+      case Map.lookup i m of
+        Just e -> return e
+        Nothing -> do
+          --io $ putStrLn $ unwords ["Forcing env map value", show i]
+          let e = zipListEnv benvs i
+          io $ writeIORef r (Map.insert i e m)
+          return e

 -- | Turn a list of matches into the final environments for each iteration of
 -- the branch.
-branchEnvs :: ListEnv -> [Match] -> ListEnv
-branchEnvs env matches = foldl evalMatch env matches
+branchEnvs :: ListEnv -> [Match] -> Eval ListEnv
+branchEnvs env matches = foldM evalMatch env matches

 -- | Turn a match into the list of environments it represents.
-evalMatch :: ListEnv -> Match -> ListEnv
+evalMatch :: ListEnv -> Match -> Eval ListEnv
 evalMatch lenv m = case m of

  -- many envs
-  From n _ty expr -> bindVarList n (concat vss) lenv'
+  From n l ty expr ->
+    case numTValue len of
+      Nat nLen -> do
+        vss <- memoMap $ SeqMap $ \i -> evalExpr (zipListEnv lenv i) expr
+        let stutter (Pure x) = Pure x
+            stutter (Zip xs) = Zip $ \i -> xs (i `div` nLen)
+        let lenv' = lenv { leVars = fmap stutter (leVars lenv) }
+        let vs i = do let (q,r) = i `divMod` nLen
+                      xs <- fromSeq =<< lookupSeqMap vss q
+                      lookupSeqMap xs r
+        return $ bindVarList n vs lenv'
+
+      Inf -> do
+        let stutter (Pure x) = Pure x
+            stutter (Zip xs) = Pure (xs 0)
+        let lenv' = lenv { leVars = fmap stutter (leVars lenv) }
+        xs <- delay Nothing (fromSeq =<< evalExpr (zipListEnv lenv 0) expr)
+        let vs i = do xseq <- xs
+                      lookupSeqMap xseq i
+        return $ bindVarList n vs lenv'
+
    where
-      vss = [ fromSeq (evalExpr env expr) | env <- zipListEnv lenv ]
-      stutter (Pure x) = Pure x
-      stutter (Zip xs) = Zip [ x | (x, vs) <- zip xs vss, _ <- vs ]
-      lenv' = lenv { leVars = fmap stutter (leVars lenv) }
+      tyenv = emptyEnv{ envTypes = leTypes lenv }
+      len  = evalType tyenv l
+      elty = evalType tyenv ty
+

  -- XXX we don't currently evaluate these as though they could be recursive, as
  -- they are typechecked that way; the read environment to evalExpr is the same
  -- as the environment to bind a new name in.
-  Let d -> bindVarList (dName d) (map f (zipListEnv lenv)) lenv
-    where f env =
-            case dDefinition d of
-              DPrim   -> evalPrim d
-              DExpr e -> evalExpr env e
+  Let d -> return $ bindVarList (dName d) (\i -> f (zipListEnv lenv i)) lenv
+    where
+      f env =
+          case dDefinition d of
+            DPrim   -> return $ evalPrim d
+            DExpr e -> evalExpr env e
--- a/src/Cryptol/Eval/Env.hs
+++ b/src/Cryptol/Eval/Env.hs
@ -12,6 +12,7 @@
 {-# LANGUAGE CPP #-}
 module Cryptol.Eval.Env where

+import Cryptol.Eval.Monad( Eval, delay )
 import Cryptol.Eval.Value
 import Cryptol.ModuleSystem.Name
 import Cryptol.TypeCheck.AST
@ -31,7 +32,7 @@ import Prelude.Compat
 type ReadEnv = EvalEnv

 data EvalEnv = EvalEnv
-  { envVars       :: Map.Map Name Value
+  { envVars       :: Map.Map Name (Eval Value)
  , envTypes      :: Map.Map TVar TValue
  } deriving (Generic)

@ -48,20 +49,28 @@ instance Monoid EvalEnv where
    , envTypes    = Map.union (envTypes    l) (envTypes    r)
    }

-instance PP (WithBase EvalEnv) where
-  ppPrec _ (WithBase opts env) = brackets (fsep (map bind (Map.toList (envVars env))))
-    where
-    bind (k,v) = pp k <+> text "->" <+> ppValue opts v
+ppEnv :: PPOpts -> EvalEnv -> Eval Doc
+ppEnv opts env = brackets . fsep <$> mapM bind (Map.toList (envVars env))
+  where
+   bind (k,v) = do vdoc <- ppValue opts =<< v
+                   return (pp k <+> text "->" <+> vdoc)
+
+--instance PP (WithBase EvalEnv) where
+--  ppPrec _ (WithBase opts env) = brackets (fsep (map bind (Map.toList (envVars env))))
+--    where
+--    bind (k,v) = pp k <+> text "->" <+> ppValue opts v

 emptyEnv :: EvalEnv
 emptyEnv  = mempty

 -- | Bind a variable in the evaluation environment.
-bindVar :: Name -> Value -> EvalEnv -> EvalEnv
-bindVar n val env = env { envVars = Map.insert n val (envVars env) }
+bindVar :: Name -> Eval Value -> EvalEnv -> Eval EvalEnv
+bindVar n val env = do
+  val' <- delay (Just (show (ppLocName n))) val
+  return $ env { envVars = Map.insert n val' (envVars env) }

 -- | Lookup a variable in the environment.
-lookupVar :: Name -> EvalEnv -> Maybe Value
+lookupVar :: Name -> EvalEnv -> Maybe (Eval Value)
 lookupVar n env = Map.lookup n (envVars env)

 -- | Bind a type variable of kind *.
--- a/src/Cryptol/Eval/Error.hs
+++ b/src/Cryptol/Eval/Error.hs
@ -1,69 +0,0 @@
-- |
-- Module      :  $Header$
-- Copyright   :  (c) 2013-2016 Galois, Inc.
-- License     :  BSD3
-- Maintainer  :  cryptol@galois.com
-- Stability   :  provisional
-- Portability :  portable
-
-{-# LANGUAGE Safe #-}
-{-# LANGUAGE DeriveDataTypeable #-}
-
-module Cryptol.Eval.Error where
-
-import Cryptol.Utils.Panic
-import Cryptol.Utils.PP
-import Cryptol.TypeCheck.AST(Type)
-
-import           Data.Typeable (Typeable)
-import qualified Control.Exception as X
-
-
-- Errors ----------------------------------------------------------------------
-
-- | Panic from an Eval context.
-evalPanic :: String -> [String] -> a
-evalPanic cxt = panic ("[Eval] " ++ cxt)
-
-
-data EvalError
-  = InvalidIndex Integer
-  | TypeCannotBeDemoted Type
-  | DivideByZero
-  | WordTooWide Integer
-  | UserError String
-    deriving (Typeable,Show)
-
-instance PP EvalError where
-  ppPrec _ e = case e of
-    InvalidIndex i -> text "invalid sequence index:" <+> integer i
-    TypeCannotBeDemoted t -> text "type cannot be demoted:" <+> pp t
-    DivideByZero -> text "division by 0"
-    WordTooWide w ->
-      text "word too wide for memory:" <+> integer w <+> text "bits"
-    UserError x -> text "Run-time error:" <+> text x
-
-instance X.Exception EvalError
-
-- | A sequencing operation has gotten an invalid index.
-invalidIndex :: Integer -> a
-invalidIndex i = X.throw (InvalidIndex i)
-
-- | For things like `(inf) or `(0-1)
-typeCannotBeDemoted :: Type -> a
-typeCannotBeDemoted t = X.throw (TypeCannotBeDemoted t)
-
-- | For division by 0.
-divideByZero :: a
-divideByZero = X.throw DivideByZero
-
-- | For when we know that a word is too wide and will exceed gmp's
-- limits (though words approaching this size will probably cause the
-- system to crash anyway due to lack of memory)
-wordTooWide :: Integer -> a
-wordTooWide w = X.throw (WordTooWide w)
-
-- | For `error`
-cryUserError :: String -> a
-cryUserError msg = X.throw (UserError msg)
-
--- a/src/Cryptol/Eval/Monad.hs
+++ b/src/Cryptol/Eval/Monad.hs
@ -0,0 +1,161 @@
+-- |
+-- Module      :  $Header$
+-- Copyright   :  (c) 2013-2016 Galois, Inc.
+-- License     :  BSD3
+-- Maintainer  :  cryptol@galois.com
+-- Stability   :  provisional
+-- Portability :  portable
+
+{-# LANGUAGE Safe #-}
+{-# LANGUAGE DeriveDataTypeable #-}
+{-# LANGUAGE DeriveFunctor #-}
+
+module Cryptol.Eval.Monad where
+
+  --   Eval(..)
+  -- , runEval
+  -- , io
+  -- , delay
+  -- , ready
+  -- , blackhole
+  -- ) where
+
+
+import           Control.DeepSeq
+import           Control.Monad
+import           Control.Monad.Fix
+import           Control.Monad.IO.Class
+import           Data.IORef
+import           Data.Typeable (Typeable)
+import qualified Control.Exception as X
+
+
+import Cryptol.Utils.Panic
+import Cryptol.Utils.PP
+import Cryptol.TypeCheck.AST(Type)
+
+
+ready :: a -> Eval a
+ready a = Ready a
+
+data Eval a
+   = Ready a
+   | Thunk !(IO a)
+ deriving (Functor)
+
+data ThunkState a
+  = Unforced
+  | BlackHole
+  | Forced a
+
+delay :: Maybe String -> Eval a -> Eval (Eval a)
+delay _ (Ready a) = Ready (Ready a)
+delay msg (Thunk x) = Thunk $ do
+  r <- newIORef Unforced
+  return $ unDelay msg r x
+
+blackhole :: String -> Eval (Eval a, Eval a -> Eval ())
+blackhole msg = do
+  r <- io $ newIORef (fail msg)
+  let get = join (io $ readIORef r)
+  let set = io . writeIORef r
+  return (get, set)
+
+unDelay :: Maybe String -> IORef (ThunkState a) -> IO a -> Eval a
+unDelay msg r x = do
+  rval <- io $ readIORef r
+  case rval of
+    Forced val -> return val
+    BlackHole  -> do
+      let msg' = maybe "" ("while evaluating "++) msg
+      cryLoopError msg'
+    Unforced -> io $ do
+      writeIORef r BlackHole
+      val <- x
+      writeIORef r (Forced val)
+      return val
+
+runEval :: Eval a -> IO a
+runEval (Ready a) = return a
+runEval (Thunk x) = x
+
+evalBind :: Eval a -> (a -> Eval b) -> Eval b
+evalBind (Ready a) f  = f a
+evalBind (Thunk x) f  = Thunk (x >>= runEval . f)
+
+instance Applicative Eval where
+  pure  = return
+  (<*>) = ap
+
+instance Monad Eval where
+  return = Ready
+  fail   = Thunk . fail
+  (>>=)  = evalBind
+
+instance MonadIO Eval where
+  liftIO = io
+
+instance NFData a => NFData (Eval a) where
+  rnf (Ready a) = rnf a
+  rnf (Thunk _) = ()
+
+instance MonadFix Eval where
+  mfix f = Thunk $ mfix (\x -> runEval (f x))
+
+io :: IO a -> Eval a
+io = Thunk
+
+
+-- Errors ----------------------------------------------------------------------
+
+-- | Panic from an Eval context.
+evalPanic :: String -> [String] -> a
+evalPanic cxt = panic ("[Eval] " ++ cxt)
+
+
+data EvalError
+  = InvalidIndex Integer
+  | TypeCannotBeDemoted Type
+  | DivideByZero
+  | WordTooWide Integer
+  | UserError String
+  | LoopError String
+    deriving (Typeable,Show)
+
+instance PP EvalError where
+  ppPrec _ e = case e of
+    InvalidIndex i -> text "invalid sequence index:" <+> integer i
+    TypeCannotBeDemoted t -> text "type cannot be demoted:" <+> pp t
+    DivideByZero -> text "division by 0"
+    WordTooWide w ->
+      text "word too wide for memory:" <+> integer w <+> text "bits"
+    UserError x -> text "Run-time error:" <+> text x
+    LoopError x -> text "<<loop>>" <+> text x
+
+instance X.Exception EvalError
+
+-- | For things like `(inf) or `(0-1)
+typeCannotBeDemoted :: Type -> a
+typeCannotBeDemoted t = X.throw (TypeCannotBeDemoted t)
+
+-- | For division by 0.
+divideByZero :: a
+divideByZero = X.throw DivideByZero
+
+-- | For when we know that a word is too wide and will exceed gmp's
+-- limits (though words approaching this size will probably cause the
+-- system to crash anyway due to lack of memory)
+wordTooWide :: Integer -> a
+wordTooWide w = X.throw (WordTooWide w)
+
+-- | For `error`
+cryUserError :: String -> Eval a
+cryUserError msg = Thunk (X.throwIO (UserError msg))
+
+-- | For cases where we can detect tight loops
+cryLoopError :: String -> Eval a
+cryLoopError msg = Thunk (X.throwIO (LoopError msg))
+
+-- | A sequencing operation has gotten an invalid index.
+invalidIndex :: Integer -> Eval a
+invalidIndex i = Thunk (X.throwIO (InvalidIndex i))
--- a/src/Cryptol/Eval/Type.hs
+++ b/src/Cryptol/Eval/Type.hs
@ -11,7 +11,7 @@
 module Cryptol.Eval.Type (evalType, evalTF) where

 import Cryptol.Eval.Env
-import Cryptol.Eval.Error
+import Cryptol.Eval.Monad
 import Cryptol.Eval.Value(TValue(..),numTValue)
 import Cryptol.TypeCheck.AST
 import Cryptol.TypeCheck.Solver.InfNat
--- a/src/Cryptol/Eval/Value.hs
+++ b/src/Cryptol/Eval/Value.hs
@ -8,23 +8,35 @@

 {-# LANGUAGE PatternGuards #-}
 {-# LANGUAGE DeriveFunctor #-}
+{-# LANGUAGE DeriveGeneric #-}
 {-# LANGUAGE FlexibleInstances #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
 {-# LANGUAGE Safe #-}
-{-# LANGUAGE DeriveGeneric #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TupleSections #-}
+{-# LANGUAGE ViewPatterns #-}
+
 module Cryptol.Eval.Value where

+import Data.IORef
+--import           Data.Map (Map)
+import qualified Data.Map as Map
+
+import MonadLib
+
 import qualified Cryptol.Eval.Arch as Arch
-import Cryptol.Eval.Error
+import Cryptol.Eval.Monad
+
 import Cryptol.TypeCheck.AST
 import Cryptol.TypeCheck.Solver.InfNat(Nat'(..))
 import Cryptol.Utils.Ident (Ident,mkIdent)
 import Cryptol.Utils.PP
 import Cryptol.Utils.Panic(panic)

-import Control.Monad (guard, zipWithM)
-import Data.List(genericTake)
+--import Control.Monad (guard, zipWithM)
+import Data.List(genericLength, genericIndex)
 import Data.Bits (setBit,testBit,(.&.),shiftL)
+import qualified Data.Sequence as Seq
 import qualified Data.Text as T
 import Numeric (showIntAtBase)

@ -84,26 +96,105 @@ finTValue tval =
 -- Invariant: The value must be within the range 0 .. 2^width-1
 data BV = BV !Integer !Integer deriving (Generic)

+instance Show BV where
+  show = show . bvVal
+
+bvVal :: BV -> Integer
+bvVal (BV _w x) = x
+
 instance NFData BV where rnf = genericRnf

 -- | Smart constructor for 'BV's that checks for the width limit
 mkBv :: Integer -> Integer -> BV
 mkBv w i = BV w (mask w i)

+newtype SeqMap b w = SeqMap { lookupSeqMap :: Integer -> Eval (GenValue b w) }
+type SeqValMap = SeqMap Bool BV
+
+instance NFData (SeqMap b w) where
+  rnf x = seq x ()
+
+finiteSeqMap :: [Eval (GenValue b w)] -> Eval (SeqMap b w)
+finiteSeqMap xs = do
+   v <- Seq.fromList <$> mapM (delay Nothing) xs
+   let len = Seq.length v
+       f (fromInteger -> i) | 0 <= i && i < len = Seq.index v i
+                            | otherwise = evalPanic "finiteSeqMap" ["Index out of bounds:", show i]
+   return $ SeqMap f
+
+infiniteSeqMap :: [Eval (GenValue b w)] -> Eval (SeqMap b w)
+infiniteSeqMap xs =
+   memoMap (SeqMap $ \i -> genericIndex xs i)
+
+enumerateSeqMap :: (Integral n) => n -> SeqMap b w -> [Eval (GenValue b w)]
+enumerateSeqMap n m = [ lookupSeqMap m i | i <- [0 .. (toInteger n)-1] ]
+
+streamSeqMap :: SeqMap b w -> [Eval (GenValue b w)]
+streamSeqMap m = [ lookupSeqMap m i | i <- [0..] ]
+
+reverseSeqMap :: Integer -> SeqMap b w -> SeqMap b w
+reverseSeqMap n vals = SeqMap $ \i -> lookupSeqMap vals (n - 1 - i)
+
+splitSeqMap :: Integer -> SeqMap b w -> (SeqMap b w, SeqMap b w)
+splitSeqMap n xs = (hd,tl)
+  where
+  hd = xs
+  tl = SeqMap $ \i -> lookupSeqMap xs (i+n)
+
+memoMap :: SeqMap b w -> Eval (SeqMap b w)
+memoMap x = do
+  r <- io $ newIORef Map.empty
+  return $ SeqMap $ \i -> do
+    m <- io $ readIORef r
+    case Map.lookup i m of
+      Just (Just z) -> return z
+      Just Nothing -> 
+        cryLoopError $ unwords ["memoMap location:", show i]
+      Nothing -> do
+        --io $ putStrLn $ unwords ["Forcing memo map location", show i]
+        io $ writeIORef r (Map.insert i Nothing m)
+        v <- lookupSeqMap x i
+        io $ writeIORef r (Map.insert i (Just v) m)
+        return v
+
+
+zipSeqMap :: (GenValue b w -> GenValue b w -> Eval (GenValue b w))
+          -> SeqMap b w
+          -> SeqMap b w
+          -> Eval (SeqMap b w)
+zipSeqMap f x y =
+  memoMap (SeqMap $ \i -> join (f <$> lookupSeqMap x i <*> lookupSeqMap y i))
+  
+mapSeqMap :: (GenValue b w -> Eval (GenValue b w))
+          -> SeqMap b w -> Eval (SeqMap b w)
+mapSeqMap f x =
+  memoMap (SeqMap $ \i -> f =<< lookupSeqMap x i)
+
 -- | Generic value type, parameterized by bit and word types.
 data GenValue b w
-  = VRecord [(Ident, GenValue b w)]     -- @ { .. } @
-  | VTuple [GenValue b w]               -- @ ( .. ) @
-  | VBit b                              -- @ Bit    @
-  | VSeq Bool [GenValue b w]            -- @ [n]a   @
-                                        -- The boolean parameter indicates whether or not
-                                        -- this is a sequence of bits.
-  | VWord w                             -- @ [n]Bit @
-  | VStream [GenValue b w]              -- @ [inf]a @
-  | VFun (GenValue b w -> GenValue b w) -- functions
-  | VPoly (TValue -> GenValue b w)      -- polymorphic values (kind *)
+  = VRecord [(Ident, Eval (GenValue b w))] -- @ { .. } @
+  | VTuple [Eval (GenValue b w)]           -- @ ( .. ) @
+  | VBit b                                 -- @ Bit    @
+  | VSeq !Integer !Bool (SeqMap b w)       -- @ [n]a   @
+                                           -- The boolean parameter indicates whether or not
+                                           -- this is a sequence of bits.
+  | VWord w                                -- @ [n]Bit @
+  | VStream (SeqMap b w)                   -- @ [inf]a @
+  | VFun (Eval (GenValue b w) -> Eval (GenValue b w)) -- functions
+  | VPoly (TValue -> Eval (GenValue b w))  -- polymorphic values (kind *)
  deriving (Generic)

+instance (Show b, Show w) => Show (GenValue b w) where
+  show v = case v of
+    VRecord fs -> "record:" ++ show (map fst fs)
+    VTuple xs  -> "tuple:" ++ show (length xs)
+    VBit b     -> show b
+    VSeq n w _ -> "seq:" ++ show n ++ " " ++ show w
+    VWord x    -> "word:"  ++ show x
+    VStream _  -> "stream"
+    VFun _     -> "fun"
+    VPoly _    -> "poly"
+
 instance (NFData b, NFData w) => NFData (GenValue b w) where rnf = genericRnf

 type Value = GenValue Bool BV
@ -129,35 +220,46 @@ data PPOpts = PPOpts
 defaultPPOpts :: PPOpts
 defaultPPOpts = PPOpts { useAscii = False, useBase = 10, useInfLength = 5 }

-ppValue :: PPOpts -> Value -> Doc
+atFst :: Functor f => (a -> f b) -> (a, c) -> f (b, c)
+atFst f (x,y) = fmap (,y) $ f x
+
+atSnd :: Functor f => (a -> f b) -> (c, a) -> f (c, b)
+atSnd f (x,y) = fmap (x,) $ f y
+
+ppValue :: PPOpts -> Value -> Eval Doc
 ppValue opts = loop
  where
+  loop :: Value -> Eval Doc
  loop val = case val of
-    VRecord fs         -> braces (sep (punctuate comma (map ppField fs)))
+    VRecord fs         -> do fs' <- traverse (atSnd (>>=loop)) $ fs
+                             return $ braces (sep (punctuate comma (map ppField fs')))
      where
-      ppField (f,r) = pp f <+> char '=' <+> loop r
-    VTuple vals        -> parens (sep (punctuate comma (map loop vals)))
-    VBit b | b         -> text "True"
-           | otherwise -> text "False"
-    VSeq isWord vals
-       | isWord        -> ppWord opts (fromVWord val)
-       | otherwise     -> ppWordSeq vals
-    VWord (BV w i)     -> ppWord opts (BV w i)
-    VStream vals       -> brackets $ fsep
+      ppField (f,r) = pp f <+> char '=' <+> r
+    VTuple vals        -> do vals' <- traverse (>>=loop) vals
+                             return $ parens (sep (punctuate comma vals'))
+    VBit b | b         -> return $ text "True"
+           | otherwise -> return $ text "False"
+    VSeq sz isWord vals
+       | isWord        -> ppWord opts <$> fromVWord "ppValue" val
+       | otherwise     -> ppWordSeq sz vals
+    VWord wd           -> return $ ppWord opts wd
+    VStream vals       -> do vals' <- traverse (>>=loop) $ enumerateSeqMap (useInfLength opts) vals
+                             return $ brackets $ fsep
                                   $ punctuate comma
-                                   ( take (useInfLength opts) (map loop vals)
-                                     ++ [text "..."]
+                                   ( vals' ++ [text "..."]
                                   )
-    VFun _             -> text "<function>"
-    VPoly _            -> text "<polymorphic value>"
+    VFun _             -> return $ text "<function>"
+    VPoly _            -> return $ text "<polymorphic value>"

-  ppWordSeq ws =
+  ppWordSeq :: Integer -> SeqValMap -> Eval Doc
+  ppWordSeq sz vals = do
+    ws <- sequence (enumerateSeqMap sz vals)
    case ws of
      w : _
        | Just l <- vWordLen w, asciiMode opts l ->
-                text $ show $ map (integerToChar . fromWord) ws
-      _ -> brackets (fsep (punctuate comma (map loop ws)))
-
+              text . show . map (integerToChar . bvVal) <$> traverse (fromVWord "ppWordSeq") ws
+      _ -> do ws' <- traverse loop ws
+              return $ brackets (fsep (punctuate comma ws'))

 asciiMode :: PPOpts -> Integer -> Bool
 asciiMode opts width = useAscii opts && (width == 7 || width == 8)
@ -165,11 +267,11 @@ asciiMode opts width = useAscii opts && (width == 7 || width == 8)
 integerToChar :: Integer -> Char
 integerToChar = toEnum . fromInteger

-data WithBase a = WithBase PPOpts a
-    deriving (Functor)
+--data WithBase a = WithBase PPOpts a
+--    deriving (Functor)

-instance PP (WithBase Value) where
-  ppPrec _ (WithBase opts v) = ppValue opts v
+--instance PP (WithBase Value) where
+--  ppPrec _ (WithBase opts v) = ppValue opts v

 ppWord :: PPOpts -> BV -> Doc
 ppWord opts (BV width i)
@ -238,33 +340,47 @@ instance BitWord Bool BV where

 -- | Create a packed word of n bits.
 word :: Integer -> Integer -> Value
-word n i = VWord (mkBv n i)
+word n i = VWord $ mkBv n i

-lam :: (GenValue b w -> GenValue b w) -> GenValue b w
+lam :: (Eval (GenValue b w) -> Eval (GenValue b w)) -> GenValue b w
 lam  = VFun

+-- | Functions that assume word inputs
+wlam :: (Integer -> Eval Value) -> Value
+wlam f = VFun (\x -> x >>= fromWord "wlam" >>= f)
+
 -- | A type lambda that expects a @Type@.
 tlam :: (TValue -> GenValue b w) -> GenValue b w
-tlam  = VPoly
+tlam f = VPoly (return . f)

 -- | Generate a stream.
-toStream :: [GenValue b w] -> GenValue b w
-toStream  = VStream
+toStream :: [GenValue b w] -> Eval (GenValue b w)
+toStream vs =
+   VStream <$> infiniteSeqMap (map ready vs)

-toFinSeq :: TValue -> [GenValue b w] -> GenValue b w
-toFinSeq elty = VSeq (isTBit elty)
+toFinSeq :: Integer -> TValue -> [GenValue b w] -> Eval (GenValue b w)
+toFinSeq len elty vs =
+   VSeq len (isTBit elty) <$> finiteSeqMap (map ready vs)

 -- | This is strict!
 boolToWord :: [Bool] -> Value
-boolToWord = VWord . packWord
+boolToWord bs = VWord (packWord bs)

 -- | Construct either a finite sequence, or a stream.  In the finite case,
 -- record whether or not the elements were bits, to aid pretty-printing.
-toSeq :: TValue -> TValue -> [GenValue b w] -> GenValue b w
+toSeq :: TValue -> TValue -> [GenValue b w] -> Eval (GenValue b w)
 toSeq len elty vals = case numTValue len of
-  Nat n -> toFinSeq elty (genericTake n vals)
+  Nat n -> toFinSeq n elty vals
  Inf   -> toStream vals

+
+-- | 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 :: TValue -> TValue -> SeqMap b w -> GenValue b w
+mkSeq len elty vals = case numTValue len of
+  Nat n -> VSeq n (isTBit elty) vals
+  Inf   -> VStream vals
+
 -- | Construct one of:
 --   * a word, when the sequence is finite and the elements are bits
 --   * a sequence, when the sequence is finite but the elements aren't bits
@ -272,16 +388,15 @@ toSeq len elty vals = case numTValue len of
 --
 -- NOTE: do not use this constructor in the case where the thing may be a
 -- finite, but recursive, sequence.
-toPackedSeq :: TValue -> TValue -> [Value] -> Value
+toPackedSeq :: TValue -> TValue -> SeqValMap -> Eval Value
 toPackedSeq len elty vals = case numTValue len of

  -- finite sequence, pack a word if the elements are bits.
-  Nat _ | isTBit elty -> boolToWord (map fromVBit vals)
-        | otherwise  -> VSeq False vals
+  Nat n | isTBit elty -> boolToWord <$> (traverse (fromVBit <$>) [ lookupSeqMap vals i | i <- [0 .. n-1] ])
+        | otherwise   -> return $ VSeq n False vals

  -- infinite sequence, construct a stream
-  Inf -> VStream vals
-
+  Inf -> return $ VStream vals

 -- Value Destructors -----------------------------------------------------------

@ -292,61 +407,69 @@ fromVBit val = case val of
  _      -> evalPanic "fromVBit" ["not a Bit"]

 -- | Extract a sequence.
-fromSeq :: BitWord b w => GenValue b w -> [GenValue b w]
+fromSeq :: forall b w. BitWord b w => GenValue b w -> Eval (SeqMap b w)
 fromSeq val = case val of
-  VSeq _ vs  -> vs
-  VWord bv   -> map VBit (unpackWord bv)
-  VStream vs -> vs
+  VSeq _ _ vs  -> return vs
+  VWord bv -> do let bs = unpackWord bv
+                 return $ SeqMap $ (\i -> return . VBit . flip genericIndex i $ bs)
+  VStream vs -> return vs
  _          -> evalPanic "fromSeq" ["not a sequence"]

-fromStr :: Value -> String
-fromStr = map (toEnum . fromInteger . fromWord) . fromSeq
+fromStr :: Value -> Eval String
+fromStr (VSeq n _ vals) =
+  traverse (\x -> toEnum . fromInteger <$> (fromWord "fromStr" =<< x)) (enumerateSeqMap n vals)
+fromStr _ = evalPanic "fromStr" ["Not a finite sequence"]
+  

 -- | Extract a packed word.
-fromVWord :: BitWord b w => GenValue b w -> w
-fromVWord val = case val of
-  VWord bv                -> bv -- this should always mask
-  VSeq isWord bs | isWord -> packWord (map fromVBit bs)
-  _                       -> evalPanic "fromVWord" ["not a word"]
+fromVWord :: BitWord b w => String -> GenValue b w -> Eval w
+fromVWord msg val = case val of
+  VWord bv                  -> return bv -- this should always mask
+  VSeq n isWord bs | isWord -> packWord <$> traverse (fromVBit<$>) (enumerateSeqMap n bs)
+  _                         -> evalPanic "fromVWord" ["not a word", msg]

 vWordLen :: Value -> Maybe Integer
 vWordLen val = case val of
-  VWord (BV w _)          -> Just w
-  VSeq isWord bs | isWord -> Just (toInteger (length bs))
-  _                       -> Nothing
-
+  VWord (BV n _)           -> Just n
+  VSeq n isWord _ | isWord -> Just n
+  _                        -> Nothing

 -- | Turn a value into an integer represented by w bits.
-fromWord :: Value -> Integer
-fromWord val = a
-  where BV _ a = fromVWord val
+
+fromWord :: String -> Value -> Eval Integer
+fromWord msg val =
+   case val of
+     VWord w                   -> return $ bvVal w
+     VSeq n isWord bs | isWord -> bvVal . packWord <$> traverse (fromVBit<$>) (enumerateSeqMap n bs)
+     _ -> do --vdoc <- ppValue defaultPPOpts val
+             evalPanic "fromWord" ["not a word", msg]

 -- | Extract a function from a value.
-fromVFun :: GenValue b w -> (GenValue b w -> GenValue b w)
+fromVFun :: GenValue b w -> (Eval (GenValue b w) -> Eval (GenValue b w))
 fromVFun val = case val of
  VFun f -> f
  _      -> evalPanic "fromVFun" ["not a function"]

 -- | Extract a polymorphic function from a value.
-fromVPoly :: GenValue b w -> (TValue -> GenValue b w)
+fromVPoly :: GenValue b w -> (TValue -> Eval (GenValue b w))
 fromVPoly val = case val of
  VPoly f -> f
  _       -> evalPanic "fromVPoly" ["not a polymorphic value"]

 -- | Extract a tuple from a value.
-fromVTuple :: GenValue b w -> [GenValue b w]
+fromVTuple :: GenValue b w -> [Eval (GenValue b w)]
 fromVTuple val = case val of
  VTuple vs -> vs
  _         -> evalPanic "fromVTuple" ["not a tuple"]

 -- | Extract a record from a value.
-fromVRecord :: GenValue b w -> [(Ident, GenValue b w)]
+fromVRecord :: GenValue b w -> [(Ident, Eval (GenValue b w))]
 fromVRecord val = case val of
  VRecord fs -> fs
  _          -> evalPanic "fromVRecord" ["not a record"]

 -- | Lookup a field in a record.
-lookupRecord :: Ident -> GenValue b w -> GenValue b w
+lookupRecord :: Ident -> GenValue b w -> Eval (GenValue b w)
 lookupRecord f rec = case lookup f (fromVRecord rec) of
  Just val -> val
  Nothing  -> evalPanic "lookupRecord" ["malformed record"]
@ -357,29 +480,30 @@ lookupRecord f rec = case lookup f (fromVRecord rec) of
 -- this value, if we can determine it.
 --
 -- XXX: View patterns would probably clean up this definition a lot.
-toExpr :: PrimMap -> Type -> Value -> Maybe Expr
-toExpr prims = go
+toExpr :: PrimMap -> Type -> Value -> Eval (Maybe Expr)
+toExpr prims t0 v0 = findOne (go t0 v0)
  where

  prim n = ePrim prims (mkIdent (T.pack n))

+  go :: Type -> Value -> ChoiceT Eval Expr
  go ty val = case (ty, val) of
    (TRec tfs, VRecord vfs) -> do
      let fns = map fst vfs
      guard (map fst tfs == fns)
-      fes <- zipWithM go (map snd tfs) (map snd vfs)
+      fes <- zipWithM go (map snd tfs) =<< lift (traverse snd vfs)
      return $ ERec (zip fns fes)
    (TCon (TC (TCTuple tl)) ts, VTuple tvs) -> do
      guard (tl == (length tvs))
-      ETuple `fmap` zipWithM go ts tvs
+      ETuple `fmap` (zipWithM go ts =<< lift (sequence tvs))
    (TCon (TC TCBit) [], VBit True ) -> return (prim "True")
    (TCon (TC TCBit) [], VBit False) -> return (prim "False")
-    (TCon (TC TCSeq) [a,b], VSeq _ []) -> do
+    (TCon (TC TCSeq) [a,b], VSeq 0 _ _) -> do
      guard (a == tZero)
      return $ EList [] b
-    (TCon (TC TCSeq) [a,b], VSeq _ svs) -> do
-      guard (a == tNum (length svs))
-      ses <- mapM (go b) svs
+    (TCon (TC TCSeq) [a,b], VSeq n _ svs) -> do
+      guard (a == tNum n)
+      ses <- mapM (go b) =<< lift (sequence (enumerateSeqMap n svs))
      return $ EList ses b
    (TCon (TC TCSeq) [a,(TCon (TC TCBit) [])], VWord (BV w v)) -> do
      guard (a == tNum w)
@ -387,8 +511,9 @@ toExpr prims = go
    (_, VStream _) -> fail "cannot construct infinite expressions"
    (_, VFun    _) -> fail "cannot convert function values to expressions"
    (_, VPoly   _) -> fail "cannot convert polymorphic values to expressions"
-    _ -> panic "Cryptol.Eval.Value.toExpr"
-           ["type mismatch:"
-           , pretty ty
-           , render (ppValue defaultPPOpts val)
-           ]
+    _ -> do doc <- lift (ppValue defaultPPOpts val)
+            panic "Cryptol.Eval.Value.toExpr"
+             ["type mismatch:"
+             , pretty ty
+             , render doc
+             ]
--- a/src/Cryptol/ModuleSystem/Base.hs
+++ b/src/Cryptol/ModuleSystem/Base.hs
@ -18,6 +18,7 @@ import Cryptol.ModuleSystem.Name (Name,liftSupply,PrimMap)
 import Cryptol.ModuleSystem.Env (lookupModule, LoadedModule(..)
                                , meCoreLint, CoreLint(..))
 import qualified Cryptol.Eval                 as E
+import qualified Cryptol.Eval.Monad           as E
 import qualified Cryptol.Eval.Value           as E
 import qualified Cryptol.ModuleSystem.NamingEnv as R
 import qualified Cryptol.ModuleSystem.Renamer as R
@ -459,14 +460,15 @@ evalExpr :: T.Expr -> ModuleM E.Value
 evalExpr e = do
  env <- getEvalEnv
  denv <- getDynEnv
-  return (E.evalExpr (env <> deEnv denv) e)
+  io $ E.runEval $ (E.evalExpr (env <> deEnv denv) e)

 evalDecls :: [T.DeclGroup] -> ModuleM ()
 evalDecls dgs = do
  env <- getEvalEnv
  denv <- getDynEnv
  let env' = env <> deEnv denv
-      denv' = denv { deDecls = deDecls denv ++ dgs
-                   , deEnv = E.evalDecls dgs env'
+  deEnv' <- io $ E.runEval $ E.evalDecls dgs env'
+  let denv' = denv { deDecls = deDecls denv ++ dgs
+                   , deEnv = deEnv'
                   }
  setDynEnv denv'
--- a/src/Cryptol/ModuleSystem/Monad.hs
+++ b/src/Cryptol/ModuleSystem/Monad.hs
@ -11,6 +11,7 @@
 module Cryptol.ModuleSystem.Monad where

 import           Cryptol.Eval.Env (EvalEnv)
+import qualified Cryptol.Eval.Monad           as E
 import           Cryptol.ModuleSystem.Env
 import           Cryptol.ModuleSystem.Interface
 import           Cryptol.ModuleSystem.Name (FreshM(..),Supply)
@ -389,10 +390,12 @@ loadedModule path m = ModuleT $ do
  env <- get
  set $! env { meLoadedModules = addLoadedModule path m (meLoadedModules env) }

-modifyEvalEnv :: (EvalEnv -> EvalEnv) -> ModuleM ()
+modifyEvalEnv :: (EvalEnv -> E.Eval EvalEnv) -> ModuleM ()
 modifyEvalEnv f = ModuleT $ do
  env <- get
-  set $! env { meEvalEnv = f (meEvalEnv env) }
+  let evalEnv = meEvalEnv env
+  evalEnv' <- inBase $ E.runEval (f evalEnv)
+  set $! env { meEvalEnv = evalEnv' }

 getEvalEnv :: ModuleM EvalEnv
 getEvalEnv  = ModuleT (meEvalEnv `fmap` get)
--- a/src/Cryptol/Prims/Eval.hs
+++ b/src/Cryptol/Prims/Eval.hs
@ -11,23 +11,28 @@
 {-# LANGUAGE RecordWildCards #-}
 {-# LANGUAGE Rank2Types #-}
 {-# LANGUAGE PatternGuards #-}
+{-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE ViewPatterns #-}
 {-# LANGUAGE BangPatterns #-}
 module Cryptol.Prims.Eval where

+import Control.Monad (join)
+
 import Cryptol.TypeCheck.AST
 import Cryptol.TypeCheck.Solver.InfNat (Nat'(..),fromNat,genLog, nMul)
 import qualified Cryptol.Eval.Arch as Arch
-import Cryptol.Eval.Error
+import Cryptol.Eval.Monad
 import Cryptol.Eval.Type(evalTF)
 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 Data.List (sortBy, transpose, genericTake, genericDrop,
-                  genericReplicate, genericSplitAt, genericIndex)
+                  genericReplicate, genericSplitAt, genericIndex,
+                  foldl')
 import Data.Ord (comparing)
 import Data.Bits (Bits(..))

@ -55,12 +60,12 @@ primTable = Map.fromList $ map (\(n, v) -> (mkIdent (T.pack n), v))
  , ("^^"         , binary (arithBinary modExp))
  , ("lg2"        , unary  (arithUnary lg2))
  , ("negate"     , unary  (arithUnary negate))
-  , ("<"          , binary (cmpOrder (\o -> o == LT           )))
-  , (">"          , binary (cmpOrder (\o -> o == GT           )))
-  , ("<="         , binary (cmpOrder (\o -> o == LT || o == EQ)))
-  , (">="         , binary (cmpOrder (\o -> o == GT || o == EQ)))
-  , ("=="         , binary (cmpOrder (\o ->            o == EQ)))
-  , ("!="         , binary (cmpOrder (\o ->            o /= EQ)))
+  , ("<"          , binary (cmpOrder "<"  (\o -> o == LT           )))
+  , (">"          , binary (cmpOrder ">"  (\o -> o == GT           )))
+  , ("<="         , binary (cmpOrder "<=" (\o -> o == LT || o == EQ)))
+  , (">="         , binary (cmpOrder ">=" (\o -> o == GT || o == EQ)))
+  , ("=="         , binary (cmpOrder "==" (\o ->            o == EQ)))
+  , ("!="         , binary (cmpOrder "!=" (\o ->            o /= EQ)))
  , ("&&"         , binary (logicBinary (.&.)))
  , ("||"         , binary (logicBinary (.|.)))
  , ("^"          , binary (logicBinary xor))
@ -77,58 +82,55 @@ primTable = Map.fromList $ map (\(n, v) -> (mkIdent (T.pack n), v))
  , ("#"          , tlam $ \ front ->
                    tlam $ \ back  ->
                    tlam $ \ elty  ->
-                    lam  $ \ l     ->
+                    lam  $ \ l     -> return $
                    lam  $ \ r     -> ccatV front back elty l r)

  , ("@"          , indexPrimOne  indexFront)
-  , ("@@"         , indexPrimMany indexFrontRange)
+  , ("@@"         , indexPrimMany indexFront)
  , ("!"          , indexPrimOne  indexBack)
-  , ("!!"         , indexPrimMany indexBackRange)
+  , ("!!"         , indexPrimMany indexBack)

  , ("zero"       , tlam zeroV)

  , ("join"       , tlam $ \ parts ->
                    tlam $ \ each  ->
-                    tlam $ \ a     -> lam (joinV parts each a))
+                    tlam $ \ a     ->
+                    lam  $ \ x     ->
+                      joinV parts each a =<< x)

  , ("split"      , ecSplitV)

  , ("splitAt"    , tlam $ \ front ->
                    tlam $ \ back  ->
-                    tlam $ \ a     -> lam (splitAtV front back a))
+                    tlam $ \ a     ->
+                    lam  $ \ x     ->
+                       splitAtV front back a =<< x)

  , ("fromThen"   , fromThenV)
  , ("fromTo"     , fromToV)
  , ("fromThenTo" , fromThenToV)

  , ("infFrom"    , tlam $ \(finTValue -> bits)  ->
-                     lam $ \(fromWord  -> first) ->
-                    toStream (map (word bits) [ first .. ]))
+                    wlam $ \first ->
+                    toStream $ map (word bits) [ first .. ])

  , ("infFromThen", tlam $ \(finTValue -> bits)  ->
-                     lam $ \(fromWord  -> first) ->
-                     lam $ \(fromWord  -> next)  ->
+                    wlam $ \first -> return $
+                    wlam $ \next  ->
                    toStream [ word bits n | n <- [ first, next .. ] ])

-  , ("error"      , tlam $ \_              ->
-                    tlam $ \_              ->
-                     lam $ \(fromStr -> s) -> cryUserError s)
+  , ("error"      , tlam $ \_ ->
+                    tlam $ \_ ->
+                     lam $ \s -> cryUserError =<< (fromStr =<< s))

  , ("reverse"    , tlam $ \a ->
                    tlam $ \b ->
-                     lam $ \(fromSeq -> xs) -> toSeq a b (reverse xs))
+                     lam $ \xs -> reverseV =<< xs)

  , ("transpose"  , tlam $ \a ->
                    tlam $ \b ->
                    tlam $ \c ->
-                     lam $ \((map fromSeq . fromSeq) -> xs) ->
-                        case numTValue a of
-                           Nat 0 ->
-                             let val = toSeq a c []
-                             in case numTValue b of
-                                  Nat n -> toSeq b (tvSeq a c) $ genericReplicate n val
-                                  Inf   -> VStream $ repeat val
-                           _ -> toSeq b (tvSeq a c) $ map (toSeq a c) $ transpose xs)
+                     lam $ \xs -> transposeV a b c =<< xs)

  , ("pmult"       ,
    let mul !res !_ !_ 0 = res
@ -136,22 +138,36 @@ primTable = Map.fromList $ map (\(n, v) -> (mkIdent (T.pack n), v))
                               (bs `shiftL` 1) (as `shiftR` 1) (n-1)
     in tlam $ \(finTValue -> a) ->
        tlam $ \(finTValue -> b) ->
-         lam $ \(fromWord  -> x) ->
-         lam $ \(fromWord  -> y) -> word (max 1 (a + b) - 1) (mul 0 x y b))
+        wlam $ \x -> return $
+        wlam $ \y -> return $ word (max 1 (a + b) - 1) (mul 0 x y b))

  , ("pdiv"        , tlam $ \(fromInteger . finTValue -> a) ->
                     tlam $ \(fromInteger . finTValue -> b) ->
-                      lam $ \(fromWord  -> x) ->
-                      lam $ \(fromWord  -> y) -> word (toInteger a)
-                                                      (fst (divModPoly x a y b)))
+                     wlam $ \x -> return $
+                     wlam $ \y -> return $ word (toInteger a)
+                                                (fst (divModPoly x a y b)))

  , ("pmod"        , tlam $ \(fromInteger . finTValue -> a) ->
                     tlam $ \(fromInteger . finTValue -> b) ->
-                      lam $ \(fromWord  -> x) ->
-                      lam $ \(fromWord  -> y) -> word (toInteger b)
-                                                      (snd (divModPoly x a y (b+1))))
+                     wlam $ \x -> return $
+                     wlam $ \y -> return $ word (toInteger b)
+                                                (snd (divModPoly x a y (b+1))))
  , ("random"      , tlam $ \a ->
-                      lam $ \(fromWord -> x) -> randomV a x)
+                     wlam $ \x -> return $ randomV a x)
+  , ("trace"       , tlam $ \_n ->
+                     tlam $ \_a ->
+                     tlam $ \_b ->
+                      lam $ \s -> return $
+                      lam $ \x -> return $
+                      lam $ \y -> do
+                         msg <- fromStr =<< s
+                         -- FIXME? get PPOPts from elsewhere?
+                         doc <- ppValue defaultPPOpts =<< x
+                         io $ putStrLn $ show $ if null msg then
+                                                  doc
+                                                else
+                                                  text msg <+> doc
+                         y)
  ]


@ -230,20 +246,22 @@ doubleAndAdd base0 expMask modulus = go 1 base0 expMask

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

-type GenBinary b w = TValue -> GenValue b w -> GenValue b w -> GenValue b w
+type GenBinary b w = TValue -> GenValue b w -> GenValue b w -> Eval (GenValue b w)
 type Binary = GenBinary Bool BV

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

-type GenUnary b w = TValue -> GenValue b w -> GenValue b w
+type GenUnary b w = TValue -> GenValue b w -> Eval (GenValue b w)
 type Unary = GenUnary Bool BV

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


 -- Arith -----------------------------------------------------------------------
@ -256,60 +274,73 @@ type BinArith = Integer -> Integer -> Integer -> Integer

 arithBinary :: BinArith -> Binary
 arithBinary op = loop
+--arithBinary op ty0 l0 r0 = io (putStrLn "Entering arithBinary") >> loop ty0 l0 r0
  where
+  loop' :: TValue -> Eval Value -> Eval Value -> Eval Value
+  loop' ty l r = join (loop ty <$> l <*> r)
+
+  loop :: TValue -> Value -> Value -> Eval Value
  loop ty l r

    | Just (len,a) <- isTSeq ty = case numTValue len of

      -- words and finite sequences
-      Nat w | isTBit a  -> VWord (mkBv w (op w (fromWord l) (fromWord r)))
-            | otherwise -> VSeq False (zipWith (loop a) (fromSeq l) (fromSeq r))
-
+      Nat w | isTBit a -> do
+                  BV _ lw <- fromVWord "arithLeft" l
+                  BV _ rw <- fromVWord "arithRight" r
+                  return $ VWord $ mkBv w (op w lw rw)
+            | otherwise -> VSeq w (isTBit a) <$> (join (zipSeqMap (loop a) <$> (fromSeq l) <*> (fromSeq r)))
      -- streams
-      Inf -> toStream (zipWith (loop a) (fromSeq l) (fromSeq r))
+      Inf -> VStream <$> (join (zipSeqMap (loop a) <$> (fromSeq l) <*> (fromSeq r)))

    -- functions
    | Just (_,ety) <- isTFun ty =
-      lam $ \ x -> loop ety (fromVFun l x) (fromVFun r x)
+      return $ lam $ \ x -> loop' ety (fromVFun l x) (fromVFun r x)

    -- tuples
    | Just (_,tys) <- isTTuple ty =
      let ls = fromVTuple l
          rs = fromVTuple r
-       in VTuple (zipWith3 loop tys ls rs)
+       in return $ VTuple (zipWith3 loop' tys ls rs)

    -- records
    | Just fs <- isTRec ty =
-      VRecord [ (f, loop fty (lookupRecord f l) (lookupRecord f r))
-              | (f,fty) <- fs ]
+      return $ VRecord [ (f, loop' fty (lookupRecord f l) (lookupRecord f r))
+                       | (f,fty) <- fs ]

-    | otherwise = evalPanic "arithBinop" ["Invalid arguments"]
+    | otherwise = evalPanic "arithBinop" ["Invalid arguments", show ty, show l, show r]

 arithUnary :: (Integer -> Integer) -> Unary
 arithUnary op = loop
  where
+  loop' :: TValue -> Eval Value -> Eval Value
+  loop' ty x = loop ty =<< x
+
+  loop :: TValue -> Value -> Eval Value
  loop ty x

    | Just (len,a) <- isTSeq ty = case numTValue len of

      -- words and finite sequences
-      Nat w | isTBit a  -> VWord (mkBv w (op (fromWord x)))
-            | otherwise -> VSeq False (map (loop a) (fromSeq x))
+      Nat w | isTBit a -> do
+                   BV _ wx <- fromVWord "arithUnary" x
+                   return $ VWord $ mkBv w $ op wx
+            | otherwise -> VSeq w (isTBit a) <$> (mapSeqMap (loop a) =<< fromSeq x)

-      Inf -> toStream (map (loop a) (fromSeq x))
+      Inf -> VStream <$> (mapSeqMap (loop a) =<< fromSeq x)

    -- functions
    | Just (_,ety) <- isTFun ty =
-      lam $ \ y -> loop ety (fromVFun x y)
+      return $ lam $ \ y -> loop' ety (fromVFun x y)

    -- tuples
    | Just (_,tys) <- isTTuple ty =
      let as = fromVTuple x
-       in VTuple (zipWith loop tys as)
+       in return $ VTuple (zipWith loop' tys as)

    -- records
    | Just fs <- isTRec ty =
-      VRecord [ (f, loop fty (lookupRecord f x)) | (f,fty) <- fs ]
+      return $ VRecord [ (f, loop' fty (lookupRecord f x)) | (f,fty) <- fs ]

    | otherwise = evalPanic "arithUnary" ["Invalid arguments"]

@ -330,47 +361,58 @@ modWrap x y = x `mod` y
 -- Cmp -------------------------------------------------------------------------

 -- | Lexicographic ordering on two values.
-lexCompare :: TValue -> Value -> Value -> Ordering
-lexCompare ty l r
+lexCompare :: String -> TValue -> Value -> Value -> Eval Ordering
+lexCompare nm ty l r

  | isTBit ty =
-    compare (fromVBit l) (fromVBit r)
+    return $ compare (fromVBit l) (fromVBit r)

-  | Just (_,b) <- isTSeq ty, isTBit b =
-    compare (fromWord l) (fromWord r)
+  | Just (_,b) <- isTSeq ty, isTBit b = do
+    --ldoc <- ppValue defaultPPOpts l
+    --io $ putStrLn $ unwords ["lexCompare left", nm, show l]
+    compare <$> (fromWord "compareLeft" l) <*> (fromWord "compareRight" r)

-  | Just (_,e) <- isTSeq ty =
-    zipLexCompare (repeat e) (fromSeq l) (fromSeq r)
+  | Just (len,e) <- isTSeq ty = case numTValue len of
+      Nat w -> join (zipLexCompare nm (repeat e) <$>
+                    (enumerateSeqMap w <$> fromSeq l) <*>
+                    (enumerateSeqMap w <$> fromSeq r))
+      Inf   -> join (zipLexCompare nm (repeat e) <$>
+                    (streamSeqMap <$> fromSeq l) <*>
+                    (streamSeqMap <$> fromSeq r))

  -- tuples
  | Just (_,etys) <- isTTuple ty =
-    zipLexCompare etys (fromVTuple l) (fromVTuple r)
+    zipLexCompare nm etys (fromVTuple l) (fromVTuple r)

  -- records
  | Just fields <- isTRec ty =
    let tys    = map snd (sortBy (comparing fst) fields)
        ls     = map snd (sortBy (comparing fst) (fromVRecord l))
        rs     = map snd (sortBy (comparing fst) (fromVRecord r))
-     in zipLexCompare tys ls rs
+     in zipLexCompare nm tys ls rs

  | otherwise = evalPanic "lexCompare" ["invalid type"]


 -- XXX the lists are expected to be of the same length, as this should only be
 -- used with values that come from type-correct expressions.
-zipLexCompare :: [TValue] -> [Value] -> [Value] -> Ordering
-zipLexCompare tys ls rs = foldr choose EQ (zipWith3 lexCompare tys ls rs)
+zipLexCompare :: String -> [TValue] -> [Eval Value] -> [Eval Value] -> Eval Ordering
+zipLexCompare nm tys ls rs = foldr choose (return EQ) (zipWith3 lexCompare' tys ls rs)
  where
-  choose c acc = case c of
+  lexCompare' t l r = join (lexCompare nm t <$> l <*> r)
+
+  choose c acc = c >>= \c' -> case c' of
    EQ -> acc
-    _  -> c
+    _  -> return c'

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

-withOrder :: (Ordering -> TValue -> Value -> Value -> Value) -> Binary
-withOrder choose ty l r = choose (lexCompare ty l r) ty l r
+withOrder :: String -> (Ordering -> TValue -> Value -> Value -> Value) -> Binary
+withOrder nm choose ty l r =
+  do ord <- lexCompare nm ty l r
+     return $ choose ord ty l r

 maxV :: Ordering -> TValue -> Value -> Value -> Value
 maxV o _ l r = case o of
@ -387,9 +429,15 @@ funCmp :: (Ordering -> Bool) -> Value
 funCmp op =
  tlam $ \ _a ->
  tlam $ \  b ->
-   lam $ \  l ->
-   lam $ \  r ->
-   lam $ \  x -> cmpOrder op b (fromVFun l x) (fromVFun r x)
+   lam $ \  l -> return $
+   lam $ \  r -> return $
+   lam $ \  x -> do
+      l' <- l
+      r' <- r
+      x' <- x
+      fl <- fromVFun l' (ready x')
+      fr <- fromVFun r' (ready x')
+      cmpOrder "funCmp" op b fl fr


 -- Logic -----------------------------------------------------------------------
@ -405,45 +453,87 @@ zeroV ty
  | Just (n,ety) <- isTSeq ty =
    case numTValue n of
      Nat w | isTBit ety -> word w 0
-            | otherwise  -> toSeq n ety (replicate (fromInteger w) (zeroV ety))
-      Inf                -> toSeq n ety (repeat                    (zeroV ety))
+            | otherwise  -> mkSeq n ety (SeqMap $ \_ -> ready $ zeroV ety)
+      Inf                -> mkSeq n ety (SeqMap $ \_ -> ready $ zeroV ety)

  -- functions
  | Just (_,bty) <- isTFun ty =
-    lam (\ _ -> zeroV bty)
+    lam (\ _ -> ready (zeroV bty))

  -- tuples
  | Just (_,tys) <- isTTuple ty =
-    VTuple (map zeroV tys)
+    VTuple (map (ready . zeroV) tys)

  -- records
  | Just fields <- isTRec ty =
-    VRecord [ (f,zeroV fty) | (f,fty) <- fields ]
+    VRecord [ (f,ready $ zeroV fty) | (f,fty) <- fields ]

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

-- | Join a sequence of sequences into a single sequence.
-joinV :: TValue -> TValue -> TValue -> Value -> Value
-joinV parts each a val =
-  let len = toNumTValue (numTValue parts `nMul` numTValue each)
-  in toSeq len a (concatMap fromSeq (fromSeq val))

-splitAtV :: TValue -> TValue -> TValue -> Value -> Value
+joinWord :: BV -> BV -> BV
+joinWord (BV i x) (BV j y) =
+  BV (i + j) (shiftL x (fromInteger j) + y)
+
+joinWords :: Integer -> Integer -> SeqValMap -> Eval Value -> Eval Value
+joinWords nParts nEach xs fallback =
+  loop (mkBv 0 0) (enumerateSeqMap nParts xs)
+
+ where
+ loop !bv [] = return $ VWord bv
+ loop !bv (Ready (VWord w) : ws) = loop (joinWord bv w) ws
+ loop _   _ = fallback
+
+joinSeq :: TValue -> TValue -> TValue -> SeqValMap -> Eval Value
+joinSeq parts each a xs
+  | Nat nEach <- numTValue each
+  = mkSeq <$> memoMap (SeqMap $ \i -> do
+      let (q,r) = divMod i nEach
+      ys <- fromSeq =<< lookupSeqMap xs q
+      lookupSeqMap ys r)
+
+  where
+  len = numTValue parts `nMul` numTValue each
+  mkSeq = case len of
+            Inf    -> VStream
+            Nat n  -> VSeq n (isTBit a)
+
+-- | Join a sequence of sequences into a single sequence.
+joinV :: TValue -> TValue -> TValue -> Value -> Eval Value
+joinV parts each a val
+  -- Try to join a sequence of words, if we can determine that
+  -- each element is actually a word.  Fall back on sequence
+  -- join otherwise.
+  | Nat nParts  <- numTValue parts
+  , Nat nEach   <- numTValue each
+  , isTBit a
+  = do xs <- fromSeq val
+       joinWords nParts nEach xs (joinSeq parts each a xs)
+
+joinV parts each a val =
+       joinSeq parts each a =<< fromSeq val
+
+
+splitAtV :: TValue -> TValue -> TValue -> Value -> Eval Value
 splitAtV front back a val =
  case numTValue back of

    -- Remember that words are big-endian in cryptol, so the first component
    -- needs to be shifted, and the second component just needs to be masked.
-    Nat rightWidth | aBit, VWord (BV _ i) <- val ->
-          VTuple [ VWord (BV leftWidth (i `shiftR` fromInteger rightWidth))
-                 , VWord (mkBv rightWidth i) ]
+    Nat rightWidth | aBit, VWord (BV _ i) <- val -> do
+          return $ VTuple
+                   [ ready $ VWord (BV leftWidth (i `shiftR` fromInteger rightWidth))
+                   , ready $ VWord (mkBv rightWidth i) ]

-    _ ->
-      let (ls,rs) = genericSplitAt leftWidth (fromSeq val)
-       in VTuple [VSeq aBit ls, toSeq back a rs]
+    _ -> do
+       seq <- delay Nothing (fromSeq val)
+       ls  <- delay Nothing (fst . splitSeqMap leftWidth <$> seq)
+       rs  <- delay Nothing (snd . splitSeqMap leftWidth <$> seq)
+       return $ VTuple [ VSeq leftWidth aBit <$> ls
+                       , mkSeq back a <$> rs
+                       ]

  where
-
  aBit = isTBit a

  leftWidth = case numTValue front of
@ -457,12 +547,18 @@ ecSplitV =
  tlam $ \ parts ->
  tlam $ \ each  ->
  tlam $ \ a     ->
-  lam  $ \ val ->
-  let mkChunks f = map (toFinSeq a) $ f $ fromSeq val
-  in case (numTValue parts, numTValue each) of
-       (Nat p, Nat e) -> VSeq False $ mkChunks (finChunksOf p e)
-       (Inf  , Nat e) -> toStream   $ mkChunks (infChunksOf e)
-       _              -> evalPanic "splitV" ["invalid type arguments to split"]
+  lam  $ \ val -> do
+  val' <- delay Nothing (fromSeq =<< val)
+  case (numTValue parts, numTValue each) of
+     (Nat p, Nat e) -> return $ VSeq p False $ SeqMap $ \i ->
+                       return $ VSeq e (isTBit a) $ SeqMap $ \j -> do
+                         xs <- val'
+                         lookupSeqMap xs (e * i + j)
+     (Inf  , Nat e) -> return $ VStream $ SeqMap $ \i ->
+                       return $ VSeq e (isTBit a) $ SeqMap $ \j -> do
+                         xs <- val'
+                         lookupSeqMap xs (e * i + j)
+     _              -> evalPanic "splitV" ["invalid type arguments to split"]

 -- | Split into infinitely many chunks
 infChunksOf :: Integer -> [a] -> [[a]]
@ -476,73 +572,122 @@ finChunksOf parts each xs = let (as,bs) = genericSplitAt each xs
                            in as : finChunksOf (parts - 1) each bs


-ccatV :: TValue -> TValue -> TValue -> Value -> Value -> Value
-ccatV _front _back (isTBit -> True) (VWord (BV i x)) (VWord (BV j y)) =
-  VWord (BV (i + j) (shiftL x (fromInteger j) + y))
-ccatV front back elty l r =
-  toSeq (evalTF TCAdd [front,back]) elty (fromSeq l ++ fromSeq r)
+reverseV :: Value -> Eval Value
+reverseV (VSeq n isWord xs) =
+  return $ VSeq n isWord $ reverseSeqMap n xs
+reverseV (VWord w) = return (VWord revword)
+ where
+ revword = do
+   let bs = unpackWord w :: [Bool]
+    in packWord $ reverse bs
+reverseV _ =
+  evalPanic "reverseV" ["Not a finite sequence"]
+
+
+transposeV :: TValue -> TValue -> TValue -> Value -> Eval Value
+transposeV a b c xs = do
+  let bseq = 
+        case numTValue b of
+          Nat nb -> VSeq nb (isTBit b)
+          Inf    -> VStream
+  let aseq =
+        case numTValue a of
+          Nat na -> VSeq na (isTBit a)
+          Inf    -> VStream
+  return $ bseq $ SeqMap $ \bi ->
+    return $ aseq $ SeqMap $ \ai -> do
+      ys  <- flip lookupSeqMap ai =<< fromSeq xs
+      z   <- flip lookupSeqMap bi =<< fromSeq ys  
+      return z
+
+ccatV :: TValue -> TValue -> TValue -> Eval Value -> Eval Value -> Eval Value
+ccatV _front _back (isTBit -> True) (Ready (VWord x)) (Ready (VWord y)) =
+  return $ VWord $ joinWord x y
+
+ccatV front back elty l r = do
+  l' <- delay Nothing (fromSeq =<< l)
+  r' <- delay Nothing (fromSeq =<< r)
+  let Nat n = numTValue front
+  mkSeq (evalTF TCAdd [front,back]) elty <$> memoMap (SeqMap $ \i ->
+     if i < n then do
+       ls <- l'
+       lookupSeqMap ls i
+     else do
+       rs <- r'
+       lookupSeqMap rs (i-n))

 -- | Merge two values given a binop.  This is used for and, or and xor.
 logicBinary :: (forall a. Bits a => a -> a -> a) -> Binary
 logicBinary op = loop
  where
+  loop' :: TValue -> Eval Value -> Eval Value -> Eval Value
+  loop' ty l r = join (loop ty <$> l <*> r)
+
+  loop :: TValue -> Value -> Value -> Eval Value
  loop ty l r
-    | isTBit ty = VBit (op (fromVBit l) (fromVBit r))
+    | isTBit ty = return $ VBit (op (fromVBit l) (fromVBit r))
    | Just (len,aty) <- isTSeq ty =

      case numTValue len of

         -- words or finite sequences
-         Nat w | isTBit aty -> VWord (BV w (op (fromWord l) (fromWord r)))
-                               -- We assume that bitwise ops do not need re-masking
-               | otherwise -> VSeq False (zipWith (loop aty) (fromSeq l)
-                                                             (fromSeq r))
+         Nat w | isTBit aty, VWord (BV _ lw) <- l, VWord (BV _ rw) <- r
+              -> return $ VWord $ (BV w (op lw rw))
+                   -- We assume that bitwise ops do not need re-masking
+               | otherwise -> VSeq w (isTBit aty) <$> (join (zipSeqMap (loop aty) <$> (fromSeq l) <*> (fromSeq r)))

         -- streams
-         Inf -> toStream (zipWith (loop aty) (fromSeq l) (fromSeq r))
+         Inf -> VStream <$> (join (zipSeqMap (loop aty) <$> (fromSeq l) <*> (fromSeq r)))

-    | Just (_,etys) <- isTTuple ty =
-      let ls = fromVTuple l
-          rs = fromVTuple r
-       in VTuple (zipWith3 loop etys ls rs)
+    | Just (_,etys) <- isTTuple ty = do
+        let ls = fromVTuple l
+        let rs = fromVTuple r
+        return $ VTuple $ (zipWith3 loop' etys ls rs)

    | Just (_,bty) <- isTFun ty =
-      lam $ \ a -> loop bty (fromVFun l a) (fromVFun r a)
+        return $ lam $ \ a -> loop' bty (fromVFun l a) (fromVFun r a)

    | Just fields <- isTRec ty =
-      VRecord [ (f,loop fty a b) | (f,fty) <- fields
-                                 , let a = lookupRecord f l
-                                       b = lookupRecord f r
-                                 ]
+        return $ VRecord [ (f,loop' fty a b)
+                         | (f,fty) <- fields 
+                         , let a = lookupRecord f l
+                               b = lookupRecord f r 
+                         ]

    | otherwise = evalPanic "logicBinary" ["invalid logic type"]

 logicUnary :: (forall a. Bits a => a -> a) -> Unary
 logicUnary op = loop
  where
+  loop' :: TValue -> Eval Value -> Eval Value
+  loop' ty val = loop ty =<< val
+
+  loop :: TValue -> Value -> Eval Value
  loop ty val
-    | isTBit ty = VBit (op (fromVBit val))
+    | isTBit ty = return . VBit . op $ fromVBit val

    | Just (len,ety) <- isTSeq ty =

      case numTValue len of

         -- words or finite sequences
-         Nat w | isTBit ety -> VWord (mkBv w (op (fromWord val)))
-               | otherwise -> VSeq False (map (loop ety) (fromSeq val))
+         Nat w | isTBit ety, VWord (BV _ v) <- val
+              -> return $ VWord (mkBv w $ op v)
+               | otherwise
+              -> VSeq w (isTBit ety) <$> (mapSeqMap (loop ety) =<< fromSeq val)

         -- streams
-         Inf -> toStream (map (loop ety) (fromSeq val))
+         Inf -> VStream <$> (mapSeqMap (loop ety) =<< fromSeq val)

    | Just (_,etys) <- isTTuple ty =
      let as = fromVTuple val
-       in VTuple (zipWith loop etys as)
+       in return $ VTuple (zipWith loop' etys as)

    | Just (_,bty) <- isTFun ty =
-      lam $ \ a -> loop bty (fromVFun val a)
+      return $ lam $ \ a -> loop' bty (fromVFun val a)

    | Just fields <- isTRec ty =
-      VRecord [ (f,loop fty a) | (f,fty) <- fields, let a = lookupRecord f val ]
+      return $ VRecord [ (f,loop' fty a) | (f,fty) <- fields, let a = lookupRecord f val ]

    | otherwise = evalPanic "logicUnary" ["invalid logic type"]

@ -550,20 +695,21 @@ logicUnary op = loop
 logicShift :: (Integer -> Integer -> Integer -> Integer)
              -- ^ The function may assume its arguments are masked.
              -- It is responsible for masking its result if needed.
-           -> (TValue -> TValue -> [Value] -> Integer -> [Value])
+           -> (TValue -> TValue -> SeqValMap -> Integer -> SeqValMap)
           -> Value
 logicShift opW opS
  = tlam $ \ a ->
    tlam $ \ _ ->
    tlam $ \ c ->
-     lam  $ \ l ->
-     lam  $ \ r ->
+     lam  $ \ l -> return $
+     lam  $ \ r -> do
        if isTBit c
-          then -- words
-            let BV w i  = fromVWord l
-            in VWord (BV w (opW w i (fromWord r)))
-
-          else toSeq a c (opS a c (fromSeq l) (fromWord r))
+          then do -- words
+            l' <- l
+            BV w i <- fromVWord ("logicShift " ++ show l') l'
+            VWord <$> (BV w <$> (opW w i <$> (fromWord "logic shift amount" =<< r)))
+          else do
+            mkSeq a c <$> (opS a c <$> (fromSeq =<< l) <*> (fromWord "logic shift amount" =<< r))

 -- Left shift for words.
 shiftLW :: Integer -> Integer -> Integer -> Integer
@ -571,26 +717,31 @@ shiftLW w ival by
  | by >= w   = 0
  | otherwise = mask w (shiftL ival (fromInteger by))

-shiftLS :: TValue -> TValue -> [Value] -> Integer -> [Value]
-shiftLS w ety vs by =
+shiftLS :: TValue -> TValue -> SeqValMap -> Integer -> SeqValMap
+shiftLS w ety vs by = SeqMap $ \i ->
  case numTValue w of
    Nat len
-      | by < len  -> genericTake len (genericDrop by vs ++ repeat (zeroV ety))
-      | otherwise -> genericReplicate len (zeroV ety)
-    Inf           -> genericDrop by vs
+      | 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)

-shiftRS :: TValue -> TValue -> [Value] -> Integer -> [Value]
-shiftRS w ety vs by =
+shiftRS :: TValue -> TValue -> SeqValMap -> Integer -> SeqValMap
+shiftRS w ety vs by = SeqMap $ \i ->
  case numTValue w of
    Nat len
-      | by < len  -> genericTake len (genericReplicate by (zeroV ety) ++ vs)
-      | otherwise -> genericReplicate len (zeroV ety)
-    Inf           -> genericReplicate by (zeroV ety) ++ vs
+      | 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
@ -598,12 +749,10 @@ 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 :: TValue -> TValue -> [Value] -> Integer -> [Value]
-rotateLS w _ vs at =
+rotateLS :: TValue -> TValue -> SeqValMap -> Integer -> SeqValMap
+rotateLS w _ vs by = SeqMap $ \i ->
  case numTValue w of
-    Nat len -> let at'     = at `mod` len
-                   (ls,rs) = genericSplitAt at' vs
-                in rs ++ ls
+    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
@ -612,61 +761,61 @@ 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 :: TValue -> TValue -> [Value] -> Integer -> [Value]
-rotateRS w _ vs at =
+rotateRS :: TValue -> TValue -> SeqValMap -> Integer -> SeqValMap
+rotateRS w _ vs by = SeqMap $ \i ->
  case numTValue w of
-    Nat len -> let at'     = at `mod` len
-                   (ls,rs) = genericSplitAt (len - at') vs
-                in rs ++ ls
+    Nat len -> lookupSeqMap vs ((len - by + i) `mod` len)
    _ -> panic "Cryptol.Eval.Prim.rotateRS" [ "unexpected infinite sequence" ]


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

 -- | Indexing operations that return one element.
-indexPrimOne :: (Maybe Integer -> [Value] -> Integer -> Value) -> Value
+indexPrimOne :: (Maybe Integer -> SeqValMap -> Integer -> Eval Value) -> Value
 indexPrimOne op =
  tlam $ \ n  ->
  tlam $ \ _a ->
  tlam $ \ _i ->
-   lam $ \ l  ->
-   lam $ \ r  ->
-     let vs  = fromSeq l
-         ix  = fromWord r
-      in op (fromNat (numTValue n)) vs ix
+   lam $ \ l  -> return $
+   lam $ \ r  -> do
+      vs <- fromSeq =<< l
+      ix <- fromWord "index one" =<< r
+      op (fromNat (numTValue n)) vs ix

-indexFront :: Maybe Integer -> [Value] -> Integer -> Value
+indexFront :: Maybe Integer -> SeqValMap -> Integer -> Eval Value
 indexFront mblen vs ix =
  case mblen of
    Just len | len <= ix -> invalidIndex ix
-    _                    -> genericIndex vs ix
+    _                    -> lookupSeqMap vs ix

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

 -- | Indexing operations that return many elements.
-indexPrimMany :: (Maybe Integer -> [Value] -> [Integer] -> [Value]) -> Value
+indexPrimMany :: (Maybe Integer -> SeqValMap -> Integer -> Eval Value) -> Value
 indexPrimMany op =
  tlam $ \ n  ->
  tlam $ \ a  ->
  tlam $ \ m  ->
  tlam $ \ _i ->
-   lam $ \ l  ->
-   lam $ \ r  ->
-     let vs    = fromSeq l
-         ixs   = map fromWord (fromSeq r)
-     in toSeq m a (op (fromNat (numTValue n)) vs ixs)
+   lam $ \ l  -> return $
+   lam $ \ r  -> do
+     vs  <- fromSeq =<< l
+     ixs <- fromSeq =<< r
+     mkSeq m a <$> memoMap (SeqMap $ \i -> do
+       i' <- fromWord "index many" =<< lookupSeqMap ixs i
+       op (fromNat (numTValue n)) vs i')

-indexFrontRange :: Maybe Integer -> [Value] -> [Integer] -> [Value]
-indexFrontRange mblen vs = map (indexFront mblen vs)
+--indexFrontRange :: Maybe Integer -> [Value] -> [Integer] -> [Value]
+--indexFrontRange mblen vs = map (indexFront mblen vs)

-indexBackRange :: Maybe Integer -> [Value] -> [Integer] -> [Value]
-indexBackRange mblen vs = map (indexBack mblen vs)
+--indexBackRange :: Maybe Integer -> [Value] -> [Integer] -> [Value]
+--indexBackRange mblen vs = map (indexBack mblen vs)

 -- @[ 0, 1 .. ]@
 fromThenV :: Value
@ -680,7 +829,8 @@ fromThenV  =
        | bits' >= Arch.maxBigIntWidth -> wordTooWide bits'
      (Nat first', Nat next', Nat len', Nat bits') ->
        let nums = enumFromThen first' next'
-         in VSeq False (genericTake len' (map (VWord . BV bits') nums))
+         in VSeq len' False $ SeqMap $ genericIndex $ genericTake len'
+              $ map (ready . VWord . BV bits') nums
      _ -> evalPanic "fromThenV" ["invalid arguments"]

 -- @[ 0 .. 10 ]@
@ -695,7 +845,8 @@ fromToV  =
      (Nat first', Nat lst', Nat bits') ->
        let nums = enumFromThenTo first' (first' + 1) lst'
            len  = 1 + (lst' - first')
-         in VSeq False (genericTake len (map (VWord . BV bits') nums))
+         in VSeq len False $ SeqMap $ genericIndex $ genericTake len
+              $ map (ready . VWord . BV bits') nums

      _ -> evalPanic "fromThenV" ["invalid arguments"]

@ -712,7 +863,8 @@ fromThenToV  =
        | bits' >= Arch.maxBigIntWidth -> wordTooWide bits'
      (Nat first', Nat next', Nat lst', Nat len', Nat bits') ->
        let nums = enumFromThenTo first' next' lst'
-         in VSeq False (genericTake len' (map (VWord . BV bits') nums))
+         in VSeq len' False $ SeqMap $ genericIndex $ genericTake len' $
+            map (ready . VWord . BV bits') nums

      _ -> evalPanic "fromThenV" ["invalid arguments"]

@ -735,4 +887,4 @@ randomV ty seed =
 -- Miscellaneous ---------------------------------------------------------------

 tlamN :: (Nat' -> GenValue b w) -> GenValue b w
-tlamN f = VPoly (\x -> f (numTValue x))
+tlamN f = VPoly (\x -> ready $ f (numTValue x))
--- a/src/Cryptol/REPL/Command.hs
+++ b/src/Cryptol/REPL/Command.hs
@ -56,6 +56,7 @@ import qualified Cryptol.ModuleSystem.NamingEnv as M
 import qualified Cryptol.ModuleSystem.Renamer as M (RenamerWarning(SymbolShadowed))
 import qualified Cryptol.Utils.Ident as M

+import qualified Cryptol.Eval.Monad as E
 import qualified Cryptol.Eval.Value as E
 import Cryptol.Testing.Concrete
 import qualified Cryptol.Testing.Random  as TestR
@ -245,13 +246,16 @@ evalCmd str = do
    P.ExprInput expr -> do
      (val,_ty) <- replEvalExpr expr
      ppOpts <- getPPValOpts
+      valDoc <- io $ rethrowEvalError $ E.runEval $ E.ppValue ppOpts val
+
      -- This is the point where the value gets forced. We deepseq the
      -- pretty-printed representation of it, rather than the value
      -- itself, leaving it up to the pretty-printer to determine how
      -- much of the value to force
-      out <- io $ rethrowEvalError
-                $ return $!! show $ pp $ E.WithBase ppOpts val
-      rPutStrLn out
+      --out <- io $ rethrowEvalError
+      --          $ return $!! show $ pp $ E.WithBase ppOpts val
+
+      rPutStrLn (show valDoc)
    P.LetInput decl -> do
      -- explicitly make this a top-level declaration, so that it will
      -- be generalized if mono-binds is enabled
@ -367,13 +371,13 @@ qcCmd qcMode str =
        prtLn "FAILED"
      FailFalse vs -> do
        prtLn "FAILED for the following inputs:"
-        mapM_ (rPrint . pp . E.WithBase opts) vs
+        mapM_ (\v -> rPrint =<< (io $ E.runEval $ E.ppValue opts v)) vs
      FailError err [] -> do
        prtLn "ERROR"
        rPrint (pp err)
      FailError err vs -> do
        prtLn "ERROR for the following inputs:"
-        mapM_ (rPrint . pp . E.WithBase opts) vs
+        mapM_ (\v -> rPrint =<< (io $ E.runEval $ E.ppValue opts v)) vs
        rPrint (pp err)
      Pass -> panic "Cryptol.REPL.Command" ["unexpected Test.Pass"]

@ -436,8 +440,8 @@ cmdProveSat isSat expr = do
              vss  = map (map $ \(_,_,v) -> v)     tevss
              ppvs vs = do
                parseExpr <- replParseExpr expr
-                let docs = map (pp . E.WithBase ppOpts) vs
-                    -- function application has precedence 3
+                docs <- mapM (io . E.runEval . E.ppValue ppOpts) vs
+                let -- function application has precedence 3
                    doc = ppPrec 3 parseExpr
                rPrint $ hsep (doc : docs) <+>
                  text (if isSat then "= True" else "= False")
@ -580,8 +584,9 @@ writeFileCmd file str = do
  tIsByte    x = maybe False
                       (\(n,b) -> T.tIsBit b && T.tIsNum n == Just 8)
                       (T.tIsSeq x)
-  serializeValue (E.VSeq _ vs) =
-    return $ BS.pack $ map (serializeByte . E.fromVWord) vs
+  serializeValue (E.VSeq n _ vs) = do
+    ws <- io $ E.runEval (mapM (>>=E.fromVWord "serializeValue") $ E.enumerateSeqMap n vs)
+    return $ BS.pack $ map serializeByte ws
  serializeValue _             =
    panic "Cryptol.REPL.Command.writeFileCmd"
      ["Impossible: Non-VSeq value of type [n][8]."]
@ -901,8 +906,7 @@ replEvalExpr expr =
               let su = T.listSubst [ (T.tpVar a, t) | (a,t) <- tys ]
               return (def1, T.apSubst su (T.sType sig))

-     val <- liftModuleCmd (M.evalExpr def1)
-     _ <- io $ rethrowEvalError $ X.evaluate val
+     val <- liftModuleCmd (rethrowEvalError . M.evalExpr def1)
     whenDebug (rPutStrLn (dump def1))
     -- add "it" to the namespace
     bindItVariable ty def1
--- a/src/Cryptol/Symbolic.hs
+++ b/src/Cryptol/Symbolic.hs
@ -113,6 +113,13 @@ proverError :: String -> M.ModuleCmd ProverResult
 proverError msg modEnv = return (Right (ProverError msg, modEnv), [])

 satProve :: ProverCommand -> M.ModuleCmd ProverResult
+satProve _ = fail "IMPLEMENT satProve"
+
+satProveOffline :: ProverCommand -> M.ModuleCmd (Either String String)
+satProveOffline _ = fail "IMPLEMENT satProveOffline"
+
+{-
+
 satProve ProverCommand {..} = protectStack proverError $ \modEnv ->
  M.runModuleM modEnv $ do
  let (isSat, mSatNum) = case pcQueryType of
@ -489,3 +496,4 @@ evalMatch :: Env -> Match -> [Env]
 evalMatch env m = case m of
  From n _ty expr -> [ bindVar (n, v) env | v <- fromSeq (evalExpr env expr) ]
  Let d           -> [ bindVar (evalDecl env d) env ]
+-}
--- a/src/Cryptol/Symbolic/Prims.hs
+++ b/src/Cryptol/Symbolic/Prims.hs
@ -47,7 +47,10 @@ evalPrim Decl { .. } =
 -- See also Cryptol.Prims.Eval.primTable
 primTable :: Map.Map Ident Value
 primTable  = Map.fromList $ map (\(n, v) -> (mkIdent (T.pack n), v))
-  [ ("True"        , VBit SBV.svTrue)
+  [
+  ]
+{-
+("True"        , VBit SBV.svTrue)
  , ("False"       , VBit SBV.svFalse)
  , ("demote"      , ecDemoteV) -- Converts a numeric type into its corresponding value.
                                -- { val, bits } (fin val, fin bits, bits >= width val) => [bits]
@ -730,3 +733,4 @@ divx n i xs ys'        = (q:qs, rs)
  where q        = xs `idx` i
        xs'      = ites q (xs `addPoly` ys') xs
        (qs, rs) = divx (n-1) (i-1) xs' (tail ys')
+-}
--- a/src/Cryptol/Symbolic/Value.hs
+++ b/src/Cryptol/Symbolic/Value.hs
@ -31,11 +31,12 @@ import Data.List (foldl')

 import Data.SBV.Dynamic

+--import Cryptol.Eval.Monad
 import Cryptol.Eval.Value (TValue, numTValue, toNumTValue, finTValue, isTBit,
                           isTFun, isTSeq, isTTuple, isTRec, tvSeq, GenValue(..),
                           BitWord(..), lam, tlam, toStream, toFinSeq, toSeq,
                           fromSeq, fromVBit, fromVWord, fromVFun, fromVPoly,
-                           fromVTuple, fromVRecord, lookupRecord)
+                           fromVTuple, fromVRecord, lookupRecord, SeqMap(..))
 import Cryptol.Utils.Panic (panic)

 -- SBool and SWord -------------------------------------------------------------
@ -79,26 +80,27 @@ mergeValue :: Bool -> SBool -> Value -> Value -> Value
 mergeValue f c v1 v2 =
  case (v1, v2) of
    (VRecord fs1, VRecord fs2) -> VRecord $ zipWith mergeField fs1 fs2
-    (VTuple vs1 , VTuple vs2 ) -> VTuple $ zipWith (mergeValue f c) vs1 vs2
+    (VTuple vs1 , VTuple vs2 ) -> VTuple $ zipWith (\x y -> mergeValue f c <$> x <*> y) vs1 vs2
    (VBit b1    , VBit b2    ) -> VBit $ mergeBit b1 b2
    (VWord w1   , VWord w2   ) -> VWord $ mergeWord w1 w2
-    (VSeq b1 vs1, VSeq _ vs2 ) -> VSeq b1 $ zipWith (mergeValue f c) vs1 vs2
-    (VStream vs1, VStream vs2) -> VStream $ mergeStream vs1 vs2
-    (VFun f1    , VFun f2    ) -> VFun $ \x -> mergeValue f c (f1 x) (f2 x)
-    (VPoly f1   , VPoly f2   ) -> VPoly $ \x -> mergeValue f c (f1 x) (f2 x)
-    (VWord w1   , _          ) -> VWord $ mergeWord w1 (fromVWord v2)
-    (_          , VWord w2   ) -> VWord $ mergeWord (fromVWord v1) w2
+    (VSeq n1 b1 vs1, VSeq n2 _ vs2 ) | n1 == n2 -> VSeq n1 b1 $ mergeSeqMap vs1 vs2
+    (VStream vs1, VStream vs2) -> VStream $ mergeSeqMap vs1 vs2
+    (VFun f1    , VFun f2    ) -> VFun $ \x -> mergeValue f c <$> (f1 x) <*> (f2 x)
+    (VPoly f1   , VPoly f2   ) -> VPoly $ \x -> mergeValue f c <$> (f1 x) <*> (f2 x)
+-- FIXME!
+--    (VWord w1   , _          ) -> VWord $ mergeWord w1 (fromVWord v2)
+--    (_          , VWord   w2 ) -> VWord $ mergeWord (fromVWord v1) w2
    (_          , _          ) -> panic "Cryptol.Symbolic.Value"
                                  [ "mergeValue: incompatible values" ]
  where
    mergeBit b1 b2 = svSymbolicMerge KBool f c b1 b2
    mergeWord w1 w2 = svSymbolicMerge (kindOf w1) f c w1 w2
    mergeField (n1, x1) (n2, x2)
-      | n1 == n2  = (n1, mergeValue f c x1 x2)
+      | n1 == n2  = (n1, mergeValue f c <$> x1 <*> x2)
      | otherwise = panic "Cryptol.Symbolic.Value"
                    [ "mergeValue.mergeField: incompatible values" ]
-    mergeStream xs ys =
-      mergeValue f c (head xs) (head ys) : mergeStream (tail xs) (tail ys)
+    mergeSeqMap x y =
+      SeqMap $ \i -> mergeValue f c <$> lookupSeqMap x i <*> lookupSeqMap y i

 -- Big-endian Words ------------------------------------------------------------

--- a/src/Cryptol/Testing/Concrete.hs
+++ b/src/Cryptol/Testing/Concrete.hs
@ -9,7 +9,9 @@
 {-# LANGUAGE RecordWildCards #-}
 module Cryptol.Testing.Concrete where

-import Cryptol.Eval.Error
+import Control.Monad (join)
+
+import Cryptol.Eval.Monad
 import Cryptol.Eval.Value
 import Cryptol.TypeCheck.AST
 import Cryptol.Utils.Panic (panic)
@ -19,6 +21,7 @@ import Data.List(genericReplicate)

 import Prelude ()
 import Prelude.Compat
+import Data.List (genericIndex)

 -- | A test result is either a pass, a failure due to evaluating to
 -- @False@, or a failure due to an exception raised during evaluation
@ -39,22 +42,24 @@ runOneTest :: Value -> [Value] -> IO TestResult
 runOneTest v0 vs0 = run `X.catch` handle
  where
    run = do
-      result <- X.evaluate (go v0 vs0)
+      result <- runEval (go v0 vs0)
      if result
        then return Pass
        else return (FailFalse vs0)
    handle e = return (FailError e vs0)

-    go :: Value -> [Value] -> Bool
-    go (VFun f) (v : vs) = go (f v) vs
+    go :: Value -> [Value] -> Eval Bool
+    go (VFun f) (v : vs) = join (go <$> (f (ready v)) <*> return vs)
    go (VFun _) []       = panic "Not enough arguments while applying function"
                           []
-    go (VBit b) []       = b
-    go v vs              = panic "Type error while running test" $
-                           [ "Function:"
-                           , show $ ppValue defaultPPOpts v
-                           , "Arguments:"
-                           ] ++ map (show . ppValue defaultPPOpts) vs
+    go (VBit b) []       = return b
+    go v vs              = do vdoc    <- ppValue defaultPPOpts v
+                              vsdocs  <- mapM (ppValue defaultPPOpts) vs
+                              panic "Type error while running test" $
+                               [ "Function:"
+                               , show vdoc
+                               , "Arguments:"
+                               ] ++ map show vsdocs

 {- | Given a (function) type, compute all possible inputs for it.
 We also return the total number of test (i.e., the length of the outer list. -}
@ -102,7 +107,7 @@ typeValues ty =
    TVar _      -> []
    TUser _ _ t -> typeValues t
    TRec fs     -> [ VRecord xs
-                   | xs <- sequence [ [ (f,v) | v <- typeValues t ]
+                   | xs <- sequence [ [ (f,ready v) | v <- typeValues t ]
                                    | (f,t) <- fs ]
                   ]
    TCon (TC tc) ts ->
@ -116,13 +121,16 @@ typeValues ty =
                  [ VWord (BV n x) | x <- [ 0 .. 2^n - 1 ] ]

              [ TCon (TC (TCNum n)) _, t ] ->
-                  [ VSeq False xs | xs <- sequence $ genericReplicate n
-                                                   $ typeValues t ]
+                  [ VSeq n False (SeqMap $ \i -> return $ genericIndex xs i)
+                  | xs <- sequence $ genericReplicate n
+                                   $ typeValues t ]
              _ -> []


        (TCFun, _)       -> []  -- We don't generate function values.
-        (TCTuple _, els) -> [ VTuple xs | xs <- sequence (map typeValues els)]
+        (TCTuple _, els) -> [ VTuple (map ready xs)
+                            | xs <- sequence (map typeValues els)
+                            ]
        (TCNewtype _, _) -> []

    TCon _ _ -> []
--- a/src/Cryptol/Testing/Random.hs
+++ b/src/Cryptol/Testing/Random.hs
@ -11,13 +11,14 @@
 {-# LANGUAGE BangPatterns #-}
 module Cryptol.Testing.Random where

-import Cryptol.Eval.Value     (BV(..),Value,GenValue(..))
+import Cryptol.Eval.Monad     (ready)
+import Cryptol.Eval.Value     (BV(..),Value,GenValue(..),SeqMap(..))
 import qualified Cryptol.Testing.Concrete as Conc
 import Cryptol.TypeCheck.AST  (Type(..),TCon(..),TC(..),tNoUser)
 import Cryptol.Utils.Ident    (Ident)

 import Control.Monad          (forM)
-import Data.List              (unfoldr, genericTake)
+import Data.List              (unfoldr, genericTake, genericIndex)
 import System.Random          (RandomGen, split, random, randomR)

 type Gen g = Integer -> g -> (Value, g)
@ -106,7 +107,7 @@ randomWord w _sz g =
 randomStream :: RandomGen g => Gen g -> Gen g
 randomStream mkElem sz g =
  let (g1,g2) = split g
-  in (VStream (unfoldr (Just . mkElem sz) g1), g2)
+  in (VStream $ SeqMap $ genericIndex (map ready (unfoldr (Just . mkElem sz) g1)), g2)

 {- | Generate a random sequence.  Generally, this should be used for sequences
 other than bits.  For sequences of bits use "randomWord".  The difference
@ -114,7 +115,7 @@ is mostly about how the results will be displayed. -}
 randomSequence :: RandomGen g => Integer -> Gen g -> Gen g
 randomSequence w mkElem sz g =
  let (g1,g2) = split g
-  in (VSeq False $ genericTake w $ unfoldr (Just . mkElem sz) g1 , g2)
+  in (VSeq w False $ SeqMap $ genericIndex (map ready (genericTake w $ unfoldr (Just . mkElem sz) g1)), g2)

 -- | Generate a random tuple value.
 randomTuple :: RandomGen g => [Gen g] -> Gen g
@ -123,7 +124,7 @@ randomTuple gens sz = go [] gens
  go els [] g = (VTuple (reverse els), g)
  go els (mkElem : more) g =
    let (v, g1) = mkElem sz g
-    in go (v : els) more g1
+    in go (ready v : els) more g1

 -- | Generate a random record value.
 randomRecord :: RandomGen g => [(Ident, Gen g)] -> Gen g
@ -132,7 +133,7 @@ randomRecord gens sz = go [] gens
  go els [] g = (VRecord (reverse els), g)
  go els ((l,mkElem) : more) g =
    let (v, g1) = mkElem sz g
-    in go ((l,v) : els) more g1
+    in go ((l,ready v) : els) more g1

 {-
 test = do
--- a/src/Cryptol/Transform/MonoValues.hs
+++ b/src/Cryptol/Transform/MonoValues.hs
@ -185,7 +185,7 @@ rewE rews = go
      ESel e s        -> ESel    <$> go e  <*> return s
      EIf e1 e2 e3    -> EIf     <$> go e1 <*> go e2 <*> go e3

-      EComp t e mss   -> EComp t <$> go e  <*> mapM (mapM (rewM rews)) mss
+      EComp len t e mss -> EComp len t <$> go e  <*> mapM (mapM (rewM rews)) mss
      EVar _          -> return expr

      ETAbs x e       -> ETAbs x  <$> go e
@ -203,7 +203,7 @@ rewE rews = go
 rewM :: RewMap -> Match -> M Match
 rewM rews ma =
  case ma of
-    From x t e -> From x t <$> rewE rews e
+    From x len t e -> From x len t <$> rewE rews e

    -- These are not recursive.
    Let d      -> Let <$> rewD rews d
--- a/src/Cryptol/Transform/Specialize.hs
+++ b/src/Cryptol/Transform/Specialize.hs
@ -78,7 +78,7 @@ specializeExpr expr =
    ERec fs       -> ERec <$> traverse (traverseSnd specializeExpr) fs
    ESel e s      -> ESel <$> specializeExpr e <*> pure s
    EIf e1 e2 e3  -> EIf <$> specializeExpr e1 <*> specializeExpr e2 <*> specializeExpr e3
-    EComp t e mss -> EComp t <$> specializeExpr e <*> traverse (traverse specializeMatch) mss
+    EComp len t e mss -> EComp len t <$> specializeExpr e <*> traverse (traverse specializeMatch) mss
    -- Bindings within list comprehensions always have monomorphic types.
    EVar {}       -> specializeConst expr
    ETAbs t e     -> do
@ -104,7 +104,7 @@ specializeExpr expr =
    EWhere e dgs  -> specializeEWhere e dgs

 specializeMatch :: Match -> SpecM Match
-specializeMatch (From qn t e) = From qn t <$> specializeExpr e
+specializeMatch (From qn l t e) = From qn l t <$> specializeExpr e
 specializeMatch (Let decl)
  | null (sVars (dSignature decl)) = return (Let decl)
  | otherwise = fail "unimplemented: specializeMatch Let unimplemented"
--- a/src/Cryptol/TypeCheck/AST.hs
+++ b/src/Cryptol/TypeCheck/AST.hs
@ -216,9 +216,10 @@ data Expr   = EList [Expr] Type         -- ^ List value (with type of elements)
            | ESel Expr Selector        -- ^ Elimination for tuple/record/list

            | EIf Expr Expr Expr        -- ^ If-then-else
-            | EComp Type Expr [[Match]] -- ^ List comprehensions
-                                        --   The type caches the type of the
-                                        --   expr.
+            | EComp Type Type Expr [[Match]]
+                                        -- ^ List comprehensions
+                                        --   The types caches the length of the
+                                        --   sequence and type of the expr.

            | EVar Name                 -- ^ Use of a bound variable

@ -270,8 +271,9 @@ data Expr   = EList [Expr] Type         -- ^ List value (with type of elements)
 instance NFData Expr where rnf = genericRnf


-data Match  = From Name Type Expr -- ^ do we need this type?  it seems like it
-                                  --   can be computed from the expr
+data Match  = From Name Type Type Expr
+                                  -- ^ Type arguments are the length and element
+                                  --   type of the sequence expression
            | Let Decl
              deriving (Show, Generic)

@ -826,8 +828,8 @@ instance PP (WithNames Expr) where
                          , text "then" <+> ppW e2
                          , text "else" <+> ppW e3 ]

-      EComp _ e mss -> let arm ms = text "|" <+> commaSep (map ppW ms)
-                       in brackets $ ppW e <+> vcat (map arm mss)
+      EComp _ _ e mss -> let arm ms = text "|" <+> commaSep (map ppW ms)
+                          in brackets $ ppW e <+> vcat (map arm mss)

      EVar x        -> ppPrefixName x

@ -916,7 +918,7 @@ instance PP Expr where
 instance PP (WithNames Match) where
  ppPrec _ (WithNames mat nm) =
    case mat of
-      From x _ e -> pp x <+> text "<-" <+> ppWithNames nm e
+      From x _ _ e -> pp x <+> text "<-" <+> ppWithNames nm e
      Let d      -> text "let" <+> ppWithNames nm d

 instance PP Match where
--- a/src/Cryptol/TypeCheck/Infer.hs
+++ b/src/Cryptol/TypeCheck/Infer.hs
@ -272,7 +272,7 @@ checkE expr tGoal =

         ds     <- combineMaps dss
         e'     <- withMonoTypes ds (checkE e a)
-         return (EComp tGoal e' mss')
+         return (EComp len a e' mss')

    P.EAppT e fs ->
      do ts <- mapM inferTyParam fs
@ -520,7 +520,7 @@ inferMatch (P.Match p e) =
  do (x,t) <- inferP (text "XXX:MATCH") p
     n     <- newType (text "sequence length of comprehension match") KNum
     e'    <- checkE e (tSeq n (thing t))
-     return (From x (thing t) e', x, t, n)
+     return (From x n (thing t) e', x, t, n)

 inferMatch (P.MatchLet b)
  | P.bMono b =
--- a/src/Cryptol/TypeCheck/Sanity.hs
+++ b/src/Cryptol/TypeCheck/Sanity.hs
@ -229,8 +229,9 @@ exprSchema expr =

         return $ tMono t1

-    EComp t e mss ->
-      do checkTypeIs KType t
+    EComp len t e mss ->
+      do checkTypeIs KNum len
+         checkTypeIs KType t

         (xs,ls) <- unzip `fmap` mapM checkArm mss
         -- XXX: check no duplicates
@ -238,7 +239,7 @@ exprSchema expr =

         case ls of
           [] -> return ()
-           _  -> convertible t (tSeq (foldr1 tMin ls) elT)
+           _  -> convertible (tSeq len t) (tSeq (foldr1 tMin ls) elT)

         return (tMono t)

@ -390,8 +391,10 @@ checkDeclGroup dg =
 checkMatch :: Match -> TcM ((Name, Schema), Type)
 checkMatch ma =
  case ma of
-    From x t e ->
-      do checkTypeIs KType t
+    From x len elt e ->
+      do checkTypeIs KNum len
+         checkTypeIs KType elt
+         let t = tSeq len elt
         t1 <- exprType e
         case tNoUser t1 of
           TCon (TC TCSeq) [ l, el ]
--- a/src/Cryptol/TypeCheck/Subst.hs
+++ b/src/Cryptol/TypeCheck/Subst.hs
@ -248,13 +248,13 @@ instance TVars Expr where
        ERec fs       -> ERec [ (f, go e) | (f,e) <- fs ]
        EList es t    -> EList (map go es) (apSubst su t)
        ESel e s      -> ESel (go e) s
-        EComp t e mss -> EComp (apSubst su t) (go e) (apSubst su mss)
+        EComp len t e mss -> EComp (apSubst su len) (apSubst su t) (go e) (apSubst su mss)
        EIf e1 e2 e3  -> EIf (go e1) (go e2) (go e3)

        EWhere e ds   -> EWhere (go e) (apSubst su ds)

 instance TVars Match where
-  apSubst su (From x t e) = From x (apSubst su t) (apSubst su e)
+  apSubst su (From x len t e) = From x (apSubst su t) (apSubst su len) (apSubst su e)
  apSubst su (Let b)      = Let (apSubst su b)

 instance TVars DeclGroup where
--- a/src/Cryptol/TypeCheck/TypeOf.hs
+++ b/src/Cryptol/TypeCheck/TypeOf.hs
@ -34,7 +34,7 @@ fastTypeOf tyenv expr =
    ERec fields   -> tRec [ (name, fastTypeOf tyenv e) | (name, e) <- fields ]
    ESel e sel    -> typeSelect (fastTypeOf tyenv e) sel
    EIf _ e _     -> fastTypeOf tyenv e
-    EComp t _ _   -> t
+    EComp len t _ _ -> tSeq len t
    EAbs x t e    -> tFun t (fastTypeOf (Map.insert x (Forall [] [] t) tyenv) e)
    EApp e _      -> case tIsFun (fastTypeOf tyenv e) of
                        Just (_, t) -> t