-- |
-- 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 #-}

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

import Cryptol.Backend
import Cryptol.Backend.Concrete( Concrete(..) )
import Cryptol.Backend.Monad
import Cryptol.Eval.Generic ( iteValue )
import Cryptol.Eval.Env
import Cryptol.Eval.Type
import Cryptol.Eval.Value
import Cryptol.ModuleSystem.Name
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 Prelude ()
import Prelude.Compat

type EvalEnv = GenEvalEnv Concrete

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

type ConcPrims = ?evalPrim :: PrimIdent -> Maybe (Either Expr (GenValue 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 :: 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]
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)
evalNewtypes sym
sym (Module -> Map Name Newtype
mNewtypes Module
m) GenEvalEnv sym
env

{-# SPECIALIZE evalExpr ::
  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 ::
  EvalPrims sym =>
  sym ->
  GenEvalEnv sym  {- ^ Evaluation environment -} ->
  Expr          {- ^ Expression to evaluate -} ->
  SEval sym (GenValue sym)
evalExpr :: sym -> GenEvalEnv sym -> Expr -> SEval sym (GenValue sym)
evalExpr sym
sym GenEvalEnv sym
env Expr
expr = case Expr
expr of

  -- Try to detect when the user has directly written a finite sequence of
  -- literal bit values and pack these into a word.
  EList [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" #-}
        GenValue sym -> SEval sym (GenValue sym)
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 -> SEval sym (WordValue sym) -> GenValue sym
forall sym. Integer -> SEval sym (WordValue sym) -> GenValue sym
VWord Integer
len (SEval sym (WordValue sym) -> GenValue sym)
-> SEval sym (WordValue sym) -> GenValue sym
forall a b. (a -> b) -> a -> b
$
          case sym -> [SEval sym (GenValue sym)] -> Maybe (SEval sym (SWord sym))
forall sym.
Backend sym =>
sym -> [SEval sym (GenValue sym)] -> Maybe (SEval sym (SWord sym))
tryFromBits sym
sym [SEval sym (GenValue sym)]
vs of
            Just SEval sym (SWord sym)
w  -> SWord sym -> WordValue sym
forall sym. SWord sym -> WordValue sym
WordVal (SWord sym -> WordValue sym)
-> SEval sym (SWord sym) -> SEval sym (WordValue sym)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SEval sym (SWord sym)
w
            Maybe (SEval sym (SWord sym))
Nothing -> 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)
mapM (sym
-> Maybe String
-> SEval sym (GenValue sym)
-> SEval sym (SEval sym (GenValue sym))
forall sym a.
Backend sym =>
sym -> Maybe String -> SEval sym a -> SEval sym (SEval sym a)
sDelay sym
sym Maybe String
forall a. Maybe a
Nothing) [SEval sym (GenValue sym)]
vs
                          WordValue sym -> SEval sym (WordValue sym)
forall (m :: * -> *) a. Monad m => a -> m a
return (WordValue sym -> SEval sym (WordValue sym))
-> WordValue sym -> SEval sym (WordValue sym)
forall a b. (a -> b) -> a -> b
$ Integer -> SeqMap sym -> WordValue sym
forall sym. Integer -> SeqMap sym -> WordValue sym
LargeBitsVal Integer
len (SeqMap sym -> WordValue sym) -> SeqMap sym -> WordValue sym
forall a b. (a -> b) -> a -> b
$ sym -> [SEval sym (GenValue sym)] -> SeqMap sym
forall sym.
Backend sym =>
sym -> [SEval sym (GenValue sym)] -> SeqMap sym
finiteSeqMap sym
sym [SEval sym (GenValue 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)
mapM (sym
-> Maybe String
-> SEval sym (GenValue sym)
-> SEval sym (SEval sym (GenValue sym))
forall sym a.
Backend sym =>
sym -> Maybe String -> SEval sym a -> SEval sym (SEval sym a)
sDelay sym
sym Maybe String
forall a. Maybe a
Nothing) [SEval sym (GenValue sym)]
vs
        GenValue sym -> SEval sym (GenValue sym)
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
forall sym. Integer -> SeqMap sym -> GenValue sym
VSeq Integer
len (SeqMap sym -> GenValue sym) -> SeqMap sym -> GenValue sym
forall a b. (a -> b) -> a -> b
$ sym -> [SEval sym (GenValue sym)] -> SeqMap sym
forall sym.
Backend sym =>
sym -> [SEval sym (GenValue sym)] -> SeqMap sym
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)
mapM (sym
-> Maybe String
-> SEval sym (GenValue sym)
-> SEval sym (SEval sym (GenValue sym))
forall sym a.
Backend sym =>
sym -> Maybe String -> SEval sym a -> SEval sym (SEval sym a)
sDelay sym
sym Maybe String
forall a. Maybe a
Nothing (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 (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)
traverse (sym
-> Maybe String
-> SEval sym (GenValue sym)
-> SEval sym (SEval sym (GenValue sym))
forall sym a.
Backend sym =>
sym -> Maybe String -> SEval sym a -> SEval sym (SEval sym a)
sDelay sym
sym Maybe String
forall a. Maybe a
Nothing (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 (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.
EvalPrims 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.
EvalPrims 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.
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 (SEval sym (GenValue sym))
forall sym.
Name -> GenEvalEnv sym -> Maybe (SEval sym (GenValue sym))
lookupVar Name
n GenEvalEnv sym
env of
      Just SEval sym (GenValue sym)
val -> SEval sym (GenValue sym)
val
      Maybe (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 -> GenValue sym -> SEval sym (GenValue sym)
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
$ (TValue -> SEval sym (GenValue sym)) -> GenValue sym
forall sym. (TValue -> SEval sym (GenValue sym)) -> GenValue sym
VPoly    ((TValue -> SEval sym (GenValue sym)) -> GenValue sym)
-> (TValue -> SEval sym (GenValue sym)) -> GenValue sym
forall a b. (a -> b) -> a -> b
$ \TValue
ty -> sym -> GenEvalEnv sym -> Expr -> SEval sym (GenValue sym)
forall sym.
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  -> GenValue sym -> SEval sym (GenValue sym)
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
$ (Nat' -> SEval sym (GenValue sym)) -> GenValue sym
forall sym. (Nat' -> SEval sym (GenValue sym)) -> GenValue sym
VNumPoly ((Nat' -> SEval sym (GenValue sym)) -> GenValue sym)
-> (Nat' -> SEval sym (GenValue sym)) -> GenValue sym
forall a b. (a -> b) -> a -> b
$ \Nat'
n  -> sym -> GenEvalEnv sym -> Expr -> SEval sym (GenValue sym)
forall sym.
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 (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
      VPoly TValue -> SEval sym (GenValue sym)
f     -> TValue -> SEval 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)
      VNumPoly Nat' -> SEval sym (GenValue sym)
f  -> Nat' -> SEval 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 (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
      VFun SEval sym (GenValue sym) -> SEval sym (GenValue sym)
f' -> SEval sym (GenValue sym) -> SEval 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" #-}
    GenValue sym -> SEval sym (GenValue sym)
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) -> SEval sym (GenValue sym))
-> GenValue sym
forall sym.
(SEval sym (GenValue sym) -> SEval sym (GenValue sym))
-> GenValue sym
VFun (\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.
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.
EvalPrims sym =>
sym -> GenEvalEnv sym -> Expr -> SEval sym (GenValue sym)
evalExpr sym
sym GenEvalEnv sym
env' Expr
e

  where

  {-# INLINE eval #-}
  eval :: Expr -> SEval sym (GenValue sym)
eval = sym -> GenEvalEnv sym -> Expr -> SEval sym (GenValue sym)
forall sym.
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


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

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

evalNewtypes ::
  EvalPrims sym =>
  sym ->
  Map.Map Name Newtype ->
  GenEvalEnv sym ->
  SEval sym (GenEvalEnv sym)
evalNewtypes :: sym
-> Map Name Newtype -> GenEvalEnv sym -> SEval sym (GenEvalEnv sym)
evalNewtypes 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)
evalNewtype 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.
evalNewtype ::
  EvalPrims sym =>
  sym ->
  Newtype ->
  GenEvalEnv sym ->
  SEval sym (GenEvalEnv sym)
evalNewtype :: sym -> Newtype -> GenEvalEnv sym -> SEval sym (GenEvalEnv sym)
evalNewtype sym
sym Newtype
nt = 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 (Newtype -> Name
ntName Newtype
nt) (GenValue sym -> SEval sym (GenValue sym)
forall (m :: * -> *) a. Monad m => a -> m a
return ((TParam -> GenValue sym -> GenValue sym)
-> GenValue sym -> [TParam] -> GenValue sym
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr TParam -> GenValue sym -> GenValue sym
forall sym p. Backend sym => p -> GenValue sym -> GenValue sym
tabs GenValue sym
forall sym. GenValue sym
con (Newtype -> [TParam]
ntParams Newtype
nt)))
  where
  tabs :: p -> GenValue sym -> GenValue sym
tabs p
_tp GenValue sym
body = (TValue -> GenValue sym) -> GenValue sym
forall sym. Backend sym => (TValue -> GenValue sym) -> GenValue sym
tlam (\ TValue
_ -> GenValue sym
body)
  con :: GenValue sym
con           = (SEval sym (GenValue sym) -> SEval sym (GenValue sym))
-> GenValue sym
forall sym.
(SEval sym (GenValue sym) -> SEval sym (GenValue sym))
-> GenValue sym
VFun SEval sym (GenValue sym) -> SEval sym (GenValue sym)
forall a. a -> a
id
{-# INLINE evalNewtype #-}


-- 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 :: 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 :: 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)
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 (SEval sym (GenValue sym))
holeEnv = [(Int, SEval sym (GenValue sym))]
-> IntMap (SEval sym (GenValue sym))
forall a. [(Int, a)] -> IntMap a
IntMap.fromList ([(Int, SEval sym (GenValue sym))]
 -> IntMap (SEval sym (GenValue sym)))
-> [(Int, SEval sym (GenValue sym))]
-> IntMap (SEval sym (GenValue sym))
forall a b. (a -> b) -> a -> b
$ [ (Name -> Int
nameUnique Name
nm, SEval sym (GenValue sym)
h) | (nm,_,h,_) <- [(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 (SEval sym (GenValue sym))
envVars = IntMap (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 (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 :: 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 (SEval sym (GenValue sym))
forall sym.
Name -> GenEvalEnv sym -> Maybe (SEval sym (GenValue sym))
lookupVar Name
nm GenEvalEnv sym
env of
    Maybe (SEval sym (GenValue sym))
Nothing -> 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)]
    Just SEval sym (GenValue sym)
v
     | GenEvalEnv sym -> Schema -> Bool
forall sym. GenEvalEnv sym -> Schema -> Bool
isValueType GenEvalEnv sym
env Schema
sch -> SEval sym (GenValue sym) -> SEval sym ()
fill (SEval sym (GenValue sym) -> SEval sym ())
-> SEval sym (SEval sym (GenValue sym)) -> SEval sym ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< sym
-> SEval sym (GenValue sym)
-> SEval sym (GenValue sym)
-> SEval sym (SEval sym (GenValue sym))
forall sym a.
Backend sym =>
sym -> SEval sym a -> SEval sym a -> SEval sym (SEval sym a)
sDelayFill sym
sym SEval sym (GenValue sym)
v (sym
-> String
-> GenEvalEnv sym
-> Schema
-> SEval sym (GenValue sym)
-> SEval sym (GenValue sym)
forall sym.
Backend sym =>
sym
-> String
-> GenEvalEnv sym
-> Schema
-> SEval sym (GenValue sym)
-> SEval sym (GenValue sym)
etaDelay sym
sym (Doc -> String
forall a. Show a => a -> String
show (Name -> Doc
ppLocName Name
nm)) GenEvalEnv sym
env Schema
sch SEval sym (GenValue sym)
v)
     | Bool
otherwise           -> SEval sym (GenValue sym) -> SEval sym ()
fill (sym
-> String
-> GenEvalEnv sym
-> Schema
-> SEval sym (GenValue sym)
-> SEval sym (GenValue sym)
forall sym.
Backend sym =>
sym
-> String
-> GenEvalEnv sym
-> Schema
-> SEval sym (GenValue sym)
-> SEval sym (GenValue sym)
etaDelay sym
sym (Doc -> String
forall a. Show a => a -> String
show (Name -> Doc
ppLocName Name
nm)) GenEvalEnv sym
env Schema
sch SEval sym (GenValue sym)
v)


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

isValueType GenEvalEnv sym
_ Schema
_ = Bool
False


{-# SPECIALIZE etaWord  ::
  Concrete ->
  Integer ->
  SEval Concrete (GenValue Concrete) ->
  SEval Concrete (WordValue Concrete)
  #-}

-- | Eta-expand a word value.  This forces an unpacked word representation.
etaWord  ::
  Backend sym =>
  sym ->
  Integer ->
  SEval sym (GenValue sym) ->
  SEval sym (WordValue sym)
etaWord :: sym
-> Integer -> SEval sym (GenValue sym) -> SEval sym (WordValue sym)
etaWord sym
sym Integer
n SEval sym (GenValue sym)
val = do
  SEval sym (WordValue sym)
w <- sym
-> Maybe String
-> SEval sym (WordValue sym)
-> SEval sym (SEval sym (WordValue sym))
forall sym a.
Backend sym =>
sym -> Maybe String -> SEval sym a -> SEval sym (SEval sym a)
sDelay sym
sym Maybe String
forall a. Maybe a
Nothing (String -> GenValue sym -> SEval sym (WordValue sym)
forall sym.
Backend sym =>
String -> GenValue sym -> SEval sym (WordValue sym)
fromWordVal String
"during eta-expansion" (GenValue sym -> SEval sym (WordValue sym))
-> SEval sym (GenValue sym) -> SEval sym (WordValue sym)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< SEval sym (GenValue sym)
val)
  SeqMap sym
xs <- SeqMap sym -> SEval sym (SeqMap sym)
forall (m :: * -> *) sym.
(MonadIO m, Backend sym) =>
SeqMap sym -> m (SeqMap sym)
memoMap (SeqMap sym -> SEval sym (SeqMap sym))
-> SeqMap sym -> SEval sym (SeqMap sym)
forall a b. (a -> b) -> a -> b
$ (Integer -> SEval sym (GenValue sym)) -> SeqMap sym
forall sym. (Integer -> SEval sym (GenValue sym)) -> SeqMap sym
IndexSeqMap ((Integer -> SEval sym (GenValue sym)) -> SeqMap sym)
-> (Integer -> SEval sym (GenValue sym)) -> SeqMap sym
forall a b. (a -> b) -> a -> b
$ \Integer
i ->
          do WordValue sym
w' <- SEval sym (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
  WordValue sym -> SEval sym (WordValue sym)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (WordValue sym -> SEval sym (WordValue sym))
-> WordValue sym -> SEval sym (WordValue sym)
forall a b. (a -> b) -> a -> b
$ Integer -> SeqMap sym -> WordValue sym
forall sym. Integer -> SeqMap sym -> WordValue sym
LargeBitsVal Integer
n SeqMap sym
xs

{-# SPECIALIZE etaDelay ::
  Concrete ->
  String ->
  GenEvalEnv Concrete ->
  Schema ->
  SEval Concrete (GenValue Concrete) ->
  SEval Concrete (GenValue Concrete)
  #-}

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

  go :: TValue -> SEval sym (GenValue sym) -> SEval sym (GenValue sym)
go TValue
tp SEval sym (GenValue sym)
x | sym -> SEval sym (GenValue sym) -> Bool
forall sym a. Backend sym => sym -> SEval sym a -> Bool
isReady sym
sym SEval sym (GenValue sym)
x = SEval sym (GenValue sym)
x SEval sym (GenValue sym)
-> (GenValue sym -> SEval sym (GenValue sym))
-> SEval sym (GenValue sym)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
      VBit{}      -> SEval sym (GenValue sym)
x
      VInteger{}  -> SEval sym (GenValue sym)
x
      VWord{}     -> SEval sym (GenValue sym)
x
      VRational{} -> SEval sym (GenValue sym)
x
      VFloat{}    -> SEval sym (GenValue sym)
x
      VSeq Integer
n SeqMap sym
xs ->
        case TValue
tp of
          TVSeq Integer
_nt TValue
el -> GenValue sym -> SEval sym (GenValue sym)
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
forall sym. Integer -> SeqMap sym -> GenValue sym
VSeq Integer
n (SeqMap sym -> GenValue sym) -> SeqMap sym -> GenValue sym
forall a b. (a -> b) -> a -> b
$ (Integer -> SEval sym (GenValue sym)) -> SeqMap sym
forall sym. (Integer -> SEval sym (GenValue sym)) -> SeqMap sym
IndexSeqMap ((Integer -> SEval sym (GenValue sym)) -> SeqMap sym)
-> (Integer -> SEval sym (GenValue sym)) -> SeqMap sym
forall a b. (a -> b) -> a -> b
$ \Integer
i -> TValue -> SEval sym (GenValue sym) -> SEval sym (GenValue sym)
go TValue
el (SeqMap sym -> Integer -> SEval sym (GenValue sym)
forall sym. SeqMap sym -> Integer -> SEval sym (GenValue sym)
lookupSeqMap SeqMap sym
xs Integer
i)
          TValue
_ -> String -> [String] -> SEval sym (GenValue sym)
forall a. HasCallStack => String -> [String] -> a
evalPanic String
"type mismatch during eta-expansion" [String
"Expected sequence type, but got " String -> String -> String
forall a. [a] -> [a] -> [a]
++ TValue -> String
forall a. Show a => a -> String
show TValue
tp]

      VStream SeqMap sym
xs ->
        case TValue
tp of
          TVStream TValue
el -> GenValue sym -> SEval sym (GenValue sym)
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
$ SeqMap sym -> GenValue sym
forall sym. SeqMap sym -> GenValue sym
VStream (SeqMap sym -> GenValue sym) -> SeqMap sym -> GenValue sym
forall a b. (a -> b) -> a -> b
$ (Integer -> SEval sym (GenValue sym)) -> SeqMap sym
forall sym. (Integer -> SEval sym (GenValue sym)) -> SeqMap sym
IndexSeqMap ((Integer -> SEval sym (GenValue sym)) -> SeqMap sym)
-> (Integer -> SEval sym (GenValue sym)) -> SeqMap sym
forall a b. (a -> b) -> a -> b
$ \Integer
i -> TValue -> SEval sym (GenValue sym) -> SEval sym (GenValue sym)
go TValue
el (SeqMap sym -> Integer -> SEval sym (GenValue sym)
forall sym. SeqMap sym -> Integer -> SEval sym (GenValue sym)
lookupSeqMap SeqMap sym
xs Integer
i)
          TValue
_ -> String -> [String] -> SEval sym (GenValue sym)
forall a. HasCallStack => String -> [String] -> a
evalPanic String
"type mismatch during eta-expansion" [String
"Expected stream type, but got " String -> String -> String
forall a. [a] -> [a] -> [a]
++ TValue -> String
forall a. Show a => a -> String
show TValue
tp]

      VTuple [SEval sym (GenValue sym)]
xs ->
        case TValue
tp of
          TVTuple [TValue]
ts | [TValue] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [TValue]
ts Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== [SEval sym (GenValue sym)] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [SEval sym (GenValue sym)]
xs -> GenValue sym -> SEval sym (GenValue sym)
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 ((TValue -> SEval sym (GenValue sym) -> SEval sym (GenValue sym))
-> [TValue]
-> [SEval sym (GenValue sym)]
-> [SEval sym (GenValue sym)]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith TValue -> SEval sym (GenValue sym) -> SEval sym (GenValue sym)
go [TValue]
ts [SEval sym (GenValue sym)]
xs)
          TValue
_ -> String -> [String] -> SEval sym (GenValue sym)
forall a. HasCallStack => String -> [String] -> a
evalPanic String
"type mismatch during eta-expansion" [String
"Expected tuple type with " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show ([SEval sym (GenValue sym)] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [SEval sym (GenValue sym)]
xs)
                                   String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" elements, but got " String -> String -> String
forall a. [a] -> [a] -> [a]
++ TValue -> String
forall a. Show a => a -> String
show TValue
tp]

      VRecord RecordMap Ident (SEval sym (GenValue sym))
fs ->
        case TValue
tp of
          TVRec RecordMap Ident TValue
fts ->
            do let res :: Either
  (Either Ident Ident) (RecordMap Ident (SEval sym (GenValue sym)))
res = (Ident
 -> SEval sym (GenValue sym) -> TValue -> SEval sym (GenValue sym))
-> RecordMap Ident (SEval sym (GenValue sym))
-> RecordMap Ident TValue
-> Either
     (Either Ident Ident) (RecordMap Ident (SEval sym (GenValue sym)))
forall a b c d.
Ord a =>
(a -> b -> c -> d)
-> RecordMap a b
-> RecordMap a c
-> Either (Either a a) (RecordMap a d)
zipRecords (\Ident
_ SEval sym (GenValue sym)
v TValue
t -> TValue -> SEval sym (GenValue sym) -> SEval sym (GenValue sym)
go TValue
t SEval sym (GenValue sym)
v) RecordMap Ident (SEval sym (GenValue sym))
fs RecordMap Ident TValue
fts
               case Either
  (Either Ident Ident) (RecordMap Ident (SEval sym (GenValue sym)))
res of
                 Left (Left Ident
f)  -> String -> [String] -> SEval sym (GenValue sym)
forall a. HasCallStack => String -> [String] -> a
evalPanic String
"type mismatch during eta-expansion" [String
"missing field " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Ident -> String
forall a. Show a => a -> String
show Ident
f]
                 Left (Right Ident
f) -> String -> [String] -> SEval sym (GenValue sym)
forall a. HasCallStack => String -> [String] -> a
evalPanic String
"type mismatch during eta-expansion" [String
"unexpected field " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Ident -> String
forall a. Show a => a -> String
show Ident
f]
                 Right RecordMap Ident (SEval sym (GenValue sym))
fs' -> GenValue sym -> SEval sym (GenValue sym)
forall (m :: * -> *) a. Monad m => a -> m a
return (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))
fs')
          TValue
_ -> String -> [String] -> SEval sym (GenValue sym)
forall a. HasCallStack => String -> [String] -> a
evalPanic String
"type mismatch during eta-expansion" [String
"Expected record type, but got " String -> String -> String
forall a. [a] -> [a] -> [a]
++ TValue -> String
forall a. Show a => a -> String
show TValue
tp]

      VFun SEval sym (GenValue sym) -> SEval sym (GenValue sym)
f ->
        case TValue
tp of
          TVFun TValue
_t1 TValue
t2 -> GenValue sym -> SEval sym (GenValue sym)
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) -> SEval sym (GenValue sym))
-> GenValue sym
forall sym.
(SEval sym (GenValue sym) -> SEval sym (GenValue sym))
-> GenValue sym
VFun ((SEval sym (GenValue sym) -> SEval sym (GenValue sym))
 -> GenValue sym)
-> (SEval sym (GenValue sym) -> SEval sym (GenValue sym))
-> GenValue sym
forall a b. (a -> b) -> a -> b
$ \SEval sym (GenValue sym)
a -> TValue -> SEval sym (GenValue sym) -> SEval sym (GenValue sym)
go TValue
t2 (SEval sym (GenValue sym) -> SEval sym (GenValue sym)
f SEval sym (GenValue sym)
a)
          TValue
_ -> String -> [String] -> SEval sym (GenValue sym)
forall a. HasCallStack => String -> [String] -> a
evalPanic String
"type mismatch during eta-expansion" [String
"Expected function type but got " String -> String -> String
forall a. [a] -> [a] -> [a]
++ TValue -> String
forall a. Show a => a -> String
show TValue
tp]

      VPoly{} ->
        String -> [String] -> SEval sym (GenValue sym)
forall a. HasCallStack => String -> [String] -> a
evalPanic String
"type mismatch during eta-expansion" [String
"Encountered polymorphic value"]

      VNumPoly{} ->
        String -> [String] -> SEval sym (GenValue sym)
forall a. HasCallStack => String -> [String] -> a
evalPanic String
"type mismatch during eta-expansion" [String
"Encountered numeric polymorphic value"]

  go TValue
tp SEval sym (GenValue sym)
v =
    case TValue
tp of
      TValue
TVBit -> SEval sym (GenValue sym)
v
      TValue
TVInteger -> SEval sym (GenValue sym)
v
      TVFloat {} -> SEval sym (GenValue sym)
v
      TVIntMod Integer
_ -> SEval sym (GenValue sym)
v
      TValue
TVRational -> SEval sym (GenValue sym)
v
      TVArray{} -> SEval sym (GenValue sym)
v

      TVSeq Integer
n TValue
TVBit ->
          do SEval sym (WordValue sym)
w <- sym
-> SEval sym (WordValue sym)
-> SEval sym (WordValue sym)
-> SEval sym (SEval sym (WordValue sym))
forall sym a.
Backend sym =>
sym -> SEval sym a -> SEval sym a -> SEval sym (SEval sym a)
sDelayFill sym
sym (String -> GenValue sym -> SEval sym (WordValue sym)
forall sym.
Backend sym =>
String -> GenValue sym -> SEval sym (WordValue sym)
fromWordVal String
"during eta-expansion" (GenValue sym -> SEval sym (WordValue sym))
-> SEval sym (GenValue sym) -> SEval sym (WordValue sym)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< SEval sym (GenValue sym)
v) (sym
-> Integer -> SEval sym (GenValue sym) -> SEval sym (WordValue sym)
forall sym.
Backend sym =>
sym
-> Integer -> SEval sym (GenValue sym) -> SEval sym (WordValue sym)
etaWord sym
sym Integer
n SEval sym (GenValue sym)
v)
             GenValue sym -> SEval sym (GenValue sym)
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 -> SEval sym (WordValue sym) -> GenValue sym
forall sym. Integer -> SEval sym (WordValue sym) -> GenValue sym
VWord Integer
n SEval sym (WordValue sym)
w

      TVSeq Integer
n TValue
el ->
          do SEval sym (SeqMap sym)
x' <- sym
-> Maybe String
-> SEval sym (SeqMap sym)
-> SEval sym (SEval sym (SeqMap sym))
forall sym a.
Backend sym =>
sym -> Maybe String -> SEval sym a -> SEval sym (SEval sym a)
sDelay sym
sym (String -> Maybe String
forall a. a -> Maybe a
Just String
msg) (String -> GenValue sym -> SEval sym (SeqMap sym)
forall sym.
Backend sym =>
String -> GenValue sym -> SEval sym (SeqMap sym)
fromSeq String
"during eta-expansion" (GenValue sym -> SEval sym (SeqMap sym))
-> SEval sym (GenValue sym) -> SEval sym (SeqMap sym)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< SEval sym (GenValue sym)
v)
             GenValue sym -> SEval sym (GenValue sym)
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
forall sym. Integer -> SeqMap sym -> GenValue sym
VSeq Integer
n (SeqMap sym -> GenValue sym) -> SeqMap sym -> GenValue sym
forall a b. (a -> b) -> a -> b
$ (Integer -> SEval sym (GenValue sym)) -> SeqMap sym
forall sym. (Integer -> SEval sym (GenValue sym)) -> SeqMap sym
IndexSeqMap ((Integer -> SEval sym (GenValue sym)) -> SeqMap sym)
-> (Integer -> SEval sym (GenValue sym)) -> SeqMap sym
forall a b. (a -> b) -> a -> b
$ \Integer
i -> do
               TValue -> SEval sym (GenValue sym) -> SEval sym (GenValue sym)
go TValue
el ((SeqMap sym -> Integer -> SEval sym (GenValue sym))
-> Integer -> SeqMap sym -> SEval sym (GenValue sym)
forall a b c. (a -> b -> c) -> b -> a -> c
flip SeqMap sym -> Integer -> SEval sym (GenValue sym)
forall sym. SeqMap sym -> Integer -> SEval sym (GenValue sym)
lookupSeqMap Integer
i (SeqMap sym -> SEval sym (GenValue sym))
-> SEval sym (SeqMap sym) -> SEval sym (GenValue sym)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< SEval sym (SeqMap sym)
x')

      TVStream TValue
el ->
          do SEval sym (SeqMap sym)
x' <- sym
-> Maybe String
-> SEval sym (SeqMap sym)
-> SEval sym (SEval sym (SeqMap sym))
forall sym a.
Backend sym =>
sym -> Maybe String -> SEval sym a -> SEval sym (SEval sym a)
sDelay sym
sym (String -> Maybe String
forall a. a -> Maybe a
Just String
msg) (String -> GenValue sym -> SEval sym (SeqMap sym)
forall sym.
Backend sym =>
String -> GenValue sym -> SEval sym (SeqMap sym)
fromSeq String
"during eta-expansion" (GenValue sym -> SEval sym (SeqMap sym))
-> SEval sym (GenValue sym) -> SEval sym (SeqMap sym)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< SEval sym (GenValue sym)
v)
             GenValue sym -> SEval sym (GenValue sym)
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
$ SeqMap sym -> GenValue sym
forall sym. SeqMap sym -> GenValue sym
VStream (SeqMap sym -> GenValue sym) -> SeqMap sym -> GenValue sym
forall a b. (a -> b) -> a -> b
$ (Integer -> SEval sym (GenValue sym)) -> SeqMap sym
forall sym. (Integer -> SEval sym (GenValue sym)) -> SeqMap sym
IndexSeqMap ((Integer -> SEval sym (GenValue sym)) -> SeqMap sym)
-> (Integer -> SEval sym (GenValue sym)) -> SeqMap sym
forall a b. (a -> b) -> a -> b
$ \Integer
i ->
               TValue -> SEval sym (GenValue sym) -> SEval sym (GenValue sym)
go TValue
el ((SeqMap sym -> Integer -> SEval sym (GenValue sym))
-> Integer -> SeqMap sym -> SEval sym (GenValue sym)
forall a b c. (a -> b -> c) -> b -> a -> c
flip SeqMap sym -> Integer -> SEval sym (GenValue sym)
forall sym. SeqMap sym -> Integer -> SEval sym (GenValue sym)
lookupSeqMap Integer
i (SeqMap sym -> SEval sym (GenValue sym))
-> SEval sym (SeqMap sym) -> SEval sym (GenValue sym)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< SEval sym (SeqMap sym)
x')

      TVFun TValue
_t1 TValue
t2 ->
          do SEval sym (SEval sym (GenValue sym) -> SEval sym (GenValue sym))
v' <- sym
-> Maybe String
-> SEval sym (SEval sym (GenValue sym) -> SEval sym (GenValue sym))
-> SEval
     sym
     (SEval sym (SEval sym (GenValue sym) -> SEval sym (GenValue sym)))
forall sym a.
Backend sym =>
sym -> Maybe String -> SEval sym a -> SEval sym (SEval sym a)
sDelay sym
sym (String -> Maybe String
forall a. a -> Maybe a
Just String
msg) (GenValue sym
-> SEval sym (GenValue sym) -> SEval sym (GenValue sym)
forall sym.
GenValue sym
-> SEval sym (GenValue sym) -> SEval sym (GenValue sym)
fromVFun (GenValue sym
 -> SEval sym (GenValue sym) -> SEval sym (GenValue sym))
-> SEval sym (GenValue sym)
-> SEval sym (SEval sym (GenValue sym) -> SEval sym (GenValue sym))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SEval sym (GenValue sym)
v)
             GenValue sym -> SEval sym (GenValue sym)
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) -> SEval sym (GenValue sym))
-> GenValue sym
forall sym.
(SEval sym (GenValue sym) -> SEval sym (GenValue sym))
-> GenValue sym
VFun ((SEval sym (GenValue sym) -> SEval sym (GenValue sym))
 -> GenValue sym)
-> (SEval sym (GenValue sym) -> SEval sym (GenValue sym))
-> GenValue sym
forall a b. (a -> b) -> a -> b
$ \SEval sym (GenValue sym)
a -> TValue -> SEval sym (GenValue sym) -> SEval sym (GenValue sym)
go TValue
t2 ( ((SEval sym (GenValue sym) -> SEval sym (GenValue sym))
-> SEval sym (GenValue sym) -> SEval sym (GenValue sym)
forall a b. (a -> b) -> a -> b
$SEval sym (GenValue sym)
a) ((SEval sym (GenValue sym) -> SEval sym (GenValue sym))
 -> SEval sym (GenValue sym))
-> SEval 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 (SEval sym (GenValue sym) -> SEval sym (GenValue sym))
v' )

      TVTuple [TValue]
ts ->
          do let n :: Int
n = [TValue] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [TValue]
ts
             SEval sym [SEval sym (GenValue sym)]
v' <- sym
-> Maybe String
-> SEval sym [SEval sym (GenValue sym)]
-> SEval sym (SEval sym [SEval sym (GenValue sym)])
forall sym a.
Backend sym =>
sym -> Maybe String -> SEval sym a -> SEval sym (SEval sym a)
sDelay sym
sym (String -> Maybe String
forall a. a -> Maybe a
Just String
msg) (GenValue sym -> [SEval sym (GenValue sym)]
forall sym. GenValue sym -> [SEval sym (GenValue sym)]
fromVTuple (GenValue sym -> [SEval sym (GenValue sym)])
-> SEval sym (GenValue sym) -> SEval sym [SEval sym (GenValue sym)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SEval sym (GenValue sym)
v)
             GenValue sym -> SEval sym (GenValue sym)
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)] -> GenValue sym)
-> [SEval sym (GenValue sym)] -> GenValue sym
forall a b. (a -> b) -> a -> b
$
                [ TValue -> SEval sym (GenValue sym) -> SEval sym (GenValue sym)
go TValue
t (SEval sym (GenValue sym) -> SEval sym (GenValue sym))
-> SEval 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)] -> Int -> SEval sym (GenValue sym))
-> Int -> [SEval sym (GenValue sym)] -> SEval sym (GenValue sym)
forall a b c. (a -> b -> c) -> b -> a -> c
flip [SEval sym (GenValue sym)] -> Int -> SEval sym (GenValue sym)
forall i a. Integral i => [a] -> i -> a
genericIndex Int
i ([SEval sym (GenValue sym)] -> SEval sym (GenValue sym))
-> SEval sym [SEval sym (GenValue sym)]
-> SEval sym (SEval sym (GenValue sym))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SEval sym [SEval sym (GenValue sym)]
v')
                | Int
i <- [Int
0..(Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1)]
                | TValue
t <- [TValue]
ts
                ]

      TVRec RecordMap Ident TValue
fs ->
          do SEval sym (RecordMap Ident (SEval sym (GenValue sym)))
v' <- sym
-> Maybe String
-> SEval sym (RecordMap Ident (SEval sym (GenValue sym)))
-> SEval
     sym (SEval sym (RecordMap Ident (SEval sym (GenValue sym))))
forall sym a.
Backend sym =>
sym -> Maybe String -> SEval sym a -> SEval sym (SEval sym a)
sDelay sym
sym (String -> Maybe String
forall a. a -> Maybe a
Just String
msg) (GenValue sym -> RecordMap Ident (SEval sym (GenValue sym))
forall sym.
GenValue sym -> RecordMap Ident (SEval sym (GenValue sym))
fromVRecord (GenValue sym -> RecordMap Ident (SEval sym (GenValue sym)))
-> SEval sym (GenValue sym)
-> SEval sym (RecordMap Ident (SEval sym (GenValue sym)))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SEval sym (GenValue sym)
v)
             let err :: a -> a
err a
f = String -> [String] -> a
forall a. HasCallStack => String -> [String] -> a
evalPanic String
"expected record value with field" [a -> String
forall a. Show a => a -> String
show a
f]
             let eta :: Ident -> TValue -> SEval sym (GenValue sym)
eta Ident
f TValue
t = TValue -> SEval sym (GenValue sym) -> SEval sym (GenValue sym)
go TValue
t (SEval sym (GenValue sym) -> SEval sym (GenValue sym))
-> SEval 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)
-> Maybe (SEval sym (GenValue sym)) -> SEval sym (GenValue sym)
forall a. a -> Maybe a -> a
fromMaybe (Ident -> SEval sym (GenValue sym)
forall a a. Show a => a -> a
err Ident
f) (Maybe (SEval sym (GenValue sym)) -> SEval sym (GenValue sym))
-> (RecordMap Ident (SEval sym (GenValue sym))
    -> Maybe (SEval sym (GenValue sym)))
-> RecordMap Ident (SEval sym (GenValue sym))
-> SEval sym (GenValue sym)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Ident
-> RecordMap Ident (SEval sym (GenValue sym))
-> Maybe (SEval sym (GenValue sym))
forall a b. Ord a => a -> RecordMap a b -> Maybe b
lookupField Ident
f (RecordMap Ident (SEval sym (GenValue sym))
 -> SEval sym (GenValue sym))
-> SEval sym (RecordMap Ident (SEval sym (GenValue sym)))
-> SEval sym (SEval sym (GenValue sym))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SEval sym (RecordMap Ident (SEval sym (GenValue sym)))
v')
             GenValue sym -> SEval sym (GenValue sym)
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 ((Ident -> TValue -> SEval sym (GenValue sym))
-> RecordMap Ident TValue
-> RecordMap Ident (SEval sym (GenValue sym))
forall a b c. (a -> b -> c) -> RecordMap a b -> RecordMap a c
mapWithFieldName Ident -> TValue -> SEval sym (GenValue sym)
eta RecordMap Ident TValue
fs)

      TVAbstract {} -> SEval sym (GenValue sym)
v


{-# 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 :: 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)]
    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 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 (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
"<<loop>> while evaluating", Doc -> String
forall a. Show a => a -> String
show (Name -> Doc
forall a. PP a => a -> Doc
pp Name
nm)]


-- | Evaluate a declaration, extending the evaluation environment.
--   Two input environments are given: the first is an environment
--   to use when evaluating the body of the declaration; the second
--   is the environment to extend.  There are two environments to
--   handle the subtle name-binding issues that arise from recursive
--   definitions.  The 'read only' environment is used to bring recursive
--   names into scope while we are still defining them.
evalDecl ::
  EvalPrims 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
-> GenEvalEnv sym
-> GenEvalEnv sym
-> Decl
-> SEval sym (GenEvalEnv sym)
evalDecl sym
sym GenEvalEnv sym
renv GenEvalEnv sym
env Decl
d =
  case Decl -> DeclDef
dDefinition Decl
d of
    DeclDef
DPrim ->
      case ?evalPrim::PrimIdent -> Maybe (Either Expr (GenValue sym))
PrimIdent -> Maybe (Either Expr (GenValue sym))
?evalPrim (PrimIdent -> Maybe (Either Expr (GenValue sym)))
-> Maybe PrimIdent -> Maybe (Either Expr (GenValue 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 GenValue sym
v) -> GenEvalEnv sym -> SEval sym (GenEvalEnv sym)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Name -> GenValue sym -> GenEvalEnv sym -> GenEvalEnv sym
forall sym.
Backend sym =>
Name -> GenValue sym -> GenEvalEnv sym -> GenEvalEnv sym
bindVarDirect (Decl -> Name
dName Decl
d) GenValue sym
v 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.
EvalPrims sym =>
sym -> GenEvalEnv sym -> Expr -> SEval sym (GenValue sym)
evalExpr sym
sym GenEvalEnv sym
renv Expr
ex) GenEvalEnv sym
env
        Maybe (Either Expr (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 -> 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

    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.
EvalPrims sym =>
sym -> GenEvalEnv sym -> Expr -> SEval sym (GenValue sym)
evalExpr sym
sym GenEvalEnv sym
renv Expr
e) GenEvalEnv sym
env


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

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

-- | Apply the the given "selector" form to the given value.  This function pushes
--   tuple and record selections pointwise down into other value constructs
--   (e.g., streams and functions).
evalSel ::
  EvalPrims sym =>
  sym ->
  GenValue sym ->
  Selector ->
  SEval sym (GenValue sym)
evalSel :: 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. [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
vs       -> SeqMap sym -> Integer -> SEval sym (GenValue sym)
forall sym. SeqMap sym -> Integer -> SEval sym (GenValue sym)
lookupSeqMap SeqMap sym
vs (a -> Integer
forall a. Integral a => a -> Integer
toInteger a
n)
      VStream SeqMap sym
vs      -> SeqMap sym -> Integer -> SEval sym (GenValue sym)
forall sym. SeqMap sym -> Integer -> SEval sym (GenValue sym)
lookupSeqMap SeqMap sym
vs (a -> Integer
forall a. Integral a => a -> Integer
toInteger a
n)
      VWord Integer
_ SEval sym (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
<$> ((WordValue sym -> Integer -> SEval sym (SBit sym))
-> Integer -> WordValue sym -> SEval sym (SBit sym)
forall a b c. (a -> b -> c) -> b -> a -> c
flip (sym -> WordValue sym -> Integer -> SEval sym (SBit sym)
forall sym.
Backend sym =>
sym -> WordValue sym -> Integer -> SEval sym (SBit sym)
indexWordValue sym
sym) (a -> Integer
forall a. Integral a => a -> Integer
toInteger a
n) (WordValue sym -> SEval sym (SBit sym))
-> SEval sym (WordValue sym) -> SEval sym (SBit sym)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< SEval sym (WordValue sym)
wv)
      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 ::
  ConcPrims =>
  Concrete -> TValue ->
  GenValue Concrete -> Selector -> SEval Concrete (GenValue Concrete) -> SEval Concrete (GenValue Concrete)
  #-}
evalSetSel :: forall sym.
  EvalPrims sym =>
  sym ->
  TValue ->
  GenValue sym -> Selector -> SEval sym (GenValue sym) -> SEval sym (GenValue sym)
evalSetSel :: 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 (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 (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
mp  -> GenValue sym -> SEval sym (GenValue sym)
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
forall sym. Integer -> SeqMap sym -> GenValue sym
VSeq Integer
i  (SeqMap sym -> GenValue sym) -> SeqMap sym -> GenValue sym
forall a b. (a -> b) -> a -> b
$ SeqMap sym -> Integer -> SEval sym (GenValue sym) -> SeqMap sym
forall sym.
SeqMap sym -> Integer -> SEval sym (GenValue sym) -> SeqMap sym
updateSeqMap SeqMap sym
mp Integer
n SEval sym (GenValue sym)
v
      VStream SeqMap sym
mp -> GenValue sym -> SEval sym (GenValue sym)
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
forall sym. SeqMap sym -> GenValue sym
VStream (SeqMap sym -> GenValue sym) -> SeqMap sym -> GenValue sym
forall a b. (a -> b) -> a -> b
$ SeqMap sym -> Integer -> SEval sym (GenValue sym) -> SeqMap sym
forall sym.
SeqMap sym -> Integer -> SEval sym (GenValue sym) -> SeqMap sym
updateSeqMap SeqMap sym
mp Integer
n SEval sym (GenValue sym)
v
      VWord Integer
i SEval sym (WordValue sym)
m  -> GenValue sym -> SEval sym (GenValue sym)
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 -> SEval sym (WordValue sym) -> GenValue sym
forall sym. Integer -> SEval sym (WordValue sym) -> GenValue sym
VWord Integer
i (SEval sym (WordValue sym) -> GenValue sym)
-> SEval sym (WordValue sym) -> GenValue sym
forall a b. (a -> b) -> a -> b
$ do WordValue sym
m1 <- SEval sym (WordValue sym)
m
                                        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
m1 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 (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
  { ListEnv sym -> IntMap (Integer -> SEval sym (GenValue sym))
leVars   :: !(IntMap.IntMap (Integer -> SEval sym (GenValue sym)))
      -- ^ Bindings whose values vary by position
  , ListEnv sym -> IntMap (SEval sym (GenValue sym))
leStatic :: !(IntMap.IntMap (SEval sym (GenValue sym)))
      -- ^ Bindings whose values are constant
  , ListEnv sym -> TypeEnv
leTypes  :: !TypeEnv
  }

instance Semigroup (ListEnv sym) where
  ListEnv sym
l <> :: ListEnv sym -> ListEnv sym -> ListEnv sym
<> ListEnv sym
r = ListEnv :: forall sym.
IntMap (Integer -> SEval sym (GenValue sym))
-> IntMap (SEval sym (GenValue sym)) -> TypeEnv -> ListEnv sym
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 (SEval sym (GenValue sym))
leStatic = IntMap (SEval sym (GenValue sym))
-> IntMap (SEval sym (GenValue sym))
-> IntMap (SEval sym (GenValue sym))
forall a. IntMap a -> IntMap a -> IntMap a
IntMap.union (ListEnv sym -> IntMap (SEval sym (GenValue sym))
forall sym. ListEnv sym -> IntMap (SEval sym (GenValue sym))
leStatic ListEnv sym
l) (ListEnv sym -> IntMap (SEval sym (GenValue sym))
forall sym. ListEnv sym -> IntMap (SEval sym (GenValue sym))
leStatic ListEnv sym
r)
    , leTypes :: TypeEnv
leTypes  = TypeEnv -> TypeEnv -> TypeEnv
forall a. IntMap a -> IntMap a -> IntMap a
IntMap.union (ListEnv sym -> TypeEnv
forall sym. ListEnv sym -> TypeEnv
leTypes ListEnv sym
l)  (ListEnv sym -> TypeEnv
forall sym. ListEnv sym -> TypeEnv
leTypes ListEnv sym
r)
    }

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

  mappend :: ListEnv sym -> ListEnv sym -> ListEnv sym
mappend ListEnv sym
l ListEnv sym
r = ListEnv sym
l ListEnv sym -> ListEnv sym -> ListEnv sym
forall a. Semigroup a => a -> a -> a
<> ListEnv sym
r

toListEnv :: GenEvalEnv sym -> ListEnv sym
toListEnv :: GenEvalEnv sym -> ListEnv sym
toListEnv GenEvalEnv sym
e =
  ListEnv :: forall sym.
IntMap (Integer -> SEval sym (GenValue sym))
-> IntMap (SEval sym (GenValue sym)) -> TypeEnv -> ListEnv sym
ListEnv
  { leVars :: IntMap (Integer -> SEval sym (GenValue sym))
leVars   = IntMap (Integer -> SEval sym (GenValue sym))
forall a. Monoid a => a
mempty
  , leStatic :: IntMap (SEval sym (GenValue sym))
leStatic = GenEvalEnv sym -> IntMap (SEval sym (GenValue sym))
forall sym. GenEvalEnv sym -> IntMap (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 :: ListEnv sym -> Integer -> GenEvalEnv sym
evalListEnv (ListEnv IntMap (Integer -> SEval sym (GenValue sym))
vm IntMap (SEval sym (GenValue sym))
st TypeEnv
tm) Integer
i =
    let v :: IntMap (SEval sym (GenValue sym))
v = ((Integer -> SEval sym (GenValue sym)) -> SEval sym (GenValue sym))
-> IntMap (Integer -> SEval sym (GenValue sym))
-> IntMap (SEval sym (GenValue sym))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((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 :: forall sym.
IntMap (SEval sym (GenValue sym)) -> TypeEnv -> GenEvalEnv sym
EvalEnv{ envVars :: IntMap (SEval sym (GenValue sym))
envVars = IntMap (SEval sym (GenValue sym))
-> IntMap (SEval sym (GenValue sym))
-> IntMap (SEval sym (GenValue sym))
forall a. IntMap a -> IntMap a -> IntMap a
IntMap.union IntMap (SEval sym (GenValue sym))
v IntMap (SEval sym (GenValue sym))
st
               , envTypes :: TypeEnv
envTypes = TypeEnv
tm
               }
{-# INLINE evalListEnv #-}


bindVarList ::
  Name ->
  (Integer -> SEval sym (GenValue sym)) ->
  ListEnv sym ->
  ListEnv sym
bindVarList :: 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 ::
  ConcPrims =>
  Concrete ->
  GenEvalEnv Concrete ->
  Nat'           ->
  TValue         ->
  Expr           ->
  [[Match]]      ->
  SEval Concrete (GenValue Concrete)
  #-}
-- | Evaluate a comprehension.
evalComp ::
  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 :: 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)
mapM (sym -> ListEnv sym -> [Match] -> SEval sym (ListEnv sym)
forall sym.
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
          Nat' -> TValue -> SeqMap sym -> GenValue sym
forall sym.
Backend sym =>
Nat' -> TValue -> SeqMap sym -> GenValue sym
mkSeq Nat'
len TValue
elty (SeqMap sym -> GenValue sym)
-> SEval sym (SeqMap sym) -> SEval sym (GenValue sym)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SeqMap sym -> SEval sym (SeqMap sym)
forall (m :: * -> *) sym.
(MonadIO m, Backend sym) =>
SeqMap sym -> m (SeqMap sym)
memoMap ((Integer -> SEval sym (GenValue sym)) -> SeqMap sym
forall sym. (Integer -> SEval sym (GenValue sym)) -> SeqMap sym
IndexSeqMap ((Integer -> SEval sym (GenValue sym)) -> SeqMap sym)
-> (Integer -> SEval sym (GenValue sym)) -> SeqMap sym
forall a b. (a -> b) -> a -> b
$ \Integer
i -> do
              sym -> GenEvalEnv sym -> Expr -> SEval sym (GenValue sym)
forall sym.
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 ::
  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 ::
  EvalPrims sym =>
  sym ->
  ListEnv sym ->
  [Match] ->
  SEval sym (ListEnv sym)
branchEnvs :: sym -> ListEnv sym -> [Match] -> SEval sym (ListEnv sym)
branchEnvs sym
sym ListEnv sym
env [Match]
matches = (ListEnv sym -> Match -> SEval sym (ListEnv sym))
-> ListEnv sym -> [Match] -> SEval sym (ListEnv sym)
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM (sym -> ListEnv sym -> Match -> SEval sym (ListEnv sym)
forall sym.
EvalPrims sym =>
sym -> ListEnv sym -> Match -> SEval sym (ListEnv sym)
evalMatch sym
sym) ListEnv sym
env [Match]
matches

{-# SPECIALIZE evalMatch ::
  ConcPrims =>
  Concrete ->
  ListEnv Concrete ->
  Match ->
  SEval Concrete (ListEnv Concrete)
  #-}

-- | Turn a match into the list of environments it represents.
evalMatch ::
  EvalPrims sym =>
  sym ->
  ListEnv sym ->
  Match ->
  SEval sym (ListEnv sym)
evalMatch :: sym -> ListEnv sym -> Match -> SEval sym (ListEnv sym)
evalMatch sym
sym ListEnv sym
lenv Match
m = 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
vss <- SeqMap sym -> SEval sym (SeqMap sym)
forall (m :: * -> *) sym.
(MonadIO m, Backend sym) =>
SeqMap sym -> m (SeqMap sym)
memoMap (SeqMap sym -> SEval sym (SeqMap sym))
-> SeqMap sym -> SEval sym (SeqMap sym)
forall a b. (a -> b) -> a -> b
$ (Integer -> SEval sym (GenValue sym)) -> SeqMap sym
forall sym. (Integer -> SEval sym (GenValue sym)) -> SeqMap sym
IndexSeqMap ((Integer -> SEval sym (GenValue sym)) -> SeqMap sym)
-> (Integer -> SEval sym (GenValue sym)) -> SeqMap sym
forall a b. (a -> b) -> a -> b
$ \Integer
i -> sym -> GenEvalEnv sym -> Expr -> SEval sym (GenValue sym)
forall sym.
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 (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 -> Integer -> SEval sym (GenValue sym)
forall sym. SeqMap sym -> Integer -> SEval sym (GenValue sym)
lookupSeqMap SeqMap sym
vss Integer
q SEval sym (GenValue sym)
-> (GenValue sym -> SEval sym (GenValue sym))
-> SEval sym (GenValue sym)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
                        VWord Integer
_ SEval sym (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
<$> ((WordValue sym -> Integer -> SEval sym (SBit sym))
-> Integer -> WordValue sym -> SEval sym (SBit sym)
forall a b c. (a -> b -> c) -> b -> a -> c
flip (sym -> WordValue sym -> Integer -> SEval sym (SBit sym)
forall sym.
Backend sym =>
sym -> WordValue sym -> Integer -> SEval sym (SBit sym)
indexWordValue sym
sym) Integer
r (WordValue sym -> SEval sym (SBit sym))
-> SEval sym (WordValue sym) -> SEval sym (SBit sym)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< SEval sym (WordValue sym)
w)
                        VSeq Integer
_ SeqMap sym
xs'  -> SeqMap sym -> Integer -> SEval sym (GenValue sym)
forall sym. SeqMap sym -> Integer -> SEval sym (GenValue sym)
lookupSeqMap SeqMap sym
xs' Integer
r
                        VStream SeqMap sym
xs' -> SeqMap sym -> Integer -> SEval sym (GenValue sym)
forall sym. SeqMap sym -> Integer -> SEval sym (GenValue sym)
lookupSeqMap SeqMap 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"]
        ListEnv sym -> SEval sym (ListEnv sym)
forall (m :: * -> *) a. Monad m => a -> m a
return (ListEnv sym -> SEval sym (ListEnv sym))
-> ListEnv sym -> SEval sym (ListEnv sym)
forall a b. (a -> b) -> a -> b
$ 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 (SEval sym (GenValue sym))
allvars = IntMap (SEval sym (GenValue sym))
-> IntMap (SEval sym (GenValue sym))
-> IntMap (SEval sym (GenValue sym))
forall a. IntMap a -> IntMap a -> IntMap a
IntMap.union (((Integer -> SEval sym (GenValue sym)) -> SEval sym (GenValue sym))
-> IntMap (Integer -> SEval sym (GenValue sym))
-> IntMap (SEval sym (GenValue sym))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((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 (SEval sym (GenValue sym))
forall sym. ListEnv sym -> IntMap (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 (SEval sym (GenValue sym))
leStatic = IntMap (SEval sym (GenValue sym))
allvars
                         }
        let env :: GenEvalEnv sym
env   = IntMap (SEval sym (GenValue sym)) -> TypeEnv -> GenEvalEnv sym
forall sym.
IntMap (SEval sym (GenValue sym)) -> TypeEnv -> GenEvalEnv sym
EvalEnv IntMap (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.
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 _ 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
<$> ((WordValue sym -> Integer -> SEval sym (SBit sym))
-> Integer -> WordValue sym -> SEval sym (SBit sym)
forall a b c. (a -> b -> c) -> b -> a -> c
flip (sym -> WordValue sym -> Integer -> SEval sym (SBit sym)
forall sym.
Backend sym =>
sym -> WordValue sym -> Integer -> SEval sym (SBit sym)
indexWordValue sym
sym) Integer
i (WordValue sym -> SEval sym (SBit sym))
-> SEval sym (WordValue sym) -> SEval sym (SBit sym)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< SEval sym (WordValue sym)
w)
                     VSeq _ xs'  -> SeqMap sym -> Integer -> SEval sym (GenValue sym)
forall sym. SeqMap sym -> Integer -> SEval sym (GenValue sym)
lookupSeqMap SeqMap sym
xs' Integer
i
                     VStream xs' -> SeqMap sym -> Integer -> SEval sym (GenValue sym)
forall sym. SeqMap sym -> Integer -> SEval sym (GenValue sym)
lookupSeqMap SeqMap 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"]
        ListEnv sym -> SEval sym (ListEnv sym)
forall (m :: * -> *) a. Monad m => a -> m a
return (ListEnv sym -> SEval sym (ListEnv sym))
-> ListEnv sym -> SEval sym (ListEnv sym)
forall a b. (a -> b) -> a -> b
$ 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 -> ListEnv sym -> SEval sym (ListEnv sym)
forall (m :: * -> *) a. Monad m => a -> m a
return (ListEnv sym -> SEval sym (ListEnv sym))
-> ListEnv sym -> SEval sym (ListEnv sym)
forall a b. (a -> b) -> a -> b
$ 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 -> (?evalPrim::PrimIdent -> Maybe (Either Expr (GenValue sym))) =>
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"]
            DExpr Expr
e -> sym -> GenEvalEnv sym -> Expr -> SEval sym (GenValue sym)
forall sym.
EvalPrims sym =>
sym -> GenEvalEnv sym -> Expr -> SEval sym (GenValue sym)
evalExpr sym
sym GenEvalEnv sym
env Expr
e