-- | The CEK machine.
-- The CEK machine relies on variables having non-equal 'Unique's whenever they have non-equal
-- string names. I.e. 'Unique's are used instead of string names. This is for efficiency reasons.
-- The CEK machines handles name capture by design.


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

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

module UntypedPlutusCore.Evaluation.Machine.Cek.Internal
    -- See Note [Compilation peculiarities].
    ( EvaluationResult(..)
    , CekValue(..)
    , CekUserError(..)
    , CekEvaluationException
    , CekBudgetSpender(..)
    , ExBudgetInfo(..)
    , ExBudgetMode(..)
    , CekEmitter
    , CekEmitterInfo(..)
    , EmitterMode(..)
    , CekM (..)
    , ErrorWithCause(..)
    , EvaluationError(..)
    , ExBudgetCategory(..)
    , StepKind(..)
    , PrettyUni
    , extractEvaluationResult
    , runCekDeBruijn
    , dischargeCekValue
    )
where

import ErrorCode
import PlutusPrelude

import UntypedPlutusCore.Core


import Data.DeBruijnEnv as Env
import PlutusCore.Builtin
import PlutusCore.DeBruijn
import PlutusCore.Evaluation.Machine.ExBudget
import PlutusCore.Evaluation.Machine.ExMemory
import PlutusCore.Evaluation.Machine.Exception
import PlutusCore.Evaluation.Machine.MachineParameters
import PlutusCore.Evaluation.Result
import PlutusCore.Pretty

import UntypedPlutusCore.Evaluation.Machine.Cek.CekMachineCosts (CekMachineCosts (..))

import Control.Lens.Review
import Control.Monad.Catch
import Control.Monad.Except
import Control.Monad.ST
import Control.Monad.ST.Unsafe
import Data.Array hiding (index)
import Data.DList (DList)
import Data.Hashable (Hashable)
import Data.Kind qualified as GHC
import Data.Semigroup (stimes)
import Data.Text (Text)
import Data.Word
import Data.Word64Array.Word8 hiding (Index)
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 number of the functions 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.
-}

{- Note [Scoping]
The CEK machine does not rely on the global uniqueness condition, so the renamer pass is not a
prerequisite. The CEK machine correctly handles name shadowing.
-}

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

cekStepCost :: CekMachineCosts -> StepKind -> ExBudget
cekStepCost :: CekMachineCosts -> StepKind -> ExBudget
cekStepCost CekMachineCosts
costs = \case
    StepKind
BConst   -> CekMachineCosts -> ExBudget
cekConstCost CekMachineCosts
costs
    StepKind
BVar     -> CekMachineCosts -> ExBudget
cekVarCost CekMachineCosts
costs
    StepKind
BLamAbs  -> CekMachineCosts -> ExBudget
cekLamCost CekMachineCosts
costs
    StepKind
BApply   -> CekMachineCosts -> ExBudget
cekApplyCost CekMachineCosts
costs
    StepKind
BDelay   -> CekMachineCosts -> ExBudget
cekDelayCost CekMachineCosts
costs
    StepKind
BForce   -> CekMachineCosts -> ExBudget
cekForceCost CekMachineCosts
costs
    StepKind
BBuiltin -> CekMachineCosts -> ExBudget
cekBuiltinCost 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
showList :: [ExBudgetCategory fun] -> ShowS
$cshowList :: forall fun. Show fun => [ExBudgetCategory fun] -> ShowS
show :: ExBudgetCategory fun -> String
$cshow :: forall fun. Show fun => ExBudgetCategory fun -> String
showsPrec :: Int -> ExBudgetCategory fun -> ShowS
$cshowsPrec :: forall fun. Show fun => Int -> 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
/= :: ExBudgetCategory fun -> ExBudgetCategory fun -> Bool
$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
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
min :: ExBudgetCategory fun
-> ExBudgetCategory fun -> ExBudgetCategory fun
$cmin :: forall fun.
Ord fun =>
ExBudgetCategory fun
-> ExBudgetCategory fun -> ExBudgetCategory fun
max :: ExBudgetCategory fun
-> ExBudgetCategory fun -> ExBudgetCategory fun
$cmax :: forall fun.
Ord fun =>
ExBudgetCategory fun
-> ExBudgetCategory fun -> ExBudgetCategory fun
>= :: 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
$c< :: forall fun.
Ord fun =>
ExBudgetCategory fun -> ExBudgetCategory fun -> Bool
compare :: ExBudgetCategory fun -> ExBudgetCategory fun -> Ordering
$ccompare :: forall fun.
Ord fun =>
ExBudgetCategory fun -> ExBudgetCategory fun -> Ordering
$cp1Ord :: forall fun. Ord fun => Eq (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
$cto :: forall fun x. Rep (ExBudgetCategory fun) x -> ExBudgetCategory fun
$cfrom :: forall fun x. ExBudgetCategory fun -> Rep (ExBudgetCategory fun) x
Generic)
    deriving anyclass (ExBudgetCategory fun -> ()
(ExBudgetCategory fun -> ()) -> NFData (ExBudgetCategory fun)
forall fun. NFData fun => ExBudgetCategory fun -> ()
forall a. (a -> ()) -> NFData a
rnf :: ExBudgetCategory fun -> ()
$crnf :: forall fun. NFData fun => ExBudgetCategory fun -> ()
NFData, Int -> ExBudgetCategory fun -> Int
ExBudgetCategory fun -> Int
(Int -> ExBudgetCategory fun -> Int)
-> (ExBudgetCategory fun -> Int) -> Hashable (ExBudgetCategory fun)
forall fun. Hashable fun => Int -> ExBudgetCategory fun -> Int
forall fun. Hashable fun => ExBudgetCategory fun -> Int
forall a. (Int -> a -> Int) -> (a -> Int) -> Hashable a
hash :: ExBudgetCategory fun -> Int
$chash :: forall fun. Hashable fun => ExBudgetCategory fun -> Int
hashWithSalt :: Int -> ExBudgetCategory fun -> Int
$chashWithSalt :: forall fun. Hashable fun => Int -> ExBudgetCategory fun -> Int
Hashable)
instance Show fun => Pretty (ExBudgetCategory fun) where
    pretty :: 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)) where
    show :: BuiltinRuntime (CekValue uni fun) -> String
show BuiltinRuntime (CekValue uni fun)
_ = String
"<builtin_runtime>"

-- 'Values' for the modified CEK machine.
data CekValue uni fun =
    -- This bang gave us a 1-2% speed-up at the time of writing.
    VCon !(Some (ValueOf uni))
  | VDelay (Term NamedDeBruijn uni fun ()) !(CekValEnv uni fun)
  | VLamAbs NamedDeBruijn (Term NamedDeBruijn uni fun ()) !(CekValEnv uni fun)
  | VBuiltin            -- A partial builtin application, accumulating arguments for eventual full application.
      !fun                   -- So that we know, for what builtin we're calculating the cost.
                             -- TODO: any chance we could sneak this into 'BuiltinRuntime'
                             -- where we have a partially instantiated costing function anyway?
      (Term NamedDeBruijn uni fun ()) -- This must be lazy. It represents the 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.
      (CekValEnv uni fun)    -- For discharging.
      !(BuiltinRuntime (CekValue uni fun))  -- The partial application and its costing function.
                                            -- Check the docs of 'BuiltinRuntime' for details.
    deriving stock (Int -> CekValue uni fun -> ShowS
[CekValue uni fun] -> ShowS
CekValue uni fun -> String
(Int -> CekValue uni fun -> ShowS)
-> (CekValue uni fun -> String)
-> ([CekValue uni fun] -> ShowS)
-> Show (CekValue uni fun)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall (uni :: * -> *) fun.
(Everywhere uni Show, GShow uni, Closed uni, Show fun) =>
Int -> CekValue uni fun -> ShowS
forall (uni :: * -> *) fun.
(Everywhere uni Show, GShow uni, Closed uni, Show fun) =>
[CekValue uni fun] -> ShowS
forall (uni :: * -> *) fun.
(Everywhere uni Show, GShow uni, Closed uni, Show fun) =>
CekValue uni fun -> String
showList :: [CekValue uni fun] -> ShowS
$cshowList :: forall (uni :: * -> *) fun.
(Everywhere uni Show, GShow uni, Closed uni, Show fun) =>
[CekValue uni fun] -> ShowS
show :: CekValue uni fun -> String
$cshow :: forall (uni :: * -> *) fun.
(Everywhere uni Show, GShow uni, Closed uni, Show fun) =>
CekValue uni fun -> String
showsPrec :: Int -> CekValue uni fun -> ShowS
$cshowsPrec :: forall (uni :: * -> *) fun.
(Everywhere uni Show, GShow uni, Closed uni, Show fun) =>
Int -> CekValue uni fun -> ShowS
Show)

type CekValEnv uni fun = RAList (CekValue uni fun)

