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

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

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

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

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

import Prelude ()
import Prelude.Compat

type EvalEnv = GenEvalEnv Bool BV Integer

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

  where

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


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

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

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


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

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

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

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

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

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

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


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


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

isValueType _ _ = Bool
False


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


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

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

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

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

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

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

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

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

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

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

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

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

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

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

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


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


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

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


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

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

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

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

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

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

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

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

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

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

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

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

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

-- | Evaluation environments for list comprehensions: Each variable
-- name is bound to a list of values, one for each element in the list
-- comprehension.
data ListEnv b w i = ListEnv
  { ListEnv b w i -> Map Name (Integer -> Eval (GenValue b w i))
leVars   :: !(Map.Map Name (Integer -> Eval (GenValue b w i)))
      -- ^ Bindings whose values vary by position
  , ListEnv b w i -> Map Name (Eval (GenValue b w i))
leStatic :: !(Map.Map Name (Eval (GenValue b w i)))
      -- ^ Bindings whose values are constant
  , ListEnv b w i -> TypeEnv
leTypes  :: !TypeEnv
  }

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

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

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

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

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

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

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

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

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

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

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

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

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

  -- XXX we don't currently evaluate these as though they could be recursive, as
  -- they are typechecked that way; the read environment to evalExpr is the same
  -- as the environment to bind a new name in.
  Let d :: Decl
d -> ListEnv b w i -> Eval (ListEnv b w i)
forall (m :: * -> *) a. Monad m => a -> m a
return (ListEnv b w i -> Eval (ListEnv b w i))
-> ListEnv b w i -> Eval (ListEnv b w i)
forall a b. (a -> b) -> a -> b
$ Name
-> (Integer -> Eval (GenValue b w i))
-> ListEnv b w i
-> ListEnv b w i
forall b w i.
Name
-> (Integer -> Eval (GenValue b w i))
-> ListEnv b w i
-> ListEnv b w i
bindVarList (Decl -> Name
dName Decl
d) (\i :: Integer
i -> GenEvalEnv b w i -> Eval (GenValue b w i)
forall b w i.
EvalPrims b w i =>
GenEvalEnv b w i -> Eval (GenValue b w i)
f (ListEnv b w i -> Integer -> GenEvalEnv b w i
forall b w i. ListEnv b w i -> Integer -> GenEvalEnv b w i
evalListEnv ListEnv b w i
lenv Integer
i)) ListEnv b w i
lenv
    where
      f :: GenEvalEnv b w i -> Eval (GenValue b w i)
f env :: GenEvalEnv b w i
env =
          case Decl -> DeclDef
dDefinition Decl
d of
            DPrim   -> String -> [String] -> Eval (GenValue b w i)
forall a. HasCallStack => String -> [String] -> a
evalPanic "evalMatch" ["Unexpected local primitive"]
            DExpr e :: Expr
e -> GenEvalEnv b w i -> Expr -> Eval (GenValue b w i)
forall b w i.
EvalPrims b w i =>
GenEvalEnv b w i -> Expr -> Eval (GenValue b w i)
evalExpr GenEvalEnv b w i
env Expr
e