-- editorconfig-checker-disable-file
-- | The CEK machine.

{-# LANGUAGE AllowAmbiguousTypes      #-}
{-# LANGUAGE BangPatterns             #-}
{-# LANGUAGE ConstraintKinds          #-}
{-# LANGUAGE DataKinds                #-}
{-# LANGUAGE DeriveAnyClass           #-}
{-# LANGUAGE FlexibleInstances        #-}
{-# LANGUAGE ImplicitParams           #-}
{-# LANGUAGE InstanceSigs             #-}
{-# LANGUAGE LambdaCase               #-}
{-# LANGUAGE MultiParamTypeClasses    #-}
{-# LANGUAGE NPlusKPatterns           #-}
{-# LANGUAGE NamedFieldPuns           #-}
{-# LANGUAGE OverloadedStrings        #-}
{-# LANGUAGE RankNTypes               #-}
{-# LANGUAGE ScopedTypeVariables      #-}
{-# LANGUAGE StandaloneKindSignatures #-}
{-# LANGUAGE TypeApplications         #-}
{-# LANGUAGE TypeFamilies             #-}
{-# LANGUAGE TypeOperators            #-}
{-# LANGUAGE UnboxedTuples            #-}
{-# LANGUAGE UndecidableInstances     #-}
{-# LANGUAGE ViewPatterns             #-}

{-# OPTIONS_GHC -fno-warn-orphans #-}

module UntypedPlutusCore.Evaluation.Machine.Cek.Internal
    -- See Note [Compilation peculiarities].
    ( EvaluationResult(..)
    , CekResult(..)
    , cekResultToEither
    , mapTermCekResult
    , CekReport(..)
    , CekValue(..)
    , DischargeResult(..)
    , dischargeResultToTerm
    , ArgStack(..)
    , EmptyOrMultiStack(..)
    , ArgStackNonEmpty(..)
    , CekUserError(..)
    , CekEvaluationException
    , CekBudgetSpender(..)
    , ExBudgetInfo(..)
    , ExBudgetMode(..)
    , CekEmitter
    , CekEmitterInfo(..)
    , EmitterMode(..)
    , CekM (..)
    , ErrorWithCause(..)
    , EvaluationError(..)
    , ExBudgetCategory(..)
    , StepKind(..)
    , ThrowableBuiltins
    , splitStructuralOperational
    , unsafeSplitStructuralOperational
    , runCekDeBruijn
    , dischargeCekValue
    , Context (..)
    , CekValEnv
    , GivenCekReqs
    , GivenCekSpender
    , StepCounter
    , NumberOfStepCounters
    , CounterSize
    , TotalCountIndex
    , Slippage
    , defaultSlippage
    , NTerm
    , runCekM
    )
where

import PlutusPrelude

import UntypedPlutusCore.Core

import Data.RandomAccessList.Class qualified as Env
import Data.RandomAccessList.SkewBinary qualified as Env
import PlutusCore.Builtin
import PlutusCore.DeBruijn
import PlutusCore.Evaluation.Machine.ExBudget
import PlutusCore.Evaluation.Machine.ExBudgetStream
import PlutusCore.Evaluation.Machine.Exception
import PlutusCore.Evaluation.Machine.ExMemoryUsage
import PlutusCore.Evaluation.Machine.MachineParameters
import PlutusCore.Evaluation.Result
import PlutusCore.Pretty

import UntypedPlutusCore.Evaluation.Machine.Cek.CekMachineCosts (CekMachineCosts,
                                                                 CekMachineCostsBase (..))
import UntypedPlutusCore.Evaluation.Machine.Cek.StepCounter

import Control.Exception qualified as Exception
import Control.Monad (unless, when)
import Control.Monad.Catch
import Control.Monad.Except (MonadError, catchError, throwError, tryError)
import Control.Monad.Primitive (PrimMonad (..))
import Control.Monad.ST
import Control.Monad.ST.Unsafe
import Data.Bifunctor
import Data.DList qualified as DList
import Data.Functor.Identity
import Data.Hashable (Hashable)
import Data.Kind qualified as GHC
import Data.Proxy
import Data.Semigroup (stimes)
import Data.Text (Text)
import Data.Vector qualified as V
import Data.Word
import GHC.Generics
import GHC.TypeLits
import Prettyprinter
import Universe

{- Note [Compilation peculiarities]
READ THIS BEFORE TOUCHING ANYTHING IN THIS FILE

Don't use @StrictData@, it makes the machine slower by several percent.

Exporting the 'computeCek' function from this module causes the CEK machine to become slower by
up to 25%. I repeat: just adding 'computeCek' to the export list makes the evaluator substantially
slower. The reason for this is that with 'computeCek' exported the generated GHC Core is much worse:
it contains more lambdas, allocates more stuff etc. While perhaps surprising, this is not an
unusual behavior of the compiler as https://wiki.haskell.org/Performance/GHC explains:

> Indeed, generally speaking GHC will inline across modules just as much as it does within modules,
> with a single large exception. If GHC sees that a function 'f' is called just once, it inlines it
> regardless of how big 'f' is. But once 'f' is exported, GHC can never see that it's called exactly
> once, even if that later turns out to be the case. This inline-once optimisation is pretty
> important in practice.
>
> So: if you care about performance, do not export functions that are not used outside the module
> (i.e. use an explicit export list, and keep it as small as possible).

Now clearly 'computeCek' cannot be inlined in 'runCek' whether it's exported or not, since
'computeCek' is recursive. However:

1. GHC is _usually_ smart enough to perform the worker/wrapper transformation and inline the wrapper
   (however experiments have shown that sticking the internals of the CEK machine, budgeting modes
   and the API into the same file prevents GHC from performing the worker/wrapper transformation for
   some reason likely related to "we've been compiling this for too long, let's leave it at that"
2. GHC seems to be able to massage the definition of 'computeCek' into something more performant
   making use of knowing exactly how 'computeCek' is used, essentially tailoring the definition of
   'computeCek' for a particular invocation in 'runCek'

Hence we don't export 'computeCek' and instead define 'runCek' in this file and export it, even
though the rest of the user-facing API (which 'runCek' is a part of) is defined downstream.

Another problem is handling mutual recursion in the 'computeCek'/'returnCek'/'forceEvaluate'/etc
family. If we keep these functions at the top level, GHC won't be able to pull the constraints out
of the family (confirmed by inspecting Core: GHC thinks that since the superclass constraints
populating the dictionary representing the @Ix fun@ constraint are redundant, they can be replaced
with calls to 'error' in a recursive call, but that changes the dictionary and so it can no longer
be pulled out of recursion). But that entails passing a redundant argument around, which slows down
the machine a tiny little bit.

Hence we define a all happy-path functions having CEK-machine-specific constraints as local
functions making use of a shared context from their parent function. This also allows GHC to inline
almost all of the machine into a single definition (with a bunch of recursive join points in it).

In general, it's advised to run benchmarks (and look at Core output if the results are suspicious)
on any changes in this file.

Finally, it's important to put bang patterns on any 'Int' arguments to ensure that GHC unboxes them:
this can make a surprisingly large difference.
-}

-- | The 'Term's that CEK can execute must have DeBruijn binders
-- 'Name' is not necessary but we leave it here for simplicity and debuggability.
type NTerm uni fun = Term NamedDeBruijn uni fun

-- | The result of evaluating a term with the CEK machine.
data CekResult name uni fun
    = CekFailure (CekEvaluationException name uni fun)
    | CekSuccessConstant (Some (ValueOf uni))
    | CekSuccessNonConstant (Term name uni fun ())

-- | All info produced by a CEK machine run.
data CekReport cost name uni fun = CekReport
    { forall cost name (uni :: * -> *) fun.
CekReport cost name uni fun -> CekResult name uni fun
_cekReportResult :: CekResult name uni fun  -- ^ The result of evaluation.
    , forall cost name (uni :: * -> *) fun.
CekReport cost name uni fun -> cost
_cekReportCost   :: cost                    -- ^ The final @cost@ value.
    , forall cost name (uni :: * -> *) fun.
CekReport cost name uni fun -> [Text]
_cekReportLogs   :: [Text]                  -- ^ Logs emitted during evaluation.
    }

-- | Convert the given 'CekResult' into an 'Either'.
-- This is useful, because in the ledger API we care whether the result is a constant or not, but in
-- tests, executables etc we don't and so handling an either-error-or-term is more natural.
cekResultToEither
    :: CekResult name uni fun
    -> Either (CekEvaluationException name uni fun) (Term name uni fun ())
cekResultToEither :: forall name (uni :: * -> *) fun.
CekResult name uni fun
-> Either
     (CekEvaluationException name uni fun) (Term name uni fun ())
cekResultToEither (CekFailure CekEvaluationException name uni fun
err)             = CekEvaluationException name uni fun
-> Either
     (CekEvaluationException name uni fun) (Term name uni fun ())
forall a b. a -> Either a b
Left CekEvaluationException name uni fun
err
cekResultToEither (CekSuccessConstant Some (ValueOf uni)
val)     = Term name uni fun ()
-> Either
     (CekEvaluationException name uni fun) (Term name uni fun ())
forall a b. b -> Either a b
Right (Term name uni fun ()
 -> Either
      (CekEvaluationException name uni fun) (Term name uni fun ()))
-> Term name uni fun ()
-> Either
     (CekEvaluationException name uni fun) (Term name uni fun ())
forall a b. (a -> b) -> a -> b
$ () -> Some (ValueOf uni) -> Term name uni fun ()
forall name (uni :: * -> *) fun ann.
ann -> Some (ValueOf uni) -> Term name uni fun ann
Constant () Some (ValueOf uni)
val
cekResultToEither (CekSuccessNonConstant Term name uni fun ()
term) = Term name uni fun ()
-> Either
     (CekEvaluationException name uni fun) (Term name uni fun ())
forall a b. b -> Either a b
Right Term name uni fun ()
term

-- | Apply the given function to the 'Term' (if any) stored in the given 'CekResult'.
mapTermCekResult
    :: (Term name uni fun () -> Term name' uni fun ())
    -> CekResult name uni fun
    -> CekResult name' uni fun
mapTermCekResult :: forall name (uni :: * -> *) fun name'.
(Term name uni fun () -> Term name' uni fun ())
-> CekResult name uni fun -> CekResult name' uni fun
mapTermCekResult Term name uni fun () -> Term name' uni fun ()
f (CekFailure CekEvaluationException name uni fun
err)             = CekEvaluationException name' uni fun -> CekResult name' uni fun
forall name (uni :: * -> *) fun.
CekEvaluationException name uni fun -> CekResult name uni fun
CekFailure (CekEvaluationException name' uni fun -> CekResult name' uni fun)
-> CekEvaluationException name' uni fun -> CekResult name' uni fun
forall a b. (a -> b) -> a -> b
$ Term name uni fun () -> Term name' uni fun ()
f (Term name uni fun () -> Term name' uni fun ())
-> CekEvaluationException name uni fun
-> CekEvaluationException name' uni fun
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> CekEvaluationException name uni fun
err
mapTermCekResult Term name uni fun () -> Term name' uni fun ()
_ (CekSuccessConstant Some (ValueOf uni)
val)     = Some (ValueOf uni) -> CekResult name' uni fun
forall name (uni :: * -> *) fun.
Some (ValueOf uni) -> CekResult name uni fun
CekSuccessConstant Some (ValueOf uni)
val
mapTermCekResult Term name uni fun () -> Term name' uni fun ()
f (CekSuccessNonConstant Term name uni fun ()
term) = Term name' uni fun () -> CekResult name' uni fun
forall name (uni :: * -> *) fun.
Term name uni fun () -> CekResult name uni fun
CekSuccessNonConstant (Term name' uni fun () -> CekResult name' uni fun)
-> Term name' uni fun () -> CekResult name' uni fun
forall a b. (a -> b) -> a -> b
$ Term name uni fun () -> Term name' uni fun ()
f Term name uni fun ()
term

data StepKind
    = BConst
    | BVar
    | BLamAbs
    | BApply
    | BDelay
    | BForce
    | BBuiltin -- Cost of evaluating a Builtin AST node, not the function itself
    | BConstr
    | BCase
    deriving stock (Int -> StepKind -> ShowS
[StepKind] -> ShowS
StepKind -> String
(Int -> StepKind -> ShowS)
-> (StepKind -> String) -> ([StepKind] -> ShowS) -> Show StepKind
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> StepKind -> ShowS
showsPrec :: Int -> StepKind -> ShowS
$cshow :: StepKind -> String
show :: StepKind -> String
$cshowList :: [StepKind] -> ShowS
showList :: [StepKind] -> ShowS
Show, StepKind -> StepKind -> Bool
(StepKind -> StepKind -> Bool)
-> (StepKind -> StepKind -> Bool) -> Eq StepKind
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: StepKind -> StepKind -> Bool
== :: StepKind -> StepKind -> Bool
$c/= :: StepKind -> StepKind -> Bool
/= :: StepKind -> StepKind -> Bool
Eq, Eq StepKind
Eq StepKind =>
(StepKind -> StepKind -> Ordering)
-> (StepKind -> StepKind -> Bool)
-> (StepKind -> StepKind -> Bool)
-> (StepKind -> StepKind -> Bool)
-> (StepKind -> StepKind -> Bool)
-> (StepKind -> StepKind -> StepKind)
-> (StepKind -> StepKind -> StepKind)
-> Ord StepKind
StepKind -> StepKind -> Bool
StepKind -> StepKind -> Ordering
StepKind -> StepKind -> StepKind
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: StepKind -> StepKind -> Ordering
compare :: StepKind -> StepKind -> Ordering
$c< :: StepKind -> StepKind -> Bool
< :: StepKind -> StepKind -> Bool
$c<= :: StepKind -> StepKind -> Bool
<= :: StepKind -> StepKind -> Bool
$c> :: StepKind -> StepKind -> Bool
> :: StepKind -> StepKind -> Bool
$c>= :: StepKind -> StepKind -> Bool
>= :: StepKind -> StepKind -> Bool
$cmax :: StepKind -> StepKind -> StepKind
max :: StepKind -> StepKind -> StepKind
$cmin :: StepKind -> StepKind -> StepKind
min :: StepKind -> StepKind -> StepKind
Ord, (forall x. StepKind -> Rep StepKind x)
-> (forall x. Rep StepKind x -> StepKind) -> Generic StepKind
forall x. Rep StepKind x -> StepKind
forall x. StepKind -> Rep StepKind x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. StepKind -> Rep StepKind x
from :: forall x. StepKind -> Rep StepKind x
$cto :: forall x. Rep StepKind x -> StepKind
to :: forall x. Rep StepKind x -> StepKind
Generic, Int -> StepKind
StepKind -> Int
StepKind -> [StepKind]
StepKind -> StepKind
StepKind -> StepKind -> [StepKind]
StepKind -> StepKind -> StepKind -> [StepKind]
(StepKind -> StepKind)
-> (StepKind -> StepKind)
-> (Int -> StepKind)
-> (StepKind -> Int)
-> (StepKind -> [StepKind])
-> (StepKind -> StepKind -> [StepKind])
-> (StepKind -> StepKind -> [StepKind])
-> (StepKind -> StepKind -> StepKind -> [StepKind])
-> Enum StepKind
forall a.
(a -> a)
-> (a -> a)
-> (Int -> a)
-> (a -> Int)
-> (a -> [a])
-> (a -> a -> [a])
-> (a -> a -> [a])
-> (a -> a -> a -> [a])
-> Enum a
$csucc :: StepKind -> StepKind
succ :: StepKind -> StepKind
$cpred :: StepKind -> StepKind
pred :: StepKind -> StepKind
$ctoEnum :: Int -> StepKind
toEnum :: Int -> StepKind
$cfromEnum :: StepKind -> Int
fromEnum :: StepKind -> Int
$cenumFrom :: StepKind -> [StepKind]
enumFrom :: StepKind -> [StepKind]
$cenumFromThen :: StepKind -> StepKind -> [StepKind]
enumFromThen :: StepKind -> StepKind -> [StepKind]
$cenumFromTo :: StepKind -> StepKind -> [StepKind]
enumFromTo :: StepKind -> StepKind -> [StepKind]
$cenumFromThenTo :: StepKind -> StepKind -> StepKind -> [StepKind]
enumFromThenTo :: StepKind -> StepKind -> StepKind -> [StepKind]
Enum, StepKind
StepKind -> StepKind -> Bounded StepKind
forall a. a -> a -> Bounded a
$cminBound :: StepKind
minBound :: StepKind
$cmaxBound :: StepKind
maxBound :: StepKind
Bounded)
    deriving anyclass (StepKind -> ()
(StepKind -> ()) -> NFData StepKind
forall a. (a -> ()) -> NFData a
$crnf :: StepKind -> ()
rnf :: StepKind -> ()
NFData, Eq StepKind
Eq StepKind =>
(Int -> StepKind -> Int) -> (StepKind -> Int) -> Hashable StepKind
Int -> StepKind -> Int
StepKind -> Int
forall a. Eq a => (Int -> a -> Int) -> (a -> Int) -> Hashable a
$chashWithSalt :: Int -> StepKind -> Int
hashWithSalt :: Int -> StepKind -> Int
$chash :: StepKind -> Int
hash :: StepKind -> Int
Hashable)

cekStepCost :: CekMachineCosts -> StepKind -> ExBudget
cekStepCost :: CekMachineCosts -> StepKind -> ExBudget
cekStepCost CekMachineCosts
costs = Identity ExBudget -> ExBudget
forall a. Identity a -> a
runIdentity (Identity ExBudget -> ExBudget)
-> (StepKind -> Identity ExBudget) -> StepKind -> ExBudget
forall b c a. (b -> c) -> (a -> b) -> a -> c
. \case
    StepKind
BConst   -> CekMachineCosts -> Identity ExBudget
forall (f :: * -> *). CekMachineCostsBase f -> f ExBudget
cekConstCost CekMachineCosts
costs
    StepKind
BVar     -> CekMachineCosts -> Identity ExBudget
forall (f :: * -> *). CekMachineCostsBase f -> f ExBudget
cekVarCost CekMachineCosts
costs
    StepKind
BLamAbs  -> CekMachineCosts -> Identity ExBudget
forall (f :: * -> *). CekMachineCostsBase f -> f ExBudget
cekLamCost CekMachineCosts
costs
    StepKind
BApply   -> CekMachineCosts -> Identity ExBudget
forall (f :: * -> *). CekMachineCostsBase f -> f ExBudget
cekApplyCost CekMachineCosts
costs
    StepKind
BDelay   -> CekMachineCosts -> Identity ExBudget
forall (f :: * -> *). CekMachineCostsBase f -> f ExBudget
cekDelayCost CekMachineCosts
costs
    StepKind
BForce   -> CekMachineCosts -> Identity ExBudget
forall (f :: * -> *). CekMachineCostsBase f -> f ExBudget
cekForceCost CekMachineCosts
costs
    StepKind
BBuiltin -> CekMachineCosts -> Identity ExBudget
forall (f :: * -> *). CekMachineCostsBase f -> f ExBudget
cekBuiltinCost CekMachineCosts
costs
    StepKind
BConstr  -> CekMachineCosts -> Identity ExBudget
forall (f :: * -> *). CekMachineCostsBase f -> f ExBudget
cekConstrCost CekMachineCosts
costs
    StepKind
BCase    -> CekMachineCosts -> Identity ExBudget
forall (f :: * -> *). CekMachineCostsBase f -> f ExBudget
cekCaseCost CekMachineCosts
costs

data ExBudgetCategory fun
    = BStep StepKind
    | BBuiltinApp fun  -- Cost of evaluating a fully applied builtin function
    | BStartup
    deriving stock (Int -> ExBudgetCategory fun -> ShowS
[ExBudgetCategory fun] -> ShowS
ExBudgetCategory fun -> String
(Int -> ExBudgetCategory fun -> ShowS)
-> (ExBudgetCategory fun -> String)
-> ([ExBudgetCategory fun] -> ShowS)
-> Show (ExBudgetCategory fun)
forall fun. Show fun => Int -> ExBudgetCategory fun -> ShowS
forall fun. Show fun => [ExBudgetCategory fun] -> ShowS
forall fun. Show fun => ExBudgetCategory fun -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall fun. Show fun => Int -> ExBudgetCategory fun -> ShowS
showsPrec :: Int -> ExBudgetCategory fun -> ShowS
$cshow :: forall fun. Show fun => ExBudgetCategory fun -> String
show :: ExBudgetCategory fun -> String
$cshowList :: forall fun. Show fun => [ExBudgetCategory fun] -> ShowS
showList :: [ExBudgetCategory fun] -> ShowS
Show, ExBudgetCategory fun -> ExBudgetCategory fun -> Bool
(ExBudgetCategory fun -> ExBudgetCategory fun -> Bool)
-> (ExBudgetCategory fun -> ExBudgetCategory fun -> Bool)
-> Eq (ExBudgetCategory fun)
forall fun.
Eq fun =>
ExBudgetCategory fun -> ExBudgetCategory fun -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall fun.
Eq fun =>
ExBudgetCategory fun -> ExBudgetCategory fun -> Bool
== :: ExBudgetCategory fun -> ExBudgetCategory fun -> Bool
$c/= :: forall fun.
Eq fun =>
ExBudgetCategory fun -> ExBudgetCategory fun -> Bool
/= :: ExBudgetCategory fun -> ExBudgetCategory fun -> Bool
Eq, Eq (ExBudgetCategory fun)
Eq (ExBudgetCategory fun) =>
(ExBudgetCategory fun -> ExBudgetCategory fun -> Ordering)
-> (ExBudgetCategory fun -> ExBudgetCategory fun -> Bool)
-> (ExBudgetCategory fun -> ExBudgetCategory fun -> Bool)
-> (ExBudgetCategory fun -> ExBudgetCategory fun -> Bool)
-> (ExBudgetCategory fun -> ExBudgetCategory fun -> Bool)
-> (ExBudgetCategory fun
    -> ExBudgetCategory fun -> ExBudgetCategory fun)
-> (ExBudgetCategory fun
    -> ExBudgetCategory fun -> ExBudgetCategory fun)
-> Ord (ExBudgetCategory fun)
ExBudgetCategory fun -> ExBudgetCategory fun -> Bool
ExBudgetCategory fun -> ExBudgetCategory fun -> Ordering
ExBudgetCategory fun
-> ExBudgetCategory fun -> ExBudgetCategory fun
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall fun. Ord fun => Eq (ExBudgetCategory fun)
forall fun.
Ord fun =>
ExBudgetCategory fun -> ExBudgetCategory fun -> Bool
forall fun.
Ord fun =>
ExBudgetCategory fun -> ExBudgetCategory fun -> Ordering
forall fun.
Ord fun =>
ExBudgetCategory fun
-> ExBudgetCategory fun -> ExBudgetCategory fun
$ccompare :: forall fun.
Ord fun =>
ExBudgetCategory fun -> ExBudgetCategory fun -> Ordering
compare :: ExBudgetCategory fun -> ExBudgetCategory fun -> Ordering
$c< :: forall fun.
Ord fun =>
ExBudgetCategory fun -> ExBudgetCategory fun -> Bool
< :: ExBudgetCategory fun -> ExBudgetCategory fun -> Bool
$c<= :: forall fun.
Ord fun =>
ExBudgetCategory fun -> ExBudgetCategory fun -> Bool
<= :: ExBudgetCategory fun -> ExBudgetCategory fun -> Bool
$c> :: forall fun.
Ord fun =>
ExBudgetCategory fun -> ExBudgetCategory fun -> Bool
> :: ExBudgetCategory fun -> ExBudgetCategory fun -> Bool
$c>= :: forall fun.
Ord fun =>
ExBudgetCategory fun -> ExBudgetCategory fun -> Bool
>= :: ExBudgetCategory fun -> ExBudgetCategory fun -> Bool
$cmax :: forall fun.
Ord fun =>
ExBudgetCategory fun
-> ExBudgetCategory fun -> ExBudgetCategory fun
max :: ExBudgetCategory fun
-> ExBudgetCategory fun -> ExBudgetCategory fun
$cmin :: forall fun.
Ord fun =>
ExBudgetCategory fun
-> ExBudgetCategory fun -> ExBudgetCategory fun
min :: ExBudgetCategory fun
-> ExBudgetCategory fun -> ExBudgetCategory fun
Ord, (forall x. ExBudgetCategory fun -> Rep (ExBudgetCategory fun) x)
-> (forall x. Rep (ExBudgetCategory fun) x -> ExBudgetCategory fun)
-> Generic (ExBudgetCategory fun)
forall x. Rep (ExBudgetCategory fun) x -> ExBudgetCategory fun
forall x. ExBudgetCategory fun -> Rep (ExBudgetCategory fun) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall fun x. Rep (ExBudgetCategory fun) x -> ExBudgetCategory fun
forall fun x. ExBudgetCategory fun -> Rep (ExBudgetCategory fun) x
$cfrom :: forall fun x. ExBudgetCategory fun -> Rep (ExBudgetCategory fun) x
from :: forall x. ExBudgetCategory fun -> Rep (ExBudgetCategory fun) x
$cto :: forall fun x. Rep (ExBudgetCategory fun) x -> ExBudgetCategory fun
to :: forall x. Rep (ExBudgetCategory fun) x -> ExBudgetCategory fun
Generic)
    deriving anyclass (ExBudgetCategory fun -> ()
(ExBudgetCategory fun -> ()) -> NFData (ExBudgetCategory fun)
forall fun. NFData fun => ExBudgetCategory fun -> ()
forall a. (a -> ()) -> NFData a
$crnf :: forall fun. NFData fun => ExBudgetCategory fun -> ()
rnf :: ExBudgetCategory fun -> ()
NFData, Eq (ExBudgetCategory fun)
Eq (ExBudgetCategory fun) =>
(Int -> ExBudgetCategory fun -> Int)
-> (ExBudgetCategory fun -> Int) -> Hashable (ExBudgetCategory fun)
Int -> ExBudgetCategory fun -> Int
ExBudgetCategory fun -> Int
forall a. Eq a => (Int -> a -> Int) -> (a -> Int) -> Hashable a
forall fun. Hashable fun => Eq (ExBudgetCategory fun)
forall fun. Hashable fun => Int -> ExBudgetCategory fun -> Int
forall fun. Hashable fun => ExBudgetCategory fun -> Int
$chashWithSalt :: forall fun. Hashable fun => Int -> ExBudgetCategory fun -> Int
hashWithSalt :: Int -> ExBudgetCategory fun -> Int
$chash :: forall fun. Hashable fun => ExBudgetCategory fun -> Int
hash :: ExBudgetCategory fun -> Int
Hashable)
instance Show fun => Pretty (ExBudgetCategory fun) where
    pretty :: forall ann. ExBudgetCategory fun -> Doc ann
pretty = ExBudgetCategory fun -> Doc ann
forall a ann. Show a => a -> Doc ann
viaShow

instance ExBudgetBuiltin fun (ExBudgetCategory fun) where
    exBudgetBuiltin :: fun -> ExBudgetCategory fun
exBudgetBuiltin = fun -> ExBudgetCategory fun
forall fun. fun -> ExBudgetCategory fun
BBuiltinApp

{- Note [Show instance for BuiltinRuntime]
We need to be able to print 'CekValue's and for that we need a 'Show' instance for 'BuiltinRuntime',
but functions are not printable and hence we provide a dummy instance.
-}

-- See Note [Show instance for BuiltinRuntime].
instance Show (BuiltinRuntime (CekValue uni fun ann)) where
    show :: BuiltinRuntime (CekValue uni fun ann) -> String
show BuiltinRuntime (CekValue uni fun ann)
_ = String
"<builtin_runtime>"

-- | A LIFO stack of 'CekValue's, used to record multiple arguments that need to be pushed
-- onto the context in reverse order.  Currently used by 'FrameConstr' for collecting the
-- elements of a 'Constr' as it is cheap to prepend new elements in 'ArgStack'.
data ArgStack uni fun ann =
  NilStack
  | ConsStack !(CekValue uni fun ann) !(ArgStack uni fun ann)

-- | A non-empty variant of 'ArgStack', used in 'FrameAwaitFunValueN' to store arguments
-- that will be applied to a term. More efficient than 'ArgStack', since this saves one
-- evaluation cycle by ensuring there is no 'NilStack'.
data ArgStackNonEmpty uni fun ann =
  LastStackNonEmpty !(CekValue uni fun ann)
  | ConsStackNonEmpty !(CekValue uni fun ann) !(ArgStackNonEmpty uni fun ann)

-- | An alternative version of 'ArgStack' that uses 'ArgNonEmptyStack' when non-empty.
-- Used in 'VConstr'. Once all evaluated elements of 'Constr' is collecting to 'ArgStack'
-- in 'FrameConstr', the collected elements gets reversed and put into 'VConstr' as
-- `EmptyOrMultiStack`. 'VConstr' using `EmptyOrMultiStack` is more efficient than 'ArgStack' when casing,
-- since 'FrameAwaitFunValueN' can be dispatched with a single pattern match.
data EmptyOrMultiStack uni fun ann =
  EmptyStack
  | MultiStack !(ArgStackNonEmpty uni fun ann)

deriving stock instance (GShow uni, Everywhere uni Show, Show fun, Show ann, Closed uni)
    => Show (ArgStack uni fun ann)
deriving stock instance (GShow uni, Everywhere uni Show, Show fun, Show ann, Closed uni)
    => Show (EmptyOrMultiStack uni fun ann)
deriving stock instance (GShow uni, Everywhere uni Show, Show fun, Show ann, Closed uni)
    => Show (ArgStackNonEmpty uni fun ann)

-- 'Values' for the modified CEK machine.
data CekValue uni fun ann =
    -- This bang gave us a 1-2% speed-up at the time of writing.
    VCon !(Some (ValueOf uni))
  | VDelay !(NTerm uni fun ann) !(CekValEnv uni fun ann)
  | VLamAbs !NamedDeBruijn !(NTerm uni fun ann) !(CekValEnv uni fun ann)
    -- | A partial builtin application, accumulating arguments for eventual full application.
    -- We don't need a 'CekValEnv' here unlike in the other constructors, because 'VBuiltin'
    -- values always store their corresponding 'Term's fully discharged, see the comments at
    -- the call sites (search for 'VBuiltin').
  | VBuiltin
      !fun
      -- ^ So that we know, for what builtin we're calculating the cost. We can sneak this into
      -- 'BuiltinRuntime', so that we don't need to store it here, but somehow doing so was
      -- consistently slowing evaluation down by half a percent. Might be noise, might be not, but
      -- at least we know that removing this @fun@ is not helpful anyway. See this commit reversing
      -- the change: https://github.com/IntersectMBO/plutus/pull/4778/commits/86a3e24ca3c671cc27c6f4344da2bcd14f961706
      (NTerm uni fun ())
      -- ^ This must be lazy. It represents the fully discharged partial application of the builtin
      -- function that we're going to run when it's fully saturated.  We need the 'Term' to be able
      -- to return it in case full saturation is never achieved and a partial application needs to
      -- be returned in the result. The laziness is important, because the arguments are discharged
      -- values and discharging is expensive, so we don't want to do it unless we really have
      -- to. Making this field strict resulted in a 3-4.5% slowdown at the time of writing.
      !(BuiltinRuntime (CekValue uni fun ann))
      -- ^ The partial application and its costing function.
      -- Check the docs of 'BuiltinRuntime' for details.
    -- | A constructor value, including fully computed arguments and the tag.
  | VConstr {-# UNPACK #-} !Word64 !(EmptyOrMultiStack uni fun ann)

deriving stock instance (GShow uni, Everywhere uni Show, Show fun, Show ann, Closed uni)
    => Show (CekValue uni fun ann)

type CekValEnv uni fun ann = Env.RAList (CekValue uni fun ann)

-- | The CEK machine is parameterized over a @spendBudget@ function. This makes the budgeting machinery extensible
-- and allows us to separate budgeting logic from evaluation logic and avoid branching on the union
-- of all possible budgeting state types during evaluation.
newtype CekBudgetSpender uni fun s = CekBudgetSpender
    { forall (uni :: * -> *) fun s.
CekBudgetSpender uni fun s
-> ExBudgetCategory fun -> ExBudget -> CekM uni fun s ()
unCekBudgetSpender :: ExBudgetCategory fun -> ExBudget -> CekM uni fun s ()
    }

-- General enough to be able to handle a spender having one, two or any number of 'STRef's
-- under the hood.
-- | Runtime budgeting info.
data ExBudgetInfo cost uni fun s = ExBudgetInfo
    { forall cost (uni :: * -> *) fun s.
ExBudgetInfo cost uni fun s -> CekBudgetSpender uni fun s
_exBudgetModeSpender       :: !(CekBudgetSpender uni fun s)  -- ^ A spending function.
    , forall cost (uni :: * -> *) fun s.
ExBudgetInfo cost uni fun s -> ST s cost
_exBudgetModeGetFinal      :: !(ST s cost) -- ^ For accessing the final state.
    , forall cost (uni :: * -> *) fun s.
ExBudgetInfo cost uni fun s -> ST s ExBudget
_exBudgetModeGetCumulative :: !(ST s ExBudget) -- ^ For accessing the cumulative budget.
    }

-- We make a separate data type here just to save the caller of the CEK machine from those pesky
-- 'ST'-related details.
-- | A budgeting mode to execute the CEK machine in.
newtype ExBudgetMode cost uni fun = ExBudgetMode
    { forall cost (uni :: * -> *) fun.
ExBudgetMode cost uni fun
-> forall s. ST s (ExBudgetInfo cost uni fun s)
unExBudgetMode :: forall s. ST s (ExBudgetInfo cost uni fun s)
    }

{- Note [Cost slippage]
Tracking the budget usage for every step in the machine adds a lot of overhead. To reduce this,
we adopt a technique which allows some overshoot of the budget ("slippage"), but only a bounded
amount.

To do this we:
- Track all the machine steps of all kinds in an set of counters in a 'StepCounter'
- Actually "spend" the budget when we've done more than some fixed number of steps, or at the end.

This saves a *lot* of time, at the cost of potentially overshooting the budget by slippage*step_cost,
which is okay so long as we bound the slippage appropriately.

Note that we're only proposing to do this for machine steps, since it's plausible that we can track
them in an optimized way. Builtins are more complicated (and infrequent), so we can just budget them
properly when we hit them.

There are two options for how to bound the slippage:
1. As a fixed number of steps
2. As a proportion of the overall budget

Option 2 initially seems much better as a bound: if we run N scripts with an overall budget of B, then
the potential overrun from 1 is N*slippage, whereas the overrun from 2 is B*slippage. That is, 2
says we always overrun by a fraction of the total amount of time you were expecting, whereas 1 says
it depends how many scripts you run... so if I send you a lot of small scripts, I could cause a lot
of overrun.

However, it turns out (empirically) that we can pick a number for 1 that gives us most of the speedup, but such
that the maximum overrun is negligible (e.g. much smaller than the "startup cost"). So in the end
we opted for option 1, which also happens to be simpler to implement.
-}

{- Note [Structure of the step counter]
The step counter is kept in a 'MutablePrimArray', which is a fast way of storing a bunch of
mutable 'Word8's.
This suits our purposes, as we need one counter for every step type, and one for the total number.

We keep the counters for each step in the first indices, so we can index them simply by using
the 'Enum' instance of 'StepKind', and the total counter in the last index.
-}

-- So that we don't need to update 'NumberOfStepCounters' manually, which would be extremely
-- error-prone and has caused a bug in the past.
type CountConstructorsEnum :: (GHC.Type -> GHC.Type) -> Nat
type family CountConstructorsEnum rep where
    CountConstructorsEnum U1         = 1
    CountConstructorsEnum (M1 _ _ f) = CountConstructorsEnum f
    CountConstructorsEnum (f :+: g)  = CountConstructorsEnum f + CountConstructorsEnum g
    CountConstructorsEnum V1         = TypeError ('Text "Cannot be empty")
    CountConstructorsEnum (f :*: g)  = TypeError ('Text "Cannot be a non-enumeration type")
    CountConstructorsEnum (K1 _ _)   = TypeError ('Text "Cannot be a non-enumeration type")
    CountConstructorsEnum (Rec1 _)   = TypeError ('Text "Cannot be a non-enumeration type")
    CountConstructorsEnum Par1       =
        TypeError ('Text "If you really want a parameterized type, handle this clause")

-- | The number of step counters that we need, should be the same as the number of constructors
-- of 'StepKind'.
type NumberOfStepCounters = CountConstructorsEnum (Rep StepKind)
-- | The total number of counters that we need, one extra for the total counter.
-- See Note [Structure of the step counter]
type CounterSize = NumberOfStepCounters + 1
-- | The index at which the total step counter is kept.
-- See Note [Structure of the step counter]
type TotalCountIndex = NumberOfStepCounters

type Slippage = Word8
-- See Note [Cost slippage]
-- | The default number of slippage (in machine steps) to allow.
defaultSlippage :: Slippage
defaultSlippage :: Slippage
defaultSlippage = Slippage
200

{- Note [DList-based emitting]
Instead of emitting log lines one by one, we have a 'DList' of them in the type of emitters
(see 'CekEmitter'). That 'DList' comes from 'Emitter' and allows the latter to be an efficient
monad for logging. We leak this implementation detail in the type of emitters, because it's the
most efficient way of doing emitting, see
https://github.com/IntersectMBO/plutus/pull/4421#issuecomment-1059186586
-}

-- See Note [DList-based emitting].
-- | The CEK machine is parameterized over an emitter function, similar to 'CekBudgetSpender'.
type CekEmitter uni fun s = DList.DList Text -> CekM uni fun s ()

-- | Runtime emitter info, similar to 'ExBudgetInfo'.
data CekEmitterInfo uni fun s = CekEmitterInfo {
    forall (uni :: * -> *) fun s.
CekEmitterInfo uni fun s -> CekEmitter uni fun s
_cekEmitterInfoEmit       :: !(CekEmitter uni fun s)
    , forall (uni :: * -> *) fun s.
CekEmitterInfo uni fun s -> ST s [Text]
_cekEmitterInfoGetFinal :: !(ST s [Text])
    }

-- | An emitting mode to execute the CEK machine in, similar to 'ExBudgetMode'.
newtype EmitterMode uni fun = EmitterMode
    { forall (uni :: * -> *) fun.
EmitterMode uni fun
-> forall s. ST s ExBudget -> ST s (CekEmitterInfo uni fun s)
unEmitterMode :: forall s. ST s ExBudget -> ST s (CekEmitterInfo uni fun s)
    }

{- Note [Implicit parameters in the machine]
The traditional way to pass context into a function is to use 'ReaderT'. However, 'ReaderT' has some
disadvantages.
- It requires threading through the context even where you don't need it (every monadic bind)
- It *can* often be optimized away, but this requires GHC to be somewhat clever and do a lot of
  case-of-case to lift all the arguments out.

Moreover, if your context is global (i.e. constant across the lifetime of the monad, i.e. you don't
need 'local'), then you're buying some extra power (the ability to pass in a different context somewhere
deep inside the computation) which you don't need.

There are three main alternatives:
- Explicit function parameters. Simple, doesn't get tied up in the Monad operations, *does* still
present the appearance of letting you do 'local'. But a bit cluttered.
- Implicit parameters. A bit esoteric, can be bundled up into a constraint synonym and just piped to
where they're needed, essentially the same as explicit parameters in terms of runtime.
- Constraints via 'reflection'. Quite esoteric, *does* get you global parameters (within their scope),
bit of a hassle threading around all the extra type parameters.

We're using implicit parameters for now, which seems to strike a good balance of speed and convenience.
I haven't tried 'reflection' in detail, but I believe the main thing it would do is to make the parameters
global - but we already have this for most of the hot functions by making them all local definitions, so
they don't actually take the context as an argument even at the source level.
-}

-- | Implicit parameter for the builtin runtime.
type GivenCekRuntime uni fun ann = (?cekRuntime :: BuiltinsRuntime fun (CekValue uni fun ann))
type GivenCekCaserBuiltin uni = (?cekCaserBuiltin :: CaserBuiltin uni)
-- | Implicit parameter for the log emitter reference.
type GivenCekEmitter uni fun s = (?cekEmitter :: CekEmitter uni fun s)
-- | Implicit parameter for budget spender.
type GivenCekSpender uni fun s = (?cekBudgetSpender :: CekBudgetSpender uni fun s)
type GivenCekSlippage = (?cekSlippage :: Slippage)
type GivenCekStepCounter s = (?cekStepCounter :: StepCounter CounterSize s)
type GivenCekCosts = (?cekCosts :: CekMachineCosts)

-- | Constraint requiring all of the machine's implicit parameters.
type GivenCekReqs uni fun ann s =
    ( GivenCekRuntime uni fun ann
    , GivenCekCaserBuiltin uni
    , GivenCekEmitter uni fun s
    , GivenCekSpender uni fun s
    , GivenCekSlippage
    , GivenCekStepCounter s
    , GivenCekCosts
    )

data CekUserError
    = CekCaseBuiltinError Text -- ^ 'Case' over a value of a built-in type failed.
    | CekOutOfExError !ExRestrictingBudget -- ^ The final overspent (i.e. negative) budget.
    | CekEvaluationFailure -- ^ Error has been called or a builtin application has failed
    deriving stock (Int -> CekUserError -> ShowS
[CekUserError] -> ShowS
CekUserError -> String
(Int -> CekUserError -> ShowS)
-> (CekUserError -> String)
-> ([CekUserError] -> ShowS)
-> Show CekUserError
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> CekUserError -> ShowS
showsPrec :: Int -> CekUserError -> ShowS
$cshow :: CekUserError -> String
show :: CekUserError -> String
$cshowList :: [CekUserError] -> ShowS
showList :: [CekUserError] -> ShowS
Show, CekUserError -> CekUserError -> Bool
(CekUserError -> CekUserError -> Bool)
-> (CekUserError -> CekUserError -> Bool) -> Eq CekUserError
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: CekUserError -> CekUserError -> Bool
== :: CekUserError -> CekUserError -> Bool
$c/= :: CekUserError -> CekUserError -> Bool
/= :: CekUserError -> CekUserError -> Bool
Eq, (forall x. CekUserError -> Rep CekUserError x)
-> (forall x. Rep CekUserError x -> CekUserError)
-> Generic CekUserError
forall x. Rep CekUserError x -> CekUserError
forall x. CekUserError -> Rep CekUserError x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. CekUserError -> Rep CekUserError x
from :: forall x. CekUserError -> Rep CekUserError x
$cto :: forall x. Rep CekUserError x -> CekUserError
to :: forall x. Rep CekUserError x -> CekUserError
Generic)
    deriving anyclass (CekUserError -> ()
(CekUserError -> ()) -> NFData CekUserError
forall a. (a -> ()) -> NFData a
$crnf :: CekUserError -> ()
rnf :: CekUserError -> ()
NFData)

type CekM :: (GHC.Type -> GHC.Type) -> GHC.Type -> GHC.Type -> GHC.Type -> GHC.Type
-- | The monad the CEK machine runs in.
newtype CekM uni fun s a = CekM
    { forall (uni :: * -> *) fun s a. CekM uni fun s a -> ST s a
unCekM :: ST s a
    } deriving newtype ((forall a b. (a -> b) -> CekM uni fun s a -> CekM uni fun s b)
-> (forall a b. a -> CekM uni fun s b -> CekM uni fun s a)
-> Functor (CekM uni fun s)
forall a b. a -> CekM uni fun s b -> CekM uni fun s a
forall a b. (a -> b) -> CekM uni fun s a -> CekM uni fun s b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
forall (uni :: * -> *) fun s a b.
a -> CekM uni fun s b -> CekM uni fun s a
forall (uni :: * -> *) fun s a b.
(a -> b) -> CekM uni fun s a -> CekM uni fun s b
$cfmap :: forall (uni :: * -> *) fun s a b.
(a -> b) -> CekM uni fun s a -> CekM uni fun s b
fmap :: forall a b. (a -> b) -> CekM uni fun s a -> CekM uni fun s b
$c<$ :: forall (uni :: * -> *) fun s a b.
a -> CekM uni fun s b -> CekM uni fun s a
<$ :: forall a b. a -> CekM uni fun s b -> CekM uni fun s a
Functor, Functor (CekM uni fun s)
Functor (CekM uni fun s) =>
(forall a. a -> CekM uni fun s a)
-> (forall a b.
    CekM uni fun s (a -> b) -> CekM uni fun s a -> CekM uni fun s b)
-> (forall a b c.
    (a -> b -> c)
    -> CekM uni fun s a -> CekM uni fun s b -> CekM uni fun s c)
-> (forall a b.
    CekM uni fun s a -> CekM uni fun s b -> CekM uni fun s b)
-> (forall a b.
    CekM uni fun s a -> CekM uni fun s b -> CekM uni fun s a)
-> Applicative (CekM uni fun s)
forall a. a -> CekM uni fun s a
forall a b.
CekM uni fun s a -> CekM uni fun s b -> CekM uni fun s a
forall a b.
CekM uni fun s a -> CekM uni fun s b -> CekM uni fun s b
forall a b.
CekM uni fun s (a -> b) -> CekM uni fun s a -> CekM uni fun s b
forall a b c.
(a -> b -> c)
-> CekM uni fun s a -> CekM uni fun s b -> CekM uni fun s c
forall (f :: * -> *).
Functor f =>
(forall a. a -> f a)
-> (forall a b. f (a -> b) -> f a -> f b)
-> (forall a b c. (a -> b -> c) -> f a -> f b -> f c)
-> (forall a b. f a -> f b -> f b)
-> (forall a b. f a -> f b -> f a)
-> Applicative f
forall (uni :: * -> *) fun s. Functor (CekM uni fun s)
forall (uni :: * -> *) fun s a. a -> CekM uni fun s a
forall (uni :: * -> *) fun s a b.
CekM uni fun s a -> CekM uni fun s b -> CekM uni fun s a
forall (uni :: * -> *) fun s a b.
CekM uni fun s a -> CekM uni fun s b -> CekM uni fun s b
forall (uni :: * -> *) fun s a b.
CekM uni fun s (a -> b) -> CekM uni fun s a -> CekM uni fun s b
forall (uni :: * -> *) fun s a b c.
(a -> b -> c)
-> CekM uni fun s a -> CekM uni fun s b -> CekM uni fun s c
$cpure :: forall (uni :: * -> *) fun s a. a -> CekM uni fun s a
pure :: forall a. a -> CekM uni fun s a
$c<*> :: forall (uni :: * -> *) fun s a b.
CekM uni fun s (a -> b) -> CekM uni fun s a -> CekM uni fun s b
<*> :: forall a b.
CekM uni fun s (a -> b) -> CekM uni fun s a -> CekM uni fun s b
$cliftA2 :: forall (uni :: * -> *) fun s a b c.
(a -> b -> c)
-> CekM uni fun s a -> CekM uni fun s b -> CekM uni fun s c
liftA2 :: forall a b c.
(a -> b -> c)
-> CekM uni fun s a -> CekM uni fun s b -> CekM uni fun s c
$c*> :: forall (uni :: * -> *) fun s a b.
CekM uni fun s a -> CekM uni fun s b -> CekM uni fun s b
*> :: forall a b.
CekM uni fun s a -> CekM uni fun s b -> CekM uni fun s b
$c<* :: forall (uni :: * -> *) fun s a b.
CekM uni fun s a -> CekM uni fun s b -> CekM uni fun s a
<* :: forall a b.
CekM uni fun s a -> CekM uni fun s b -> CekM uni fun s a
Applicative, Applicative (CekM uni fun s)
Applicative (CekM uni fun s) =>
(forall a b.
 CekM uni fun s a -> (a -> CekM uni fun s b) -> CekM uni fun s b)
-> (forall a b.
    CekM uni fun s a -> CekM uni fun s b -> CekM uni fun s b)
-> (forall a. a -> CekM uni fun s a)
-> Monad (CekM uni fun s)
forall a. a -> CekM uni fun s a
forall a b.
CekM uni fun s a -> CekM uni fun s b -> CekM uni fun s b
forall a b.
CekM uni fun s a -> (a -> CekM uni fun s b) -> CekM uni fun s b
forall (m :: * -> *).
Applicative m =>
(forall a b. m a -> (a -> m b) -> m b)
-> (forall a b. m a -> m b -> m b)
-> (forall a. a -> m a)
-> Monad m
forall (uni :: * -> *) fun s. Applicative (CekM uni fun s)
forall (uni :: * -> *) fun s a. a -> CekM uni fun s a
forall (uni :: * -> *) fun s a b.
CekM uni fun s a -> CekM uni fun s b -> CekM uni fun s b
forall (uni :: * -> *) fun s a b.
CekM uni fun s a -> (a -> CekM uni fun s b) -> CekM uni fun s b
$c>>= :: forall (uni :: * -> *) fun s a b.
CekM uni fun s a -> (a -> CekM uni fun s b) -> CekM uni fun s b
>>= :: forall a b.
CekM uni fun s a -> (a -> CekM uni fun s b) -> CekM uni fun s b
$c>> :: forall (uni :: * -> *) fun s a b.
CekM uni fun s a -> CekM uni fun s b -> CekM uni fun s b
>> :: forall a b.
CekM uni fun s a -> CekM uni fun s b -> CekM uni fun s b
$creturn :: forall (uni :: * -> *) fun s a. a -> CekM uni fun s a
return :: forall a. a -> CekM uni fun s a
Monad, Monad (CekM uni fun s)
Monad (CekM uni fun s) =>
(forall a.
 (State# (PrimState (CekM uni fun s))
  -> (# State# (PrimState (CekM uni fun s)), a #))
 -> CekM uni fun s a)
-> PrimMonad (CekM uni fun s)
forall a.
(State# (PrimState (CekM uni fun s))
 -> (# State# (PrimState (CekM uni fun s)), a #))
-> CekM uni fun s a
forall (m :: * -> *).
Monad m =>
(forall a.
 (State# (PrimState m) -> (# State# (PrimState m), a #)) -> m a)
-> PrimMonad m
forall (uni :: * -> *) fun s. Monad (CekM uni fun s)
forall (uni :: * -> *) fun s a.
(State# (PrimState (CekM uni fun s))
 -> (# State# (PrimState (CekM uni fun s)), a #))
-> CekM uni fun s a
$cprimitive :: forall (uni :: * -> *) fun s a.
(State# (PrimState (CekM uni fun s))
 -> (# State# (PrimState (CekM uni fun s)), a #))
-> CekM uni fun s a
primitive :: forall a.
(State# (PrimState (CekM uni fun s))
 -> (# State# (PrimState (CekM uni fun s)), a #))
-> CekM uni fun s a
PrimMonad)

-- | The CEK machine-specific 'EvaluationException'.
type CekEvaluationException name uni fun =
    EvaluationException (MachineError fun) CekUserError (Term name uni fun ())

instance BuiltinErrorToEvaluationError (MachineError fun) CekUserError where
  builtinErrorToEvaluationError :: BuiltinError -> EvaluationError (MachineError fun) CekUserError
builtinErrorToEvaluationError (BuiltinUnliftingEvaluationError UnliftingEvaluationError
err) =
    (UnliftingError -> MachineError fun)
-> (UnliftingError -> CekUserError)
-> EvaluationError UnliftingError UnliftingError
-> EvaluationError (MachineError fun) CekUserError
forall a b c d.
(a -> b) -> (c -> d) -> EvaluationError a c -> EvaluationError b d
forall (p :: * -> * -> *) a b c d.
Bifunctor p =>
(a -> b) -> (c -> d) -> p a c -> p b d
bimap UnliftingError -> MachineError fun
forall fun. UnliftingError -> MachineError fun
UnliftingMachineError (CekUserError -> UnliftingError -> CekUserError
forall a b. a -> b -> a
const CekUserError
CekEvaluationFailure) (EvaluationError UnliftingError UnliftingError
 -> EvaluationError (MachineError fun) CekUserError)
-> EvaluationError UnliftingError UnliftingError
-> EvaluationError (MachineError fun) CekUserError
forall a b. (a -> b) -> a -> b
$ UnliftingEvaluationError
-> EvaluationError UnliftingError UnliftingError
unUnliftingEvaluationError UnliftingEvaluationError
err
  builtinErrorToEvaluationError BuiltinError
BuiltinEvaluationFailure =
    CekUserError -> EvaluationError (MachineError fun) CekUserError
forall structural operational.
operational -> EvaluationError structural operational
OperationalError CekUserError
CekEvaluationFailure
  {-# INLINE builtinErrorToEvaluationError #-}

{- Note [Throwing exceptions in ST]
This note represents MPJ's best understanding right now, might be wrong.

We use a moderately evil trick to throw exceptions in ST, but unlike the evil trick for catching them, it's hidden.

The evil is that the 'MonadThrow' instance for 'ST' uses 'unsafeIOToST . throwIO'! Sneaky! The author has marked it
"Trustworthy", no less. However, I believe this to be safe for basically the same reasons as our trick to catch
exceptions is safe, see Note [Catching exceptions in ST]
-}

{- Note [Catching exceptions in ST]
This note represents MPJ's best understanding right now, might be wrong.

We use a moderately evil trick to catch exceptions in ST. This uses the unsafe ST <-> IO conversion functions to go into IO,
catch the exception, and then go back into ST.

Why is this okay? Recall that IO ~= ST RealWorld, i.e. it is just ST with a special thread token. The unsafe conversion functions
just coerce from one to the other. So the thread token remains the same, it's just that we'll potentially leak it from ST, and we don't
get ordering guarantees with other IO actions.

But in our case this is okay, because:

1. We do not leak the original ST thread token, since we only pass it into IO and then immediately back again.
2. We don't have ordering guarantees with other IO actions, but we don't care because we don't do any side effects, we only catch a single kind of exception.
3. We *do* have ordering guarantees between the throws inside the ST action and the catch, since they are ultimately using the same thread token.
-}

-- | Call 'dischargeCekValue' over the received 'CekVal' and feed the resulting 'Term' to
-- 'throwErrorWithCause' as the cause of the failure.
throwErrorDischarged
  :: ThrowableBuiltins uni fun
  => EvaluationError (MachineError fun) CekUserError
  -> CekValue uni fun ann
  -> CekM uni fun s x
throwErrorDischarged :: forall (uni :: * -> *) fun ann s x.
ThrowableBuiltins uni fun =>
EvaluationError (MachineError fun) CekUserError
-> CekValue uni fun ann -> CekM uni fun s x
throwErrorDischarged EvaluationError (MachineError fun) CekUserError
err = EvaluationError (MachineError fun) CekUserError
-> NTerm uni fun () -> CekM uni fun s x
forall e cause (m :: * -> *) x.
MonadError (ErrorWithCause e cause) m =>
e -> cause -> m x
throwErrorWithCause EvaluationError (MachineError fun) CekUserError
err (NTerm uni fun () -> CekM uni fun s x)
-> (CekValue uni fun ann -> NTerm uni fun ())
-> CekValue uni fun ann
-> CekM uni fun s x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DischargeResult uni fun -> NTerm uni fun ()
forall (uni :: * -> *) fun.
DischargeResult uni fun -> NTerm uni fun ()
dischargeResultToTerm (DischargeResult uni fun -> NTerm uni fun ())
-> (CekValue uni fun ann -> DischargeResult uni fun)
-> CekValue uni fun ann
-> NTerm uni fun ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CekValue uni fun ann -> DischargeResult uni fun
forall (uni :: * -> *) fun ann.
CekValue uni fun ann -> DischargeResult uni fun
dischargeCekValue

instance ThrowableBuiltins uni fun =>
        MonadError (CekEvaluationException NamedDeBruijn uni fun) (CekM uni fun s) where
    -- See Note [Throwing exceptions in ST].
    throwError :: forall a.
CekEvaluationException NamedDeBruijn uni fun -> CekM uni fun s a
throwError = ST s a -> CekM uni fun s a
forall (uni :: * -> *) fun s a. ST s a -> CekM uni fun s a
CekM (ST s a -> CekM uni fun s a)
-> (CekEvaluationException NamedDeBruijn uni fun -> ST s a)
-> CekEvaluationException NamedDeBruijn uni fun
-> CekM uni fun s a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CekEvaluationException NamedDeBruijn uni fun -> ST s a
forall e a. (HasCallStack, Exception e) => e -> ST s a
forall (m :: * -> *) e a.
(MonadThrow m, HasCallStack, Exception e) =>
e -> m a
throwM

    -- See Note [Catching exceptions in ST].
    catchError
        :: forall a.
           CekM uni fun s a
        -> (CekEvaluationException NamedDeBruijn uni fun -> CekM uni fun s a)
        -> CekM uni fun s a
    CekM uni fun s a
a catchError :: forall a.
CekM uni fun s a
-> (CekEvaluationException NamedDeBruijn uni fun
    -> CekM uni fun s a)
-> CekM uni fun s a
`catchError` CekEvaluationException NamedDeBruijn uni fun -> CekM uni fun s a
h =
        -- Here in addition to catching 'CekEvaluationException' we also catch common GHC exceptions
        -- in case one of them somehow gets triggered during script execution (which would be a bug
        -- on our side). We could probably use @enclosed-exceptions@, but spawning a thread per
        -- script is expensive. We could also use type-based disambiguation like @unliftio@ does,
        -- but it fails if an exception whose type indicates that it's a sync one gets thrown in an
        -- async way.
        -- Alexey Kuleshevich told us that the node catches exceptions anyway, so what we're doing
        -- here is for easing debugging and error reporting, it's not a proper safety measure. Hence
        -- catching several common exception types is enough.
        ST s a -> CekM uni fun s a
forall (uni :: * -> *) fun s a. ST s a -> CekM uni fun s a
CekM (ST s a -> CekM uni fun s a)
-> (IO a -> ST s a) -> IO a -> CekM uni fun s a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. IO a -> ST s a
forall a s. IO a -> ST s a
unsafeIOToST (IO a -> CekM uni fun s a) -> IO a -> CekM uni fun s a
forall a b. (a -> b) -> a -> b
$ IO a
aIO IO a -> [Handler IO a] -> IO a
forall (f :: * -> *) (m :: * -> *) a.
(HasCallStack, Foldable f, MonadCatch m) =>
m a -> f (Handler m a) -> m a
`catches`
            [ (CekEvaluationException NamedDeBruijn uni fun -> IO a)
-> Handler IO a
forall (m :: * -> *) a e. Exception e => (e -> m a) -> Handler m a
Handler CekEvaluationException NamedDeBruijn uni fun -> IO a
hIO
            , forall e. Exception e => Handler IO a
panicHandler @IOError
            , forall e. Exception e => Handler IO a
panicHandler @Exception.ErrorCall
            , forall e. Exception e => Handler IO a
panicHandler @Exception.ArithException
            , forall e. Exception e => Handler IO a
panicHandler @Exception.ArrayException
            ]
      where
        aIO :: IO a
aIO = CekM uni fun s a -> IO a
unsafeRunCekM CekM uni fun s a
a
        hIO :: CekEvaluationException NamedDeBruijn uni fun -> IO a
hIO = CekM uni fun s a -> IO a
unsafeRunCekM (CekM uni fun s a -> IO a)
-> (CekEvaluationException NamedDeBruijn uni fun
    -> CekM uni fun s a)
-> CekEvaluationException NamedDeBruijn uni fun
-> IO a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CekEvaluationException NamedDeBruijn uni fun -> CekM uni fun s a
h

        -- Unsafely run a 'CekM' computation in the 'IO' monad by converting the underlying 'ST' to
        -- it.
        unsafeRunCekM :: CekM uni fun s a -> IO a
        unsafeRunCekM :: CekM uni fun s a -> IO a
unsafeRunCekM = ST s a -> IO a
forall s a. ST s a -> IO a
unsafeSTToIO (ST s a -> IO a)
-> (CekM uni fun s a -> ST s a) -> CekM uni fun s a -> IO a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CekM uni fun s a -> ST s a
forall (uni :: * -> *) fun s a. CekM uni fun s a -> ST s a
unCekM

        panicHandler :: forall e. Exception e => Handler IO a
        panicHandler :: forall e. Exception e => Handler IO a
panicHandler =
            (e -> IO a) -> Handler IO a
forall (m :: * -> *) a e. Exception e => (e -> m a) -> Handler m a
Handler ((e -> IO a) -> Handler IO a) -> (e -> IO a) -> Handler IO a
forall a b. (a -> b) -> a -> b
$ \(e
err :: e) -> CekEvaluationException NamedDeBruijn uni fun -> IO a
hIO (CekEvaluationException NamedDeBruijn uni fun -> IO a)
-> CekEvaluationException NamedDeBruijn uni fun -> IO a
forall a b. (a -> b) -> a -> b
$
                EvaluationError (MachineError fun) CekUserError
-> Maybe (Term NamedDeBruijn uni fun ())
-> CekEvaluationException NamedDeBruijn uni fun
forall err cause. err -> Maybe cause -> ErrorWithCause err cause
ErrorWithCause
                    (MachineError fun -> EvaluationError (MachineError fun) CekUserError
forall structural operational.
structural -> EvaluationError structural operational
StructuralError (MachineError fun
 -> EvaluationError (MachineError fun) CekUserError)
-> (String -> MachineError fun)
-> String
-> EvaluationError (MachineError fun) CekUserError
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> MachineError fun
forall fun. String -> MachineError fun
PanicMachineError (String -> EvaluationError (MachineError fun) CekUserError)
-> String -> EvaluationError (MachineError fun) CekUserError
forall a b. (a -> b) -> a -> b
$ e -> String
forall e. Exception e => e -> String
displayException e
err)
                    Maybe (Term NamedDeBruijn uni fun ())
forall a. Maybe a
Nothing

instance Pretty CekUserError where
    pretty :: forall ann. CekUserError -> Doc ann
pretty (CekCaseBuiltinError Text
err) = [Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
vcat
        [ Doc ann
"'case' over a value of a built-in type failed with"
        , Text -> Doc ann
forall ann. Text -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty Text
err
        ]
    pretty (CekOutOfExError (ExRestrictingBudget ExBudget
res)) =
        [Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
cat
          [ Doc ann
"The machine terminated part way through evaluation due to overspending the budget."
          , Doc ann
"The budget when the machine terminated was:"
          , ExBudget -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. ExBudget -> Doc ann
pretty ExBudget
res
          , Doc ann
"Negative numbers indicate the overspent budget; note that this only indicates the budget that was needed for the next step, not to run the program to completion."
          ]
    pretty CekUserError
CekEvaluationFailure = Doc ann
"The machine terminated because of an error, either from a built-in function or from an explicit use of 'error'."

argNonEmptyStackToList :: ArgStackNonEmpty uni fun ann -> [CekValue uni fun ann]
argNonEmptyStackToList :: forall (uni :: * -> *) fun ann.
ArgStackNonEmpty uni fun ann -> [CekValue uni fun ann]
argNonEmptyStackToList (LastStackNonEmpty CekValue uni fun ann
val)       = [CekValue uni fun ann
val]
argNonEmptyStackToList (ConsStackNonEmpty CekValue uni fun ann
val ArgStackNonEmpty uni fun ann
stack) = CekValue uni fun ann
val CekValue uni fun ann
-> [CekValue uni fun ann] -> [CekValue uni fun ann]
forall a. a -> [a] -> [a]
: ArgStackNonEmpty uni fun ann -> [CekValue uni fun ann]
forall (uni :: * -> *) fun ann.
ArgStackNonEmpty uni fun ann -> [CekValue uni fun ann]
argNonEmptyStackToList ArgStackNonEmpty uni fun ann
stack

-- | Convert the given 'EmptyOrMultiStack to a list.
argStackToList :: EmptyOrMultiStack uni fun ann -> [CekValue uni fun ann]
argStackToList :: forall (uni :: * -> *) fun ann.
EmptyOrMultiStack uni fun ann -> [CekValue uni fun ann]
argStackToList EmptyOrMultiStack uni fun ann
EmptyStack         = []
argStackToList (MultiStack ArgStackNonEmpty uni fun ann
stack) = ArgStackNonEmpty uni fun ann -> [CekValue uni fun ann]
forall (uni :: * -> *) fun ann.
ArgStackNonEmpty uni fun ann -> [CekValue uni fun ann]
argNonEmptyStackToList ArgStackNonEmpty uni fun ann
stack

-- | The result of 'dischargeCekValue'.
data DischargeResult uni fun
    = DischargeConstant (Some (ValueOf uni))
    | DischargeNonConstant (NTerm uni fun ())

deriving stock instance (GShow uni, Everywhere uni Show, Show fun, Closed uni)
    => Show (DischargeResult uni fun)

deriving stock instance (GEq uni, Everywhere uni Eq, Eq fun, Closed uni)
    => Eq (DischargeResult uni fun)

instance (PrettyUni uni, Pretty fun) => PrettyBy PrettyConfigPlc (DischargeResult uni fun) where
    prettyBy :: forall ann. PrettyConfigPlc -> DischargeResult uni fun -> Doc ann
prettyBy PrettyConfigPlc
cfg = PrettyConfigPlc -> NTerm uni fun () -> Doc ann
forall ann. PrettyConfigPlc -> NTerm uni fun () -> Doc ann
forall config a ann. PrettyBy config a => config -> a -> Doc ann
prettyBy PrettyConfigPlc
cfg (NTerm uni fun () -> Doc ann)
-> (DischargeResult uni fun -> NTerm uni fun ())
-> DischargeResult uni fun
-> Doc ann
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DischargeResult uni fun -> NTerm uni fun ()
forall (uni :: * -> *) fun.
DischargeResult uni fun -> NTerm uni fun ()
dischargeResultToTerm

dischargeResultToTerm :: DischargeResult uni fun -> NTerm uni fun ()
dischargeResultToTerm :: forall (uni :: * -> *) fun.
DischargeResult uni fun -> NTerm uni fun ()
dischargeResultToTerm (DischargeConstant Some (ValueOf uni)
val)     = () -> Some (ValueOf uni) -> Term NamedDeBruijn uni fun ()
forall name (uni :: * -> *) fun ann.
ann -> Some (ValueOf uni) -> Term name uni fun ann
Constant () Some (ValueOf uni)
val
dischargeResultToTerm (DischargeNonConstant Term NamedDeBruijn uni fun ()
term) = Term NamedDeBruijn uni fun ()
term

-- | Convert a 'CekValue' into a 'Term' by replacing all bound variables with the terms
-- they're bound to (which themselves have to be obtained by recursively discharging values).
dischargeCekValue :: forall uni fun ann. CekValue uni fun ann -> DischargeResult uni fun
dischargeCekValue :: forall (uni :: * -> *) fun ann.
CekValue uni fun ann -> DischargeResult uni fun
dischargeCekValue (VCon Some (ValueOf uni)
val) = Some (ValueOf uni) -> DischargeResult uni fun
forall (uni :: * -> *) fun.
Some (ValueOf uni) -> DischargeResult uni fun
DischargeConstant Some (ValueOf uni)
val
dischargeCekValue CekValue uni fun ann
value0     = NTerm uni fun () -> DischargeResult uni fun
forall (uni :: * -> *) fun.
NTerm uni fun () -> DischargeResult uni fun
DischargeNonConstant (NTerm uni fun () -> DischargeResult uni fun)
-> NTerm uni fun () -> DischargeResult uni fun
forall a b. (a -> b) -> a -> b
$ CekValue uni fun ann -> NTerm uni fun ()
goValue CekValue uni fun ann
value0 where
    goValue :: CekValue uni fun ann -> NTerm uni fun ()
    goValue :: CekValue uni fun ann -> NTerm uni fun ()
goValue = \case
        VCon Some (ValueOf uni)
val -> () -> Some (ValueOf uni) -> NTerm uni fun ()
forall name (uni :: * -> *) fun ann.
ann -> Some (ValueOf uni) -> Term name uni fun ann
Constant () Some (ValueOf uni)
val
        VDelay NTerm uni fun ann
body CekValEnv uni fun ann
env -> () -> NTerm uni fun () -> NTerm uni fun ()
forall name (uni :: * -> *) fun ann.
ann -> Term name uni fun ann -> Term name uni fun ann
Delay () (NTerm uni fun () -> NTerm uni fun ())
-> NTerm uni fun () -> NTerm uni fun ()
forall a b. (a -> b) -> a -> b
$ CekValEnv uni fun ann
-> Word64 -> NTerm uni fun ann -> NTerm uni fun ()
goValEnv CekValEnv uni fun ann
env Word64
0 NTerm uni fun ann
body
        VLamAbs (NamedDeBruijn Text
n Index
_ix) NTerm uni fun ann
body CekValEnv uni fun ann
env ->
            -- The index on the binder is meaningless, we put @0@ by convention, see 'Binder'.
            () -> NamedDeBruijn -> NTerm uni fun () -> NTerm uni fun ()
forall name (uni :: * -> *) fun ann.
ann -> name -> Term name uni fun ann -> Term name uni fun ann
LamAbs () (Text -> Index -> NamedDeBruijn
NamedDeBruijn Text
n Index
deBruijnInitIndex) (NTerm uni fun () -> NTerm uni fun ())
-> NTerm uni fun () -> NTerm uni fun ()
forall a b. (a -> b) -> a -> b
$ CekValEnv uni fun ann
-> Word64 -> NTerm uni fun ann -> NTerm uni fun ()
goValEnv CekValEnv uni fun ann
env Word64
1 NTerm uni fun ann
body
        -- We only return a discharged builtin application when (a) it's being returned by the
        -- machine, or (b) it's needed for an error message.
        -- @term@ is fully discharged, so we can return it directly without any further discharging.
        VBuiltin fun
_ NTerm uni fun ()
term BuiltinRuntime (CekValue uni fun ann)
_ -> NTerm uni fun ()
term
        VConstr Word64
ind EmptyOrMultiStack uni fun ann
args -> () -> Word64 -> [NTerm uni fun ()] -> NTerm uni fun ()
forall name (uni :: * -> *) fun ann.
ann -> Word64 -> [Term name uni fun ann] -> Term name uni fun ann
Constr () Word64
ind ([NTerm uni fun ()] -> NTerm uni fun ())
-> ([CekValue uni fun ann] -> [NTerm uni fun ()])
-> [CekValue uni fun ann]
-> NTerm uni fun ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (CekValue uni fun ann -> NTerm uni fun ())
-> [CekValue uni fun ann] -> [NTerm uni fun ()]
forall a b. (a -> b) -> [a] -> [b]
map CekValue uni fun ann -> NTerm uni fun ()
goValue ([CekValue uni fun ann] -> NTerm uni fun ())
-> [CekValue uni fun ann] -> NTerm uni fun ()
forall a b. (a -> b) -> a -> b
$ EmptyOrMultiStack uni fun ann -> [CekValue uni fun ann]
forall (uni :: * -> *) fun ann.
EmptyOrMultiStack uni fun ann -> [CekValue uni fun ann]
argStackToList EmptyOrMultiStack uni fun ann
args

    -- Instantiate all the free variables of a term by looking them up in an environment.
    -- Mutually recursive with @goValue@.
    goValEnv :: CekValEnv uni fun ann -> Word64 -> NTerm uni fun ann -> NTerm uni fun ()
    goValEnv :: CekValEnv uni fun ann
-> Word64 -> NTerm uni fun ann -> NTerm uni fun ()
goValEnv CekValEnv uni fun ann
env = Word64 -> NTerm uni fun ann -> NTerm uni fun ()
go where
        -- @shift@ is just a counter that measures how many lambda-abstractions we have descended
        -- into so far.
        go :: Word64 -> NTerm uni fun ann -> NTerm uni fun ()
        go :: Word64 -> NTerm uni fun ann -> NTerm uni fun ()
go !Word64
shift =  \case
          LamAbs ann
_ NamedDeBruijn
name NTerm uni fun ann
body -> () -> NamedDeBruijn -> NTerm uni fun () -> NTerm uni fun ()
forall name (uni :: * -> *) fun ann.
ann -> name -> Term name uni fun ann -> Term name uni fun ann
LamAbs () NamedDeBruijn
name (NTerm uni fun () -> NTerm uni fun ())
-> NTerm uni fun () -> NTerm uni fun ()
forall a b. (a -> b) -> a -> b
$ Word64 -> NTerm uni fun ann -> NTerm uni fun ()
go (Word64
shift Word64 -> Word64 -> Word64
forall a. Num a => a -> a -> a
+ Word64
1) NTerm uni fun ann
body
          Var ann
_ named :: NamedDeBruijn
named@(NamedDeBruijn Text
_ (Index -> Word64
forall a b. Coercible a b => a -> b
coerce -> Word64
idx)) ->
              if Word64
shift Word64 -> Word64 -> Bool
forall a. Ord a => a -> a -> Bool
>= Word64
idx
              -- the index n is less-than-or-equal than the number of lambdas we have descended
              -- this means that n points to a bound variable, so we don't discharge it.
              then () -> NamedDeBruijn -> NTerm uni fun ()
forall name (uni :: * -> *) fun ann.
ann -> name -> Term name uni fun ann
Var () NamedDeBruijn
named
              else NTerm uni fun ()
-> (CekValue uni fun ann -> NTerm uni fun ())
-> Maybe (CekValue uni fun ann)
-> NTerm uni fun ()
forall b a. b -> (a -> b) -> Maybe a -> b
maybe
                     -- var is free, leave it alone
                     (() -> NamedDeBruijn -> NTerm uni fun ()
forall name (uni :: * -> *) fun ann.
ann -> name -> Term name uni fun ann
Var () NamedDeBruijn
named)
                     -- var is in the env, discharge its value
                     CekValue uni fun ann -> NTerm uni fun ()
goValue
                     -- index relative to (as seen from the point of view of) the environment
                     (CekValEnv uni fun ann
-> Word64 -> Maybe (Element (CekValEnv uni fun ann))
forall e. RandomAccessList e => e -> Word64 -> Maybe (Element e)
Env.indexOne CekValEnv uni fun ann
env (Word64 -> Maybe (Element (CekValEnv uni fun ann)))
-> Word64 -> Maybe (Element (CekValEnv uni fun ann))
forall a b. (a -> b) -> a -> b
$ Word64
idx Word64 -> Word64 -> Word64
forall a. Num a => a -> a -> a
- Word64
shift)
          Apply ann
_ NTerm uni fun ann
fun NTerm uni fun ann
arg    -> () -> NTerm uni fun () -> NTerm uni fun () -> NTerm uni fun ()
forall name (uni :: * -> *) fun ann.
ann
-> Term name uni fun ann
-> Term name uni fun ann
-> Term name uni fun ann
Apply () (Word64 -> NTerm uni fun ann -> NTerm uni fun ()
go Word64
shift NTerm uni fun ann
fun) (NTerm uni fun () -> NTerm uni fun ())
-> NTerm uni fun () -> NTerm uni fun ()
forall a b. (a -> b) -> a -> b
$ Word64 -> NTerm uni fun ann -> NTerm uni fun ()
go Word64
shift NTerm uni fun ann
arg
          Delay ann
_ NTerm uni fun ann
term       -> () -> NTerm uni fun () -> NTerm uni fun ()
forall name (uni :: * -> *) fun ann.
ann -> Term name uni fun ann -> Term name uni fun ann
Delay () (NTerm uni fun () -> NTerm uni fun ())
-> NTerm uni fun () -> NTerm uni fun ()
forall a b. (a -> b) -> a -> b
$ Word64 -> NTerm uni fun ann -> NTerm uni fun ()
go Word64
shift NTerm uni fun ann
term
          Force ann
_ NTerm uni fun ann
term       -> () -> NTerm uni fun () -> NTerm uni fun ()
forall name (uni :: * -> *) fun ann.
ann -> Term name uni fun ann -> Term name uni fun ann
Force () (NTerm uni fun () -> NTerm uni fun ())
-> NTerm uni fun () -> NTerm uni fun ()
forall a b. (a -> b) -> a -> b
$ Word64 -> NTerm uni fun ann -> NTerm uni fun ()
go Word64
shift NTerm uni fun ann
term
          Constant ann
_ Some (ValueOf uni)
val     -> () -> Some (ValueOf uni) -> NTerm uni fun ()
forall name (uni :: * -> *) fun ann.
ann -> Some (ValueOf uni) -> Term name uni fun ann
Constant () Some (ValueOf uni)
val
          Builtin ann
_ fun
fun      -> () -> fun -> NTerm uni fun ()
forall name (uni :: * -> *) fun ann.
ann -> fun -> Term name uni fun ann
Builtin () fun
fun
          Error ann
_            -> () -> NTerm uni fun ()
forall name (uni :: * -> *) fun ann. ann -> Term name uni fun ann
Error ()
          Constr ann
_ Word64
ind [NTerm uni fun ann]
args  -> () -> Word64 -> [NTerm uni fun ()] -> NTerm uni fun ()
forall name (uni :: * -> *) fun ann.
ann -> Word64 -> [Term name uni fun ann] -> Term name uni fun ann
Constr () Word64
ind ([NTerm uni fun ()] -> NTerm uni fun ())
-> [NTerm uni fun ()] -> NTerm uni fun ()
forall a b. (a -> b) -> a -> b
$ (NTerm uni fun ann -> NTerm uni fun ())
-> [NTerm uni fun ann] -> [NTerm uni fun ()]
forall a b. (a -> b) -> [a] -> [b]
map (Word64 -> NTerm uni fun ann -> NTerm uni fun ()
go Word64
shift) [NTerm uni fun ann]
args
          Case ann
_ NTerm uni fun ann
scrut Vector (NTerm uni fun ann)
alts  -> ()
-> NTerm uni fun ()
-> Vector (NTerm uni fun ())
-> NTerm uni fun ()
forall name (uni :: * -> *) fun ann.
ann
-> Term name uni fun ann
-> Vector (Term name uni fun ann)
-> Term name uni fun ann
Case () (Word64 -> NTerm uni fun ann -> NTerm uni fun ()
go Word64
shift NTerm uni fun ann
scrut) (Vector (NTerm uni fun ()) -> NTerm uni fun ())
-> Vector (NTerm uni fun ()) -> NTerm uni fun ()
forall a b. (a -> b) -> a -> b
$ (NTerm uni fun ann -> NTerm uni fun ())
-> Vector (NTerm uni fun ann) -> Vector (NTerm uni fun ())
forall a b. (a -> b) -> Vector a -> Vector b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Word64 -> NTerm uni fun ann -> NTerm uni fun ()
go Word64
shift) Vector (NTerm uni fun ann)
alts

instance (PrettyUni uni, Pretty fun) => PrettyBy PrettyConfigPlc (CekValue uni fun ann) where
    prettyBy :: forall ann. PrettyConfigPlc -> CekValue uni fun ann -> Doc ann
prettyBy PrettyConfigPlc
cfg = PrettyConfigPlc -> NTerm uni fun () -> Doc ann
forall ann. PrettyConfigPlc -> NTerm uni fun () -> Doc ann
forall config a ann. PrettyBy config a => config -> a -> Doc ann
prettyBy PrettyConfigPlc
cfg (NTerm uni fun () -> Doc ann)
-> (CekValue uni fun ann -> NTerm uni fun ())
-> CekValue uni fun ann
-> Doc ann
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DischargeResult uni fun -> NTerm uni fun ()
forall (uni :: * -> *) fun.
DischargeResult uni fun -> NTerm uni fun ()
dischargeResultToTerm (DischargeResult uni fun -> NTerm uni fun ())
-> (CekValue uni fun ann -> DischargeResult uni fun)
-> CekValue uni fun ann
-> NTerm uni fun ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CekValue uni fun ann -> DischargeResult uni fun
forall (uni :: * -> *) fun ann.
CekValue uni fun ann -> DischargeResult uni fun
dischargeCekValue

type instance UniOf (CekValue uni fun ann) = uni

instance HasConstant (CekValue uni fun ann) where
    asConstant :: CekValue uni fun ann
-> Either
     BuiltinError (Some (ValueOf (UniOf (CekValue uni fun ann))))
asConstant (VCon Some (ValueOf uni)
val) = Some (ValueOf uni) -> Either BuiltinError (Some (ValueOf uni))
forall a. a -> Either BuiltinError a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Some (ValueOf uni)
val
    asConstant CekValue uni fun ann
_          = BuiltinError -> Either BuiltinError (Some (ValueOf uni))
forall a. BuiltinError -> Either BuiltinError a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError BuiltinError
notAConstant
    {-# INLINE asConstant #-}

    fromConstant :: Some (ValueOf (UniOf (CekValue uni fun ann)))
-> CekValue uni fun ann
fromConstant = Some (ValueOf uni) -> CekValue uni fun ann
Some (ValueOf (UniOf (CekValue uni fun ann)))
-> CekValue uni fun ann
forall (uni :: * -> *) fun ann.
Some (ValueOf uni) -> CekValue uni fun ann
VCon
    {-# INLINE fromConstant #-}

{-|
The context in which the machine operates.

Morally, this is a stack of frames, but we use the "intrusive list" representation so that
we can match on context and the top frame in a single, strict pattern match.
-}
data Context uni fun ann
    = FrameAwaitArg !(CekValue uni fun ann) !(Context uni fun ann)
    -- ^ @[V _]@
    | FrameAwaitFunTerm !(CekValEnv uni fun ann) !(NTerm uni fun ann) !(Context uni fun ann)
    -- ^ @[_ N]@
    | FrameAwaitFunConN !(Spine (Some (ValueOf uni))) !(Context uni fun ann)
    -- ^ @[_ V]@
    | FrameAwaitFunValueN !(ArgStackNonEmpty uni fun ann) !(Context uni fun ann)
    -- ^ @[_ V1 .. Vn]@
    | FrameForce !(Context uni fun ann)
    -- ^ @(force _)@
    -- See Note [Accumulators for terms]
    | FrameConstr !(CekValEnv uni fun ann) {-# UNPACK #-} !Word64 ![NTerm uni fun ann] !(ArgStack uni fun ann) !(Context uni fun ann)
    -- ^ @(constr i V0 ... Vj-1 _ Nj ... Nn)@
    | FrameCases !(CekValEnv uni fun ann) !(V.Vector (NTerm uni fun ann)) !(Context uni fun ann)
    -- ^ @(case _ C0 .. Cn)@
    | NoFrame

deriving stock instance (GShow uni, Everywhere uni Show, Show fun, Show ann, Closed uni)
    => Show (Context uni fun ann)

-- See Note [ExMemoryUsage instances for non-constants].
instance (Closed uni, uni `Everywhere` ExMemoryUsage) => ExMemoryUsage (CekValue uni fun ann) where
    memoryUsage :: CekValue uni fun ann -> CostRose
memoryUsage = \case
        VCon Some (ValueOf uni)
c      -> Some (ValueOf uni) -> CostRose
forall a. ExMemoryUsage a => a -> CostRose
memoryUsage Some (ValueOf uni)
c
        VDelay {}   -> CostingInteger -> CostRose
singletonRose CostingInteger
1
        VLamAbs {}  -> CostingInteger -> CostRose
singletonRose CostingInteger
1
        VBuiltin {} -> CostingInteger -> CostRose
singletonRose CostingInteger
1
        VConstr {}  -> CostingInteger -> CostRose
singletonRose CostingInteger
1
    {-# INLINE memoryUsage #-}

{- Note [ArgStack vs Spine]
We use 'ArgStack' for collecting the arguments of a constructor to later pass it to the function in
the appropriate branch. Originally, all arguments of a constructor are terms and hence before we can
pass them to a function they need to be evaluated to values, which means that in case of the CEK
machine the evaluated arguments are going to be reversed: you evaluate the first argument and put
the result into a 'FrameConstr', then the second one and put it in a 'FrameConstr' again, this time
prepending it to the one that is already there etc -- in the end you get the arguments in reversed
order.

But in case of 'Spine' the builtins machinery directly produces values, not terms. Meaning, a
'Spine' that we get from the builtins machinery isn't reversed, hence we can pass its contents
directly to the head of the application. Which is why 'transferSpine' is a right fold.
-}

runCekM
    :: forall cost uni fun ann
    . ThrowableBuiltins uni fun
    => MachineParameters CekMachineCosts fun (CekValue uni fun ann)
    -> ExBudgetMode cost uni fun
    -> EmitterMode uni fun
    -> (forall s. GivenCekReqs uni fun ann s => CekM uni fun s (DischargeResult uni fun))
    -> CekReport cost NamedDeBruijn uni fun
runCekM :: forall cost (uni :: * -> *) fun ann.
ThrowableBuiltins uni fun =>
MachineParameters CekMachineCosts fun (CekValue uni fun ann)
-> ExBudgetMode cost uni fun
-> EmitterMode uni fun
-> (forall s.
    GivenCekReqs uni fun ann s =>
    CekM uni fun s (DischargeResult uni fun))
-> CekReport cost NamedDeBruijn uni fun
runCekM
        (MachineParameters CaserBuiltin (UniOf (CekValue uni fun ann))
caser (MachineVariantParameters CekMachineCosts
costs BuiltinsRuntime fun (CekValue uni fun ann)
runtime))
        (ExBudgetMode forall s. ST s (ExBudgetInfo cost uni fun s)
getExBudgetInfo)
        (EmitterMode forall s. ST s ExBudget -> ST s (CekEmitterInfo uni fun s)
getEmitterMode)
        forall s.
GivenCekReqs uni fun ann s =>
CekM uni fun s (DischargeResult uni fun)
a = (forall s. ST s (CekReport cost NamedDeBruijn uni fun))
-> CekReport cost NamedDeBruijn uni fun
forall a. (forall s. ST s a) -> a
runST ((forall s. ST s (CekReport cost NamedDeBruijn uni fun))
 -> CekReport cost NamedDeBruijn uni fun)
-> (forall s. ST s (CekReport cost NamedDeBruijn uni fun))
-> CekReport cost NamedDeBruijn uni fun
forall a b. (a -> b) -> a -> b
$ do
    ExBudgetInfo{CekBudgetSpender uni fun s
_exBudgetModeSpender :: forall cost (uni :: * -> *) fun s.
ExBudgetInfo cost uni fun s -> CekBudgetSpender uni fun s
_exBudgetModeSpender :: CekBudgetSpender uni fun s
_exBudgetModeSpender, ST s cost
_exBudgetModeGetFinal :: forall cost (uni :: * -> *) fun s.
ExBudgetInfo cost uni fun s -> ST s cost
_exBudgetModeGetFinal :: ST s cost
_exBudgetModeGetFinal, ST s ExBudget
_exBudgetModeGetCumulative :: forall cost (uni :: * -> *) fun s.
ExBudgetInfo cost uni fun s -> ST s ExBudget
_exBudgetModeGetCumulative :: ST s ExBudget
_exBudgetModeGetCumulative} <- ST s (ExBudgetInfo cost uni fun s)
forall s. ST s (ExBudgetInfo cost uni fun s)
getExBudgetInfo
    CekEmitterInfo{CekEmitter uni fun s
_cekEmitterInfoEmit :: forall (uni :: * -> *) fun s.
CekEmitterInfo uni fun s -> CekEmitter uni fun s
_cekEmitterInfoEmit :: CekEmitter uni fun s
_cekEmitterInfoEmit, ST s [Text]
_cekEmitterInfoGetFinal :: forall (uni :: * -> *) fun s.
CekEmitterInfo uni fun s -> ST s [Text]
_cekEmitterInfoGetFinal :: ST s [Text]
_cekEmitterInfoGetFinal} <- ST s ExBudget -> ST s (CekEmitterInfo uni fun s)
forall s. ST s ExBudget -> ST s (CekEmitterInfo uni fun s)
getEmitterMode ST s ExBudget
_exBudgetModeGetCumulative
    StepCounter 10 s
ctr <- Proxy 10 -> ST s (StepCounter 10 (PrimState (ST s)))
forall (n :: Nat) (m :: * -> *).
(KnownNat n, PrimMonad m) =>
Proxy n -> m (StepCounter n (PrimState m))
newCounter (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @CounterSize)
    let ?cekRuntime = ?cekRuntime::BuiltinsRuntime fun (CekValue uni fun ann)
BuiltinsRuntime fun (CekValue uni fun ann)
runtime
        ?cekCaserBuiltin = ?cekCaserBuiltin::CaserBuiltin uni
CaserBuiltin uni
CaserBuiltin (UniOf (CekValue uni fun ann))
caser
        ?cekEmitter = ?cekEmitter::CekEmitter uni fun s
CekEmitter uni fun s
_cekEmitterInfoEmit
        ?cekBudgetSpender = ?cekBudgetSpender::CekBudgetSpender uni fun s
CekBudgetSpender uni fun s
_exBudgetModeSpender
        ?cekCosts = ?cekCosts::CekMachineCosts
CekMachineCosts
costs
        ?cekSlippage = ?cekSlippage::Slippage
Slippage
defaultSlippage
        ?cekStepCounter = ?cekStepCounter::StepCounter 10 s
StepCounter 10 s
ctr
    CekResult NamedDeBruijn uni fun
res <- CekM
  uni
  fun
  s
  (Either
     (CekEvaluationException NamedDeBruijn uni fun)
     (DischargeResult uni fun))
-> ST
     s
     (Either
        (CekEvaluationException NamedDeBruijn uni fun)
        (DischargeResult uni fun))
forall (uni :: * -> *) fun s a. CekM uni fun s a -> ST s a
unCekM (CekM uni fun s (DischargeResult uni fun)
-> CekM
     uni
     fun
     s
     (Either
        (CekEvaluationException NamedDeBruijn uni fun)
        (DischargeResult uni fun))
forall e (m :: * -> *) a. MonadError e m => m a -> m (Either e a)
tryError CekM uni fun s (DischargeResult uni fun)
forall s.
GivenCekReqs uni fun ann s =>
CekM uni fun s (DischargeResult uni fun)
a) ST
  s
  (Either
     (CekEvaluationException NamedDeBruijn uni fun)
     (DischargeResult uni fun))
-> (Either
      (CekEvaluationException NamedDeBruijn uni fun)
      (DischargeResult uni fun)
    -> CekResult NamedDeBruijn uni fun)
-> ST s (CekResult NamedDeBruijn uni fun)
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \case
        Left CekEvaluationException NamedDeBruijn uni fun
err                          -> CekEvaluationException NamedDeBruijn uni fun
-> CekResult NamedDeBruijn uni fun
forall name (uni :: * -> *) fun.
CekEvaluationException name uni fun -> CekResult name uni fun
CekFailure CekEvaluationException NamedDeBruijn uni fun
err
        Right (DischargeConstant Some (ValueOf uni)
val)     -> Some (ValueOf uni) -> CekResult NamedDeBruijn uni fun
forall name (uni :: * -> *) fun.
Some (ValueOf uni) -> CekResult name uni fun
CekSuccessConstant Some (ValueOf uni)
val
        Right (DischargeNonConstant NTerm uni fun ()
term) -> NTerm uni fun () -> CekResult NamedDeBruijn uni fun
forall name (uni :: * -> *) fun.
Term name uni fun () -> CekResult name uni fun
CekSuccessNonConstant NTerm uni fun ()
term
    cost
st <- ST s cost
_exBudgetModeGetFinal
    [Text]
logs <- ST s [Text]
_cekEmitterInfoGetFinal
    CekReport cost NamedDeBruijn uni fun
-> ST s (CekReport cost NamedDeBruijn uni fun)
forall a. a -> ST s a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (CekReport cost NamedDeBruijn uni fun
 -> ST s (CekReport cost NamedDeBruijn uni fun))
-> CekReport cost NamedDeBruijn uni fun
-> ST s (CekReport cost NamedDeBruijn uni fun)
forall a b. (a -> b) -> a -> b
$ CekResult NamedDeBruijn uni fun
-> cost -> [Text] -> CekReport cost NamedDeBruijn uni fun
forall cost name (uni :: * -> *) fun.
CekResult name uni fun
-> cost -> [Text] -> CekReport cost name uni fun
CekReport CekResult NamedDeBruijn uni fun
res cost
st [Text]
logs
{-# INLINE runCekM #-}

-- See Note [Compilation peculiarities].
-- | The entering point to the CEK machine's engine.
enterComputeCek
    :: forall uni fun ann s
    . (ThrowableBuiltins uni fun, GivenCekReqs uni fun ann s)
    => Context uni fun ann
    -> CekValEnv uni fun ann
    -> NTerm uni fun ann
    -> CekM uni fun s (DischargeResult uni fun)
enterComputeCek :: forall (uni :: * -> *) fun ann s.
(ThrowableBuiltins uni fun, GivenCekReqs uni fun ann s) =>
Context uni fun ann
-> CekValEnv uni fun ann
-> NTerm uni fun ann
-> CekM uni fun s (DischargeResult uni fun)
enterComputeCek = Context uni fun ann
-> CekValEnv uni fun ann
-> NTerm uni fun ann
-> CekM uni fun s (DischargeResult uni fun)
computeCek
  where
    -- | The computing part of the CEK machine.
    -- Either
    -- 1. adds a frame to the context and calls 'computeCek' ('Force', 'Apply')
    -- 2. calls 'returnCek' on values ('Delay', 'LamAbs', 'Constant', 'Builtin')
    -- 3. throws 'EvaluationFailure' ('Error')
    -- 4. looks up a variable in the environment and calls 'returnCek' ('Var')
    computeCek
        :: Context uni fun ann
        -> CekValEnv uni fun ann
        -> NTerm uni fun ann
        -> CekM uni fun s (DischargeResult uni fun)
    -- s ; ρ ▻ {L A}  ↦ s , {_ A} ; ρ ▻ L
    computeCek :: Context uni fun ann
-> CekValEnv uni fun ann
-> NTerm uni fun ann
-> CekM uni fun s (DischargeResult uni fun)
computeCek !Context uni fun ann
ctx !CekValEnv uni fun ann
env (Var ann
_ NamedDeBruijn
varName) = do
        StepKind -> CekM uni fun s ()
stepAndMaybeSpend StepKind
BVar
        CekValue uni fun ann
val <- NamedDeBruijn
-> CekValEnv uni fun ann -> CekM uni fun s (CekValue uni fun ann)
lookupVarName NamedDeBruijn
varName CekValEnv uni fun ann
env
        Context uni fun ann
-> CekValue uni fun ann -> CekM uni fun s (DischargeResult uni fun)
returnCek Context uni fun ann
ctx CekValue uni fun ann
val
    -- s ; ρ ▻ con c  ↦  s ◅ con c
    computeCek !Context uni fun ann
ctx !CekValEnv uni fun ann
_ (Constant ann
_ Some (ValueOf uni)
val) = do
        StepKind -> CekM uni fun s ()
stepAndMaybeSpend StepKind
BConst
        Context uni fun ann
-> CekValue uni fun ann -> CekM uni fun s (DischargeResult uni fun)
returnCek Context uni fun ann
ctx (Some (ValueOf uni) -> CekValue uni fun ann
forall (uni :: * -> *) fun ann.
Some (ValueOf uni) -> CekValue uni fun ann
VCon Some (ValueOf uni)
val)
    -- s ; ρ ▻ lam x L  ↦  s ◅ lam x (L , ρ)
    computeCek !Context uni fun ann
ctx !CekValEnv uni fun ann
env (LamAbs ann
_ NamedDeBruijn
name NTerm uni fun ann
body) = do
        StepKind -> CekM uni fun s ()
stepAndMaybeSpend StepKind
BLamAbs
        Context uni fun ann
-> CekValue uni fun ann -> CekM uni fun s (DischargeResult uni fun)
returnCek Context uni fun ann
ctx (NamedDeBruijn
-> NTerm uni fun ann
-> CekValEnv uni fun ann
-> CekValue uni fun ann
forall (uni :: * -> *) fun ann.
NamedDeBruijn
-> NTerm uni fun ann
-> CekValEnv uni fun ann
-> CekValue uni fun ann
VLamAbs NamedDeBruijn
name NTerm uni fun ann
body CekValEnv uni fun ann
env)
    -- s ; ρ ▻ delay L  ↦  s ◅ delay (L , ρ)
    computeCek !Context uni fun ann
ctx !CekValEnv uni fun ann
env (Delay ann
_ NTerm uni fun ann
body) = do
        StepKind -> CekM uni fun s ()
stepAndMaybeSpend StepKind
BDelay
        Context uni fun ann
-> CekValue uni fun ann -> CekM uni fun s (DischargeResult uni fun)
returnCek Context uni fun ann
ctx (NTerm uni fun ann -> CekValEnv uni fun ann -> CekValue uni fun ann
forall (uni :: * -> *) fun ann.
NTerm uni fun ann -> CekValEnv uni fun ann -> CekValue uni fun ann
VDelay NTerm uni fun ann
body CekValEnv uni fun ann
env)
    -- s ; ρ ▻ force T  ↦  s , force _ ; ρ ▻ L
    computeCek !Context uni fun ann
ctx !CekValEnv uni fun ann
env (Force ann
_ NTerm uni fun ann
body) = do
        StepKind -> CekM uni fun s ()
stepAndMaybeSpend StepKind
BForce
        Context uni fun ann
-> CekValEnv uni fun ann
-> NTerm uni fun ann
-> CekM uni fun s (DischargeResult uni fun)
computeCek (Context uni fun ann -> Context uni fun ann
forall (uni :: * -> *) fun ann.
Context uni fun ann -> Context uni fun ann
FrameForce Context uni fun ann
ctx) CekValEnv uni fun ann
env NTerm uni fun ann
body
    -- s ; ρ ▻ [L M]  ↦  s , [_ (M,ρ)]  ; ρ ▻ L
    computeCek !Context uni fun ann
ctx !CekValEnv uni fun ann
env (Apply ann
_ NTerm uni fun ann
fun NTerm uni fun ann
arg) = do
        StepKind -> CekM uni fun s ()
stepAndMaybeSpend StepKind
BApply
        Context uni fun ann
-> CekValEnv uni fun ann
-> NTerm uni fun ann
-> CekM uni fun s (DischargeResult uni fun)
computeCek (CekValEnv uni fun ann
-> NTerm uni fun ann -> Context uni fun ann -> Context uni fun ann
forall (uni :: * -> *) fun ann.
CekValEnv uni fun ann
-> NTerm uni fun ann -> Context uni fun ann -> Context uni fun ann
FrameAwaitFunTerm CekValEnv uni fun ann
env NTerm uni fun ann
arg Context uni fun ann
ctx) CekValEnv uni fun ann
env NTerm uni fun ann
fun
    -- s ; ρ ▻ builtin bn  ↦  s ◅ builtin bn arity arity [] [] ρ
    computeCek !Context uni fun ann
ctx !CekValEnv uni fun ann
_ (Builtin ann
_ fun
bn) = do
        StepKind -> CekM uni fun s ()
stepAndMaybeSpend StepKind
BBuiltin
        let meaning :: BuiltinRuntime (CekValue uni fun ann)
meaning = fun
-> BuiltinsRuntime fun (CekValue uni fun ann)
-> BuiltinRuntime (CekValue uni fun ann)
forall fun val.
fun -> BuiltinsRuntime fun val -> BuiltinRuntime val
lookupBuiltin fun
bn ?cekRuntime::BuiltinsRuntime fun (CekValue uni fun ann)
BuiltinsRuntime fun (CekValue uni fun ann)
?cekRuntime
        -- 'Builtin' is fully discharged.
        Context uni fun ann
-> CekValue uni fun ann -> CekM uni fun s (DischargeResult uni fun)
returnCek Context uni fun ann
ctx (fun
-> Term NamedDeBruijn uni fun ()
-> BuiltinRuntime (CekValue uni fun ann)
-> CekValue uni fun ann
forall (uni :: * -> *) fun ann.
fun
-> NTerm uni fun ()
-> BuiltinRuntime (CekValue uni fun ann)
-> CekValue uni fun ann
VBuiltin fun
bn (() -> fun -> Term NamedDeBruijn uni fun ()
forall name (uni :: * -> *) fun ann.
ann -> fun -> Term name uni fun ann
Builtin () fun
bn) BuiltinRuntime (CekValue uni fun ann)
meaning)
    -- s ; ρ ▻ constr I T0 .. Tn  ↦  s , constr I _ (T1 ... Tn, ρ) ; ρ ▻ T0
    computeCek !Context uni fun ann
ctx !CekValEnv uni fun ann
env (Constr ann
_ Word64
i [NTerm uni fun ann]
es) = do
        StepKind -> CekM uni fun s ()
stepAndMaybeSpend StepKind
BConstr
        case [NTerm uni fun ann]
es of
          (NTerm uni fun ann
t : [NTerm uni fun ann]
rest) -> Context uni fun ann
-> CekValEnv uni fun ann
-> NTerm uni fun ann
-> CekM uni fun s (DischargeResult uni fun)
computeCek (CekValEnv uni fun ann
-> Word64
-> [NTerm uni fun ann]
-> ArgStack uni fun ann
-> Context uni fun ann
-> Context uni fun ann
forall (uni :: * -> *) fun ann.
CekValEnv uni fun ann
-> Word64
-> [NTerm uni fun ann]
-> ArgStack uni fun ann
-> Context uni fun ann
-> Context uni fun ann
FrameConstr CekValEnv uni fun ann
env Word64
i [NTerm uni fun ann]
rest ArgStack uni fun ann
forall (uni :: * -> *) fun ann. ArgStack uni fun ann
NilStack Context uni fun ann
ctx) CekValEnv uni fun ann
env NTerm uni fun ann
t
          []         -> Context uni fun ann
-> CekValue uni fun ann -> CekM uni fun s (DischargeResult uni fun)
returnCek Context uni fun ann
ctx (CekValue uni fun ann -> CekM uni fun s (DischargeResult uni fun))
-> CekValue uni fun ann -> CekM uni fun s (DischargeResult uni fun)
forall a b. (a -> b) -> a -> b
$ Word64 -> EmptyOrMultiStack uni fun ann -> CekValue uni fun ann
forall (uni :: * -> *) fun ann.
Word64 -> EmptyOrMultiStack uni fun ann -> CekValue uni fun ann
VConstr Word64
i EmptyOrMultiStack uni fun ann
forall (uni :: * -> *) fun ann. EmptyOrMultiStack uni fun ann
EmptyStack
    -- s ; ρ ▻ case S C0 ... Cn  ↦  s , case _ (C0 ... Cn, ρ) ; ρ ▻ S
    computeCek !Context uni fun ann
ctx !CekValEnv uni fun ann
env (Case ann
_ NTerm uni fun ann
scrut Vector (NTerm uni fun ann)
cs) = do
        StepKind -> CekM uni fun s ()
stepAndMaybeSpend StepKind
BCase
        Context uni fun ann
-> CekValEnv uni fun ann
-> NTerm uni fun ann
-> CekM uni fun s (DischargeResult uni fun)
computeCek (CekValEnv uni fun ann
-> Vector (NTerm uni fun ann)
-> Context uni fun ann
-> Context uni fun ann
forall (uni :: * -> *) fun ann.
CekValEnv uni fun ann
-> Vector (NTerm uni fun ann)
-> Context uni fun ann
-> Context uni fun ann
FrameCases CekValEnv uni fun ann
env Vector (NTerm uni fun ann)
cs Context uni fun ann
ctx) CekValEnv uni fun ann
env NTerm uni fun ann
scrut
    -- s ; ρ ▻ error  ↦  <> A
    computeCek !Context uni fun ann
_ !CekValEnv uni fun ann
_ (Error ann
_) =
        EvaluationError (MachineError fun) CekUserError
-> Term NamedDeBruijn uni fun ()
-> CekM uni fun s (DischargeResult uni fun)
forall e cause (m :: * -> *) x.
MonadError (ErrorWithCause e cause) m =>
e -> cause -> m x
throwErrorWithCause (CekUserError -> EvaluationError (MachineError fun) CekUserError
forall structural operational.
operational -> EvaluationError structural operational
OperationalError CekUserError
CekEvaluationFailure) (() -> Term NamedDeBruijn uni fun ()
forall name (uni :: * -> *) fun ann. ann -> Term name uni fun ann
Error ())

    {- | The returning phase of the CEK machine.
    Returns 'EvaluationSuccess' in case the context is empty, otherwise pops up one frame
    from the context and uses it to decide how to proceed with the current value v.

      * 'FrameForce': call forceEvaluate
      * 'FrameApplyArg': call 'computeCek' over the context extended with 'FrameApplyFun'
      * 'FrameApplyFun': call 'applyEvaluate' to attempt to apply the function
          stored in the frame to an argument.
    -}
    returnCek
        :: Context uni fun ann
        -> CekValue uni fun ann
        -> CekM uni fun s (DischargeResult uni fun)
    --- Instantiate all the free variable of the resulting term in case there are any.
    -- . ◅ V           ↦  [] V
    returnCek :: Context uni fun ann
-> CekValue uni fun ann -> CekM uni fun s (DischargeResult uni fun)
returnCek Context uni fun ann
NoFrame CekValue uni fun ann
val = do
        CekM uni fun s ()
spendAccumulatedBudget
        DischargeResult uni fun -> CekM uni fun s (DischargeResult uni fun)
forall a. a -> CekM uni fun s a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (DischargeResult uni fun
 -> CekM uni fun s (DischargeResult uni fun))
-> DischargeResult uni fun
-> CekM uni fun s (DischargeResult uni fun)
forall a b. (a -> b) -> a -> b
$ CekValue uni fun ann -> DischargeResult uni fun
forall (uni :: * -> *) fun ann.
CekValue uni fun ann -> DischargeResult uni fun
dischargeCekValue CekValue uni fun ann
val
    -- s , {_ A} ◅ abs α M  ↦  s ; ρ ▻ M [ α / A ]*
    returnCek (FrameForce Context uni fun ann
ctx) CekValue uni fun ann
fun = Context uni fun ann
-> CekValue uni fun ann -> CekM uni fun s (DischargeResult uni fun)
forceEvaluate Context uni fun ann
ctx CekValue uni fun ann
fun
    -- s , [_ (M,ρ)] ◅ V  ↦  s , [V _] ; ρ ▻ M
    returnCek (FrameAwaitFunTerm CekValEnv uni fun ann
argVarEnv NTerm uni fun ann
arg Context uni fun ann
ctx) CekValue uni fun ann
fun =
        Context uni fun ann
-> CekValEnv uni fun ann
-> NTerm uni fun ann
-> CekM uni fun s (DischargeResult uni fun)
computeCek (CekValue uni fun ann -> Context uni fun ann -> Context uni fun ann
forall (uni :: * -> *) fun ann.
CekValue uni fun ann -> Context uni fun ann -> Context uni fun ann
FrameAwaitArg CekValue uni fun ann
fun Context uni fun ann
ctx) CekValEnv uni fun ann
argVarEnv NTerm uni fun ann
arg
    -- s , [(lam x (M,ρ)) _] ◅ V  ↦  s ; ρ [ x  ↦  V ] ▻ M
    -- FIXME (https://github.com/IntersectMBO/plutus-private/issues/1878):
    -- add rule for VBuiltin once it's in the specification.
    returnCek (FrameAwaitArg CekValue uni fun ann
fun Context uni fun ann
ctx) CekValue uni fun ann
arg =
        Context uni fun ann
-> CekValue uni fun ann
-> CekValue uni fun ann
-> CekM uni fun s (DischargeResult uni fun)
applyEvaluate Context uni fun ann
ctx CekValue uni fun ann
fun CekValue uni fun ann
arg
    -- s , [_ V] ◅ lam x (M,ρ) ↦ s ; ρ [ x  ↦  V ] ▻ M
    returnCek (FrameAwaitFunConN Spine (Some (ValueOf uni))
args Context uni fun ann
ctx) CekValue uni fun ann
fun =
      -- In the future, if we want to revert back to more general
      -- 'FrameAwaitFunValue (CekValue uni fun ann)', we can use optimization proposed in
      -- https://github.com/IntersectMBO/plutus/pull/7288.  #7288 have almost equivalent
      -- performance improvement as using 'FrameAwaitFunConN' while keeping more general
      -- 'FrameAwaitFunValue'.
      case Spine (Some (ValueOf uni))
args of
        SpineLast Some (ValueOf uni)
arg      -> Context uni fun ann
-> CekValue uni fun ann
-> CekValue uni fun ann
-> CekM uni fun s (DischargeResult uni fun)
applyEvaluate Context uni fun ann
ctx CekValue uni fun ann
fun (Some (ValueOf uni) -> CekValue uni fun ann
forall (uni :: * -> *) fun ann.
Some (ValueOf uni) -> CekValue uni fun ann
VCon Some (ValueOf uni)
arg)
        SpineCons Some (ValueOf uni)
arg Spine (Some (ValueOf uni))
rest -> Context uni fun ann
-> CekValue uni fun ann
-> CekValue uni fun ann
-> CekM uni fun s (DischargeResult uni fun)
applyEvaluate (Spine (Some (ValueOf uni))
-> Context uni fun ann -> Context uni fun ann
forall (uni :: * -> *) fun ann.
Spine (Some (ValueOf uni))
-> Context uni fun ann -> Context uni fun ann
FrameAwaitFunConN Spine (Some (ValueOf uni))
rest Context uni fun ann
ctx) CekValue uni fun ann
fun (Some (ValueOf uni) -> CekValue uni fun ann
forall (uni :: * -> *) fun ann.
Some (ValueOf uni) -> CekValue uni fun ann
VCon Some (ValueOf uni)
arg)
    -- s , [_ V1 .. Vn] ◅ lam x (M,ρ)  ↦  s , [_ V2 .. Vn]; ρ [ x  ↦  V1 ] ▻ M
    returnCek (FrameAwaitFunValueN ArgStackNonEmpty uni fun ann
args Context uni fun ann
ctx) CekValue uni fun ann
fun =
        case ArgStackNonEmpty uni fun ann
args of
          LastStackNonEmpty CekValue uni fun ann
arg ->
            Context uni fun ann
-> CekValue uni fun ann
-> CekValue uni fun ann
-> CekM uni fun s (DischargeResult uni fun)
applyEvaluate Context uni fun ann
ctx CekValue uni fun ann
fun CekValue uni fun ann
arg
          ConsStackNonEmpty CekValue uni fun ann
arg ArgStackNonEmpty uni fun ann
rest ->
            Context uni fun ann
-> CekValue uni fun ann
-> CekValue uni fun ann
-> CekM uni fun s (DischargeResult uni fun)
applyEvaluate (ArgStackNonEmpty uni fun ann
-> Context uni fun ann -> Context uni fun ann
forall (uni :: * -> *) fun ann.
ArgStackNonEmpty uni fun ann
-> Context uni fun ann -> Context uni fun ann
FrameAwaitFunValueN ArgStackNonEmpty uni fun ann
rest Context uni fun ann
ctx) CekValue uni fun ann
fun CekValue uni fun ann
arg
    -- s , constr I V0 ... Vj-1 _ (Tj+1 ... Tn, ρ) ◅ Vj  ↦  s , constr i V0 ... Vj _ (Tj+2... Tn, ρ)  ; ρ ▻ Tj+1
    returnCek (FrameConstr CekValEnv uni fun ann
env Word64
i [NTerm uni fun ann]
todo ArgStack uni fun ann
done Context uni fun ann
ctx) CekValue uni fun ann
e = do
        case [NTerm uni fun ann]
todo of
          (NTerm uni fun ann
next : [NTerm uni fun ann]
todo') -> Context uni fun ann
-> CekValEnv uni fun ann
-> NTerm uni fun ann
-> CekM uni fun s (DischargeResult uni fun)
computeCek (CekValEnv uni fun ann
-> Word64
-> [NTerm uni fun ann]
-> ArgStack uni fun ann
-> Context uni fun ann
-> Context uni fun ann
forall (uni :: * -> *) fun ann.
CekValEnv uni fun ann
-> Word64
-> [NTerm uni fun ann]
-> ArgStack uni fun ann
-> Context uni fun ann
-> Context uni fun ann
FrameConstr CekValEnv uni fun ann
env Word64
i [NTerm uni fun ann]
todo' (CekValue uni fun ann
-> ArgStack uni fun ann -> ArgStack uni fun ann
forall (uni :: * -> *) fun ann.
CekValue uni fun ann
-> ArgStack uni fun ann -> ArgStack uni fun ann
ConsStack CekValue uni fun ann
e ArgStack uni fun ann
done) Context uni fun ann
ctx) CekValEnv uni fun ann
env NTerm uni fun ann
next
          []             ->
            let go :: ArgStackNonEmpty uni fun ann
-> ArgStack uni fun ann -> ArgStackNonEmpty uni fun ann
go ArgStackNonEmpty uni fun ann
acc ArgStack uni fun ann
NilStack         = ArgStackNonEmpty uni fun ann
acc
                go ArgStackNonEmpty uni fun ann
acc (ConsStack CekValue uni fun ann
x ArgStack uni fun ann
xs) = ArgStackNonEmpty uni fun ann
-> ArgStack uni fun ann -> ArgStackNonEmpty uni fun ann
go (CekValue uni fun ann
-> ArgStackNonEmpty uni fun ann -> ArgStackNonEmpty uni fun ann
forall (uni :: * -> *) fun ann.
CekValue uni fun ann
-> ArgStackNonEmpty uni fun ann -> ArgStackNonEmpty uni fun ann
ConsStackNonEmpty CekValue uni fun ann
x ArgStackNonEmpty uni fun ann
acc) ArgStack uni fun ann
xs
            in Context uni fun ann
-> CekValue uni fun ann -> CekM uni fun s (DischargeResult uni fun)
returnCek Context uni fun ann
ctx (CekValue uni fun ann -> CekM uni fun s (DischargeResult uni fun))
-> CekValue uni fun ann -> CekM uni fun s (DischargeResult uni fun)
forall a b. (a -> b) -> a -> b
$ Word64 -> EmptyOrMultiStack uni fun ann -> CekValue uni fun ann
forall (uni :: * -> *) fun ann.
Word64 -> EmptyOrMultiStack uni fun ann -> CekValue uni fun ann
VConstr Word64
i (ArgStackNonEmpty uni fun ann -> EmptyOrMultiStack uni fun ann
forall (uni :: * -> *) fun ann.
ArgStackNonEmpty uni fun ann -> EmptyOrMultiStack uni fun ann
MultiStack (ArgStackNonEmpty uni fun ann -> EmptyOrMultiStack uni fun ann)
-> ArgStackNonEmpty uni fun ann -> EmptyOrMultiStack uni fun ann
forall a b. (a -> b) -> a -> b
$ ArgStackNonEmpty uni fun ann
-> ArgStack uni fun ann -> ArgStackNonEmpty uni fun ann
forall {uni :: * -> *} {fun} {ann}.
ArgStackNonEmpty uni fun ann
-> ArgStack uni fun ann -> ArgStackNonEmpty uni fun ann
go (CekValue uni fun ann -> ArgStackNonEmpty uni fun ann
forall (uni :: * -> *) fun ann.
CekValue uni fun ann -> ArgStackNonEmpty uni fun ann
LastStackNonEmpty CekValue uni fun ann
e) ArgStack uni fun ann
done)
    -- s , case _ (C0 ... CN, ρ) ◅ constr i V1 .. Vm  ↦  s , [_ V1 ... Vm] ; ρ ▻ Ci
    returnCek (FrameCases CekValEnv uni fun ann
env Vector (NTerm uni fun ann)
cs Context uni fun ann
ctx) CekValue uni fun ann
e = case CekValue uni fun ann
e of
        -- If the index is larger than the max bound of an Int, or negative, then it's a bad index
        -- As it happens, this will currently never trigger, since i is a Word64, and the largest
        -- Word64 value wraps to -1 as an Int64. So you can't wrap around enough to get an
        -- "apparently good" value.
        (VConstr Word64
i EmptyOrMultiStack uni fun ann
_) | forall a b. (Integral a, Num b) => a -> b
fromIntegral @_ @Integer Word64
i Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
> forall a b. (Integral a, Num b) => a -> b
fromIntegral @Int @Integer Int
forall a. Bounded a => a
maxBound ->
                        EvaluationError (MachineError fun) CekUserError
-> CekValue uni fun ann -> CekM uni fun s (DischargeResult uni fun)
forall (uni :: * -> *) fun ann s x.
ThrowableBuiltins uni fun =>
EvaluationError (MachineError fun) CekUserError
-> CekValue uni fun ann -> CekM uni fun s x
throwErrorDischarged (MachineError fun -> EvaluationError (MachineError fun) CekUserError
forall structural operational.
structural -> EvaluationError structural operational
StructuralError (Word64 -> MachineError fun
forall fun. Word64 -> MachineError fun
MissingCaseBranchMachineError Word64
i)) CekValue uni fun ann
e
        -- Otherwise, we can safely convert the index to an Int and use it.
        (VConstr Word64
i EmptyOrMultiStack uni fun ann
args) -> case Vector (NTerm uni fun ann) -> Int -> Maybe (NTerm uni fun ann)
forall a. Vector a -> Int -> Maybe a
(V.!?) Vector (NTerm uni fun ann)
cs (Word64 -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Word64
i) of
            Just NTerm uni fun ann
t  -> case EmptyOrMultiStack uni fun ann
args of
              EmptyOrMultiStack uni fun ann
EmptyStack      -> Context uni fun ann
-> CekValEnv uni fun ann
-> NTerm uni fun ann
-> CekM uni fun s (DischargeResult uni fun)
computeCek Context uni fun ann
ctx CekValEnv uni fun ann
env NTerm uni fun ann
t
              MultiStack ArgStackNonEmpty uni fun ann
rest -> Context uni fun ann
-> CekValEnv uni fun ann
-> NTerm uni fun ann
-> CekM uni fun s (DischargeResult uni fun)
computeCek (ArgStackNonEmpty uni fun ann
-> Context uni fun ann -> Context uni fun ann
forall (uni :: * -> *) fun ann.
ArgStackNonEmpty uni fun ann
-> Context uni fun ann -> Context uni fun ann
FrameAwaitFunValueN ArgStackNonEmpty uni fun ann
rest Context uni fun ann
ctx) CekValEnv uni fun ann
env NTerm uni fun ann
t
            Maybe (NTerm uni fun ann)
Nothing -> EvaluationError (MachineError fun) CekUserError
-> CekValue uni fun ann -> CekM uni fun s (DischargeResult uni fun)
forall (uni :: * -> *) fun ann s x.
ThrowableBuiltins uni fun =>
EvaluationError (MachineError fun) CekUserError
-> CekValue uni fun ann -> CekM uni fun s x
throwErrorDischarged (MachineError fun -> EvaluationError (MachineError fun) CekUserError
forall structural operational.
structural -> EvaluationError structural operational
StructuralError (MachineError fun
 -> EvaluationError (MachineError fun) CekUserError)
-> MachineError fun
-> EvaluationError (MachineError fun) CekUserError
forall a b. (a -> b) -> a -> b
$ Word64 -> MachineError fun
forall fun. Word64 -> MachineError fun
MissingCaseBranchMachineError Word64
i) CekValue uni fun ann
e
        -- Proceed with caser when expression given is not Constr.
        VCon Some (ValueOf uni)
val -> case CaserBuiltin uni
-> forall term.
   (UniOf term ~ uni) =>
   Some (ValueOf uni)
   -> Vector term -> Either Text (HeadSpine term (Some (ValueOf uni)))
forall (uni :: * -> *).
CaserBuiltin uni
-> forall term.
   (UniOf term ~ uni) =>
   Some (ValueOf uni)
   -> Vector term -> Either Text (HeadSpine term (Some (ValueOf uni)))
unCaserBuiltin ?cekCaserBuiltin::CaserBuiltin uni
CaserBuiltin uni
?cekCaserBuiltin Some (ValueOf uni)
val Vector (NTerm uni fun ann)
cs of
            Left Text
err          -> EvaluationError (MachineError fun) CekUserError
-> CekValue uni fun ann -> CekM uni fun s (DischargeResult uni fun)
forall (uni :: * -> *) fun ann s x.
ThrowableBuiltins uni fun =>
EvaluationError (MachineError fun) CekUserError
-> CekValue uni fun ann -> CekM uni fun s x
throwErrorDischarged (CekUserError -> EvaluationError (MachineError fun) CekUserError
forall structural operational.
operational -> EvaluationError structural operational
OperationalError (CekUserError -> EvaluationError (MachineError fun) CekUserError)
-> CekUserError -> EvaluationError (MachineError fun) CekUserError
forall a b. (a -> b) -> a -> b
$ Text -> CekUserError
CekCaseBuiltinError Text
err) CekValue uni fun ann
e
            Right (HeadOnly NTerm uni fun ann
fX) -> Context uni fun ann
-> CekValEnv uni fun ann
-> NTerm uni fun ann
-> CekM uni fun s (DischargeResult uni fun)
computeCek Context uni fun ann
ctx CekValEnv uni fun ann
env NTerm uni fun ann
fX
            Right (HeadSpine NTerm uni fun ann
f Spine (Some (ValueOf uni))
xs) -> Context uni fun ann
-> CekValEnv uni fun ann
-> NTerm uni fun ann
-> CekM uni fun s (DischargeResult uni fun)
computeCek (Spine (Some (ValueOf uni))
-> Context uni fun ann -> Context uni fun ann
forall (uni :: * -> *) fun ann.
Spine (Some (ValueOf uni))
-> Context uni fun ann -> Context uni fun ann
FrameAwaitFunConN Spine (Some (ValueOf uni))
xs Context uni fun ann
ctx) CekValEnv uni fun ann
env NTerm uni fun ann
f
        CekValue uni fun ann
_ -> EvaluationError (MachineError fun) CekUserError
-> CekValue uni fun ann -> CekM uni fun s (DischargeResult uni fun)
forall (uni :: * -> *) fun ann s x.
ThrowableBuiltins uni fun =>
EvaluationError (MachineError fun) CekUserError
-> CekValue uni fun ann -> CekM uni fun s x
throwErrorDischarged (MachineError fun -> EvaluationError (MachineError fun) CekUserError
forall structural operational.
structural -> EvaluationError structural operational
StructuralError MachineError fun
forall fun. MachineError fun
NonConstrScrutinizedMachineError) CekValue uni fun ann
e

    -- | @force@ a term and proceed.
    -- If v is a delay then compute the body of v;
    -- if v is a builtin application then check that it's expecting a type argument,
    -- and either calculate the builtin application or stick a 'Force' on top of its 'Term'
    -- representation depending on whether the application is saturated or not,
    -- if v is anything else, fail.
    forceEvaluate
        :: Context uni fun ann
        -> CekValue uni fun ann
        -> CekM uni fun s (DischargeResult uni fun)
    forceEvaluate :: Context uni fun ann
-> CekValue uni fun ann -> CekM uni fun s (DischargeResult uni fun)
forceEvaluate !Context uni fun ann
ctx (VDelay NTerm uni fun ann
body CekValEnv uni fun ann
env) = Context uni fun ann
-> CekValEnv uni fun ann
-> NTerm uni fun ann
-> CekM uni fun s (DischargeResult uni fun)
computeCek Context uni fun ann
ctx CekValEnv uni fun ann
env NTerm uni fun ann
body
    forceEvaluate !Context uni fun ann
ctx (VBuiltin fun
fun Term NamedDeBruijn uni fun ()
term BuiltinRuntime (CekValue uni fun ann)
runtime) = do
        -- @term@ is fully discharged, and so @term'@ is, hence we can put it in a 'VBuiltin'.
        let term' :: Term NamedDeBruijn uni fun ()
term' = ()
-> Term NamedDeBruijn uni fun () -> Term NamedDeBruijn uni fun ()
forall name (uni :: * -> *) fun ann.
ann -> Term name uni fun ann -> Term name uni fun ann
Force () Term NamedDeBruijn uni fun ()
term
        case BuiltinRuntime (CekValue uni fun ann)
runtime of
            -- It's only possible to force a builtin application if the builtin expects a type
            -- argument next.
            BuiltinExpectForce BuiltinRuntime (CekValue uni fun ann)
runtime' ->
                -- We allow a type argument to appear last in the type of a built-in function,
                -- otherwise we could just assemble a 'VBuiltin' without trying to evaluate the
                -- application.
                Context uni fun ann
-> fun
-> Term NamedDeBruijn uni fun ()
-> BuiltinRuntime (CekValue uni fun ann)
-> CekM uni fun s (DischargeResult uni fun)
evalBuiltinApp Context uni fun ann
ctx fun
fun Term NamedDeBruijn uni fun ()
term' BuiltinRuntime (CekValue uni fun ann)
runtime'
            BuiltinRuntime (CekValue uni fun ann)
_ ->
                EvaluationError (MachineError fun) CekUserError
-> Term NamedDeBruijn uni fun ()
-> CekM uni fun s (DischargeResult uni fun)
forall e cause (m :: * -> *) x.
MonadError (ErrorWithCause e cause) m =>
e -> cause -> m x
throwErrorWithCause (MachineError fun -> EvaluationError (MachineError fun) CekUserError
forall structural operational.
structural -> EvaluationError structural operational
StructuralError MachineError fun
forall fun. MachineError fun
BuiltinTermArgumentExpectedMachineError) Term NamedDeBruijn uni fun ()
term'
    forceEvaluate !Context uni fun ann
_ CekValue uni fun ann
val =
        EvaluationError (MachineError fun) CekUserError
-> CekValue uni fun ann -> CekM uni fun s (DischargeResult uni fun)
forall (uni :: * -> *) fun ann s x.
ThrowableBuiltins uni fun =>
EvaluationError (MachineError fun) CekUserError
-> CekValue uni fun ann -> CekM uni fun s x
throwErrorDischarged (MachineError fun -> EvaluationError (MachineError fun) CekUserError
forall structural operational.
structural -> EvaluationError structural operational
StructuralError MachineError fun
forall fun. MachineError fun
NonPolymorphicInstantiationMachineError) CekValue uni fun ann
val

    -- | Apply a function to an argument and proceed.
    -- If the function is a lambda 'lam x ty body' then extend the environment with a binding of @v@
    -- to x@ and call 'computeCek' on the body.
    -- If the function is a builtin application then check that it's expecting a term argument,
    -- and either calculate the builtin application or stick a 'Apply' on top of its 'Term'
    -- representation depending on whether the application is saturated or not.
    -- If v is anything else, fail.
    applyEvaluate
        :: Context uni fun ann
        -> CekValue uni fun ann   -- lhs of application
        -> CekValue uni fun ann   -- rhs of application
        -> CekM uni fun s (DischargeResult uni fun)
    applyEvaluate :: Context uni fun ann
-> CekValue uni fun ann
-> CekValue uni fun ann
-> CekM uni fun s (DischargeResult uni fun)
applyEvaluate !Context uni fun ann
ctx (VLamAbs NamedDeBruijn
_ NTerm uni fun ann
body CekValEnv uni fun ann
env) CekValue uni fun ann
arg =
        Context uni fun ann
-> CekValEnv uni fun ann
-> NTerm uni fun ann
-> CekM uni fun s (DischargeResult uni fun)
computeCek Context uni fun ann
ctx (Element (CekValEnv uni fun ann)
-> CekValEnv uni fun ann -> CekValEnv uni fun ann
forall e. RandomAccessList e => Element e -> e -> e
Env.cons Element (CekValEnv uni fun ann)
CekValue uni fun ann
arg CekValEnv uni fun ann
env) NTerm uni fun ann
body
    -- Annotating @f@ and @exF@ with bangs gave us some speed-up, but only until we added a bang to
    -- 'VCon'. After that the bangs here were making things a tiny bit slower and so we removed them.
    applyEvaluate !Context uni fun ann
ctx (VBuiltin fun
fun Term NamedDeBruijn uni fun ()
funTerm BuiltinRuntime (CekValue uni fun ann)
runtime) CekValue uni fun ann
arg = do
        let argTerm :: Term NamedDeBruijn uni fun ()
argTerm = DischargeResult uni fun -> Term NamedDeBruijn uni fun ()
forall (uni :: * -> *) fun.
DischargeResult uni fun -> NTerm uni fun ()
dischargeResultToTerm (DischargeResult uni fun -> Term NamedDeBruijn uni fun ())
-> DischargeResult uni fun -> Term NamedDeBruijn uni fun ()
forall a b. (a -> b) -> a -> b
$ CekValue uni fun ann -> DischargeResult uni fun
forall (uni :: * -> *) fun ann.
CekValue uni fun ann -> DischargeResult uni fun
dischargeCekValue CekValue uni fun ann
arg
            -- @term@ and @argTerm@ are fully discharged, and so @term'@ is, hence we can put it
            -- in a 'VBuiltin'.
            term' :: Term NamedDeBruijn uni fun ()
term' = ()
-> Term NamedDeBruijn uni fun ()
-> Term NamedDeBruijn uni fun ()
-> Term NamedDeBruijn uni fun ()
forall name (uni :: * -> *) fun ann.
ann
-> Term name uni fun ann
-> Term name uni fun ann
-> Term name uni fun ann
Apply () Term NamedDeBruijn uni fun ()
funTerm Term NamedDeBruijn uni fun ()
argTerm
        case BuiltinRuntime (CekValue uni fun ann)
runtime of
            -- It's only possible to apply a builtin application if the builtin expects a term
            -- argument next.
            BuiltinExpectArgument CekValue uni fun ann -> BuiltinRuntime (CekValue uni fun ann)
f ->
                Context uni fun ann
-> fun
-> Term NamedDeBruijn uni fun ()
-> BuiltinRuntime (CekValue uni fun ann)
-> CekM uni fun s (DischargeResult uni fun)
evalBuiltinApp Context uni fun ann
ctx fun
fun Term NamedDeBruijn uni fun ()
term' (BuiltinRuntime (CekValue uni fun ann)
 -> CekM uni fun s (DischargeResult uni fun))
-> BuiltinRuntime (CekValue uni fun ann)
-> CekM uni fun s (DischargeResult uni fun)
forall a b. (a -> b) -> a -> b
$ CekValue uni fun ann -> BuiltinRuntime (CekValue uni fun ann)
f CekValue uni fun ann
arg
            BuiltinRuntime (CekValue uni fun ann)
_ ->
                EvaluationError (MachineError fun) CekUserError
-> Term NamedDeBruijn uni fun ()
-> CekM uni fun s (DischargeResult uni fun)
forall e cause (m :: * -> *) x.
MonadError (ErrorWithCause e cause) m =>
e -> cause -> m x
throwErrorWithCause (MachineError fun -> EvaluationError (MachineError fun) CekUserError
forall structural operational.
structural -> EvaluationError structural operational
StructuralError MachineError fun
forall fun. MachineError fun
UnexpectedBuiltinTermArgumentMachineError) Term NamedDeBruijn uni fun ()
term'
    applyEvaluate !Context uni fun ann
_ CekValue uni fun ann
val CekValue uni fun ann
_ =
        EvaluationError (MachineError fun) CekUserError
-> CekValue uni fun ann -> CekM uni fun s (DischargeResult uni fun)
forall (uni :: * -> *) fun ann s x.
ThrowableBuiltins uni fun =>
EvaluationError (MachineError fun) CekUserError
-> CekValue uni fun ann -> CekM uni fun s x
throwErrorDischarged (MachineError fun -> EvaluationError (MachineError fun) CekUserError
forall structural operational.
structural -> EvaluationError structural operational
StructuralError MachineError fun
forall fun. MachineError fun
NonFunctionalApplicationMachineError) CekValue uni fun ann
val

    -- | Spend the budget that has been accumulated for a number of machine steps.
    spendAccumulatedBudget :: CekM uni fun s ()
    spendAccumulatedBudget :: CekM uni fun s ()
spendAccumulatedBudget = do
        let ctr :: StepCounter 10 s
ctr = ?cekStepCounter::StepCounter 10 s
StepCounter 10 s
?cekStepCounter
        StepCounter 10 (PrimState (CekM uni fun s))
-> (Int -> Slippage -> CekM uni fun s ()) -> CekM uni fun s ()
forall (m :: * -> *) (n :: Nat).
(UpwardsM m (NatToPeano n), PrimMonad m) =>
StepCounter n (PrimState m) -> (Int -> Slippage -> m ()) -> m ()
iforCounter_ StepCounter 10 s
StepCounter 10 (PrimState (CekM uni fun s))
ctr Int -> Slippage -> CekM uni fun s ()
spend
        StepCounter 10 (PrimState (CekM uni fun s)) -> CekM uni fun s ()
forall (n :: Nat) (m :: * -> *).
(KnownNat n, PrimMonad m) =>
StepCounter n (PrimState m) -> m ()
resetCounter StepCounter 10 s
StepCounter 10 (PrimState (CekM uni fun s))
ctr
    -- It's very important for this definition not to get inlined. Inlining it caused performance to
    -- degrade by 16+%: https://github.com/IntersectMBO/plutus/pull/5931
    {-# OPAQUE spendAccumulatedBudget #-}

    -- Making this a definition of its own causes it to inline better than actually writing it inline, for
    -- some reason.
    -- Skip index 7, that's the total counter!
    -- See Note [Structure of the step counter]
    spend :: Int -> Slippage -> CekM uni fun s ()
spend !Int
i !Slippage
w = Bool -> CekM uni fun s () -> CekM uni fun s ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Int
i Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== (Integer -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Integer -> Int) -> Integer -> Int
forall a b. (a -> b) -> a -> b
$ Proxy 9 -> Integer
forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Integer
natVal (Proxy 9 -> Integer) -> Proxy 9 -> Integer
forall a b. (a -> b) -> a -> b
$ forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @TotalCountIndex)) (CekM uni fun s () -> CekM uni fun s ())
-> CekM uni fun s () -> CekM uni fun s ()
forall a b. (a -> b) -> a -> b
$
      let kind :: StepKind
kind = Int -> StepKind
forall a. Enum a => Int -> a
toEnum Int
i in ExBudgetCategory fun -> ExBudget -> CekM uni fun s ()
spendBudget (StepKind -> ExBudgetCategory fun
forall fun. StepKind -> ExBudgetCategory fun
BStep StepKind
kind) (Slippage -> ExBudget -> ExBudget
forall b. Integral b => b -> ExBudget -> ExBudget
forall a b. (Semigroup a, Integral b) => b -> a -> a
stimes Slippage
w (CekMachineCosts -> StepKind -> ExBudget
cekStepCost ?cekCosts::CekMachineCosts
CekMachineCosts
?cekCosts StepKind
kind))
    {-# INLINE spend #-}

    -- | Accumulate a step, and maybe spend the budget that has accumulated for a number of machine steps, but only if we've exceeded our slippage.
    stepAndMaybeSpend :: StepKind -> CekM uni fun s ()
    stepAndMaybeSpend :: StepKind -> CekM uni fun s ()
stepAndMaybeSpend !StepKind
kind = do
        -- See Note [Structure of the step counter]
        -- This generates let-expressions in GHC Core, however all of them bind unboxed things and
        -- so they don't survive further compilation, see https://stackoverflow.com/a/14090277
        let !counterIndex :: Int
counterIndex = StepKind -> Int
forall a. Enum a => a -> Int
fromEnum StepKind
kind
            ctr :: StepCounter 10 s
ctr = ?cekStepCounter::StepCounter 10 s
StepCounter 10 s
?cekStepCounter
            !totalStepIndex :: Int
totalStepIndex = Integer -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Integer -> Int) -> Integer -> Int
forall a b. (a -> b) -> a -> b
$ Proxy 9 -> Integer
forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Integer
natVal (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @TotalCountIndex)
        !Slippage
unbudgetedStepsTotal <-  Int
-> (Slippage -> Slippage)
-> StepCounter 10 (PrimState (CekM uni fun s))
-> CekM uni fun s Slippage
forall (m :: * -> *) (n :: Nat).
PrimMonad m =>
Int
-> (Slippage -> Slippage)
-> StepCounter n (PrimState m)
-> m Slippage
modifyCounter Int
totalStepIndex (Slippage -> Slippage -> Slippage
forall a. Num a => a -> a -> a
+Slippage
1) StepCounter 10 s
StepCounter 10 (PrimState (CekM uni fun s))
ctr
        Slippage
_ <- Int
-> (Slippage -> Slippage)
-> StepCounter 10 (PrimState (CekM uni fun s))
-> CekM uni fun s Slippage
forall (m :: * -> *) (n :: Nat).
PrimMonad m =>
Int
-> (Slippage -> Slippage)
-> StepCounter n (PrimState m)
-> m Slippage
modifyCounter Int
counterIndex (Slippage -> Slippage -> Slippage
forall a. Num a => a -> a -> a
+Slippage
1) StepCounter 10 s
StepCounter 10 (PrimState (CekM uni fun s))
ctr
        -- There's no risk of overflow here, since we only ever increment the total
        -- steps by 1 and then check this condition.
        Bool -> CekM uni fun s () -> CekM uni fun s ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Slippage
unbudgetedStepsTotal Slippage -> Slippage -> Bool
forall a. Ord a => a -> a -> Bool
>= ?cekSlippage::Slippage
Slippage
?cekSlippage) CekM uni fun s ()
spendAccumulatedBudget
    {-# INLINE stepAndMaybeSpend #-}

    -- | Take a possibly partial builtin application and
    --
    -- - either create a 'CekValue' by evaluating the application if it's saturated (emitting logs,
    --    if any, along the way), potentially failing evaluation
    -- - or create a partial builtin application otherwise
    --
    -- and proceed with the returning phase of the CEK machine.
    evalBuiltinApp
        :: Context uni fun ann
        -> fun
        -> NTerm uni fun ()
        -> BuiltinRuntime (CekValue uni fun ann)
        -> CekM uni fun s (DischargeResult uni fun)
    evalBuiltinApp :: Context uni fun ann
-> fun
-> Term NamedDeBruijn uni fun ()
-> BuiltinRuntime (CekValue uni fun ann)
-> CekM uni fun s (DischargeResult uni fun)
evalBuiltinApp Context uni fun ann
ctx fun
fun Term NamedDeBruijn uni fun ()
term BuiltinRuntime (CekValue uni fun ann)
runtime = case BuiltinRuntime (CekValue uni fun ann)
runtime of
        BuiltinCostedResult ExBudgetStream
budgets0 BuiltinResult (CekValue uni fun ann)
getFXs -> do
            let exCat :: ExBudgetCategory fun
exCat = fun -> ExBudgetCategory fun
forall fun. fun -> ExBudgetCategory fun
BBuiltinApp fun
fun
                spendBudgets :: ExBudgetStream -> CekM uni fun s ()
spendBudgets (ExBudgetLast ExBudget
budget) = ExBudgetCategory fun -> ExBudget -> CekM uni fun s ()
spendBudget ExBudgetCategory fun
exCat ExBudget
budget
                spendBudgets (ExBudgetCons ExBudget
budget ExBudgetStream
budgets) =
                    ExBudgetCategory fun -> ExBudget -> CekM uni fun s ()
spendBudget ExBudgetCategory fun
exCat ExBudget
budget CekM uni fun s () -> CekM uni fun s () -> CekM uni fun s ()
forall a b.
CekM uni fun s a -> CekM uni fun s b -> CekM uni fun s b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> ExBudgetStream -> CekM uni fun s ()
spendBudgets ExBudgetStream
budgets
            ExBudgetStream -> CekM uni fun s ()
spendBudgets ExBudgetStream
budgets0
            case BuiltinResult (CekValue uni fun ann)
getFXs of
                BuiltinSuccess CekValue uni fun ann
y ->
                    Context uni fun ann
-> CekValue uni fun ann -> CekM uni fun s (DischargeResult uni fun)
returnCek Context uni fun ann
ctx CekValue uni fun ann
y
                BuiltinSuccessWithLogs DList Text
logs CekValue uni fun ann
y -> do
                    ?cekEmitter::DList Text -> CekM uni fun s ()
DList Text -> CekM uni fun s ()
?cekEmitter DList Text
logs
                    Context uni fun ann
-> CekValue uni fun ann -> CekM uni fun s (DischargeResult uni fun)
returnCek Context uni fun ann
ctx CekValue uni fun ann
y
                BuiltinFailure DList Text
logs BuiltinError
err -> do
                    ?cekEmitter::DList Text -> CekM uni fun s ()
DList Text -> CekM uni fun s ()
?cekEmitter DList Text
logs
                    Term NamedDeBruijn uni fun ()
-> BuiltinError -> CekM uni fun s (DischargeResult uni fun)
forall structural operational cause (m :: * -> *) void.
(MonadError (EvaluationException structural operational cause) m,
 BuiltinErrorToEvaluationError structural operational) =>
cause -> BuiltinError -> m void
throwBuiltinErrorWithCause Term NamedDeBruijn uni fun ()
term BuiltinError
err
        BuiltinRuntime (CekValue uni fun ann)
_ -> Context uni fun ann
-> CekValue uni fun ann -> CekM uni fun s (DischargeResult uni fun)
returnCek Context uni fun ann
ctx (CekValue uni fun ann -> CekM uni fun s (DischargeResult uni fun))
-> CekValue uni fun ann -> CekM uni fun s (DischargeResult uni fun)
forall a b. (a -> b) -> a -> b
$ fun
-> Term NamedDeBruijn uni fun ()
-> BuiltinRuntime (CekValue uni fun ann)
-> CekValue uni fun ann
forall (uni :: * -> *) fun ann.
fun
-> NTerm uni fun ()
-> BuiltinRuntime (CekValue uni fun ann)
-> CekValue uni fun ann
VBuiltin fun
fun Term NamedDeBruijn uni fun ()
term BuiltinRuntime (CekValue uni fun ann)
runtime
    {-# INLINE evalBuiltinApp #-}

    spendBudget :: ExBudgetCategory fun -> ExBudget -> CekM uni fun s ()
    spendBudget :: ExBudgetCategory fun -> ExBudget -> CekM uni fun s ()
spendBudget = CekBudgetSpender uni fun s
-> ExBudgetCategory fun -> ExBudget -> CekM uni fun s ()
forall (uni :: * -> *) fun s.
CekBudgetSpender uni fun s
-> ExBudgetCategory fun -> ExBudget -> CekM uni fun s ()
unCekBudgetSpender ?cekBudgetSpender::CekBudgetSpender uni fun s
CekBudgetSpender uni fun s
?cekBudgetSpender
    {-# INLINE spendBudget #-}

    -- | Look up a variable name in the environment.
    lookupVarName :: NamedDeBruijn -> CekValEnv uni fun ann -> CekM uni fun s (CekValue uni fun ann)
    lookupVarName :: NamedDeBruijn
-> CekValEnv uni fun ann -> CekM uni fun s (CekValue uni fun ann)
lookupVarName varName :: NamedDeBruijn
varName@(NamedDeBruijn Text
_ Index
varIx) CekValEnv uni fun ann
varEnv =
        CekM uni fun s (CekValue uni fun ann)
-> (CekValue uni fun ann -> CekM uni fun s (CekValue uni fun ann))
-> CekValEnv uni fun ann
-> Word64
-> CekM uni fun s (CekValue uni fun ann)
forall a b. b -> (a -> b) -> RAList a -> Word64 -> b
Env.contIndexOne
            (EvaluationError (MachineError fun) CekUserError
-> Term NamedDeBruijn uni fun ()
-> CekM uni fun s (CekValue uni fun ann)
forall e cause (m :: * -> *) x.
MonadError (ErrorWithCause e cause) m =>
e -> cause -> m x
throwErrorWithCause (MachineError fun -> EvaluationError (MachineError fun) CekUserError
forall structural operational.
structural -> EvaluationError structural operational
StructuralError MachineError fun
forall fun. MachineError fun
OpenTermEvaluatedMachineError) (Term NamedDeBruijn uni fun ()
 -> CekM uni fun s (CekValue uni fun ann))
-> Term NamedDeBruijn uni fun ()
-> CekM uni fun s (CekValue uni fun ann)
forall a b. (a -> b) -> a -> b
$ () -> NamedDeBruijn -> Term NamedDeBruijn uni fun ()
forall name (uni :: * -> *) fun ann.
ann -> name -> Term name uni fun ann
Var () NamedDeBruijn
varName)
            CekValue uni fun ann -> CekM uni fun s (CekValue uni fun ann)
forall a. a -> CekM uni fun s a
forall (f :: * -> *) a. Applicative f => a -> f a
pure
            CekValEnv uni fun ann
varEnv
            (Index -> Word64
forall a b. Coercible a b => a -> b
coerce Index
varIx)
    {-# INLINE lookupVarName #-}

-- See Note [Compilation peculiarities].
-- | Evaluate a term using the CEK machine and keep track of costing, logging is optional.
runCekDeBruijn
    :: ThrowableBuiltins uni fun
    => MachineParameters CekMachineCosts fun (CekValue uni fun ann)
    -> ExBudgetMode cost uni fun
    -> EmitterMode uni fun
    -> NTerm uni fun ann
    -> CekReport cost NamedDeBruijn uni fun
runCekDeBruijn :: forall (uni :: * -> *) fun ann cost.
ThrowableBuiltins uni fun =>
MachineParameters CekMachineCosts fun (CekValue uni fun ann)
-> ExBudgetMode cost uni fun
-> EmitterMode uni fun
-> NTerm uni fun ann
-> CekReport cost NamedDeBruijn uni fun
runCekDeBruijn MachineParameters CekMachineCosts fun (CekValue uni fun ann)
params ExBudgetMode cost uni fun
mode EmitterMode uni fun
emitMode NTerm uni fun ann
term =
    MachineParameters CekMachineCosts fun (CekValue uni fun ann)
-> ExBudgetMode cost uni fun
-> EmitterMode uni fun
-> (forall {s}.
    GivenCekReqs uni fun ann s =>
    CekM uni fun s (DischargeResult uni fun))
-> CekReport cost NamedDeBruijn uni fun
forall cost (uni :: * -> *) fun ann.
ThrowableBuiltins uni fun =>
MachineParameters CekMachineCosts fun (CekValue uni fun ann)
-> ExBudgetMode cost uni fun
-> EmitterMode uni fun
-> (forall s.
    GivenCekReqs uni fun ann s =>
    CekM uni fun s (DischargeResult uni fun))
-> CekReport cost NamedDeBruijn uni fun
runCekM MachineParameters CekMachineCosts fun (CekValue uni fun ann)
params ExBudgetMode cost uni fun
mode EmitterMode uni fun
emitMode ((forall {s}.
  GivenCekReqs uni fun ann s =>
  CekM uni fun s (DischargeResult uni fun))
 -> CekReport cost NamedDeBruijn uni fun)
-> (forall {s}.
    GivenCekReqs uni fun ann s =>
    CekM uni fun s (DischargeResult uni fun))
-> CekReport cost NamedDeBruijn uni fun
forall a b. (a -> b) -> a -> b
$ do
        CekBudgetSpender uni fun s
-> ExBudgetCategory fun -> ExBudget -> CekM uni fun s ()
forall (uni :: * -> *) fun s.
CekBudgetSpender uni fun s
-> ExBudgetCategory fun -> ExBudget -> CekM uni fun s ()
unCekBudgetSpender ?cekBudgetSpender::CekBudgetSpender uni fun s
CekBudgetSpender uni fun s
?cekBudgetSpender ExBudgetCategory fun
forall fun. ExBudgetCategory fun
BStartup (ExBudget -> CekM uni fun s ()) -> ExBudget -> CekM uni fun s ()
forall a b. (a -> b) -> a -> b
$ Identity ExBudget -> ExBudget
forall a. Identity a -> a
runIdentity (Identity ExBudget -> ExBudget) -> Identity ExBudget -> ExBudget
forall a b. (a -> b) -> a -> b
$ CekMachineCosts -> Identity ExBudget
forall (f :: * -> *). CekMachineCostsBase f -> f ExBudget
cekStartupCost ?cekCosts::CekMachineCosts
CekMachineCosts
?cekCosts
        Context uni fun ann
-> CekValEnv uni fun ann
-> NTerm uni fun ann
-> CekM uni fun s (DischargeResult uni fun)
forall (uni :: * -> *) fun ann s.
(ThrowableBuiltins uni fun, GivenCekReqs uni fun ann s) =>
Context uni fun ann
-> CekValEnv uni fun ann
-> NTerm uni fun ann
-> CekM uni fun s (DischargeResult uni fun)
enterComputeCek Context uni fun ann
forall (uni :: * -> *) fun ann. Context uni fun ann
NoFrame CekValEnv uni fun ann
forall e. RandomAccessList e => e
Env.empty NTerm uni fun ann
term

{- Note [Accumulators for terms]
At a couple of points in the CEK machine (notably building the arguments to a constructor value)
we need to compute a list of terms into values.

Our usual strategy is to make a frame which has an (implicit) "hole" for the value we are computing,
and which stores the other sub-parts of the term as terms or values depending on whether we've computed
them yet or not (see e.g. how applications work).

We want to do the same sort of strategy here, but it's a bit more complicated. We need a hole
"in the middle" of the list, with computed values on one side and yet-to-be-computed terms on the other.
We also very much want to avoid allocating as much as possible.

The basic structure that we end up with has three parts:
1. Use the list of sub-terms from the original term as our "todo" queue, a list is a good structure for this.
2. Use an accumulator type with fast snoc to accumulate the values as we compute them.
3. Convert the accumulator quickly into a final type that is fast to process/lookup in later.

(this process was at one point made explicit with an interface, but in the end we just inlined it all away)

We tried at least three variants of this:
1. List/MutableVector/Vector
2. List/Seq/Seq
3. List/DList/List

Suprisingly, option 3 was just as performant as the others, so we opted to go with it for simplicity.
But there may well be a faster version.
-}