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

    {-# LANGUAGE ConstraintKinds #-}
    {-# LANGUAGE DoAndIfThenElse #-}
    {-# LANGUAGE ImplicitParams #-}
    {-# LANGUAGE LambdaCase #-}
    {-# LANGUAGE MultiParamTypeClasses #-}
    {-# LANGUAGE ParallelListComp #-}
    {-# LANGUAGE ScopedTypeVariables #-}
    {-# LANGUAGE PatternGuards #-}
    {-# LANGUAGE ViewPatterns #-}
    {-# LANGUAGE NamedFieldPuns #-}

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

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

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

    import           Control.Monad
    import           Data.List
    import           Data.Maybe
    import qualified Data.IntMap.Strict as IntMap
    import qualified Data.Map.Strict as Map
    import           Data.Semigroup
    import           Control.Applicative

    import Prelude ()
    import Prelude.Compat

    type EvalEnv = GenEvalEnv Concrete

    type EvalPrims sym =
      ( Backend sym, ?callStacks :: Bool, ?evalPrim :: PrimIdent -> Maybe (Either Expr (Prim sym)) )

    type ConcPrims =
      (?callStacks :: Bool, ?evalPrim :: PrimIdent -> Maybe (Either Expr (Prim Concrete)))

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

    {-# SPECIALIZE moduleEnv ::
      ConcPrims =>
      Concrete ->
      Module ->
      GenEvalEnv Concrete ->
      SEval Concrete (GenEvalEnv Concrete)
      #-}

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

    {-# SPECIALIZE evalExpr ::
      (?range :: Range, ConcPrims) =>
      Concrete ->
      GenEvalEnv Concrete ->
      Expr ->
      SEval Concrete (GenValue Concrete)
      #-}

    -- | 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 ::
      (?range :: Range, EvalPrims sym) =>
      sym ->
      GenEvalEnv sym  {- ^ Evaluation environment -} ->
      Expr          {- ^ Expression to evaluate -} ->
      SEval sym (GenValue sym)
    evalExpr :: forall sym.
    (?range::Range, EvalPrims sym) =>
    sym -> GenEvalEnv sym -> Expr -> SEval sym (GenValue sym)
    evalExpr sym
    sym GenEvalEnv sym
    env Expr
    expr = case Expr
    expr of

      ELocated Range
    r Expr
    e ->
        let ?range = ?range::Range
    Range
    r in
        sym -> GenEvalEnv sym -> Expr -> SEval sym (GenValue sym)
    forall sym.
    (?range::Range, EvalPrims sym) =>
    sym -> GenEvalEnv sym -> Expr -> SEval sym (GenValue sym)
    evalExpr sym
    sym GenEvalEnv sym
    env Expr
    e

      -- Try to detect when the user has directly written a finite sequence of
      -- literal bit values and pack these into a word.
      EList [Expr]
    es 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" #-}
            Integer -> WordValue sym -> GenValue sym
    forall sym. Integer -> WordValue sym -> GenValue sym
    VWord Integer
    len (WordValue sym -> GenValue sym)
    -> SEval sym (WordValue sym) -> SEval sym (GenValue sym)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$>
              (sym -> [SEval sym (GenValue sym)] -> SEval sym (Maybe (SWord sym))
    forall sym.
    Backend sym =>
    sym -> [SEval sym (GenValue sym)] -> SEval sym (Maybe (SWord sym))
    tryFromBits sym
    sym [SEval sym (GenValue sym)]
    vs SEval sym (Maybe (SWord sym))
    -> (Maybe (SWord sym) -> SEval sym (WordValue sym))
    -> SEval sym (WordValue sym)
    forall a b. SEval sym a -> (a -> SEval sym b) -> SEval sym b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \case
                 Just SWord sym
    w  -> WordValue sym -> SEval sym (WordValue sym)
    forall a. a -> SEval sym a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (SWord sym -> WordValue sym
    forall sym. SWord sym -> WordValue sym
    wordVal SWord sym
    w)
                 Maybe (SWord sym)
    Nothing -> do [SEval sym (SBit sym)]
    xs <- (SEval sym (GenValue sym) -> SEval sym (SEval sym (SBit sym)))
    -> [SEval sym (GenValue sym)] -> SEval sym [SEval sym (SBit sym)]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
    mapM (\SEval sym (GenValue sym)
    x -> sym -> SEval sym (SBit sym) -> SEval sym (SEval sym (SBit sym))
    forall sym a.
    Backend sym =>
    sym -> SEval sym a -> SEval sym (SEval sym a)
    sDelay sym
    sym (GenValue sym -> SBit sym
    forall sym. GenValue sym -> SBit sym
    fromVBit (GenValue sym -> SBit sym)
    -> SEval sym (GenValue sym) -> SEval sym (SBit sym)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> SEval sym (GenValue sym)
    x)) [SEval sym (GenValue sym)]
    vs
                               sym
    -> Integer -> SeqMap sym (SBit sym) -> SEval sym (WordValue sym)
    forall sym.
    Backend sym =>
    sym
    -> Integer -> SeqMap sym (SBit sym) -> SEval sym (WordValue sym)
    bitmapWordVal sym
    sym Integer
    len (SeqMap sym (SBit sym) -> SEval sym (WordValue sym))
    -> SeqMap sym (SBit sym) -> SEval sym (WordValue sym)
    forall a b. (a -> b) -> a -> b
    $ sym -> [SEval sym (SBit sym)] -> SeqMap sym (SBit sym)
    forall sym a. Backend sym => sym -> [SEval sym a] -> SeqMap sym a
    finiteSeqMap sym
    sym [SEval sym (SBit sym)]
    xs)
        | Bool
    otherwise -> {-# SCC "evalExpr->EList" #-} do
            [SEval sym (GenValue sym)]
    xs <- (SEval sym (GenValue sym) -> SEval sym (SEval sym (GenValue sym)))
    -> [SEval sym (GenValue sym)]
    -> SEval sym [SEval sym (GenValue sym)]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
    mapM (sym
    -> SEval sym (GenValue sym) -> SEval sym (SEval sym (GenValue sym))
    forall sym a.
    Backend sym =>
    sym -> SEval sym a -> SEval sym (SEval sym a)
    sDelay sym
    sym) [SEval sym (GenValue sym)]
    vs
            GenValue sym -> SEval sym (GenValue sym)
    forall a. a -> SEval sym a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (GenValue sym -> SEval sym (GenValue sym))
    -> GenValue sym -> SEval sym (GenValue sym)
    forall a b. (a -> b) -> a -> b
    $ Integer -> SeqMap sym (GenValue sym) -> GenValue sym
    forall sym. Integer -> SeqMap sym (GenValue sym) -> GenValue sym
    VSeq Integer
    len (SeqMap sym (GenValue sym) -> GenValue sym)
    -> SeqMap sym (GenValue sym) -> GenValue sym
    forall a b. (a -> b) -> a -> b
    $ sym -> [SEval sym (GenValue sym)] -> SeqMap sym (GenValue sym)
    forall sym a. Backend sym => sym -> [SEval sym a] -> SeqMap sym a
    finiteSeqMap sym
    sym [SEval sym (GenValue sym)]
    xs
       where
        tyv :: TValue
    tyv = TypeEnv -> Type -> TValue
    evalValType (GenEvalEnv sym -> TypeEnv
    forall sym. GenEvalEnv sym -> TypeEnv
    envTypes GenEvalEnv sym
    env) Type
    ty
        vs :: [SEval sym (GenValue sym)]
    vs  = (Expr -> SEval sym (GenValue sym))
    -> [Expr] -> [SEval sym (GenValue sym)]
    forall a b. (a -> b) -> [a] -> [b]
    map Expr -> SEval sym (GenValue sym)
    eval [Expr]
    es
        len :: Integer
    len = [Expr] -> Integer
    forall i a. Num i => [a] -> i
    genericLength [Expr]
    es

      ETuple [Expr]
    es -> {-# SCC "evalExpr->ETuple" #-} do
         [SEval sym (GenValue sym)]
    xs <- (Expr -> SEval sym (SEval sym (GenValue sym)))
    -> [Expr] -> SEval sym [SEval sym (GenValue sym)]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
    mapM (sym
    -> SEval sym (GenValue sym) -> SEval sym (SEval sym (GenValue sym))
    forall sym a.
    Backend sym =>
    sym -> SEval sym a -> SEval sym (SEval sym a)
    sDelay sym
    sym (SEval sym (GenValue sym) -> SEval sym (SEval sym (GenValue sym)))
    -> (Expr -> SEval sym (GenValue sym))
    -> Expr
    -> SEval sym (SEval sym (GenValue sym))
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Expr -> SEval sym (GenValue sym)
    eval) [Expr]
    es
         GenValue sym -> SEval sym (GenValue sym)
    forall a. a -> SEval sym a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (GenValue sym -> SEval sym (GenValue sym))
    -> GenValue sym -> SEval sym (GenValue sym)
    forall a b. (a -> b) -> a -> b
    $ [SEval sym (GenValue sym)] -> GenValue sym
    forall sym. [SEval sym (GenValue sym)] -> GenValue sym
    VTuple [SEval sym (GenValue sym)]
    xs

      ERec RecordMap Ident Expr
    fields -> {-# SCC "evalExpr->ERec" #-} do
         RecordMap Ident (SEval sym (GenValue sym))
    xs <- (Expr -> SEval sym (SEval sym (GenValue sym)))
    -> RecordMap Ident Expr
    -> SEval sym (RecordMap Ident (SEval sym (GenValue sym)))
    forall (t :: * -> *) (f :: * -> *) a b.
    (Traversable t, Applicative f) =>
    (a -> f b) -> t a -> f (t b)
    forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> RecordMap Ident a -> f (RecordMap Ident b)
    traverse (sym
    -> SEval sym (GenValue sym) -> SEval sym (SEval sym (GenValue sym))
    forall sym a.
    Backend sym =>
    sym -> SEval sym a -> SEval sym (SEval sym a)
    sDelay sym
    sym (SEval sym (GenValue sym) -> SEval sym (SEval sym (GenValue sym)))
    -> (Expr -> SEval sym (GenValue sym))
    -> Expr
    -> SEval sym (SEval sym (GenValue sym))
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Expr -> SEval sym (GenValue sym)
    eval) RecordMap Ident Expr
    fields
         GenValue sym -> SEval sym (GenValue sym)
    forall a. a -> SEval sym a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (GenValue sym -> SEval sym (GenValue sym))
    -> GenValue sym -> SEval sym (GenValue sym)
    forall a b. (a -> b) -> a -> b
    $ RecordMap Ident (SEval sym (GenValue sym)) -> GenValue sym
    forall sym.
    RecordMap Ident (SEval sym (GenValue sym)) -> GenValue sym
    VRecord RecordMap Ident (SEval sym (GenValue sym))
    xs

      ESel Expr
    e Selector
    sel -> {-# SCC "evalExpr->ESel" #-} do
         GenValue sym
    e' <- Expr -> SEval sym (GenValue sym)
    eval Expr
    e
         sym -> GenValue sym -> Selector -> SEval sym (GenValue sym)
    forall sym.
    Backend sym =>
    sym -> GenValue sym -> Selector -> SEval sym (GenValue sym)
    evalSel sym
    sym GenValue sym
    e' Selector
    sel

      ESet Type
    ty Expr
    e Selector
    sel Expr
    v -> {-# SCC "evalExpr->ESet" #-}
        do GenValue sym
    e' <- Expr -> SEval sym (GenValue sym)
    eval Expr
    e
           let tyv :: TValue
    tyv = TypeEnv -> Type -> TValue
    evalValType (GenEvalEnv sym -> TypeEnv
    forall sym. GenEvalEnv sym -> TypeEnv
    envTypes GenEvalEnv sym
    env) Type
    ty
           sym
    -> TValue
    -> GenValue sym
    -> Selector
    -> SEval sym (GenValue sym)
    -> SEval sym (GenValue sym)
    forall sym.
    Backend sym =>
    sym
    -> TValue
    -> GenValue sym
    -> Selector
    -> SEval sym (GenValue sym)
    -> SEval sym (GenValue sym)
    evalSetSel sym
    sym TValue
    tyv GenValue sym
    e' Selector
    sel (Expr -> SEval sym (GenValue sym)
    eval Expr
    v)

      EIf Expr
    c Expr
    t Expr
    f -> {-# SCC "evalExpr->EIf" #-} do
         SBit sym
    b <- GenValue sym -> SBit sym
    forall sym. GenValue sym -> SBit sym
    fromVBit (GenValue sym -> SBit sym)
    -> SEval sym (GenValue sym) -> SEval sym (SBit sym)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Expr -> SEval sym (GenValue sym)
    eval Expr
    c
         sym
    -> SBit sym
    -> SEval sym (GenValue sym)
    -> SEval sym (GenValue sym)
    -> SEval sym (GenValue sym)
    forall sym.
    Backend sym =>
    sym
    -> SBit sym
    -> SEval sym (GenValue sym)
    -> SEval sym (GenValue sym)
    -> SEval sym (GenValue sym)
    iteValue sym
    sym SBit sym
    b (Expr -> SEval sym (GenValue sym)
    eval Expr
    t) (Expr -> SEval sym (GenValue sym)
    eval Expr
    f)

      EComp Type
    n Type
    t Expr
    h [[Match]]
    gs -> {-# SCC "evalExpr->EComp" #-} do
          let len :: Nat'
    len  = TypeEnv -> Type -> Nat'
    evalNumType (GenEvalEnv sym -> TypeEnv
    forall sym. GenEvalEnv sym -> TypeEnv
    envTypes GenEvalEnv sym
    env) Type
    n
          let elty :: TValue
    elty = TypeEnv -> Type -> TValue
    evalValType (GenEvalEnv sym -> TypeEnv
    forall sym. GenEvalEnv sym -> TypeEnv
    envTypes GenEvalEnv sym
    env) Type
    t
          sym
    -> GenEvalEnv sym
    -> Nat'
    -> TValue
    -> Expr
    -> [[Match]]
    -> SEval sym (GenValue sym)
    forall sym.
    (?range::Range, EvalPrims sym) =>
    sym
    -> GenEvalEnv sym
    -> Nat'
    -> TValue
    -> Expr
    -> [[Match]]
    -> SEval sym (GenValue sym)
    evalComp sym
    sym GenEvalEnv sym
    env Nat'
    len TValue
    elty Expr
    h [[Match]]
    gs

      EVar Name
    n -> {-# SCC "evalExpr->EVar" #-} do
        case Name
    -> GenEvalEnv sym
    -> Maybe (Either (Prim sym) (SEval sym (GenValue sym)))
    forall sym.
    Name
    -> GenEvalEnv sym
    -> Maybe (Either (Prim sym) (SEval sym (GenValue sym)))
    lookupVar Name
    n GenEvalEnv sym
    env of
          Just (Left Prim sym
    p)
            | ?callStacks::Bool
    Bool
    ?callStacks -> sym
    -> Name
    -> Range
    -> SEval sym (GenValue sym)
    -> SEval sym (GenValue sym)
    forall a. sym -> Name -> Range -> SEval sym a -> SEval sym a
    forall sym a.
    Backend sym =>
    sym -> Name -> Range -> SEval sym a -> SEval sym a
    sPushFrame sym
    sym Name
    n ?range::Range
    Range
    ?range (sym -> GenValue sym -> SEval sym (GenValue sym)
    forall sym.
    Backend sym =>
    sym -> GenValue sym -> SEval sym (GenValue sym)
    cacheCallStack sym
    sym (GenValue sym -> SEval sym (GenValue sym))
    -> SEval sym (GenValue sym) -> SEval sym (GenValue sym)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< sym -> Name -> Prim sym -> SEval sym (GenValue sym)
    forall sym.
    Backend sym =>
    sym -> Name -> Prim sym -> SEval sym (GenValue sym)
    evalPrim sym
    sym Name
    n Prim sym
    p)
            | Bool
    otherwise   -> sym -> Name -> Prim sym -> SEval sym (GenValue sym)
    forall sym.
    Backend sym =>
    sym -> Name -> Prim sym -> SEval sym (GenValue sym)
    evalPrim sym
    sym Name
    n Prim sym
    p
          Just (Right SEval sym (GenValue sym)
    val)
            | ?callStacks::Bool
    Bool
    ?callStacks ->
                case Name -> NameInfo
    nameInfo Name
    n of
                  GlobalName {} ->
                     sym
    -> Name
    -> Range
    -> SEval sym (GenValue sym)
    -> SEval sym (GenValue sym)
    forall a. sym -> Name -> Range -> SEval sym a -> SEval sym a
    forall sym a.
    Backend sym =>
    sym -> Name -> Range -> SEval sym a -> SEval sym a
    sPushFrame sym
    sym Name
    n ?range::Range
    Range
    ?range (sym -> GenValue sym -> SEval sym (GenValue sym)
    forall sym.
    Backend sym =>
    sym -> GenValue sym -> SEval sym (GenValue sym)
    cacheCallStack sym
    sym (GenValue sym -> SEval sym (GenValue sym))
    -> SEval sym (GenValue sym) -> SEval sym (GenValue sym)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< SEval sym (GenValue sym)
    val)
                  LocalName {} -> sym -> GenValue sym -> SEval sym (GenValue sym)
    forall sym.
    Backend sym =>
    sym -> GenValue sym -> SEval sym (GenValue sym)
    cacheCallStack sym
    sym (GenValue sym -> SEval sym (GenValue sym))
    -> SEval sym (GenValue sym) -> SEval sym (GenValue sym)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< SEval sym (GenValue sym)
    val
            | Bool
    otherwise -> SEval sym (GenValue sym)
    val
          Maybe (Either (Prim sym) (SEval sym (GenValue sym)))
    Nothing  -> do
            Doc
    envdoc <- sym -> PPOpts -> GenEvalEnv sym -> SEval sym Doc
    forall sym.
    Backend sym =>
    sym -> PPOpts -> GenEvalEnv sym -> SEval sym Doc
    ppEnv sym
    sym PPOpts
    defaultPPOpts GenEvalEnv sym
    env
            String -> [String] -> SEval sym (GenValue sym)
    forall a. HasCallStack => String -> [String] -> a
    panic String
    "[Eval] evalExpr"
                         [String
    "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]
    ++ String
    "` (" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Int -> String
    forall a. Show a => a -> String
    show (Name -> Int
    nameUnique Name
    n) String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ") is not defined"
                         , Doc -> String
    forall a. Show a => a -> String
    show Doc
    envdoc
                         ]

      ETAbs TParam
    tv Expr
    b -> {-# SCC "evalExpr->ETAbs" #-}
        case TParam -> Kind
    tpKind TParam
    tv of
          Kind
    KType -> sym
    -> (TValue -> SEval sym (GenValue sym)) -> SEval sym (GenValue sym)
    forall sym.
    Backend sym =>
    sym
    -> (TValue -> SEval sym (GenValue sym)) -> SEval sym (GenValue sym)
    tlam sym
    sym ((TValue -> SEval sym (GenValue sym)) -> SEval sym (GenValue sym))
    -> (TValue -> SEval sym (GenValue sym)) -> SEval sym (GenValue sym)
    forall a b. (a -> b) -> a -> b
    $ \TValue
    ty -> sym -> GenEvalEnv sym -> Expr -> SEval sym (GenValue sym)
    forall sym.
    (?range::Range, EvalPrims sym) =>
    sym -> GenEvalEnv sym -> Expr -> SEval sym (GenValue sym)
    evalExpr sym
    sym (TVar -> Either Nat' TValue -> GenEvalEnv sym -> GenEvalEnv sym
    forall sym.
    TVar -> Either Nat' TValue -> GenEvalEnv sym -> GenEvalEnv sym
    bindType (TParam -> TVar
    tpVar TParam
    tv) (TValue -> Either Nat' TValue
    forall a b. b -> Either a b
    Right TValue
    ty) GenEvalEnv sym
    env) Expr
    b
          Kind
    KNum  -> sym
    -> (Nat' -> SEval sym (GenValue sym)) -> SEval sym (GenValue sym)
    forall sym.
    Backend sym =>
    sym
    -> (Nat' -> SEval sym (GenValue sym)) -> SEval sym (GenValue sym)
    nlam sym
    sym ((Nat' -> SEval sym (GenValue sym)) -> SEval sym (GenValue sym))
    -> (Nat' -> SEval sym (GenValue sym)) -> SEval sym (GenValue sym)
    forall a b. (a -> b) -> a -> b
    $ \Nat'
    n  -> sym -> GenEvalEnv sym -> Expr -> SEval sym (GenValue sym)
    forall sym.
    (?range::Range, EvalPrims sym) =>
    sym -> GenEvalEnv sym -> Expr -> SEval sym (GenValue sym)
    evalExpr sym
    sym (TVar -> Either Nat' TValue -> GenEvalEnv sym -> GenEvalEnv sym
    forall sym.
    TVar -> Either Nat' TValue -> GenEvalEnv sym -> GenEvalEnv sym
    bindType (TParam -> TVar
    tpVar TParam
    tv) (Nat' -> Either Nat' TValue
    forall a b. a -> Either a b
    Left Nat'
    n) GenEvalEnv sym
    env) Expr
    b
          Kind
    k     -> String -> [String] -> SEval sym (GenValue sym)
    forall a. HasCallStack => String -> [String] -> a
    panic String
    "[Eval] evalExpr" [String
    "invalid kind on type abstraction", Kind -> String
    forall a. Show a => a -> String
    show Kind
    k]

      ETApp Expr
    e Type
    ty -> {-# SCC "evalExpr->ETApp" #-} do
        Expr -> SEval sym (GenValue sym)
    eval Expr
    e SEval sym (GenValue sym)
    -> (GenValue sym -> SEval sym (GenValue sym))
    -> SEval sym (GenValue sym)
    forall a b. SEval sym a -> (a -> SEval sym b) -> SEval sym b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \case
          f :: GenValue sym
    f@VPoly{}    -> sym -> GenValue sym -> TValue -> SEval sym (GenValue sym)
    forall sym.
    Backend sym =>
    sym -> GenValue sym -> TValue -> SEval sym (GenValue sym)
    fromVPoly sym
    sym GenValue sym
    f    (TValue -> SEval sym (GenValue sym))
    -> TValue -> SEval sym (GenValue sym)
    forall a b. (a -> b) -> a -> b
    $! (TypeEnv -> Type -> TValue
    evalValType (GenEvalEnv sym -> TypeEnv
    forall sym. GenEvalEnv sym -> TypeEnv
    envTypes GenEvalEnv sym
    env) Type
    ty)
          f :: GenValue sym
    f@VNumPoly{} -> sym -> GenValue sym -> Nat' -> SEval sym (GenValue sym)
    forall sym.
    Backend sym =>
    sym -> GenValue sym -> Nat' -> SEval sym (GenValue sym)
    fromVNumPoly sym
    sym GenValue sym
    f (Nat' -> SEval sym (GenValue sym))
    -> Nat' -> SEval sym (GenValue sym)
    forall a b. (a -> b) -> a -> b
    $! (TypeEnv -> Type -> Nat'
    evalNumType (GenEvalEnv sym -> TypeEnv
    forall sym. GenEvalEnv sym -> TypeEnv
    envTypes GenEvalEnv sym
    env) Type
    ty)
          GenValue sym
    val     -> do Doc
    vdoc <- GenValue sym -> SEval sym Doc
    ppV GenValue sym
    val
                        String -> [String] -> SEval sym (GenValue sym)
    forall a. HasCallStack => String -> [String] -> a
    panic String
    "[Eval] evalExpr"
                          [String
    "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 Expr
    f Expr
    v -> {-# SCC "evalExpr->EApp" #-} do
        Expr -> SEval sym (GenValue sym)
    eval Expr
    f SEval sym (GenValue sym)
    -> (GenValue sym -> SEval sym (GenValue sym))
    -> SEval sym (GenValue sym)
    forall a b. SEval sym a -> (a -> SEval sym b) -> SEval sym b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \case
          f' :: GenValue sym
    f'@VFun {} -> sym
    -> GenValue sym
    -> SEval sym (GenValue sym)
    -> SEval sym (GenValue sym)
    forall sym.
    Backend sym =>
    sym
    -> GenValue sym
    -> SEval sym (GenValue sym)
    -> SEval sym (GenValue sym)
    fromVFun sym
    sym GenValue sym
    f' (Expr -> SEval sym (GenValue sym)
    eval Expr
    v)
          GenValue sym
    it         -> do Doc
    itdoc <- GenValue sym -> SEval sym Doc
    ppV GenValue sym
    it
                           String -> [String] -> SEval sym (GenValue sym)
    forall a. HasCallStack => String -> [String] -> a
    panic String
    "[Eval] evalExpr" [String
    "not a function", Doc -> String
    forall a. Show a => a -> String
    show Doc
    itdoc ]

      EAbs Name
    n Type
    _ty Expr
    b -> {-# SCC "evalExpr->EAbs" #-}
        sym
    -> (SEval sym (GenValue sym) -> SEval sym (GenValue sym))
    -> SEval sym (GenValue sym)
    forall sym.
    Backend sym =>
    sym
    -> (SEval sym (GenValue sym) -> SEval sym (GenValue sym))
    -> SEval sym (GenValue sym)
    lam sym
    sym (\SEval sym (GenValue sym)
    v -> do GenEvalEnv sym
    env' <- sym
    -> Name
    -> SEval sym (GenValue sym)
    -> GenEvalEnv sym
    -> SEval sym (GenEvalEnv sym)
    forall sym.
    Backend sym =>
    sym
    -> Name
    -> SEval sym (GenValue sym)
    -> GenEvalEnv sym
    -> SEval sym (GenEvalEnv sym)
    bindVar sym
    sym Name
    n SEval sym (GenValue sym)
    v GenEvalEnv sym
    env
                          sym -> GenEvalEnv sym -> Expr -> SEval sym (GenValue sym)
    forall sym.
    (?range::Range, EvalPrims sym) =>
    sym -> GenEvalEnv sym -> Expr -> SEval sym (GenValue sym)
    evalExpr sym
    sym GenEvalEnv sym
    env' Expr
    b)

      -- XXX these will likely change once there is an evidence value
      EProofAbs Type
    _ Expr
    e -> Expr -> SEval sym (GenValue sym)
    eval Expr
    e
      EProofApp Expr
    e   -> Expr -> SEval sym (GenValue sym)
    eval Expr
    e

      EWhere Expr
    e [DeclGroup]
    ds -> {-# SCC "evalExpr->EWhere" #-} do
         GenEvalEnv sym
    env' <- sym -> [DeclGroup] -> GenEvalEnv sym -> SEval sym (GenEvalEnv sym)
    forall sym.
    EvalPrims sym =>
    sym -> [DeclGroup] -> GenEvalEnv sym -> SEval sym (GenEvalEnv sym)
    evalDecls sym
    sym [DeclGroup]
    ds GenEvalEnv sym
    env
         sym -> GenEvalEnv sym -> Expr -> SEval sym (GenValue sym)
    forall sym.
    (?range::Range, EvalPrims sym) =>
    sym -> GenEvalEnv sym -> Expr -> SEval sym (GenValue sym)
    evalExpr sym
    sym GenEvalEnv sym
    env' Expr
    e

      EPropGuards [([Type], Expr)]
    guards Type
    _ -> {-# SCC "evalExpr->EPropGuards" #-} do
        let checkedGuards :: [Expr]
    checkedGuards = [ Expr
    e | ([Type]
    ps,Expr
    e) <- [([Type], Expr)]
    guards, (Type -> Bool) -> [Type] -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    all (Type -> Bool
    checkProp (Type -> Bool) -> (Type -> Type) -> Type -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . GenEvalEnv sym -> Type -> Type
    forall sym. GenEvalEnv sym -> Type -> Type
    evalProp GenEvalEnv sym
    env) [Type]
    ps ]
        case [Expr]
    checkedGuards of
          (Expr
    e:[Expr]
    _) -> Expr -> SEval sym (GenValue sym)
    eval Expr
    e
          [] -> sym -> EvalError -> SEval sym (GenValue sym)
    forall a. sym -> EvalError -> SEval sym a
    forall sym a. Backend sym => sym -> EvalError -> SEval sym a
    raiseError sym
    sym (String -> EvalError
    NoMatchingPropGuardCase (String -> EvalError) -> String -> EvalError
    forall a b. (a -> b) -> a -> b
    $ String
    "Among constraint guards: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ [[Doc]] -> String
    forall a. Show a => a -> String
    show ((Type -> Doc) -> [Type] -> [Doc]
    forall a b. (a -> b) -> [a] -> [b]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap Type -> Doc
    forall a. PP a => a -> Doc
    pp ([Type] -> [Doc])
    -> (([Type], Expr) -> [Type]) -> ([Type], Expr) -> [Doc]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ([Type], Expr) -> [Type]
    forall a b. (a, b) -> a
    fst (([Type], Expr) -> [Doc]) -> [([Type], Expr)] -> [[Doc]]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> [([Type], Expr)]
    guards))

      where

      {-# INLINE eval #-}
      eval :: Expr -> SEval sym (GenValue sym)
    eval = sym -> GenEvalEnv sym -> Expr -> SEval sym (GenValue sym)
    forall sym.
    (?range::Range, EvalPrims sym) =>
    sym -> GenEvalEnv sym -> Expr -> SEval sym (GenValue sym)
    evalExpr sym
    sym GenEvalEnv sym
    env
      ppV :: GenValue sym -> SEval sym Doc
    ppV = sym -> PPOpts -> GenValue sym -> SEval sym Doc
    forall sym.
    Backend sym =>
    sym -> PPOpts -> GenValue sym -> SEval sym Doc
    ppValue sym
    sym PPOpts
    defaultPPOpts

    -- | Checks whether an evaluated `Prop` holds
    checkProp :: Prop -> Bool
    checkProp :: Type -> Bool
    checkProp = \case
      TCon TCon
    tcon [Type]
    ts ->
        let ns :: [Nat']
    ns = Type -> Nat'
    toNat' (Type -> Nat') -> [Type] -> [Nat']
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> [Type]
    ts in
        case TCon
    tcon of
          PC PC
    PEqual | [Nat'
    n1, Nat'
    n2] <- [Nat']
    ns -> Nat'
    n1 Nat' -> Nat' -> Bool
    forall a. Eq a => a -> a -> Bool
    == Nat'
    n2
          PC PC
    PNeq | [Nat'
    n1, Nat'
    n2] <- [Nat']
    ns -> Nat'
    n1 Nat' -> Nat' -> Bool
    forall a. Eq a => a -> a -> Bool
    /= Nat'
    n2
          PC PC
    PGeq | [Nat'
    n1, Nat'
    n2] <- [Nat']
    ns -> Nat'
    n1 Nat' -> Nat' -> Bool
    forall a. Ord a => a -> a -> Bool
    >= Nat'
    n2
          PC PC
    PFin | [Nat'
    n] <- [Nat']
    ns -> Nat'
    n Nat' -> Nat' -> Bool
    forall a. Eq a => a -> a -> Bool
    /= Nat'
    Inf
          -- TODO: instantiate UniqueFactorization for Nat'?
          -- PC PPrime | [n] <- ns -> isJust (isPrime n)
          PC PC
    PTrue -> Bool
    True
          TError {} -> Bool
    False
          TCon
    _ -> String -> [String] -> Bool
    forall a. HasCallStack => String -> [String] -> a
    evalPanic String
    "evalProp" [String
    "cannot use this as a guarding constraint: ", Doc -> String
    forall a. Show a => a -> String
    show (Doc -> String) -> (Type -> Doc) -> Type -> String
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Type -> Doc
    forall a. PP a => a -> Doc
    pp (Type -> String) -> Type -> String
    forall a b. (a -> b) -> a -> b
    $ TCon -> [Type] -> Type
    TCon TCon
    tcon [Type]
    ts ]
      Type
    prop -> String -> [String] -> Bool
    forall a. HasCallStack => String -> [String] -> a
    evalPanic String
    "evalProp" [String
    "cannot use this as a guarding constraint: ", Doc -> String
    forall a. Show a => a -> String
    show (Doc -> String) -> (Type -> Doc) -> Type -> String
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Type -> Doc
    forall a. PP a => a -> Doc
    pp (Type -> String) -> Type -> String
    forall a b. (a -> b) -> a -> b
    $ Type
    prop ]
      where
        toNat' :: Type -> Nat'
        toNat' :: Type -> Nat'
    toNat' = \case
          TCon (TC (TCNum Integer
    n)) [] -> Integer -> Nat'
    Nat Integer
    n
          TCon (TC TC
    TCInf) [] -> Nat'
    Inf
          Type
    prop -> String -> [String] -> Nat'
    forall a. HasCallStack => String -> [String] -> a
    panic String
    "checkProp" [String
    "Expected `" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Type -> String
    forall a. PP a => a -> String
    pretty Type
    prop String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    "` to be an evaluated numeric type"]

    -- | Evaluates a `Prop` in an `EvalEnv` by substituting all variables according
    -- to `envTypes` and expanding all type synonyms via `tNoUser`.
    evalProp :: GenEvalEnv sym -> Prop -> Prop
    evalProp :: forall sym. GenEvalEnv sym -> Type -> Type
    evalProp env :: GenEvalEnv sym
    env@EvalEnv { TypeEnv
    envTypes :: forall sym. GenEvalEnv sym -> TypeEnv
    envTypes :: TypeEnv
    envTypes } = \case
      TCon TCon
    tc [Type]
    tys
        | TError Kind
    KProp <- TCon
    tc, [Type
    p] <- [Type]
    tys ->
          case GenEvalEnv sym -> Type -> Type
    forall sym. GenEvalEnv sym -> Type -> Type
    evalProp GenEvalEnv sym
    env Type
    p of
            x :: Type
    x@(TCon (TError Kind
    KProp) [Type]
    _) -> Type
    x
            Type
    _                         -> TCon -> [Type] -> Type
    TCon (Kind -> TCon
    TError Kind
    KProp) [GenEvalEnv sym -> Type -> Type
    forall sym. GenEvalEnv sym -> Type -> Type
    evalProp GenEvalEnv sym
    env Type
    p]
        | Bool
    otherwise -> TCon -> [Type] -> Type
    TCon TCon
    tc (Either Nat' TValue -> Type
    toType (Either Nat' TValue -> Type)
    -> (Type -> Either Nat' TValue) -> Type -> Type
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . TypeEnv -> Type -> Either Nat' TValue
    evalType TypeEnv
    envTypes (Type -> Type) -> [Type] -> [Type]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> [Type]
    tys)
      TVar TVar
    tv | Just (Either Nat' TValue -> Type
    toType -> Type
    ty) <- TVar -> TypeEnv -> Maybe (Either Nat' TValue)
    lookupTypeVar TVar
    tv TypeEnv
    envTypes -> Type
    ty
      prop :: Type
    prop@TUser {} -> GenEvalEnv sym -> Type -> Type
    forall sym. GenEvalEnv sym -> Type -> Type
    evalProp GenEvalEnv sym
    env (Type -> Type
    tNoUser Type
    prop)
      TVar TVar
    tv | Maybe (Either Nat' TValue)
    Nothing <- TVar -> TypeEnv -> Maybe (Either Nat' TValue)
    lookupTypeVar TVar
    tv TypeEnv
    envTypes -> String -> [String] -> Type
    forall a. HasCallStack => String -> [String] -> a
    panic String
    "evalProp" [String
    "Could not find type variable `" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ TVar -> String
    forall a. PP a => a -> String
    pretty TVar
    tv String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    "` in the type evaluation environment"]
      Type
    prop -> String -> [String] -> Type
    forall a. HasCallStack => String -> [String] -> a
    panic String
    "evalProp" [String
    "Cannot use the following as a type constraint: `" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Type -> String
    forall a. PP a => a -> String
    pretty Type
    prop String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    "`"]
      where
        toType :: Either Nat' TValue -> Type
    toType = (Nat' -> Type) -> (TValue -> Type) -> Either Nat' TValue -> Type
    forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
    either Nat' -> Type
    tNumTy TValue -> Type
    tValTy

    -- | Capure the current call stack from the evaluation monad and
    --   annotate function values.  When arguments are later applied
    --   to the function, the call stacks will be combined together.
    cacheCallStack ::
      Backend sym =>
      sym ->
      GenValue sym ->
      SEval sym (GenValue sym)
    cacheCallStack :: forall sym.
    Backend sym =>
    sym -> GenValue sym -> SEval sym (GenValue sym)
    cacheCallStack sym
    sym GenValue sym
    v = case GenValue sym
    v of
      VFun CallStack
    fnstk SEval sym (GenValue sym) -> SEval sym (GenValue sym)
    f ->
        do CallStack
    stk <- sym -> SEval sym CallStack
    forall sym. Backend sym => sym -> SEval sym CallStack
    sGetCallStack sym
    sym
           GenValue sym -> SEval sym (GenValue sym)
    forall a. a -> SEval sym a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (CallStack
    -> (SEval sym (GenValue sym) -> SEval sym (GenValue sym))
    -> GenValue sym
    forall sym.
    CallStack
    -> (SEval sym (GenValue sym) -> SEval sym (GenValue sym))
    -> GenValue sym
    VFun (CallStack -> CallStack -> CallStack
    combineCallStacks CallStack
    stk CallStack
    fnstk) SEval sym (GenValue sym) -> SEval sym (GenValue sym)
    f)
      VPoly CallStack
    fnstk TValue -> SEval sym (GenValue sym)
    f ->
        do CallStack
    stk <- sym -> SEval sym CallStack
    forall sym. Backend sym => sym -> SEval sym CallStack
    sGetCallStack sym
    sym
           GenValue sym -> SEval sym (GenValue sym)
    forall a. a -> SEval sym a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (CallStack -> (TValue -> SEval sym (GenValue sym)) -> GenValue sym
    forall sym.
    CallStack -> (TValue -> SEval sym (GenValue sym)) -> GenValue sym
    VPoly (CallStack -> CallStack -> CallStack
    combineCallStacks CallStack
    stk CallStack
    fnstk) TValue -> SEval sym (GenValue sym)
    f)
      VNumPoly CallStack
    fnstk Nat' -> SEval sym (GenValue sym)
    f ->
        do CallStack
    stk <- sym -> SEval sym CallStack
    forall sym. Backend sym => sym -> SEval sym CallStack
    sGetCallStack sym
    sym
           GenValue sym -> SEval sym (GenValue sym)
    forall a. a -> SEval sym a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (CallStack -> (Nat' -> SEval sym (GenValue sym)) -> GenValue sym
    forall sym.
    CallStack -> (Nat' -> SEval sym (GenValue sym)) -> GenValue sym
    VNumPoly (CallStack -> CallStack -> CallStack
    combineCallStacks CallStack
    stk CallStack
    fnstk) Nat' -> SEval sym (GenValue sym)
    f)

      -- non-function types don't get annotated
      GenValue sym
    _ -> GenValue sym -> SEval sym (GenValue sym)
    forall a. a -> SEval sym a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure GenValue sym
    v

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

    {-# SPECIALIZE evalNewtypeDecls ::
      ConcPrims =>
      Concrete ->
      Map.Map Name Newtype ->
      GenEvalEnv Concrete ->
      SEval Concrete (GenEvalEnv Concrete)
      #-}

    evalNewtypeDecls ::
      EvalPrims sym =>
      sym ->
      Map.Map Name Newtype ->
      GenEvalEnv sym ->
      SEval sym (GenEvalEnv sym)
    evalNewtypeDecls :: forall sym.
    EvalPrims sym =>
    sym
    -> Map Name Newtype -> GenEvalEnv sym -> SEval sym (GenEvalEnv sym)
    evalNewtypeDecls sym
    sym Map Name Newtype
    nts GenEvalEnv sym
    env = (GenEvalEnv sym -> Newtype -> SEval sym (GenEvalEnv sym))
    -> GenEvalEnv sym -> [Newtype] -> SEval sym (GenEvalEnv sym)
    forall (t :: * -> *) (m :: * -> *) b a.
    (Foldable t, Monad m) =>
    (b -> a -> m b) -> b -> t a -> m b
    foldM ((Newtype -> GenEvalEnv sym -> SEval sym (GenEvalEnv sym))
    -> GenEvalEnv sym -> Newtype -> SEval sym (GenEvalEnv sym)
    forall a b c. (a -> b -> c) -> b -> a -> c
    flip (sym -> Newtype -> GenEvalEnv sym -> SEval sym (GenEvalEnv sym)
    forall sym.
    EvalPrims sym =>
    sym -> Newtype -> GenEvalEnv sym -> SEval sym (GenEvalEnv sym)
    evalNewtypeDecl sym
    sym)) GenEvalEnv sym
    env ([Newtype] -> SEval sym (GenEvalEnv sym))
    -> [Newtype] -> SEval sym (GenEvalEnv sym)
    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.
    evalNewtypeDecl ::
      EvalPrims sym =>
      sym ->
      Newtype ->
      GenEvalEnv sym ->
      SEval sym (GenEvalEnv sym)
    evalNewtypeDecl :: forall sym.
    EvalPrims sym =>
    sym -> Newtype -> GenEvalEnv sym -> SEval sym (GenEvalEnv sym)
    evalNewtypeDecl sym
    _sym Newtype
    nt = GenEvalEnv sym -> SEval sym (GenEvalEnv sym)
    forall a. a -> SEval sym a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (GenEvalEnv sym -> SEval sym (GenEvalEnv sym))
    -> (GenEvalEnv sym -> GenEvalEnv sym)
    -> GenEvalEnv sym
    -> SEval sym (GenEvalEnv sym)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Name -> Prim sym -> GenEvalEnv sym -> GenEvalEnv sym
    forall sym.
    Backend sym =>
    Name -> Prim sym -> GenEvalEnv sym -> GenEvalEnv sym
    bindVarDirect (Newtype -> Name
    ntConName Newtype
    nt) ((TParam -> Prim sym -> Prim sym)
    -> Prim sym -> [TParam] -> Prim sym
    forall a b. (a -> b -> b) -> b -> [a] -> b
    forall (t :: * -> *) a b.
    Foldable t =>
    (a -> b -> b) -> b -> t a -> b
    foldr TParam -> Prim sym -> Prim sym
    forall {sym}. TParam -> Prim sym -> Prim sym
    tabs Prim sym
    forall {sym}. Prim sym
    con (Newtype -> [TParam]
    ntParams Newtype
    nt))
      where
      con :: Prim sym
    con           = (SEval sym (GenValue sym) -> Prim sym) -> Prim sym
    forall sym. (SEval sym (GenValue sym) -> Prim sym) -> Prim sym
    PFun SEval sym (GenValue sym) -> Prim sym
    forall sym. SEval sym (GenValue sym) -> Prim sym
    PPrim

      tabs :: TParam -> Prim sym -> Prim sym
    tabs TParam
    tp Prim sym
    body =
        case TParam -> Kind
    tpKind TParam
    tp of
          Kind
    KType -> (TValue -> Prim sym) -> Prim sym
    forall sym. (TValue -> Prim sym) -> Prim sym
    PTyPoly  (\ TValue
    _ -> Prim sym
    body)
          Kind
    KNum  -> (Nat' -> Prim sym) -> Prim sym
    forall sym. (Nat' -> Prim sym) -> Prim sym
    PNumPoly (\ Nat'
    _ -> Prim sym
    body)
          Kind
    k -> String -> [String] -> Prim sym
    forall a. HasCallStack => String -> [String] -> a
    evalPanic String
    "evalNewtypeDecl" [String
    "illegal newtype parameter kind", Doc -> String
    forall a. Show a => a -> String
    show (Kind -> Doc
    forall a. PP a => a -> Doc
    pp Kind
    k)]

    {-# INLINE evalNewtypeDecl #-}

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

    {-# SPECIALIZE evalDecls ::
      ConcPrims =>
      Concrete ->
      [DeclGroup] ->
      GenEvalEnv Concrete ->
      SEval Concrete (GenEvalEnv Concrete)
      #-}

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

    {-# SPECIALIZE evalDeclGroup ::
      ConcPrims =>
      Concrete ->
      GenEvalEnv Concrete ->
      DeclGroup ->
      SEval Concrete (GenEvalEnv Concrete)
      #-}

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

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

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

          -- return the map containing the holes
          GenEvalEnv sym -> SEval sym (GenEvalEnv sym)
    forall a. a -> SEval sym a
    forall (m :: * -> *) a. Monad m => a -> m a
    return GenEvalEnv sym
    env'

        NonRecursive Decl
    d -> do
          sym
    -> GenEvalEnv sym
    -> GenEvalEnv sym
    -> Decl
    -> SEval sym (GenEvalEnv sym)
    forall sym.
    EvalPrims sym =>
    sym
    -> GenEvalEnv sym
    -> GenEvalEnv sym
    -> Decl
    -> SEval sym (GenEvalEnv sym)
    evalDecl sym
    sym GenEvalEnv sym
    env GenEvalEnv sym
    env Decl
    d

    {-# SPECIALIZE fillHole ::
      Concrete ->
      GenEvalEnv Concrete ->
      (Name, Schema, SEval Concrete (GenValue Concrete), SEval Concrete (GenValue Concrete) -> SEval Concrete ()) ->
      SEval Concrete ()
      #-}

    -- | 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 ::
      Backend sym =>
      sym ->
      GenEvalEnv sym ->
      (Name, Schema, SEval sym (GenValue sym), SEval sym (GenValue sym) -> SEval sym ()) ->
      SEval sym ()
    fillHole :: forall sym.
    Backend sym =>
    sym
    -> GenEvalEnv sym
    -> (Name, Schema, SEval sym (GenValue sym),
        SEval sym (GenValue sym) -> SEval sym ())
    -> SEval sym ()
    fillHole sym
    _sym GenEvalEnv sym
    env (Name
    nm, Schema
    _sch, SEval sym (GenValue sym)
    _, SEval sym (GenValue sym) -> SEval sym ()
    fill) = do
      case Name
    -> GenEvalEnv sym
    -> Maybe (Either (Prim sym) (SEval sym (GenValue sym)))
    forall sym.
    Name
    -> GenEvalEnv sym
    -> Maybe (Either (Prim sym) (SEval sym (GenValue sym)))
    lookupVar Name
    nm GenEvalEnv sym
    env of
        Just (Right SEval sym (GenValue sym)
    v) -> SEval sym (GenValue sym) -> SEval sym ()
    fill SEval sym (GenValue sym)
    v
        Maybe (Either (Prim sym) (SEval sym (GenValue sym)))
    _ -> String -> [String] -> SEval sym ()
    forall a. HasCallStack => String -> [String] -> a
    evalPanic String
    "fillHole" [String
    "Recursive definition not completed", Doc -> String
    forall a. Show a => a -> String
    show (Name -> Doc
    ppLocName Name
    nm)]

    {-# SPECIALIZE declHole ::
      Concrete ->
      Decl ->
      SEval Concrete
        (Name, Schema, SEval Concrete (GenValue Concrete), SEval Concrete (GenValue Concrete) -> SEval Concrete ())
      #-}

    declHole ::
      Backend sym =>
      sym -> Decl -> SEval sym (Name, Schema, SEval sym (GenValue sym), SEval sym (GenValue sym) -> SEval sym ())
    declHole :: forall sym.
    Backend sym =>
    sym
    -> Decl
    -> SEval
         sym
         (Name, Schema, SEval sym (GenValue sym),
          SEval sym (GenValue sym) -> SEval sym ())
    declHole sym
    sym Decl
    d =
      case Decl -> DeclDef
    dDefinition Decl
    d of
        DeclDef
    DPrim      -> String
    -> [String]
    -> SEval
         sym
         (Name, Schema, SEval sym (GenValue sym),
          SEval sym (GenValue sym) -> SEval sym ())
    forall a. HasCallStack => String -> [String] -> a
    evalPanic String
    "Unexpected primitive declaration in recursive group"
                                [Doc -> String
    forall a. Show a => a -> String
    show (Name -> Doc
    ppLocName Name
    nm)]
        DForeign FFIFunType
    _ -> String
    -> [String]
    -> SEval
         sym
         (Name, Schema, SEval sym (GenValue sym),
          SEval sym (GenValue sym) -> SEval sym ())
    forall a. HasCallStack => String -> [String] -> a
    evalPanic String
    "Unexpected foreign declaration in recursive group"
                                [Doc -> String
    forall a. Show a => a -> String
    show (Name -> Doc
    ppLocName Name
    nm)]
        DExpr Expr
    _    -> do
          (SEval sym (GenValue sym)
    hole, SEval sym (GenValue sym) -> SEval sym ()
    fill) <- sym
    -> String
    -> SEval
         sym
         (SEval sym (GenValue sym),
          SEval sym (GenValue sym) -> SEval sym ())
    forall a.
    sym
    -> String -> SEval sym (SEval sym a, SEval sym a -> SEval sym ())
    forall sym a.
    Backend sym =>
    sym
    -> String -> SEval sym (SEval sym a, SEval sym a -> SEval sym ())
    sDeclareHole sym
    sym String
    msg
          (Name, Schema, SEval sym (GenValue sym),
     SEval sym (GenValue sym) -> SEval sym ())
    -> SEval
         sym
         (Name, Schema, SEval sym (GenValue sym),
          SEval sym (GenValue sym) -> SEval sym ())
    forall a. a -> SEval sym a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Name
    nm, Schema
    sch, SEval sym (GenValue sym)
    hole, SEval sym (GenValue sym) -> SEval sym ()
    fill)
      where
      nm :: Name
    nm = Decl -> Name
    dName Decl
    d
      sch :: Schema
    sch = Decl -> Schema
    dSignature Decl
    d
      msg :: String
    msg = [String] -> String
    unwords [String
    "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 sym =>
      sym ->
      GenEvalEnv sym  {- ^ A 'read only' environment for use in declaration bodies -} ->
      GenEvalEnv sym  {- ^ An evaluation environment to extend with the given declaration -} ->
      Decl            {- ^ The declaration to evaluate -} ->
      SEval sym (GenEvalEnv sym)
    -- evalDecl sym renv env d =
    --   let ?range = nameLoc (dName d) in
    evalDecl :: forall sym.
    EvalPrims sym =>
    sym
    -> GenEvalEnv sym
    -> GenEvalEnv sym
    -> Decl
    -> SEval sym (GenEvalEnv sym)
    evalDecl sym
    sym GenEvalEnv sym
    renv GenEvalEnv sym
    env Decl
    d = do
      let ?range = Name -> Range
    nameLoc (Decl -> Name
    dName Decl
    d)
      case Decl -> DeclDef
    dDefinition Decl
    d of
        DeclDef
    DPrim ->
          case ?evalPrim::PrimIdent -> Maybe (Either Expr (Prim sym))
    PrimIdent -> Maybe (Either Expr (Prim sym))
    ?evalPrim (PrimIdent -> Maybe (Either Expr (Prim sym)))
    -> Maybe PrimIdent -> Maybe (Either Expr (Prim sym))
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< Name -> Maybe PrimIdent
    asPrim (Decl -> Name
    dName Decl
    d) of
            Just (Right Prim sym
    p) -> GenEvalEnv sym -> SEval sym (GenEvalEnv sym)
    forall a. a -> SEval sym a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (GenEvalEnv sym -> SEval sym (GenEvalEnv sym))
    -> GenEvalEnv sym -> SEval sym (GenEvalEnv sym)
    forall a b. (a -> b) -> a -> b
    $ Name -> Prim sym -> GenEvalEnv sym -> GenEvalEnv sym
    forall sym.
    Backend sym =>
    Name -> Prim sym -> GenEvalEnv sym -> GenEvalEnv sym
    bindVarDirect (Decl -> Name
    dName Decl
    d) Prim sym
    p GenEvalEnv sym
    env
            Just (Left Expr
    ex) -> sym
    -> Name
    -> SEval sym (GenValue sym)
    -> GenEvalEnv sym
    -> SEval sym (GenEvalEnv sym)
    forall sym.
    Backend sym =>
    sym
    -> Name
    -> SEval sym (GenValue sym)
    -> GenEvalEnv sym
    -> SEval sym (GenEvalEnv sym)
    bindVar sym
    sym (Decl -> Name
    dName Decl
    d) (sym -> GenEvalEnv sym -> Expr -> SEval sym (GenValue sym)
    forall sym.
    (?range::Range, EvalPrims sym) =>
    sym -> GenEvalEnv sym -> Expr -> SEval sym (GenValue sym)
    evalExpr sym
    sym GenEvalEnv sym
    renv Expr
    ex) GenEvalEnv sym
    env
            Maybe (Either Expr (Prim sym))
    Nothing        -> sym
    -> Name
    -> SEval sym (GenValue sym)
    -> GenEvalEnv sym
    -> SEval sym (GenEvalEnv sym)
    forall sym.
    Backend sym =>
    sym
    -> Name
    -> SEval sym (GenValue sym)
    -> GenEvalEnv sym
    -> SEval sym (GenEvalEnv sym)
    bindVar sym
    sym (Decl -> Name
    dName Decl
    d) (sym -> Name -> SEval sym (GenValue sym)
    forall sym a. Backend sym => sym -> Name -> SEval sym a
    cryNoPrimError sym
    sym (Decl -> Name
    dName Decl
    d)) GenEvalEnv sym
    env

        DForeign FFIFunType
    _ -> do
          -- Foreign declarations should have been handled by the previous
          -- Cryptol.Eval.FFI.evalForeignDecls pass already, so they should already
          -- be in the environment. If not, then either Cryptol was not compiled
          -- with FFI support enabled, or we are in a non-Concrete backend. In that
          -- case, we just bind the name to an error computation which will raise an
          -- error if we try to evaluate it.
          case Name
    -> GenEvalEnv sym
    -> Maybe (Either (Prim sym) (SEval sym (GenValue sym)))
    forall sym.
    Name
    -> GenEvalEnv sym
    -> Maybe (Either (Prim sym) (SEval sym (GenValue sym)))
    lookupVar (Decl -> Name
    dName Decl
    d) GenEvalEnv sym
    env of
            Just Either (Prim sym) (SEval sym (GenValue sym))
    _  -> GenEvalEnv sym -> SEval sym (GenEvalEnv sym)
    forall a. a -> SEval sym a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure GenEvalEnv sym
    env
            Maybe (Either (Prim sym) (SEval sym (GenValue sym)))
    Nothing -> sym
    -> Name
    -> SEval sym (GenValue sym)
    -> GenEvalEnv sym
    -> SEval sym (GenEvalEnv sym)
    forall sym.
    Backend sym =>
    sym
    -> Name
    -> SEval sym (GenValue sym)
    -> GenEvalEnv sym
    -> SEval sym (GenEvalEnv sym)
    bindVar sym
    sym (Decl -> Name
    dName Decl
    d)
              (sym -> EvalError -> SEval sym (GenValue sym)
    forall a. sym -> EvalError -> SEval sym a
    forall sym a. Backend sym => sym -> EvalError -> SEval sym a
    raiseError sym
    sym (EvalError -> SEval sym (GenValue sym))
    -> EvalError -> SEval sym (GenValue sym)
    forall a b. (a -> b) -> a -> b
    $ Name -> EvalError
    FFINotSupported (Name -> EvalError) -> Name -> EvalError
    forall a b. (a -> b) -> a -> b
    $ Decl -> Name
    dName Decl
    d) GenEvalEnv sym
    env

        DExpr Expr
    e -> sym
    -> Name
    -> SEval sym (GenValue sym)
    -> GenEvalEnv sym
    -> SEval sym (GenEvalEnv sym)
    forall sym.
    Backend sym =>
    sym
    -> Name
    -> SEval sym (GenValue sym)
    -> GenEvalEnv sym
    -> SEval sym (GenEvalEnv sym)
    bindVar sym
    sym (Decl -> Name
    dName Decl
    d) (sym -> GenEvalEnv sym -> Expr -> SEval sym (GenValue sym)
    forall sym.
    (?range::Range, EvalPrims sym) =>
    sym -> GenEvalEnv sym -> Expr -> SEval sym (GenValue sym)
    evalExpr sym
    sym GenEvalEnv sym
    renv Expr
    e) GenEvalEnv sym
    env

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

    {-# SPECIALIZE evalSel ::
      Concrete ->
      GenValue Concrete ->
      Selector ->
      SEval Concrete (GenValue Concrete)
      #-}

    -- | Apply the the given "selector" form to the given value.  Note that
    --   selectors are expected to apply only to values of the right type,
    --   e.g. tuple selectors expect only tuple values.  The lifting of
    --   tuple an record selectors over functions and sequences has already
    --   been resolved earlier in the typechecker.
    evalSel ::
      Backend sym =>
      sym ->
      GenValue sym ->
      Selector ->
      SEval sym (GenValue sym)
    evalSel :: forall sym.
    Backend sym =>
    sym -> GenValue sym -> Selector -> SEval sym (GenValue sym)
    evalSel sym
    sym GenValue sym
    val Selector
    sel = case Selector
    sel of

      TupleSel Int
    n Maybe Int
    _  -> Int -> GenValue sym -> SEval sym (GenValue sym)
    tupleSel Int
    n GenValue sym
    val
      RecordSel Ident
    n Maybe [Ident]
    _ -> Ident -> GenValue sym -> SEval sym (GenValue sym)
    recordSel Ident
    n GenValue sym
    val
      ListSel Int
    ix Maybe Int
    _  -> Int -> GenValue sym -> SEval sym (GenValue sym)
    forall {a}.
    Integral a =>
    a -> GenValue sym -> SEval sym (GenValue sym)
    listSel Int
    ix GenValue sym
    val
      where

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

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

      listSel :: a -> GenValue sym -> SEval sym (GenValue sym)
    listSel a
    n GenValue sym
    v =
        case GenValue sym
    v of
          VSeq Integer
    _ SeqMap sym (GenValue sym)
    vs       -> SeqMap sym (GenValue sym) -> Integer -> SEval sym (GenValue sym)
    forall sym a. Backend sym => SeqMap sym a -> Integer -> SEval sym a
    lookupSeqMap SeqMap sym (GenValue sym)
    vs (a -> Integer
    forall a. Integral a => a -> Integer
    toInteger a
    n)
          VStream SeqMap sym (GenValue sym)
    vs      -> SeqMap sym (GenValue sym) -> Integer -> SEval sym (GenValue sym)
    forall sym a. Backend sym => SeqMap sym a -> Integer -> SEval sym a
    lookupSeqMap SeqMap sym (GenValue sym)
    vs (a -> Integer
    forall a. Integral a => a -> Integer
    toInteger a
    n)
          VWord Integer
    _ WordValue sym
    wv      -> SBit sym -> GenValue sym
    forall sym. SBit sym -> GenValue sym
    VBit (SBit sym -> GenValue sym)
    -> SEval sym (SBit sym) -> SEval sym (GenValue sym)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> sym -> WordValue sym -> Integer -> SEval sym (SBit sym)
    forall sym.
    Backend sym =>
    sym -> WordValue sym -> Integer -> SEval sym (SBit sym)
    indexWordValue sym
    sym WordValue sym
    wv (a -> Integer
    forall a. Integral a => a -> Integer
    toInteger a
    n)
          GenValue sym
    _               -> do Doc
    vdoc <- sym -> PPOpts -> GenValue sym -> SEval sym Doc
    forall sym.
    Backend sym =>
    sym -> PPOpts -> GenValue sym -> SEval sym Doc
    ppValue sym
    sym PPOpts
    defaultPPOpts GenValue sym
    val
                                String -> [String] -> SEval sym (GenValue sym)
    forall a. HasCallStack => String -> [String] -> a
    evalPanic String
    "Cryptol.Eval.evalSel"
                                  [ String
    "Unexpected value in list selection"
                                  , Doc -> String
    forall a. Show a => a -> String
    show Doc
    vdoc ]
    {-# SPECIALIZE evalSetSel ::
      Concrete -> TValue ->
      GenValue Concrete -> Selector -> SEval Concrete (GenValue Concrete) -> SEval Concrete (GenValue Concrete)
      #-}
    evalSetSel :: forall sym.
      Backend sym =>
      sym ->
      TValue ->
      GenValue sym -> Selector -> SEval sym (GenValue sym) -> SEval sym (GenValue sym)
    evalSetSel :: forall sym.
    Backend sym =>
    sym
    -> TValue
    -> GenValue sym
    -> Selector
    -> SEval sym (GenValue sym)
    -> SEval sym (GenValue sym)
    evalSetSel sym
    sym TValue
    _tyv GenValue sym
    e Selector
    sel SEval sym (GenValue sym)
    v =
      case Selector
    sel of
        TupleSel Int
    n Maybe Int
    _  -> Int -> SEval sym (GenValue sym)
    setTuple Int
    n
        RecordSel Ident
    n Maybe [Ident]
    _ -> Ident -> SEval sym (GenValue sym)
    setRecord Ident
    n
        ListSel Int
    ix Maybe Int
    _  -> Integer -> SEval sym (GenValue sym)
    setList (Int -> Integer
    forall a. Integral a => a -> Integer
    toInteger Int
    ix)

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

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

      setRecord :: Ident -> SEval sym (GenValue sym)
    setRecord Ident
    n =
        case GenValue sym
    e of
          VRecord RecordMap Ident (SEval sym (GenValue sym))
    xs ->
            case Ident
    -> (SEval sym (GenValue sym) -> SEval sym (GenValue sym))
    -> RecordMap Ident (SEval sym (GenValue sym))
    -> Maybe (RecordMap Ident (SEval sym (GenValue sym)))
    forall a b.
    Ord a =>
    a -> (b -> b) -> RecordMap a b -> Maybe (RecordMap a b)
    adjustField Ident
    n (\SEval sym (GenValue sym)
    _ -> SEval sym (GenValue sym)
    v) RecordMap Ident (SEval sym (GenValue sym))
    xs of
              Just RecordMap Ident (SEval sym (GenValue sym))
    xs' -> GenValue sym -> SEval sym (GenValue sym)
    forall a. a -> SEval sym a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (RecordMap Ident (SEval sym (GenValue sym)) -> GenValue sym
    forall sym.
    RecordMap Ident (SEval sym (GenValue sym)) -> GenValue sym
    VRecord RecordMap Ident (SEval sym (GenValue sym))
    xs')
              Maybe (RecordMap Ident (SEval sym (GenValue sym)))
    Nothing -> String -> SEval sym (GenValue sym)
    forall {b}. String -> SEval sym b
    bad String
    "Missing field in record update."
          GenValue sym
    _ -> String -> SEval sym (GenValue sym)
    forall {b}. String -> SEval sym b
    bad String
    "Record update on a non-record."

      setList :: Integer -> SEval sym (GenValue sym)
    setList Integer
    n =
        case GenValue sym
    e of
          VSeq Integer
    i SeqMap sym (GenValue sym)
    mp  -> GenValue sym -> SEval sym (GenValue sym)
    forall a. a -> SEval sym a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (GenValue sym -> SEval sym (GenValue sym))
    -> GenValue sym -> SEval sym (GenValue sym)
    forall a b. (a -> b) -> a -> b
    $ Integer -> SeqMap sym (GenValue sym) -> GenValue sym
    forall sym. Integer -> SeqMap sym (GenValue sym) -> GenValue sym
    VSeq Integer
    i  (SeqMap sym (GenValue sym) -> GenValue sym)
    -> SeqMap sym (GenValue sym) -> GenValue sym
    forall a b. (a -> b) -> a -> b
    $ SeqMap sym (GenValue sym)
    -> Integer -> SEval sym (GenValue sym) -> SeqMap sym (GenValue sym)
    forall sym a.
    SeqMap sym a -> Integer -> SEval sym a -> SeqMap sym a
    updateSeqMap SeqMap sym (GenValue sym)
    mp Integer
    n SEval sym (GenValue sym)
    v
          VStream SeqMap sym (GenValue sym)
    mp -> GenValue sym -> SEval sym (GenValue sym)
    forall a. a -> SEval sym a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (GenValue sym -> SEval sym (GenValue sym))
    -> GenValue sym -> SEval sym (GenValue sym)
    forall a b. (a -> b) -> a -> b
    $ SeqMap sym (GenValue sym) -> GenValue sym
    forall sym. SeqMap sym (GenValue sym) -> GenValue sym
    VStream (SeqMap sym (GenValue sym) -> GenValue sym)
    -> SeqMap sym (GenValue sym) -> GenValue sym
    forall a b. (a -> b) -> a -> b
    $ SeqMap sym (GenValue sym)
    -> Integer -> SEval sym (GenValue sym) -> SeqMap sym (GenValue sym)
    forall sym a.
    SeqMap sym a -> Integer -> SEval sym a -> SeqMap sym a
    updateSeqMap SeqMap sym (GenValue sym)
    mp Integer
    n SEval sym (GenValue sym)
    v
          VWord Integer
    i WordValue sym
    m  -> Integer -> WordValue sym -> GenValue sym
    forall sym. Integer -> WordValue sym -> GenValue sym
    VWord Integer
    i (WordValue sym -> GenValue sym)
    -> SEval sym (WordValue sym) -> SEval sym (GenValue sym)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> sym
    -> WordValue sym
    -> Integer
    -> SEval sym (SBit sym)
    -> SEval sym (WordValue sym)
    forall sym.
    Backend sym =>
    sym
    -> WordValue sym
    -> Integer
    -> SEval sym (SBit sym)
    -> SEval sym (WordValue sym)
    updateWordValue sym
    sym WordValue sym
    m Integer
    n SEval sym (SBit sym)
    asBit
          GenValue sym
    _ -> String -> SEval sym (GenValue sym)
    forall {b}. String -> SEval sym b
    bad String
    "Sequence update on a non-sequence."

      asBit :: SEval sym (SBit sym)
    asBit = do GenValue sym
    res <- SEval sym (GenValue sym)
    v
                 case GenValue sym
    res of
                   VBit SBit sym
    b -> SBit sym -> SEval sym (SBit sym)
    forall a. a -> SEval sym a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure SBit sym
    b
                   GenValue sym
    _      -> String -> SEval sym (SBit sym)
    forall {b}. String -> SEval sym b
    bad String
    "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 sym = ListEnv
      { forall sym.
    ListEnv sym -> IntMap (Integer -> SEval sym (GenValue sym))
    leVars   :: !(IntMap.IntMap (Integer -> SEval sym (GenValue sym)))
          -- ^ Bindings whose values vary by position
      , forall sym.
    ListEnv sym
    -> IntMap (Either (Prim sym) (SEval sym (GenValue sym)))
    leStatic :: !(IntMap.IntMap (Either (Prim sym) (SEval sym (GenValue sym))))
          -- ^ Bindings whose values are constant
      , forall sym. ListEnv sym -> TypeEnv
    leTypes  :: !TypeEnv
      }

    instance Semigroup (ListEnv sym) where
      ListEnv sym
    l <> :: ListEnv sym -> ListEnv sym -> ListEnv sym
    <> ListEnv sym
    r = ListEnv
        { leVars :: IntMap (Integer -> SEval sym (GenValue sym))
    leVars   = IntMap (Integer -> SEval sym (GenValue sym))
    -> IntMap (Integer -> SEval sym (GenValue sym))
    -> IntMap (Integer -> SEval sym (GenValue sym))
    forall a. IntMap a -> IntMap a -> IntMap a
    IntMap.union (ListEnv sym -> IntMap (Integer -> SEval sym (GenValue sym))
    forall sym.
    ListEnv sym -> IntMap (Integer -> SEval sym (GenValue sym))
    leVars  ListEnv sym
    l)  (ListEnv sym -> IntMap (Integer -> SEval sym (GenValue sym))
    forall sym.
    ListEnv sym -> IntMap (Integer -> SEval sym (GenValue sym))
    leVars  ListEnv sym
    r)
        , leStatic :: IntMap (Either (Prim sym) (SEval sym (GenValue sym)))
    leStatic = IntMap (Either (Prim sym) (SEval sym (GenValue sym)))
    -> IntMap (Either (Prim sym) (SEval sym (GenValue sym)))
    -> IntMap (Either (Prim sym) (SEval sym (GenValue sym)))
    forall a. IntMap a -> IntMap a -> IntMap a
    IntMap.union (ListEnv sym
    -> IntMap (Either (Prim sym) (SEval sym (GenValue sym)))
    forall sym.
    ListEnv sym
    -> IntMap (Either (Prim sym) (SEval sym (GenValue sym)))
    leStatic ListEnv sym
    l) (ListEnv sym
    -> IntMap (Either (Prim sym) (SEval sym (GenValue sym)))
    forall sym.
    ListEnv sym
    -> IntMap (Either (Prim sym) (SEval sym (GenValue sym)))
    leStatic ListEnv sym
    r)
        , leTypes :: TypeEnv
    leTypes  = ListEnv sym -> TypeEnv
    forall sym. ListEnv sym -> TypeEnv
    leTypes ListEnv sym
    l TypeEnv -> TypeEnv -> TypeEnv
    forall a. Semigroup a => a -> a -> a
    <> ListEnv sym -> TypeEnv
    forall sym. ListEnv sym -> TypeEnv
    leTypes ListEnv sym
    r
        }

    instance Monoid (ListEnv sym) where
      mempty :: ListEnv sym
    mempty = ListEnv
        { leVars :: IntMap (Integer -> SEval sym (GenValue sym))
    leVars   = IntMap (Integer -> SEval sym (GenValue sym))
    forall a. IntMap a
    IntMap.empty
        , leStatic :: IntMap (Either (Prim sym) (SEval sym (GenValue sym)))
    leStatic = IntMap (Either (Prim sym) (SEval sym (GenValue sym)))
    forall a. IntMap a
    IntMap.empty
        , leTypes :: TypeEnv
    leTypes  = TypeEnv
    forall a. Monoid a => a
    mempty
        }

      mappend :: ListEnv sym -> ListEnv sym -> ListEnv sym
    mappend = ListEnv sym -> ListEnv sym -> ListEnv sym
    forall a. Semigroup a => a -> a -> a
    (<>)

    toListEnv :: GenEvalEnv sym -> ListEnv sym
    toListEnv :: forall sym. GenEvalEnv sym -> ListEnv sym
    toListEnv GenEvalEnv sym
    e =
      ListEnv
      { leVars :: IntMap (Integer -> SEval sym (GenValue sym))
    leVars   = IntMap (Integer -> SEval sym (GenValue sym))
    forall a. Monoid a => a
    mempty
      , leStatic :: IntMap (Either (Prim sym) (SEval sym (GenValue sym)))
    leStatic = GenEvalEnv sym
    -> IntMap (Either (Prim sym) (SEval sym (GenValue sym)))
    forall sym.
    GenEvalEnv sym
    -> IntMap (Either (Prim sym) (SEval sym (GenValue sym)))
    envVars GenEvalEnv sym
    e
      , leTypes :: TypeEnv
    leTypes  = GenEvalEnv sym -> TypeEnv
    forall sym. GenEvalEnv sym -> TypeEnv
    envTypes GenEvalEnv sym
    e
      }
    {-# INLINE toListEnv #-}

    -- | Evaluate a list environment at a position.
    --   This choses a particular value for the varying
    --   locations.
    evalListEnv :: ListEnv sym -> Integer -> GenEvalEnv sym
    evalListEnv :: forall sym. ListEnv sym -> Integer -> GenEvalEnv sym
    evalListEnv (ListEnv IntMap (Integer -> SEval sym (GenValue sym))
    vm IntMap (Either (Prim sym) (SEval sym (GenValue sym)))
    st TypeEnv
    tm) Integer
    i =
        let v :: IntMap (Either a (SEval sym (GenValue sym)))
    v = ((Integer -> SEval sym (GenValue sym))
     -> Either a (SEval sym (GenValue sym)))
    -> IntMap (Integer -> SEval sym (GenValue sym))
    -> IntMap (Either a (SEval sym (GenValue sym)))
    forall a b. (a -> b) -> IntMap a -> IntMap b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (SEval sym (GenValue sym) -> Either a (SEval sym (GenValue sym))
    forall a b. b -> Either a b
    Right (SEval sym (GenValue sym) -> Either a (SEval sym (GenValue sym)))
    -> ((Integer -> SEval sym (GenValue sym))
        -> SEval sym (GenValue sym))
    -> (Integer -> SEval sym (GenValue sym))
    -> Either a (SEval sym (GenValue sym))
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ((Integer -> SEval sym (GenValue sym))
    -> Integer -> SEval sym (GenValue sym)
    forall a b. (a -> b) -> a -> b
    $ Integer
    i)) IntMap (Integer -> SEval sym (GenValue sym))
    vm
         in EvalEnv{ envVars :: IntMap (Either (Prim sym) (SEval sym (GenValue sym)))
    envVars = IntMap (Either (Prim sym) (SEval sym (GenValue sym)))
    -> IntMap (Either (Prim sym) (SEval sym (GenValue sym)))
    -> IntMap (Either (Prim sym) (SEval sym (GenValue sym)))
    forall a. IntMap a -> IntMap a -> IntMap a
    IntMap.union IntMap (Either (Prim sym) (SEval sym (GenValue sym)))
    forall {a}. IntMap (Either a (SEval sym (GenValue sym)))
    v IntMap (Either (Prim sym) (SEval sym (GenValue sym)))
    st
                   , envTypes :: TypeEnv
    envTypes = TypeEnv
    tm
                   }
    {-# INLINE evalListEnv #-}

    bindVarList ::
      Name ->
      (Integer -> SEval sym (GenValue sym)) ->
      ListEnv sym ->
      ListEnv sym
    bindVarList :: forall sym.
    Name
    -> (Integer -> SEval sym (GenValue sym))
    -> ListEnv sym
    -> ListEnv sym
    bindVarList Name
    n Integer -> SEval sym (GenValue sym)
    vs ListEnv sym
    lenv = ListEnv sym
    lenv { leVars :: IntMap (Integer -> SEval sym (GenValue sym))
    leVars = Int
    -> (Integer -> SEval sym (GenValue sym))
    -> IntMap (Integer -> SEval sym (GenValue sym))
    -> IntMap (Integer -> SEval sym (GenValue sym))
    forall a. Int -> a -> IntMap a -> IntMap a
    IntMap.insert (Name -> Int
    nameUnique Name
    n) Integer -> SEval sym (GenValue sym)
    vs (ListEnv sym -> IntMap (Integer -> SEval sym (GenValue sym))
    forall sym.
    ListEnv sym -> IntMap (Integer -> SEval sym (GenValue sym))
    leVars ListEnv sym
    lenv) }
    {-# INLINE bindVarList #-}

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

    {-# SPECIALIZE evalComp ::
      (?range :: Range, ConcPrims) =>
      Concrete ->
      GenEvalEnv Concrete ->
      Nat'           ->
      TValue         ->
      Expr           ->
      [[Match]]      ->
      SEval Concrete (GenValue Concrete)
      #-}
    -- | Evaluate a comprehension.
    evalComp ::
      (?range :: Range, EvalPrims sym) =>
      sym ->
      GenEvalEnv sym {- ^ 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 -} ->
      SEval sym (GenValue sym)
    evalComp :: forall sym.
    (?range::Range, EvalPrims sym) =>
    sym
    -> GenEvalEnv sym
    -> Nat'
    -> TValue
    -> Expr
    -> [[Match]]
    -> SEval sym (GenValue sym)
    evalComp sym
    sym GenEvalEnv sym
    env Nat'
    len TValue
    elty Expr
    body [[Match]]
    ms =
           do ListEnv sym
    lenv <- [ListEnv sym] -> ListEnv sym
    forall a. Monoid a => [a] -> a
    mconcat ([ListEnv sym] -> ListEnv sym)
    -> SEval sym [ListEnv sym] -> SEval sym (ListEnv sym)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> ([Match] -> SEval sym (ListEnv sym))
    -> [[Match]] -> SEval sym [ListEnv sym]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
    mapM (sym -> ListEnv sym -> [Match] -> SEval sym (ListEnv sym)
    forall sym.
    (?range::Range, EvalPrims sym) =>
    sym -> ListEnv sym -> [Match] -> SEval sym (ListEnv sym)
    branchEnvs sym
    sym (GenEvalEnv sym -> ListEnv sym
    forall sym. GenEvalEnv sym -> ListEnv sym
    toListEnv GenEvalEnv sym
    env)) [[Match]]
    ms
              sym
    -> Nat'
    -> TValue
    -> SeqMap sym (GenValue sym)
    -> SEval sym (GenValue sym)
    forall sym.
    Backend sym =>
    sym
    -> Nat'
    -> TValue
    -> SeqMap sym (GenValue sym)
    -> SEval sym (GenValue sym)
    mkSeq sym
    sym Nat'
    len TValue
    elty (SeqMap sym (GenValue sym) -> SEval sym (GenValue sym))
    -> SEval sym (SeqMap sym (GenValue sym))
    -> SEval sym (GenValue sym)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< sym
    -> Nat'
    -> SeqMap sym (GenValue sym)
    -> SEval sym (SeqMap sym (GenValue sym))
    forall sym a.
    Backend sym =>
    sym -> Nat' -> SeqMap sym a -> SEval sym (SeqMap sym a)
    memoMap sym
    sym Nat'
    len ((Integer -> SEval sym (GenValue sym)) -> SeqMap sym (GenValue sym)
    forall sym a. (Integer -> SEval sym a) -> SeqMap sym a
    indexSeqMap ((Integer -> SEval sym (GenValue sym))
     -> SeqMap sym (GenValue sym))
    -> (Integer -> SEval sym (GenValue sym))
    -> SeqMap sym (GenValue sym)
    forall a b. (a -> b) -> a -> b
    $ \Integer
    i -> do
                  sym -> GenEvalEnv sym -> Expr -> SEval sym (GenValue sym)
    forall sym.
    (?range::Range, EvalPrims sym) =>
    sym -> GenEvalEnv sym -> Expr -> SEval sym (GenValue sym)
    evalExpr sym
    sym (ListEnv sym -> Integer -> GenEvalEnv sym
    forall sym. ListEnv sym -> Integer -> GenEvalEnv sym
    evalListEnv ListEnv sym
    lenv Integer
    i) Expr
    body)

    {-# SPECIALIZE branchEnvs ::
      (?range :: Range, ConcPrims) =>
      Concrete ->
      ListEnv Concrete ->
      [Match] ->
      SEval Concrete (ListEnv Concrete)
      #-}
    -- | Turn a list of matches into the final environments for each iteration of
    -- the branch.
    branchEnvs ::
      (?range :: Range, EvalPrims sym) =>
      sym ->
      ListEnv sym ->
      [Match] ->
      SEval sym (ListEnv sym)
    branchEnvs :: forall sym.
    (?range::Range, EvalPrims sym) =>
    sym -> ListEnv sym -> [Match] -> SEval sym (ListEnv sym)
    branchEnvs sym
    sym ListEnv sym
    env [Match]
    matches = (Integer, ListEnv sym) -> ListEnv sym
    forall a b. (a, b) -> b
    snd ((Integer, ListEnv sym) -> ListEnv sym)
    -> SEval sym (Integer, ListEnv sym) -> SEval sym (ListEnv sym)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> ((Integer, ListEnv sym)
     -> Match -> SEval sym (Integer, ListEnv sym))
    -> (Integer, ListEnv sym)
    -> [Match]
    -> SEval sym (Integer, ListEnv sym)
    forall (t :: * -> *) (m :: * -> *) b a.
    (Foldable t, Monad m) =>
    (b -> a -> m b) -> b -> t a -> m b
    foldM (sym
    -> (Integer, ListEnv sym)
    -> Match
    -> SEval sym (Integer, ListEnv sym)
    forall sym.
    (?range::Range, EvalPrims sym) =>
    sym
    -> (Integer, ListEnv sym)
    -> Match
    -> SEval sym (Integer, ListEnv sym)
    evalMatch sym
    sym) (Integer
    1, ListEnv sym
    env) [Match]
    matches

    {-# SPECIALIZE evalMatch ::
      (?range :: Range, ConcPrims) =>
      Concrete ->
      (Integer, ListEnv Concrete) ->
      Match ->
      SEval Concrete (Integer, ListEnv Concrete)
      #-}

    -- | Turn a match into the list of environments it represents.
    evalMatch ::
      (?range :: Range, EvalPrims sym) =>
      sym ->
      (Integer, ListEnv sym) ->
      Match ->
      SEval sym (Integer, ListEnv sym)
    evalMatch :: forall sym.
    (?range::Range, EvalPrims sym) =>
    sym
    -> (Integer, ListEnv sym)
    -> Match
    -> SEval sym (Integer, ListEnv sym)
    evalMatch sym
    sym (Integer
    lsz, ListEnv sym
    lenv) Match
    m = Integer
    -> SEval sym (Integer, ListEnv sym)
    -> SEval sym (Integer, ListEnv sym)
    forall a b. a -> b -> b
    seq Integer
    lsz (SEval sym (Integer, ListEnv sym)
     -> SEval sym (Integer, ListEnv sym))
    -> SEval sym (Integer, ListEnv sym)
    -> SEval sym (Integer, ListEnv sym)
    forall a b. (a -> b) -> a -> b
    $ case Match
    m of

      -- many envs
      From Name
    n Type
    l Type
    _ty 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 Integer
    nLen -> do
            SeqMap sym (GenValue sym)
    vss <- sym
    -> Nat'
    -> SeqMap sym (GenValue sym)
    -> SEval sym (SeqMap sym (GenValue sym))
    forall sym a.
    Backend sym =>
    sym -> Nat' -> SeqMap sym a -> SEval sym (SeqMap sym a)
    memoMap sym
    sym (Integer -> Nat'
    Nat Integer
    lsz) (SeqMap sym (GenValue sym)
     -> SEval sym (SeqMap sym (GenValue sym)))
    -> SeqMap sym (GenValue sym)
    -> SEval sym (SeqMap sym (GenValue sym))
    forall a b. (a -> b) -> a -> b
    $ (Integer -> SEval sym (GenValue sym)) -> SeqMap sym (GenValue sym)
    forall sym a. (Integer -> SEval sym a) -> SeqMap sym a
    indexSeqMap ((Integer -> SEval sym (GenValue sym))
     -> SeqMap sym (GenValue sym))
    -> (Integer -> SEval sym (GenValue sym))
    -> SeqMap sym (GenValue sym)
    forall a b. (a -> b) -> a -> b
    $ \Integer
    i -> sym -> GenEvalEnv sym -> Expr -> SEval sym (GenValue sym)
    forall sym.
    (?range::Range, EvalPrims sym) =>
    sym -> GenEvalEnv sym -> Expr -> SEval sym (GenValue sym)
    evalExpr sym
    sym (ListEnv sym -> Integer -> GenEvalEnv sym
    forall sym. ListEnv sym -> Integer -> GenEvalEnv sym
    evalListEnv ListEnv sym
    lenv Integer
    i) Expr
    expr
            let stutter :: (Integer -> t) -> Integer -> t
    stutter Integer -> t
    xs = \Integer
    i -> Integer -> t
    xs (Integer
    i Integer -> Integer -> Integer
    forall a. Integral a => a -> a -> a
    `div` Integer
    nLen)
            let lenv' :: ListEnv sym
    lenv' = ListEnv sym
    lenv { leVars :: IntMap (Integer -> SEval sym (GenValue sym))
    leVars = ((Integer -> SEval sym (GenValue sym))
     -> Integer -> SEval sym (GenValue sym))
    -> IntMap (Integer -> SEval sym (GenValue sym))
    -> IntMap (Integer -> SEval sym (GenValue sym))
    forall a b. (a -> b) -> IntMap a -> IntMap b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (Integer -> SEval sym (GenValue sym))
    -> Integer -> SEval sym (GenValue sym)
    forall {t}. (Integer -> t) -> Integer -> t
    stutter (ListEnv sym -> IntMap (Integer -> SEval sym (GenValue sym))
    forall sym.
    ListEnv sym -> IntMap (Integer -> SEval sym (GenValue sym))
    leVars ListEnv sym
    lenv) }
            let vs :: Integer -> SEval sym (GenValue sym)
    vs Integer
    i = do let (Integer
    q, Integer
    r) = Integer
    i Integer -> Integer -> (Integer, Integer)
    forall a. Integral a => a -> a -> (a, a)
    `divMod` Integer
    nLen
                          SeqMap sym (GenValue sym) -> Integer -> SEval sym (GenValue sym)
    forall sym a. Backend sym => SeqMap sym a -> Integer -> SEval sym a
    lookupSeqMap SeqMap sym (GenValue sym)
    vss Integer
    q SEval sym (GenValue sym)
    -> (GenValue sym -> SEval sym (GenValue sym))
    -> SEval sym (GenValue sym)
    forall a b. SEval sym a -> (a -> SEval sym b) -> SEval sym b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \case
                            VWord Integer
    _ WordValue sym
    w   -> SBit sym -> GenValue sym
    forall sym. SBit sym -> GenValue sym
    VBit (SBit sym -> GenValue sym)
    -> SEval sym (SBit sym) -> SEval sym (GenValue sym)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> sym -> WordValue sym -> Integer -> SEval sym (SBit sym)
    forall sym.
    Backend sym =>
    sym -> WordValue sym -> Integer -> SEval sym (SBit sym)
    indexWordValue sym
    sym WordValue sym
    w Integer
    r
                            VSeq Integer
    _ SeqMap sym (GenValue sym)
    xs'  -> SeqMap sym (GenValue sym) -> Integer -> SEval sym (GenValue sym)
    forall sym a. Backend sym => SeqMap sym a -> Integer -> SEval sym a
    lookupSeqMap SeqMap sym (GenValue sym)
    xs' Integer
    r
                            VStream SeqMap sym (GenValue sym)
    xs' -> SeqMap sym (GenValue sym) -> Integer -> SEval sym (GenValue sym)
    forall sym a. Backend sym => SeqMap sym a -> Integer -> SEval sym a
    lookupSeqMap SeqMap sym (GenValue sym)
    xs' Integer
    r
                            GenValue sym
    _           -> String -> [String] -> SEval sym (GenValue sym)
    forall a. HasCallStack => String -> [String] -> a
    evalPanic String
    "evalMatch" [String
    "Not a list value"]
            (Integer, ListEnv sym) -> SEval sym (Integer, ListEnv sym)
    forall a. a -> SEval sym a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Integer
    lsz Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    * Integer
    nLen, Name
    -> (Integer -> SEval sym (GenValue sym))
    -> ListEnv sym
    -> ListEnv sym
    forall sym.
    Name
    -> (Integer -> SEval sym (GenValue sym))
    -> ListEnv sym
    -> ListEnv sym
    bindVarList Name
    n Integer -> SEval sym (GenValue sym)
    vs ListEnv sym
    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.
          Nat'
    Inf -> do
            let allvars :: IntMap (Either (Prim sym) (SEval sym (GenValue sym)))
    allvars = IntMap (Either (Prim sym) (SEval sym (GenValue sym)))
    -> IntMap (Either (Prim sym) (SEval sym (GenValue sym)))
    -> IntMap (Either (Prim sym) (SEval sym (GenValue sym)))
    forall a. IntMap a -> IntMap a -> IntMap a
    IntMap.union (((Integer -> SEval sym (GenValue sym))
     -> Either (Prim sym) (SEval sym (GenValue sym)))
    -> IntMap (Integer -> SEval sym (GenValue sym))
    -> IntMap (Either (Prim sym) (SEval sym (GenValue sym)))
    forall a b. (a -> b) -> IntMap a -> IntMap b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (SEval sym (GenValue sym)
    -> Either (Prim sym) (SEval sym (GenValue sym))
    forall a b. b -> Either a b
    Right (SEval sym (GenValue sym)
     -> Either (Prim sym) (SEval sym (GenValue sym)))
    -> ((Integer -> SEval sym (GenValue sym))
        -> SEval sym (GenValue sym))
    -> (Integer -> SEval sym (GenValue sym))
    -> Either (Prim sym) (SEval sym (GenValue sym))
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ((Integer -> SEval sym (GenValue sym))
    -> Integer -> SEval sym (GenValue sym)
    forall a b. (a -> b) -> a -> b
    $ Integer
    0)) (ListEnv sym -> IntMap (Integer -> SEval sym (GenValue sym))
    forall sym.
    ListEnv sym -> IntMap (Integer -> SEval sym (GenValue sym))
    leVars ListEnv sym
    lenv)) (ListEnv sym
    -> IntMap (Either (Prim sym) (SEval sym (GenValue sym)))
    forall sym.
    ListEnv sym
    -> IntMap (Either (Prim sym) (SEval sym (GenValue sym)))
    leStatic ListEnv sym
    lenv)
            let lenv' :: ListEnv sym
    lenv' = ListEnv sym
    lenv { leVars :: IntMap (Integer -> SEval sym (GenValue sym))
    leVars   = IntMap (Integer -> SEval sym (GenValue sym))
    forall a. IntMap a
    IntMap.empty
                             , leStatic :: IntMap (Either (Prim sym) (SEval sym (GenValue sym)))
    leStatic = IntMap (Either (Prim sym) (SEval sym (GenValue sym)))
    allvars
                             }
            let env :: GenEvalEnv sym
    env   = IntMap (Either (Prim sym) (SEval sym (GenValue sym)))
    -> TypeEnv -> GenEvalEnv sym
    forall sym.
    IntMap (Either (Prim sym) (SEval sym (GenValue sym)))
    -> TypeEnv -> GenEvalEnv sym
    EvalEnv IntMap (Either (Prim sym) (SEval sym (GenValue sym)))
    allvars (ListEnv sym -> TypeEnv
    forall sym. ListEnv sym -> TypeEnv
    leTypes ListEnv sym
    lenv)
            GenValue sym
    xs <- sym -> GenEvalEnv sym -> Expr -> SEval sym (GenValue sym)
    forall sym.
    (?range::Range, EvalPrims sym) =>
    sym -> GenEvalEnv sym -> Expr -> SEval sym (GenValue sym)
    evalExpr sym
    sym GenEvalEnv sym
    env Expr
    expr
            let vs :: Integer -> SEval sym (GenValue sym)
    vs Integer
    i = case GenValue sym
    xs of
                         VWord Integer
    _ WordValue sym
    w   -> SBit sym -> GenValue sym
    forall sym. SBit sym -> GenValue sym
    VBit (SBit sym -> GenValue sym)
    -> SEval sym (SBit sym) -> SEval sym (GenValue sym)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> sym -> WordValue sym -> Integer -> SEval sym (SBit sym)
    forall sym.
    Backend sym =>
    sym -> WordValue sym -> Integer -> SEval sym (SBit sym)
    indexWordValue sym
    sym WordValue sym
    w Integer
    i
                         VSeq Integer
    _ SeqMap sym (GenValue sym)
    xs'  -> SeqMap sym (GenValue sym) -> Integer -> SEval sym (GenValue sym)
    forall sym a. Backend sym => SeqMap sym a -> Integer -> SEval sym a
    lookupSeqMap SeqMap sym (GenValue sym)
    xs' Integer
    i
                         VStream SeqMap sym (GenValue sym)
    xs' -> SeqMap sym (GenValue sym) -> Integer -> SEval sym (GenValue sym)
    forall sym a. Backend sym => SeqMap sym a -> Integer -> SEval sym a
    lookupSeqMap SeqMap sym (GenValue sym)
    xs' Integer
    i
                         GenValue sym
    _           -> String -> [String] -> SEval sym (GenValue sym)
    forall a. HasCallStack => String -> [String] -> a
    evalPanic String
    "evalMatch" [String
    "Not a list value"]
            -- Selecting from an infinite list effectively resets the length of the
            -- list environment, so return 1 as the length
            (Integer, ListEnv sym) -> SEval sym (Integer, ListEnv sym)
    forall a. a -> SEval sym a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Integer
    1, Name
    -> (Integer -> SEval sym (GenValue sym))
    -> ListEnv sym
    -> ListEnv sym
    forall sym.
    Name
    -> (Integer -> SEval sym (GenValue sym))
    -> ListEnv sym
    -> ListEnv sym
    bindVarList Name
    n Integer -> SEval sym (GenValue sym)
    vs ListEnv sym
    lenv')

        where
          len :: Nat'
    len  = TypeEnv -> Type -> Nat'
    evalNumType (ListEnv sym -> TypeEnv
    forall sym. ListEnv sym -> TypeEnv
    leTypes ListEnv sym
    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 Decl
    d -> (Integer, ListEnv sym) -> SEval sym (Integer, ListEnv sym)
    forall a. a -> SEval sym a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Integer
    lsz, Name
    -> (Integer -> SEval sym (GenValue sym))
    -> ListEnv sym
    -> ListEnv sym
    forall sym.
    Name
    -> (Integer -> SEval sym (GenValue sym))
    -> ListEnv sym
    -> ListEnv sym
    bindVarList (Decl -> Name
    dName Decl
    d) (\Integer
    i -> (?range::Range,
     ?evalPrim::PrimIdent -> Maybe (Either Expr (Prim sym)),
     ?callStacks::Bool) =>
    GenEvalEnv sym -> SEval sym (GenValue sym)
    GenEvalEnv sym -> SEval sym (GenValue sym)
    f (ListEnv sym -> Integer -> GenEvalEnv sym
    forall sym. ListEnv sym -> Integer -> GenEvalEnv sym
    evalListEnv ListEnv sym
    lenv Integer
    i)) ListEnv sym
    lenv)
        where
          f :: GenEvalEnv sym -> SEval sym (GenValue sym)
    f GenEvalEnv sym
    env =
              case Decl -> DeclDef
    dDefinition Decl
    d of
                DeclDef
    DPrim      -> String -> [String] -> SEval sym (GenValue sym)
    forall a. HasCallStack => String -> [String] -> a
    evalPanic String
    "evalMatch" [String
    "Unexpected local primitive"]
                DForeign FFIFunType
    _ -> String -> [String] -> SEval sym (GenValue sym)
    forall a. HasCallStack => String -> [String] -> a
    evalPanic String
    "evalMatch" [String
    "Unexpected local foreign"]
                DExpr Expr
    e    -> sym -> GenEvalEnv sym -> Expr -> SEval sym (GenValue sym)
    forall sym.
    (?range::Range, EvalPrims sym) =>
    sym -> GenEvalEnv sym -> Expr -> SEval sym (GenValue sym)
    evalExpr sym
    sym GenEvalEnv sym
    env Expr
    e