-- | 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
    { 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
    { ExBudgetInfo cost uni fun s -> CekBudgetSpender uni fun s
_exBudgetModeSpender       :: !(CekBudgetSpender uni fun s)  -- ^ A spending function.
    , ExBudgetInfo cost uni fun s -> ST s cost
_exBudgetModeGetFinal      :: !(ST s cost) -- ^ For accessing the final state.
    , 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
    { 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 optimized way in a 'WordArray'.
- 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 'WordArray', which is 8 'Word8's packed into a single 'Word64'.
This happens to suit our purposes exactly, as we want to keep a counter for each kind of step
that we know about (of which there are 7) and one for the total number.

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

Why use a 'WordArray'? It optimizes well, since GHC can often do quite a lot of constant-folding
on the bitwise operations that get emitted. We are restricted to counters of size 'Word8', but this
is fine since we will reset when we get to 200 steps.

The sharp-eyed reader might notice that the benchmarks in 'word-array' show that 'PrimArray'
seems to be faster! However, we tried that and it was slower overall, we don't know why.
-}

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/input-output-hk/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 Text -> CekM uni fun s ()

-- | Runtime emitter info, similar to 'ExBudgetInfo'.
data CekEmitterInfo uni fun s = CekEmitterInfo {
    CekEmitterInfo uni fun s -> CekEmitter uni fun s
_cekEmitterInfoEmit       :: CekEmitter 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
    { 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 = (?cekRuntime :: (BuiltinsRuntime fun (CekValue uni fun)))
-- | 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 GivenCekCosts = (?cekCosts :: CekMachineCosts)

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

data CekUserError
    = 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
showList :: [CekUserError] -> ShowS
$cshowList :: [CekUserError] -> ShowS
show :: CekUserError -> String
$cshow :: CekUserError -> String
showsPrec :: Int -> CekUserError -> ShowS
$cshowsPrec :: Int -> CekUserError -> ShowS
Show, CekUserError -> CekUserError -> Bool
(CekUserError -> CekUserError -> Bool)
-> (CekUserError -> CekUserError -> Bool) -> Eq CekUserError
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: CekUserError -> CekUserError -> Bool
$c/= :: CekUserError -> CekUserError -> Bool
== :: CekUserError -> CekUserError -> Bool
$c== :: 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
$cto :: forall x. Rep CekUserError x -> CekUserError
$cfrom :: forall x. CekUserError -> Rep CekUserError x
Generic)
    deriving anyclass (CekUserError -> ()
(CekUserError -> ()) -> NFData CekUserError
forall a. (a -> ()) -> NFData a
rnf :: CekUserError -> ()
$crnf :: CekUserError -> ()
NFData)

instance HasErrorCode CekUserError where
    errorCode :: CekUserError -> ErrorCode
errorCode CekEvaluationFailure {} = Natural -> ErrorCode
ErrorCode Natural
37
    errorCode CekOutOfExError {}      = Natural -> ErrorCode
ErrorCode Natural
36

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
    { CekM uni fun s a -> ST s a
unCekM :: ST s a
    } deriving newtype (a -> CekM uni fun s b -> CekM uni fun s a
(a -> b) -> CekM uni fun s a -> CekM uni fun s b
(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
<$ :: a -> CekM uni fun s b -> CekM uni fun s a
$c<$ :: forall (uni :: * -> *) fun s a b.
a -> CekM uni fun s b -> CekM uni fun s a
fmap :: (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
Functor, Functor (CekM uni fun s)
a -> CekM uni fun s a
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)
CekM uni fun s a -> CekM uni fun s b -> CekM uni fun s b
CekM uni fun s a -> CekM uni fun s b -> CekM uni fun s a
CekM uni fun s (a -> b) -> CekM uni fun s a -> CekM uni fun s b
(a -> b -> c)
-> CekM uni fun s a -> CekM uni fun s b -> CekM uni fun s c
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
<* :: CekM uni fun s a -> CekM uni fun s b -> CekM uni fun s a
$c<* :: forall (uni :: * -> *) fun s a b.
CekM uni fun s a -> CekM uni fun s b -> CekM uni fun s a
*> :: 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 b
liftA2 :: (a -> b -> c)
-> CekM uni fun s a -> CekM uni fun s b -> CekM uni fun s c
$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
<*> :: CekM uni fun s (a -> b) -> CekM uni fun s a -> CekM uni fun s b
$c<*> :: forall (uni :: * -> *) fun s a b.
CekM uni fun s (a -> b) -> CekM uni fun s a -> CekM uni fun s b
pure :: a -> CekM uni fun s a
$cpure :: forall (uni :: * -> *) fun s a. a -> CekM uni fun s a
$cp1Applicative :: forall (uni :: * -> *) fun s. Functor (CekM uni fun s)
Applicative, Applicative (CekM uni fun s)
a -> CekM uni fun s a
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)
CekM uni fun s a -> (a -> CekM uni fun s b) -> CekM uni fun s b
CekM uni fun s a -> CekM uni fun s b -> CekM uni fun s b
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
return :: a -> CekM uni fun s a
$creturn :: forall (uni :: * -> *) fun s a. a -> CekM uni fun s a
>> :: 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 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
$cp1Monad :: forall (uni :: * -> *) fun s. Applicative (CekM uni fun s)
Monad)

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

-- | The set of constraints we need to be able to print things in universes, which we need in order to throw exceptions.
type PrettyUni uni fun = (GShow uni, Closed uni, Pretty fun, Typeable uni, Typeable fun, Everywhere uni PrettyConst)

{- 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
-- 'throwingWithCause' as the cause of the failure.
throwingDischarged
    :: (PrettyUni uni fun)
    => AReview (EvaluationError CekUserError (MachineError fun)) t
    -> t
    -> CekValue uni fun
    -> CekM uni fun s x
throwingDischarged :: AReview (EvaluationError CekUserError (MachineError fun)) t
-> t -> CekValue uni fun -> CekM uni fun s x
throwingDischarged AReview (EvaluationError CekUserError (MachineError fun)) t
l t
t = AReview (EvaluationError CekUserError (MachineError fun)) t
-> t -> Maybe (Term NamedDeBruijn uni fun ()) -> CekM uni fun s x
forall exc e t term (m :: * -> *) x.
(exc ~ ErrorWithCause e term, MonadError exc m) =>
AReview e t -> t -> Maybe term -> m x
throwingWithCause AReview (EvaluationError CekUserError (MachineError fun)) t
l t
t (Maybe (Term NamedDeBruijn uni fun ()) -> CekM uni fun s x)
-> (CekValue uni fun -> Maybe (Term NamedDeBruijn uni fun ()))
-> CekValue uni fun
-> CekM uni fun s x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term NamedDeBruijn uni fun ()
-> Maybe (Term NamedDeBruijn uni fun ())
forall a. a -> Maybe a
Just (Term NamedDeBruijn uni fun ()
 -> Maybe (Term NamedDeBruijn uni fun ()))
-> (CekValue uni fun -> Term NamedDeBruijn uni fun ())
-> CekValue uni fun
-> Maybe (Term NamedDeBruijn uni fun ())
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CekValue uni fun -> Term NamedDeBruijn uni fun ()
forall (uni :: * -> *) fun.
CekValue uni fun -> Term NamedDeBruijn uni fun ()
dischargeCekValue

instance PrettyUni uni fun => MonadError (CekEvaluationException NamedDeBruijn uni fun) (CekM uni fun s) where
    -- See Note [Throwing exceptions in ST].
    throwError :: 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 (m :: * -> *) e a. (MonadThrow m, Exception e) => e -> m a
throwM

    -- See Note [Catching exceptions in ST].
    CekM uni fun s a
a catchError :: 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 = 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
-> (CekEvaluationException NamedDeBruijn uni fun -> IO a) -> IO a
forall (m :: * -> *) e a.
(MonadCatch m, Exception e) =>
m a -> (e -> m a) -> m a
`catch` CekEvaluationException NamedDeBruijn uni fun -> IO a
hIO where
        aIO :: IO a
aIO = CekM uni fun s a -> IO a
forall a. 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
forall a. 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

-- It would be really nice to define this instance, so that we can use 'makeKnown' directly in
-- the 'CekM' monad without the 'WithEmitterT' nonsense. Unfortunately, GHC doesn't like
-- implicit params in instance contexts. As GHC's docs explain:
--
-- > Reason: exactly which implicit parameter you pick up depends on exactly where you invoke a
-- > function. But the "invocation" of instance declarations is done behind the scenes by the
-- > compiler, so it's hard to figure out exactly where it is done. The easiest thing is to outlaw
-- > the offending types.
-- instance GivenCekEmitter s => MonadEmitter (CekM uni fun s) where
--     emit = emitCek

instance AsEvaluationFailure CekUserError where
    _EvaluationFailure :: p () (f ()) -> p CekUserError (f CekUserError)
_EvaluationFailure = CekUserError -> Prism' CekUserError ()
forall err. Eq err => err -> Prism' err ()
_EvaluationFailureVia CekUserError
CekEvaluationFailure

instance Pretty CekUserError where
    pretty :: CekUserError -> Doc ann
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
pretty ExBudget
res
          , Doc ann
"Negative numbers indicate the overspent budget; note that this only indicatessthe 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'."

spendBudgetCek :: GivenCekSpender uni fun s => ExBudgetCategory fun -> ExBudget -> CekM uni fun s ()
spendBudgetCek :: ExBudgetCategory fun -> ExBudget -> CekM uni fun s ()
spendBudgetCek = let (CekBudgetSpender ExBudgetCategory fun -> ExBudget -> CekM uni fun s ()
spend) = ?cekBudgetSpender::CekBudgetSpender uni fun s
CekBudgetSpender uni fun s
?cekBudgetSpender in ExBudgetCategory fun -> ExBudget -> CekM uni fun s ()
spend

-- see Note [Scoping].
-- | Instantiate all the free variables of a term by looking them up in an environment.
-- Mutually recursive with dischargeCekVal.
dischargeCekValEnv :: forall uni fun. CekValEnv uni fun -> Term NamedDeBruijn uni fun () -> Term NamedDeBruijn uni fun ()
dischargeCekValEnv :: CekValEnv uni fun
-> Term NamedDeBruijn uni fun () -> Term NamedDeBruijn uni fun ()
dischargeCekValEnv CekValEnv uni fun
valEnv = Word64
-> Term NamedDeBruijn uni fun () -> Term NamedDeBruijn uni fun ()
go Word64
0
 where
  -- The lamCnt is just a counter that measures how many lambda-abstractions
  -- we have descended in the `go` loop.
  go :: Word64 -> Term NamedDeBruijn uni fun () -> Term NamedDeBruijn uni fun ()
  go :: Word64
-> Term NamedDeBruijn uni fun () -> Term NamedDeBruijn uni fun ()
go !Word64
lamCnt =  \case
    LamAbs ()
ann NamedDeBruijn
name Term NamedDeBruijn uni fun ()
body -> ()
-> NamedDeBruijn
-> Term NamedDeBruijn uni fun ()
-> Term NamedDeBruijn uni fun ()
forall name (uni :: * -> *) fun ann.
ann -> name -> Term name uni fun ann -> Term name uni fun ann
LamAbs ()
ann NamedDeBruijn
name (Term NamedDeBruijn uni fun () -> Term NamedDeBruijn uni fun ())
-> Term NamedDeBruijn uni fun () -> Term NamedDeBruijn uni fun ()
forall a b. (a -> b) -> a -> b
$ Word64
-> Term NamedDeBruijn uni fun () -> Term NamedDeBruijn uni fun ()
go (Word64
lamCntWord64 -> Word64 -> Word64
forall a. Num a => a -> a -> a
+Word64
1) Term NamedDeBruijn uni fun ()
body
    var :: Term NamedDeBruijn uni fun ()
var@(Var ()
_ (NamedDeBruijn Text
_ Index
ndbnIx)) -> let ix :: Word64
ix = Index -> Word64
coerce Index
ndbnIx :: Word64  in
        if Word64
lamCnt Word64 -> Word64 -> Bool
forall a. Ord a => a -> a -> Bool
>= Word64
ix
        -- 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 Term NamedDeBruijn uni fun ()
var
        else Term NamedDeBruijn uni fun ()
-> (CekValue uni fun -> Term NamedDeBruijn uni fun ())
-> Maybe (CekValue uni fun)
-> Term NamedDeBruijn uni fun ()
forall b a. b -> (a -> b) -> Maybe a -> b
maybe
               -- var is free, leave it alone
               Term NamedDeBruijn uni fun ()
var
               -- var is in the env, discharge its value
               CekValue uni fun -> Term NamedDeBruijn uni fun ()
forall (uni :: * -> *) fun.
CekValue uni fun -> Term NamedDeBruijn uni fun ()
dischargeCekValue
               -- index relative to (as seen from the point of view of) the environment
               (CekValEnv uni fun -> Word64 -> Maybe (Element (CekValEnv uni fun))
forall e. DeBruijnEnv e => e -> Word64 -> Maybe (Element e)
Env.index CekValEnv uni fun
valEnv (Word64 -> Maybe (Element (CekValEnv uni fun)))
-> Word64 -> Maybe (Element (CekValEnv uni fun))
forall a b. (a -> b) -> a -> b
$ Word64
ix Word64 -> Word64 -> Word64
forall a. Num a => a -> a -> a
- Word64
lamCnt)
    Apply ()
ann Term NamedDeBruijn uni fun ()
fun Term NamedDeBruijn uni fun ()
arg    -> ()
-> 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 ()
ann (Word64
-> Term NamedDeBruijn uni fun () -> Term NamedDeBruijn uni fun ()
go Word64
lamCnt Term NamedDeBruijn uni fun ()
fun) (Term NamedDeBruijn uni fun () -> Term NamedDeBruijn uni fun ())
-> Term NamedDeBruijn uni fun () -> Term NamedDeBruijn uni fun ()
forall a b. (a -> b) -> a -> b
$ Word64
-> Term NamedDeBruijn uni fun () -> Term NamedDeBruijn uni fun ()
go Word64
lamCnt Term NamedDeBruijn uni fun ()
arg
    Delay ()
ann 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
Delay ()
ann (Term NamedDeBruijn uni fun () -> Term NamedDeBruijn uni fun ())
-> Term NamedDeBruijn uni fun () -> Term NamedDeBruijn uni fun ()
forall a b. (a -> b) -> a -> b
$ Word64
-> Term NamedDeBruijn uni fun () -> Term NamedDeBruijn uni fun ()
go Word64
lamCnt Term NamedDeBruijn uni fun ()
term
    Force ()
ann 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 ()
ann (Term NamedDeBruijn uni fun () -> Term NamedDeBruijn uni fun ())
-> Term NamedDeBruijn uni fun () -> Term NamedDeBruijn uni fun ()
forall a b. (a -> b) -> a -> b
$ Word64
-> Term NamedDeBruijn uni fun () -> Term NamedDeBruijn uni fun ()
go Word64
lamCnt Term NamedDeBruijn uni fun ()
term
    Term NamedDeBruijn uni fun ()
t -> Term NamedDeBruijn uni fun ()
t

-- | Convert a 'CekValue' into a 'Term' by replacing all bound variables with the terms
-- they're bound to (which themselves have to be obtain by recursively discharging values).
dischargeCekValue :: CekValue uni fun -> Term NamedDeBruijn uni fun ()
dischargeCekValue :: CekValue uni fun -> Term NamedDeBruijn uni fun ()
dischargeCekValue = \case
    VCon     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
    VDelay   Term NamedDeBruijn uni fun ()
body CekValEnv uni fun
env                    -> CekValEnv uni fun
-> Term NamedDeBruijn uni fun () -> Term NamedDeBruijn uni fun ()
forall (uni :: * -> *) fun.
CekValEnv uni fun
-> Term NamedDeBruijn uni fun () -> Term NamedDeBruijn uni fun ()
dischargeCekValEnv CekValEnv uni fun
env (Term NamedDeBruijn uni fun () -> Term NamedDeBruijn uni fun ())
-> Term NamedDeBruijn uni fun () -> Term NamedDeBruijn uni fun ()
forall a b. (a -> b) -> a -> b
$ ()
-> Term NamedDeBruijn uni fun () -> Term NamedDeBruijn uni fun ()
forall name (uni :: * -> *) fun ann.
ann -> Term name uni fun ann -> Term name uni fun ann
Delay () Term NamedDeBruijn uni fun ()
body
    -- 'computeCek' turns @LamAbs _ name body@ into @VLamAbs name body env@ where @env@ is an
    -- argument of 'computeCek' and hence we need to start discharging outside of the reassembled
    -- lambda, otherwise @name@ could clash with the names that we have in @env@.
    VLamAbs (NamedDeBruijn Text
n Index
_ix) Term NamedDeBruijn uni fun ()
body CekValEnv uni fun
env ->
        -- The index on the binder is meaningless, we put `0` by convention, see 'Binder'.
        CekValEnv uni fun
-> Term NamedDeBruijn uni fun () -> Term NamedDeBruijn uni fun ()
forall (uni :: * -> *) fun.
CekValEnv uni fun
-> Term NamedDeBruijn uni fun () -> Term NamedDeBruijn uni fun ()
dischargeCekValEnv CekValEnv uni fun
env (Term NamedDeBruijn uni fun () -> Term NamedDeBruijn uni fun ())
-> Term NamedDeBruijn uni fun () -> Term NamedDeBruijn uni fun ()
forall a b. (a -> b) -> a -> b
$ ()
-> NamedDeBruijn
-> Term NamedDeBruijn uni fun ()
-> Term NamedDeBruijn 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) Term NamedDeBruijn uni fun ()
body
    -- We only discharge a value when (a) it's being returned by the machine,
    -- or (b) it's needed for an error message.
    VBuiltin fun
_ Term NamedDeBruijn uni fun ()
term CekValEnv uni fun
env BuiltinRuntime (CekValue uni fun)
_                -> CekValEnv uni fun
-> Term NamedDeBruijn uni fun () -> Term NamedDeBruijn uni fun ()
forall (uni :: * -> *) fun.
CekValEnv uni fun
-> Term NamedDeBruijn uni fun () -> Term NamedDeBruijn uni fun ()
dischargeCekValEnv CekValEnv uni fun
env Term NamedDeBruijn uni fun ()
term

instance (Closed uni, GShow uni, uni `Everywhere` PrettyConst, Pretty fun) =>
            PrettyBy PrettyConfigPlc (CekValue uni fun) where
    prettyBy :: PrettyConfigPlc -> CekValue uni fun -> Doc ann
prettyBy PrettyConfigPlc
cfg = PrettyConfigPlc -> Term NamedDeBruijn uni fun () -> Doc ann
forall config a ann. PrettyBy config a => config -> a -> Doc ann
prettyBy PrettyConfigPlc
cfg (Term NamedDeBruijn uni fun () -> Doc ann)
-> (CekValue uni fun -> Term NamedDeBruijn uni fun ())
-> CekValue uni fun
-> Doc ann
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CekValue uni fun -> Term NamedDeBruijn uni fun ()
forall (uni :: * -> *) fun.
CekValue uni fun -> Term NamedDeBruijn uni fun ()
dischargeCekValue

type instance UniOf (CekValue uni fun) = uni

instance HasConstant (CekValue uni fun) where
    asConstant :: Maybe cause
-> CekValue uni fun
-> Either
     (ErrorWithCause err cause)
     (Some (ValueOf (UniOf (CekValue uni fun))))
asConstant Maybe cause
_        (VCon Some (ValueOf uni)
val) = Some (ValueOf uni)
-> Either (ErrorWithCause err cause) (Some (ValueOf uni))
forall (f :: * -> *) a. Applicative f => a -> f a
pure Some (ValueOf uni)
val
    asConstant Maybe cause
mayCause CekValue uni fun
_          = Maybe cause
-> Either (ErrorWithCause err cause) (Some (ValueOf uni))
forall err cause (m :: * -> *) r.
(MonadError (ErrorWithCause err cause) m, AsUnliftingError err) =>
Maybe cause -> m r
throwNotAConstant Maybe cause
mayCause

    fromConstant :: Some (ValueOf (UniOf (CekValue uni fun))) -> CekValue uni fun
fromConstant = Some (ValueOf (UniOf (CekValue uni fun))) -> CekValue uni fun
forall (uni :: * -> *) fun. Some (ValueOf uni) -> CekValue uni fun
VCon

{-|
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
    = FrameApplyFun !(CekValue uni fun) !(Context uni fun)                         -- ^ @[V _]@
    | FrameApplyArg !(CekValEnv uni fun) (Term NamedDeBruijn uni fun ()) !(Context uni fun) -- ^ @[_ N]@
    | FrameForce !(Context uni fun)                                               -- ^ @(force _)@
    | NoFrame
    deriving stock (Int -> Context uni fun -> ShowS
[Context uni fun] -> ShowS
Context uni fun -> String
(Int -> Context uni fun -> ShowS)
-> (Context uni fun -> String)
-> ([Context uni fun] -> ShowS)
-> Show (Context uni fun)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall (uni :: * -> *) fun.
(Everywhere uni Show, GShow uni, Closed uni, Show fun) =>
Int -> Context uni fun -> ShowS
forall (uni :: * -> *) fun.
(Everywhere uni Show, GShow uni, Closed uni, Show fun) =>
[Context uni fun] -> ShowS
forall (uni :: * -> *) fun.
(Everywhere uni Show, GShow uni, Closed uni, Show fun) =>
Context uni fun -> String
showList :: [Context uni fun] -> ShowS
$cshowList :: forall (uni :: * -> *) fun.
(Everywhere uni Show, GShow uni, Closed uni, Show fun) =>
[Context uni fun] -> ShowS
show :: Context uni fun -> String
$cshow :: forall (uni :: * -> *) fun.
(Everywhere uni Show, GShow uni, Closed uni, Show fun) =>
Context uni fun -> String
showsPrec :: Int -> Context uni fun -> ShowS
$cshowsPrec :: forall (uni :: * -> *) fun.
(Everywhere uni Show, GShow uni, Closed uni, Show fun) =>
Int -> Context uni fun -> ShowS
Show)

toExMemory :: (Closed uni, uni `Everywhere` ExMemoryUsage) => CekValue uni fun -> ExMemory
toExMemory :: CekValue uni fun -> ExMemory
toExMemory = \case
    VCon Some (ValueOf uni)
c      -> Some (ValueOf uni) -> ExMemory
forall a. ExMemoryUsage a => a -> ExMemory
memoryUsage Some (ValueOf uni)
c
    VDelay {}   -> ExMemory
1
    VLamAbs {}  -> ExMemory
1
    VBuiltin {} -> ExMemory
1
{-# INLINE toExMemory #-}  -- It probably gets inlined anyway, but an explicit pragma
                           -- shouldn't hurt.

-- | A 'MonadError' version of 'try'.
tryError :: MonadError e m => m a -> m (Either e a)
tryError :: m a -> m (Either e a)
tryError m a
a = (a -> Either e a
forall a b. b -> Either a b
Right (a -> Either e a) -> m a -> m (Either e a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m a
a) m (Either e a) -> (e -> m (Either e a)) -> m (Either e a)
forall e (m :: * -> *) a.
MonadError e m =>
m a -> (e -> m a) -> m a
`catchError` (Either e a -> m (Either e a)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Either e a -> m (Either e a))
-> (e -> Either e a) -> e -> m (Either e a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. e -> Either e a
forall a b. a -> Either a b
Left)

runCekM
    :: forall a cost uni fun.
    (PrettyUni uni fun)
    => MachineParameters CekMachineCosts CekValue uni fun
    -> ExBudgetMode cost uni fun
    -> EmitterMode uni fun
    -> (forall s. GivenCekReqs uni fun s => CekM uni fun s a)
    -> (Either (CekEvaluationException NamedDeBruijn uni fun) a, cost, [Text])
runCekM :: MachineParameters CekMachineCosts CekValue uni fun
-> ExBudgetMode cost uni fun
-> EmitterMode uni fun
-> (forall s. GivenCekReqs uni fun s => CekM uni fun s a)
-> (Either (CekEvaluationException NamedDeBruijn uni fun) a, cost,
    [Text])
runCekM (MachineParameters CekMachineCosts
costs BuiltinsRuntime fun (CekValue uni fun)
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 s => CekM uni fun s a
a = (forall s.
 ST
   s
   (Either (CekEvaluationException NamedDeBruijn uni fun) a, cost,
    [Text]))
-> (Either (CekEvaluationException NamedDeBruijn uni fun) a, cost,
    [Text])
forall a. (forall s. ST s a) -> a
runST ((forall s.
  ST
    s
    (Either (CekEvaluationException NamedDeBruijn uni fun) a, cost,
     [Text]))
 -> (Either (CekEvaluationException NamedDeBruijn uni fun) a, cost,
     [Text]))
-> (forall s.
    ST
      s
      (Either (CekEvaluationException NamedDeBruijn uni fun) a, cost,
       [Text]))
-> (Either (CekEvaluationException NamedDeBruijn uni fun) a, cost,
    [Text])
forall a b. (a -> b) -> a -> b
$ do
    ExBudgetInfo{CekBudgetSpender uni fun s
_exBudgetModeSpender :: CekBudgetSpender uni fun s
_exBudgetModeSpender :: forall cost (uni :: * -> *) fun s.
ExBudgetInfo cost uni fun s -> CekBudgetSpender uni fun s
_exBudgetModeSpender, ST s cost
_exBudgetModeGetFinal :: ST s cost
_exBudgetModeGetFinal :: forall cost (uni :: * -> *) fun s.
ExBudgetInfo cost uni fun s -> ST s cost
_exBudgetModeGetFinal, ST s ExBudget
_exBudgetModeGetCumulative :: ST s ExBudget
_exBudgetModeGetCumulative :: forall cost (uni :: * -> *) fun s.
ExBudgetInfo cost uni fun s -> 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 :: CekEmitter uni fun s
_cekEmitterInfoEmit :: forall (uni :: * -> *) fun s.
CekEmitterInfo uni fun s -> CekEmitter uni fun s
_cekEmitterInfoEmit, ST s [Text]
_cekEmitterInfoGetFinal :: ST s [Text]
_cekEmitterInfoGetFinal :: forall (uni :: * -> *) fun s.
CekEmitterInfo uni fun s -> 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
    let ?cekRuntime = runtime
        ?cekEmitter = _cekEmitterInfoEmit
        ?cekBudgetSpender = _exBudgetModeSpender
        ?cekCosts = costs
        ?cekSlippage = defaultSlippage
    Either (CekEvaluationException NamedDeBruijn uni fun) a
errOrRes <- CekM
  uni fun s (Either (CekEvaluationException NamedDeBruijn uni fun) a)
-> ST s (Either (CekEvaluationException NamedDeBruijn uni fun) a)
forall (uni :: * -> *) fun s a. CekM uni fun s a -> ST s a
unCekM (CekM
   uni fun s (Either (CekEvaluationException NamedDeBruijn uni fun) a)
 -> ST s (Either (CekEvaluationException NamedDeBruijn uni fun) a))
-> CekM
     uni fun s (Either (CekEvaluationException NamedDeBruijn uni fun) a)
-> ST s (Either (CekEvaluationException NamedDeBruijn uni fun) a)
forall a b. (a -> b) -> a -> b
$ CekM uni fun s a
-> CekM
     uni fun s (Either (CekEvaluationException NamedDeBruijn uni fun) a)
forall e (m :: * -> *) a. MonadError e m => m a -> m (Either e a)
tryError CekM uni fun s a
forall s. GivenCekReqs uni fun s => CekM uni fun s a
a
    cost
st <- ST s cost
_exBudgetModeGetFinal
    [Text]
logs <- ST s [Text]
_cekEmitterInfoGetFinal
    (Either (CekEvaluationException NamedDeBruijn uni fun) a, cost,
 [Text])
-> ST
     s
     (Either (CekEvaluationException NamedDeBruijn uni fun) a, cost,
      [Text])
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Either (CekEvaluationException NamedDeBruijn uni fun) a
errOrRes, cost
st, [Text]
logs)

-- | Look up a variable name in the environment.
lookupVarName :: forall uni fun s . (PrettyUni uni fun) => NamedDeBruijn -> CekValEnv uni fun -> CekM uni fun s (CekValue uni fun)
lookupVarName :: NamedDeBruijn
-> CekValEnv uni fun -> CekM uni fun s (CekValue uni fun)
lookupVarName varName :: NamedDeBruijn
varName@(NamedDeBruijn Text
_ Index
varIx) CekValEnv uni fun
varEnv =
    case CekValEnv uni fun
varEnv CekValEnv uni fun -> Word64 -> Maybe (Element (CekValEnv uni fun))
forall e. DeBruijnEnv e => e -> Word64 -> Maybe (Element e)
`Env.index` Index -> Word64
coerce Index
varIx of
        Maybe (Element (CekValEnv uni fun))
Nothing  -> AReview
  (EvaluationError CekUserError (MachineError fun))
  (MachineError fun)
-> MachineError fun
-> Maybe (Term NamedDeBruijn uni fun ())
-> CekM uni fun s (CekValue uni fun)
forall exc e t term (m :: * -> *) x.
(exc ~ ErrorWithCause e term, MonadError exc m) =>
AReview e t -> t -> Maybe term -> m x
throwingWithCause AReview
  (EvaluationError CekUserError (MachineError fun))
  (MachineError fun)
forall r fun. AsMachineError r fun => Prism' r (MachineError fun)
_MachineError MachineError fun
forall fun. MachineError fun
OpenTermEvaluatedMachineError (Maybe (Term NamedDeBruijn uni fun ())
 -> CekM uni fun s (CekValue uni fun))
-> Maybe (Term NamedDeBruijn uni fun ())
-> CekM uni fun s (CekValue uni fun)
forall a b. (a -> b) -> a -> b
$ Term NamedDeBruijn uni fun ()
-> Maybe (Term NamedDeBruijn uni fun ())
forall a. a -> Maybe a
Just Term NamedDeBruijn uni fun ()
var where
            var :: Term NamedDeBruijn uni fun ()
var = () -> NamedDeBruijn -> Term NamedDeBruijn uni fun ()
forall name (uni :: * -> *) fun ann.
ann -> name -> Term name uni fun ann
Var () NamedDeBruijn
varName
        Just Element (CekValEnv uni fun)
val -> CekValue uni fun -> CekM uni fun s (CekValue uni fun)
forall (f :: * -> *) a. Applicative f => a -> f a
pure Element (CekValEnv uni fun)
CekValue uni fun
val

-- | Take pieces of a possibly partial builtin application and either create a 'CekValue' using
-- 'makeKnown' or a partial builtin application depending on whether the built-in function is
-- fully saturated or not.
evalBuiltinApp
    :: (GivenCekReqs uni fun s, PrettyUni uni fun)
    => fun
    -> Term NamedDeBruijn uni fun ()
    -> CekValEnv uni fun
    -> BuiltinRuntime (CekValue uni fun)
    -> CekM uni fun s (CekValue uni fun)
evalBuiltinApp :: fun
-> Term NamedDeBruijn uni fun ()
-> CekValEnv uni fun
-> BuiltinRuntime (CekValue uni fun)
-> CekM uni fun s (CekValue uni fun)
evalBuiltinApp fun
fun Term NamedDeBruijn uni fun ()
term CekValEnv uni fun
env runtime :: BuiltinRuntime (CekValue uni fun)
runtime@(BuiltinRuntime RuntimeScheme n
sch ToRuntimeDenotationType (CekValue uni fun) n
getX ToCostingType n
cost) = case RuntimeScheme n
sch of
    RuntimeScheme n
RuntimeSchemeResult -> do
        ExBudgetCategory fun -> ExBudget -> CekM uni fun s ()
forall (uni :: * -> *) fun s.
GivenCekSpender uni fun s =>
ExBudgetCategory fun -> ExBudget -> CekM uni fun s ()
spendBudgetCek (fun -> ExBudgetCategory fun
forall fun. fun -> ExBudgetCategory fun
BBuiltinApp fun
fun) ExBudget
ToCostingType n
cost
        let !(Either (ErrorWithCause KnownTypeError ()) (CekValue uni fun)
errOrRes, DList Text
logs) = Emitter
  (Either (ErrorWithCause KnownTypeError ()) (CekValue uni fun))
-> (Either (ErrorWithCause KnownTypeError ()) (CekValue uni fun),
    DList Text)
forall a. Emitter a -> (a, DList Text)
runEmitter (Emitter
   (Either (ErrorWithCause KnownTypeError ()) (CekValue uni fun))
 -> (Either (ErrorWithCause KnownTypeError ()) (CekValue uni fun),
     DList Text))
-> Emitter
     (Either (ErrorWithCause KnownTypeError ()) (CekValue uni fun))
-> (Either (ErrorWithCause KnownTypeError ()) (CekValue uni fun),
    DList Text)
forall a b. (a -> b) -> a -> b
$ ExceptT
  (ErrorWithCause KnownTypeError ()) Emitter (CekValue uni fun)
-> Emitter
     (Either (ErrorWithCause KnownTypeError ()) (CekValue uni fun))
forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
runExceptT ExceptT
  (ErrorWithCause KnownTypeError ()) Emitter (CekValue uni fun)
ToRuntimeDenotationType (CekValue uni fun) n
getX
        ?cekEmitter::DList Text -> CekM uni fun s ()
DList Text -> CekM uni fun s ()
?cekEmitter DList Text
logs
        case Either (ErrorWithCause KnownTypeError ()) (CekValue uni fun)
errOrRes of
            Left ErrorWithCause KnownTypeError ()
err  -> ErrorWithCause KnownTypeError (Term NamedDeBruijn uni fun ())
-> CekM uni fun s (CekValue uni fun)
forall err cause (m :: * -> *) void.
(MonadError (ErrorWithCause err cause) m, AsUnliftingError err,
 AsEvaluationFailure err) =>
ErrorWithCause KnownTypeError cause -> m void
throwKnownTypeErrorWithCause (ErrorWithCause KnownTypeError (Term NamedDeBruijn uni fun ())
 -> CekM uni fun s (CekValue uni fun))
-> ErrorWithCause KnownTypeError (Term NamedDeBruijn uni fun ())
-> CekM uni fun s (CekValue uni fun)
forall a b. (a -> b) -> a -> b
$ Term NamedDeBruijn uni fun ()
term Term NamedDeBruijn uni fun ()
-> ErrorWithCause KnownTypeError ()
-> ErrorWithCause KnownTypeError (Term NamedDeBruijn uni fun ())
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ ErrorWithCause KnownTypeError ()
err
            Right CekValue uni fun
res -> CekValue uni fun -> CekM uni fun s (CekValue uni fun)
forall (f :: * -> *) a. Applicative f => a -> f a
pure CekValue uni fun
res
    RuntimeScheme n
_ -> CekValue uni fun -> CekM uni fun s (CekValue uni fun)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (CekValue uni fun -> CekM uni fun s (CekValue uni fun))
-> CekValue uni fun -> CekM uni fun s (CekValue uni fun)
forall a b. (a -> b) -> a -> b
$ fun
-> Term NamedDeBruijn uni fun ()
-> CekValEnv uni fun
-> BuiltinRuntime (CekValue uni fun)
-> CekValue uni fun
forall (uni :: * -> *) fun.
fun
-> Term NamedDeBruijn uni fun ()
-> CekValEnv uni fun
-> BuiltinRuntime (CekValue uni fun)
-> CekValue uni fun
VBuiltin fun
fun Term NamedDeBruijn uni fun ()
term CekValEnv uni fun
env BuiltinRuntime (CekValue uni fun)
runtime
{-# INLINE evalBuiltinApp #-}

-- See Note [Compilation peculiarities].
-- | The entering point to the CEK machine's engine.
enterComputeCek
    :: forall uni fun s
    . (Ix fun, PrettyUni uni fun, GivenCekReqs uni fun s, uni `Everywhere` ExMemoryUsage)
    => Context uni fun
    -> CekValEnv uni fun
    -> Term NamedDeBruijn uni fun ()
    -> CekM uni fun s (Term NamedDeBruijn uni fun ())
enterComputeCek :: Context uni fun
-> CekValEnv uni fun
-> Term NamedDeBruijn uni fun ()
-> CekM uni fun s (Term NamedDeBruijn uni fun ())
enterComputeCek = WordArray
-> Context uni fun
-> CekValEnv uni fun
-> Term NamedDeBruijn uni fun ()
-> CekM uni fun s (Term NamedDeBruijn uni fun ())
computeCek (Word64 -> WordArray
toWordArray Word64
0) 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
        :: WordArray
        -> Context uni fun
        -> CekValEnv uni fun
        -> Term NamedDeBruijn uni fun ()
        -> CekM uni fun s (Term NamedDeBruijn uni fun ())
    -- s ; ρ ▻ {L A}  ↦ s , {_ A} ; ρ ▻ L
    computeCek :: WordArray
-> Context uni fun
-> CekValEnv uni fun
-> Term NamedDeBruijn uni fun ()
-> CekM uni fun s (Term NamedDeBruijn uni fun ())
computeCek !WordArray
unbudgetedSteps !Context uni fun
ctx !CekValEnv uni fun
env (Var ()
_ NamedDeBruijn
varName) = do
        !WordArray
unbudgetedSteps' <- StepKind -> WordArray -> CekM uni fun s WordArray
stepAndMaybeSpend StepKind
BVar WordArray
unbudgetedSteps
        CekValue uni fun
val <- NamedDeBruijn
-> CekValEnv uni fun -> CekM uni fun s (CekValue uni fun)
forall (uni :: * -> *) fun s.
PrettyUni uni fun =>
NamedDeBruijn
-> CekValEnv uni fun -> CekM uni fun s (CekValue uni fun)
lookupVarName NamedDeBruijn
varName CekValEnv uni fun
env
        WordArray
-> Context uni fun
-> CekValue uni fun
-> CekM uni fun s (Term NamedDeBruijn uni fun ())
returnCek WordArray
unbudgetedSteps' Context uni fun
ctx CekValue uni fun
val
    computeCek !WordArray
unbudgetedSteps !Context uni fun
ctx !CekValEnv uni fun
_ (Constant ()
_ Some (ValueOf uni)
val) = do
        !WordArray
unbudgetedSteps' <- StepKind -> WordArray -> CekM uni fun s WordArray
stepAndMaybeSpend StepKind
BConst WordArray
unbudgetedSteps
        WordArray
-> Context uni fun
-> CekValue uni fun
-> CekM uni fun s (Term NamedDeBruijn uni fun ())
returnCek WordArray
unbudgetedSteps' Context uni fun
ctx (Some (ValueOf uni) -> CekValue uni fun
forall (uni :: * -> *) fun. Some (ValueOf uni) -> CekValue uni fun
VCon Some (ValueOf uni)
val)
    computeCek !WordArray
unbudgetedSteps !Context uni fun
ctx !CekValEnv uni fun
env (LamAbs ()
_ NamedDeBruijn
name Term NamedDeBruijn uni fun ()
body) = do
        !WordArray
unbudgetedSteps' <- StepKind -> WordArray -> CekM uni fun s WordArray
stepAndMaybeSpend StepKind
BLamAbs WordArray
unbudgetedSteps
        WordArray
-> Context uni fun
-> CekValue uni fun
-> CekM uni fun s (Term NamedDeBruijn uni fun ())
returnCek WordArray
unbudgetedSteps' Context uni fun
ctx (NamedDeBruijn
-> Term NamedDeBruijn uni fun ()
-> CekValEnv uni fun
-> CekValue uni fun
forall (uni :: * -> *) fun.
NamedDeBruijn
-> Term NamedDeBruijn uni fun ()
-> CekValEnv uni fun
-> CekValue uni fun
VLamAbs NamedDeBruijn
name Term NamedDeBruijn uni fun ()
body CekValEnv uni fun
env)
    computeCek !WordArray
unbudgetedSteps !Context uni fun
ctx !CekValEnv uni fun
env (Delay ()
_ Term NamedDeBruijn uni fun ()
body) = do
        !WordArray
unbudgetedSteps' <- StepKind -> WordArray -> CekM uni fun s WordArray
stepAndMaybeSpend StepKind
BDelay WordArray
unbudgetedSteps
        WordArray
-> Context uni fun
-> CekValue uni fun
-> CekM uni fun s (Term NamedDeBruijn uni fun ())
returnCek WordArray
unbudgetedSteps' Context uni fun
ctx (Term NamedDeBruijn uni fun ()
-> CekValEnv uni fun -> CekValue uni fun
forall (uni :: * -> *) fun.
Term NamedDeBruijn uni fun ()
-> CekValEnv uni fun -> CekValue uni fun
VDelay Term NamedDeBruijn uni fun ()
body CekValEnv uni fun
env)
    -- s ; ρ ▻ lam x L  ↦  s ◅ lam x (L , ρ)
    computeCek !WordArray
unbudgetedSteps !Context uni fun
ctx !CekValEnv uni fun
env (Force ()
_ Term NamedDeBruijn uni fun ()
body) = do
        !WordArray
unbudgetedSteps' <- StepKind -> WordArray -> CekM uni fun s WordArray
stepAndMaybeSpend StepKind
BForce WordArray
unbudgetedSteps
        WordArray
-> Context uni fun
-> CekValEnv uni fun
-> Term NamedDeBruijn uni fun ()
-> CekM uni fun s (Term NamedDeBruijn uni fun ())
computeCek WordArray
unbudgetedSteps' (Context uni fun -> Context uni fun
forall (uni :: * -> *) fun. Context uni fun -> Context uni fun
FrameForce Context uni fun
ctx) CekValEnv uni fun
env Term NamedDeBruijn uni fun ()
body
    -- s ; ρ ▻ [L M]  ↦  s , [_ (M,ρ)]  ; ρ ▻ L
    computeCek !WordArray
unbudgetedSteps !Context uni fun
ctx !CekValEnv uni fun
env (Apply ()
_ Term NamedDeBruijn uni fun ()
fun Term NamedDeBruijn uni fun ()
arg) = do
        !WordArray
unbudgetedSteps' <- StepKind -> WordArray -> CekM uni fun s WordArray
stepAndMaybeSpend StepKind
BApply WordArray
unbudgetedSteps
        WordArray
-> Context uni fun
-> CekValEnv uni fun
-> Term NamedDeBruijn uni fun ()
-> CekM uni fun s (Term NamedDeBruijn uni fun ())
computeCek WordArray
unbudgetedSteps' (CekValEnv uni fun
-> Term NamedDeBruijn uni fun ()
-> Context uni fun
-> Context uni fun
forall (uni :: * -> *) fun.
CekValEnv uni fun
-> Term NamedDeBruijn uni fun ()
-> Context uni fun
-> Context uni fun
FrameApplyArg CekValEnv uni fun
env Term NamedDeBruijn uni fun ()
arg Context uni fun
ctx) CekValEnv uni fun
env Term NamedDeBruijn uni fun ()
fun
    -- s ; ρ ▻ abs α L  ↦  s ◅ abs α (L , ρ)
    -- s ; ρ ▻ con c  ↦  s ◅ con c
    -- s ; ρ ▻ builtin bn  ↦  s ◅ builtin bn arity arity [] [] ρ
    computeCek !WordArray
unbudgetedSteps !Context uni fun
ctx !CekValEnv uni fun
env term :: Term NamedDeBruijn uni fun ()
term@(Builtin ()
_ fun
bn) = do
        !WordArray
unbudgetedSteps' <- StepKind -> WordArray -> CekM uni fun s WordArray
stepAndMaybeSpend StepKind
BBuiltin WordArray
unbudgetedSteps
        BuiltinRuntime (CekValue uni fun)
meaning <- fun
-> BuiltinsRuntime fun (CekValue uni fun)
-> CekM uni fun s (BuiltinRuntime (CekValue uni fun))
forall err cause (m :: * -> *) fun val.
(MonadError (ErrorWithCause err cause) m, AsMachineError err fun,
 Ix fun) =>
fun -> BuiltinsRuntime fun val -> m (BuiltinRuntime val)
lookupBuiltin fun
bn ?cekRuntime::BuiltinsRuntime fun (CekValue uni fun)
BuiltinsRuntime fun (CekValue uni fun)
?cekRuntime
        WordArray
-> Context uni fun
-> CekValue uni fun
-> CekM uni fun s (Term NamedDeBruijn uni fun ())
returnCek WordArray
unbudgetedSteps' Context uni fun
ctx (fun
-> Term NamedDeBruijn uni fun ()
-> CekValEnv uni fun
-> BuiltinRuntime (CekValue uni fun)
-> CekValue uni fun
forall (uni :: * -> *) fun.
fun
-> Term NamedDeBruijn uni fun ()
-> CekValEnv uni fun
-> BuiltinRuntime (CekValue uni fun)
-> CekValue uni fun
VBuiltin fun
bn Term NamedDeBruijn uni fun ()
term CekValEnv uni fun
env BuiltinRuntime (CekValue uni fun)
meaning)
    -- s ; ρ ▻ error A  ↦  <> A
    computeCek !WordArray
_ !Context uni fun
_ !CekValEnv uni fun
_ (Error ()
_) =
        AReview (CekEvaluationException NamedDeBruijn uni fun) ()
-> CekM uni fun s (Term NamedDeBruijn uni fun ())
forall e (m :: * -> *) x. MonadError e m => AReview e () -> m x
throwing_ AReview (CekEvaluationException NamedDeBruijn uni fun) ()
forall err. AsEvaluationFailure err => Prism' err ()
_EvaluationFailure

    {- | 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
        :: WordArray
        -> Context uni fun
        -> CekValue uni fun
        -> CekM uni fun s (Term NamedDeBruijn uni fun ())
    --- Instantiate all the free variable of the resulting term in case there are any.
    -- . ◅ V           ↦  [] V
    returnCek :: WordArray
-> Context uni fun
-> CekValue uni fun
-> CekM uni fun s (Term NamedDeBruijn uni fun ())
returnCek !WordArray
unbudgetedSteps Context uni fun
NoFrame CekValue uni fun
val = do
        WordArray -> CekM uni fun s ()
spendAccumulatedBudget WordArray
unbudgetedSteps
        Term NamedDeBruijn uni fun ()
-> CekM uni fun s (Term NamedDeBruijn uni fun ())
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Term NamedDeBruijn uni fun ()
 -> CekM uni fun s (Term NamedDeBruijn uni fun ()))
-> Term NamedDeBruijn uni fun ()
-> CekM uni fun s (Term NamedDeBruijn uni fun ())
forall a b. (a -> b) -> a -> b
$ CekValue uni fun -> Term NamedDeBruijn uni fun ()
forall (uni :: * -> *) fun.
CekValue uni fun -> Term NamedDeBruijn uni fun ()
dischargeCekValue CekValue uni fun
val
    -- s , {_ A} ◅ abs α M  ↦  s ; ρ ▻ M [ α / A ]*
    returnCek !WordArray
unbudgetedSteps (FrameForce Context uni fun
ctx) CekValue uni fun
fun = WordArray
-> Context uni fun
-> CekValue uni fun
-> CekM uni fun s (Term NamedDeBruijn uni fun ())
forceEvaluate WordArray
unbudgetedSteps Context uni fun
ctx CekValue uni fun
fun
    -- s , [_ (M,ρ)] ◅ V  ↦  s , [V _] ; ρ ▻ M
    returnCek !WordArray
unbudgetedSteps (FrameApplyArg CekValEnv uni fun
argVarEnv Term NamedDeBruijn uni fun ()
arg Context uni fun
ctx) CekValue uni fun
fun =
        WordArray
-> Context uni fun
-> CekValEnv uni fun
-> Term NamedDeBruijn uni fun ()
-> CekM uni fun s (Term NamedDeBruijn uni fun ())
computeCek WordArray
unbudgetedSteps (CekValue uni fun -> Context uni fun -> Context uni fun
forall (uni :: * -> *) fun.
CekValue uni fun -> Context uni fun -> Context uni fun
FrameApplyFun CekValue uni fun
fun Context uni fun
ctx) CekValEnv uni fun
argVarEnv Term NamedDeBruijn uni fun ()
arg
    -- s , [(lam x (M,ρ)) _] ◅ V  ↦  s ; ρ [ x  ↦  V ] ▻ M
    -- FIXME: add rule for VBuiltin once it's in the specification.
    returnCek !WordArray
unbudgetedSteps (FrameApplyFun CekValue uni fun
fun Context uni fun
ctx) CekValue uni fun
arg =
        WordArray
-> Context uni fun
-> CekValue uni fun
-> CekValue uni fun
-> CekM uni fun s (Term NamedDeBruijn uni fun ())
applyEvaluate WordArray
unbudgetedSteps Context uni fun
ctx CekValue uni fun
fun CekValue uni fun
arg

    -- | @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
        :: WordArray
        -> Context uni fun
        -> CekValue uni fun
        -> CekM uni fun s (Term NamedDeBruijn uni fun ())
    forceEvaluate :: WordArray
-> Context uni fun
-> CekValue uni fun
-> CekM uni fun s (Term NamedDeBruijn uni fun ())
forceEvaluate !WordArray
unbudgetedSteps !Context uni fun
ctx (VDelay Term NamedDeBruijn uni fun ()
body CekValEnv uni fun
env) = WordArray
-> Context uni fun
-> CekValEnv uni fun
-> Term NamedDeBruijn uni fun ()
-> CekM uni fun s (Term NamedDeBruijn uni fun ())
computeCek WordArray
unbudgetedSteps Context uni fun
ctx CekValEnv uni fun
env Term NamedDeBruijn uni fun ()
body
    forceEvaluate !WordArray
unbudgetedSteps !Context uni fun
ctx (VBuiltin fun
fun Term NamedDeBruijn uni fun ()
term CekValEnv uni fun
env (BuiltinRuntime RuntimeScheme n
sch ToRuntimeDenotationType (CekValue uni fun) n
f ToCostingType n
exF)) = do
        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 RuntimeScheme n
sch of
            -- It's only possible to force a builtin application if the builtin expects a type
            -- argument next.
            RuntimeSchemeAll RuntimeScheme n
schK -> do
                let runtime' :: BuiltinRuntime (CekValue uni fun)
runtime' = RuntimeScheme n
-> ToRuntimeDenotationType (CekValue uni fun) n
-> ToCostingType n
-> BuiltinRuntime (CekValue uni fun)
forall val (n :: Peano).
RuntimeScheme n
-> ToRuntimeDenotationType val n
-> ToCostingType n
-> BuiltinRuntime val
BuiltinRuntime RuntimeScheme n
schK ToRuntimeDenotationType (CekValue uni fun) n
f ToCostingType n
exF
                -- 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.
                CekValue uni fun
res <- fun
-> Term NamedDeBruijn uni fun ()
-> CekValEnv uni fun
-> BuiltinRuntime (CekValue uni fun)
-> CekM uni fun s (CekValue uni fun)
forall (uni :: * -> *) fun s.
(GivenCekReqs uni fun s, PrettyUni uni fun) =>
fun
-> Term NamedDeBruijn uni fun ()
-> CekValEnv uni fun
-> BuiltinRuntime (CekValue uni fun)
-> CekM uni fun s (CekValue uni fun)
evalBuiltinApp fun
fun Term NamedDeBruijn uni fun ()
term' CekValEnv uni fun
env BuiltinRuntime (CekValue uni fun)
runtime'
                WordArray
-> Context uni fun
-> CekValue uni fun
-> CekM uni fun s (Term NamedDeBruijn uni fun ())
returnCek WordArray
unbudgetedSteps Context uni fun
ctx CekValue uni fun
res
            RuntimeScheme n
_ ->
                AReview
  (EvaluationError CekUserError (MachineError fun))
  (MachineError fun)
-> MachineError fun
-> Maybe (Term NamedDeBruijn uni fun ())
-> CekM uni fun s (Term NamedDeBruijn uni fun ())
forall exc e t term (m :: * -> *) x.
(exc ~ ErrorWithCause e term, MonadError exc m) =>
AReview e t -> t -> Maybe term -> m x
throwingWithCause AReview
  (EvaluationError CekUserError (MachineError fun))
  (MachineError fun)
forall r fun. AsMachineError r fun => Prism' r (MachineError fun)
_MachineError MachineError fun
forall fun. MachineError fun
BuiltinTermArgumentExpectedMachineError (Term NamedDeBruijn uni fun ()
-> Maybe (Term NamedDeBruijn uni fun ())
forall a. a -> Maybe a
Just Term NamedDeBruijn uni fun ()
term')
    forceEvaluate !WordArray
_ !Context uni fun
_ CekValue uni fun
val =
        AReview
  (EvaluationError CekUserError (MachineError fun))
  (MachineError fun)
-> MachineError fun
-> CekValue uni fun
-> CekM uni fun s (Term NamedDeBruijn uni fun ())
forall (uni :: * -> *) fun t s x.
PrettyUni uni fun =>
AReview (EvaluationError CekUserError (MachineError fun)) t
-> t -> CekValue uni fun -> CekM uni fun s x
throwingDischarged AReview
  (EvaluationError CekUserError (MachineError fun))
  (MachineError fun)
forall r fun. AsMachineError r fun => Prism' r (MachineError fun)
_MachineError MachineError fun
forall fun. MachineError fun
NonPolymorphicInstantiationMachineError CekValue uni fun
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
        :: WordArray
        -> Context uni fun
        -> CekValue uni fun   -- lhs of application
        -> CekValue uni fun   -- rhs of application
        -> CekM uni fun s (Term NamedDeBruijn uni fun ())
    applyEvaluate :: WordArray
-> Context uni fun
-> CekValue uni fun
-> CekValue uni fun
-> CekM uni fun s (Term NamedDeBruijn uni fun ())
applyEvaluate !WordArray
unbudgetedSteps !Context uni fun
ctx (VLamAbs NamedDeBruijn
_ Term NamedDeBruijn uni fun ()
body CekValEnv uni fun
env) CekValue uni fun
arg =
        WordArray
-> Context uni fun
-> CekValEnv uni fun
-> Term NamedDeBruijn uni fun ()
-> CekM uni fun s (Term NamedDeBruijn uni fun ())
computeCek WordArray
unbudgetedSteps Context uni fun
ctx (Element (CekValEnv uni fun)
-> CekValEnv uni fun -> CekValEnv uni fun
forall e. DeBruijnEnv e => Element e -> e -> e
Env.cons Element (CekValEnv uni fun)
CekValue uni fun
arg CekValEnv uni fun
env) Term NamedDeBruijn uni fun ()
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 !WordArray
unbudgetedSteps !Context uni fun
ctx (VBuiltin fun
fun Term NamedDeBruijn uni fun ()
term CekValEnv uni fun
env (BuiltinRuntime RuntimeScheme n
sch ToRuntimeDenotationType (CekValue uni fun) n
f ToCostingType n
exF)) CekValue uni fun
arg = do
        let argTerm :: Term NamedDeBruijn uni fun ()
argTerm = CekValue uni fun -> Term NamedDeBruijn uni fun ()
forall (uni :: * -> *) fun.
CekValue uni fun -> Term NamedDeBruijn uni fun ()
dischargeCekValue CekValue uni fun
arg
            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 ()
term Term NamedDeBruijn uni fun ()
argTerm
        case RuntimeScheme n
sch of
            -- It's only possible to apply a builtin application if the builtin expects a term
            -- argument next.
            RuntimeSchemeArrow RuntimeScheme n
schB -> case ToRuntimeDenotationType (CekValue uni fun) n
CekValue uni fun
-> ReadKnownM () (ToRuntimeDenotationType (CekValue uni fun) n)
f CekValue uni fun
arg of
                Left ErrorWithCause KnownTypeError ()
err -> ErrorWithCause KnownTypeError (Term NamedDeBruijn uni fun ())
-> CekM uni fun s (Term NamedDeBruijn uni fun ())
forall err cause (m :: * -> *) void.
(MonadError (ErrorWithCause err cause) m, AsUnliftingError err,
 AsEvaluationFailure err) =>
ErrorWithCause KnownTypeError cause -> m void
throwKnownTypeErrorWithCause (ErrorWithCause KnownTypeError (Term NamedDeBruijn uni fun ())
 -> CekM uni fun s (Term NamedDeBruijn uni fun ()))
-> ErrorWithCause KnownTypeError (Term NamedDeBruijn uni fun ())
-> CekM uni fun s (Term NamedDeBruijn uni fun ())
forall a b. (a -> b) -> a -> b
$ Term NamedDeBruijn uni fun ()
argTerm Term NamedDeBruijn uni fun ()
-> ErrorWithCause KnownTypeError ()
-> ErrorWithCause KnownTypeError (Term NamedDeBruijn uni fun ())
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ ErrorWithCause KnownTypeError ()
err
                Right ToRuntimeDenotationType (CekValue uni fun) n
y  -> do
                    -- TODO: should we bother computing that 'ExMemory' eagerly? We may not need it.
                    -- We pattern match on @arg@ twice: in 'readKnown' and in 'toExMemory'.
                    -- Maybe we could fuse the two?
                    let runtime' :: BuiltinRuntime (CekValue uni fun)
runtime' = RuntimeScheme n
-> ToRuntimeDenotationType (CekValue uni fun) n
-> ToCostingType n
-> BuiltinRuntime (CekValue uni fun)
forall val (n :: Peano).
RuntimeScheme n
-> ToRuntimeDenotationType val n
-> ToCostingType n
-> BuiltinRuntime val
BuiltinRuntime RuntimeScheme n
schB ToRuntimeDenotationType (CekValue uni fun) n
y (ToCostingType n -> BuiltinRuntime (CekValue uni fun))
-> (ExMemory -> ToCostingType n)
-> ExMemory
-> BuiltinRuntime (CekValue uni fun)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ToCostingType n
ExMemory -> ToCostingType n
exF (ExMemory -> BuiltinRuntime (CekValue uni fun))
-> ExMemory -> BuiltinRuntime (CekValue uni fun)
forall a b. (a -> b) -> a -> b
$ CekValue uni fun -> ExMemory
forall (uni :: * -> *) fun.
(Closed uni, Everywhere uni ExMemoryUsage) =>
CekValue uni fun -> ExMemory
toExMemory CekValue uni fun
arg
                    CekValue uni fun
res <- fun
-> Term NamedDeBruijn uni fun ()
-> CekValEnv uni fun
-> BuiltinRuntime (CekValue uni fun)
-> CekM uni fun s (CekValue uni fun)
forall (uni :: * -> *) fun s.
(GivenCekReqs uni fun s, PrettyUni uni fun) =>
fun
-> Term NamedDeBruijn uni fun ()
-> CekValEnv uni fun
-> BuiltinRuntime (CekValue uni fun)
-> CekM uni fun s (CekValue uni fun)
evalBuiltinApp fun
fun Term NamedDeBruijn uni fun ()
term' CekValEnv uni fun
env BuiltinRuntime (CekValue uni fun)
runtime'
                    WordArray
-> Context uni fun
-> CekValue uni fun
-> CekM uni fun s (Term NamedDeBruijn uni fun ())
returnCek WordArray
unbudgetedSteps Context uni fun
ctx CekValue uni fun
res
            RuntimeScheme n
_ ->
                AReview
  (EvaluationError CekUserError (MachineError fun))
  (MachineError fun)
-> MachineError fun
-> Maybe (Term NamedDeBruijn uni fun ())
-> CekM uni fun s (Term NamedDeBruijn uni fun ())
forall exc e t term (m :: * -> *) x.
(exc ~ ErrorWithCause e term, MonadError exc m) =>
AReview e t -> t -> Maybe term -> m x
throwingWithCause AReview
  (EvaluationError CekUserError (MachineError fun))
  (MachineError fun)
forall r fun. AsMachineError r fun => Prism' r (MachineError fun)
_MachineError MachineError fun
forall fun. MachineError fun
UnexpectedBuiltinTermArgumentMachineError (Term NamedDeBruijn uni fun ()
-> Maybe (Term NamedDeBruijn uni fun ())
forall a. a -> Maybe a
Just Term NamedDeBruijn uni fun ()
term')
    applyEvaluate !WordArray
_ !Context uni fun
_ CekValue uni fun
val CekValue uni fun
_ =
        AReview
  (EvaluationError CekUserError (MachineError fun))
  (MachineError fun)
-> MachineError fun
-> CekValue uni fun
-> CekM uni fun s (Term NamedDeBruijn uni fun ())
forall (uni :: * -> *) fun t s x.
PrettyUni uni fun =>
AReview (EvaluationError CekUserError (MachineError fun)) t
-> t -> CekValue uni fun -> CekM uni fun s x
throwingDischarged AReview
  (EvaluationError CekUserError (MachineError fun))
  (MachineError fun)
forall r fun. AsMachineError r fun => Prism' r (MachineError fun)
_MachineError MachineError fun
forall fun. MachineError fun
NonFunctionalApplicationMachineError CekValue uni fun
val

    -- | Spend the budget that has been accumulated for a number of machine steps.
    spendAccumulatedBudget :: WordArray -> CekM uni fun s ()
    spendAccumulatedBudget :: WordArray -> CekM uni fun s ()
spendAccumulatedBudget !WordArray
unbudgetedSteps = WordArray
-> (Int -> Element WordArray -> CekM uni fun s ())
-> CekM uni fun s ()
forall (f :: * -> *).
Applicative f =>
WordArray -> (Int -> Element WordArray -> f ()) -> f ()
iforWordArray WordArray
unbudgetedSteps Int -> Element WordArray -> CekM uni fun s ()
forall b (uni :: * -> *) fun s.
(Integral b, ?cekBudgetSpender::CekBudgetSpender uni fun s,
 ?cekCosts::CekMachineCosts) =>
Int -> b -> CekM uni fun s ()
spend

    -- 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]
    {-# INLINE spend #-}
    spend :: Int -> b -> CekM uni fun s ()
spend !Int
i !b
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
== Int
7) (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 ()
forall (uni :: * -> *) fun s.
GivenCekSpender uni fun s =>
ExBudgetCategory fun -> ExBudget -> CekM uni fun s ()
spendBudgetCek (StepKind -> ExBudgetCategory fun
forall fun. StepKind -> ExBudgetCategory fun
BStep StepKind
kind) (b -> ExBudget -> ExBudget
forall a b. (Semigroup a, Integral b) => b -> a -> a
stimes b
w (CekMachineCosts -> StepKind -> ExBudget
cekStepCost ?cekCosts::CekMachineCosts
CekMachineCosts
?cekCosts StepKind
kind))

    -- | 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 -> WordArray -> CekM uni fun s WordArray
    stepAndMaybeSpend :: StepKind -> WordArray -> CekM uni fun s WordArray
stepAndMaybeSpend !StepKind
kind !WordArray
unbudgetedSteps = do
        -- See Note [Structure of the step counter]
        let !ix :: Index
ix = Int -> Index
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Int -> Index) -> Int -> Index
forall a b. (a -> b) -> a -> b
$ StepKind -> Int
forall a. Enum a => a -> Int
fromEnum StepKind
kind
            !unbudgetedSteps' :: WordArray
unbudgetedSteps' = Index
-> (Element WordArray -> Element WordArray)
-> WordArray
-> WordArray
overIndex Index
7 (Slippage -> Slippage -> Slippage
forall a. Num a => a -> a -> a
+Slippage
1) (WordArray -> WordArray) -> WordArray -> WordArray
forall a b. (a -> b) -> a -> b
$ Index
-> (Element WordArray -> Element WordArray)
-> WordArray
-> WordArray
overIndex Index
ix (Slippage -> Slippage -> Slippage
forall a. Num a => a -> a -> a
+Slippage
1) WordArray
unbudgetedSteps
            !unbudgetedStepsTotal :: Element WordArray
unbudgetedStepsTotal = WordArray -> Index -> Element WordArray
readArray WordArray
unbudgetedSteps' Index
7
        -- There's no risk of overflow here, since we only ever increment the total
        -- steps by 1 and then check this condition.
        if Slippage
Element WordArray
unbudgetedStepsTotal Slippage -> Slippage -> Bool
forall a. Ord a => a -> a -> Bool
>= ?cekSlippage::Slippage
Slippage
?cekSlippage
        then WordArray -> CekM uni fun s ()
spendAccumulatedBudget WordArray
unbudgetedSteps' CekM uni fun s ()
-> CekM uni fun s WordArray -> CekM uni fun s WordArray
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> WordArray -> CekM uni fun s WordArray
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Word64 -> WordArray
toWordArray Word64
0)
        else WordArray -> CekM uni fun s WordArray
forall (f :: * -> *) a. Applicative f => a -> f a
pure WordArray
unbudgetedSteps'

-- See Note [Compilation peculiarities].
-- | Evaluate a term using the CEK machine and keep track of costing, logging is optional.
runCekDeBruijn
    :: ( uni `Everywhere` ExMemoryUsage, Ix fun, PrettyUni uni fun)
    => MachineParameters CekMachineCosts CekValue uni fun
    -> ExBudgetMode cost uni fun
    -> EmitterMode uni fun
    -> Term NamedDeBruijn uni fun ()
    -> (Either (CekEvaluationException NamedDeBruijn uni fun) (Term NamedDeBruijn uni fun ()), cost, [Text])
runCekDeBruijn :: MachineParameters CekMachineCosts CekValue uni fun
-> ExBudgetMode cost uni fun
-> EmitterMode uni fun
-> Term NamedDeBruijn uni fun ()
-> (Either
      (CekEvaluationException NamedDeBruijn uni fun)
      (Term NamedDeBruijn uni fun ()),
    cost, [Text])
runCekDeBruijn MachineParameters CekMachineCosts CekValue uni fun
params ExBudgetMode cost uni fun
mode EmitterMode uni fun
emitMode Term NamedDeBruijn uni fun ()
term =
    MachineParameters CekMachineCosts CekValue uni fun
-> ExBudgetMode cost uni fun
-> EmitterMode uni fun
-> (forall s.
    GivenCekReqs uni fun s =>
    CekM uni fun s (Term NamedDeBruijn uni fun ()))
-> (Either
      (CekEvaluationException NamedDeBruijn uni fun)
      (Term NamedDeBruijn uni fun ()),
    cost, [Text])
forall a cost (uni :: * -> *) fun.
PrettyUni uni fun =>
MachineParameters CekMachineCosts CekValue uni fun
-> ExBudgetMode cost uni fun
-> EmitterMode uni fun
-> (forall s. GivenCekReqs uni fun s => CekM uni fun s a)
-> (Either (CekEvaluationException NamedDeBruijn uni fun) a, cost,
    [Text])
runCekM MachineParameters CekMachineCosts CekValue uni fun
params ExBudgetMode cost uni fun
mode EmitterMode uni fun
emitMode ((forall s.
  GivenCekReqs uni fun s =>
  CekM uni fun s (Term NamedDeBruijn uni fun ()))
 -> (Either
       (CekEvaluationException NamedDeBruijn uni fun)
       (Term NamedDeBruijn uni fun ()),
     cost, [Text]))
-> (forall s.
    GivenCekReqs uni fun s =>
    CekM uni fun s (Term NamedDeBruijn uni fun ()))
-> (Either
      (CekEvaluationException NamedDeBruijn uni fun)
      (Term NamedDeBruijn uni fun ()),
    cost, [Text])
forall a b. (a -> b) -> a -> b
$ do
        ExBudgetCategory fun -> ExBudget -> CekM uni fun s ()
forall (uni :: * -> *) fun s.
GivenCekSpender uni fun s =>
ExBudgetCategory fun -> ExBudget -> CekM uni fun s ()
spendBudgetCek ExBudgetCategory fun
forall fun. ExBudgetCategory fun
BStartup (CekMachineCosts -> ExBudget
cekStartupCost ?cekCosts::CekMachineCosts
CekMachineCosts
?cekCosts)
        Context uni fun
-> CekValEnv uni fun
-> Term NamedDeBruijn uni fun ()
-> CekM uni fun s (Term NamedDeBruijn uni fun ())
forall (uni :: * -> *) fun s.
(Ix fun, PrettyUni uni fun, GivenCekReqs uni fun s,
 Everywhere uni ExMemoryUsage) =>
Context uni fun
-> CekValEnv uni fun
-> Term NamedDeBruijn uni fun ()
-> CekM uni fun s (Term NamedDeBruijn uni fun ())
enterComputeCek Context uni fun
forall (uni :: * -> *) fun. Context uni fun
NoFrame CekValEnv uni fun
forall e. DeBruijnEnv e => e
Env.empty Term NamedDeBruijn uni fun ()
term