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

    {-# LANGUAGE DoAndIfThenElse #-}
    {-# LANGUAGE LambdaCase #-}
    {-# LANGUAGE MultiParamTypeClasses #-}
    {-# LANGUAGE ParallelListComp #-}
    {-# LANGUAGE ScopedTypeVariables #-}
    {-# LANGUAGE Safe #-}
    {-# LANGUAGE PatternGuards #-}

    module Cryptol.Eval (
        moduleEnv
      , runEval
      , EvalOpts(..)
      , PPOpts(..)
      , defaultPPOpts
      , Eval
      , EvalEnv
      , emptyEnv
      , evalExpr
      , evalDecls
      , evalSel
      , evalSetSel
      , EvalError(..)
      , forceValue
      ) where

    import Cryptol.Eval.Env
    import Cryptol.Eval.Monad
    import Cryptol.Eval.Type
    import Cryptol.Eval.Value
    import Cryptol.Parser.Selector(ppSelector)
    import Cryptol.ModuleSystem.Name
    import Cryptol.TypeCheck.AST
    import Cryptol.TypeCheck.Solver.InfNat(Nat'(..))
    import Cryptol.Utils.Panic (panic)
    import Cryptol.Utils.PP

    import           Control.Monad
    import qualified Data.Sequence as Seq
    import           Data.List
    import           Data.Maybe
    import qualified Data.Map.Strict as Map
    import           Data.Semigroup

    import Prelude ()
    import Prelude.Compat

    type EvalEnv = GenEvalEnv Bool BV Integer

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

    -- | Extend the given evaluation environment with all the declarations
    --   contained in the given module.
    moduleEnv :: EvalPrims b w i
              => Module           -- ^ Module containing declarations to evaluate
              -> GenEvalEnv b w i -- ^ Environment to extend
              -> Eval (GenEvalEnv b w i)
    moduleEnv :: Module -> GenEvalEnv b w i -> Eval (GenEvalEnv b w i)
    moduleEnv m :: Module
    m env :: GenEvalEnv b w i
    env = [DeclGroup] -> GenEvalEnv b w i -> Eval (GenEvalEnv b w i)
    forall b w i.
    EvalPrims b w i =>
    [DeclGroup] -> GenEvalEnv b w i -> Eval (GenEvalEnv b w i)
    evalDecls (Module -> [DeclGroup]
    mDecls Module
    m) (GenEvalEnv b w i -> Eval (GenEvalEnv b w i))
    -> Eval (GenEvalEnv b w i) -> Eval (GenEvalEnv b w i)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< Map Name Newtype -> GenEvalEnv b w i -> Eval (GenEvalEnv b w i)
    forall b w i.
    EvalPrims b w i =>
    Map Name Newtype -> GenEvalEnv b w i -> Eval (GenEvalEnv b w i)
    evalNewtypes (Module -> Map Name Newtype
    mNewtypes Module
    m) GenEvalEnv b w i
    env

    -- | Evaluate a Cryptol expression to a value.  This evaluator is parameterized
    --   by the `EvalPrims` class, which defines the behavior of bits and words, in
    --   addition to providing implementations for all the primitives.
    evalExpr :: EvalPrims b w i
             => GenEvalEnv b w i   -- ^ Evaluation environment
             -> Expr               -- ^ Expression to evaluate
             -> Eval (GenValue b w i)
    evalExpr :: GenEvalEnv b w i -> Expr -> Eval (GenValue b w i)
    evalExpr env :: GenEvalEnv b w i
    env expr :: Expr
    expr = case Expr
    expr of

      -- Try to detect when the user has directly written a finite sequence of
      -- literal bit values and pack these into a word.
      EList es :: [Expr]
    es ty :: Type
    ty
        -- NB, even if the list cannot be packed, we must use `VWord`
        -- when the element type is `Bit`.
        | TValue -> Bool
    isTBit TValue
    tyv -> {-# SCC "evalExpr->Elist/bit" #-}
            GenValue b w i -> Eval (GenValue b w i)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (GenValue b w i -> Eval (GenValue b w i))
    -> GenValue b w i -> Eval (GenValue b w i)
    forall a b. (a -> b) -> a -> b
    $ Integer -> Eval (WordValue b w i) -> GenValue b w i
    forall b w i. Integer -> Eval (WordValue b w i) -> GenValue b w i
    VWord Integer
    len (Eval (WordValue b w i) -> GenValue b w i)
    -> Eval (WordValue b w i) -> GenValue b w i
    forall a b. (a -> b) -> a -> b
    $
              case [Eval (GenValue b w i)] -> Maybe w
    forall b w i. BitWord b w i => [Eval (GenValue b w i)] -> Maybe w
    tryFromBits [Eval (GenValue b w i)]
    vs of
                Just w :: w
    w  -> WordValue b w i -> Eval (WordValue b w i)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (WordValue b w i -> Eval (WordValue b w i))
    -> WordValue b w i -> Eval (WordValue b w i)
    forall a b. (a -> b) -> a -> b
    $ w -> WordValue b w i
    forall b w i. w -> WordValue b w i
    WordVal w
    w
                Nothing -> do [Eval (GenValue b w i)]
    xs <- (Eval (GenValue b w i) -> Eval (Eval (GenValue b w i)))
    -> [Eval (GenValue b w i)] -> Eval [Eval (GenValue b w i)]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    mapM (Maybe String
    -> Eval (GenValue b w i) -> Eval (Eval (GenValue b w i))
    forall a. Maybe String -> Eval a -> Eval (Eval a)
    delay Maybe String
    forall a. Maybe a
    Nothing) [Eval (GenValue b w i)]
    vs
                              WordValue b w i -> Eval (WordValue b w i)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (WordValue b w i -> Eval (WordValue b w i))
    -> WordValue b w i -> Eval (WordValue b w i)
    forall a b. (a -> b) -> a -> b
    $ Seq (Eval b) -> WordValue b w i
    forall b w i. Seq (Eval b) -> WordValue b w i
    BitsVal (Seq (Eval b) -> WordValue b w i)
    -> Seq (Eval b) -> WordValue b w i
    forall a b. (a -> b) -> a -> b
    $ [Eval b] -> Seq (Eval b)
    forall a. [a] -> Seq a
    Seq.fromList ([Eval b] -> Seq (Eval b)) -> [Eval b] -> Seq (Eval b)
    forall a b. (a -> b) -> a -> b
    $ (Eval (GenValue b w i) -> Eval b)
    -> [Eval (GenValue b w i)] -> [Eval b]
    forall a b. (a -> b) -> [a] -> [b]
    map (GenValue b w i -> b
    forall b w i. GenValue b w i -> b
    fromVBit (GenValue b w i -> b) -> Eval (GenValue b w i) -> Eval b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$>) [Eval (GenValue b w i)]
    xs
        | Bool
    otherwise -> {-# SCC "evalExpr->EList" #-} do
            [Eval (GenValue b w i)]
    xs <- (Eval (GenValue b w i) -> Eval (Eval (GenValue b w i)))
    -> [Eval (GenValue b w i)] -> Eval [Eval (GenValue b w i)]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    mapM (Maybe String
    -> Eval (GenValue b w i) -> Eval (Eval (GenValue b w i))
    forall a. Maybe String -> Eval a -> Eval (Eval a)
    delay Maybe String
    forall a. Maybe a
    Nothing) [Eval (GenValue b w i)]
    vs
            GenValue b w i -> Eval (GenValue b w i)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (GenValue b w i -> Eval (GenValue b w i))
    -> GenValue b w i -> Eval (GenValue b w i)
    forall a b. (a -> b) -> a -> b
    $ Integer -> SeqMap b w i -> GenValue b w i
    forall b w i. Integer -> SeqMap b w i -> GenValue b w i
    VSeq Integer
    len (SeqMap b w i -> GenValue b w i) -> SeqMap b w i -> GenValue b w i
    forall a b. (a -> b) -> a -> b
    $ [Eval (GenValue b w i)] -> SeqMap b w i
    forall b w i. [Eval (GenValue b w i)] -> SeqMap b w i
    finiteSeqMap [Eval (GenValue b w i)]
    xs
       where
        tyv :: TValue
    tyv = HasCallStack => TypeEnv -> Type -> TValue
    TypeEnv -> Type -> TValue
    evalValType (GenEvalEnv b w i -> TypeEnv
    forall b w i. GenEvalEnv b w i -> TypeEnv
    envTypes GenEvalEnv b w i
    env) Type
    ty
        vs :: [Eval (GenValue b w i)]
    vs  = (Expr -> Eval (GenValue b w i))
    -> [Expr] -> [Eval (GenValue b w i)]
    forall a b. (a -> b) -> [a] -> [b]
    map (GenEvalEnv b w i -> Expr -> Eval (GenValue b w i)
    forall b w i.
    EvalPrims b w i =>
    GenEvalEnv b w i -> Expr -> Eval (GenValue b w i)
    evalExpr GenEvalEnv b w i
    env) [Expr]
    es
        len :: Integer
    len = [Expr] -> Integer
    forall i a. Num i => [a] -> i
    genericLength [Expr]
    es

      ETuple es :: [Expr]
    es -> {-# SCC "evalExpr->ETuple" #-} do
         [Eval (GenValue b w i)]
    xs <- (Expr -> Eval (Eval (GenValue b w i)))
    -> [Expr] -> Eval [Eval (GenValue b w i)]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    mapM (Maybe String
    -> Eval (GenValue b w i) -> Eval (Eval (GenValue b w i))
    forall a. Maybe String -> Eval a -> Eval (Eval a)
    delay Maybe String
    forall a. Maybe a
    Nothing (Eval (GenValue b w i) -> Eval (Eval (GenValue b w i)))
    -> (Expr -> Eval (GenValue b w i))
    -> Expr
    -> Eval (Eval (GenValue b w i))
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Expr -> Eval (GenValue b w i)
    eval) [Expr]
    es
         GenValue b w i -> Eval (GenValue b w i)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (GenValue b w i -> Eval (GenValue b w i))
    -> GenValue b w i -> Eval (GenValue b w i)
    forall a b. (a -> b) -> a -> b
    $ [Eval (GenValue b w i)] -> GenValue b w i
    forall b w i. [Eval (GenValue b w i)] -> GenValue b w i
    VTuple [Eval (GenValue b w i)]
    xs

      ERec fields :: [(Ident, Expr)]
    fields -> {-# SCC "evalExpr->ERec" #-} do
         [(Ident, Eval (GenValue b w i))]
    xs <- [Eval (Ident, Eval (GenValue b w i))]
    -> Eval [(Ident, Eval (GenValue b w i))]
    forall (t :: * -> *) (m :: * -> *) a.
    (Traversable t, Monad m) =>
    t (m a) -> m (t a)
    sequence [ do Eval (GenValue b w i)
    thk <- Maybe String
    -> Eval (GenValue b w i) -> Eval (Eval (GenValue b w i))
    forall a. Maybe String -> Eval a -> Eval (Eval a)
    delay Maybe String
    forall a. Maybe a
    Nothing (Expr -> Eval (GenValue b w i)
    eval Expr
    e)
                             (Ident, Eval (GenValue b w i))
    -> Eval (Ident, Eval (GenValue b w i))
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Ident
    f, Eval (GenValue b w i)
    thk)
                        | (f :: Ident
    f, e :: Expr
    e) <- [(Ident, Expr)]
    fields
                        ]
         GenValue b w i -> Eval (GenValue b w i)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (GenValue b w i -> Eval (GenValue b w i))
    -> GenValue b w i -> Eval (GenValue b w i)
    forall a b. (a -> b) -> a -> b
    $ [(Ident, Eval (GenValue b w i))] -> GenValue b w i
    forall b w i. [(Ident, Eval (GenValue b w i))] -> GenValue b w i
    VRecord [(Ident, Eval (GenValue b w i))]
    xs

      ESel e :: Expr
    e sel :: Selector
    sel -> {-# SCC "evalExpr->ESel" #-} do
         GenValue b w i
    x <- Expr -> Eval (GenValue b w i)
    eval Expr
    e
         GenValue b w i -> Selector -> Eval (GenValue b w i)
    forall b w i.
    EvalPrims b w i =>
    GenValue b w i -> Selector -> Eval (GenValue b w i)
    evalSel GenValue b w i
    x Selector
    sel

      ESet e :: Expr
    e sel :: Selector
    sel v :: Expr
    v -> {-# SCC "evalExpr->ESet" #-}
        do GenValue b w i
    x <- Expr -> Eval (GenValue b w i)
    eval Expr
    e
           GenValue b w i
    -> Selector -> Eval (GenValue b w i) -> Eval (GenValue b w i)
    forall b w i.
    EvalPrims b w i =>
    GenValue b w i
    -> Selector -> Eval (GenValue b w i) -> Eval (GenValue b w i)
    evalSetSel GenValue b w i
    x Selector
    sel (Expr -> Eval (GenValue b w i)
    eval Expr
    v)

      EIf c :: Expr
    c t :: Expr
    t f :: Expr
    f -> {-# SCC "evalExpr->EIf" #-} do
         b
    b <- GenValue b w i -> b
    forall b w i. GenValue b w i -> b
    fromVBit (GenValue b w i -> b) -> Eval (GenValue b w i) -> Eval b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Expr -> Eval (GenValue b w i)
    eval Expr
    c
         b
    -> Eval (GenValue b w i)
    -> Eval (GenValue b w i)
    -> Eval (GenValue b w i)
    forall b w i.
    EvalPrims b w i =>
    b
    -> Eval (GenValue b w i)
    -> Eval (GenValue b w i)
    -> Eval (GenValue b w i)
    iteValue b
    b (Expr -> Eval (GenValue b w i)
    eval Expr
    t) (Expr -> Eval (GenValue b w i)
    eval Expr
    f)

      EComp n :: Type
    n t :: Type
    t h :: Expr
    h gs :: [[Match]]
    gs -> {-# SCC "evalExpr->EComp" #-} do
          let len :: Nat'
    len  = HasCallStack => TypeEnv -> Type -> Nat'
    TypeEnv -> Type -> Nat'
    evalNumType (GenEvalEnv b w i -> TypeEnv
    forall b w i. GenEvalEnv b w i -> TypeEnv
    envTypes GenEvalEnv b w i
    env) Type
    n
          let elty :: TValue
    elty = HasCallStack => TypeEnv -> Type -> TValue
    TypeEnv -> Type -> TValue
    evalValType (GenEvalEnv b w i -> TypeEnv
    forall b w i. GenEvalEnv b w i -> TypeEnv
    envTypes GenEvalEnv b w i
    env) Type
    t
          GenEvalEnv b w i
    -> Nat' -> TValue -> Expr -> [[Match]] -> Eval (GenValue b w i)
    forall b w i.
    EvalPrims b w i =>
    GenEvalEnv b w i
    -> Nat' -> TValue -> Expr -> [[Match]] -> Eval (GenValue b w i)
    evalComp GenEvalEnv b w i
    env Nat'
    len TValue
    elty Expr
    h [[Match]]
    gs

      EVar n :: Name
    n -> {-# SCC "evalExpr->EVar" #-} do
        case Name -> GenEvalEnv b w i -> Maybe (Eval (GenValue b w i))
    forall b w i.
    Name -> GenEvalEnv b w i -> Maybe (Eval (GenValue b w i))
    lookupVar Name
    n GenEvalEnv b w i
    env of
          Just val :: Eval (GenValue b w i)
    val -> Eval (GenValue b w i)
    val
          Nothing  -> do
            Doc
    envdoc <- PPOpts -> GenEvalEnv b w i -> Eval Doc
    forall b w i.
    BitWord b w i =>
    PPOpts -> GenEvalEnv b w i -> Eval Doc
    ppEnv PPOpts
    defaultPPOpts GenEvalEnv b w i
    env
            String -> [String] -> Eval (GenValue b w i)
    forall a. HasCallStack => String -> [String] -> a
    panic "[Eval] evalExpr"
                         ["var `" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Doc -> String
    forall a. Show a => a -> String
    show (Name -> Doc
    forall a. PP a => a -> Doc
    pp Name
    n) String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ "` is not defined"
                         , Doc -> String
    forall a. Show a => a -> String
    show Doc
    envdoc
                         ]

      ETAbs tv :: TParam
    tv b :: Expr
    b -> {-# SCC "evalExpr->ETAbs" #-}
        case TParam -> Kind
    tpKind TParam
    tv of
          KType -> GenValue b w i -> Eval (GenValue b w i)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (GenValue b w i -> Eval (GenValue b w i))
    -> GenValue b w i -> Eval (GenValue b w i)
    forall a b. (a -> b) -> a -> b
    $ (TValue -> Eval (GenValue b w i)) -> GenValue b w i
    forall b w i. (TValue -> Eval (GenValue b w i)) -> GenValue b w i
    VPoly    ((TValue -> Eval (GenValue b w i)) -> GenValue b w i)
    -> (TValue -> Eval (GenValue b w i)) -> GenValue b w i
    forall a b. (a -> b) -> a -> b
    $ \ty :: TValue
    ty -> GenEvalEnv b w i -> Expr -> Eval (GenValue b w i)
    forall b w i.
    EvalPrims b w i =>
    GenEvalEnv b w i -> Expr -> Eval (GenValue b w i)
    evalExpr (TVar -> Either Nat' TValue -> GenEvalEnv b w i -> GenEvalEnv b w i
    forall b w i.
    TVar -> Either Nat' TValue -> GenEvalEnv b w i -> GenEvalEnv b w i
    bindType (TParam -> TVar
    tpVar TParam
    tv) (TValue -> Either Nat' TValue
    forall a b. b -> Either a b
    Right TValue
    ty) GenEvalEnv b w i
    env) Expr
    b
          KNum  -> GenValue b w i -> Eval (GenValue b w i)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (GenValue b w i -> Eval (GenValue b w i))
    -> GenValue b w i -> Eval (GenValue b w i)
    forall a b. (a -> b) -> a -> b
    $ (Nat' -> Eval (GenValue b w i)) -> GenValue b w i
    forall b w i. (Nat' -> Eval (GenValue b w i)) -> GenValue b w i
    VNumPoly ((Nat' -> Eval (GenValue b w i)) -> GenValue b w i)
    -> (Nat' -> Eval (GenValue b w i)) -> GenValue b w i
    forall a b. (a -> b) -> a -> b
    $ \n :: Nat'
    n  -> GenEvalEnv b w i -> Expr -> Eval (GenValue b w i)
    forall b w i.
    EvalPrims b w i =>
    GenEvalEnv b w i -> Expr -> Eval (GenValue b w i)
    evalExpr (TVar -> Either Nat' TValue -> GenEvalEnv b w i -> GenEvalEnv b w i
    forall b w i.
    TVar -> Either Nat' TValue -> GenEvalEnv b w i -> GenEvalEnv b w i
    bindType (TParam -> TVar
    tpVar TParam
    tv) (Nat' -> Either Nat' TValue
    forall a b. a -> Either a b
    Left Nat'
    n) GenEvalEnv b w i
    env) Expr
    b
          k :: Kind
    k     -> String -> [String] -> Eval (GenValue b w i)
    forall a. HasCallStack => String -> [String] -> a
    panic "[Eval] evalExpr" ["invalid kind on type abstraction", Kind -> String
    forall a. Show a => a -> String
    show Kind
    k]

      ETApp e :: Expr
    e ty :: Type
    ty -> {-# SCC "evalExpr->ETApp" #-} do
        Expr -> Eval (GenValue b w i)
    eval Expr
    e Eval (GenValue b w i)
    -> (GenValue b w i -> Eval (GenValue b w i))
    -> Eval (GenValue b w i)
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \case
          VPoly f :: TValue -> Eval (GenValue b w i)
    f     -> TValue -> Eval (GenValue b w i)
    f (TValue -> Eval (GenValue b w i))
    -> TValue -> Eval (GenValue b w i)
    forall a b. (a -> b) -> a -> b
    $! (HasCallStack => TypeEnv -> Type -> TValue
    TypeEnv -> Type -> TValue
    evalValType (GenEvalEnv b w i -> TypeEnv
    forall b w i. GenEvalEnv b w i -> TypeEnv
    envTypes GenEvalEnv b w i
    env) Type
    ty)
          VNumPoly f :: Nat' -> Eval (GenValue b w i)
    f  -> Nat' -> Eval (GenValue b w i)
    f (Nat' -> Eval (GenValue b w i)) -> Nat' -> Eval (GenValue b w i)
    forall a b. (a -> b) -> a -> b
    $! (HasCallStack => TypeEnv -> Type -> Nat'
    TypeEnv -> Type -> Nat'
    evalNumType (GenEvalEnv b w i -> TypeEnv
    forall b w i. GenEvalEnv b w i -> TypeEnv
    envTypes GenEvalEnv b w i
    env) Type
    ty)
          val :: GenValue b w i
    val     -> do Doc
    vdoc <- GenValue b w i -> Eval Doc
    ppV GenValue b w i
    val
                        String -> [String] -> Eval (GenValue b w i)
    forall a. HasCallStack => String -> [String] -> a
    panic "[Eval] evalExpr"
                          ["expected a polymorphic value"
                          , Doc -> String
    forall a. Show a => a -> String
    show Doc
    vdoc, Doc -> String
    forall a. Show a => a -> String
    show (Expr -> Doc
    forall a. PP a => a -> Doc
    pp Expr
    e), Doc -> String
    forall a. Show a => a -> String
    show (Type -> Doc
    forall a. PP a => a -> Doc
    pp Type
    ty)
                          ]

      EApp f :: Expr
    f x :: Expr
    x -> {-# SCC "evalExpr->EApp" #-} do
        Expr -> Eval (GenValue b w i)
    eval Expr
    f Eval (GenValue b w i)
    -> (GenValue b w i -> Eval (GenValue b w i))
    -> Eval (GenValue b w i)
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \case
          VFun f' :: Eval (GenValue b w i) -> Eval (GenValue b w i)
    f' -> Eval (GenValue b w i) -> Eval (GenValue b w i)
    f' (Expr -> Eval (GenValue b w i)
    eval Expr
    x)
          it :: GenValue b w i
    it      -> do Doc
    itdoc <- GenValue b w i -> Eval Doc
    ppV GenValue b w i
    it
                        String -> [String] -> Eval (GenValue b w i)
    forall a. HasCallStack => String -> [String] -> a
    panic "[Eval] evalExpr" ["not a function", Doc -> String
    forall a. Show a => a -> String
    show Doc
    itdoc ]

      EAbs n :: Name
    n _ty :: Type
    _ty b :: Expr
    b -> {-# SCC "evalExpr->EAbs" #-}
        GenValue b w i -> Eval (GenValue b w i)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (GenValue b w i -> Eval (GenValue b w i))
    -> GenValue b w i -> Eval (GenValue b w i)
    forall a b. (a -> b) -> a -> b
    $ (Eval (GenValue b w i) -> Eval (GenValue b w i)) -> GenValue b w i
    forall b w i.
    (Eval (GenValue b w i) -> Eval (GenValue b w i)) -> GenValue b w i
    VFun (\v :: Eval (GenValue b w i)
    v -> do GenEvalEnv b w i
    env' <- Name
    -> Eval (GenValue b w i)
    -> GenEvalEnv b w i
    -> Eval (GenEvalEnv b w i)
    forall b w i.
    Name
    -> Eval (GenValue b w i)
    -> GenEvalEnv b w i
    -> Eval (GenEvalEnv b w i)
    bindVar Name
    n Eval (GenValue b w i)
    v GenEvalEnv b w i
    env
                                GenEvalEnv b w i -> Expr -> Eval (GenValue b w i)
    forall b w i.
    EvalPrims b w i =>
    GenEvalEnv b w i -> Expr -> Eval (GenValue b w i)
    evalExpr GenEvalEnv b w i
    env' Expr
    b)

      -- XXX these will likely change once there is an evidence value
      EProofAbs _ e :: Expr
    e -> GenEvalEnv b w i -> Expr -> Eval (GenValue b w i)
    forall b w i.
    EvalPrims b w i =>
    GenEvalEnv b w i -> Expr -> Eval (GenValue b w i)
    evalExpr GenEvalEnv b w i
    env Expr
    e
      EProofApp e :: Expr
    e   -> GenEvalEnv b w i -> Expr -> Eval (GenValue b w i)
    forall b w i.
    EvalPrims b w i =>
    GenEvalEnv b w i -> Expr -> Eval (GenValue b w i)
    evalExpr GenEvalEnv b w i
    env Expr
    e

      EWhere e :: Expr
    e ds :: [DeclGroup]
    ds -> {-# SCC "evalExpr->EWhere" #-} do
         GenEvalEnv b w i
    env' <- [DeclGroup] -> GenEvalEnv b w i -> Eval (GenEvalEnv b w i)
    forall b w i.
    EvalPrims b w i =>
    [DeclGroup] -> GenEvalEnv b w i -> Eval (GenEvalEnv b w i)
    evalDecls [DeclGroup]
    ds GenEvalEnv b w i
    env
         GenEvalEnv b w i -> Expr -> Eval (GenValue b w i)
    forall b w i.
    EvalPrims b w i =>
    GenEvalEnv b w i -> Expr -> Eval (GenValue b w i)
    evalExpr GenEvalEnv b w i
    env' Expr
    e

      where

      {-# INLINE eval #-}
      eval :: Expr -> Eval (GenValue b w i)
    eval = GenEvalEnv b w i -> Expr -> Eval (GenValue b w i)
    forall b w i.
    EvalPrims b w i =>
    GenEvalEnv b w i -> Expr -> Eval (GenValue b w i)
    evalExpr GenEvalEnv b w i
    env
      ppV :: GenValue b w i -> Eval Doc
    ppV = PPOpts -> GenValue b w i -> Eval Doc
    forall b w i. BitWord b w i => PPOpts -> GenValue b w i -> Eval Doc
    ppValue PPOpts
    defaultPPOpts

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

    evalNewtypes :: EvalPrims b w i
                 => Map.Map Name Newtype
                 -> GenEvalEnv b w i
                 -> Eval (GenEvalEnv b w i)
    evalNewtypes :: Map Name Newtype -> GenEvalEnv b w i -> Eval (GenEvalEnv b w i)
    evalNewtypes nts :: Map Name Newtype
    nts env :: GenEvalEnv b w i
    env = (GenEvalEnv b w i -> Newtype -> Eval (GenEvalEnv b w i))
    -> GenEvalEnv b w i -> [Newtype] -> Eval (GenEvalEnv b w i)
    forall (t :: * -> *) (m :: * -> *) b a.
    (Foldable t, Monad m) =>
    (b -> a -> m b) -> b -> t a -> m b
    foldM ((Newtype -> GenEvalEnv b w i -> Eval (GenEvalEnv b w i))
    -> GenEvalEnv b w i -> Newtype -> Eval (GenEvalEnv b w i)
    forall a b c. (a -> b -> c) -> b -> a -> c
    flip Newtype -> GenEvalEnv b w i -> Eval (GenEvalEnv b w i)
    forall b w i.
    EvalPrims b w i =>
    Newtype -> GenEvalEnv b w i -> Eval (GenEvalEnv b w i)
    evalNewtype) GenEvalEnv b w i
    env ([Newtype] -> Eval (GenEvalEnv b w i))
    -> [Newtype] -> Eval (GenEvalEnv b w i)
    forall a b. (a -> b) -> a -> b
    $ Map Name Newtype -> [Newtype]
    forall k a. Map k a -> [a]
    Map.elems Map Name Newtype
    nts

    -- | Introduce the constructor function for a newtype.
    evalNewtype :: EvalPrims b w i
                => Newtype
                -> GenEvalEnv b w i
                -> Eval (GenEvalEnv b w i)
    evalNewtype :: Newtype -> GenEvalEnv b w i -> Eval (GenEvalEnv b w i)
    evalNewtype nt :: Newtype
    nt = Name
    -> Eval (GenValue b w i)
    -> GenEvalEnv b w i
    -> Eval (GenEvalEnv b w i)
    forall b w i.
    Name
    -> Eval (GenValue b w i)
    -> GenEvalEnv b w i
    -> Eval (GenEvalEnv b w i)
    bindVar (Newtype -> Name
    ntName Newtype
    nt) (GenValue b w i -> Eval (GenValue b w i)
    forall (m :: * -> *) a. Monad m => a -> m a
    return ((TParam -> GenValue b w i -> GenValue b w i)
    -> GenValue b w i -> [TParam] -> GenValue b w i
    forall (t :: * -> *) a b.
    Foldable t =>
    (a -> b -> b) -> b -> t a -> b
    foldr TParam -> GenValue b w i -> GenValue b w i
    forall p b w i. p -> GenValue b w i -> GenValue b w i
    tabs GenValue b w i
    forall b w i. GenValue b w i
    con (Newtype -> [TParam]
    ntParams Newtype
    nt)))
      where
      tabs :: p -> GenValue b w i -> GenValue b w i
    tabs _tp :: p
    _tp body :: GenValue b w i
    body = (TValue -> GenValue b w i) -> GenValue b w i
    forall b w i. (TValue -> GenValue b w i) -> GenValue b w i
    tlam (\ _ -> GenValue b w i
    body)
      con :: GenValue b w i
    con           = (Eval (GenValue b w i) -> Eval (GenValue b w i)) -> GenValue b w i
    forall b w i.
    (Eval (GenValue b w i) -> Eval (GenValue b w i)) -> GenValue b w i
    VFun Eval (GenValue b w i) -> Eval (GenValue b w i)
    forall a. a -> a
    id

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

    -- | Extend the given evaluation environment with the result of evaluating the
    --   given collection of declaration groups.
    evalDecls :: EvalPrims b w i
              => [DeclGroup]         -- ^ Declaration groups to evaluate
              -> GenEvalEnv b w i    -- ^ Environment to extend
              -> Eval (GenEvalEnv b w i)
    evalDecls :: [DeclGroup] -> GenEvalEnv b w i -> Eval (GenEvalEnv b w i)
    evalDecls dgs :: [DeclGroup]
    dgs env :: GenEvalEnv b w i
    env = (GenEvalEnv b w i -> DeclGroup -> Eval (GenEvalEnv b w i))
    -> GenEvalEnv b w i -> [DeclGroup] -> Eval (GenEvalEnv b w i)
    forall (t :: * -> *) (m :: * -> *) b a.
    (Foldable t, Monad m) =>
    (b -> a -> m b) -> b -> t a -> m b
    foldM GenEvalEnv b w i -> DeclGroup -> Eval (GenEvalEnv b w i)
    forall b w i.
    EvalPrims b w i =>
    GenEvalEnv b w i -> DeclGroup -> Eval (GenEvalEnv b w i)
    evalDeclGroup GenEvalEnv b w i
    env [DeclGroup]
    dgs

    evalDeclGroup :: EvalPrims b w i
                  => GenEvalEnv b w i
                  -> DeclGroup
                  -> Eval (GenEvalEnv b w i)
    evalDeclGroup :: GenEvalEnv b w i -> DeclGroup -> Eval (GenEvalEnv b w i)
    evalDeclGroup env :: GenEvalEnv b w i
    env dg :: DeclGroup
    dg = do
      case DeclGroup
    dg of
        Recursive ds :: [Decl]
    ds -> do
          -- declare a "hole" for each declaration
          -- and extend the evaluation environment
          [(Name, Schema, Eval (GenValue b w i),
      Eval (GenValue b w i) -> Eval ())]
    holes <- (Decl
     -> Eval
          (Name, Schema, Eval (GenValue b w i),
           Eval (GenValue b w i) -> Eval ()))
    -> [Decl]
    -> Eval
         [(Name, Schema, Eval (GenValue b w i),
           Eval (GenValue b w i) -> Eval ())]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    mapM Decl
    -> Eval
         (Name, Schema, Eval (GenValue b w i),
          Eval (GenValue b w i) -> Eval ())
    forall b w i.
    Decl
    -> Eval
         (Name, Schema, Eval (GenValue b w i),
          Eval (GenValue b w i) -> Eval ())
    declHole [Decl]
    ds
          let holeEnv :: Map Name (Eval (GenValue b w i))
    holeEnv = [(Name, Eval (GenValue b w i))] -> Map Name (Eval (GenValue b w i))
    forall k a. Ord k => [(k, a)] -> Map k a
    Map.fromList ([(Name, Eval (GenValue b w i))]
     -> Map Name (Eval (GenValue b w i)))
    -> [(Name, Eval (GenValue b w i))]
    -> Map Name (Eval (GenValue b w i))
    forall a b. (a -> b) -> a -> b
    $ [ (Name
    nm,Eval (GenValue b w i)
    h) | (nm :: Name
    nm,_,h :: Eval (GenValue b w i)
    h,_) <- [(Name, Schema, Eval (GenValue b w i),
      Eval (GenValue b w i) -> Eval ())]
    holes ]
          let env' :: GenEvalEnv b w i
    env' = GenEvalEnv b w i
    env GenEvalEnv b w i -> GenEvalEnv b w i -> GenEvalEnv b w i
    forall a. Monoid a => a -> a -> a
    `mappend` GenEvalEnv Any Any Any
    forall b w i. GenEvalEnv b w i
    emptyEnv{ envVars :: Map Name (Eval (GenValue b w i))
    envVars = Map Name (Eval (GenValue b w i))
    holeEnv }

          -- evaluate the declaration bodies, building a new evaluation environment
          GenEvalEnv b w i
    env'' <- (GenEvalEnv b w i -> Decl -> Eval (GenEvalEnv b w i))
    -> GenEvalEnv b w i -> [Decl] -> Eval (GenEvalEnv b w i)
    forall (t :: * -> *) (m :: * -> *) b a.
    (Foldable t, Monad m) =>
    (b -> a -> m b) -> b -> t a -> m b
    foldM (GenEvalEnv b w i
    -> GenEvalEnv b w i -> Decl -> Eval (GenEvalEnv b w i)
    forall b w i.
    EvalPrims b w i =>
    GenEvalEnv b w i
    -> GenEvalEnv b w i -> Decl -> Eval (GenEvalEnv b w i)
    evalDecl GenEvalEnv b w i
    env') GenEvalEnv b w i
    env [Decl]
    ds

          -- now backfill the holes we declared earlier using the definitions
          -- calculated in the previous step
          ((Name, Schema, Eval (GenValue b w i),
      Eval (GenValue b w i) -> Eval ())
     -> Eval ())
    -> [(Name, Schema, Eval (GenValue b w i),
         Eval (GenValue b w i) -> Eval ())]
    -> Eval ()
    forall (t :: * -> *) (m :: * -> *) a b.
    (Foldable t, Monad m) =>
    (a -> m b) -> t a -> m ()
    mapM_ (GenEvalEnv b w i
    -> (Name, Schema, Eval (GenValue b w i),
        Eval (GenValue b w i) -> Eval ())
    -> Eval ()
    forall b w i.
    BitWord b w i =>
    GenEvalEnv b w i
    -> (Name, Schema, Eval (GenValue b w i),
        Eval (GenValue b w i) -> Eval ())
    -> Eval ()
    fillHole GenEvalEnv b w i
    env'') [(Name, Schema, Eval (GenValue b w i),
      Eval (GenValue b w i) -> Eval ())]
    holes

          -- return the map containing the holes
          GenEvalEnv b w i -> Eval (GenEvalEnv b w i)
    forall (m :: * -> *) a. Monad m => a -> m a
    return GenEvalEnv b w i
    env'

        NonRecursive d :: Decl
    d -> do
          GenEvalEnv b w i
    -> GenEvalEnv b w i -> Decl -> Eval (GenEvalEnv b w i)
    forall b w i.
    EvalPrims b w i =>
    GenEvalEnv b w i
    -> GenEvalEnv b w i -> Decl -> Eval (GenEvalEnv b w i)
    evalDecl GenEvalEnv b w i
    env GenEvalEnv b w i
    env Decl
    d

    -- | This operation is used to complete the process of setting up recursive declaration
    --   groups.  It 'backfills' previously-allocated thunk values with the actual evaluation
    --   procedure for the body of recursive definitions.
    --
    --   In order to faithfully evaluate the nonstrict semantics of Cryptol, we have to take some
    --   care in this process.  In particular, we need to ensure that every recursive definition
    --   binding is indistinguishable from its eta-expanded form.  The straightforward solution
    --   to this is to force an eta-expansion procedure on all recursive definitions.
    --   However, for the so-called 'Value' types we can instead optimistically use the 'delayFill'
    --   operation and only fall back on full eta expansion if the thunk is double-forced.
    fillHole :: BitWord b w i
             => GenEvalEnv b w i
             -> (Name, Schema, Eval (GenValue b w i), Eval (GenValue b w i) -> Eval ())
             -> Eval ()
    fillHole :: GenEvalEnv b w i
    -> (Name, Schema, Eval (GenValue b w i),
        Eval (GenValue b w i) -> Eval ())
    -> Eval ()
    fillHole env :: GenEvalEnv b w i
    env (nm :: Name
    nm, sch :: Schema
    sch, _, fill :: Eval (GenValue b w i) -> Eval ()
    fill) = do
      case Name -> GenEvalEnv b w i -> Maybe (Eval (GenValue b w i))
    forall b w i.
    Name -> GenEvalEnv b w i -> Maybe (Eval (GenValue b w i))
    lookupVar Name
    nm GenEvalEnv b w i
    env of
        Nothing -> String -> [String] -> Eval ()
    forall a. HasCallStack => String -> [String] -> a
    evalPanic "fillHole" ["Recursive definition not completed", Doc -> String
    forall a. Show a => a -> String
    show (Name -> Doc
    ppLocName Name
    nm)]
        Just x :: Eval (GenValue b w i)
    x
         | GenEvalEnv b w i -> Schema -> Bool
    forall b w i. GenEvalEnv b w i -> Schema -> Bool
    isValueType GenEvalEnv b w i
    env Schema
    sch -> Eval (GenValue b w i) -> Eval ()
    fill (Eval (GenValue b w i) -> Eval ())
    -> Eval (Eval (GenValue b w i)) -> Eval ()
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< Eval (GenValue b w i)
    -> Eval (GenValue b w i) -> Eval (Eval (GenValue b w i))
    forall a. Eval a -> Eval a -> Eval (Eval a)
    delayFill Eval (GenValue b w i)
    x (String
    -> GenEvalEnv b w i
    -> Schema
    -> Eval (GenValue b w i)
    -> Eval (GenValue b w i)
    forall b w i.
    BitWord b w i =>
    String
    -> GenEvalEnv b w i
    -> Schema
    -> Eval (GenValue b w i)
    -> Eval (GenValue b w i)
    etaDelay (Doc -> String
    forall a. Show a => a -> String
    show (Name -> Doc
    ppLocName Name
    nm)) GenEvalEnv b w i
    env Schema
    sch Eval (GenValue b w i)
    x)
         | Bool
    otherwise           -> Eval (GenValue b w i) -> Eval ()
    fill (String
    -> GenEvalEnv b w i
    -> Schema
    -> Eval (GenValue b w i)
    -> Eval (GenValue b w i)
    forall b w i.
    BitWord b w i =>
    String
    -> GenEvalEnv b w i
    -> Schema
    -> Eval (GenValue b w i)
    -> Eval (GenValue b w i)
    etaDelay (Doc -> String
    forall a. Show a => a -> String
    show (Name -> Doc
    ppLocName Name
    nm)) GenEvalEnv b w i
    env Schema
    sch Eval (GenValue b w i)
    x)

    -- | 'Value' types are non-polymorphic types recursive constructed from
    --   bits, finite sequences, tuples and records.  Types of this form can
    --   be implemented rather more efficently than general types because we can
    --   rely on the 'delayFill' operation to build a thunk that falls back on performing
    --   eta-expansion rather than doing it eagerly.
    isValueType :: GenEvalEnv b w i -> Schema -> Bool
    isValueType :: GenEvalEnv b w i -> Schema -> Bool
    isValueType env :: GenEvalEnv b w i
    env Forall{ sVars :: Schema -> [TParam]
    sVars = [], sProps :: Schema -> [Type]
    sProps = [], sType :: Schema -> Type
    sType = Type
    t0 }
       = TValue -> Bool
    go (HasCallStack => TypeEnv -> Type -> TValue
    TypeEnv -> Type -> TValue
    evalValType (GenEvalEnv b w i -> TypeEnv
    forall b w i. GenEvalEnv b w i -> TypeEnv
    envTypes GenEvalEnv b w i
    env) Type
    t0)
     where
      go :: TValue -> Bool
    go TVBit = Bool
    True
      go (TVSeq _ x :: TValue
    x)  = TValue -> Bool
    go TValue
    x
      go (TVTuple xs :: [TValue]
    xs) = [Bool] -> Bool
    forall (t :: * -> *). Foldable t => t Bool -> Bool
    and ((TValue -> Bool) -> [TValue] -> [Bool]
    forall a b. (a -> b) -> [a] -> [b]
    map TValue -> Bool
    go [TValue]
    xs)
      go (TVRec xs :: [(Ident, TValue)]
    xs)   = [Bool] -> Bool
    forall (t :: * -> *). Foldable t => t Bool -> Bool
    and (((Ident, TValue) -> Bool) -> [(Ident, TValue)] -> [Bool]
    forall a b. (a -> b) -> [a] -> [b]
    map (TValue -> Bool
    go (TValue -> Bool)
    -> ((Ident, TValue) -> TValue) -> (Ident, TValue) -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Ident, TValue) -> TValue
    forall a b. (a, b) -> b
    snd) [(Ident, TValue)]
    xs)
      go _            = Bool
    False

    isValueType _ _ = Bool
    False

    -- | Eta-expand a word value.  This forces an unpacked word representation.
    etaWord  :: BitWord b w i
             => Integer
             -> Eval (GenValue b w i)
             -> Eval (WordValue b w i)
    etaWord :: Integer -> Eval (GenValue b w i) -> Eval (WordValue b w i)
    etaWord n :: Integer
    n x :: Eval (GenValue b w i)
    x = do
      Eval (WordValue b w i)
    w <- Maybe String
    -> Eval (WordValue b w i) -> Eval (Eval (WordValue b w i))
    forall a. Maybe String -> Eval a -> Eval (Eval a)
    delay Maybe String
    forall a. Maybe a
    Nothing (String -> GenValue b w i -> Eval (WordValue b w i)
    forall b w i. String -> GenValue b w i -> Eval (WordValue b w i)
    fromWordVal "during eta-expansion" (GenValue b w i -> Eval (WordValue b w i))
    -> Eval (GenValue b w i) -> Eval (WordValue b w i)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< Eval (GenValue b w i)
    x)
      WordValue b w i -> Eval (WordValue b w i)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (WordValue b w i -> Eval (WordValue b w i))
    -> WordValue b w i -> Eval (WordValue b w i)
    forall a b. (a -> b) -> a -> b
    $ Seq (Eval b) -> WordValue b w i
    forall b w i. Seq (Eval b) -> WordValue b w i
    BitsVal (Seq (Eval b) -> WordValue b w i)
    -> Seq (Eval b) -> WordValue b w i
    forall a b. (a -> b) -> a -> b
    $ Int -> (Int -> Eval b) -> Seq (Eval b)
    forall a. Int -> (Int -> a) -> Seq a
    Seq.fromFunction (Integer -> Int
    forall a. Num a => Integer -> a
    fromInteger Integer
    n) ((Int -> Eval b) -> Seq (Eval b))
    -> (Int -> Eval b) -> Seq (Eval b)
    forall a b. (a -> b) -> a -> b
    $ \i :: Int
    i ->
        do WordValue b w i
    w' <- Eval (WordValue b w i)
    w; WordValue b w i -> Integer -> Eval b
    forall b w i. BitWord b w i => WordValue b w i -> Integer -> Eval b
    indexWordValue WordValue b w i
    w' (Int -> Integer
    forall a. Integral a => a -> Integer
    toInteger Int
    i)

    -- | Given a simulator value and its type, fully eta-expand the value.  This
    --   is a type-directed pass that always produces a canonical value of the
    --   expected shape.  Eta expansion of values is sometimes necessary to ensure
    --   the correct evaluation semantics of recursive definitions.  Otherwise,
    --   expressions that should be expected to produce well-defined values in the
    --   denotational semantics will fail to terminate instead.
    etaDelay :: BitWord b w i
             => String
             -> GenEvalEnv b w i
             -> Schema
             -> Eval (GenValue b w i)
             -> Eval (GenValue b w i)
    etaDelay :: String
    -> GenEvalEnv b w i
    -> Schema
    -> Eval (GenValue b w i)
    -> Eval (GenValue b w i)
    etaDelay msg :: String
    msg env0 :: GenEvalEnv b w i
    env0 Forall{ sVars :: Schema -> [TParam]
    sVars = [TParam]
    vs0, sType :: Schema -> Type
    sType = Type
    tp0 } = GenEvalEnv b w i
    -> [TParam] -> Eval (GenValue b w i) -> Eval (GenValue b w i)
    forall b w i b w i.
    BitWord b w i =>
    GenEvalEnv b w i
    -> [TParam] -> Eval (GenValue b w i) -> Eval (GenValue b w i)
    goTpVars GenEvalEnv b w i
    env0 [TParam]
    vs0
      where
      goTpVars :: GenEvalEnv b w i
    -> [TParam] -> Eval (GenValue b w i) -> Eval (GenValue b w i)
    goTpVars env :: GenEvalEnv b w i
    env []     x :: Eval (GenValue b w i)
    x = TValue -> Eval (GenValue b w i) -> Eval (GenValue b w i)
    forall b w i.
    BitWord b w i =>
    TValue -> Eval (GenValue b w i) -> Eval (GenValue b w i)
    go (HasCallStack => TypeEnv -> Type -> TValue
    TypeEnv -> Type -> TValue
    evalValType (GenEvalEnv b w i -> TypeEnv
    forall b w i. GenEvalEnv b w i -> TypeEnv
    envTypes GenEvalEnv b w i
    env) Type
    tp0) Eval (GenValue b w i)
    x
      goTpVars env :: GenEvalEnv b w i
    env (v :: TParam
    v:vs :: [TParam]
    vs) x :: Eval (GenValue b w i)
    x =
        case TParam -> Kind
    tpKind TParam
    v of
          KType -> GenValue b w i -> Eval (GenValue b w i)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (GenValue b w i -> Eval (GenValue b w i))
    -> GenValue b w i -> Eval (GenValue b w i)
    forall a b. (a -> b) -> a -> b
    $ (TValue -> Eval (GenValue b w i)) -> GenValue b w i
    forall b w i. (TValue -> Eval (GenValue b w i)) -> GenValue b w i
    VPoly ((TValue -> Eval (GenValue b w i)) -> GenValue b w i)
    -> (TValue -> Eval (GenValue b w i)) -> GenValue b w i
    forall a b. (a -> b) -> a -> b
    $ \t :: TValue
    t ->
                      GenEvalEnv b w i
    -> [TParam] -> Eval (GenValue b w i) -> Eval (GenValue b w i)
    goTpVars (TVar -> Either Nat' TValue -> GenEvalEnv b w i -> GenEvalEnv b w i
    forall b w i.
    TVar -> Either Nat' TValue -> GenEvalEnv b w i -> GenEvalEnv b w i
    bindType (TParam -> TVar
    tpVar TParam
    v) (TValue -> Either Nat' TValue
    forall a b. b -> Either a b
    Right TValue
    t) GenEvalEnv b w i
    env) [TParam]
    vs ( ((TValue -> Eval (GenValue b w i))
    -> TValue -> Eval (GenValue b w i)
    forall a b. (a -> b) -> a -> b
    $TValue
    t) ((TValue -> Eval (GenValue b w i)) -> Eval (GenValue b w i))
    -> (GenValue b w i -> TValue -> Eval (GenValue b w i))
    -> GenValue b w i
    -> Eval (GenValue b w i)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . GenValue b w i -> TValue -> Eval (GenValue b w i)
    forall b w i. GenValue b w i -> TValue -> Eval (GenValue b w i)
    fromVPoly (GenValue b w i -> Eval (GenValue b w i))
    -> Eval (GenValue b w i) -> Eval (GenValue b w i)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< Eval (GenValue b w i)
    x )
          KNum  -> GenValue b w i -> Eval (GenValue b w i)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (GenValue b w i -> Eval (GenValue b w i))
    -> GenValue b w i -> Eval (GenValue b w i)
    forall a b. (a -> b) -> a -> b
    $ (Nat' -> Eval (GenValue b w i)) -> GenValue b w i
    forall b w i. (Nat' -> Eval (GenValue b w i)) -> GenValue b w i
    VNumPoly ((Nat' -> Eval (GenValue b w i)) -> GenValue b w i)
    -> (Nat' -> Eval (GenValue b w i)) -> GenValue b w i
    forall a b. (a -> b) -> a -> b
    $ \n :: Nat'
    n ->
                      GenEvalEnv b w i
    -> [TParam] -> Eval (GenValue b w i) -> Eval (GenValue b w i)
    goTpVars (TVar -> Either Nat' TValue -> GenEvalEnv b w i -> GenEvalEnv b w i
    forall b w i.
    TVar -> Either Nat' TValue -> GenEvalEnv b w i -> GenEvalEnv b w i
    bindType (TParam -> TVar
    tpVar TParam
    v) (Nat' -> Either Nat' TValue
    forall a b. a -> Either a b
    Left Nat'
    n) GenEvalEnv b w i
    env) [TParam]
    vs ( ((Nat' -> Eval (GenValue b w i)) -> Nat' -> Eval (GenValue b w i)
    forall a b. (a -> b) -> a -> b
    $Nat'
    n) ((Nat' -> Eval (GenValue b w i)) -> Eval (GenValue b w i))
    -> (GenValue b w i -> Nat' -> Eval (GenValue b w i))
    -> GenValue b w i
    -> Eval (GenValue b w i)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . GenValue b w i -> Nat' -> Eval (GenValue b w i)
    forall b w i. GenValue b w i -> Nat' -> Eval (GenValue b w i)
    fromVNumPoly (GenValue b w i -> Eval (GenValue b w i))
    -> Eval (GenValue b w i) -> Eval (GenValue b w i)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< Eval (GenValue b w i)
    x )
          k :: Kind
    k     -> String -> [String] -> Eval (GenValue b w i)
    forall a. HasCallStack => String -> [String] -> a
    panic "[Eval] etaDelay" ["invalid kind on type abstraction", Kind -> String
    forall a. Show a => a -> String
    show Kind
    k]

      go :: TValue -> Eval (GenValue b w i) -> Eval (GenValue b w i)
    go tp :: TValue
    tp (Ready x :: GenValue b w i
    x) =
        case GenValue b w i
    x of
          VBit _     -> GenValue b w i -> Eval (GenValue b w i)
    forall (m :: * -> *) a. Monad m => a -> m a
    return GenValue b w i
    x
          VInteger _ -> GenValue b w i -> Eval (GenValue b w i)
    forall (m :: * -> *) a. Monad m => a -> m a
    return GenValue b w i
    x
          VWord _ _  -> GenValue b w i -> Eval (GenValue b w i)
    forall (m :: * -> *) a. Monad m => a -> m a
    return GenValue b w i
    x
          VSeq n :: Integer
    n xs :: SeqMap b w i
    xs
            | TVSeq _nt :: Integer
    _nt el :: TValue
    el <- TValue
    tp
            -> GenValue b w i -> Eval (GenValue b w i)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (GenValue b w i -> Eval (GenValue b w i))
    -> GenValue b w i -> Eval (GenValue b w i)
    forall a b. (a -> b) -> a -> b
    $ Integer -> SeqMap b w i -> GenValue b w i
    forall b w i. Integer -> SeqMap b w i -> GenValue b w i
    VSeq Integer
    n (SeqMap b w i -> GenValue b w i) -> SeqMap b w i -> GenValue b w i
    forall a b. (a -> b) -> a -> b
    $ (Integer -> Eval (GenValue b w i)) -> SeqMap b w i
    forall b w i. (Integer -> Eval (GenValue b w i)) -> SeqMap b w i
    IndexSeqMap ((Integer -> Eval (GenValue b w i)) -> SeqMap b w i)
    -> (Integer -> Eval (GenValue b w i)) -> SeqMap b w i
    forall a b. (a -> b) -> a -> b
    $ \i :: Integer
    i -> TValue -> Eval (GenValue b w i) -> Eval (GenValue b w i)
    go TValue
    el (SeqMap b w i -> Integer -> Eval (GenValue b w i)
    forall b w i. SeqMap b w i -> Integer -> Eval (GenValue b w i)
    lookupSeqMap SeqMap b w i
    xs Integer
    i)

          VStream xs :: SeqMap b w i
    xs
            | TVStream el :: TValue
    el <- TValue
    tp
            -> GenValue b w i -> Eval (GenValue b w i)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (GenValue b w i -> Eval (GenValue b w i))
    -> GenValue b w i -> Eval (GenValue b w i)
    forall a b. (a -> b) -> a -> b
    $ SeqMap b w i -> GenValue b w i
    forall b w i. SeqMap b w i -> GenValue b w i
    VStream (SeqMap b w i -> GenValue b w i) -> SeqMap b w i -> GenValue b w i
    forall a b. (a -> b) -> a -> b
    $ (Integer -> Eval (GenValue b w i)) -> SeqMap b w i
    forall b w i. (Integer -> Eval (GenValue b w i)) -> SeqMap b w i
    IndexSeqMap ((Integer -> Eval (GenValue b w i)) -> SeqMap b w i)
    -> (Integer -> Eval (GenValue b w i)) -> SeqMap b w i
    forall a b. (a -> b) -> a -> b
    $ \i :: Integer
    i -> TValue -> Eval (GenValue b w i) -> Eval (GenValue b w i)
    go TValue
    el (SeqMap b w i -> Integer -> Eval (GenValue b w i)
    forall b w i. SeqMap b w i -> Integer -> Eval (GenValue b w i)
    lookupSeqMap SeqMap b w i
    xs Integer
    i)

          VTuple xs :: [Eval (GenValue b w i)]
    xs
            | TVTuple ts :: [TValue]
    ts <- TValue
    tp
            -> GenValue b w i -> Eval (GenValue b w i)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (GenValue b w i -> Eval (GenValue b w i))
    -> GenValue b w i -> Eval (GenValue b w i)
    forall a b. (a -> b) -> a -> b
    $ [Eval (GenValue b w i)] -> GenValue b w i
    forall b w i. [Eval (GenValue b w i)] -> GenValue b w i
    VTuple ((TValue -> Eval (GenValue b w i) -> Eval (GenValue b w i))
    -> [TValue] -> [Eval (GenValue b w i)] -> [Eval (GenValue b w i)]
    forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
    zipWith TValue -> Eval (GenValue b w i) -> Eval (GenValue b w i)
    go [TValue]
    ts [Eval (GenValue b w i)]
    xs)

          VRecord fs :: [(Ident, Eval (GenValue b w i))]
    fs
            | TVRec fts :: [(Ident, TValue)]
    fts <- TValue
    tp
            -> GenValue b w i -> Eval (GenValue b w i)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (GenValue b w i -> Eval (GenValue b w i))
    -> GenValue b w i -> Eval (GenValue b w i)
    forall a b. (a -> b) -> a -> b
    $ [(Ident, Eval (GenValue b w i))] -> GenValue b w i
    forall b w i. [(Ident, Eval (GenValue b w i))] -> GenValue b w i
    VRecord ([(Ident, Eval (GenValue b w i))] -> GenValue b w i)
    -> [(Ident, Eval (GenValue b w i))] -> GenValue b w i
    forall a b. (a -> b) -> a -> b
    $
                 let err :: a -> a
    err f :: a
    f = String -> [String] -> a
    forall a. HasCallStack => String -> [String] -> a
    evalPanic "expected record value with field" [a -> String
    forall a. Show a => a -> String
    show a
    f] in
                 [ (Ident
    f, TValue -> Eval (GenValue b w i) -> Eval (GenValue b w i)
    go (TValue -> Maybe TValue -> TValue
    forall a. a -> Maybe a -> a
    fromMaybe (Ident -> TValue
    forall a a. Show a => a -> a
    err Ident
    f) (Ident -> [(Ident, TValue)] -> Maybe TValue
    forall a b. Eq a => a -> [(a, b)] -> Maybe b
    lookup Ident
    f [(Ident, TValue)]
    fts)) Eval (GenValue b w i)
    y)
                 | (f :: Ident
    f, y :: Eval (GenValue b w i)
    y) <- [(Ident, Eval (GenValue b w i))]
    fs
                 ]

          VFun f :: Eval (GenValue b w i) -> Eval (GenValue b w i)
    f
            | TVFun _t1 :: TValue
    _t1 t2 :: TValue
    t2 <- TValue
    tp
            -> GenValue b w i -> Eval (GenValue b w i)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (GenValue b w i -> Eval (GenValue b w i))
    -> GenValue b w i -> Eval (GenValue b w i)
    forall a b. (a -> b) -> a -> b
    $ (Eval (GenValue b w i) -> Eval (GenValue b w i)) -> GenValue b w i
    forall b w i.
    (Eval (GenValue b w i) -> Eval (GenValue b w i)) -> GenValue b w i
    VFun ((Eval (GenValue b w i) -> Eval (GenValue b w i))
     -> GenValue b w i)
    -> (Eval (GenValue b w i) -> Eval (GenValue b w i))
    -> GenValue b w i
    forall a b. (a -> b) -> a -> b
    $ \a :: Eval (GenValue b w i)
    a -> TValue -> Eval (GenValue b w i) -> Eval (GenValue b w i)
    go TValue
    t2 (Eval (GenValue b w i) -> Eval (GenValue b w i)
    f Eval (GenValue b w i)
    a)

          _ -> String -> [String] -> Eval (GenValue b w i)
    forall a. HasCallStack => String -> [String] -> a
    evalPanic "type mismatch during eta-expansion" []

      go tp :: TValue
    tp x :: Eval (GenValue b w i)
    x =
        case TValue
    tp of
          TVBit -> Eval (GenValue b w i)
    x
          TVInteger -> Eval (GenValue b w i)
    x
          TVIntMod _ -> Eval (GenValue b w i)
    x

          TVSeq n :: Integer
    n TVBit ->
              do Eval (WordValue b w i)
    w <- Eval (WordValue b w i)
    -> Eval (WordValue b w i) -> Eval (Eval (WordValue b w i))
    forall a. Eval a -> Eval a -> Eval (Eval a)
    delayFill (String -> GenValue b w i -> Eval (WordValue b w i)
    forall b w i. String -> GenValue b w i -> Eval (WordValue b w i)
    fromWordVal "during eta-expansion" (GenValue b w i -> Eval (WordValue b w i))
    -> Eval (GenValue b w i) -> Eval (WordValue b w i)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< Eval (GenValue b w i)
    x) (Integer -> Eval (GenValue b w i) -> Eval (WordValue b w i)
    forall b w i.
    BitWord b w i =>
    Integer -> Eval (GenValue b w i) -> Eval (WordValue b w i)
    etaWord Integer
    n Eval (GenValue b w i)
    x)
                 GenValue b w i -> Eval (GenValue b w i)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (GenValue b w i -> Eval (GenValue b w i))
    -> GenValue b w i -> Eval (GenValue b w i)
    forall a b. (a -> b) -> a -> b
    $ Integer -> Eval (WordValue b w i) -> GenValue b w i
    forall b w i. Integer -> Eval (WordValue b w i) -> GenValue b w i
    VWord Integer
    n Eval (WordValue b w i)
    w

          TVSeq n :: Integer
    n el :: TValue
    el ->
              do Eval (SeqMap b w i)
    x' <- Maybe String -> Eval (SeqMap b w i) -> Eval (Eval (SeqMap b w i))
    forall a. Maybe String -> Eval a -> Eval (Eval a)
    delay (String -> Maybe String
    forall a. a -> Maybe a
    Just String
    msg) (String -> GenValue b w i -> Eval (SeqMap b w i)
    forall b w i.
    BitWord b w i =>
    String -> GenValue b w i -> Eval (SeqMap b w i)
    fromSeq "during eta-expansion" (GenValue b w i -> Eval (SeqMap b w i))
    -> Eval (GenValue b w i) -> Eval (SeqMap b w i)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< Eval (GenValue b w i)
    x)
                 GenValue b w i -> Eval (GenValue b w i)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (GenValue b w i -> Eval (GenValue b w i))
    -> GenValue b w i -> Eval (GenValue b w i)
    forall a b. (a -> b) -> a -> b
    $ Integer -> SeqMap b w i -> GenValue b w i
    forall b w i. Integer -> SeqMap b w i -> GenValue b w i
    VSeq Integer
    n (SeqMap b w i -> GenValue b w i) -> SeqMap b w i -> GenValue b w i
    forall a b. (a -> b) -> a -> b
    $ (Integer -> Eval (GenValue b w i)) -> SeqMap b w i
    forall b w i. (Integer -> Eval (GenValue b w i)) -> SeqMap b w i
    IndexSeqMap ((Integer -> Eval (GenValue b w i)) -> SeqMap b w i)
    -> (Integer -> Eval (GenValue b w i)) -> SeqMap b w i
    forall a b. (a -> b) -> a -> b
    $ \i :: Integer
    i -> do
                   TValue -> Eval (GenValue b w i) -> Eval (GenValue b w i)
    go TValue
    el ((SeqMap b w i -> Integer -> Eval (GenValue b w i))
    -> Integer -> SeqMap b w i -> Eval (GenValue b w i)
    forall a b c. (a -> b -> c) -> b -> a -> c
    flip SeqMap b w i -> Integer -> Eval (GenValue b w i)
    forall b w i. SeqMap b w i -> Integer -> Eval (GenValue b w i)
    lookupSeqMap Integer
    i (SeqMap b w i -> Eval (GenValue b w i))
    -> Eval (SeqMap b w i) -> Eval (GenValue b w i)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< Eval (SeqMap b w i)
    x')

          TVStream el :: TValue
    el ->
              do Eval (SeqMap b w i)
    x' <- Maybe String -> Eval (SeqMap b w i) -> Eval (Eval (SeqMap b w i))
    forall a. Maybe String -> Eval a -> Eval (Eval a)
    delay (String -> Maybe String
    forall a. a -> Maybe a
    Just String
    msg) (String -> GenValue b w i -> Eval (SeqMap b w i)
    forall b w i.
    BitWord b w i =>
    String -> GenValue b w i -> Eval (SeqMap b w i)
    fromSeq "during eta-expansion" (GenValue b w i -> Eval (SeqMap b w i))
    -> Eval (GenValue b w i) -> Eval (SeqMap b w i)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< Eval (GenValue b w i)
    x)
                 GenValue b w i -> Eval (GenValue b w i)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (GenValue b w i -> Eval (GenValue b w i))
    -> GenValue b w i -> Eval (GenValue b w i)
    forall a b. (a -> b) -> a -> b
    $ SeqMap b w i -> GenValue b w i
    forall b w i. SeqMap b w i -> GenValue b w i
    VStream (SeqMap b w i -> GenValue b w i) -> SeqMap b w i -> GenValue b w i
    forall a b. (a -> b) -> a -> b
    $ (Integer -> Eval (GenValue b w i)) -> SeqMap b w i
    forall b w i. (Integer -> Eval (GenValue b w i)) -> SeqMap b w i
    IndexSeqMap ((Integer -> Eval (GenValue b w i)) -> SeqMap b w i)
    -> (Integer -> Eval (GenValue b w i)) -> SeqMap b w i
    forall a b. (a -> b) -> a -> b
    $ \i :: Integer
    i ->
                   TValue -> Eval (GenValue b w i) -> Eval (GenValue b w i)
    go TValue
    el ((SeqMap b w i -> Integer -> Eval (GenValue b w i))
    -> Integer -> SeqMap b w i -> Eval (GenValue b w i)
    forall a b c. (a -> b -> c) -> b -> a -> c
    flip SeqMap b w i -> Integer -> Eval (GenValue b w i)
    forall b w i. SeqMap b w i -> Integer -> Eval (GenValue b w i)
    lookupSeqMap Integer
    i (SeqMap b w i -> Eval (GenValue b w i))
    -> Eval (SeqMap b w i) -> Eval (GenValue b w i)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< Eval (SeqMap b w i)
    x')

          TVFun _t1 :: TValue
    _t1 t2 :: TValue
    t2 ->
              do Eval (Eval (GenValue b w i) -> Eval (GenValue b w i))
    x' <- Maybe String
    -> Eval (Eval (GenValue b w i) -> Eval (GenValue b w i))
    -> Eval (Eval (Eval (GenValue b w i) -> Eval (GenValue b w i)))
    forall a. Maybe String -> Eval a -> Eval (Eval a)
    delay (String -> Maybe String
    forall a. a -> Maybe a
    Just String
    msg) (GenValue b w i -> Eval (GenValue b w i) -> Eval (GenValue b w i)
    forall b w i.
    GenValue b w i -> Eval (GenValue b w i) -> Eval (GenValue b w i)
    fromVFun (GenValue b w i -> Eval (GenValue b w i) -> Eval (GenValue b w i))
    -> Eval (GenValue b w i)
    -> Eval (Eval (GenValue b w i) -> Eval (GenValue b w i))
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Eval (GenValue b w i)
    x)
                 GenValue b w i -> Eval (GenValue b w i)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (GenValue b w i -> Eval (GenValue b w i))
    -> GenValue b w i -> Eval (GenValue b w i)
    forall a b. (a -> b) -> a -> b
    $ (Eval (GenValue b w i) -> Eval (GenValue b w i)) -> GenValue b w i
    forall b w i.
    (Eval (GenValue b w i) -> Eval (GenValue b w i)) -> GenValue b w i
    VFun ((Eval (GenValue b w i) -> Eval (GenValue b w i))
     -> GenValue b w i)
    -> (Eval (GenValue b w i) -> Eval (GenValue b w i))
    -> GenValue b w i
    forall a b. (a -> b) -> a -> b
    $ \a :: Eval (GenValue b w i)
    a -> TValue -> Eval (GenValue b w i) -> Eval (GenValue b w i)
    go TValue
    t2 ( ((Eval (GenValue b w i) -> Eval (GenValue b w i))
    -> Eval (GenValue b w i) -> Eval (GenValue b w i)
    forall a b. (a -> b) -> a -> b
    $Eval (GenValue b w i)
    a) ((Eval (GenValue b w i) -> Eval (GenValue b w i))
     -> Eval (GenValue b w i))
    -> Eval (Eval (GenValue b w i) -> Eval (GenValue b w i))
    -> Eval (GenValue b w i)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< Eval (Eval (GenValue b w i) -> Eval (GenValue b w i))
    x' )

          TVTuple ts :: [TValue]
    ts ->
              do let n :: Int
    n = [TValue] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length [TValue]
    ts
                 Eval [Eval (GenValue b w i)]
    x' <- Maybe String
    -> Eval [Eval (GenValue b w i)]
    -> Eval (Eval [Eval (GenValue b w i)])
    forall a. Maybe String -> Eval a -> Eval (Eval a)
    delay (String -> Maybe String
    forall a. a -> Maybe a
    Just String
    msg) (GenValue b w i -> [Eval (GenValue b w i)]
    forall b w i. GenValue b w i -> [Eval (GenValue b w i)]
    fromVTuple (GenValue b w i -> [Eval (GenValue b w i)])
    -> Eval (GenValue b w i) -> Eval [Eval (GenValue b w i)]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Eval (GenValue b w i)
    x)
                 GenValue b w i -> Eval (GenValue b w i)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (GenValue b w i -> Eval (GenValue b w i))
    -> GenValue b w i -> Eval (GenValue b w i)
    forall a b. (a -> b) -> a -> b
    $ [Eval (GenValue b w i)] -> GenValue b w i
    forall b w i. [Eval (GenValue b w i)] -> GenValue b w i
    VTuple ([Eval (GenValue b w i)] -> GenValue b w i)
    -> [Eval (GenValue b w i)] -> GenValue b w i
    forall a b. (a -> b) -> a -> b
    $
                    [ TValue -> Eval (GenValue b w i) -> Eval (GenValue b w i)
    go TValue
    t (Eval (GenValue b w i) -> Eval (GenValue b w i))
    -> Eval (Eval (GenValue b w i)) -> Eval (GenValue b w i)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< (([Eval (GenValue b w i)] -> Int -> Eval (GenValue b w i))
    -> Int -> [Eval (GenValue b w i)] -> Eval (GenValue b w i)
    forall a b c. (a -> b -> c) -> b -> a -> c
    flip [Eval (GenValue b w i)] -> Int -> Eval (GenValue b w i)
    forall i a. Integral i => [a] -> i -> a
    genericIndex Int
    i ([Eval (GenValue b w i)] -> Eval (GenValue b w i))
    -> Eval [Eval (GenValue b w i)] -> Eval (Eval (GenValue b w i))
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Eval [Eval (GenValue b w i)]
    x')
                    | Int
    i <- [0..(Int
    nInt -> Int -> Int
    forall a. Num a => a -> a -> a
    -1)]
                    | TValue
    t <- [TValue]
    ts
                    ]

          TVRec fs :: [(Ident, TValue)]
    fs ->
              do Eval [(Ident, Eval (GenValue b w i))]
    x' <- Maybe String
    -> Eval [(Ident, Eval (GenValue b w i))]
    -> Eval (Eval [(Ident, Eval (GenValue b w i))])
    forall a. Maybe String -> Eval a -> Eval (Eval a)
    delay (String -> Maybe String
    forall a. a -> Maybe a
    Just String
    msg) (GenValue b w i -> [(Ident, Eval (GenValue b w i))]
    forall b w i. GenValue b w i -> [(Ident, Eval (GenValue b w i))]
    fromVRecord (GenValue b w i -> [(Ident, Eval (GenValue b w i))])
    -> Eval (GenValue b w i) -> Eval [(Ident, Eval (GenValue b w i))]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Eval (GenValue b w i)
    x)
                 let err :: a -> a
    err f :: a
    f = String -> [String] -> a
    forall a. HasCallStack => String -> [String] -> a
    evalPanic "expected record value with field" [a -> String
    forall a. Show a => a -> String
    show a
    f]
                 GenValue b w i -> Eval (GenValue b w i)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (GenValue b w i -> Eval (GenValue b w i))
    -> GenValue b w i -> Eval (GenValue b w i)
    forall a b. (a -> b) -> a -> b
    $ [(Ident, Eval (GenValue b w i))] -> GenValue b w i
    forall b w i. [(Ident, Eval (GenValue b w i))] -> GenValue b w i
    VRecord ([(Ident, Eval (GenValue b w i))] -> GenValue b w i)
    -> [(Ident, Eval (GenValue b w i))] -> GenValue b w i
    forall a b. (a -> b) -> a -> b
    $
                    [ (Ident
    f, TValue -> Eval (GenValue b w i) -> Eval (GenValue b w i)
    go TValue
    t (Eval (GenValue b w i) -> Eval (GenValue b w i))
    -> Eval (Eval (GenValue b w i)) -> Eval (GenValue b w i)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< (Eval (GenValue b w i)
    -> Maybe (Eval (GenValue b w i)) -> Eval (GenValue b w i)
    forall a. a -> Maybe a -> a
    fromMaybe (Ident -> Eval (GenValue b w i)
    forall a a. Show a => a -> a
    err Ident
    f) (Maybe (Eval (GenValue b w i)) -> Eval (GenValue b w i))
    -> ([(Ident, Eval (GenValue b w i))]
        -> Maybe (Eval (GenValue b w i)))
    -> [(Ident, Eval (GenValue b w i))]
    -> Eval (GenValue b w i)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Ident
    -> [(Ident, Eval (GenValue b w i))]
    -> Maybe (Eval (GenValue b w i))
    forall a b. Eq a => a -> [(a, b)] -> Maybe b
    lookup Ident
    f ([(Ident, Eval (GenValue b w i))] -> Eval (GenValue b w i))
    -> Eval [(Ident, Eval (GenValue b w i))]
    -> Eval (Eval (GenValue b w i))
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Eval [(Ident, Eval (GenValue b w i))]
    x'))
                    | (f :: Ident
    f,t :: TValue
    t) <- [(Ident, TValue)]
    fs
                    ]

          TVAbstract {} -> Eval (GenValue b w i)
    x

    declHole :: Decl
             -> Eval (Name, Schema, Eval (GenValue b w i), Eval (GenValue b w i) -> Eval ())
    declHole :: Decl
    -> Eval
         (Name, Schema, Eval (GenValue b w i),
          Eval (GenValue b w i) -> Eval ())
    declHole d :: Decl
    d =
      case Decl -> DeclDef
    dDefinition Decl
    d of
        DPrim   -> String
    -> [String]
    -> Eval
         (Name, Schema, Eval (GenValue b w i),
          Eval (GenValue b w i) -> Eval ())
    forall a. HasCallStack => String -> [String] -> a
    evalPanic "Unexpected primitive declaration in recursive group"
                             [Doc -> String
    forall a. Show a => a -> String
    show (Name -> Doc
    ppLocName Name
    nm)]
        DExpr _ -> do
          (hole :: Eval (GenValue b w i)
    hole, fill :: Eval (GenValue b w i) -> Eval ()
    fill) <- String
    -> Eval (Eval (GenValue b w i), Eval (GenValue b w i) -> Eval ())
    forall a. String -> Eval (Eval a, Eval a -> Eval ())
    blackhole String
    msg
          (Name, Schema, Eval (GenValue b w i),
     Eval (GenValue b w i) -> Eval ())
    -> Eval
         (Name, Schema, Eval (GenValue b w i),
          Eval (GenValue b w i) -> Eval ())
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Name
    nm, Schema
    sch, Eval (GenValue b w i)
    hole, Eval (GenValue b w i) -> Eval ()
    fill)
      where
      nm :: Name
    nm = Decl -> Name
    dName Decl
    d
      sch :: Schema
    sch = Decl -> Schema
    dSignature Decl
    d
      msg :: String
    msg = [String] -> String
    unwords ["<<loop>> while evaluating", Doc -> String
    forall a. Show a => a -> String
    show (Name -> Doc
    forall a. PP a => a -> Doc
    pp Name
    nm)]

    -- | Evaluate a declaration, extending the evaluation environment.
    --   Two input environments are given: the first is an environment
    --   to use when evaluating the body of the declaration; the second
    --   is the environment to extend.  There are two environments to
    --   handle the subtle name-binding issues that arise from recursive
    --   definitions.  The 'read only' environment is used to bring recursive
    --   names into scope while we are still defining them.
    evalDecl :: EvalPrims b w i
             => GenEvalEnv b w i  -- ^ A 'read only' environment for use in declaration bodies
             -> GenEvalEnv b w i  -- ^ An evaluation environment to extend with the given declaration
             -> Decl              -- ^ The declaration to evaluate
             -> Eval (GenEvalEnv b w i)
    evalDecl :: GenEvalEnv b w i
    -> GenEvalEnv b w i -> Decl -> Eval (GenEvalEnv b w i)
    evalDecl renv :: GenEvalEnv b w i
    renv env :: GenEvalEnv b w i
    env d :: Decl
    d =
      case Decl -> DeclDef
    dDefinition Decl
    d of
        DPrim   -> case Decl -> Maybe (GenValue b w i)
    forall b w i. EvalPrims b w i => Decl -> Maybe (GenValue b w i)
    evalPrim Decl
    d of
                     Just v :: GenValue b w i
    v  -> GenEvalEnv b w i -> Eval (GenEvalEnv b w i)
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Name -> GenValue b w i -> GenEvalEnv b w i -> GenEvalEnv b w i
    forall b w i.
    Name -> GenValue b w i -> GenEvalEnv b w i -> GenEvalEnv b w i
    bindVarDirect (Decl -> Name
    dName Decl
    d) GenValue b w i
    v GenEvalEnv b w i
    env)
                     Nothing -> Name
    -> Eval (GenValue b w i)
    -> GenEvalEnv b w i
    -> Eval (GenEvalEnv b w i)
    forall b w i.
    Name
    -> Eval (GenValue b w i)
    -> GenEvalEnv b w i
    -> Eval (GenEvalEnv b w i)
    bindVar (Decl -> Name
    dName Decl
    d) (Name -> Eval (GenValue b w i)
    forall a. Name -> Eval a
    cryNoPrimError (Decl -> Name
    dName Decl
    d)) GenEvalEnv b w i
    env

        DExpr e :: Expr
    e -> Name
    -> Eval (GenValue b w i)
    -> GenEvalEnv b w i
    -> Eval (GenEvalEnv b w i)
    forall b w i.
    Name
    -> Eval (GenValue b w i)
    -> GenEvalEnv b w i
    -> Eval (GenEvalEnv b w i)
    bindVar (Decl -> Name
    dName Decl
    d) (GenEvalEnv b w i -> Expr -> Eval (GenValue b w i)
    forall b w i.
    EvalPrims b w i =>
    GenEvalEnv b w i -> Expr -> Eval (GenValue b w i)
    evalExpr GenEvalEnv b w i
    renv Expr
    e) GenEvalEnv b w i
    env

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

    -- | Apply the the given "selector" form to the given value.  This function pushes
    --   tuple and record selections pointwise down into other value constructs
    --   (e.g., streams and functions).
    evalSel :: forall b w i
             . EvalPrims b w i
            => GenValue b w i
            -> Selector
            -> Eval (GenValue b w i)
    evalSel :: GenValue b w i -> Selector -> Eval (GenValue b w i)
    evalSel val :: GenValue b w i
    val sel :: Selector
    sel = case Selector
    sel of

      TupleSel n :: Int
    n _  -> Int -> GenValue b w i -> Eval (GenValue b w i)
    forall b w i.
    BitWord b w i =>
    Int -> GenValue b w i -> Eval (GenValue b w i)
    tupleSel Int
    n GenValue b w i
    val
      RecordSel n :: Ident
    n _ -> Ident -> GenValue b w i -> Eval (GenValue b w i)
    forall b w i.
    BitWord b w i =>
    Ident -> GenValue b w i -> Eval (GenValue b w i)
    recordSel Ident
    n GenValue b w i
    val
      ListSel ix :: Int
    ix _  -> Int -> GenValue b w i -> Eval (GenValue b w i)
    forall a b w i.
    (Integral a, BitWord b w i) =>
    a -> GenValue b w i -> Eval (GenValue b w i)
    listSel Int
    ix GenValue b w i
    val
      where

      tupleSel :: Int -> GenValue b w i -> Eval (GenValue b w i)
    tupleSel n :: Int
    n v :: GenValue b w i
    v =
        case GenValue b w i
    v of
          VTuple vs :: [Eval (GenValue b w i)]
    vs       -> [Eval (GenValue b w i)]
    vs [Eval (GenValue b w i)] -> Int -> Eval (GenValue b w i)
    forall a. [a] -> Int -> a
    !! Int
    n
          _               -> do Doc
    vdoc <- PPOpts -> GenValue b w i -> Eval Doc
    forall b w i. BitWord b w i => PPOpts -> GenValue b w i -> Eval Doc
    ppValue PPOpts
    defaultPPOpts GenValue b w i
    v
                                String -> [String] -> Eval (GenValue b w i)
    forall a. HasCallStack => String -> [String] -> a
    evalPanic "Cryptol.Eval.evalSel"
                                  [ "Unexpected value in tuple selection"
                                  , Doc -> String
    forall a. Show a => a -> String
    show Doc
    vdoc ]

      recordSel :: Ident -> GenValue b w i -> Eval (GenValue b w i)
    recordSel n :: Ident
    n v :: GenValue b w i
    v =
        case GenValue b w i
    v of
          VRecord {}      -> Ident -> GenValue b w i -> Eval (GenValue b w i)
    forall b w i. Ident -> GenValue b w i -> Eval (GenValue b w i)
    lookupRecord Ident
    n GenValue b w i
    v
          _               -> do Doc
    vdoc <- PPOpts -> GenValue b w i -> Eval Doc
    forall b w i. BitWord b w i => PPOpts -> GenValue b w i -> Eval Doc
    ppValue PPOpts
    defaultPPOpts GenValue b w i
    v
                                String -> [String] -> Eval (GenValue b w i)
    forall a. HasCallStack => String -> [String] -> a
    evalPanic "Cryptol.Eval.evalSel"
                                  [ "Unexpected value in record selection"
                                  , Doc -> String
    forall a. Show a => a -> String
    show Doc
    vdoc ]

      listSel :: a -> GenValue b w i -> Eval (GenValue b w i)
    listSel n :: a
    n v :: GenValue b w i
    v =
        case GenValue b w i
    v of
          VSeq _ vs :: SeqMap b w i
    vs       -> SeqMap b w i -> Integer -> Eval (GenValue b w i)
    forall b w i. SeqMap b w i -> Integer -> Eval (GenValue b w i)
    lookupSeqMap SeqMap b w i
    vs (a -> Integer
    forall a. Integral a => a -> Integer
    toInteger a
    n)
          VStream vs :: SeqMap b w i
    vs      -> SeqMap b w i -> Integer -> Eval (GenValue b w i)
    forall b w i. SeqMap b w i -> Integer -> Eval (GenValue b w i)
    lookupSeqMap SeqMap b w i
    vs (a -> Integer
    forall a. Integral a => a -> Integer
    toInteger a
    n)
          VWord _ wv :: Eval (WordValue b w i)
    wv      -> b -> GenValue b w i
    forall b w i. b -> GenValue b w i
    VBit (b -> GenValue b w i) -> Eval b -> Eval (GenValue b w i)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> ((WordValue b w i -> Integer -> Eval b)
    -> Integer -> WordValue b w i -> Eval b
    forall a b c. (a -> b -> c) -> b -> a -> c
    flip WordValue b w i -> Integer -> Eval b
    forall b w i. BitWord b w i => WordValue b w i -> Integer -> Eval b
    indexWordValue (a -> Integer
    forall a. Integral a => a -> Integer
    toInteger a
    n) (WordValue b w i -> Eval b) -> Eval (WordValue b w i) -> Eval b
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< Eval (WordValue b w i)
    wv)
          _               -> do Doc
    vdoc <- PPOpts -> GenValue b w i -> Eval Doc
    forall b w i. BitWord b w i => PPOpts -> GenValue b w i -> Eval Doc
    ppValue PPOpts
    defaultPPOpts GenValue b w i
    val
                                String -> [String] -> Eval (GenValue b w i)
    forall a. HasCallStack => String -> [String] -> a
    evalPanic "Cryptol.Eval.evalSel"
                                  [ "Unexpected value in list selection"
                                  , Doc -> String
    forall a. Show a => a -> String
    show Doc
    vdoc ]

    evalSetSel :: forall b w i. EvalPrims b w i =>
      GenValue b w i -> Selector -> Eval (GenValue b w i) -> Eval (GenValue b w i)
    evalSetSel :: GenValue b w i
    -> Selector -> Eval (GenValue b w i) -> Eval (GenValue b w i)
    evalSetSel e :: GenValue b w i
    e x :: Selector
    x v :: Eval (GenValue b w i)
    v =
      case Selector
    x of
        TupleSel n :: Int
    n _  -> Int -> Eval (GenValue b w i)
    setTuple Int
    n
        RecordSel n :: Ident
    n _ -> Ident -> Eval (GenValue b w i)
    setRecord Ident
    n
        ListSel ix :: Int
    ix _  -> Integer -> Eval (GenValue b w i)
    setList (Int -> Integer
    forall a. Integral a => a -> Integer
    toInteger Int
    ix)

      where
      bad :: String -> Eval b
    bad msg :: String
    msg =
        do Doc
    ed <- PPOpts -> GenValue b w i -> Eval Doc
    forall b w i. BitWord b w i => PPOpts -> GenValue b w i -> Eval Doc
    ppValue PPOpts
    defaultPPOpts GenValue b w i
    e
           String -> [String] -> Eval b
    forall a. HasCallStack => String -> [String] -> a
    evalPanic "Cryptol.Eval.evalSetSel"
              [ String
    msg
              , "Selector: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Doc -> String
    forall a. Show a => a -> String
    show (Selector -> Doc
    ppSelector Selector
    x)
              , "Value: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Doc -> String
    forall a. Show a => a -> String
    show Doc
    ed
              ]

      setTuple :: Int -> Eval (GenValue b w i)
    setTuple n :: Int
    n =
        case GenValue b w i
    e of
          VTuple xs :: [Eval (GenValue b w i)]
    xs ->
            case Int
    -> [Eval (GenValue b w i)]
    -> ([Eval (GenValue b w i)], [Eval (GenValue b w i)])
    forall a. Int -> [a] -> ([a], [a])
    splitAt Int
    n [Eval (GenValue b w i)]
    xs of
              (as :: [Eval (GenValue b w i)]
    as, _: bs :: [Eval (GenValue b w i)]
    bs) -> GenValue b w i -> Eval (GenValue b w i)
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure ([Eval (GenValue b w i)] -> GenValue b w i
    forall b w i. [Eval (GenValue b w i)] -> GenValue b w i
    VTuple ([Eval (GenValue b w i)]
    as [Eval (GenValue b w i)]
    -> [Eval (GenValue b w i)] -> [Eval (GenValue b w i)]
    forall a. [a] -> [a] -> [a]
    ++ Eval (GenValue b w i)
    v Eval (GenValue b w i)
    -> [Eval (GenValue b w i)] -> [Eval (GenValue b w i)]
    forall a. a -> [a] -> [a]
    : [Eval (GenValue b w i)]
    bs))
              _ -> String -> Eval (GenValue b w i)
    forall b. String -> Eval b
    bad "Tuple update out of bounds."
          _ -> String -> Eval (GenValue b w i)
    forall b. String -> Eval b
    bad "Tuple update on a non-tuple."

      setRecord :: Ident -> Eval (GenValue b w i)
    setRecord n :: Ident
    n =
        case GenValue b w i
    e of
          VRecord xs :: [(Ident, Eval (GenValue b w i))]
    xs ->
            case ((Ident, Eval (GenValue b w i)) -> Bool)
    -> [(Ident, Eval (GenValue b w i))]
    -> ([(Ident, Eval (GenValue b w i))],
        [(Ident, Eval (GenValue b w i))])
    forall a. (a -> Bool) -> [a] -> ([a], [a])
    break ((Ident
    n Ident -> Ident -> Bool
    forall a. Eq a => a -> a -> Bool
    ==) (Ident -> Bool)
    -> ((Ident, Eval (GenValue b w i)) -> Ident)
    -> (Ident, Eval (GenValue b w i))
    -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Ident, Eval (GenValue b w i)) -> Ident
    forall a b. (a, b) -> a
    fst) [(Ident, Eval (GenValue b w i))]
    xs of
              (as :: [(Ident, Eval (GenValue b w i))]
    as, (i :: Ident
    i,_) : bs :: [(Ident, Eval (GenValue b w i))]
    bs) -> GenValue b w i -> Eval (GenValue b w i)
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure ([(Ident, Eval (GenValue b w i))] -> GenValue b w i
    forall b w i. [(Ident, Eval (GenValue b w i))] -> GenValue b w i
    VRecord ([(Ident, Eval (GenValue b w i))]
    as [(Ident, Eval (GenValue b w i))]
    -> [(Ident, Eval (GenValue b w i))]
    -> [(Ident, Eval (GenValue b w i))]
    forall a. [a] -> [a] -> [a]
    ++ (Ident
    i,Eval (GenValue b w i)
    v) (Ident, Eval (GenValue b w i))
    -> [(Ident, Eval (GenValue b w i))]
    -> [(Ident, Eval (GenValue b w i))]
    forall a. a -> [a] -> [a]
    : [(Ident, Eval (GenValue b w i))]
    bs))
              _ -> String -> Eval (GenValue b w i)
    forall b. String -> Eval b
    bad "Missing field in record update."
          _ -> String -> Eval (GenValue b w i)
    forall b. String -> Eval b
    bad "Record update on a non-record."

      setList :: Integer -> Eval (GenValue b w i)
    setList n :: Integer
    n =
        case GenValue b w i
    e of
          VSeq i :: Integer
    i mp :: SeqMap b w i
    mp  -> GenValue b w i -> Eval (GenValue b w i)
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (GenValue b w i -> Eval (GenValue b w i))
    -> GenValue b w i -> Eval (GenValue b w i)
    forall a b. (a -> b) -> a -> b
    $ Integer -> SeqMap b w i -> GenValue b w i
    forall b w i. Integer -> SeqMap b w i -> GenValue b w i
    VSeq Integer
    i  (SeqMap b w i -> GenValue b w i) -> SeqMap b w i -> GenValue b w i
    forall a b. (a -> b) -> a -> b
    $ SeqMap b w i -> Integer -> Eval (GenValue b w i) -> SeqMap b w i
    forall b w i.
    SeqMap b w i -> Integer -> Eval (GenValue b w i) -> SeqMap b w i
    updateSeqMap SeqMap b w i
    mp Integer
    n Eval (GenValue b w i)
    v
          VStream mp :: SeqMap b w i
    mp -> GenValue b w i -> Eval (GenValue b w i)
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (GenValue b w i -> Eval (GenValue b w i))
    -> GenValue b w i -> Eval (GenValue b w i)
    forall a b. (a -> b) -> a -> b
    $ SeqMap b w i -> GenValue b w i
    forall b w i. SeqMap b w i -> GenValue b w i
    VStream (SeqMap b w i -> GenValue b w i) -> SeqMap b w i -> GenValue b w i
    forall a b. (a -> b) -> a -> b
    $ SeqMap b w i -> Integer -> Eval (GenValue b w i) -> SeqMap b w i
    forall b w i.
    SeqMap b w i -> Integer -> Eval (GenValue b w i) -> SeqMap b w i
    updateSeqMap SeqMap b w i
    mp Integer
    n Eval (GenValue b w i)
    v
          VWord i :: Integer
    i m :: Eval (WordValue b w i)
    m  -> GenValue b w i -> Eval (GenValue b w i)
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (GenValue b w i -> Eval (GenValue b w i))
    -> GenValue b w i -> Eval (GenValue b w i)
    forall a b. (a -> b) -> a -> b
    $ Integer -> Eval (WordValue b w i) -> GenValue b w i
    forall b w i. Integer -> Eval (WordValue b w i) -> GenValue b w i
    VWord Integer
    i (Eval (WordValue b w i) -> GenValue b w i)
    -> Eval (WordValue b w i) -> GenValue b w i
    forall a b. (a -> b) -> a -> b
    $ do WordValue b w i
    m1 <- Eval (WordValue b w i)
    m
                                            WordValue b w i -> Integer -> Eval b -> Eval (WordValue b w i)
    forall b w i.
    BitWord b w i =>
    WordValue b w i -> Integer -> Eval b -> Eval (WordValue b w i)
    updateWordValue WordValue b w i
    m1 Integer
    n Eval b
    asBit
          _ -> String -> Eval (GenValue b w i)
    forall b. String -> Eval b
    bad "Sequence update on a non-sequence."

      asBit :: Eval b
    asBit = do GenValue b w i
    res <- Eval (GenValue b w i)
    v
                 case GenValue b w i
    res of
                   VBit b :: b
    b -> b -> Eval b
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure b
    b
                   _      -> String -> Eval b
    forall b. String -> Eval b
    bad "Expected a bit, but got something else"

    -- List Comprehension Environments ---------------------------------------------

    -- | 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 b w i = ListEnv
      { ListEnv b w i -> Map Name (Integer -> Eval (GenValue b w i))
    leVars   :: !(Map.Map Name (Integer -> Eval (GenValue b w i)))
          -- ^ Bindings whose values vary by position
      , ListEnv b w i -> Map Name (Eval (GenValue b w i))
    leStatic :: !(Map.Map Name (Eval (GenValue b w i)))
          -- ^ Bindings whose values are constant
      , ListEnv b w i -> TypeEnv
    leTypes  :: !TypeEnv
      }

    instance Semigroup (ListEnv b w i) where
      l :: ListEnv b w i
    l <> :: ListEnv b w i -> ListEnv b w i -> ListEnv b w i
    <> r :: ListEnv b w i
    r = $WListEnv :: forall b w i.
    Map Name (Integer -> Eval (GenValue b w i))
    -> Map Name (Eval (GenValue b w i)) -> TypeEnv -> ListEnv b w i
    ListEnv
        { leVars :: Map Name (Integer -> Eval (GenValue b w i))
    leVars   = Map Name (Integer -> Eval (GenValue b w i))
    -> Map Name (Integer -> Eval (GenValue b w i))
    -> Map Name (Integer -> Eval (GenValue b w i))
    forall k a. Ord k => Map k a -> Map k a -> Map k a
    Map.union (ListEnv b w i -> Map Name (Integer -> Eval (GenValue b w i))
    forall b w i.
    ListEnv b w i -> Map Name (Integer -> Eval (GenValue b w i))
    leVars  ListEnv b w i
    l)  (ListEnv b w i -> Map Name (Integer -> Eval (GenValue b w i))
    forall b w i.
    ListEnv b w i -> Map Name (Integer -> Eval (GenValue b w i))
    leVars  ListEnv b w i
    r)
        , leStatic :: Map Name (Eval (GenValue b w i))
    leStatic = Map Name (Eval (GenValue b w i))
    -> Map Name (Eval (GenValue b w i))
    -> Map Name (Eval (GenValue b w i))
    forall k a. Ord k => Map k a -> Map k a -> Map k a
    Map.union (ListEnv b w i -> Map Name (Eval (GenValue b w i))
    forall b w i. ListEnv b w i -> Map Name (Eval (GenValue b w i))
    leStatic ListEnv b w i
    l) (ListEnv b w i -> Map Name (Eval (GenValue b w i))
    forall b w i. ListEnv b w i -> Map Name (Eval (GenValue b w i))
    leStatic ListEnv b w i
    r)
        , leTypes :: TypeEnv
    leTypes  = TypeEnv -> TypeEnv -> TypeEnv
    forall k a. Ord k => Map k a -> Map k a -> Map k a
    Map.union (ListEnv b w i -> TypeEnv
    forall b w i. ListEnv b w i -> TypeEnv
    leTypes ListEnv b w i
    l)  (ListEnv b w i -> TypeEnv
    forall b w i. ListEnv b w i -> TypeEnv
    leTypes ListEnv b w i
    r)
        }

    instance Monoid (ListEnv b w i) where
      mempty :: ListEnv b w i
    mempty = $WListEnv :: forall b w i.
    Map Name (Integer -> Eval (GenValue b w i))
    -> Map Name (Eval (GenValue b w i)) -> TypeEnv -> ListEnv b w i
    ListEnv
        { leVars :: Map Name (Integer -> Eval (GenValue b w i))
    leVars   = Map Name (Integer -> Eval (GenValue b w i))
    forall k a. Map k a
    Map.empty
        , leStatic :: Map Name (Eval (GenValue b w i))
    leStatic = Map Name (Eval (GenValue b w i))
    forall k a. Map k a
    Map.empty
        , leTypes :: TypeEnv
    leTypes  = TypeEnv
    forall k a. Map k a
    Map.empty
        }

      mappend :: ListEnv b w i -> ListEnv b w i -> ListEnv b w i
    mappend l :: ListEnv b w i
    l r :: ListEnv b w i
    r = ListEnv b w i
    l ListEnv b w i -> ListEnv b w i -> ListEnv b w i
    forall a. Semigroup a => a -> a -> a
    <> ListEnv b w i
    r

    toListEnv :: GenEvalEnv b w i -> ListEnv b w i
    toListEnv :: GenEvalEnv b w i -> ListEnv b w i
    toListEnv e :: GenEvalEnv b w i
    e =
      $WListEnv :: forall b w i.
    Map Name (Integer -> Eval (GenValue b w i))
    -> Map Name (Eval (GenValue b w i)) -> TypeEnv -> ListEnv b w i
    ListEnv
      { leVars :: Map Name (Integer -> Eval (GenValue b w i))
    leVars   = Map Name (Integer -> Eval (GenValue b w i))
    forall a. Monoid a => a
    mempty
      , leStatic :: Map Name (Eval (GenValue b w i))
    leStatic = GenEvalEnv b w i -> Map Name (Eval (GenValue b w i))
    forall b w i. GenEvalEnv b w i -> Map Name (Eval (GenValue b w i))
    envVars GenEvalEnv b w i
    e
      , leTypes :: TypeEnv
    leTypes  = GenEvalEnv b w i -> TypeEnv
    forall b w i. GenEvalEnv b w i -> TypeEnv
    envTypes GenEvalEnv b w i
    e
      }

    -- | Evaluate a list environment at a position.
    --   This choses a particular value for the varying
    --   locations.
    evalListEnv :: ListEnv b w i -> Integer -> GenEvalEnv b w i
    evalListEnv :: ListEnv b w i -> Integer -> GenEvalEnv b w i
    evalListEnv (ListEnv vm :: Map Name (Integer -> Eval (GenValue b w i))
    vm st :: Map Name (Eval (GenValue b w i))
    st tm :: TypeEnv
    tm) i :: Integer
    i =
        let v :: Map Name (Eval (GenValue b w i))
    v = ((Integer -> Eval (GenValue b w i)) -> Eval (GenValue b w i))
    -> Map Name (Integer -> Eval (GenValue b w i))
    -> Map Name (Eval (GenValue b w i))
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap ((Integer -> Eval (GenValue b w i))
    -> Integer -> Eval (GenValue b w i)
    forall a b. (a -> b) -> a -> b
    $Integer
    i) Map Name (Integer -> Eval (GenValue b w i))
    vm
         in $WEvalEnv :: forall b w i.
    Map Name (Eval (GenValue b w i)) -> TypeEnv -> GenEvalEnv b w i
    EvalEnv{ envVars :: Map Name (Eval (GenValue b w i))
    envVars = Map Name (Eval (GenValue b w i))
    -> Map Name (Eval (GenValue b w i))
    -> Map Name (Eval (GenValue b w i))
    forall k a. Ord k => Map k a -> Map k a -> Map k a
    Map.union Map Name (Eval (GenValue b w i))
    v Map Name (Eval (GenValue b w i))
    st
                   , envTypes :: TypeEnv
    envTypes = TypeEnv
    tm
                   }

    bindVarList :: Name
                -> (Integer -> Eval (GenValue b w i))
                -> ListEnv b w i
                -> ListEnv b w i
    bindVarList :: Name
    -> (Integer -> Eval (GenValue b w i))
    -> ListEnv b w i
    -> ListEnv b w i
    bindVarList n :: Name
    n vs :: Integer -> Eval (GenValue b w i)
    vs lenv :: ListEnv b w i
    lenv = ListEnv b w i
    lenv { leVars :: Map Name (Integer -> Eval (GenValue b w i))
    leVars = Name
    -> (Integer -> Eval (GenValue b w i))
    -> Map Name (Integer -> Eval (GenValue b w i))
    -> Map Name (Integer -> Eval (GenValue b w i))
    forall k a. Ord k => k -> a -> Map k a -> Map k a
    Map.insert Name
    n Integer -> Eval (GenValue b w i)
    vs (ListEnv b w i -> Map Name (Integer -> Eval (GenValue b w i))
    forall b w i.
    ListEnv b w i -> Map Name (Integer -> Eval (GenValue b w i))
    leVars ListEnv b w i
    lenv) }

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

    -- | Evaluate a comprehension.
    evalComp :: EvalPrims b w i
             => GenEvalEnv b w i -- ^ Starting evaluation environment
             -> Nat'             -- ^ Length of the comprehension
             -> TValue           -- ^ Type of the comprehension elements
             -> Expr             -- ^ Head expression of the comprehension
             -> [[Match]]        -- ^ List of parallel comprehension branches
             -> Eval (GenValue b w i)
    evalComp :: GenEvalEnv b w i
    -> Nat' -> TValue -> Expr -> [[Match]] -> Eval (GenValue b w i)
    evalComp env :: GenEvalEnv b w i
    env len :: Nat'
    len elty :: TValue
    elty body :: Expr
    body ms :: [[Match]]
    ms =
           do ListEnv b w i
    lenv <- [ListEnv b w i] -> ListEnv b w i
    forall a. Monoid a => [a] -> a
    mconcat ([ListEnv b w i] -> ListEnv b w i)
    -> Eval [ListEnv b w i] -> Eval (ListEnv b w i)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> ([Match] -> Eval (ListEnv b w i))
    -> [[Match]] -> Eval [ListEnv b w i]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    mapM (ListEnv b w i -> [Match] -> Eval (ListEnv b w i)
    forall b w i.
    EvalPrims b w i =>
    ListEnv b w i -> [Match] -> Eval (ListEnv b w i)
    branchEnvs (GenEvalEnv b w i -> ListEnv b w i
    forall b w i. GenEvalEnv b w i -> ListEnv b w i
    toListEnv GenEvalEnv b w i
    env)) [[Match]]
    ms
              Nat' -> TValue -> SeqMap b w i -> GenValue b w i
    forall b w i. Nat' -> TValue -> SeqMap b w i -> GenValue b w i
    mkSeq Nat'
    len TValue
    elty (SeqMap b w i -> GenValue b w i)
    -> Eval (SeqMap b w i) -> Eval (GenValue b w i)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> SeqMap b w i -> Eval (SeqMap b w i)
    forall b w i. SeqMap b w i -> Eval (SeqMap b w i)
    memoMap ((Integer -> Eval (GenValue b w i)) -> SeqMap b w i
    forall b w i. (Integer -> Eval (GenValue b w i)) -> SeqMap b w i
    IndexSeqMap ((Integer -> Eval (GenValue b w i)) -> SeqMap b w i)
    -> (Integer -> Eval (GenValue b w i)) -> SeqMap b w i
    forall a b. (a -> b) -> a -> b
    $ \i :: Integer
    i -> do
                  GenEvalEnv b w i -> Expr -> Eval (GenValue b w i)
    forall b w i.
    EvalPrims b w i =>
    GenEvalEnv b w i -> Expr -> Eval (GenValue b w i)
    evalExpr (ListEnv b w i -> Integer -> GenEvalEnv b w i
    forall b w i. ListEnv b w i -> Integer -> GenEvalEnv b w i
    evalListEnv ListEnv b w i
    lenv Integer
    i) Expr
    body)

    -- | Turn a list of matches into the final environments for each iteration of
    -- the branch.
    branchEnvs :: EvalPrims b w i
               => ListEnv b w i
               -> [Match]
               -> Eval (ListEnv b w i)
    branchEnvs :: ListEnv b w i -> [Match] -> Eval (ListEnv b w i)
    branchEnvs env :: ListEnv b w i
    env matches :: [Match]
    matches = (ListEnv b w i -> Match -> Eval (ListEnv b w i))
    -> ListEnv b w i -> [Match] -> Eval (ListEnv b w i)
    forall (t :: * -> *) (m :: * -> *) b a.
    (Foldable t, Monad m) =>
    (b -> a -> m b) -> b -> t a -> m b
    foldM ListEnv b w i -> Match -> Eval (ListEnv b w i)
    forall b w i.
    EvalPrims b w i =>
    ListEnv b w i -> Match -> Eval (ListEnv b w i)
    evalMatch ListEnv b w i
    env [Match]
    matches

    -- | Turn a match into the list of environments it represents.
    evalMatch :: EvalPrims b w i
              => ListEnv b w i
              -> Match
              -> Eval (ListEnv b w i)
    evalMatch :: ListEnv b w i -> Match -> Eval (ListEnv b w i)
    evalMatch lenv :: ListEnv b w i
    lenv m :: Match
    m = case Match
    m of

      -- many envs
      From n :: Name
    n l :: Type
    l _ty :: Type
    _ty expr :: Expr
    expr ->
        case Nat'
    len of
          -- Select from a sequence of finite length.  This causes us to 'stutter'
          -- through our previous choices `nLen` times.
          Nat nLen :: Integer
    nLen -> do
            SeqMap b w i
    vss <- SeqMap b w i -> Eval (SeqMap b w i)
    forall b w i. SeqMap b w i -> Eval (SeqMap b w i)
    memoMap (SeqMap b w i -> Eval (SeqMap b w i))
    -> SeqMap b w i -> Eval (SeqMap b w i)
    forall a b. (a -> b) -> a -> b
    $ (Integer -> Eval (GenValue b w i)) -> SeqMap b w i
    forall b w i. (Integer -> Eval (GenValue b w i)) -> SeqMap b w i
    IndexSeqMap ((Integer -> Eval (GenValue b w i)) -> SeqMap b w i)
    -> (Integer -> Eval (GenValue b w i)) -> SeqMap b w i
    forall a b. (a -> b) -> a -> b
    $ \i :: Integer
    i -> GenEvalEnv b w i -> Expr -> Eval (GenValue b w i)
    forall b w i.
    EvalPrims b w i =>
    GenEvalEnv b w i -> Expr -> Eval (GenValue b w i)
    evalExpr (ListEnv b w i -> Integer -> GenEvalEnv b w i
    forall b w i. ListEnv b w i -> Integer -> GenEvalEnv b w i
    evalListEnv ListEnv b w i
    lenv Integer
    i) Expr
    expr
            let stutter :: (Integer -> t) -> Integer -> t
    stutter xs :: Integer -> t
    xs = \i :: Integer
    i -> Integer -> t
    xs (Integer
    i Integer -> Integer -> Integer
    forall a. Integral a => a -> a -> a
    `div` Integer
    nLen)
            let lenv' :: ListEnv b w i
    lenv' = ListEnv b w i
    lenv { leVars :: Map Name (Integer -> Eval (GenValue b w i))
    leVars = ((Integer -> Eval (GenValue b w i))
     -> Integer -> Eval (GenValue b w i))
    -> Map Name (Integer -> Eval (GenValue b w i))
    -> Map Name (Integer -> Eval (GenValue b w i))
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (Integer -> Eval (GenValue b w i))
    -> Integer -> Eval (GenValue b w i)
    forall t. (Integer -> t) -> Integer -> t
    stutter (ListEnv b w i -> Map Name (Integer -> Eval (GenValue b w i))
    forall b w i.
    ListEnv b w i -> Map Name (Integer -> Eval (GenValue b w i))
    leVars ListEnv b w i
    lenv) }
            let vs :: Integer -> Eval (GenValue b w i)
    vs i :: Integer
    i = do let (q :: Integer
    q, r :: Integer
    r) = Integer
    i Integer -> Integer -> (Integer, Integer)
    forall a. Integral a => a -> a -> (a, a)
    `divMod` Integer
    nLen
                          SeqMap b w i -> Integer -> Eval (GenValue b w i)
    forall b w i. SeqMap b w i -> Integer -> Eval (GenValue b w i)
    lookupSeqMap SeqMap b w i
    vss Integer
    q Eval (GenValue b w i)
    -> (GenValue b w i -> Eval (GenValue b w i))
    -> Eval (GenValue b w i)
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \case
                            VWord _ w :: Eval (WordValue b w i)
    w   -> b -> GenValue b w i
    forall b w i. b -> GenValue b w i
    VBit (b -> GenValue b w i) -> Eval b -> Eval (GenValue b w i)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> ((WordValue b w i -> Integer -> Eval b)
    -> Integer -> WordValue b w i -> Eval b
    forall a b c. (a -> b -> c) -> b -> a -> c
    flip WordValue b w i -> Integer -> Eval b
    forall b w i. BitWord b w i => WordValue b w i -> Integer -> Eval b
    indexWordValue Integer
    r (WordValue b w i -> Eval b) -> Eval (WordValue b w i) -> Eval b
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< Eval (WordValue b w i)
    w)
                            VSeq _ xs' :: SeqMap b w i
    xs'  -> SeqMap b w i -> Integer -> Eval (GenValue b w i)
    forall b w i. SeqMap b w i -> Integer -> Eval (GenValue b w i)
    lookupSeqMap SeqMap b w i
    xs' Integer
    r
                            VStream xs' :: SeqMap b w i
    xs' -> SeqMap b w i -> Integer -> Eval (GenValue b w i)
    forall b w i. SeqMap b w i -> Integer -> Eval (GenValue b w i)
    lookupSeqMap SeqMap b w i
    xs' Integer
    r
                            _           -> String -> [String] -> Eval (GenValue b w i)
    forall a. HasCallStack => String -> [String] -> a
    evalPanic "evalMatch" ["Not a list value"]
            ListEnv b w i -> Eval (ListEnv b w i)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (ListEnv b w i -> Eval (ListEnv b w i))
    -> ListEnv b w i -> Eval (ListEnv b w i)
    forall a b. (a -> b) -> a -> b
    $ Name
    -> (Integer -> Eval (GenValue b w i))
    -> ListEnv b w i
    -> ListEnv b w i
    forall b w i.
    Name
    -> (Integer -> Eval (GenValue b w i))
    -> ListEnv b w i
    -> ListEnv b w i
    bindVarList Name
    n Integer -> Eval (GenValue b w i)
    vs ListEnv b w i
    lenv'

          -- Select from a sequence of infinite length.  Note that this means we
          -- will never need to backtrack into previous branches.  Thus, we can convert
          -- `leVars` elements of the comprehension environment into `leStatic` elements
          -- by selecting out the 0th element.
          Inf -> do
            let allvars :: Map Name (Eval (GenValue b w i))
    allvars = Map Name (Eval (GenValue b w i))
    -> Map Name (Eval (GenValue b w i))
    -> Map Name (Eval (GenValue b w i))
    forall k a. Ord k => Map k a -> Map k a -> Map k a
    Map.union (((Integer -> Eval (GenValue b w i)) -> Eval (GenValue b w i))
    -> Map Name (Integer -> Eval (GenValue b w i))
    -> Map Name (Eval (GenValue b w i))
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap ((Integer -> Eval (GenValue b w i))
    -> Integer -> Eval (GenValue b w i)
    forall a b. (a -> b) -> a -> b
    $0) (ListEnv b w i -> Map Name (Integer -> Eval (GenValue b w i))
    forall b w i.
    ListEnv b w i -> Map Name (Integer -> Eval (GenValue b w i))
    leVars ListEnv b w i
    lenv)) (ListEnv b w i -> Map Name (Eval (GenValue b w i))
    forall b w i. ListEnv b w i -> Map Name (Eval (GenValue b w i))
    leStatic ListEnv b w i
    lenv)
            let lenv' :: ListEnv b w i
    lenv' = ListEnv b w i
    lenv { leVars :: Map Name (Integer -> Eval (GenValue b w i))
    leVars   = Map Name (Integer -> Eval (GenValue b w i))
    forall k a. Map k a
    Map.empty
                             , leStatic :: Map Name (Eval (GenValue b w i))
    leStatic = Map Name (Eval (GenValue b w i))
    allvars
                             }
            let env :: GenEvalEnv b w i
    env   = Map Name (Eval (GenValue b w i)) -> TypeEnv -> GenEvalEnv b w i
    forall b w i.
    Map Name (Eval (GenValue b w i)) -> TypeEnv -> GenEvalEnv b w i
    EvalEnv Map Name (Eval (GenValue b w i))
    allvars (ListEnv b w i -> TypeEnv
    forall b w i. ListEnv b w i -> TypeEnv
    leTypes ListEnv b w i
    lenv)
            GenValue b w i
    xs <- GenEvalEnv b w i -> Expr -> Eval (GenValue b w i)
    forall b w i.
    EvalPrims b w i =>
    GenEvalEnv b w i -> Expr -> Eval (GenValue b w i)
    evalExpr GenEvalEnv b w i
    env Expr
    expr
            let vs :: Integer -> Eval (GenValue b w i)
    vs i :: Integer
    i = case GenValue b w i
    xs of
                         VWord _ w :: Eval (WordValue b w i)
    w   -> b -> GenValue b w i
    forall b w i. b -> GenValue b w i
    VBit (b -> GenValue b w i) -> Eval b -> Eval (GenValue b w i)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> ((WordValue b w i -> Integer -> Eval b)
    -> Integer -> WordValue b w i -> Eval b
    forall a b c. (a -> b -> c) -> b -> a -> c
    flip WordValue b w i -> Integer -> Eval b
    forall b w i. BitWord b w i => WordValue b w i -> Integer -> Eval b
    indexWordValue Integer
    i (WordValue b w i -> Eval b) -> Eval (WordValue b w i) -> Eval b
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< Eval (WordValue b w i)
    w)
                         VSeq _ xs' :: SeqMap b w i
    xs'  -> SeqMap b w i -> Integer -> Eval (GenValue b w i)
    forall b w i. SeqMap b w i -> Integer -> Eval (GenValue b w i)
    lookupSeqMap SeqMap b w i
    xs' Integer
    i
                         VStream xs' :: SeqMap b w i
    xs' -> SeqMap b w i -> Integer -> Eval (GenValue b w i)
    forall b w i. SeqMap b w i -> Integer -> Eval (GenValue b w i)
    lookupSeqMap SeqMap b w i
    xs' Integer
    i
                         _           -> String -> [String] -> Eval (GenValue b w i)
    forall a. HasCallStack => String -> [String] -> a
    evalPanic "evalMatch" ["Not a list value"]
            ListEnv b w i -> Eval (ListEnv b w i)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (ListEnv b w i -> Eval (ListEnv b w i))
    -> ListEnv b w i -> Eval (ListEnv b w i)
    forall a b. (a -> b) -> a -> b
    $ Name
    -> (Integer -> Eval (GenValue b w i))
    -> ListEnv b w i
    -> ListEnv b w i
    forall b w i.
    Name
    -> (Integer -> Eval (GenValue b w i))
    -> ListEnv b w i
    -> ListEnv b w i
    bindVarList Name
    n Integer -> Eval (GenValue b w i)
    vs ListEnv b w i
    lenv'

        where
          len :: Nat'
    len  = HasCallStack => TypeEnv -> Type -> Nat'
    TypeEnv -> Type -> Nat'
    evalNumType (ListEnv b w i -> TypeEnv
    forall b w i. ListEnv b w i -> TypeEnv
    leTypes ListEnv b w i
    lenv) Type
    l

      -- 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 :: Decl
    d -> ListEnv b w i -> Eval (ListEnv b w i)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (ListEnv b w i -> Eval (ListEnv b w i))
    -> ListEnv b w i -> Eval (ListEnv b w i)
    forall a b. (a -> b) -> a -> b
    $ Name
    -> (Integer -> Eval (GenValue b w i))
    -> ListEnv b w i
    -> ListEnv b w i
    forall b w i.
    Name
    -> (Integer -> Eval (GenValue b w i))
    -> ListEnv b w i
    -> ListEnv b w i
    bindVarList (Decl -> Name
    dName Decl
    d) (\i :: Integer
    i -> GenEvalEnv b w i -> Eval (GenValue b w i)
    forall b w i.
    EvalPrims b w i =>
    GenEvalEnv b w i -> Eval (GenValue b w i)
    f (ListEnv b w i -> Integer -> GenEvalEnv b w i
    forall b w i. ListEnv b w i -> Integer -> GenEvalEnv b w i
    evalListEnv ListEnv b w i
    lenv Integer
    i)) ListEnv b w i
    lenv
        where
          f :: GenEvalEnv b w i -> Eval (GenValue b w i)
    f env :: GenEvalEnv b w i
    env =
              case Decl -> DeclDef
    dDefinition Decl
    d of
                DPrim   -> String -> [String] -> Eval (GenValue b w i)
    forall a. HasCallStack => String -> [String] -> a
    evalPanic "evalMatch" ["Unexpected local primitive"]
                DExpr e :: Expr
    e -> GenEvalEnv b w i -> Expr -> Eval (GenValue b w i)
    forall b w i.
    EvalPrims b w i =>
    GenEvalEnv b w i -> Expr -> Eval (GenValue b w i)
    evalExpr GenEvalEnv b w i
    env Expr
    e