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

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

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

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

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

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

import Prelude ()
import Prelude.Compat

type EvalEnv = GenEvalEnv Concrete

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

  where

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

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


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

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

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

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

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

evalNewtypeDecls ::
  EvalPrims sym =>
  sym ->
  Map.Map Name Newtype ->
  GenEvalEnv sym ->
  SEval sym (GenEvalEnv sym)
evalNewtypeDecls :: forall sym.
EvalPrims sym =>
sym
-> Map Name Newtype -> GenEvalEnv sym -> SEval sym (GenEvalEnv sym)
evalNewtypeDecls sym
sym Map Name Newtype
nts GenEvalEnv sym
env = forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM (forall a b c. (a -> b -> c) -> b -> a -> c
flip (forall sym.
EvalPrims sym =>
sym -> Newtype -> GenEvalEnv sym -> SEval sym (GenEvalEnv sym)
evalNewtypeDecl sym
sym)) GenEvalEnv sym
env forall a b. (a -> b) -> a -> b
$ forall k a. Map k a -> [a]
Map.elems Map Name Newtype
nts

-- | Introduce the constructor function for a newtype.
evalNewtypeDecl ::
  EvalPrims sym =>
  sym ->
  Newtype ->
  GenEvalEnv sym ->
  SEval sym (GenEvalEnv sym)
evalNewtypeDecl :: forall sym.
EvalPrims sym =>
sym -> Newtype -> GenEvalEnv sym -> SEval sym (GenEvalEnv sym)
evalNewtypeDecl sym
_sym Newtype
nt = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall sym.
Backend sym =>
Name -> Prim sym -> GenEvalEnv sym -> GenEvalEnv sym
bindVarDirect (Newtype -> Name
ntConName Newtype
nt) (forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr forall {sym}. TParam -> Prim sym -> Prim sym
tabs forall {sym}. Prim sym
con (Newtype -> [TParam]
ntParams Newtype
nt))
  where
  con :: Prim sym
con           = forall sym. (SEval sym (GenValue sym) -> Prim sym) -> Prim sym
PFun forall sym. SEval sym (GenValue sym) -> Prim sym
PPrim

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

{-# INLINE evalNewtypeDecl #-}


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

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

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

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

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

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

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

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

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



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

-- | This operation is used to complete the process of setting up recursive declaration
--   groups.  It 'backfills' previously-allocated thunk values with the actual evaluation
--   procedure for the body of recursive definitions.
--
--   In order to faithfully evaluate the nonstrict semantics of Cryptol, we have to take some
--   care in this process.  In particular, we need to ensure that every recursive definition
--   binding is indistinguishable from its eta-expanded form.  The straightforward solution
--   to this is to force an eta-expansion procedure on all recursive definitions.
--   However, for the so-called 'Value' types we can instead optimistically use the 'delayFill'
--   operation and only fall back on full eta expansion if the thunk is double-forced.

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


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

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


-- | Evaluate a declaration, extending the evaluation environment.
--   Two input environments are given: the first is an environment
--   to use when evaluating the body of the declaration; the second
--   is the environment to extend.  There are two environments to
--   handle the subtle name-binding issues that arise from recursive
--   definitions.  The 'read only' environment is used to bring recursive
--   names into scope while we are still defining them.
evalDecl ::
  EvalPrims sym =>
  sym ->
  GenEvalEnv sym  {- ^ A 'read only' environment for use in declaration bodies -} ->
  GenEvalEnv sym  {- ^ An evaluation environment to extend with the given declaration -} ->
  Decl            {- ^ The declaration to evaluate -} ->
  SEval sym (GenEvalEnv sym)
-- evalDecl sym renv env d =
--   let ?range = nameLoc (dName d) in
evalDecl :: forall sym.
EvalPrims sym =>
sym
-> GenEvalEnv sym
-> GenEvalEnv sym
-> Decl
-> SEval sym (GenEvalEnv sym)
evalDecl sym
sym GenEvalEnv sym
renv GenEvalEnv sym
env Decl
d = do
  let ?range = Name -> Range
nameLoc (Decl -> Name
dName Decl
d)
  case Decl -> DeclDef
dDefinition Decl
d of
    DeclDef
DPrim ->
      case ?evalPrim::PrimIdent -> Maybe (Either Expr (Prim sym))
?evalPrim forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Name -> Maybe PrimIdent
asPrim (Decl -> Name
dName Decl
d) of
        Just (Right Prim sym
p) -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall sym.
Backend sym =>
Name -> Prim sym -> GenEvalEnv sym -> GenEvalEnv sym
bindVarDirect (Decl -> Name
dName Decl
d) Prim sym
p GenEvalEnv sym
env
        Just (Left Expr
ex) -> forall sym.
Backend sym =>
sym
-> Name
-> SEval sym (GenValue sym)
-> GenEvalEnv sym
-> SEval sym (GenEvalEnv sym)
bindVar sym
sym (Decl -> Name
dName Decl
d) (forall sym.
(?range::Range, EvalPrims sym) =>
sym -> GenEvalEnv sym -> Expr -> SEval sym (GenValue sym)
evalExpr sym
sym GenEvalEnv sym
renv Expr
ex) GenEvalEnv sym
env
        Maybe (Either Expr (Prim sym))
Nothing        -> forall sym.
Backend sym =>
sym
-> Name
-> SEval sym (GenValue sym)
-> GenEvalEnv sym
-> SEval sym (GenEvalEnv sym)
bindVar sym
sym (Decl -> Name
dName Decl
d) (forall sym a. Backend sym => sym -> Name -> SEval sym a
cryNoPrimError sym
sym (Decl -> Name
dName Decl
d)) GenEvalEnv sym
env

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

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


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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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


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

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

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

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

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

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

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

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

    where
      len :: Nat'
len  = TypeEnv -> Type -> Nat'
evalNumType (forall sym. ListEnv sym -> TypeEnv
leTypes ListEnv sym
lenv) Type
l

  -- XXX we don't currently evaluate these as though they could be recursive, as
  -- they are typechecked that way; the read environment to evalExpr is the same
  -- as the environment to bind a new name in.
  Let Decl
d -> forall (m :: * -> *) a. Monad m => a -> m a
return (Integer
lsz, forall sym.
Name
-> (Integer -> SEval sym (GenValue sym))
-> ListEnv sym
-> ListEnv sym
bindVarList (Decl -> Name
dName Decl
d) (\Integer
i -> (?range::Range,
 ?evalPrim::PrimIdent -> Maybe (Either Expr (Prim sym)),
 ?callStacks::Bool) =>
GenEvalEnv sym -> SEval sym (GenValue sym)
f (forall sym. ListEnv sym -> Integer -> GenEvalEnv sym
evalListEnv ListEnv sym
lenv Integer
i)) ListEnv sym
lenv)
    where
      f :: GenEvalEnv sym -> SEval sym (GenValue sym)
f GenEvalEnv sym
env =
          case Decl -> DeclDef
dDefinition Decl
d of
            DeclDef
DPrim      -> forall a. HasCallStack => String -> [String] -> a
evalPanic String
"evalMatch" [String
"Unexpected local primitive"]
            DForeign FFIFunType
_ -> forall a. HasCallStack => String -> [String] -> a
evalPanic String
"evalMatch" [String
"Unexpected local foreign"]
            DExpr Expr
e    -> forall sym.
(?range::Range, EvalPrims sym) =>
sym -> GenEvalEnv sym -> Expr -> SEval sym (GenValue sym)
evalExpr sym
sym GenEvalEnv sym
env Expr
e