-- |
-- 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 ScopedTypeVariables #-}
{-# LANGUAGE PatternGuards #-}
{-# LANGUAGE ViewPatterns #-}
{-# LANGUAGE NamedFieldPuns #-}

module Cryptol.Eval (
    moduleEnv
  , runEval
  , EvalOpts(..)
  , PPOpts(..)
  , defaultPPOpts
  , Eval
  , EvalEnv
  , emptyEnv
  , evalExpr
  , evalDecls
  , evalNominalDecls
  , evalSel
  , evalSetSel
  , evalEnumCon
  , 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'(..),nMul)
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           Data.Vector(Vector)
import qualified Data.Vector as Vector
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 = sym -> [DeclGroup] -> GenEvalEnv sym -> SEval sym (GenEvalEnv sym)
forall sym.
EvalPrims sym =>
sym -> [DeclGroup] -> GenEvalEnv sym -> SEval sym (GenEvalEnv sym)
evalDecls sym
sym (Module -> [DeclGroup]
forall mname. ModuleG mname -> [DeclGroup]
mDecls Module
m) (GenEvalEnv sym -> SEval sym (GenEvalEnv sym))
-> SEval sym (GenEvalEnv sym) -> SEval sym (GenEvalEnv sym)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<<
                          sym
-> Map Name NominalType
-> GenEvalEnv sym
-> SEval sym (GenEvalEnv sym)
forall sym.
EvalPrims sym =>
sym
-> Map Name NominalType
-> GenEvalEnv sym
-> SEval sym (GenEvalEnv sym)
evalNominalDecls sym
sym (Module -> Map Name NominalType
forall mname. ModuleG mname -> Map Name NominalType
mNominalTypes 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::Range
Range
r in
    sym -> GenEvalEnv sym -> Expr -> SEval sym (GenValue sym)
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" #-}
        Integer -> WordValue sym -> GenValue sym
forall sym. Integer -> WordValue sym -> GenValue sym
VWord Integer
len (WordValue sym -> GenValue sym)
-> SEval sym (WordValue sym) -> SEval sym (GenValue sym)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
          (sym -> [SEval sym (GenValue sym)] -> SEval sym (Maybe (SWord sym))
forall sym.
Backend sym =>
sym -> [SEval sym (GenValue sym)] -> SEval sym (Maybe (SWord sym))
tryFromBits sym
sym [SEval sym (GenValue sym)]
vs SEval sym (Maybe (SWord sym))
-> (Maybe (SWord sym) -> SEval sym (WordValue sym))
-> SEval sym (WordValue sym)
forall a b. SEval sym a -> (a -> SEval sym b) -> SEval sym b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
             Just SWord sym
w  -> WordValue sym -> SEval sym (WordValue sym)
forall a. a -> SEval sym a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SWord sym -> WordValue sym
forall sym. SWord sym -> WordValue sym
wordVal SWord sym
w)
             Maybe (SWord sym)
Nothing -> do [SEval sym (SBit sym)]
xs <- (SEval sym (GenValue sym) -> SEval sym (SEval sym (SBit sym)))
-> [SEval sym (GenValue sym)] -> SEval sym [SEval sym (SBit sym)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (\SEval sym (GenValue sym)
x -> sym -> SEval sym (SBit sym) -> SEval sym (SEval sym (SBit sym))
forall sym a.
Backend sym =>
sym -> SEval sym a -> SEval sym (SEval sym a)
sDelay sym
sym (GenValue sym -> SBit sym
forall sym. GenValue sym -> SBit sym
fromVBit (GenValue sym -> SBit sym)
-> SEval sym (GenValue sym) -> SEval sym (SBit sym)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SEval sym (GenValue sym)
x)) [SEval sym (GenValue sym)]
vs
                           sym
-> Integer -> SeqMap sym (SBit sym) -> SEval sym (WordValue sym)
forall sym.
Backend sym =>
sym
-> Integer -> SeqMap sym (SBit sym) -> SEval sym (WordValue sym)
bitmapWordVal sym
sym Integer
len (SeqMap sym (SBit sym) -> SEval sym (WordValue sym))
-> SeqMap sym (SBit sym) -> SEval sym (WordValue sym)
forall a b. (a -> b) -> a -> b
$ sym -> [SEval sym (SBit sym)] -> SeqMap sym (SBit sym)
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 <- (SEval sym (GenValue sym) -> SEval sym (SEval sym (GenValue sym)))
-> [SEval sym (GenValue sym)]
-> SEval sym [SEval sym (GenValue sym)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (sym
-> SEval sym (GenValue sym) -> SEval sym (SEval sym (GenValue sym))
forall sym a.
Backend sym =>
sym -> SEval sym a -> SEval sym (SEval sym a)
sDelay sym
sym) [SEval sym (GenValue sym)]
vs
        GenValue sym -> SEval sym (GenValue sym)
forall a. a -> SEval sym a
forall (m :: * -> *) a. Monad m => a -> m a
return (GenValue sym -> SEval sym (GenValue sym))
-> GenValue sym -> SEval sym (GenValue sym)
forall a b. (a -> b) -> a -> b
$ Integer -> SeqMap sym (GenValue sym) -> GenValue sym
forall sym. Integer -> SeqMap sym (GenValue sym) -> GenValue sym
VSeq Integer
len (SeqMap sym (GenValue sym) -> GenValue sym)
-> SeqMap sym (GenValue sym) -> GenValue sym
forall a b. (a -> b) -> a -> b
$ sym -> [SEval sym (GenValue sym)] -> SeqMap sym (GenValue sym)
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 (GenEvalEnv sym -> TypeEnv
forall sym. GenEvalEnv sym -> TypeEnv
envTypes GenEvalEnv sym
env) Type
ty
    vs :: [SEval sym (GenValue sym)]
vs  = (Expr -> SEval sym (GenValue sym))
-> [Expr] -> [SEval sym (GenValue sym)]
forall a b. (a -> b) -> [a] -> [b]
map Expr -> SEval sym (GenValue sym)
eval [Expr]
es
    len :: Integer
len = [Expr] -> Integer
forall i a. Num i => [a] -> i
genericLength [Expr]
es

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

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

  ESel Expr
e Selector
sel -> {-# SCC "evalExpr->ESel" #-} do
     GenValue sym
e' <- Expr -> SEval sym (GenValue sym)
eval Expr
e
     sym -> GenValue sym -> Selector -> SEval sym (GenValue sym)
forall sym.
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 (GenEvalEnv sym -> TypeEnv
forall sym. GenEvalEnv sym -> TypeEnv
envTypes GenEvalEnv sym
env) Type
ty
       sym
-> TValue
-> GenValue sym
-> Selector
-> SEval sym (GenValue sym)
-> SEval sym (GenValue sym)
forall sym.
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 <- GenValue sym -> SBit sym
forall sym. GenValue sym -> SBit sym
fromVBit (GenValue sym -> SBit sym)
-> SEval sym (GenValue sym) -> SEval sym (SBit sym)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr -> SEval sym (GenValue sym)
eval Expr
c
     sym
-> SBit sym
-> SEval sym (GenValue sym)
-> SEval sym (GenValue sym)
-> SEval sym (GenValue sym)
forall sym.
Backend sym =>
sym
-> SBit sym
-> SEval sym (GenValue sym)
-> SEval sym (GenValue sym)
-> SEval sym (GenValue sym)
iteValue sym
sym SBit sym
b (Expr -> SEval sym (GenValue sym)
eval Expr
t) (Expr -> SEval sym (GenValue sym)
eval Expr
f)

  ECase Expr
e Map Ident CaseAlt
as Maybe CaseAlt
d -> {-# SCC "evalExpr->ECase" #-} do
    GenValue sym
val <- Expr -> SEval sym (GenValue sym)
eval Expr
e
    let (SInteger sym
con,IntMap (ConValue sym)
fs) = GenValue sym -> (SInteger sym, IntMap (ConValue sym))
forall sym. GenValue sym -> (SInteger sym, IntMap (ConValue sym))
fromVEnum GenValue sym
val
    sym
-> SInteger sym
-> IntMap (ConValue sym)
-> CaseCont sym
-> SEval sym (GenValue sym)
forall sym.
Backend sym =>
sym
-> SInteger sym
-> IntMap (ConValue sym)
-> CaseCont sym
-> SEval sym (GenValue sym)
caseValue sym
sym SInteger sym
con IntMap (ConValue sym)
fs
      CaseCont
        { caseCon :: Map Ident ([SEval sym (GenValue sym)] -> SEval sym (GenValue sym))
caseCon = (?range::Range,
 ?evalPrim::PrimIdent -> Maybe (Either Expr (Prim sym)),
 ?callStacks::Bool) =>
CaseAlt -> [SEval sym (GenValue sym)] -> SEval sym (GenValue sym)
CaseAlt -> [SEval sym (GenValue sym)] -> SEval sym (GenValue sym)
evalCase (CaseAlt -> [SEval sym (GenValue sym)] -> SEval sym (GenValue sym))
-> Map Ident CaseAlt
-> Map
     Ident ([SEval sym (GenValue sym)] -> SEval sym (GenValue sym))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Map Ident CaseAlt
as
        , caseDflt :: Maybe (SEval sym (GenValue sym))
caseDflt =
            do CaseAlt
rhs <- Maybe CaseAlt
d
               SEval sym (GenValue sym) -> Maybe (SEval sym (GenValue sym))
forall a. a -> Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ((?range::Range,
 ?evalPrim::PrimIdent -> Maybe (Either Expr (Prim sym)),
 ?callStacks::Bool) =>
CaseAlt -> [SEval sym (GenValue sym)] -> SEval sym (GenValue sym)
CaseAlt -> [SEval sym (GenValue sym)] -> SEval sym (GenValue sym)
evalCase CaseAlt
rhs [GenValue sym -> SEval sym (GenValue sym)
forall a. a -> SEval sym a
forall (f :: * -> *) a. Applicative f => a -> f a
pure GenValue sym
val])
        }

  EComp Type
n Type
t Expr
h [[Match]]
gs -> {-# SCC "evalExpr->EComp" #-} do
      let len :: Nat'
len  = TypeEnv -> Type -> Nat'
evalNumType (GenEvalEnv sym -> TypeEnv
forall sym. GenEvalEnv sym -> TypeEnv
envTypes GenEvalEnv sym
env) Type
n
      let elty :: TValue
elty = TypeEnv -> Type -> TValue
evalValType (GenEvalEnv sym -> TypeEnv
forall sym. GenEvalEnv sym -> TypeEnv
envTypes GenEvalEnv sym
env) Type
t
      sym
-> GenEvalEnv sym
-> Nat'
-> TValue
-> Expr
-> [[Match]]
-> SEval sym (GenValue sym)
forall sym.
(?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 Name
-> GenEvalEnv sym
-> Maybe (Either (Prim sym) (SEval sym (GenValue sym)))
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
Bool
?callStacks -> sym
-> Name
-> Range
-> SEval sym (GenValue sym)
-> SEval sym (GenValue sym)
forall a. sym -> Name -> Range -> SEval sym a -> SEval sym a
forall sym a.
Backend sym =>
sym -> Name -> Range -> SEval sym a -> SEval sym a
sPushFrame sym
sym Name
n ?range::Range
Range
?range (sym -> GenValue sym -> SEval sym (GenValue sym)
forall sym.
Backend sym =>
sym -> GenValue sym -> SEval sym (GenValue sym)
cacheCallStack sym
sym (GenValue sym -> SEval sym (GenValue sym))
-> SEval sym (GenValue sym) -> SEval sym (GenValue sym)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< sym -> Name -> Prim sym -> SEval sym (GenValue sym)
forall sym.
Backend sym =>
sym -> Name -> Prim sym -> SEval sym (GenValue sym)
evalPrim sym
sym Name
n Prim sym
p)
        | Bool
otherwise   -> sym -> Name -> Prim sym -> SEval sym (GenValue sym)
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
Bool
?callStacks ->
            case Name -> NameInfo
nameInfo Name
n of
              GlobalName {} ->
                 sym
-> Name
-> Range
-> SEval sym (GenValue sym)
-> SEval sym (GenValue sym)
forall a. sym -> Name -> Range -> SEval sym a -> SEval sym a
forall sym a.
Backend sym =>
sym -> Name -> Range -> SEval sym a -> SEval sym a
sPushFrame sym
sym Name
n ?range::Range
Range
?range (sym -> GenValue sym -> SEval sym (GenValue sym)
forall sym.
Backend sym =>
sym -> GenValue sym -> SEval sym (GenValue sym)
cacheCallStack sym
sym (GenValue sym -> SEval sym (GenValue sym))
-> SEval sym (GenValue sym) -> SEval sym (GenValue sym)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< SEval sym (GenValue sym)
val)
              LocalName {} -> sym -> GenValue sym -> SEval sym (GenValue sym)
forall sym.
Backend sym =>
sym -> GenValue sym -> SEval sym (GenValue sym)
cacheCallStack sym
sym (GenValue sym -> SEval sym (GenValue sym))
-> SEval sym (GenValue sym) -> SEval sym (GenValue sym)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< SEval sym (GenValue sym)
val
        | Bool
otherwise -> SEval sym (GenValue sym)
val
      Maybe (Either (Prim sym) (SEval sym (GenValue sym)))
Nothing  -> do
        Doc
envdoc <- sym -> PPOpts -> GenEvalEnv sym -> SEval sym Doc
forall sym.
Backend sym =>
sym -> PPOpts -> GenEvalEnv sym -> SEval sym Doc
ppEnv sym
sym PPOpts
defaultPPOpts GenEvalEnv sym
env
        String -> [String] -> SEval sym (GenValue sym)
forall a. HasCallStack => String -> [String] -> a
panic String
"[Eval] evalExpr"
                     [String
"var `" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Doc -> String
forall a. Show a => a -> String
show (Name -> Doc
forall a. PP a => a -> Doc
pp Name
n) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"` (" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show (Name -> Int
nameUnique Name
n) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
") is not defined"
                     , Doc -> String
forall a. Show a => a -> String
show Doc
envdoc
                     ]

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

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

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

  EAbs Name
n Type
_ty Expr
b -> {-# SCC "evalExpr->EAbs" #-}
    sym
-> (SEval sym (GenValue sym) -> SEval sym (GenValue sym))
-> SEval sym (GenValue sym)
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' <- sym
-> Name
-> SEval sym (GenValue sym)
-> GenEvalEnv sym
-> SEval sym (GenEvalEnv sym)
forall sym.
Backend sym =>
sym
-> Name
-> SEval sym (GenValue sym)
-> GenEvalEnv sym
-> SEval sym (GenEvalEnv sym)
bindVar sym
sym Name
n SEval sym (GenValue sym)
v GenEvalEnv sym
env
                      sym -> GenEvalEnv sym -> Expr -> SEval sym (GenValue sym)
forall sym.
(?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' <- sym -> [DeclGroup] -> GenEvalEnv sym -> SEval sym (GenEvalEnv sym)
forall sym.
EvalPrims sym =>
sym -> [DeclGroup] -> GenEvalEnv sym -> SEval sym (GenEvalEnv sym)
evalDecls sym
sym [DeclGroup]
ds GenEvalEnv sym
env
     sym -> GenEvalEnv sym -> Expr -> SEval sym (GenValue sym)
forall sym.
(?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, (Type -> Bool) -> [Type] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (Type -> Bool
checkProp (Type -> Bool) -> (Type -> Type) -> Type -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. GenEvalEnv sym -> Type -> Type
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
      [] -> sym -> EvalError -> SEval sym (GenValue sym)
forall a. sym -> EvalError -> SEval sym a
forall sym a. Backend sym => sym -> EvalError -> SEval sym a
raiseError sym
sym (String -> EvalError
NoMatchingPropGuardCase (String -> EvalError) -> String -> EvalError
forall a b. (a -> b) -> a -> b
$ String
"Among constraint guards: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [[Doc]] -> String
forall a. Show a => a -> String
show ((Type -> Doc) -> [Type] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Type -> Doc
forall a. PP a => a -> Doc
pp ([Type] -> [Doc])
-> (([Type], Expr) -> [Type]) -> ([Type], Expr) -> [Doc]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([Type], Expr) -> [Type]
forall a b. (a, b) -> a
fst (([Type], Expr) -> [Doc]) -> [([Type], Expr)] -> [[Doc]]
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 = sym -> GenEvalEnv sym -> Expr -> SEval sym (GenValue sym)
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 = sym -> PPOpts -> GenValue sym -> SEval sym Doc
forall sym.
Backend sym =>
sym -> PPOpts -> GenValue sym -> SEval sym Doc
ppValue sym
sym PPOpts
defaultPPOpts
  evalCase :: CaseAlt -> [SEval sym (GenValue sym)] -> SEval sym (GenValue sym)
evalCase (CaseAlt [(Name, Type)]
xs Expr
e) [SEval sym (GenValue sym)]
vs =
    do let addVar :: GenEvalEnv sym
-> ((Name, b), SEval sym (GenValue sym))
-> SEval sym (GenEvalEnv sym)
addVar GenEvalEnv sym
env' ((Name
x,b
_),SEval sym (GenValue sym)
v) = sym
-> Name
-> SEval sym (GenValue sym)
-> GenEvalEnv sym
-> SEval sym (GenEvalEnv sym)
forall sym.
Backend sym =>
sym
-> Name
-> SEval sym (GenValue sym)
-> GenEvalEnv sym
-> SEval sym (GenEvalEnv sym)
bindVar sym
sym Name
x SEval sym (GenValue sym)
v GenEvalEnv sym
env'
       GenEvalEnv sym
newEnv <- (GenEvalEnv sym
 -> ((Name, Type), SEval sym (GenValue sym))
 -> SEval sym (GenEvalEnv sym))
-> GenEvalEnv sym
-> [((Name, Type), SEval sym (GenValue sym))]
-> SEval sym (GenEvalEnv sym)
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM GenEvalEnv sym
-> ((Name, Type), SEval sym (GenValue sym))
-> SEval sym (GenEvalEnv sym)
forall {b}.
GenEvalEnv sym
-> ((Name, b), SEval sym (GenValue sym))
-> SEval sym (GenEvalEnv sym)
addVar GenEvalEnv sym
env ([(Name, Type)]
-> [SEval sym (GenValue sym)]
-> [((Name, Type), SEval sym (GenValue sym))]
forall a b. [a] -> [b] -> [(a, b)]
zip [(Name, Type)]
xs [SEval sym (GenValue sym)]
vs)
       sym -> GenEvalEnv sym -> Expr -> SEval sym (GenValue sym)
forall sym.
(?range::Range, EvalPrims sym) =>
sym -> GenEvalEnv sym -> Expr -> SEval sym (GenValue sym)
evalExpr sym
sym GenEvalEnv sym
newEnv Expr
e

-- | 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' (Type -> Nat') -> [Type] -> [Nat']
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 Nat' -> Nat' -> Bool
forall a. Eq a => a -> a -> Bool
== Nat'
n2
      PC PC
PNeq | [Nat'
n1, Nat'
n2] <- [Nat']
ns -> Nat'
n1 Nat' -> Nat' -> Bool
forall a. Eq a => a -> a -> Bool
/= Nat'
n2
      PC PC
PGeq | [Nat'
n1, Nat'
n2] <- [Nat']
ns -> Nat'
n1 Nat' -> Nat' -> Bool
forall a. Ord a => a -> a -> Bool
>= Nat'
n2
      PC PC
PFin | [Nat'
n] <- [Nat']
ns -> Nat'
n Nat' -> Nat' -> Bool
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
_ -> String -> [String] -> Bool
forall a. HasCallStack => String -> [String] -> a
evalPanic String
"evalProp" [String
"cannot use this as a guarding constraint: ", Doc -> String
forall a. Show a => a -> String
show (Doc -> String) -> (Type -> Doc) -> Type -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> Doc
forall a. PP a => a -> Doc
pp (Type -> String) -> Type -> String
forall a b. (a -> b) -> a -> b
$ TCon -> [Type] -> Type
TCon TCon
tcon [Type]
ts ]
  Type
prop -> String -> [String] -> Bool
forall a. HasCallStack => String -> [String] -> a
evalPanic String
"evalProp" [String
"cannot use this as a guarding constraint: ", Doc -> String
forall a. Show a => a -> String
show (Doc -> String) -> (Type -> Doc) -> Type -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> Doc
forall a. PP a => a -> Doc
pp (Type -> String) -> Type -> String
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 -> String -> [String] -> Nat'
forall a. HasCallStack => String -> [String] -> a
panic String
"checkProp" [String
"Expected `" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Type -> String
forall a. PP a => a -> String
pretty Type
prop String -> String -> String
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 :: forall sym. GenEvalEnv sym -> TypeEnv
envTypes :: TypeEnv
envTypes } = \case
  TCon TCon
tc [Type]
tys
    | TError Kind
KProp <- TCon
tc, [Type
p] <- [Type]
tys ->
      case GenEvalEnv sym -> Type -> Type
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) [GenEvalEnv sym -> Type -> Type
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 (Either Nat' TValue -> Type)
-> (Type -> Either Nat' TValue) -> Type -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypeEnv -> Type -> Either Nat' TValue
evalType TypeEnv
envTypes (Type -> Type) -> [Type] -> [Type]
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 {} -> GenEvalEnv sym -> Type -> Type
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 -> String -> [String] -> Type
forall a. HasCallStack => String -> [String] -> a
panic String
"evalProp" [String
"Could not find type variable `" String -> String -> String
forall a. [a] -> [a] -> [a]
++ TVar -> String
forall a. PP a => a -> String
pretty TVar
tv String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"` in the type evaluation environment"]
  Type
prop -> String -> [String] -> Type
forall a. HasCallStack => String -> [String] -> a
panic String
"evalProp" [String
"Cannot use the following as a type constraint: `" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Type -> String
forall a. PP a => a -> String
pretty Type
prop String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"`"]
  where
    toType :: Either Nat' TValue -> Type
toType = (Nat' -> Type) -> (TValue -> Type) -> Either Nat' TValue -> Type
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 <- sym -> SEval sym CallStack
forall sym. Backend sym => sym -> SEval sym CallStack
sGetCallStack sym
sym
       GenValue sym -> SEval sym (GenValue sym)
forall a. a -> SEval sym a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (CallStack
-> (SEval sym (GenValue sym) -> SEval sym (GenValue sym))
-> GenValue sym
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 <- sym -> SEval sym CallStack
forall sym. Backend sym => sym -> SEval sym CallStack
sGetCallStack sym
sym
       GenValue sym -> SEval sym (GenValue sym)
forall a. a -> SEval sym a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (CallStack -> (TValue -> SEval sym (GenValue sym)) -> GenValue sym
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 <- sym -> SEval sym CallStack
forall sym. Backend sym => sym -> SEval sym CallStack
sGetCallStack sym
sym
       GenValue sym -> SEval sym (GenValue sym)
forall a. a -> SEval sym a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (CallStack -> (Nat' -> SEval sym (GenValue sym)) -> GenValue sym
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
_ -> GenValue sym -> SEval sym (GenValue sym)
forall a. a -> SEval sym a
forall (f :: * -> *) a. Applicative f => a -> f a
pure GenValue sym
v

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

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

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

-- | Introduce the constructor function for a newtype.
evalNominalDecl ::
  EvalPrims sym =>
  sym ->
  NominalType ->
  GenEvalEnv sym ->
  SEval sym (GenEvalEnv sym)
evalNominalDecl :: forall sym.
EvalPrims sym =>
sym -> NominalType -> GenEvalEnv sym -> SEval sym (GenEvalEnv sym)
evalNominalDecl sym
sym NominalType
nt GenEvalEnv sym
env0 =
  case NominalType -> NominalTypeDef
ntDef NominalType
nt of
    Struct StructCon
c -> GenEvalEnv sym -> SEval sym (GenEvalEnv sym)
forall a. a -> SEval sym a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Name -> Prim sym -> GenEvalEnv sym -> GenEvalEnv sym
forall sym.
Backend sym =>
Name -> Prim sym -> GenEvalEnv sym -> GenEvalEnv sym
bindVarDirect (StructCon -> Name
ntConName StructCon
c) (Prim sym -> Prim sym
forall {sym}. Prim sym -> Prim sym
mkCon Prim sym
forall {sym}. Prim sym
structCon) GenEvalEnv sym
env0)
    Enum [EnumCon]
cs  -> (GenEvalEnv sym -> EnumCon -> SEval sym (GenEvalEnv sym))
-> GenEvalEnv sym -> [EnumCon] -> SEval sym (GenEvalEnv sym)
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM GenEvalEnv sym -> EnumCon -> SEval sym (GenEvalEnv sym)
enumCon GenEvalEnv sym
env0 [EnumCon]
cs
    NominalTypeDef
Abstract -> GenEvalEnv sym -> SEval sym (GenEvalEnv sym)
forall a. a -> SEval sym a
forall (f :: * -> *) a. Applicative f => a -> f a
pure GenEvalEnv sym
env0
  where
  structCon :: Prim sym
structCon = (SEval sym (GenValue sym) -> Prim sym) -> Prim sym
forall sym. (SEval sym (GenValue sym) -> Prim sym) -> Prim sym
PFun SEval sym (GenValue sym) -> Prim sym
forall sym. SEval sym (GenValue sym) -> Prim sym
PPrim
  mkCon :: Prim sym -> Prim sym
mkCon Prim sym
c   = (TParam -> Prim sym -> Prim sym)
-> Prim sym -> [TParam] -> Prim sym
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr TParam -> Prim sym -> Prim sym
forall {sym}. TParam -> Prim sym -> Prim sym
tabs Prim sym
c (NominalType -> [TParam]
ntParams NominalType
nt)

  enumCon :: GenEvalEnv sym -> EnumCon -> SEval sym (GenEvalEnv sym)
enumCon GenEvalEnv sym
env EnumCon
c =
    do Vector (SEval sym (GenValue sym)) -> GenValue sym
con <- sym
-> Ident
-> Int
-> SEval sym (Vector (SEval sym (GenValue sym)) -> GenValue sym)
forall sym.
Backend sym =>
sym
-> Ident
-> Int
-> SEval sym (Vector (SEval sym (GenValue sym)) -> GenValue sym)
evalEnumCon sym
sym (Name -> Ident
nameIdent (EnumCon -> Name
ecName EnumCon
c)) (EnumCon -> Int
ecNumber EnumCon
c)
       let done :: [SEval sym (GenValue sym)] -> Prim sym
done        = GenValue sym -> Prim sym
forall sym. GenValue sym -> Prim sym
PVal (GenValue sym -> Prim sym)
-> ([SEval sym (GenValue sym)] -> GenValue sym)
-> [SEval sym (GenValue sym)]
-> Prim sym
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Vector (SEval sym (GenValue sym)) -> GenValue sym
con (Vector (SEval sym (GenValue sym)) -> GenValue sym)
-> ([SEval sym (GenValue sym)]
    -> Vector (SEval sym (GenValue sym)))
-> [SEval sym (GenValue sym)]
-> GenValue sym
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [SEval sym (GenValue sym)] -> Vector (SEval sym (GenValue sym))
forall a. [a] -> Vector a
Vector.fromList ([SEval sym (GenValue sym)] -> Vector (SEval sym (GenValue sym)))
-> ([SEval sym (GenValue sym)] -> [SEval sym (GenValue sym)])
-> [SEval sym (GenValue sym)]
-> Vector (SEval sym (GenValue sym))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [SEval sym (GenValue sym)] -> [SEval sym (GenValue sym)]
forall a. [a] -> [a]
reverse
           fu :: p
-> ([SEval sym (GenValue sym)] -> Prim sym)
-> [SEval sym (GenValue sym)]
-> Prim sym
fu p
_t [SEval sym (GenValue sym)] -> Prim sym
f [SEval sym (GenValue sym)]
xs  = (SEval sym (GenValue sym) -> Prim sym) -> Prim sym
forall sym. (SEval sym (GenValue sym) -> Prim sym) -> Prim sym
PFun (\SEval sym (GenValue sym)
v -> [SEval sym (GenValue sym)] -> Prim sym
f (SEval sym (GenValue sym)
vSEval sym (GenValue sym)
-> [SEval sym (GenValue sym)] -> [SEval sym (GenValue sym)]
forall a. a -> [a] -> [a]
:[SEval sym (GenValue sym)]
xs))
       GenEvalEnv sym -> SEval sym (GenEvalEnv sym)
forall a. a -> SEval sym a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Name -> Prim sym -> GenEvalEnv sym -> GenEvalEnv sym
forall sym.
Backend sym =>
Name -> Prim sym -> GenEvalEnv sym -> GenEvalEnv sym
bindVarDirect (EnumCon -> Name
ecName EnumCon
c)
                           (Prim sym -> Prim sym
forall {sym}. Prim sym -> Prim sym
mkCon ((Type
 -> ([SEval sym (GenValue sym)] -> Prim sym)
 -> [SEval sym (GenValue sym)]
 -> Prim sym)
-> ([SEval sym (GenValue sym)] -> Prim sym)
-> [Type]
-> [SEval sym (GenValue sym)]
-> Prim sym
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Type
-> ([SEval sym (GenValue sym)] -> Prim sym)
-> [SEval sym (GenValue sym)]
-> Prim sym
forall {p} {sym}.
p
-> ([SEval sym (GenValue sym)] -> Prim sym)
-> [SEval sym (GenValue sym)]
-> Prim sym
fu [SEval sym (GenValue sym)] -> Prim sym
done (EnumCon -> [Type]
ecFields EnumCon
c) [])) GenEvalEnv sym
env)

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

{-# INLINE evalNominalDecl #-}

-- | Make the function for a known constructor
evalEnumCon ::
  Backend sym =>
  sym -> Ident -> Int ->
  SEval sym (Vector (SEval sym (GenValue sym)) -> GenValue sym)
evalEnumCon :: forall sym.
Backend sym =>
sym
-> Ident
-> Int
-> SEval sym (Vector (SEval sym (GenValue sym)) -> GenValue sym)
evalEnumCon sym
sym Ident
i Int
n =
  do SInteger sym
tag <- sym -> Integer -> SEval sym (SInteger sym)
forall sym.
Backend sym =>
sym -> Integer -> SEval sym (SInteger sym)
integerLit sym
sym (Int -> Integer
forall a. Integral a => a -> Integer
toInteger Int
n)
     (Vector (SEval sym (GenValue sym)) -> GenValue sym)
-> SEval sym (Vector (SEval sym (GenValue sym)) -> GenValue sym)
forall a. a -> SEval sym a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SInteger sym
-> IntMap (ConInfo (SEval sym (GenValue sym))) -> GenValue sym
forall sym. SInteger sym -> IntMap (ConValue sym) -> GenValue sym
VEnum SInteger sym
tag (IntMap (ConInfo (SEval sym (GenValue sym))) -> GenValue sym)
-> (Vector (SEval sym (GenValue sym))
    -> IntMap (ConInfo (SEval sym (GenValue sym))))
-> Vector (SEval sym (GenValue sym))
-> GenValue sym
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int
-> ConInfo (SEval sym (GenValue sym))
-> IntMap (ConInfo (SEval sym (GenValue sym)))
forall a. Int -> a -> IntMap a
IntMap.singleton Int
n (ConInfo (SEval sym (GenValue sym))
 -> IntMap (ConInfo (SEval sym (GenValue sym))))
-> (Vector (SEval sym (GenValue sym))
    -> ConInfo (SEval sym (GenValue sym)))
-> Vector (SEval sym (GenValue sym))
-> IntMap (ConInfo (SEval sym (GenValue sym)))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Ident
-> Vector (SEval sym (GenValue sym))
-> ConInfo (SEval sym (GenValue sym))
forall a. Ident -> Vector a -> ConInfo a
ConInfo Ident
i)



-- 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 = (GenEvalEnv sym -> DeclGroup -> SEval sym (GenEvalEnv sym))
-> GenEvalEnv sym -> [DeclGroup] -> SEval sym (GenEvalEnv sym)
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM (sym -> GenEvalEnv sym -> DeclGroup -> SEval sym (GenEvalEnv sym)
forall sym.
EvalPrims sym =>
sym -> GenEvalEnv sym -> DeclGroup -> SEval sym (GenEvalEnv sym)
evalDeclGroup sym
x) GenEvalEnv sym
env [DeclGroup]
dgs

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

evalDeclGroup ::
  EvalPrims sym =>
  sym ->
  GenEvalEnv sym ->
  DeclGroup ->
  SEval sym (GenEvalEnv sym)
evalDeclGroup :: 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]
ds0 -> do
      let ds :: [Decl]
ds = (Decl -> Bool) -> [Decl] -> [Decl]
forall a. (a -> Bool) -> [a] -> [a]
filter Decl -> Bool
shouldEval [Decl]
ds0
          -- If there are foreign declarations, we should only evaluate them if
          -- they are not already bound in the environment by the previous
          -- Cryptol.Eval.FFI.evalForeignDecls pass.
          shouldEval :: Decl -> Bool
shouldEval Decl
d =
            case (Decl -> DeclDef
dDefinition Decl
d, Name
-> GenEvalEnv sym
-> Maybe (Either (Prim sym) (SEval sym (GenValue sym)))
forall sym.
Name
-> GenEvalEnv sym
-> Maybe (Either (Prim sym) (SEval sym (GenValue sym)))
lookupVar (Decl -> Name
dName Decl
d) GenEvalEnv sym
env) of
              (DForeign FFIFunType
_ Maybe Expr
_, Just Either (Prim sym) (SEval sym (GenValue sym))
_) -> Bool
False
              (DeclDef, Maybe (Either (Prim sym) (SEval sym (GenValue sym))))
_                      -> Bool
True

      -- declare a "hole" for each declaration
      -- and extend the evaluation environment
      [(Name, Schema, SEval sym (GenValue sym),
  SEval sym (GenValue sym) -> SEval sym ())]
holes <- (Decl
 -> SEval
      sym
      (Name, Schema, SEval sym (GenValue sym),
       SEval sym (GenValue sym) -> SEval sym ()))
-> [Decl]
-> SEval
     sym
     [(Name, Schema, SEval sym (GenValue sym),
       SEval sym (GenValue sym) -> SEval sym ())]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (sym
-> Decl
-> SEval
     sym
     (Name, Schema, SEval sym (GenValue sym),
      SEval sym (GenValue sym) -> SEval sym ())
forall sym.
Backend sym =>
sym
-> Decl
-> SEval
     sym
     (Name, Schema, SEval sym (GenValue sym),
      SEval sym (GenValue sym) -> SEval sym ())
declHole sym
sym) [Decl]
ds
      let holeEnv :: IntMap (Either a (SEval sym (GenValue sym)))
holeEnv = [(Int, Either a (SEval sym (GenValue sym)))]
-> IntMap (Either a (SEval sym (GenValue sym)))
forall a. [(Int, a)] -> IntMap a
IntMap.fromList ([(Int, Either a (SEval sym (GenValue sym)))]
 -> IntMap (Either a (SEval sym (GenValue sym))))
-> [(Int, Either a (SEval sym (GenValue sym)))]
-> IntMap (Either a (SEval sym (GenValue sym)))
forall a b. (a -> b) -> a -> b
$ [ (Name -> Int
nameUnique Name
nm, SEval sym (GenValue sym) -> Either a (SEval sym (GenValue sym))
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 GenEvalEnv sym -> GenEvalEnv sym -> GenEvalEnv sym
forall a. Monoid a => a -> a -> a
`mappend` GenEvalEnv Any
forall sym. GenEvalEnv sym
emptyEnv{ envVars = holeEnv }

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

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

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

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



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

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

fillHole ::
  Backend sym =>
  sym ->
  GenEvalEnv sym ->
  (Name, Schema, SEval sym (GenValue sym), SEval sym (GenValue sym) -> SEval sym ()) ->
  SEval sym ()
fillHole :: 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 Name
-> GenEvalEnv sym
-> Maybe (Either (Prim sym) (SEval sym (GenValue sym)))
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)))
_ -> String -> [String] -> SEval sym ()
forall a. HasCallStack => String -> [String] -> a
evalPanic String
"fillHole" [String
"Recursive definition not completed", Doc -> String
forall a. Show a => a -> String
show (Name -> Doc
ppLocName Name
nm)]


{-# 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 -> String
-> [String]
-> SEval
     sym
     (Name, Schema, SEval sym (GenValue sym),
      SEval sym (GenValue sym) -> SEval sym ())
forall a. HasCallStack => String -> [String] -> a
evalPanic String
"Unexpected primitive declaration in recursive group"
                       [Doc -> String
forall a. Show a => a -> String
show (Name -> Doc
ppLocName Name
nm)]
    DForeign FFIFunType
_ Maybe Expr
me ->
      case Maybe Expr
me of
        Maybe Expr
Nothing -> String
-> [String]
-> SEval
     sym
     (Name, Schema, SEval sym (GenValue sym),
      SEval sym (GenValue sym) -> SEval sym ())
forall a. HasCallStack => String -> [String] -> a
evalPanic
          String
"Unexpected foreign declaration with no cryptol implementation in recursive group"
          [Doc -> String
forall a. Show a => a -> String
show (Name -> Doc
ppLocName Name
nm)]
        Just Expr
_ -> SEval
  sym
  (Name, Schema, SEval sym (GenValue sym),
   SEval sym (GenValue sym) -> SEval sym ())
forall {a}.
SEval sym (Name, Schema, SEval sym a, SEval sym a -> SEval sym ())
doHole
    DExpr Expr
_ -> SEval
  sym
  (Name, Schema, SEval sym (GenValue sym),
   SEval sym (GenValue sym) -> SEval sym ())
forall {a}.
SEval sym (Name, Schema, SEval sym a, SEval sym a -> SEval sym ())
doHole
  where
  doHole :: SEval sym (Name, Schema, SEval sym a, SEval sym a -> SEval sym ())
doHole = do
    (SEval sym a
hole, SEval sym a -> SEval sym ()
fill) <- sym
-> String -> SEval sym (SEval sym a, SEval sym a -> SEval sym ())
forall a.
sym
-> String -> SEval sym (SEval sym a, SEval sym a -> SEval sym ())
forall sym a.
Backend sym =>
sym
-> String -> SEval sym (SEval sym a, SEval sym a -> SEval sym ())
sDeclareHole sym
sym String
msg
    (Name, Schema, SEval sym a, SEval sym a -> SEval sym ())
-> SEval
     sym (Name, Schema, SEval sym a, SEval sym a -> SEval sym ())
forall a. a -> SEval sym a
forall (m :: * -> *) a. Monad m => a -> m a
return (Name
nm, Schema
sch, SEval sym a
hole, SEval sym a -> SEval sym ()
fill)
  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", Doc -> String
forall a. Show a => a -> String
show (Name -> Doc
forall a. PP a => a -> Doc
pp Name
nm)]


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

    DForeign FFIFunType
_ Maybe Expr
me -> 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 the foreign source was
      -- missing, Cryptol was not compiled with FFI support enabled, or we are
      -- in a non-Concrete backend. In that case, we bind the name to the
      -- fallback cryptol implementation if present, or otherwise to an error
      -- computation which will raise an error if we try to evaluate it.
      case Name
-> GenEvalEnv sym
-> Maybe (Either (Prim sym) (SEval sym (GenValue sym)))
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))
_  -> GenEvalEnv sym -> SEval sym (GenEvalEnv sym)
forall a. a -> SEval sym a
forall (f :: * -> *) a. Applicative f => a -> f a
pure GenEvalEnv sym
env
        Maybe (Either (Prim sym) (SEval sym (GenValue sym)))
Nothing -> sym
-> Name
-> SEval sym (GenValue sym)
-> GenEvalEnv sym
-> SEval sym (GenEvalEnv sym)
forall sym.
Backend sym =>
sym
-> Name
-> SEval sym (GenValue sym)
-> GenEvalEnv sym
-> SEval sym (GenEvalEnv sym)
bindVar sym
sym (Decl -> Name
dName Decl
d) SEval sym (GenValue sym)
val GenEvalEnv sym
env
          where
          val :: SEval sym (GenValue sym)
val =
            case Maybe Expr
me of
              Just Expr
e -> sym -> GenEvalEnv sym -> Expr -> SEval sym (GenValue sym)
forall sym.
(?range::Range, EvalPrims sym) =>
sym -> GenEvalEnv sym -> Expr -> SEval sym (GenValue sym)
evalExpr sym
sym GenEvalEnv sym
renv Expr
e
              Maybe Expr
Nothing -> sym -> EvalError -> SEval sym (GenValue sym)
forall a. sym -> EvalError -> SEval sym a
forall sym a. Backend sym => sym -> EvalError -> SEval sym a
raiseError sym
sym (EvalError -> SEval sym (GenValue sym))
-> EvalError -> SEval sym (GenValue sym)
forall a b. (a -> b) -> a -> b
$ Name -> EvalError
FFINotSupported (Name -> EvalError) -> Name -> EvalError
forall a b. (a -> b) -> a -> b
$ Decl -> Name
dName Decl
d

    DExpr Expr
e -> sym
-> Name
-> SEval sym (GenValue sym)
-> GenEvalEnv sym
-> SEval sym (GenEvalEnv sym)
forall sym.
Backend sym =>
sym
-> Name
-> SEval sym (GenValue sym)
-> GenEvalEnv sym
-> SEval sym (GenEvalEnv sym)
bindVar sym
sym (Decl -> Name
dName Decl
d) (sym -> GenEvalEnv sym -> Expr -> SEval sym (GenValue sym)
forall sym.
(?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
_  -> Int -> GenValue sym -> SEval sym (GenValue sym)
forall {a}.
Integral a =>
a -> GenValue sym -> SEval sym (GenValue sym)
listSel Int
ix GenValue sym
val
  where

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

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

  listSel :: a -> GenValue sym -> SEval sym (GenValue sym)
listSel a
n GenValue sym
v =
    case GenValue sym
v of
      VSeq Integer
_ SeqMap sym (GenValue sym)
vs       -> SeqMap sym (GenValue sym) -> Integer -> SEval sym (GenValue sym)
forall sym a. Backend sym => SeqMap sym a -> Integer -> SEval sym a
lookupSeqMap SeqMap sym (GenValue sym)
vs (a -> Integer
forall a. Integral a => a -> Integer
toInteger a
n)
      VStream SeqMap sym (GenValue sym)
vs      -> SeqMap sym (GenValue sym) -> Integer -> SEval sym (GenValue sym)
forall sym a. Backend sym => SeqMap sym a -> Integer -> SEval sym a
lookupSeqMap SeqMap sym (GenValue sym)
vs (a -> Integer
forall a. Integral a => a -> Integer
toInteger a
n)
      VWord Integer
_ WordValue sym
wv      -> SBit sym -> GenValue sym
forall sym. SBit sym -> GenValue sym
VBit (SBit sym -> GenValue sym)
-> SEval sym (SBit sym) -> SEval sym (GenValue sym)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> sym -> WordValue sym -> Integer -> SEval sym (SBit sym)
forall sym.
Backend sym =>
sym -> WordValue sym -> Integer -> SEval sym (SBit sym)
indexWordValue sym
sym WordValue sym
wv (a -> Integer
forall a. Integral a => a -> Integer
toInteger a
n)
      GenValue sym
_               -> do Doc
vdoc <- sym -> PPOpts -> GenValue sym -> SEval sym Doc
forall sym.
Backend sym =>
sym -> PPOpts -> GenValue sym -> SEval sym Doc
ppValue sym
sym PPOpts
defaultPPOpts GenValue sym
val
                            String -> [String] -> SEval sym (GenValue sym)
forall a. HasCallStack => String -> [String] -> a
evalPanic String
"Cryptol.Eval.evalSel"
                              [ String
"Unexpected value in list selection"
                              , Doc -> String
forall a. Show a => a -> String
show Doc
vdoc ]
{-# SPECIALIZE evalSetSel ::
  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 (Int -> Integer
forall a. Integral a => a -> Integer
toInteger Int
ix)

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

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

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

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

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

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

-- | Evaluation environments for list comprehensions: Each variable
-- name is bound to a list of values, one for each element in the list
-- comprehension.
data ListEnv sym = ListEnv
  { 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   = IntMap (Integer -> SEval sym (GenValue sym))
-> IntMap (Integer -> SEval sym (GenValue sym))
-> IntMap (Integer -> SEval sym (GenValue sym))
forall a. IntMap a -> IntMap a -> IntMap a
IntMap.union (ListEnv sym -> IntMap (Integer -> SEval sym (GenValue sym))
forall sym.
ListEnv sym -> IntMap (Integer -> SEval sym (GenValue sym))
leVars  ListEnv sym
l)  (ListEnv sym -> IntMap (Integer -> SEval sym (GenValue sym))
forall sym.
ListEnv sym -> IntMap (Integer -> SEval sym (GenValue sym))
leVars  ListEnv sym
r)
    , leStatic :: IntMap (Either (Prim sym) (SEval sym (GenValue sym)))
leStatic = IntMap (Either (Prim sym) (SEval sym (GenValue sym)))
-> IntMap (Either (Prim sym) (SEval sym (GenValue sym)))
-> IntMap (Either (Prim sym) (SEval sym (GenValue sym)))
forall a. IntMap a -> IntMap a -> IntMap a
IntMap.union (ListEnv sym
-> IntMap (Either (Prim sym) (SEval sym (GenValue sym)))
forall sym.
ListEnv sym
-> IntMap (Either (Prim sym) (SEval sym (GenValue sym)))
leStatic ListEnv sym
l) (ListEnv sym
-> IntMap (Either (Prim sym) (SEval sym (GenValue sym)))
forall sym.
ListEnv sym
-> IntMap (Either (Prim sym) (SEval sym (GenValue sym)))
leStatic ListEnv sym
r)
    , leTypes :: TypeEnv
leTypes  = ListEnv sym -> TypeEnv
forall sym. ListEnv sym -> TypeEnv
leTypes ListEnv sym
l TypeEnv -> TypeEnv -> TypeEnv
forall a. Semigroup a => a -> a -> a
<> ListEnv sym -> TypeEnv
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   = IntMap (Integer -> SEval sym (GenValue sym))
forall a. IntMap a
IntMap.empty
    , leStatic :: IntMap (Either (Prim sym) (SEval sym (GenValue sym)))
leStatic = IntMap (Either (Prim sym) (SEval sym (GenValue sym)))
forall a. IntMap a
IntMap.empty
    , leTypes :: TypeEnv
leTypes  = TypeEnv
forall a. Monoid a => a
mempty
    }

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

-- | Evaluate a list environment at a position.
--   This choses a particular value for the varying
--   locations.
evalListEnv :: ListEnv sym -> Integer -> GenEvalEnv sym
evalListEnv :: 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 = ((Integer -> SEval sym (GenValue sym))
 -> Either a (SEval sym (GenValue sym)))
-> IntMap (Integer -> SEval sym (GenValue sym))
-> IntMap (Either a (SEval sym (GenValue sym)))
forall a b. (a -> b) -> IntMap a -> IntMap b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (SEval sym (GenValue sym) -> Either a (SEval sym (GenValue sym))
forall a b. b -> Either a b
Right (SEval sym (GenValue sym) -> Either a (SEval sym (GenValue sym)))
-> ((Integer -> SEval sym (GenValue sym))
    -> SEval sym (GenValue sym))
-> (Integer -> SEval sym (GenValue sym))
-> Either a (SEval sym (GenValue sym))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Integer -> SEval sym (GenValue sym))
-> Integer -> SEval sym (GenValue sym)
forall a b. (a -> b) -> a -> b
$ Integer
i)) IntMap (Integer -> SEval sym (GenValue sym))
vm
     in EvalEnv{ envVars :: IntMap (Either (Prim sym) (SEval sym (GenValue sym)))
envVars = IntMap (Either (Prim sym) (SEval sym (GenValue sym)))
-> IntMap (Either (Prim sym) (SEval sym (GenValue sym)))
-> IntMap (Either (Prim sym) (SEval sym (GenValue sym)))
forall a. IntMap a -> IntMap a -> IntMap a
IntMap.union IntMap (Either (Prim sym) (SEval sym (GenValue sym)))
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.insert (nameUnique n) vs (leVars 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 <- [ListEnv sym] -> ListEnv sym
forall a. Monoid a => [a] -> a
mconcat ([ListEnv sym] -> ListEnv sym)
-> SEval sym [ListEnv sym] -> SEval sym (ListEnv sym)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ([Match] -> SEval sym (ListEnv sym))
-> [[Match]] -> SEval sym [ListEnv sym]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (sym -> ListEnv sym -> [Match] -> SEval sym (ListEnv sym)
forall sym.
(?range::Range, EvalPrims sym) =>
sym -> ListEnv sym -> [Match] -> SEval sym (ListEnv sym)
branchEnvs sym
sym (GenEvalEnv sym -> ListEnv sym
forall sym. GenEvalEnv sym -> ListEnv sym
toListEnv GenEvalEnv sym
env)) [[Match]]
ms
          sym
-> Nat'
-> TValue
-> SeqMap sym (GenValue sym)
-> SEval sym (GenValue sym)
forall sym.
Backend sym =>
sym
-> Nat'
-> TValue
-> SeqMap sym (GenValue sym)
-> SEval sym (GenValue sym)
mkSeq sym
sym Nat'
len TValue
elty (SeqMap sym (GenValue sym) -> SEval sym (GenValue sym))
-> SEval sym (SeqMap sym (GenValue sym))
-> SEval sym (GenValue sym)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< sym
-> Nat'
-> SeqMap sym (GenValue sym)
-> SEval sym (SeqMap sym (GenValue sym))
forall sym a.
Backend sym =>
sym -> Nat' -> SeqMap sym a -> SEval sym (SeqMap sym a)
memoMap sym
sym Nat'
len ((Integer -> SEval sym (GenValue sym)) -> SeqMap sym (GenValue sym)
forall sym a. (Integer -> SEval sym a) -> SeqMap sym a
indexSeqMap ((Integer -> SEval sym (GenValue sym))
 -> SeqMap sym (GenValue sym))
-> (Integer -> SEval sym (GenValue sym))
-> SeqMap sym (GenValue sym)
forall a b. (a -> b) -> a -> b
$ \Integer
i -> do
              sym -> GenEvalEnv sym -> Expr -> SEval sym (GenValue sym)
forall sym.
(?range::Range, EvalPrims sym) =>
sym -> GenEvalEnv sym -> Expr -> SEval sym (GenValue sym)
evalExpr sym
sym (ListEnv sym -> Integer -> GenEvalEnv sym
forall sym. ListEnv sym -> Integer -> GenEvalEnv sym
evalListEnv ListEnv sym
lenv Integer
i) Expr
body)

{-# SPECIALIZE branchEnvs ::
  (?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 = (Nat', ListEnv sym) -> ListEnv sym
forall a b. (a, b) -> b
snd ((Nat', ListEnv sym) -> ListEnv sym)
-> SEval sym (Nat', ListEnv sym) -> SEval sym (ListEnv sym)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((Nat', ListEnv sym) -> Match -> SEval sym (Nat', ListEnv sym))
-> (Nat', ListEnv sym) -> [Match] -> SEval sym (Nat', ListEnv sym)
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM (sym
-> (Nat', ListEnv sym) -> Match -> SEval sym (Nat', ListEnv sym)
forall sym.
(?range::Range, EvalPrims sym) =>
sym
-> (Nat', ListEnv sym) -> Match -> SEval sym (Nat', ListEnv sym)
evalMatch sym
sym) (Integer -> Nat'
Nat Integer
1, ListEnv sym
env) [Match]
matches

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

-- | Turn a match into the list of environments it represents.
evalMatch ::
  (?range :: Range, EvalPrims sym) =>
  sym ->
  (Nat', ListEnv sym) ->
  Match ->
  SEval sym (Nat', ListEnv sym)
evalMatch :: forall sym.
(?range::Range, EvalPrims sym) =>
sym
-> (Nat', ListEnv sym) -> Match -> SEval sym (Nat', ListEnv sym)
evalMatch sym
sym (Nat'
lsz, ListEnv sym
lenv) Match
m = Nat'
-> SEval sym (Nat', ListEnv sym) -> SEval sym (Nat', ListEnv sym)
forall a b. a -> b -> b
seq Nat'
lsz (SEval sym (Nat', ListEnv sym) -> SEval sym (Nat', ListEnv sym))
-> SEval sym (Nat', ListEnv sym) -> SEval sym (Nat', ListEnv sym)
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 <- sym
-> Nat'
-> SeqMap sym (GenValue sym)
-> SEval sym (SeqMap sym (GenValue sym))
forall sym a.
Backend sym =>
sym -> Nat' -> SeqMap sym a -> SEval sym (SeqMap sym a)
memoMap sym
sym Nat'
lsz (SeqMap sym (GenValue sym)
 -> SEval sym (SeqMap sym (GenValue sym)))
-> SeqMap sym (GenValue sym)
-> SEval sym (SeqMap sym (GenValue sym))
forall a b. (a -> b) -> a -> b
$ (Integer -> SEval sym (GenValue sym)) -> SeqMap sym (GenValue sym)
forall sym a. (Integer -> SEval sym a) -> SeqMap sym a
indexSeqMap ((Integer -> SEval sym (GenValue sym))
 -> SeqMap sym (GenValue sym))
-> (Integer -> SEval sym (GenValue sym))
-> SeqMap sym (GenValue sym)
forall a b. (a -> b) -> a -> b
$ \Integer
i -> sym -> GenEvalEnv sym -> Expr -> SEval sym (GenValue sym)
forall sym.
(?range::Range, EvalPrims sym) =>
sym -> GenEvalEnv sym -> Expr -> SEval sym (GenValue sym)
evalExpr sym
sym (ListEnv sym -> Integer -> GenEvalEnv sym
forall sym. ListEnv sym -> Integer -> GenEvalEnv sym
evalListEnv ListEnv sym
lenv Integer
i) Expr
expr
        let stutter :: (Integer -> t) -> Integer -> t
stutter Integer -> t
xs = \Integer
i -> Integer -> t
xs (Integer
i Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`div` Integer
nLen)
        let lenv' :: ListEnv sym
lenv' = ListEnv sym
lenv { leVars = fmap stutter (leVars lenv) }
        let vs :: Integer -> SEval sym (GenValue sym)
vs Integer
i = do let (Integer
q, Integer
r) = Integer
i Integer -> Integer -> (Integer, Integer)
forall a. Integral a => a -> a -> (a, a)
`divMod` Integer
nLen
                      SeqMap sym (GenValue sym) -> Integer -> SEval sym (GenValue sym)
forall sym a. Backend sym => SeqMap sym a -> Integer -> SEval sym a
lookupSeqMap SeqMap sym (GenValue sym)
vss Integer
q SEval sym (GenValue sym)
-> (GenValue sym -> SEval sym (GenValue sym))
-> SEval sym (GenValue sym)
forall a b. SEval sym a -> (a -> SEval sym b) -> SEval sym b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
                        VWord Integer
_ WordValue sym
w   -> SBit sym -> GenValue sym
forall sym. SBit sym -> GenValue sym
VBit (SBit sym -> GenValue sym)
-> SEval sym (SBit sym) -> SEval sym (GenValue sym)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> sym -> WordValue sym -> Integer -> SEval sym (SBit sym)
forall sym.
Backend sym =>
sym -> WordValue sym -> Integer -> SEval sym (SBit sym)
indexWordValue sym
sym WordValue sym
w Integer
r
                        VSeq Integer
_ SeqMap sym (GenValue sym)
xs'  -> SeqMap sym (GenValue sym) -> Integer -> SEval sym (GenValue sym)
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' -> SeqMap sym (GenValue sym) -> Integer -> SEval sym (GenValue sym)
forall sym a. Backend sym => SeqMap sym a -> Integer -> SEval sym a
lookupSeqMap SeqMap sym (GenValue sym)
xs' Integer
r
                        GenValue sym
_           -> String -> [String] -> SEval sym (GenValue sym)
forall a. HasCallStack => String -> [String] -> a
evalPanic String
"evalMatch" [String
"Not a list value"]
        (Nat', ListEnv sym) -> SEval sym (Nat', ListEnv sym)
forall a. a -> SEval sym a
forall (m :: * -> *) a. Monad m => a -> m a
return (Nat' -> Nat' -> Nat'
nMul Nat'
lsz Nat'
len, Name
-> (Integer -> SEval sym (GenValue sym))
-> ListEnv sym
-> ListEnv sym
forall sym.
Name
-> (Integer -> SEval sym (GenValue sym))
-> ListEnv sym
-> ListEnv sym
bindVarList Name
n Integer -> SEval sym (GenValue sym)
vs ListEnv sym
lenv')

      {- Select from a sequence of infinite length.  Note that only the
         first generator in a sequence of generators may have infinite length,
         so we can just evaluate it once an for all (i.e., it does not change
         on each loop iteration, as it may happen in the finite case). -}
      Nat'
Inf -> do
        let env :: GenEvalEnv sym
env = IntMap (Either (Prim sym) (SEval sym (GenValue sym)))
-> TypeEnv -> GenEvalEnv sym
forall sym.
IntMap (Either (Prim sym) (SEval sym (GenValue sym)))
-> TypeEnv -> GenEvalEnv sym
EvalEnv (ListEnv sym
-> IntMap (Either (Prim sym) (SEval sym (GenValue sym)))
forall sym.
ListEnv sym
-> IntMap (Either (Prim sym) (SEval sym (GenValue sym)))
leStatic ListEnv sym
lenv) (ListEnv sym -> TypeEnv
forall sym. ListEnv sym -> TypeEnv
leTypes ListEnv sym
lenv)
        GenValue sym
xs <- sym -> GenEvalEnv sym -> Expr -> SEval sym (GenValue sym)
forall sym.
(?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   -> SBit sym -> GenValue sym
forall sym. SBit sym -> GenValue sym
VBit (SBit sym -> GenValue sym)
-> SEval sym (SBit sym) -> SEval sym (GenValue sym)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> sym -> WordValue sym -> Integer -> SEval sym (SBit sym)
forall sym.
Backend sym =>
sym -> WordValue sym -> Integer -> SEval sym (SBit sym)
indexWordValue sym
sym WordValue sym
w Integer
i
                     VSeq Integer
_ SeqMap sym (GenValue sym)
xs'  -> SeqMap sym (GenValue sym) -> Integer -> SEval sym (GenValue sym)
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' -> SeqMap sym (GenValue sym) -> Integer -> SEval sym (GenValue sym)
forall sym a. Backend sym => SeqMap sym a -> Integer -> SEval sym a
lookupSeqMap SeqMap sym (GenValue sym)
xs' Integer
i
                     GenValue sym
_           -> String -> [String] -> SEval sym (GenValue sym)
forall a. HasCallStack => String -> [String] -> a
evalPanic String
"evalMatch" [String
"Not a list value"]
        (Nat', ListEnv sym) -> SEval sym (Nat', ListEnv sym)
forall a. a -> SEval sym a
forall (m :: * -> *) a. Monad m => a -> m a
return (Nat'
Inf, Name
-> (Integer -> SEval sym (GenValue sym))
-> ListEnv sym
-> ListEnv sym
forall sym.
Name
-> (Integer -> SEval sym (GenValue sym))
-> ListEnv sym
-> ListEnv sym
bindVarList Name
n Integer -> SEval sym (GenValue sym)
vs ListEnv sym
lenv)

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

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