{-# 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)))
{-# SPECIALIZE moduleEnv ::
ConcPrims =>
Concrete ->
Module ->
GenEvalEnv Concrete ->
SEval Concrete (GenEvalEnv Concrete)
#-}
moduleEnv ::
EvalPrims sym =>
sym ->
Module ->
GenEvalEnv sym ->
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)
#-}
evalExpr ::
(?range :: Range, EvalPrims sym) =>
sym ->
GenEvalEnv sym ->
Expr ->
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
EList [Expr]
es Type
ty
| 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)
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
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
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"]
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
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)
GenValue sym
_ -> forall (f :: * -> *) a. Applicative f => a -> f a
pure GenValue sym
v
{-# 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
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 #-}
{-# SPECIALIZE evalDecls ::
ConcPrims =>
Concrete ->
[DeclGroup] ->
GenEvalEnv Concrete ->
SEval Concrete (GenEvalEnv Concrete)
#-}
evalDecls ::
EvalPrims sym =>
sym ->
[DeclGroup] ->
GenEvalEnv sym ->
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
[(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 }
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
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
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 ()
#-}
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)]
evalDecl ::
EvalPrims sym =>
sym ->
GenEvalEnv sym ->
GenEvalEnv sym ->
Decl ->
SEval sym (GenEvalEnv sym)
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
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
{-# SPECIALIZE evalSel ::
Concrete ->
GenValue Concrete ->
Selector ->
SEval Concrete (GenValue Concrete)
#-}
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"
data ListEnv sym = ListEnv
{ forall sym.
ListEnv sym -> IntMap (Integer -> SEval sym (GenValue sym))
leVars :: !(IntMap.IntMap (Integer -> SEval sym (GenValue sym)))
, forall sym.
ListEnv sym
-> IntMap (Either (Prim sym) (SEval sym (GenValue sym)))
leStatic :: !(IntMap.IntMap (Either (Prim sym) (SEval sym (GenValue sym))))
, 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 #-}
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 #-}
{-# SPECIALIZE evalComp ::
(?range :: Range, ConcPrims) =>
Concrete ->
GenEvalEnv Concrete ->
Nat' ->
TValue ->
Expr ->
[[Match]] ->
SEval Concrete (GenValue Concrete)
#-}
evalComp ::
(?range :: Range, EvalPrims sym) =>
sym ->
GenEvalEnv sym ->
Nat' ->
TValue ->
Expr ->
[[Match]] ->
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)
#-}
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)
#-}
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
From Name
n Type
l Type
_ty Expr
expr ->
case Nat'
len of
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')
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"]
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
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