{-# LANGUAGE DoAndIfThenElse #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE ParallelListComp #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE Safe #-}
{-# LANGUAGE PatternGuards #-}
module Cryptol.Eval (
moduleEnv
, runEval
, EvalOpts(..)
, PPOpts(..)
, defaultPPOpts
, Eval
, EvalEnv
, emptyEnv
, evalExpr
, evalDecls
, evalSel
, evalSetSel
, EvalError(..)
, forceValue
) where
import Cryptol.Eval.Env
import Cryptol.Eval.Monad
import Cryptol.Eval.Type
import Cryptol.Eval.Value
import Cryptol.Parser.Selector(ppSelector)
import Cryptol.ModuleSystem.Name
import Cryptol.TypeCheck.AST
import Cryptol.TypeCheck.Solver.InfNat(Nat'(..))
import Cryptol.Utils.Panic (panic)
import Cryptol.Utils.PP
import Control.Monad
import qualified Data.Sequence as Seq
import Data.List
import Data.Maybe
import qualified Data.Map.Strict as Map
import Data.Semigroup
import Prelude ()
import Prelude.Compat
type EvalEnv = GenEvalEnv Bool BV Integer
moduleEnv :: EvalPrims b w i
=> Module
-> GenEvalEnv b w i
-> Eval (GenEvalEnv b w i)
moduleEnv :: Module -> GenEvalEnv b w i -> Eval (GenEvalEnv b w i)
moduleEnv m :: Module
m env :: GenEvalEnv b w i
env = [DeclGroup] -> GenEvalEnv b w i -> Eval (GenEvalEnv b w i)
forall b w i.
EvalPrims b w i =>
[DeclGroup] -> GenEvalEnv b w i -> Eval (GenEvalEnv b w i)
evalDecls (Module -> [DeclGroup]
mDecls Module
m) (GenEvalEnv b w i -> Eval (GenEvalEnv b w i))
-> Eval (GenEvalEnv b w i) -> Eval (GenEvalEnv b w i)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Map Name Newtype -> GenEvalEnv b w i -> Eval (GenEvalEnv b w i)
forall b w i.
EvalPrims b w i =>
Map Name Newtype -> GenEvalEnv b w i -> Eval (GenEvalEnv b w i)
evalNewtypes (Module -> Map Name Newtype
mNewtypes Module
m) GenEvalEnv b w i
env
evalExpr :: EvalPrims b w i
=> GenEvalEnv b w i
-> Expr
-> Eval (GenValue b w i)
evalExpr :: GenEvalEnv b w i -> Expr -> Eval (GenValue b w i)
evalExpr env :: GenEvalEnv b w i
env expr :: Expr
expr = case Expr
expr of
EList es :: [Expr]
es ty :: Type
ty
| TValue -> Bool
isTBit TValue
tyv -> {-# SCC "evalExpr->Elist/bit" #-}
GenValue b w i -> Eval (GenValue b w i)
forall (m :: * -> *) a. Monad m => a -> m a
return (GenValue b w i -> Eval (GenValue b w i))
-> GenValue b w i -> Eval (GenValue b w i)
forall a b. (a -> b) -> a -> b
$ Integer -> Eval (WordValue b w i) -> GenValue b w i
forall b w i. Integer -> Eval (WordValue b w i) -> GenValue b w i
VWord Integer
len (Eval (WordValue b w i) -> GenValue b w i)
-> Eval (WordValue b w i) -> GenValue b w i
forall a b. (a -> b) -> a -> b
$
case [Eval (GenValue b w i)] -> Maybe w
forall b w i. BitWord b w i => [Eval (GenValue b w i)] -> Maybe w
tryFromBits [Eval (GenValue b w i)]
vs of
Just w :: w
w -> WordValue b w i -> Eval (WordValue b w i)
forall (m :: * -> *) a. Monad m => a -> m a
return (WordValue b w i -> Eval (WordValue b w i))
-> WordValue b w i -> Eval (WordValue b w i)
forall a b. (a -> b) -> a -> b
$ w -> WordValue b w i
forall b w i. w -> WordValue b w i
WordVal w
w
Nothing -> do [Eval (GenValue b w i)]
xs <- (Eval (GenValue b w i) -> Eval (Eval (GenValue b w i)))
-> [Eval (GenValue b w i)] -> Eval [Eval (GenValue b w i)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Maybe String
-> Eval (GenValue b w i) -> Eval (Eval (GenValue b w i))
forall a. Maybe String -> Eval a -> Eval (Eval a)
delay Maybe String
forall a. Maybe a
Nothing) [Eval (GenValue b w i)]
vs
WordValue b w i -> Eval (WordValue b w i)
forall (m :: * -> *) a. Monad m => a -> m a
return (WordValue b w i -> Eval (WordValue b w i))
-> WordValue b w i -> Eval (WordValue b w i)
forall a b. (a -> b) -> a -> b
$ Seq (Eval b) -> WordValue b w i
forall b w i. Seq (Eval b) -> WordValue b w i
BitsVal (Seq (Eval b) -> WordValue b w i)
-> Seq (Eval b) -> WordValue b w i
forall a b. (a -> b) -> a -> b
$ [Eval b] -> Seq (Eval b)
forall a. [a] -> Seq a
Seq.fromList ([Eval b] -> Seq (Eval b)) -> [Eval b] -> Seq (Eval b)
forall a b. (a -> b) -> a -> b
$ (Eval (GenValue b w i) -> Eval b)
-> [Eval (GenValue b w i)] -> [Eval b]
forall a b. (a -> b) -> [a] -> [b]
map (GenValue b w i -> b
forall b w i. GenValue b w i -> b
fromVBit (GenValue b w i -> b) -> Eval (GenValue b w i) -> Eval b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>) [Eval (GenValue b w i)]
xs
| Bool
otherwise -> {-# SCC "evalExpr->EList" #-} do
[Eval (GenValue b w i)]
xs <- (Eval (GenValue b w i) -> Eval (Eval (GenValue b w i)))
-> [Eval (GenValue b w i)] -> Eval [Eval (GenValue b w i)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Maybe String
-> Eval (GenValue b w i) -> Eval (Eval (GenValue b w i))
forall a. Maybe String -> Eval a -> Eval (Eval a)
delay Maybe String
forall a. Maybe a
Nothing) [Eval (GenValue b w i)]
vs
GenValue b w i -> Eval (GenValue b w i)
forall (m :: * -> *) a. Monad m => a -> m a
return (GenValue b w i -> Eval (GenValue b w i))
-> GenValue b w i -> Eval (GenValue b w i)
forall a b. (a -> b) -> a -> b
$ Integer -> SeqMap b w i -> GenValue b w i
forall b w i. Integer -> SeqMap b w i -> GenValue b w i
VSeq Integer
len (SeqMap b w i -> GenValue b w i) -> SeqMap b w i -> GenValue b w i
forall a b. (a -> b) -> a -> b
$ [Eval (GenValue b w i)] -> SeqMap b w i
forall b w i. [Eval (GenValue b w i)] -> SeqMap b w i
finiteSeqMap [Eval (GenValue b w i)]
xs
where
tyv :: TValue
tyv = HasCallStack => TypeEnv -> Type -> TValue
TypeEnv -> Type -> TValue
evalValType (GenEvalEnv b w i -> TypeEnv
forall b w i. GenEvalEnv b w i -> TypeEnv
envTypes GenEvalEnv b w i
env) Type
ty
vs :: [Eval (GenValue b w i)]
vs = (Expr -> Eval (GenValue b w i))
-> [Expr] -> [Eval (GenValue b w i)]
forall a b. (a -> b) -> [a] -> [b]
map (GenEvalEnv b w i -> Expr -> Eval (GenValue b w i)
forall b w i.
EvalPrims b w i =>
GenEvalEnv b w i -> Expr -> Eval (GenValue b w i)
evalExpr GenEvalEnv b w i
env) [Expr]
es
len :: Integer
len = [Expr] -> Integer
forall i a. Num i => [a] -> i
genericLength [Expr]
es
ETuple es :: [Expr]
es -> {-# SCC "evalExpr->ETuple" #-} do
[Eval (GenValue b w i)]
xs <- (Expr -> Eval (Eval (GenValue b w i)))
-> [Expr] -> Eval [Eval (GenValue b w i)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Maybe String
-> Eval (GenValue b w i) -> Eval (Eval (GenValue b w i))
forall a. Maybe String -> Eval a -> Eval (Eval a)
delay Maybe String
forall a. Maybe a
Nothing (Eval (GenValue b w i) -> Eval (Eval (GenValue b w i)))
-> (Expr -> Eval (GenValue b w i))
-> Expr
-> Eval (Eval (GenValue b w i))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr -> Eval (GenValue b w i)
eval) [Expr]
es
GenValue b w i -> Eval (GenValue b w i)
forall (m :: * -> *) a. Monad m => a -> m a
return (GenValue b w i -> Eval (GenValue b w i))
-> GenValue b w i -> Eval (GenValue b w i)
forall a b. (a -> b) -> a -> b
$ [Eval (GenValue b w i)] -> GenValue b w i
forall b w i. [Eval (GenValue b w i)] -> GenValue b w i
VTuple [Eval (GenValue b w i)]
xs
ERec fields :: [(Ident, Expr)]
fields -> {-# SCC "evalExpr->ERec" #-} do
[(Ident, Eval (GenValue b w i))]
xs <- [Eval (Ident, Eval (GenValue b w i))]
-> Eval [(Ident, Eval (GenValue b w i))]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence [ do Eval (GenValue b w i)
thk <- Maybe String
-> Eval (GenValue b w i) -> Eval (Eval (GenValue b w i))
forall a. Maybe String -> Eval a -> Eval (Eval a)
delay Maybe String
forall a. Maybe a
Nothing (Expr -> Eval (GenValue b w i)
eval Expr
e)
(Ident, Eval (GenValue b w i))
-> Eval (Ident, Eval (GenValue b w i))
forall (m :: * -> *) a. Monad m => a -> m a
return (Ident
f, Eval (GenValue b w i)
thk)
| (f :: Ident
f, e :: Expr
e) <- [(Ident, Expr)]
fields
]
GenValue b w i -> Eval (GenValue b w i)
forall (m :: * -> *) a. Monad m => a -> m a
return (GenValue b w i -> Eval (GenValue b w i))
-> GenValue b w i -> Eval (GenValue b w i)
forall a b. (a -> b) -> a -> b
$ [(Ident, Eval (GenValue b w i))] -> GenValue b w i
forall b w i. [(Ident, Eval (GenValue b w i))] -> GenValue b w i
VRecord [(Ident, Eval (GenValue b w i))]
xs
ESel e :: Expr
e sel :: Selector
sel -> {-# SCC "evalExpr->ESel" #-} do
GenValue b w i
x <- Expr -> Eval (GenValue b w i)
eval Expr
e
GenValue b w i -> Selector -> Eval (GenValue b w i)
forall b w i.
EvalPrims b w i =>
GenValue b w i -> Selector -> Eval (GenValue b w i)
evalSel GenValue b w i
x Selector
sel
ESet e :: Expr
e sel :: Selector
sel v :: Expr
v -> {-# SCC "evalExpr->ESet" #-}
do GenValue b w i
x <- Expr -> Eval (GenValue b w i)
eval Expr
e
GenValue b w i
-> Selector -> Eval (GenValue b w i) -> Eval (GenValue b w i)
forall b w i.
EvalPrims b w i =>
GenValue b w i
-> Selector -> Eval (GenValue b w i) -> Eval (GenValue b w i)
evalSetSel GenValue b w i
x Selector
sel (Expr -> Eval (GenValue b w i)
eval Expr
v)
EIf c :: Expr
c t :: Expr
t f :: Expr
f -> {-# SCC "evalExpr->EIf" #-} do
b
b <- GenValue b w i -> b
forall b w i. GenValue b w i -> b
fromVBit (GenValue b w i -> b) -> Eval (GenValue b w i) -> Eval b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr -> Eval (GenValue b w i)
eval Expr
c
b
-> Eval (GenValue b w i)
-> Eval (GenValue b w i)
-> Eval (GenValue b w i)
forall b w i.
EvalPrims b w i =>
b
-> Eval (GenValue b w i)
-> Eval (GenValue b w i)
-> Eval (GenValue b w i)
iteValue b
b (Expr -> Eval (GenValue b w i)
eval Expr
t) (Expr -> Eval (GenValue b w i)
eval Expr
f)
EComp n :: Type
n t :: Type
t h :: Expr
h gs :: [[Match]]
gs -> {-# SCC "evalExpr->EComp" #-} do
let len :: Nat'
len = HasCallStack => TypeEnv -> Type -> Nat'
TypeEnv -> Type -> Nat'
evalNumType (GenEvalEnv b w i -> TypeEnv
forall b w i. GenEvalEnv b w i -> TypeEnv
envTypes GenEvalEnv b w i
env) Type
n
let elty :: TValue
elty = HasCallStack => TypeEnv -> Type -> TValue
TypeEnv -> Type -> TValue
evalValType (GenEvalEnv b w i -> TypeEnv
forall b w i. GenEvalEnv b w i -> TypeEnv
envTypes GenEvalEnv b w i
env) Type
t
GenEvalEnv b w i
-> Nat' -> TValue -> Expr -> [[Match]] -> Eval (GenValue b w i)
forall b w i.
EvalPrims b w i =>
GenEvalEnv b w i
-> Nat' -> TValue -> Expr -> [[Match]] -> Eval (GenValue b w i)
evalComp GenEvalEnv b w i
env Nat'
len TValue
elty Expr
h [[Match]]
gs
EVar n :: Name
n -> {-# SCC "evalExpr->EVar" #-} do
case Name -> GenEvalEnv b w i -> Maybe (Eval (GenValue b w i))
forall b w i.
Name -> GenEvalEnv b w i -> Maybe (Eval (GenValue b w i))
lookupVar Name
n GenEvalEnv b w i
env of
Just val :: Eval (GenValue b w i)
val -> Eval (GenValue b w i)
val
Nothing -> do
Doc
envdoc <- PPOpts -> GenEvalEnv b w i -> Eval Doc
forall b w i.
BitWord b w i =>
PPOpts -> GenEvalEnv b w i -> Eval Doc
ppEnv PPOpts
defaultPPOpts GenEvalEnv b w i
env
String -> [String] -> Eval (GenValue b w i)
forall a. HasCallStack => String -> [String] -> a
panic "[Eval] evalExpr"
["var `" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Doc -> String
forall a. Show a => a -> String
show (Name -> Doc
forall a. PP a => a -> Doc
pp Name
n) String -> String -> String
forall a. [a] -> [a] -> [a]
++ "` is not defined"
, Doc -> String
forall a. Show a => a -> String
show Doc
envdoc
]
ETAbs tv :: TParam
tv b :: Expr
b -> {-# SCC "evalExpr->ETAbs" #-}
case TParam -> Kind
tpKind TParam
tv of
KType -> GenValue b w i -> Eval (GenValue b w i)
forall (m :: * -> *) a. Monad m => a -> m a
return (GenValue b w i -> Eval (GenValue b w i))
-> GenValue b w i -> Eval (GenValue b w i)
forall a b. (a -> b) -> a -> b
$ (TValue -> Eval (GenValue b w i)) -> GenValue b w i
forall b w i. (TValue -> Eval (GenValue b w i)) -> GenValue b w i
VPoly ((TValue -> Eval (GenValue b w i)) -> GenValue b w i)
-> (TValue -> Eval (GenValue b w i)) -> GenValue b w i
forall a b. (a -> b) -> a -> b
$ \ty :: TValue
ty -> GenEvalEnv b w i -> Expr -> Eval (GenValue b w i)
forall b w i.
EvalPrims b w i =>
GenEvalEnv b w i -> Expr -> Eval (GenValue b w i)
evalExpr (TVar -> Either Nat' TValue -> GenEvalEnv b w i -> GenEvalEnv b w i
forall b w i.
TVar -> Either Nat' TValue -> GenEvalEnv b w i -> GenEvalEnv b w i
bindType (TParam -> TVar
tpVar TParam
tv) (TValue -> Either Nat' TValue
forall a b. b -> Either a b
Right TValue
ty) GenEvalEnv b w i
env) Expr
b
KNum -> GenValue b w i -> Eval (GenValue b w i)
forall (m :: * -> *) a. Monad m => a -> m a
return (GenValue b w i -> Eval (GenValue b w i))
-> GenValue b w i -> Eval (GenValue b w i)
forall a b. (a -> b) -> a -> b
$ (Nat' -> Eval (GenValue b w i)) -> GenValue b w i
forall b w i. (Nat' -> Eval (GenValue b w i)) -> GenValue b w i
VNumPoly ((Nat' -> Eval (GenValue b w i)) -> GenValue b w i)
-> (Nat' -> Eval (GenValue b w i)) -> GenValue b w i
forall a b. (a -> b) -> a -> b
$ \n :: Nat'
n -> GenEvalEnv b w i -> Expr -> Eval (GenValue b w i)
forall b w i.
EvalPrims b w i =>
GenEvalEnv b w i -> Expr -> Eval (GenValue b w i)
evalExpr (TVar -> Either Nat' TValue -> GenEvalEnv b w i -> GenEvalEnv b w i
forall b w i.
TVar -> Either Nat' TValue -> GenEvalEnv b w i -> GenEvalEnv b w i
bindType (TParam -> TVar
tpVar TParam
tv) (Nat' -> Either Nat' TValue
forall a b. a -> Either a b
Left Nat'
n) GenEvalEnv b w i
env) Expr
b
k :: Kind
k -> String -> [String] -> Eval (GenValue b w i)
forall a. HasCallStack => String -> [String] -> a
panic "[Eval] evalExpr" ["invalid kind on type abstraction", Kind -> String
forall a. Show a => a -> String
show Kind
k]
ETApp e :: Expr
e ty :: Type
ty -> {-# SCC "evalExpr->ETApp" #-} do
Expr -> Eval (GenValue b w i)
eval Expr
e Eval (GenValue b w i)
-> (GenValue b w i -> Eval (GenValue b w i))
-> Eval (GenValue b w i)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
VPoly f :: TValue -> Eval (GenValue b w i)
f -> TValue -> Eval (GenValue b w i)
f (TValue -> Eval (GenValue b w i))
-> TValue -> Eval (GenValue b w i)
forall a b. (a -> b) -> a -> b
$! (HasCallStack => TypeEnv -> Type -> TValue
TypeEnv -> Type -> TValue
evalValType (GenEvalEnv b w i -> TypeEnv
forall b w i. GenEvalEnv b w i -> TypeEnv
envTypes GenEvalEnv b w i
env) Type
ty)
VNumPoly f :: Nat' -> Eval (GenValue b w i)
f -> Nat' -> Eval (GenValue b w i)
f (Nat' -> Eval (GenValue b w i)) -> Nat' -> Eval (GenValue b w i)
forall a b. (a -> b) -> a -> b
$! (HasCallStack => TypeEnv -> Type -> Nat'
TypeEnv -> Type -> Nat'
evalNumType (GenEvalEnv b w i -> TypeEnv
forall b w i. GenEvalEnv b w i -> TypeEnv
envTypes GenEvalEnv b w i
env) Type
ty)
val :: GenValue b w i
val -> do Doc
vdoc <- GenValue b w i -> Eval Doc
ppV GenValue b w i
val
String -> [String] -> Eval (GenValue b w i)
forall a. HasCallStack => String -> [String] -> a
panic "[Eval] evalExpr"
["expected a polymorphic value"
, Doc -> String
forall a. Show a => a -> String
show Doc
vdoc, Doc -> String
forall a. Show a => a -> String
show (Expr -> Doc
forall a. PP a => a -> Doc
pp Expr
e), Doc -> String
forall a. Show a => a -> String
show (Type -> Doc
forall a. PP a => a -> Doc
pp Type
ty)
]
EApp f :: Expr
f x :: Expr
x -> {-# SCC "evalExpr->EApp" #-} do
Expr -> Eval (GenValue b w i)
eval Expr
f Eval (GenValue b w i)
-> (GenValue b w i -> Eval (GenValue b w i))
-> Eval (GenValue b w i)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
VFun f' :: Eval (GenValue b w i) -> Eval (GenValue b w i)
f' -> Eval (GenValue b w i) -> Eval (GenValue b w i)
f' (Expr -> Eval (GenValue b w i)
eval Expr
x)
it :: GenValue b w i
it -> do Doc
itdoc <- GenValue b w i -> Eval Doc
ppV GenValue b w i
it
String -> [String] -> Eval (GenValue b w i)
forall a. HasCallStack => String -> [String] -> a
panic "[Eval] evalExpr" ["not a function", Doc -> String
forall a. Show a => a -> String
show Doc
itdoc ]
EAbs n :: Name
n _ty :: Type
_ty b :: Expr
b -> {-# SCC "evalExpr->EAbs" #-}
GenValue b w i -> Eval (GenValue b w i)
forall (m :: * -> *) a. Monad m => a -> m a
return (GenValue b w i -> Eval (GenValue b w i))
-> GenValue b w i -> Eval (GenValue b w i)
forall a b. (a -> b) -> a -> b
$ (Eval (GenValue b w i) -> Eval (GenValue b w i)) -> GenValue b w i
forall b w i.
(Eval (GenValue b w i) -> Eval (GenValue b w i)) -> GenValue b w i
VFun (\v :: Eval (GenValue b w i)
v -> do GenEvalEnv b w i
env' <- Name
-> Eval (GenValue b w i)
-> GenEvalEnv b w i
-> Eval (GenEvalEnv b w i)
forall b w i.
Name
-> Eval (GenValue b w i)
-> GenEvalEnv b w i
-> Eval (GenEvalEnv b w i)
bindVar Name
n Eval (GenValue b w i)
v GenEvalEnv b w i
env
GenEvalEnv b w i -> Expr -> Eval (GenValue b w i)
forall b w i.
EvalPrims b w i =>
GenEvalEnv b w i -> Expr -> Eval (GenValue b w i)
evalExpr GenEvalEnv b w i
env' Expr
b)
EProofAbs _ e :: Expr
e -> GenEvalEnv b w i -> Expr -> Eval (GenValue b w i)
forall b w i.
EvalPrims b w i =>
GenEvalEnv b w i -> Expr -> Eval (GenValue b w i)
evalExpr GenEvalEnv b w i
env Expr
e
EProofApp e :: Expr
e -> GenEvalEnv b w i -> Expr -> Eval (GenValue b w i)
forall b w i.
EvalPrims b w i =>
GenEvalEnv b w i -> Expr -> Eval (GenValue b w i)
evalExpr GenEvalEnv b w i
env Expr
e
EWhere e :: Expr
e ds :: [DeclGroup]
ds -> {-# SCC "evalExpr->EWhere" #-} do
GenEvalEnv b w i
env' <- [DeclGroup] -> GenEvalEnv b w i -> Eval (GenEvalEnv b w i)
forall b w i.
EvalPrims b w i =>
[DeclGroup] -> GenEvalEnv b w i -> Eval (GenEvalEnv b w i)
evalDecls [DeclGroup]
ds GenEvalEnv b w i
env
GenEvalEnv b w i -> Expr -> Eval (GenValue b w i)
forall b w i.
EvalPrims b w i =>
GenEvalEnv b w i -> Expr -> Eval (GenValue b w i)
evalExpr GenEvalEnv b w i
env' Expr
e
where
{-# INLINE eval #-}
eval :: Expr -> Eval (GenValue b w i)
eval = GenEvalEnv b w i -> Expr -> Eval (GenValue b w i)
forall b w i.
EvalPrims b w i =>
GenEvalEnv b w i -> Expr -> Eval (GenValue b w i)
evalExpr GenEvalEnv b w i
env
ppV :: GenValue b w i -> Eval Doc
ppV = PPOpts -> GenValue b w i -> Eval Doc
forall b w i. BitWord b w i => PPOpts -> GenValue b w i -> Eval Doc
ppValue PPOpts
defaultPPOpts
evalNewtypes :: EvalPrims b w i
=> Map.Map Name Newtype
-> GenEvalEnv b w i
-> Eval (GenEvalEnv b w i)
evalNewtypes :: Map Name Newtype -> GenEvalEnv b w i -> Eval (GenEvalEnv b w i)
evalNewtypes nts :: Map Name Newtype
nts env :: GenEvalEnv b w i
env = (GenEvalEnv b w i -> Newtype -> Eval (GenEvalEnv b w i))
-> GenEvalEnv b w i -> [Newtype] -> Eval (GenEvalEnv b w i)
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM ((Newtype -> GenEvalEnv b w i -> Eval (GenEvalEnv b w i))
-> GenEvalEnv b w i -> Newtype -> Eval (GenEvalEnv b w i)
forall a b c. (a -> b -> c) -> b -> a -> c
flip Newtype -> GenEvalEnv b w i -> Eval (GenEvalEnv b w i)
forall b w i.
EvalPrims b w i =>
Newtype -> GenEvalEnv b w i -> Eval (GenEvalEnv b w i)
evalNewtype) GenEvalEnv b w i
env ([Newtype] -> Eval (GenEvalEnv b w i))
-> [Newtype] -> Eval (GenEvalEnv b w i)
forall a b. (a -> b) -> a -> b
$ Map Name Newtype -> [Newtype]
forall k a. Map k a -> [a]
Map.elems Map Name Newtype
nts
evalNewtype :: EvalPrims b w i
=> Newtype
-> GenEvalEnv b w i
-> Eval (GenEvalEnv b w i)
evalNewtype :: Newtype -> GenEvalEnv b w i -> Eval (GenEvalEnv b w i)
evalNewtype nt :: Newtype
nt = Name
-> Eval (GenValue b w i)
-> GenEvalEnv b w i
-> Eval (GenEvalEnv b w i)
forall b w i.
Name
-> Eval (GenValue b w i)
-> GenEvalEnv b w i
-> Eval (GenEvalEnv b w i)
bindVar (Newtype -> Name
ntName Newtype
nt) (GenValue b w i -> Eval (GenValue b w i)
forall (m :: * -> *) a. Monad m => a -> m a
return ((TParam -> GenValue b w i -> GenValue b w i)
-> GenValue b w i -> [TParam] -> GenValue b w i
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr TParam -> GenValue b w i -> GenValue b w i
forall p b w i. p -> GenValue b w i -> GenValue b w i
tabs GenValue b w i
forall b w i. GenValue b w i
con (Newtype -> [TParam]
ntParams Newtype
nt)))
where
tabs :: p -> GenValue b w i -> GenValue b w i
tabs _tp :: p
_tp body :: GenValue b w i
body = (TValue -> GenValue b w i) -> GenValue b w i
forall b w i. (TValue -> GenValue b w i) -> GenValue b w i
tlam (\ _ -> GenValue b w i
body)
con :: GenValue b w i
con = (Eval (GenValue b w i) -> Eval (GenValue b w i)) -> GenValue b w i
forall b w i.
(Eval (GenValue b w i) -> Eval (GenValue b w i)) -> GenValue b w i
VFun Eval (GenValue b w i) -> Eval (GenValue b w i)
forall a. a -> a
id
evalDecls :: EvalPrims b w i
=> [DeclGroup]
-> GenEvalEnv b w i
-> Eval (GenEvalEnv b w i)
evalDecls :: [DeclGroup] -> GenEvalEnv b w i -> Eval (GenEvalEnv b w i)
evalDecls dgs :: [DeclGroup]
dgs env :: GenEvalEnv b w i
env = (GenEvalEnv b w i -> DeclGroup -> Eval (GenEvalEnv b w i))
-> GenEvalEnv b w i -> [DeclGroup] -> Eval (GenEvalEnv b w i)
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM GenEvalEnv b w i -> DeclGroup -> Eval (GenEvalEnv b w i)
forall b w i.
EvalPrims b w i =>
GenEvalEnv b w i -> DeclGroup -> Eval (GenEvalEnv b w i)
evalDeclGroup GenEvalEnv b w i
env [DeclGroup]
dgs
evalDeclGroup :: EvalPrims b w i
=> GenEvalEnv b w i
-> DeclGroup
-> Eval (GenEvalEnv b w i)
evalDeclGroup :: GenEvalEnv b w i -> DeclGroup -> Eval (GenEvalEnv b w i)
evalDeclGroup env :: GenEvalEnv b w i
env dg :: DeclGroup
dg = do
case DeclGroup
dg of
Recursive ds :: [Decl]
ds -> do
[(Name, Schema, Eval (GenValue b w i),
Eval (GenValue b w i) -> Eval ())]
holes <- (Decl
-> Eval
(Name, Schema, Eval (GenValue b w i),
Eval (GenValue b w i) -> Eval ()))
-> [Decl]
-> Eval
[(Name, Schema, Eval (GenValue b w i),
Eval (GenValue b w i) -> Eval ())]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Decl
-> Eval
(Name, Schema, Eval (GenValue b w i),
Eval (GenValue b w i) -> Eval ())
forall b w i.
Decl
-> Eval
(Name, Schema, Eval (GenValue b w i),
Eval (GenValue b w i) -> Eval ())
declHole [Decl]
ds
let holeEnv :: Map Name (Eval (GenValue b w i))
holeEnv = [(Name, Eval (GenValue b w i))] -> Map Name (Eval (GenValue b w i))
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ([(Name, Eval (GenValue b w i))]
-> Map Name (Eval (GenValue b w i)))
-> [(Name, Eval (GenValue b w i))]
-> Map Name (Eval (GenValue b w i))
forall a b. (a -> b) -> a -> b
$ [ (Name
nm,Eval (GenValue b w i)
h) | (nm :: Name
nm,_,h :: Eval (GenValue b w i)
h,_) <- [(Name, Schema, Eval (GenValue b w i),
Eval (GenValue b w i) -> Eval ())]
holes ]
let env' :: GenEvalEnv b w i
env' = GenEvalEnv b w i
env GenEvalEnv b w i -> GenEvalEnv b w i -> GenEvalEnv b w i
forall a. Monoid a => a -> a -> a
`mappend` GenEvalEnv Any Any Any
forall b w i. GenEvalEnv b w i
emptyEnv{ envVars :: Map Name (Eval (GenValue b w i))
envVars = Map Name (Eval (GenValue b w i))
holeEnv }
GenEvalEnv b w i
env'' <- (GenEvalEnv b w i -> Decl -> Eval (GenEvalEnv b w i))
-> GenEvalEnv b w i -> [Decl] -> Eval (GenEvalEnv b w i)
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM (GenEvalEnv b w i
-> GenEvalEnv b w i -> Decl -> Eval (GenEvalEnv b w i)
forall b w i.
EvalPrims b w i =>
GenEvalEnv b w i
-> GenEvalEnv b w i -> Decl -> Eval (GenEvalEnv b w i)
evalDecl GenEvalEnv b w i
env') GenEvalEnv b w i
env [Decl]
ds
((Name, Schema, Eval (GenValue b w i),
Eval (GenValue b w i) -> Eval ())
-> Eval ())
-> [(Name, Schema, Eval (GenValue b w i),
Eval (GenValue b w i) -> Eval ())]
-> Eval ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (GenEvalEnv b w i
-> (Name, Schema, Eval (GenValue b w i),
Eval (GenValue b w i) -> Eval ())
-> Eval ()
forall b w i.
BitWord b w i =>
GenEvalEnv b w i
-> (Name, Schema, Eval (GenValue b w i),
Eval (GenValue b w i) -> Eval ())
-> Eval ()
fillHole GenEvalEnv b w i
env'') [(Name, Schema, Eval (GenValue b w i),
Eval (GenValue b w i) -> Eval ())]
holes
GenEvalEnv b w i -> Eval (GenEvalEnv b w i)
forall (m :: * -> *) a. Monad m => a -> m a
return GenEvalEnv b w i
env'
NonRecursive d :: Decl
d -> do
GenEvalEnv b w i
-> GenEvalEnv b w i -> Decl -> Eval (GenEvalEnv b w i)
forall b w i.
EvalPrims b w i =>
GenEvalEnv b w i
-> GenEvalEnv b w i -> Decl -> Eval (GenEvalEnv b w i)
evalDecl GenEvalEnv b w i
env GenEvalEnv b w i
env Decl
d
fillHole :: BitWord b w i
=> GenEvalEnv b w i
-> (Name, Schema, Eval (GenValue b w i), Eval (GenValue b w i) -> Eval ())
-> Eval ()
fillHole :: GenEvalEnv b w i
-> (Name, Schema, Eval (GenValue b w i),
Eval (GenValue b w i) -> Eval ())
-> Eval ()
fillHole env :: GenEvalEnv b w i
env (nm :: Name
nm, sch :: Schema
sch, _, fill :: Eval (GenValue b w i) -> Eval ()
fill) = do
case Name -> GenEvalEnv b w i -> Maybe (Eval (GenValue b w i))
forall b w i.
Name -> GenEvalEnv b w i -> Maybe (Eval (GenValue b w i))
lookupVar Name
nm GenEvalEnv b w i
env of
Nothing -> String -> [String] -> Eval ()
forall a. HasCallStack => String -> [String] -> a
evalPanic "fillHole" ["Recursive definition not completed", Doc -> String
forall a. Show a => a -> String
show (Name -> Doc
ppLocName Name
nm)]
Just x :: Eval (GenValue b w i)
x
| GenEvalEnv b w i -> Schema -> Bool
forall b w i. GenEvalEnv b w i -> Schema -> Bool
isValueType GenEvalEnv b w i
env Schema
sch -> Eval (GenValue b w i) -> Eval ()
fill (Eval (GenValue b w i) -> Eval ())
-> Eval (Eval (GenValue b w i)) -> Eval ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Eval (GenValue b w i)
-> Eval (GenValue b w i) -> Eval (Eval (GenValue b w i))
forall a. Eval a -> Eval a -> Eval (Eval a)
delayFill Eval (GenValue b w i)
x (String
-> GenEvalEnv b w i
-> Schema
-> Eval (GenValue b w i)
-> Eval (GenValue b w i)
forall b w i.
BitWord b w i =>
String
-> GenEvalEnv b w i
-> Schema
-> Eval (GenValue b w i)
-> Eval (GenValue b w i)
etaDelay (Doc -> String
forall a. Show a => a -> String
show (Name -> Doc
ppLocName Name
nm)) GenEvalEnv b w i
env Schema
sch Eval (GenValue b w i)
x)
| Bool
otherwise -> Eval (GenValue b w i) -> Eval ()
fill (String
-> GenEvalEnv b w i
-> Schema
-> Eval (GenValue b w i)
-> Eval (GenValue b w i)
forall b w i.
BitWord b w i =>
String
-> GenEvalEnv b w i
-> Schema
-> Eval (GenValue b w i)
-> Eval (GenValue b w i)
etaDelay (Doc -> String
forall a. Show a => a -> String
show (Name -> Doc
ppLocName Name
nm)) GenEvalEnv b w i
env Schema
sch Eval (GenValue b w i)
x)
isValueType :: GenEvalEnv b w i -> Schema -> Bool
isValueType :: GenEvalEnv b w i -> Schema -> Bool
isValueType env :: GenEvalEnv b w i
env Forall{ sVars :: Schema -> [TParam]
sVars = [], sProps :: Schema -> [Type]
sProps = [], sType :: Schema -> Type
sType = Type
t0 }
= TValue -> Bool
go (HasCallStack => TypeEnv -> Type -> TValue
TypeEnv -> Type -> TValue
evalValType (GenEvalEnv b w i -> TypeEnv
forall b w i. GenEvalEnv b w i -> TypeEnv
envTypes GenEvalEnv b w i
env) Type
t0)
where
go :: TValue -> Bool
go TVBit = Bool
True
go (TVSeq _ x :: TValue
x) = TValue -> Bool
go TValue
x
go (TVTuple xs :: [TValue]
xs) = [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and ((TValue -> Bool) -> [TValue] -> [Bool]
forall a b. (a -> b) -> [a] -> [b]
map TValue -> Bool
go [TValue]
xs)
go (TVRec xs :: [(Ident, TValue)]
xs) = [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and (((Ident, TValue) -> Bool) -> [(Ident, TValue)] -> [Bool]
forall a b. (a -> b) -> [a] -> [b]
map (TValue -> Bool
go (TValue -> Bool)
-> ((Ident, TValue) -> TValue) -> (Ident, TValue) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Ident, TValue) -> TValue
forall a b. (a, b) -> b
snd) [(Ident, TValue)]
xs)
go _ = Bool
False
isValueType _ _ = Bool
False
etaWord :: BitWord b w i
=> Integer
-> Eval (GenValue b w i)
-> Eval (WordValue b w i)
etaWord :: Integer -> Eval (GenValue b w i) -> Eval (WordValue b w i)
etaWord n :: Integer
n x :: Eval (GenValue b w i)
x = do
Eval (WordValue b w i)
w <- Maybe String
-> Eval (WordValue b w i) -> Eval (Eval (WordValue b w i))
forall a. Maybe String -> Eval a -> Eval (Eval a)
delay Maybe String
forall a. Maybe a
Nothing (String -> GenValue b w i -> Eval (WordValue b w i)
forall b w i. String -> GenValue b w i -> Eval (WordValue b w i)
fromWordVal "during eta-expansion" (GenValue b w i -> Eval (WordValue b w i))
-> Eval (GenValue b w i) -> Eval (WordValue b w i)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Eval (GenValue b w i)
x)
WordValue b w i -> Eval (WordValue b w i)
forall (m :: * -> *) a. Monad m => a -> m a
return (WordValue b w i -> Eval (WordValue b w i))
-> WordValue b w i -> Eval (WordValue b w i)
forall a b. (a -> b) -> a -> b
$ Seq (Eval b) -> WordValue b w i
forall b w i. Seq (Eval b) -> WordValue b w i
BitsVal (Seq (Eval b) -> WordValue b w i)
-> Seq (Eval b) -> WordValue b w i
forall a b. (a -> b) -> a -> b
$ Int -> (Int -> Eval b) -> Seq (Eval b)
forall a. Int -> (Int -> a) -> Seq a
Seq.fromFunction (Integer -> Int
forall a. Num a => Integer -> a
fromInteger Integer
n) ((Int -> Eval b) -> Seq (Eval b))
-> (Int -> Eval b) -> Seq (Eval b)
forall a b. (a -> b) -> a -> b
$ \i :: Int
i ->
do WordValue b w i
w' <- Eval (WordValue b w i)
w; WordValue b w i -> Integer -> Eval b
forall b w i. BitWord b w i => WordValue b w i -> Integer -> Eval b
indexWordValue WordValue b w i
w' (Int -> Integer
forall a. Integral a => a -> Integer
toInteger Int
i)
etaDelay :: BitWord b w i
=> String
-> GenEvalEnv b w i
-> Schema
-> Eval (GenValue b w i)
-> Eval (GenValue b w i)
etaDelay :: String
-> GenEvalEnv b w i
-> Schema
-> Eval (GenValue b w i)
-> Eval (GenValue b w i)
etaDelay msg :: String
msg env0 :: GenEvalEnv b w i
env0 Forall{ sVars :: Schema -> [TParam]
sVars = [TParam]
vs0, sType :: Schema -> Type
sType = Type
tp0 } = GenEvalEnv b w i
-> [TParam] -> Eval (GenValue b w i) -> Eval (GenValue b w i)
forall b w i b w i.
BitWord b w i =>
GenEvalEnv b w i
-> [TParam] -> Eval (GenValue b w i) -> Eval (GenValue b w i)
goTpVars GenEvalEnv b w i
env0 [TParam]
vs0
where
goTpVars :: GenEvalEnv b w i
-> [TParam] -> Eval (GenValue b w i) -> Eval (GenValue b w i)
goTpVars env :: GenEvalEnv b w i
env [] x :: Eval (GenValue b w i)
x = TValue -> Eval (GenValue b w i) -> Eval (GenValue b w i)
forall b w i.
BitWord b w i =>
TValue -> Eval (GenValue b w i) -> Eval (GenValue b w i)
go (HasCallStack => TypeEnv -> Type -> TValue
TypeEnv -> Type -> TValue
evalValType (GenEvalEnv b w i -> TypeEnv
forall b w i. GenEvalEnv b w i -> TypeEnv
envTypes GenEvalEnv b w i
env) Type
tp0) Eval (GenValue b w i)
x
goTpVars env :: GenEvalEnv b w i
env (v :: TParam
v:vs :: [TParam]
vs) x :: Eval (GenValue b w i)
x =
case TParam -> Kind
tpKind TParam
v of
KType -> GenValue b w i -> Eval (GenValue b w i)
forall (m :: * -> *) a. Monad m => a -> m a
return (GenValue b w i -> Eval (GenValue b w i))
-> GenValue b w i -> Eval (GenValue b w i)
forall a b. (a -> b) -> a -> b
$ (TValue -> Eval (GenValue b w i)) -> GenValue b w i
forall b w i. (TValue -> Eval (GenValue b w i)) -> GenValue b w i
VPoly ((TValue -> Eval (GenValue b w i)) -> GenValue b w i)
-> (TValue -> Eval (GenValue b w i)) -> GenValue b w i
forall a b. (a -> b) -> a -> b
$ \t :: TValue
t ->
GenEvalEnv b w i
-> [TParam] -> Eval (GenValue b w i) -> Eval (GenValue b w i)
goTpVars (TVar -> Either Nat' TValue -> GenEvalEnv b w i -> GenEvalEnv b w i
forall b w i.
TVar -> Either Nat' TValue -> GenEvalEnv b w i -> GenEvalEnv b w i
bindType (TParam -> TVar
tpVar TParam
v) (TValue -> Either Nat' TValue
forall a b. b -> Either a b
Right TValue
t) GenEvalEnv b w i
env) [TParam]
vs ( ((TValue -> Eval (GenValue b w i))
-> TValue -> Eval (GenValue b w i)
forall a b. (a -> b) -> a -> b
$TValue
t) ((TValue -> Eval (GenValue b w i)) -> Eval (GenValue b w i))
-> (GenValue b w i -> TValue -> Eval (GenValue b w i))
-> GenValue b w i
-> Eval (GenValue b w i)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. GenValue b w i -> TValue -> Eval (GenValue b w i)
forall b w i. GenValue b w i -> TValue -> Eval (GenValue b w i)
fromVPoly (GenValue b w i -> Eval (GenValue b w i))
-> Eval (GenValue b w i) -> Eval (GenValue b w i)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Eval (GenValue b w i)
x )
KNum -> GenValue b w i -> Eval (GenValue b w i)
forall (m :: * -> *) a. Monad m => a -> m a
return (GenValue b w i -> Eval (GenValue b w i))
-> GenValue b w i -> Eval (GenValue b w i)
forall a b. (a -> b) -> a -> b
$ (Nat' -> Eval (GenValue b w i)) -> GenValue b w i
forall b w i. (Nat' -> Eval (GenValue b w i)) -> GenValue b w i
VNumPoly ((Nat' -> Eval (GenValue b w i)) -> GenValue b w i)
-> (Nat' -> Eval (GenValue b w i)) -> GenValue b w i
forall a b. (a -> b) -> a -> b
$ \n :: Nat'
n ->
GenEvalEnv b w i
-> [TParam] -> Eval (GenValue b w i) -> Eval (GenValue b w i)
goTpVars (TVar -> Either Nat' TValue -> GenEvalEnv b w i -> GenEvalEnv b w i
forall b w i.
TVar -> Either Nat' TValue -> GenEvalEnv b w i -> GenEvalEnv b w i
bindType (TParam -> TVar
tpVar TParam
v) (Nat' -> Either Nat' TValue
forall a b. a -> Either a b
Left Nat'
n) GenEvalEnv b w i
env) [TParam]
vs ( ((Nat' -> Eval (GenValue b w i)) -> Nat' -> Eval (GenValue b w i)
forall a b. (a -> b) -> a -> b
$Nat'
n) ((Nat' -> Eval (GenValue b w i)) -> Eval (GenValue b w i))
-> (GenValue b w i -> Nat' -> Eval (GenValue b w i))
-> GenValue b w i
-> Eval (GenValue b w i)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. GenValue b w i -> Nat' -> Eval (GenValue b w i)
forall b w i. GenValue b w i -> Nat' -> Eval (GenValue b w i)
fromVNumPoly (GenValue b w i -> Eval (GenValue b w i))
-> Eval (GenValue b w i) -> Eval (GenValue b w i)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Eval (GenValue b w i)
x )
k :: Kind
k -> String -> [String] -> Eval (GenValue b w i)
forall a. HasCallStack => String -> [String] -> a
panic "[Eval] etaDelay" ["invalid kind on type abstraction", Kind -> String
forall a. Show a => a -> String
show Kind
k]
go :: TValue -> Eval (GenValue b w i) -> Eval (GenValue b w i)
go tp :: TValue
tp (Ready x :: GenValue b w i
x) =
case GenValue b w i
x of
VBit _ -> GenValue b w i -> Eval (GenValue b w i)
forall (m :: * -> *) a. Monad m => a -> m a
return GenValue b w i
x
VInteger _ -> GenValue b w i -> Eval (GenValue b w i)
forall (m :: * -> *) a. Monad m => a -> m a
return GenValue b w i
x
VWord _ _ -> GenValue b w i -> Eval (GenValue b w i)
forall (m :: * -> *) a. Monad m => a -> m a
return GenValue b w i
x
VSeq n :: Integer
n xs :: SeqMap b w i
xs
| TVSeq _nt :: Integer
_nt el :: TValue
el <- TValue
tp
-> GenValue b w i -> Eval (GenValue b w i)
forall (m :: * -> *) a. Monad m => a -> m a
return (GenValue b w i -> Eval (GenValue b w i))
-> GenValue b w i -> Eval (GenValue b w i)
forall a b. (a -> b) -> a -> b
$ Integer -> SeqMap b w i -> GenValue b w i
forall b w i. Integer -> SeqMap b w i -> GenValue b w i
VSeq Integer
n (SeqMap b w i -> GenValue b w i) -> SeqMap b w i -> GenValue b w i
forall a b. (a -> b) -> a -> b
$ (Integer -> Eval (GenValue b w i)) -> SeqMap b w i
forall b w i. (Integer -> Eval (GenValue b w i)) -> SeqMap b w i
IndexSeqMap ((Integer -> Eval (GenValue b w i)) -> SeqMap b w i)
-> (Integer -> Eval (GenValue b w i)) -> SeqMap b w i
forall a b. (a -> b) -> a -> b
$ \i :: Integer
i -> TValue -> Eval (GenValue b w i) -> Eval (GenValue b w i)
go TValue
el (SeqMap b w i -> Integer -> Eval (GenValue b w i)
forall b w i. SeqMap b w i -> Integer -> Eval (GenValue b w i)
lookupSeqMap SeqMap b w i
xs Integer
i)
VStream xs :: SeqMap b w i
xs
| TVStream el :: TValue
el <- TValue
tp
-> GenValue b w i -> Eval (GenValue b w i)
forall (m :: * -> *) a. Monad m => a -> m a
return (GenValue b w i -> Eval (GenValue b w i))
-> GenValue b w i -> Eval (GenValue b w i)
forall a b. (a -> b) -> a -> b
$ SeqMap b w i -> GenValue b w i
forall b w i. SeqMap b w i -> GenValue b w i
VStream (SeqMap b w i -> GenValue b w i) -> SeqMap b w i -> GenValue b w i
forall a b. (a -> b) -> a -> b
$ (Integer -> Eval (GenValue b w i)) -> SeqMap b w i
forall b w i. (Integer -> Eval (GenValue b w i)) -> SeqMap b w i
IndexSeqMap ((Integer -> Eval (GenValue b w i)) -> SeqMap b w i)
-> (Integer -> Eval (GenValue b w i)) -> SeqMap b w i
forall a b. (a -> b) -> a -> b
$ \i :: Integer
i -> TValue -> Eval (GenValue b w i) -> Eval (GenValue b w i)
go TValue
el (SeqMap b w i -> Integer -> Eval (GenValue b w i)
forall b w i. SeqMap b w i -> Integer -> Eval (GenValue b w i)
lookupSeqMap SeqMap b w i
xs Integer
i)
VTuple xs :: [Eval (GenValue b w i)]
xs
| TVTuple ts :: [TValue]
ts <- TValue
tp
-> GenValue b w i -> Eval (GenValue b w i)
forall (m :: * -> *) a. Monad m => a -> m a
return (GenValue b w i -> Eval (GenValue b w i))
-> GenValue b w i -> Eval (GenValue b w i)
forall a b. (a -> b) -> a -> b
$ [Eval (GenValue b w i)] -> GenValue b w i
forall b w i. [Eval (GenValue b w i)] -> GenValue b w i
VTuple ((TValue -> Eval (GenValue b w i) -> Eval (GenValue b w i))
-> [TValue] -> [Eval (GenValue b w i)] -> [Eval (GenValue b w i)]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith TValue -> Eval (GenValue b w i) -> Eval (GenValue b w i)
go [TValue]
ts [Eval (GenValue b w i)]
xs)
VRecord fs :: [(Ident, Eval (GenValue b w i))]
fs
| TVRec fts :: [(Ident, TValue)]
fts <- TValue
tp
-> GenValue b w i -> Eval (GenValue b w i)
forall (m :: * -> *) a. Monad m => a -> m a
return (GenValue b w i -> Eval (GenValue b w i))
-> GenValue b w i -> Eval (GenValue b w i)
forall a b. (a -> b) -> a -> b
$ [(Ident, Eval (GenValue b w i))] -> GenValue b w i
forall b w i. [(Ident, Eval (GenValue b w i))] -> GenValue b w i
VRecord ([(Ident, Eval (GenValue b w i))] -> GenValue b w i)
-> [(Ident, Eval (GenValue b w i))] -> GenValue b w i
forall a b. (a -> b) -> a -> b
$
let err :: a -> a
err f :: a
f = String -> [String] -> a
forall a. HasCallStack => String -> [String] -> a
evalPanic "expected record value with field" [a -> String
forall a. Show a => a -> String
show a
f] in
[ (Ident
f, TValue -> Eval (GenValue b w i) -> Eval (GenValue b w i)
go (TValue -> Maybe TValue -> TValue
forall a. a -> Maybe a -> a
fromMaybe (Ident -> TValue
forall a a. Show a => a -> a
err Ident
f) (Ident -> [(Ident, TValue)] -> Maybe TValue
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Ident
f [(Ident, TValue)]
fts)) Eval (GenValue b w i)
y)
| (f :: Ident
f, y :: Eval (GenValue b w i)
y) <- [(Ident, Eval (GenValue b w i))]
fs
]
VFun f :: Eval (GenValue b w i) -> Eval (GenValue b w i)
f
| TVFun _t1 :: TValue
_t1 t2 :: TValue
t2 <- TValue
tp
-> GenValue b w i -> Eval (GenValue b w i)
forall (m :: * -> *) a. Monad m => a -> m a
return (GenValue b w i -> Eval (GenValue b w i))
-> GenValue b w i -> Eval (GenValue b w i)
forall a b. (a -> b) -> a -> b
$ (Eval (GenValue b w i) -> Eval (GenValue b w i)) -> GenValue b w i
forall b w i.
(Eval (GenValue b w i) -> Eval (GenValue b w i)) -> GenValue b w i
VFun ((Eval (GenValue b w i) -> Eval (GenValue b w i))
-> GenValue b w i)
-> (Eval (GenValue b w i) -> Eval (GenValue b w i))
-> GenValue b w i
forall a b. (a -> b) -> a -> b
$ \a :: Eval (GenValue b w i)
a -> TValue -> Eval (GenValue b w i) -> Eval (GenValue b w i)
go TValue
t2 (Eval (GenValue b w i) -> Eval (GenValue b w i)
f Eval (GenValue b w i)
a)
_ -> String -> [String] -> Eval (GenValue b w i)
forall a. HasCallStack => String -> [String] -> a
evalPanic "type mismatch during eta-expansion" []
go tp :: TValue
tp x :: Eval (GenValue b w i)
x =
case TValue
tp of
TVBit -> Eval (GenValue b w i)
x
TVInteger -> Eval (GenValue b w i)
x
TVIntMod _ -> Eval (GenValue b w i)
x
TVSeq n :: Integer
n TVBit ->
do Eval (WordValue b w i)
w <- Eval (WordValue b w i)
-> Eval (WordValue b w i) -> Eval (Eval (WordValue b w i))
forall a. Eval a -> Eval a -> Eval (Eval a)
delayFill (String -> GenValue b w i -> Eval (WordValue b w i)
forall b w i. String -> GenValue b w i -> Eval (WordValue b w i)
fromWordVal "during eta-expansion" (GenValue b w i -> Eval (WordValue b w i))
-> Eval (GenValue b w i) -> Eval (WordValue b w i)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Eval (GenValue b w i)
x) (Integer -> Eval (GenValue b w i) -> Eval (WordValue b w i)
forall b w i.
BitWord b w i =>
Integer -> Eval (GenValue b w i) -> Eval (WordValue b w i)
etaWord Integer
n Eval (GenValue b w i)
x)
GenValue b w i -> Eval (GenValue b w i)
forall (m :: * -> *) a. Monad m => a -> m a
return (GenValue b w i -> Eval (GenValue b w i))
-> GenValue b w i -> Eval (GenValue b w i)
forall a b. (a -> b) -> a -> b
$ Integer -> Eval (WordValue b w i) -> GenValue b w i
forall b w i. Integer -> Eval (WordValue b w i) -> GenValue b w i
VWord Integer
n Eval (WordValue b w i)
w
TVSeq n :: Integer
n el :: TValue
el ->
do Eval (SeqMap b w i)
x' <- Maybe String -> Eval (SeqMap b w i) -> Eval (Eval (SeqMap b w i))
forall a. Maybe String -> Eval a -> Eval (Eval a)
delay (String -> Maybe String
forall a. a -> Maybe a
Just String
msg) (String -> GenValue b w i -> Eval (SeqMap b w i)
forall b w i.
BitWord b w i =>
String -> GenValue b w i -> Eval (SeqMap b w i)
fromSeq "during eta-expansion" (GenValue b w i -> Eval (SeqMap b w i))
-> Eval (GenValue b w i) -> Eval (SeqMap b w i)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Eval (GenValue b w i)
x)
GenValue b w i -> Eval (GenValue b w i)
forall (m :: * -> *) a. Monad m => a -> m a
return (GenValue b w i -> Eval (GenValue b w i))
-> GenValue b w i -> Eval (GenValue b w i)
forall a b. (a -> b) -> a -> b
$ Integer -> SeqMap b w i -> GenValue b w i
forall b w i. Integer -> SeqMap b w i -> GenValue b w i
VSeq Integer
n (SeqMap b w i -> GenValue b w i) -> SeqMap b w i -> GenValue b w i
forall a b. (a -> b) -> a -> b
$ (Integer -> Eval (GenValue b w i)) -> SeqMap b w i
forall b w i. (Integer -> Eval (GenValue b w i)) -> SeqMap b w i
IndexSeqMap ((Integer -> Eval (GenValue b w i)) -> SeqMap b w i)
-> (Integer -> Eval (GenValue b w i)) -> SeqMap b w i
forall a b. (a -> b) -> a -> b
$ \i :: Integer
i -> do
TValue -> Eval (GenValue b w i) -> Eval (GenValue b w i)
go TValue
el ((SeqMap b w i -> Integer -> Eval (GenValue b w i))
-> Integer -> SeqMap b w i -> Eval (GenValue b w i)
forall a b c. (a -> b -> c) -> b -> a -> c
flip SeqMap b w i -> Integer -> Eval (GenValue b w i)
forall b w i. SeqMap b w i -> Integer -> Eval (GenValue b w i)
lookupSeqMap Integer
i (SeqMap b w i -> Eval (GenValue b w i))
-> Eval (SeqMap b w i) -> Eval (GenValue b w i)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Eval (SeqMap b w i)
x')
TVStream el :: TValue
el ->
do Eval (SeqMap b w i)
x' <- Maybe String -> Eval (SeqMap b w i) -> Eval (Eval (SeqMap b w i))
forall a. Maybe String -> Eval a -> Eval (Eval a)
delay (String -> Maybe String
forall a. a -> Maybe a
Just String
msg) (String -> GenValue b w i -> Eval (SeqMap b w i)
forall b w i.
BitWord b w i =>
String -> GenValue b w i -> Eval (SeqMap b w i)
fromSeq "during eta-expansion" (GenValue b w i -> Eval (SeqMap b w i))
-> Eval (GenValue b w i) -> Eval (SeqMap b w i)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Eval (GenValue b w i)
x)
GenValue b w i -> Eval (GenValue b w i)
forall (m :: * -> *) a. Monad m => a -> m a
return (GenValue b w i -> Eval (GenValue b w i))
-> GenValue b w i -> Eval (GenValue b w i)
forall a b. (a -> b) -> a -> b
$ SeqMap b w i -> GenValue b w i
forall b w i. SeqMap b w i -> GenValue b w i
VStream (SeqMap b w i -> GenValue b w i) -> SeqMap b w i -> GenValue b w i
forall a b. (a -> b) -> a -> b
$ (Integer -> Eval (GenValue b w i)) -> SeqMap b w i
forall b w i. (Integer -> Eval (GenValue b w i)) -> SeqMap b w i
IndexSeqMap ((Integer -> Eval (GenValue b w i)) -> SeqMap b w i)
-> (Integer -> Eval (GenValue b w i)) -> SeqMap b w i
forall a b. (a -> b) -> a -> b
$ \i :: Integer
i ->
TValue -> Eval (GenValue b w i) -> Eval (GenValue b w i)
go TValue
el ((SeqMap b w i -> Integer -> Eval (GenValue b w i))
-> Integer -> SeqMap b w i -> Eval (GenValue b w i)
forall a b c. (a -> b -> c) -> b -> a -> c
flip SeqMap b w i -> Integer -> Eval (GenValue b w i)
forall b w i. SeqMap b w i -> Integer -> Eval (GenValue b w i)
lookupSeqMap Integer
i (SeqMap b w i -> Eval (GenValue b w i))
-> Eval (SeqMap b w i) -> Eval (GenValue b w i)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Eval (SeqMap b w i)
x')
TVFun _t1 :: TValue
_t1 t2 :: TValue
t2 ->
do Eval (Eval (GenValue b w i) -> Eval (GenValue b w i))
x' <- Maybe String
-> Eval (Eval (GenValue b w i) -> Eval (GenValue b w i))
-> Eval (Eval (Eval (GenValue b w i) -> Eval (GenValue b w i)))
forall a. Maybe String -> Eval a -> Eval (Eval a)
delay (String -> Maybe String
forall a. a -> Maybe a
Just String
msg) (GenValue b w i -> Eval (GenValue b w i) -> Eval (GenValue b w i)
forall b w i.
GenValue b w i -> Eval (GenValue b w i) -> Eval (GenValue b w i)
fromVFun (GenValue b w i -> Eval (GenValue b w i) -> Eval (GenValue b w i))
-> Eval (GenValue b w i)
-> Eval (Eval (GenValue b w i) -> Eval (GenValue b w i))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Eval (GenValue b w i)
x)
GenValue b w i -> Eval (GenValue b w i)
forall (m :: * -> *) a. Monad m => a -> m a
return (GenValue b w i -> Eval (GenValue b w i))
-> GenValue b w i -> Eval (GenValue b w i)
forall a b. (a -> b) -> a -> b
$ (Eval (GenValue b w i) -> Eval (GenValue b w i)) -> GenValue b w i
forall b w i.
(Eval (GenValue b w i) -> Eval (GenValue b w i)) -> GenValue b w i
VFun ((Eval (GenValue b w i) -> Eval (GenValue b w i))
-> GenValue b w i)
-> (Eval (GenValue b w i) -> Eval (GenValue b w i))
-> GenValue b w i
forall a b. (a -> b) -> a -> b
$ \a :: Eval (GenValue b w i)
a -> TValue -> Eval (GenValue b w i) -> Eval (GenValue b w i)
go TValue
t2 ( ((Eval (GenValue b w i) -> Eval (GenValue b w i))
-> Eval (GenValue b w i) -> Eval (GenValue b w i)
forall a b. (a -> b) -> a -> b
$Eval (GenValue b w i)
a) ((Eval (GenValue b w i) -> Eval (GenValue b w i))
-> Eval (GenValue b w i))
-> Eval (Eval (GenValue b w i) -> Eval (GenValue b w i))
-> Eval (GenValue b w i)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Eval (Eval (GenValue b w i) -> Eval (GenValue b w i))
x' )
TVTuple ts :: [TValue]
ts ->
do let n :: Int
n = [TValue] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [TValue]
ts
Eval [Eval (GenValue b w i)]
x' <- Maybe String
-> Eval [Eval (GenValue b w i)]
-> Eval (Eval [Eval (GenValue b w i)])
forall a. Maybe String -> Eval a -> Eval (Eval a)
delay (String -> Maybe String
forall a. a -> Maybe a
Just String
msg) (GenValue b w i -> [Eval (GenValue b w i)]
forall b w i. GenValue b w i -> [Eval (GenValue b w i)]
fromVTuple (GenValue b w i -> [Eval (GenValue b w i)])
-> Eval (GenValue b w i) -> Eval [Eval (GenValue b w i)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Eval (GenValue b w i)
x)
GenValue b w i -> Eval (GenValue b w i)
forall (m :: * -> *) a. Monad m => a -> m a
return (GenValue b w i -> Eval (GenValue b w i))
-> GenValue b w i -> Eval (GenValue b w i)
forall a b. (a -> b) -> a -> b
$ [Eval (GenValue b w i)] -> GenValue b w i
forall b w i. [Eval (GenValue b w i)] -> GenValue b w i
VTuple ([Eval (GenValue b w i)] -> GenValue b w i)
-> [Eval (GenValue b w i)] -> GenValue b w i
forall a b. (a -> b) -> a -> b
$
[ TValue -> Eval (GenValue b w i) -> Eval (GenValue b w i)
go TValue
t (Eval (GenValue b w i) -> Eval (GenValue b w i))
-> Eval (Eval (GenValue b w i)) -> Eval (GenValue b w i)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< (([Eval (GenValue b w i)] -> Int -> Eval (GenValue b w i))
-> Int -> [Eval (GenValue b w i)] -> Eval (GenValue b w i)
forall a b c. (a -> b -> c) -> b -> a -> c
flip [Eval (GenValue b w i)] -> Int -> Eval (GenValue b w i)
forall i a. Integral i => [a] -> i -> a
genericIndex Int
i ([Eval (GenValue b w i)] -> Eval (GenValue b w i))
-> Eval [Eval (GenValue b w i)] -> Eval (Eval (GenValue b w i))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Eval [Eval (GenValue b w i)]
x')
| Int
i <- [0..(Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
-1)]
| TValue
t <- [TValue]
ts
]
TVRec fs :: [(Ident, TValue)]
fs ->
do Eval [(Ident, Eval (GenValue b w i))]
x' <- Maybe String
-> Eval [(Ident, Eval (GenValue b w i))]
-> Eval (Eval [(Ident, Eval (GenValue b w i))])
forall a. Maybe String -> Eval a -> Eval (Eval a)
delay (String -> Maybe String
forall a. a -> Maybe a
Just String
msg) (GenValue b w i -> [(Ident, Eval (GenValue b w i))]
forall b w i. GenValue b w i -> [(Ident, Eval (GenValue b w i))]
fromVRecord (GenValue b w i -> [(Ident, Eval (GenValue b w i))])
-> Eval (GenValue b w i) -> Eval [(Ident, Eval (GenValue b w i))]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Eval (GenValue b w i)
x)
let err :: a -> a
err f :: a
f = String -> [String] -> a
forall a. HasCallStack => String -> [String] -> a
evalPanic "expected record value with field" [a -> String
forall a. Show a => a -> String
show a
f]
GenValue b w i -> Eval (GenValue b w i)
forall (m :: * -> *) a. Monad m => a -> m a
return (GenValue b w i -> Eval (GenValue b w i))
-> GenValue b w i -> Eval (GenValue b w i)
forall a b. (a -> b) -> a -> b
$ [(Ident, Eval (GenValue b w i))] -> GenValue b w i
forall b w i. [(Ident, Eval (GenValue b w i))] -> GenValue b w i
VRecord ([(Ident, Eval (GenValue b w i))] -> GenValue b w i)
-> [(Ident, Eval (GenValue b w i))] -> GenValue b w i
forall a b. (a -> b) -> a -> b
$
[ (Ident
f, TValue -> Eval (GenValue b w i) -> Eval (GenValue b w i)
go TValue
t (Eval (GenValue b w i) -> Eval (GenValue b w i))
-> Eval (Eval (GenValue b w i)) -> Eval (GenValue b w i)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< (Eval (GenValue b w i)
-> Maybe (Eval (GenValue b w i)) -> Eval (GenValue b w i)
forall a. a -> Maybe a -> a
fromMaybe (Ident -> Eval (GenValue b w i)
forall a a. Show a => a -> a
err Ident
f) (Maybe (Eval (GenValue b w i)) -> Eval (GenValue b w i))
-> ([(Ident, Eval (GenValue b w i))]
-> Maybe (Eval (GenValue b w i)))
-> [(Ident, Eval (GenValue b w i))]
-> Eval (GenValue b w i)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Ident
-> [(Ident, Eval (GenValue b w i))]
-> Maybe (Eval (GenValue b w i))
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Ident
f ([(Ident, Eval (GenValue b w i))] -> Eval (GenValue b w i))
-> Eval [(Ident, Eval (GenValue b w i))]
-> Eval (Eval (GenValue b w i))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Eval [(Ident, Eval (GenValue b w i))]
x'))
| (f :: Ident
f,t :: TValue
t) <- [(Ident, TValue)]
fs
]
TVAbstract {} -> Eval (GenValue b w i)
x
declHole :: Decl
-> Eval (Name, Schema, Eval (GenValue b w i), Eval (GenValue b w i) -> Eval ())
declHole :: Decl
-> Eval
(Name, Schema, Eval (GenValue b w i),
Eval (GenValue b w i) -> Eval ())
declHole d :: Decl
d =
case Decl -> DeclDef
dDefinition Decl
d of
DPrim -> String
-> [String]
-> Eval
(Name, Schema, Eval (GenValue b w i),
Eval (GenValue b w i) -> Eval ())
forall a. HasCallStack => String -> [String] -> a
evalPanic "Unexpected primitive declaration in recursive group"
[Doc -> String
forall a. Show a => a -> String
show (Name -> Doc
ppLocName Name
nm)]
DExpr _ -> do
(hole :: Eval (GenValue b w i)
hole, fill :: Eval (GenValue b w i) -> Eval ()
fill) <- String
-> Eval (Eval (GenValue b w i), Eval (GenValue b w i) -> Eval ())
forall a. String -> Eval (Eval a, Eval a -> Eval ())
blackhole String
msg
(Name, Schema, Eval (GenValue b w i),
Eval (GenValue b w i) -> Eval ())
-> Eval
(Name, Schema, Eval (GenValue b w i),
Eval (GenValue b w i) -> Eval ())
forall (m :: * -> *) a. Monad m => a -> m a
return (Name
nm, Schema
sch, Eval (GenValue b w i)
hole, Eval (GenValue b w i) -> Eval ()
fill)
where
nm :: Name
nm = Decl -> Name
dName Decl
d
sch :: Schema
sch = Decl -> Schema
dSignature Decl
d
msg :: String
msg = [String] -> String
unwords ["<<loop>> while evaluating", Doc -> String
forall a. Show a => a -> String
show (Name -> Doc
forall a. PP a => a -> Doc
pp Name
nm)]
evalDecl :: EvalPrims b w i
=> GenEvalEnv b w i
-> GenEvalEnv b w i
-> Decl
-> Eval (GenEvalEnv b w i)
evalDecl :: GenEvalEnv b w i
-> GenEvalEnv b w i -> Decl -> Eval (GenEvalEnv b w i)
evalDecl renv :: GenEvalEnv b w i
renv env :: GenEvalEnv b w i
env d :: Decl
d =
case Decl -> DeclDef
dDefinition Decl
d of
DPrim -> case Decl -> Maybe (GenValue b w i)
forall b w i. EvalPrims b w i => Decl -> Maybe (GenValue b w i)
evalPrim Decl
d of
Just v :: GenValue b w i
v -> GenEvalEnv b w i -> Eval (GenEvalEnv b w i)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Name -> GenValue b w i -> GenEvalEnv b w i -> GenEvalEnv b w i
forall b w i.
Name -> GenValue b w i -> GenEvalEnv b w i -> GenEvalEnv b w i
bindVarDirect (Decl -> Name
dName Decl
d) GenValue b w i
v GenEvalEnv b w i
env)
Nothing -> Name
-> Eval (GenValue b w i)
-> GenEvalEnv b w i
-> Eval (GenEvalEnv b w i)
forall b w i.
Name
-> Eval (GenValue b w i)
-> GenEvalEnv b w i
-> Eval (GenEvalEnv b w i)
bindVar (Decl -> Name
dName Decl
d) (Name -> Eval (GenValue b w i)
forall a. Name -> Eval a
cryNoPrimError (Decl -> Name
dName Decl
d)) GenEvalEnv b w i
env
DExpr e :: Expr
e -> Name
-> Eval (GenValue b w i)
-> GenEvalEnv b w i
-> Eval (GenEvalEnv b w i)
forall b w i.
Name
-> Eval (GenValue b w i)
-> GenEvalEnv b w i
-> Eval (GenEvalEnv b w i)
bindVar (Decl -> Name
dName Decl
d) (GenEvalEnv b w i -> Expr -> Eval (GenValue b w i)
forall b w i.
EvalPrims b w i =>
GenEvalEnv b w i -> Expr -> Eval (GenValue b w i)
evalExpr GenEvalEnv b w i
renv Expr
e) GenEvalEnv b w i
env
evalSel :: forall b w i
. EvalPrims b w i
=> GenValue b w i
-> Selector
-> Eval (GenValue b w i)
evalSel :: GenValue b w i -> Selector -> Eval (GenValue b w i)
evalSel val :: GenValue b w i
val sel :: Selector
sel = case Selector
sel of
TupleSel n :: Int
n _ -> Int -> GenValue b w i -> Eval (GenValue b w i)
forall b w i.
BitWord b w i =>
Int -> GenValue b w i -> Eval (GenValue b w i)
tupleSel Int
n GenValue b w i
val
RecordSel n :: Ident
n _ -> Ident -> GenValue b w i -> Eval (GenValue b w i)
forall b w i.
BitWord b w i =>
Ident -> GenValue b w i -> Eval (GenValue b w i)
recordSel Ident
n GenValue b w i
val
ListSel ix :: Int
ix _ -> Int -> GenValue b w i -> Eval (GenValue b w i)
forall a b w i.
(Integral a, BitWord b w i) =>
a -> GenValue b w i -> Eval (GenValue b w i)
listSel Int
ix GenValue b w i
val
where
tupleSel :: Int -> GenValue b w i -> Eval (GenValue b w i)
tupleSel n :: Int
n v :: GenValue b w i
v =
case GenValue b w i
v of
VTuple vs :: [Eval (GenValue b w i)]
vs -> [Eval (GenValue b w i)]
vs [Eval (GenValue b w i)] -> Int -> Eval (GenValue b w i)
forall a. [a] -> Int -> a
!! Int
n
_ -> do Doc
vdoc <- PPOpts -> GenValue b w i -> Eval Doc
forall b w i. BitWord b w i => PPOpts -> GenValue b w i -> Eval Doc
ppValue PPOpts
defaultPPOpts GenValue b w i
v
String -> [String] -> Eval (GenValue b w i)
forall a. HasCallStack => String -> [String] -> a
evalPanic "Cryptol.Eval.evalSel"
[ "Unexpected value in tuple selection"
, Doc -> String
forall a. Show a => a -> String
show Doc
vdoc ]
recordSel :: Ident -> GenValue b w i -> Eval (GenValue b w i)
recordSel n :: Ident
n v :: GenValue b w i
v =
case GenValue b w i
v of
VRecord {} -> Ident -> GenValue b w i -> Eval (GenValue b w i)
forall b w i. Ident -> GenValue b w i -> Eval (GenValue b w i)
lookupRecord Ident
n GenValue b w i
v
_ -> do Doc
vdoc <- PPOpts -> GenValue b w i -> Eval Doc
forall b w i. BitWord b w i => PPOpts -> GenValue b w i -> Eval Doc
ppValue PPOpts
defaultPPOpts GenValue b w i
v
String -> [String] -> Eval (GenValue b w i)
forall a. HasCallStack => String -> [String] -> a
evalPanic "Cryptol.Eval.evalSel"
[ "Unexpected value in record selection"
, Doc -> String
forall a. Show a => a -> String
show Doc
vdoc ]
listSel :: a -> GenValue b w i -> Eval (GenValue b w i)
listSel n :: a
n v :: GenValue b w i
v =
case GenValue b w i
v of
VSeq _ vs :: SeqMap b w i
vs -> SeqMap b w i -> Integer -> Eval (GenValue b w i)
forall b w i. SeqMap b w i -> Integer -> Eval (GenValue b w i)
lookupSeqMap SeqMap b w i
vs (a -> Integer
forall a. Integral a => a -> Integer
toInteger a
n)
VStream vs :: SeqMap b w i
vs -> SeqMap b w i -> Integer -> Eval (GenValue b w i)
forall b w i. SeqMap b w i -> Integer -> Eval (GenValue b w i)
lookupSeqMap SeqMap b w i
vs (a -> Integer
forall a. Integral a => a -> Integer
toInteger a
n)
VWord _ wv :: Eval (WordValue b w i)
wv -> b -> GenValue b w i
forall b w i. b -> GenValue b w i
VBit (b -> GenValue b w i) -> Eval b -> Eval (GenValue b w i)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((WordValue b w i -> Integer -> Eval b)
-> Integer -> WordValue b w i -> Eval b
forall a b c. (a -> b -> c) -> b -> a -> c
flip WordValue b w i -> Integer -> Eval b
forall b w i. BitWord b w i => WordValue b w i -> Integer -> Eval b
indexWordValue (a -> Integer
forall a. Integral a => a -> Integer
toInteger a
n) (WordValue b w i -> Eval b) -> Eval (WordValue b w i) -> Eval b
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Eval (WordValue b w i)
wv)
_ -> do Doc
vdoc <- PPOpts -> GenValue b w i -> Eval Doc
forall b w i. BitWord b w i => PPOpts -> GenValue b w i -> Eval Doc
ppValue PPOpts
defaultPPOpts GenValue b w i
val
String -> [String] -> Eval (GenValue b w i)
forall a. HasCallStack => String -> [String] -> a
evalPanic "Cryptol.Eval.evalSel"
[ "Unexpected value in list selection"
, Doc -> String
forall a. Show a => a -> String
show Doc
vdoc ]
evalSetSel :: forall b w i. EvalPrims b w i =>
GenValue b w i -> Selector -> Eval (GenValue b w i) -> Eval (GenValue b w i)
evalSetSel :: GenValue b w i
-> Selector -> Eval (GenValue b w i) -> Eval (GenValue b w i)
evalSetSel e :: GenValue b w i
e x :: Selector
x v :: Eval (GenValue b w i)
v =
case Selector
x of
TupleSel n :: Int
n _ -> Int -> Eval (GenValue b w i)
setTuple Int
n
RecordSel n :: Ident
n _ -> Ident -> Eval (GenValue b w i)
setRecord Ident
n
ListSel ix :: Int
ix _ -> Integer -> Eval (GenValue b w i)
setList (Int -> Integer
forall a. Integral a => a -> Integer
toInteger Int
ix)
where
bad :: String -> Eval b
bad msg :: String
msg =
do Doc
ed <- PPOpts -> GenValue b w i -> Eval Doc
forall b w i. BitWord b w i => PPOpts -> GenValue b w i -> Eval Doc
ppValue PPOpts
defaultPPOpts GenValue b w i
e
String -> [String] -> Eval b
forall a. HasCallStack => String -> [String] -> a
evalPanic "Cryptol.Eval.evalSetSel"
[ String
msg
, "Selector: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Doc -> String
forall a. Show a => a -> String
show (Selector -> Doc
ppSelector Selector
x)
, "Value: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Doc -> String
forall a. Show a => a -> String
show Doc
ed
]
setTuple :: Int -> Eval (GenValue b w i)
setTuple n :: Int
n =
case GenValue b w i
e of
VTuple xs :: [Eval (GenValue b w i)]
xs ->
case Int
-> [Eval (GenValue b w i)]
-> ([Eval (GenValue b w i)], [Eval (GenValue b w i)])
forall a. Int -> [a] -> ([a], [a])
splitAt Int
n [Eval (GenValue b w i)]
xs of
(as :: [Eval (GenValue b w i)]
as, _: bs :: [Eval (GenValue b w i)]
bs) -> GenValue b w i -> Eval (GenValue b w i)
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([Eval (GenValue b w i)] -> GenValue b w i
forall b w i. [Eval (GenValue b w i)] -> GenValue b w i
VTuple ([Eval (GenValue b w i)]
as [Eval (GenValue b w i)]
-> [Eval (GenValue b w i)] -> [Eval (GenValue b w i)]
forall a. [a] -> [a] -> [a]
++ Eval (GenValue b w i)
v Eval (GenValue b w i)
-> [Eval (GenValue b w i)] -> [Eval (GenValue b w i)]
forall a. a -> [a] -> [a]
: [Eval (GenValue b w i)]
bs))
_ -> String -> Eval (GenValue b w i)
forall b. String -> Eval b
bad "Tuple update out of bounds."
_ -> String -> Eval (GenValue b w i)
forall b. String -> Eval b
bad "Tuple update on a non-tuple."
setRecord :: Ident -> Eval (GenValue b w i)
setRecord n :: Ident
n =
case GenValue b w i
e of
VRecord xs :: [(Ident, Eval (GenValue b w i))]
xs ->
case ((Ident, Eval (GenValue b w i)) -> Bool)
-> [(Ident, Eval (GenValue b w i))]
-> ([(Ident, Eval (GenValue b w i))],
[(Ident, Eval (GenValue b w i))])
forall a. (a -> Bool) -> [a] -> ([a], [a])
break ((Ident
n Ident -> Ident -> Bool
forall a. Eq a => a -> a -> Bool
==) (Ident -> Bool)
-> ((Ident, Eval (GenValue b w i)) -> Ident)
-> (Ident, Eval (GenValue b w i))
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Ident, Eval (GenValue b w i)) -> Ident
forall a b. (a, b) -> a
fst) [(Ident, Eval (GenValue b w i))]
xs of
(as :: [(Ident, Eval (GenValue b w i))]
as, (i :: Ident
i,_) : bs :: [(Ident, Eval (GenValue b w i))]
bs) -> GenValue b w i -> Eval (GenValue b w i)
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([(Ident, Eval (GenValue b w i))] -> GenValue b w i
forall b w i. [(Ident, Eval (GenValue b w i))] -> GenValue b w i
VRecord ([(Ident, Eval (GenValue b w i))]
as [(Ident, Eval (GenValue b w i))]
-> [(Ident, Eval (GenValue b w i))]
-> [(Ident, Eval (GenValue b w i))]
forall a. [a] -> [a] -> [a]
++ (Ident
i,Eval (GenValue b w i)
v) (Ident, Eval (GenValue b w i))
-> [(Ident, Eval (GenValue b w i))]
-> [(Ident, Eval (GenValue b w i))]
forall a. a -> [a] -> [a]
: [(Ident, Eval (GenValue b w i))]
bs))
_ -> String -> Eval (GenValue b w i)
forall b. String -> Eval b
bad "Missing field in record update."
_ -> String -> Eval (GenValue b w i)
forall b. String -> Eval b
bad "Record update on a non-record."
setList :: Integer -> Eval (GenValue b w i)
setList n :: Integer
n =
case GenValue b w i
e of
VSeq i :: Integer
i mp :: SeqMap b w i
mp -> GenValue b w i -> Eval (GenValue b w i)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (GenValue b w i -> Eval (GenValue b w i))
-> GenValue b w i -> Eval (GenValue b w i)
forall a b. (a -> b) -> a -> b
$ Integer -> SeqMap b w i -> GenValue b w i
forall b w i. Integer -> SeqMap b w i -> GenValue b w i
VSeq Integer
i (SeqMap b w i -> GenValue b w i) -> SeqMap b w i -> GenValue b w i
forall a b. (a -> b) -> a -> b
$ SeqMap b w i -> Integer -> Eval (GenValue b w i) -> SeqMap b w i
forall b w i.
SeqMap b w i -> Integer -> Eval (GenValue b w i) -> SeqMap b w i
updateSeqMap SeqMap b w i
mp Integer
n Eval (GenValue b w i)
v
VStream mp :: SeqMap b w i
mp -> GenValue b w i -> Eval (GenValue b w i)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (GenValue b w i -> Eval (GenValue b w i))
-> GenValue b w i -> Eval (GenValue b w i)
forall a b. (a -> b) -> a -> b
$ SeqMap b w i -> GenValue b w i
forall b w i. SeqMap b w i -> GenValue b w i
VStream (SeqMap b w i -> GenValue b w i) -> SeqMap b w i -> GenValue b w i
forall a b. (a -> b) -> a -> b
$ SeqMap b w i -> Integer -> Eval (GenValue b w i) -> SeqMap b w i
forall b w i.
SeqMap b w i -> Integer -> Eval (GenValue b w i) -> SeqMap b w i
updateSeqMap SeqMap b w i
mp Integer
n Eval (GenValue b w i)
v
VWord i :: Integer
i m :: Eval (WordValue b w i)
m -> GenValue b w i -> Eval (GenValue b w i)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (GenValue b w i -> Eval (GenValue b w i))
-> GenValue b w i -> Eval (GenValue b w i)
forall a b. (a -> b) -> a -> b
$ Integer -> Eval (WordValue b w i) -> GenValue b w i
forall b w i. Integer -> Eval (WordValue b w i) -> GenValue b w i
VWord Integer
i (Eval (WordValue b w i) -> GenValue b w i)
-> Eval (WordValue b w i) -> GenValue b w i
forall a b. (a -> b) -> a -> b
$ do WordValue b w i
m1 <- Eval (WordValue b w i)
m
WordValue b w i -> Integer -> Eval b -> Eval (WordValue b w i)
forall b w i.
BitWord b w i =>
WordValue b w i -> Integer -> Eval b -> Eval (WordValue b w i)
updateWordValue WordValue b w i
m1 Integer
n Eval b
asBit
_ -> String -> Eval (GenValue b w i)
forall b. String -> Eval b
bad "Sequence update on a non-sequence."
asBit :: Eval b
asBit = do GenValue b w i
res <- Eval (GenValue b w i)
v
case GenValue b w i
res of
VBit b :: b
b -> b -> Eval b
forall (f :: * -> *) a. Applicative f => a -> f a
pure b
b
_ -> String -> Eval b
forall b. String -> Eval b
bad "Expected a bit, but got something else"
data ListEnv b w i = ListEnv
{ ListEnv b w i -> Map Name (Integer -> Eval (GenValue b w i))
leVars :: !(Map.Map Name (Integer -> Eval (GenValue b w i)))
, ListEnv b w i -> Map Name (Eval (GenValue b w i))
leStatic :: !(Map.Map Name (Eval (GenValue b w i)))
, ListEnv b w i -> TypeEnv
leTypes :: !TypeEnv
}
instance Semigroup (ListEnv b w i) where
l :: ListEnv b w i
l <> :: ListEnv b w i -> ListEnv b w i -> ListEnv b w i
<> r :: ListEnv b w i
r = $WListEnv :: forall b w i.
Map Name (Integer -> Eval (GenValue b w i))
-> Map Name (Eval (GenValue b w i)) -> TypeEnv -> ListEnv b w i
ListEnv
{ leVars :: Map Name (Integer -> Eval (GenValue b w i))
leVars = Map Name (Integer -> Eval (GenValue b w i))
-> Map Name (Integer -> Eval (GenValue b w i))
-> Map Name (Integer -> Eval (GenValue b w i))
forall k a. Ord k => Map k a -> Map k a -> Map k a
Map.union (ListEnv b w i -> Map Name (Integer -> Eval (GenValue b w i))
forall b w i.
ListEnv b w i -> Map Name (Integer -> Eval (GenValue b w i))
leVars ListEnv b w i
l) (ListEnv b w i -> Map Name (Integer -> Eval (GenValue b w i))
forall b w i.
ListEnv b w i -> Map Name (Integer -> Eval (GenValue b w i))
leVars ListEnv b w i
r)
, leStatic :: Map Name (Eval (GenValue b w i))
leStatic = Map Name (Eval (GenValue b w i))
-> Map Name (Eval (GenValue b w i))
-> Map Name (Eval (GenValue b w i))
forall k a. Ord k => Map k a -> Map k a -> Map k a
Map.union (ListEnv b w i -> Map Name (Eval (GenValue b w i))
forall b w i. ListEnv b w i -> Map Name (Eval (GenValue b w i))
leStatic ListEnv b w i
l) (ListEnv b w i -> Map Name (Eval (GenValue b w i))
forall b w i. ListEnv b w i -> Map Name (Eval (GenValue b w i))
leStatic ListEnv b w i
r)
, leTypes :: TypeEnv
leTypes = TypeEnv -> TypeEnv -> TypeEnv
forall k a. Ord k => Map k a -> Map k a -> Map k a
Map.union (ListEnv b w i -> TypeEnv
forall b w i. ListEnv b w i -> TypeEnv
leTypes ListEnv b w i
l) (ListEnv b w i -> TypeEnv
forall b w i. ListEnv b w i -> TypeEnv
leTypes ListEnv b w i
r)
}
instance Monoid (ListEnv b w i) where
mempty :: ListEnv b w i
mempty = $WListEnv :: forall b w i.
Map Name (Integer -> Eval (GenValue b w i))
-> Map Name (Eval (GenValue b w i)) -> TypeEnv -> ListEnv b w i
ListEnv
{ leVars :: Map Name (Integer -> Eval (GenValue b w i))
leVars = Map Name (Integer -> Eval (GenValue b w i))
forall k a. Map k a
Map.empty
, leStatic :: Map Name (Eval (GenValue b w i))
leStatic = Map Name (Eval (GenValue b w i))
forall k a. Map k a
Map.empty
, leTypes :: TypeEnv
leTypes = TypeEnv
forall k a. Map k a
Map.empty
}
mappend :: ListEnv b w i -> ListEnv b w i -> ListEnv b w i
mappend l :: ListEnv b w i
l r :: ListEnv b w i
r = ListEnv b w i
l ListEnv b w i -> ListEnv b w i -> ListEnv b w i
forall a. Semigroup a => a -> a -> a
<> ListEnv b w i
r
toListEnv :: GenEvalEnv b w i -> ListEnv b w i
toListEnv :: GenEvalEnv b w i -> ListEnv b w i
toListEnv e :: GenEvalEnv b w i
e =
$WListEnv :: forall b w i.
Map Name (Integer -> Eval (GenValue b w i))
-> Map Name (Eval (GenValue b w i)) -> TypeEnv -> ListEnv b w i
ListEnv
{ leVars :: Map Name (Integer -> Eval (GenValue b w i))
leVars = Map Name (Integer -> Eval (GenValue b w i))
forall a. Monoid a => a
mempty
, leStatic :: Map Name (Eval (GenValue b w i))
leStatic = GenEvalEnv b w i -> Map Name (Eval (GenValue b w i))
forall b w i. GenEvalEnv b w i -> Map Name (Eval (GenValue b w i))
envVars GenEvalEnv b w i
e
, leTypes :: TypeEnv
leTypes = GenEvalEnv b w i -> TypeEnv
forall b w i. GenEvalEnv b w i -> TypeEnv
envTypes GenEvalEnv b w i
e
}
evalListEnv :: ListEnv b w i -> Integer -> GenEvalEnv b w i
evalListEnv :: ListEnv b w i -> Integer -> GenEvalEnv b w i
evalListEnv (ListEnv vm :: Map Name (Integer -> Eval (GenValue b w i))
vm st :: Map Name (Eval (GenValue b w i))
st tm :: TypeEnv
tm) i :: Integer
i =
let v :: Map Name (Eval (GenValue b w i))
v = ((Integer -> Eval (GenValue b w i)) -> Eval (GenValue b w i))
-> Map Name (Integer -> Eval (GenValue b w i))
-> Map Name (Eval (GenValue b w i))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Integer -> Eval (GenValue b w i))
-> Integer -> Eval (GenValue b w i)
forall a b. (a -> b) -> a -> b
$Integer
i) Map Name (Integer -> Eval (GenValue b w i))
vm
in $WEvalEnv :: forall b w i.
Map Name (Eval (GenValue b w i)) -> TypeEnv -> GenEvalEnv b w i
EvalEnv{ envVars :: Map Name (Eval (GenValue b w i))
envVars = Map Name (Eval (GenValue b w i))
-> Map Name (Eval (GenValue b w i))
-> Map Name (Eval (GenValue b w i))
forall k a. Ord k => Map k a -> Map k a -> Map k a
Map.union Map Name (Eval (GenValue b w i))
v Map Name (Eval (GenValue b w i))
st
, envTypes :: TypeEnv
envTypes = TypeEnv
tm
}
bindVarList :: Name
-> (Integer -> Eval (GenValue b w i))
-> ListEnv b w i
-> ListEnv b w i
bindVarList :: Name
-> (Integer -> Eval (GenValue b w i))
-> ListEnv b w i
-> ListEnv b w i
bindVarList n :: Name
n vs :: Integer -> Eval (GenValue b w i)
vs lenv :: ListEnv b w i
lenv = ListEnv b w i
lenv { leVars :: Map Name (Integer -> Eval (GenValue b w i))
leVars = Name
-> (Integer -> Eval (GenValue b w i))
-> Map Name (Integer -> Eval (GenValue b w i))
-> Map Name (Integer -> Eval (GenValue b w i))
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Name
n Integer -> Eval (GenValue b w i)
vs (ListEnv b w i -> Map Name (Integer -> Eval (GenValue b w i))
forall b w i.
ListEnv b w i -> Map Name (Integer -> Eval (GenValue b w i))
leVars ListEnv b w i
lenv) }
evalComp :: EvalPrims b w i
=> GenEvalEnv b w i
-> Nat'
-> TValue
-> Expr
-> [[Match]]
-> Eval (GenValue b w i)
evalComp :: GenEvalEnv b w i
-> Nat' -> TValue -> Expr -> [[Match]] -> Eval (GenValue b w i)
evalComp env :: GenEvalEnv b w i
env len :: Nat'
len elty :: TValue
elty body :: Expr
body ms :: [[Match]]
ms =
do ListEnv b w i
lenv <- [ListEnv b w i] -> ListEnv b w i
forall a. Monoid a => [a] -> a
mconcat ([ListEnv b w i] -> ListEnv b w i)
-> Eval [ListEnv b w i] -> Eval (ListEnv b w i)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ([Match] -> Eval (ListEnv b w i))
-> [[Match]] -> Eval [ListEnv b w i]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (ListEnv b w i -> [Match] -> Eval (ListEnv b w i)
forall b w i.
EvalPrims b w i =>
ListEnv b w i -> [Match] -> Eval (ListEnv b w i)
branchEnvs (GenEvalEnv b w i -> ListEnv b w i
forall b w i. GenEvalEnv b w i -> ListEnv b w i
toListEnv GenEvalEnv b w i
env)) [[Match]]
ms
Nat' -> TValue -> SeqMap b w i -> GenValue b w i
forall b w i. Nat' -> TValue -> SeqMap b w i -> GenValue b w i
mkSeq Nat'
len TValue
elty (SeqMap b w i -> GenValue b w i)
-> Eval (SeqMap b w i) -> Eval (GenValue b w i)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SeqMap b w i -> Eval (SeqMap b w i)
forall b w i. SeqMap b w i -> Eval (SeqMap b w i)
memoMap ((Integer -> Eval (GenValue b w i)) -> SeqMap b w i
forall b w i. (Integer -> Eval (GenValue b w i)) -> SeqMap b w i
IndexSeqMap ((Integer -> Eval (GenValue b w i)) -> SeqMap b w i)
-> (Integer -> Eval (GenValue b w i)) -> SeqMap b w i
forall a b. (a -> b) -> a -> b
$ \i :: Integer
i -> do
GenEvalEnv b w i -> Expr -> Eval (GenValue b w i)
forall b w i.
EvalPrims b w i =>
GenEvalEnv b w i -> Expr -> Eval (GenValue b w i)
evalExpr (ListEnv b w i -> Integer -> GenEvalEnv b w i
forall b w i. ListEnv b w i -> Integer -> GenEvalEnv b w i
evalListEnv ListEnv b w i
lenv Integer
i) Expr
body)
branchEnvs :: EvalPrims b w i
=> ListEnv b w i
-> [Match]
-> Eval (ListEnv b w i)
branchEnvs :: ListEnv b w i -> [Match] -> Eval (ListEnv b w i)
branchEnvs env :: ListEnv b w i
env matches :: [Match]
matches = (ListEnv b w i -> Match -> Eval (ListEnv b w i))
-> ListEnv b w i -> [Match] -> Eval (ListEnv b w i)
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM ListEnv b w i -> Match -> Eval (ListEnv b w i)
forall b w i.
EvalPrims b w i =>
ListEnv b w i -> Match -> Eval (ListEnv b w i)
evalMatch ListEnv b w i
env [Match]
matches
evalMatch :: EvalPrims b w i
=> ListEnv b w i
-> Match
-> Eval (ListEnv b w i)
evalMatch :: ListEnv b w i -> Match -> Eval (ListEnv b w i)
evalMatch lenv :: ListEnv b w i
lenv m :: Match
m = case Match
m of
From n :: Name
n l :: Type
l _ty :: Type
_ty expr :: Expr
expr ->
case Nat'
len of
Nat nLen :: Integer
nLen -> do
SeqMap b w i
vss <- SeqMap b w i -> Eval (SeqMap b w i)
forall b w i. SeqMap b w i -> Eval (SeqMap b w i)
memoMap (SeqMap b w i -> Eval (SeqMap b w i))
-> SeqMap b w i -> Eval (SeqMap b w i)
forall a b. (a -> b) -> a -> b
$ (Integer -> Eval (GenValue b w i)) -> SeqMap b w i
forall b w i. (Integer -> Eval (GenValue b w i)) -> SeqMap b w i
IndexSeqMap ((Integer -> Eval (GenValue b w i)) -> SeqMap b w i)
-> (Integer -> Eval (GenValue b w i)) -> SeqMap b w i
forall a b. (a -> b) -> a -> b
$ \i :: Integer
i -> GenEvalEnv b w i -> Expr -> Eval (GenValue b w i)
forall b w i.
EvalPrims b w i =>
GenEvalEnv b w i -> Expr -> Eval (GenValue b w i)
evalExpr (ListEnv b w i -> Integer -> GenEvalEnv b w i
forall b w i. ListEnv b w i -> Integer -> GenEvalEnv b w i
evalListEnv ListEnv b w i
lenv Integer
i) Expr
expr
let stutter :: (Integer -> t) -> Integer -> t
stutter xs :: Integer -> t
xs = \i :: Integer
i -> Integer -> t
xs (Integer
i Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`div` Integer
nLen)
let lenv' :: ListEnv b w i
lenv' = ListEnv b w i
lenv { leVars :: Map Name (Integer -> Eval (GenValue b w i))
leVars = ((Integer -> Eval (GenValue b w i))
-> Integer -> Eval (GenValue b w i))
-> Map Name (Integer -> Eval (GenValue b w i))
-> Map Name (Integer -> Eval (GenValue b w i))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Integer -> Eval (GenValue b w i))
-> Integer -> Eval (GenValue b w i)
forall t. (Integer -> t) -> Integer -> t
stutter (ListEnv b w i -> Map Name (Integer -> Eval (GenValue b w i))
forall b w i.
ListEnv b w i -> Map Name (Integer -> Eval (GenValue b w i))
leVars ListEnv b w i
lenv) }
let vs :: Integer -> Eval (GenValue b w i)
vs i :: Integer
i = do let (q :: Integer
q, r :: Integer
r) = Integer
i Integer -> Integer -> (Integer, Integer)
forall a. Integral a => a -> a -> (a, a)
`divMod` Integer
nLen
SeqMap b w i -> Integer -> Eval (GenValue b w i)
forall b w i. SeqMap b w i -> Integer -> Eval (GenValue b w i)
lookupSeqMap SeqMap b w i
vss Integer
q Eval (GenValue b w i)
-> (GenValue b w i -> Eval (GenValue b w i))
-> Eval (GenValue b w i)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
VWord _ w :: Eval (WordValue b w i)
w -> b -> GenValue b w i
forall b w i. b -> GenValue b w i
VBit (b -> GenValue b w i) -> Eval b -> Eval (GenValue b w i)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((WordValue b w i -> Integer -> Eval b)
-> Integer -> WordValue b w i -> Eval b
forall a b c. (a -> b -> c) -> b -> a -> c
flip WordValue b w i -> Integer -> Eval b
forall b w i. BitWord b w i => WordValue b w i -> Integer -> Eval b
indexWordValue Integer
r (WordValue b w i -> Eval b) -> Eval (WordValue b w i) -> Eval b
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Eval (WordValue b w i)
w)
VSeq _ xs' :: SeqMap b w i
xs' -> SeqMap b w i -> Integer -> Eval (GenValue b w i)
forall b w i. SeqMap b w i -> Integer -> Eval (GenValue b w i)
lookupSeqMap SeqMap b w i
xs' Integer
r
VStream xs' :: SeqMap b w i
xs' -> SeqMap b w i -> Integer -> Eval (GenValue b w i)
forall b w i. SeqMap b w i -> Integer -> Eval (GenValue b w i)
lookupSeqMap SeqMap b w i
xs' Integer
r
_ -> String -> [String] -> Eval (GenValue b w i)
forall a. HasCallStack => String -> [String] -> a
evalPanic "evalMatch" ["Not a list value"]
ListEnv b w i -> Eval (ListEnv b w i)
forall (m :: * -> *) a. Monad m => a -> m a
return (ListEnv b w i -> Eval (ListEnv b w i))
-> ListEnv b w i -> Eval (ListEnv b w i)
forall a b. (a -> b) -> a -> b
$ Name
-> (Integer -> Eval (GenValue b w i))
-> ListEnv b w i
-> ListEnv b w i
forall b w i.
Name
-> (Integer -> Eval (GenValue b w i))
-> ListEnv b w i
-> ListEnv b w i
bindVarList Name
n Integer -> Eval (GenValue b w i)
vs ListEnv b w i
lenv'
Inf -> do
let allvars :: Map Name (Eval (GenValue b w i))
allvars = Map Name (Eval (GenValue b w i))
-> Map Name (Eval (GenValue b w i))
-> Map Name (Eval (GenValue b w i))
forall k a. Ord k => Map k a -> Map k a -> Map k a
Map.union (((Integer -> Eval (GenValue b w i)) -> Eval (GenValue b w i))
-> Map Name (Integer -> Eval (GenValue b w i))
-> Map Name (Eval (GenValue b w i))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Integer -> Eval (GenValue b w i))
-> Integer -> Eval (GenValue b w i)
forall a b. (a -> b) -> a -> b
$0) (ListEnv b w i -> Map Name (Integer -> Eval (GenValue b w i))
forall b w i.
ListEnv b w i -> Map Name (Integer -> Eval (GenValue b w i))
leVars ListEnv b w i
lenv)) (ListEnv b w i -> Map Name (Eval (GenValue b w i))
forall b w i. ListEnv b w i -> Map Name (Eval (GenValue b w i))
leStatic ListEnv b w i
lenv)
let lenv' :: ListEnv b w i
lenv' = ListEnv b w i
lenv { leVars :: Map Name (Integer -> Eval (GenValue b w i))
leVars = Map Name (Integer -> Eval (GenValue b w i))
forall k a. Map k a
Map.empty
, leStatic :: Map Name (Eval (GenValue b w i))
leStatic = Map Name (Eval (GenValue b w i))
allvars
}
let env :: GenEvalEnv b w i
env = Map Name (Eval (GenValue b w i)) -> TypeEnv -> GenEvalEnv b w i
forall b w i.
Map Name (Eval (GenValue b w i)) -> TypeEnv -> GenEvalEnv b w i
EvalEnv Map Name (Eval (GenValue b w i))
allvars (ListEnv b w i -> TypeEnv
forall b w i. ListEnv b w i -> TypeEnv
leTypes ListEnv b w i
lenv)
GenValue b w i
xs <- GenEvalEnv b w i -> Expr -> Eval (GenValue b w i)
forall b w i.
EvalPrims b w i =>
GenEvalEnv b w i -> Expr -> Eval (GenValue b w i)
evalExpr GenEvalEnv b w i
env Expr
expr
let vs :: Integer -> Eval (GenValue b w i)
vs i :: Integer
i = case GenValue b w i
xs of
VWord _ w :: Eval (WordValue b w i)
w -> b -> GenValue b w i
forall b w i. b -> GenValue b w i
VBit (b -> GenValue b w i) -> Eval b -> Eval (GenValue b w i)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((WordValue b w i -> Integer -> Eval b)
-> Integer -> WordValue b w i -> Eval b
forall a b c. (a -> b -> c) -> b -> a -> c
flip WordValue b w i -> Integer -> Eval b
forall b w i. BitWord b w i => WordValue b w i -> Integer -> Eval b
indexWordValue Integer
i (WordValue b w i -> Eval b) -> Eval (WordValue b w i) -> Eval b
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Eval (WordValue b w i)
w)
VSeq _ xs' :: SeqMap b w i
xs' -> SeqMap b w i -> Integer -> Eval (GenValue b w i)
forall b w i. SeqMap b w i -> Integer -> Eval (GenValue b w i)
lookupSeqMap SeqMap b w i
xs' Integer
i
VStream xs' :: SeqMap b w i
xs' -> SeqMap b w i -> Integer -> Eval (GenValue b w i)
forall b w i. SeqMap b w i -> Integer -> Eval (GenValue b w i)
lookupSeqMap SeqMap b w i
xs' Integer
i
_ -> String -> [String] -> Eval (GenValue b w i)
forall a. HasCallStack => String -> [String] -> a
evalPanic "evalMatch" ["Not a list value"]
ListEnv b w i -> Eval (ListEnv b w i)
forall (m :: * -> *) a. Monad m => a -> m a
return (ListEnv b w i -> Eval (ListEnv b w i))
-> ListEnv b w i -> Eval (ListEnv b w i)
forall a b. (a -> b) -> a -> b
$ Name
-> (Integer -> Eval (GenValue b w i))
-> ListEnv b w i
-> ListEnv b w i
forall b w i.
Name
-> (Integer -> Eval (GenValue b w i))
-> ListEnv b w i
-> ListEnv b w i
bindVarList Name
n Integer -> Eval (GenValue b w i)
vs ListEnv b w i
lenv'
where
len :: Nat'
len = HasCallStack => TypeEnv -> Type -> Nat'
TypeEnv -> Type -> Nat'
evalNumType (ListEnv b w i -> TypeEnv
forall b w i. ListEnv b w i -> TypeEnv
leTypes ListEnv b w i
lenv) Type
l
Let d :: Decl
d -> ListEnv b w i -> Eval (ListEnv b w i)
forall (m :: * -> *) a. Monad m => a -> m a
return (ListEnv b w i -> Eval (ListEnv b w i))
-> ListEnv b w i -> Eval (ListEnv b w i)
forall a b. (a -> b) -> a -> b
$ Name
-> (Integer -> Eval (GenValue b w i))
-> ListEnv b w i
-> ListEnv b w i
forall b w i.
Name
-> (Integer -> Eval (GenValue b w i))
-> ListEnv b w i
-> ListEnv b w i
bindVarList (Decl -> Name
dName Decl
d) (\i :: Integer
i -> GenEvalEnv b w i -> Eval (GenValue b w i)
forall b w i.
EvalPrims b w i =>
GenEvalEnv b w i -> Eval (GenValue b w i)
f (ListEnv b w i -> Integer -> GenEvalEnv b w i
forall b w i. ListEnv b w i -> Integer -> GenEvalEnv b w i
evalListEnv ListEnv b w i
lenv Integer
i)) ListEnv b w i
lenv
where
f :: GenEvalEnv b w i -> Eval (GenValue b w i)
f env :: GenEvalEnv b w i
env =
case Decl -> DeclDef
dDefinition Decl
d of
DPrim -> String -> [String] -> Eval (GenValue b w i)
forall a. HasCallStack => String -> [String] -> a
evalPanic "evalMatch" ["Unexpected local primitive"]
DExpr e :: Expr
e -> GenEvalEnv b w i -> Expr -> Eval (GenValue b w i)
forall b w i.
EvalPrims b w i =>
GenEvalEnv b w i -> Expr -> Eval (GenValue b w i)
evalExpr GenEvalEnv b w i
env Expr
e