-- editorconfig-checker-disable-file
{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE ImplicitParams #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE NPlusKPatterns #-}
{-# LANGUAGE NamedFieldPuns #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}

{-| 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. -}
module UntypedPlutusCore.Evaluation.Machine.SteppableCek.Internal
  ( CekState (..)
  , Context (..)
  , contextAnn
  , liftCek
  , PrimMonad (..)
  , lenContext
  , cekStateContext
  , cekStateAnn
  , runCekDeBruijn
  , computeCek
  , returnCek
  , mkCekTrans
  , CekTrans
  , nilSlippage
  , module UntypedPlutusCore.Evaluation.Machine.Cek.Internal
  )
where

import PlutusCore.Builtin
import PlutusCore.DeBruijn
import PlutusCore.Evaluation.Machine.ExBudget
import PlutusCore.Evaluation.Machine.ExBudgetStream
import PlutusCore.Evaluation.Machine.Exception
import PlutusCore.Evaluation.Machine.MachineParameters
import PlutusCore.Evaluation.Result
import PlutusPrelude
import UntypedPlutusCore.Core
import UntypedPlutusCore.Evaluation.Machine.Cek.CekMachineCosts
  ( CekMachineCosts
  , CekMachineCostsBase (..)
  )
import UntypedPlutusCore.Evaluation.Machine.Cek.Internal hiding (Context (..), runCekDeBruijn)
import UntypedPlutusCore.Evaluation.Machine.Cek.StepCounter

import Control.Lens hiding (Context)
import Control.Monad
import Control.Monad.Primitive
import Data.Proxy
import Data.RandomAccessList.Class qualified as Env
import Data.RandomAccessList.SkewBinary qualified as Env
import Data.Semigroup (stimes)
import Data.Vector qualified as V
import Data.Word (Word64)
import GHC.TypeNats
import Universe

{- Note [Debuggable vs Original versions of CEK]

The debuggable version of CEK was created from copying over the original CEK/Internal.hs module
and modifying the `computeCek`, `returnCek` functions.
These functions were modified so as to execute a single step (Compute or Return resp.) and immediately
return with the CEK's machine new state (`CekState`), whereas previously these two functions would iteratively run to completion.

The interface otherwise remains the same. Moreover, the `Original.runCekDeBruijn` and `Debug.runCekDeBruijn` must behave equivalently.
-}

data CekState uni fun ann
  = -- loaded a term but not fired the cek yet
    Starting (NTerm uni fun ann)
  | -- the next state is computing
    Computing (Context uni fun ann) (CekValEnv uni fun ann) (NTerm uni fun ann)
  | -- the next state is returning
    Returning (Context uni fun ann) (CekValue uni fun ann)
  | -- evaluation finished
    Terminating (DischargeResult uni fun)

instance Pretty (CekState uni fun ann) where
  pretty :: forall ann. CekState uni fun ann -> Doc ann
pretty = \case
    Starting {} -> Doc ann
"Starting"
    Computing {} -> Doc ann
"Computing"
    Returning {} -> Doc ann
"Returning"
    Terminating {} -> Doc ann
"Terminating"

-- | Similar to 'Cek.Internal.Context', but augmented with an 'ann'
data Context uni fun ann
  = -- | @[V _]@
    FrameAwaitArg ann !(CekValue uni fun ann) !(Context uni fun ann)
  | -- | @[_ N]@
    FrameAwaitFunTerm ann !(CekValEnv uni fun ann) !(NTerm uni fun ann) !(Context uni fun ann)
  | FrameAwaitFunConN ann !(Spine (Some (ValueOf uni))) !(Context uni fun ann)
  | FrameAwaitFunValueN ann !(ArgStackNonEmpty uni fun ann) !(Context uni fun ann)
  | -- | @(force _)@
    FrameForce ann !(Context uni fun ann)
  | FrameConstr ann !(CekValEnv uni fun ann) {-# UNPACK #-} !Word64 ![NTerm uni fun ann] !(ArgStack uni fun ann) !(Context uni fun ann)
  | FrameCases ann !(CekValEnv uni fun ann) !(V.Vector (NTerm uni fun ann)) !(Context uni fun ann)
  | NoFrame

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

computeCek
  :: forall uni fun ann s
   . (ThrowableBuiltins uni fun, GivenCekReqs uni fun ann s)
  => Context uni fun ann
  -> CekValEnv uni fun ann
  -> NTerm uni fun ann
  -> CekM uni fun s (CekState uni fun ann)
-- s ; ρ ▻ {L A}  ↦ s , {_ A} ; ρ ▻ L
computeCek :: forall (uni :: * -> *) fun ann s.
(ThrowableBuiltins uni fun, GivenCekReqs uni fun ann s) =>
Context uni fun ann
-> CekValEnv uni fun ann
-> NTerm uni fun ann
-> CekM uni fun s (CekState uni fun ann)
computeCek !Context uni fun ann
ctx !CekValEnv uni fun ann
env (Var ann
_ NamedDeBruijn
varName) = do
  StepKind -> CekM uni fun s ()
forall (uni :: * -> *) fun ann s.
GivenCekReqs uni fun ann s =>
StepKind -> CekM uni fun s ()
stepAndMaybeSpend StepKind
BVar
  CekValue uni fun ann
val <- NamedDeBruijn
-> CekValEnv uni fun ann -> CekM uni fun s (CekValue uni fun ann)
forall (uni :: * -> *) fun ann s.
ThrowableBuiltins uni fun =>
NamedDeBruijn
-> CekValEnv uni fun ann -> CekM uni fun s (CekValue uni fun ann)
lookupVarName NamedDeBruijn
varName CekValEnv uni fun ann
env
  CekState uni fun ann -> CekM uni fun s (CekState uni fun ann)
forall a. a -> CekM uni fun s a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (CekState uni fun ann -> CekM uni fun s (CekState uni fun ann))
-> CekState uni fun ann -> CekM uni fun s (CekState uni fun ann)
forall a b. (a -> b) -> a -> b
$ Context uni fun ann -> CekValue uni fun ann -> CekState uni fun ann
forall (uni :: * -> *) fun ann.
Context uni fun ann -> CekValue uni fun ann -> CekState uni fun ann
Returning Context uni fun ann
ctx CekValue uni fun ann
val
computeCek !Context uni fun ann
ctx !CekValEnv uni fun ann
_ (Constant ann
_ Some (ValueOf uni)
val) = do
  StepKind -> CekM uni fun s ()
forall (uni :: * -> *) fun ann s.
GivenCekReqs uni fun ann s =>
StepKind -> CekM uni fun s ()
stepAndMaybeSpend StepKind
BConst
  CekState uni fun ann -> CekM uni fun s (CekState uni fun ann)
forall a. a -> CekM uni fun s a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (CekState uni fun ann -> CekM uni fun s (CekState uni fun ann))
-> CekState uni fun ann -> CekM uni fun s (CekState uni fun ann)
forall a b. (a -> b) -> a -> b
$ Context uni fun ann -> CekValue uni fun ann -> CekState uni fun ann
forall (uni :: * -> *) fun ann.
Context uni fun ann -> CekValue uni fun ann -> CekState uni fun ann
Returning Context uni fun ann
ctx (Some (ValueOf uni) -> CekValue uni fun ann
forall (uni :: * -> *) fun ann.
Some (ValueOf uni) -> CekValue uni fun ann
VCon Some (ValueOf uni)
val)
computeCek !Context uni fun ann
ctx !CekValEnv uni fun ann
env (LamAbs ann
_ NamedDeBruijn
name Term NamedDeBruijn uni fun ann
body) = do
  StepKind -> CekM uni fun s ()
forall (uni :: * -> *) fun ann s.
GivenCekReqs uni fun ann s =>
StepKind -> CekM uni fun s ()
stepAndMaybeSpend StepKind
BLamAbs
  CekState uni fun ann -> CekM uni fun s (CekState uni fun ann)
forall a. a -> CekM uni fun s a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (CekState uni fun ann -> CekM uni fun s (CekState uni fun ann))
-> CekState uni fun ann -> CekM uni fun s (CekState uni fun ann)
forall a b. (a -> b) -> a -> b
$ Context uni fun ann -> CekValue uni fun ann -> CekState uni fun ann
forall (uni :: * -> *) fun ann.
Context uni fun ann -> CekValue uni fun ann -> CekState uni fun ann
Returning Context uni fun ann
ctx (NamedDeBruijn
-> Term NamedDeBruijn uni fun ann
-> CekValEnv uni fun ann
-> CekValue uni fun ann
forall (uni :: * -> *) fun ann.
NamedDeBruijn
-> NTerm uni fun ann
-> CekValEnv uni fun ann
-> CekValue uni fun ann
VLamAbs NamedDeBruijn
name Term NamedDeBruijn uni fun ann
body CekValEnv uni fun ann
env)
computeCek !Context uni fun ann
ctx !CekValEnv uni fun ann
env (Delay ann
_ Term NamedDeBruijn uni fun ann
body) = do
  StepKind -> CekM uni fun s ()
forall (uni :: * -> *) fun ann s.
GivenCekReqs uni fun ann s =>
StepKind -> CekM uni fun s ()
stepAndMaybeSpend StepKind
BDelay
  CekState uni fun ann -> CekM uni fun s (CekState uni fun ann)
forall a. a -> CekM uni fun s a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (CekState uni fun ann -> CekM uni fun s (CekState uni fun ann))
-> CekState uni fun ann -> CekM uni fun s (CekState uni fun ann)
forall a b. (a -> b) -> a -> b
$ Context uni fun ann -> CekValue uni fun ann -> CekState uni fun ann
forall (uni :: * -> *) fun ann.
Context uni fun ann -> CekValue uni fun ann -> CekState uni fun ann
Returning Context uni fun ann
ctx (Term NamedDeBruijn uni fun ann
-> CekValEnv uni fun ann -> CekValue uni fun ann
forall (uni :: * -> *) fun ann.
NTerm uni fun ann -> CekValEnv uni fun ann -> CekValue uni fun ann
VDelay Term NamedDeBruijn uni fun ann
body CekValEnv uni fun ann
env)
-- s ; ρ ▻ lam x L  ↦  s ◅ lam x (L , ρ)
computeCek !Context uni fun ann
ctx !CekValEnv uni fun ann
env (Force ann
_ Term NamedDeBruijn uni fun ann
body) = do
  StepKind -> CekM uni fun s ()
forall (uni :: * -> *) fun ann s.
GivenCekReqs uni fun ann s =>
StepKind -> CekM uni fun s ()
stepAndMaybeSpend StepKind
BForce
  CekState uni fun ann -> CekM uni fun s (CekState uni fun ann)
forall a. a -> CekM uni fun s a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (CekState uni fun ann -> CekM uni fun s (CekState uni fun ann))
-> CekState uni fun ann -> CekM uni fun s (CekState uni fun ann)
forall a b. (a -> b) -> a -> b
$ Context uni fun ann
-> CekValEnv uni fun ann
-> Term NamedDeBruijn uni fun ann
-> CekState uni fun ann
forall (uni :: * -> *) fun ann.
Context uni fun ann
-> CekValEnv uni fun ann
-> NTerm uni fun ann
-> CekState uni fun ann
Computing (ann -> Context uni fun ann -> Context uni fun ann
forall (uni :: * -> *) fun ann.
ann -> Context uni fun ann -> Context uni fun ann
FrameForce (Term NamedDeBruijn uni fun ann -> ann
forall name (uni :: * -> *) fun ann. Term name uni fun ann -> ann
termAnn Term NamedDeBruijn uni fun ann
body) Context uni fun ann
ctx) CekValEnv uni fun ann
env Term NamedDeBruijn uni fun ann
body
-- s ; ρ ▻ [L M]  ↦  s , [_ (M,ρ)]  ; ρ ▻ L
computeCek !Context uni fun ann
ctx !CekValEnv uni fun ann
env (Apply ann
_ Term NamedDeBruijn uni fun ann
fun Term NamedDeBruijn uni fun ann
arg) = do
  StepKind -> CekM uni fun s ()
forall (uni :: * -> *) fun ann s.
GivenCekReqs uni fun ann s =>
StepKind -> CekM uni fun s ()
stepAndMaybeSpend StepKind
BApply
  CekState uni fun ann -> CekM uni fun s (CekState uni fun ann)
forall a. a -> CekM uni fun s a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (CekState uni fun ann -> CekM uni fun s (CekState uni fun ann))
-> CekState uni fun ann -> CekM uni fun s (CekState uni fun ann)
forall a b. (a -> b) -> a -> b
$ Context uni fun ann
-> CekValEnv uni fun ann
-> Term NamedDeBruijn uni fun ann
-> CekState uni fun ann
forall (uni :: * -> *) fun ann.
Context uni fun ann
-> CekValEnv uni fun ann
-> NTerm uni fun ann
-> CekState uni fun ann
Computing (ann
-> CekValEnv uni fun ann
-> Term NamedDeBruijn uni fun ann
-> Context uni fun ann
-> Context uni fun ann
forall (uni :: * -> *) fun ann.
ann
-> CekValEnv uni fun ann
-> NTerm uni fun ann
-> Context uni fun ann
-> Context uni fun ann
FrameAwaitFunTerm (Term NamedDeBruijn uni fun ann -> ann
forall name (uni :: * -> *) fun ann. Term name uni fun ann -> ann
termAnn Term NamedDeBruijn uni fun ann
fun) CekValEnv uni fun ann
env Term NamedDeBruijn uni fun ann
arg Context uni fun ann
ctx) CekValEnv uni fun ann
env Term NamedDeBruijn uni fun ann
fun
-- s ; ρ ▻ abs α L  ↦  s ◅ abs α (L , ρ)
-- s ; ρ ▻ con c  ↦  s ◅ con c
-- s ; ρ ▻ builtin bn  ↦  s ◅ builtin bn arity arity [] [] ρ
computeCek !Context uni fun ann
ctx !CekValEnv uni fun ann
_ (Builtin ann
_ fun
bn) = do
  StepKind -> CekM uni fun s ()
forall (uni :: * -> *) fun ann s.
GivenCekReqs uni fun ann s =>
StepKind -> CekM uni fun s ()
stepAndMaybeSpend StepKind
BBuiltin
  let meaning :: BuiltinRuntime (CekValue uni fun ann)
meaning = fun
-> BuiltinsRuntime fun (CekValue uni fun ann)
-> BuiltinRuntime (CekValue uni fun ann)
forall fun val.
fun -> BuiltinsRuntime fun val -> BuiltinRuntime val
lookupBuiltin fun
bn ?cekRuntime::BuiltinsRuntime fun (CekValue uni fun ann)
BuiltinsRuntime fun (CekValue uni fun ann)
?cekRuntime
  -- 'Builtin' is fully discharged.
  CekState uni fun ann -> CekM uni fun s (CekState uni fun ann)
forall a. a -> CekM uni fun s a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (CekState uni fun ann -> CekM uni fun s (CekState uni fun ann))
-> CekState uni fun ann -> CekM uni fun s (CekState uni fun ann)
forall a b. (a -> b) -> a -> b
$ Context uni fun ann -> CekValue uni fun ann -> CekState uni fun ann
forall (uni :: * -> *) fun ann.
Context uni fun ann -> CekValue uni fun ann -> CekState uni fun ann
Returning Context uni fun ann
ctx (fun
-> Term NamedDeBruijn uni fun ()
-> BuiltinRuntime (CekValue uni fun ann)
-> CekValue uni fun ann
forall (uni :: * -> *) fun ann.
fun
-> NTerm uni fun ()
-> BuiltinRuntime (CekValue uni fun ann)
-> CekValue uni fun ann
VBuiltin fun
bn (() -> fun -> Term NamedDeBruijn uni fun ()
forall name (uni :: * -> *) fun ann.
ann -> fun -> Term name uni fun ann
Builtin () fun
bn) BuiltinRuntime (CekValue uni fun ann)
meaning)
-- s ; ρ ▻ constr I T0 .. Tn  ↦  s , constr I _ (T1 ... Tn, ρ) ; ρ ▻ T0
computeCek !Context uni fun ann
ctx !CekValEnv uni fun ann
env (Constr ann
ann Word64
i [Term NamedDeBruijn uni fun ann]
es) = do
  StepKind -> CekM uni fun s ()
forall (uni :: * -> *) fun ann s.
GivenCekReqs uni fun ann s =>
StepKind -> CekM uni fun s ()
stepAndMaybeSpend StepKind
BConstr
  CekState uni fun ann -> CekM uni fun s (CekState uni fun ann)
forall a. a -> CekM uni fun s a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (CekState uni fun ann -> CekM uni fun s (CekState uni fun ann))
-> CekState uni fun ann -> CekM uni fun s (CekState uni fun ann)
forall a b. (a -> b) -> a -> b
$ case [Term NamedDeBruijn uni fun ann]
es of
    (Term NamedDeBruijn uni fun ann
t : [Term NamedDeBruijn uni fun ann]
rest) -> Context uni fun ann
-> CekValEnv uni fun ann
-> Term NamedDeBruijn uni fun ann
-> CekState uni fun ann
forall (uni :: * -> *) fun ann.
Context uni fun ann
-> CekValEnv uni fun ann
-> NTerm uni fun ann
-> CekState uni fun ann
Computing (ann
-> CekValEnv uni fun ann
-> Word64
-> [Term NamedDeBruijn uni fun ann]
-> ArgStack uni fun ann
-> Context uni fun ann
-> Context uni fun ann
forall (uni :: * -> *) fun ann.
ann
-> CekValEnv uni fun ann
-> Word64
-> [NTerm uni fun ann]
-> ArgStack uni fun ann
-> Context uni fun ann
-> Context uni fun ann
FrameConstr ann
ann CekValEnv uni fun ann
env Word64
i [Term NamedDeBruijn uni fun ann]
rest ArgStack uni fun ann
forall (uni :: * -> *) fun ann. ArgStack uni fun ann
NilStack Context uni fun ann
ctx) CekValEnv uni fun ann
env Term NamedDeBruijn uni fun ann
t
    [] -> Context uni fun ann -> CekValue uni fun ann -> CekState uni fun ann
forall (uni :: * -> *) fun ann.
Context uni fun ann -> CekValue uni fun ann -> CekState uni fun ann
Returning Context uni fun ann
ctx (CekValue uni fun ann -> CekState uni fun ann)
-> CekValue uni fun ann -> CekState uni fun ann
forall a b. (a -> b) -> a -> b
$ Word64 -> EmptyOrMultiStack uni fun ann -> CekValue uni fun ann
forall (uni :: * -> *) fun ann.
Word64 -> EmptyOrMultiStack uni fun ann -> CekValue uni fun ann
VConstr Word64
i EmptyOrMultiStack uni fun ann
forall (uni :: * -> *) fun ann. EmptyOrMultiStack uni fun ann
EmptyStack
-- s ; ρ ▻ case S C0 ... Cn  ↦  s , case _ (C0 ... Cn, ρ) ; ρ ▻ S
computeCek !Context uni fun ann
ctx !CekValEnv uni fun ann
env (Case ann
ann Term NamedDeBruijn uni fun ann
scrut Vector (Term NamedDeBruijn uni fun ann)
cs) = do
  StepKind -> CekM uni fun s ()
forall (uni :: * -> *) fun ann s.
GivenCekReqs uni fun ann s =>
StepKind -> CekM uni fun s ()
stepAndMaybeSpend StepKind
BCase
  CekState uni fun ann -> CekM uni fun s (CekState uni fun ann)
forall a. a -> CekM uni fun s a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (CekState uni fun ann -> CekM uni fun s (CekState uni fun ann))
-> CekState uni fun ann -> CekM uni fun s (CekState uni fun ann)
forall a b. (a -> b) -> a -> b
$ Context uni fun ann
-> CekValEnv uni fun ann
-> Term NamedDeBruijn uni fun ann
-> CekState uni fun ann
forall (uni :: * -> *) fun ann.
Context uni fun ann
-> CekValEnv uni fun ann
-> NTerm uni fun ann
-> CekState uni fun ann
Computing (ann
-> CekValEnv uni fun ann
-> Vector (Term NamedDeBruijn uni fun ann)
-> Context uni fun ann
-> Context uni fun ann
forall (uni :: * -> *) fun ann.
ann
-> CekValEnv uni fun ann
-> Vector (NTerm uni fun ann)
-> Context uni fun ann
-> Context uni fun ann
FrameCases ann
ann CekValEnv uni fun ann
env Vector (Term NamedDeBruijn uni fun ann)
cs Context uni fun ann
ctx) CekValEnv uni fun ann
env Term NamedDeBruijn uni fun ann
scrut
-- s ; ρ ▻ error A  ↦  <> A
computeCek !Context uni fun ann
_ !CekValEnv uni fun ann
_ (Error ann
_) =
  EvaluationError (MachineError fun) CekUserError
-> Term NamedDeBruijn uni fun ()
-> CekM uni fun s (CekState uni fun ann)
forall e cause (m :: * -> *) x.
MonadError (ErrorWithCause e cause) m =>
e -> cause -> m x
throwErrorWithCause (CekUserError -> EvaluationError (MachineError fun) CekUserError
forall structural operational.
operational -> EvaluationError structural operational
OperationalError CekUserError
CekEvaluationFailure) (() -> Term NamedDeBruijn uni fun ()
forall name (uni :: * -> *) fun ann. ann -> Term name uni fun ann
Error ())

returnCek
  :: forall uni fun ann s
   . (ThrowableBuiltins uni fun, GivenCekReqs uni fun ann s)
  => Context uni fun ann
  -> CekValue uni fun ann
  -> CekM uni fun s (CekState uni fun ann)
--- Instantiate all the free variable of the resulting term in case there are any.
-- . ◅ V           ↦  [] V
returnCek :: forall (uni :: * -> *) fun ann s.
(ThrowableBuiltins uni fun, GivenCekReqs uni fun ann s) =>
Context uni fun ann
-> CekValue uni fun ann -> CekM uni fun s (CekState uni fun ann)
returnCek Context uni fun ann
NoFrame CekValue uni fun ann
val = do
  CekM uni fun s ()
forall (uni :: * -> *) fun ann s.
GivenCekReqs uni fun ann s =>
CekM uni fun s ()
spendAccumulatedBudget
  CekState uni fun ann -> CekM uni fun s (CekState uni fun ann)
forall a. a -> CekM uni fun s a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (CekState uni fun ann -> CekM uni fun s (CekState uni fun ann))
-> CekState uni fun ann -> CekM uni fun s (CekState uni fun ann)
forall a b. (a -> b) -> a -> b
$ DischargeResult uni fun -> CekState uni fun ann
forall (uni :: * -> *) fun ann.
DischargeResult uni fun -> CekState uni fun ann
Terminating (CekValue uni fun ann -> DischargeResult uni fun
forall (uni :: * -> *) fun ann.
CekValue uni fun ann -> DischargeResult uni fun
dischargeCekValue CekValue uni fun ann
val)
-- s , {_ A} ◅ abs α M  ↦  s ; ρ ▻ M [ α / A ]*
returnCek (FrameForce ann
_ Context uni fun ann
ctx) CekValue uni fun ann
fun = Context uni fun ann
-> CekValue uni fun ann -> CekM uni fun s (CekState uni fun ann)
forall (uni :: * -> *) fun ann s.
(ThrowableBuiltins uni fun, GivenCekReqs uni fun ann s) =>
Context uni fun ann
-> CekValue uni fun ann -> CekM uni fun s (CekState uni fun ann)
forceEvaluate Context uni fun ann
ctx CekValue uni fun ann
fun
-- s , [_ (M,ρ)] ◅ V  ↦  s , [V _] ; ρ ▻ M
returnCek (FrameAwaitFunTerm ann
_funAnn CekValEnv uni fun ann
argVarEnv NTerm uni fun ann
arg Context uni fun ann
ctx) CekValue uni fun ann
fun =
  -- MAYBE: perhaps it is worth here to merge the _funAnn with argAnn
  CekState uni fun ann -> CekM uni fun s (CekState uni fun ann)
forall a. a -> CekM uni fun s a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (CekState uni fun ann -> CekM uni fun s (CekState uni fun ann))
-> CekState uni fun ann -> CekM uni fun s (CekState uni fun ann)
forall a b. (a -> b) -> a -> b
$ Context uni fun ann
-> CekValEnv uni fun ann
-> NTerm uni fun ann
-> CekState uni fun ann
forall (uni :: * -> *) fun ann.
Context uni fun ann
-> CekValEnv uni fun ann
-> NTerm uni fun ann
-> CekState uni fun ann
Computing (ann
-> CekValue uni fun ann
-> Context uni fun ann
-> Context uni fun ann
forall (uni :: * -> *) fun ann.
ann
-> CekValue uni fun ann
-> Context uni fun ann
-> Context uni fun ann
FrameAwaitArg (NTerm uni fun ann -> ann
forall name (uni :: * -> *) fun ann. Term name uni fun ann -> ann
termAnn NTerm uni fun ann
arg) CekValue uni fun ann
fun Context uni fun ann
ctx) CekValEnv uni fun ann
argVarEnv NTerm uni fun ann
arg
-- s , [(lam x (M,ρ)) _] ◅ V  ↦  s ; ρ [ x  ↦  V ] ▻ M
-- FIXME (https://github.com/IntersectMBO/plutus-private/issues/1878):
-- add rule for VBuiltin once it's in the specification.
returnCek (FrameAwaitArg ann
_ CekValue uni fun ann
fun Context uni fun ann
ctx) CekValue uni fun ann
arg =
  Context uni fun ann
-> CekValue uni fun ann
-> CekValue uni fun ann
-> CekM uni fun s (CekState uni fun ann)
forall (uni :: * -> *) fun ann s.
(ThrowableBuiltins uni fun, GivenCekReqs uni fun ann s) =>
Context uni fun ann
-> CekValue uni fun ann
-> CekValue uni fun ann
-> CekM uni fun s (CekState uni fun ann)
applyEvaluate Context uni fun ann
ctx CekValue uni fun ann
fun CekValue uni fun ann
arg
-- s , [_ V1 .. Vn] ◅ lam x (M,ρ)  ↦  s , [_ V2 .. Vn]; ρ [ x  ↦  V1 ] ▻ M
returnCek (FrameAwaitFunConN ann
ann Spine (Some (ValueOf uni))
args Context uni fun ann
ctx) CekValue uni fun ann
fun =
  case Spine (Some (ValueOf uni))
args of
    SpineLast Some (ValueOf uni)
arg -> Context uni fun ann
-> CekValue uni fun ann
-> CekValue uni fun ann
-> CekM uni fun s (CekState uni fun ann)
forall (uni :: * -> *) fun ann s.
(ThrowableBuiltins uni fun, GivenCekReqs uni fun ann s) =>
Context uni fun ann
-> CekValue uni fun ann
-> CekValue uni fun ann
-> CekM uni fun s (CekState uni fun ann)
applyEvaluate Context uni fun ann
ctx CekValue uni fun ann
fun (Some (ValueOf uni) -> CekValue uni fun ann
forall (uni :: * -> *) fun ann.
Some (ValueOf uni) -> CekValue uni fun ann
VCon Some (ValueOf uni)
arg)
    SpineCons Some (ValueOf uni)
arg Spine (Some (ValueOf uni))
rest -> Context uni fun ann
-> CekValue uni fun ann
-> CekValue uni fun ann
-> CekM uni fun s (CekState uni fun ann)
forall (uni :: * -> *) fun ann s.
(ThrowableBuiltins uni fun, GivenCekReqs uni fun ann s) =>
Context uni fun ann
-> CekValue uni fun ann
-> CekValue uni fun ann
-> CekM uni fun s (CekState uni fun ann)
applyEvaluate (ann
-> Spine (Some (ValueOf uni))
-> Context uni fun ann
-> Context uni fun ann
forall (uni :: * -> *) fun ann.
ann
-> Spine (Some (ValueOf uni))
-> Context uni fun ann
-> Context uni fun ann
FrameAwaitFunConN ann
ann Spine (Some (ValueOf uni))
rest Context uni fun ann
ctx) CekValue uni fun ann
fun (Some (ValueOf uni) -> CekValue uni fun ann
forall (uni :: * -> *) fun ann.
Some (ValueOf uni) -> CekValue uni fun ann
VCon Some (ValueOf uni)
arg)
-- s , [_ V1 .. Vn] ◅ lam x (M,ρ)  ↦  s , [_ V2 .. Vn]; ρ [ x  ↦  V1 ] ▻ M
returnCek (FrameAwaitFunValueN ann
ann ArgStackNonEmpty uni fun ann
args Context uni fun ann
ctx) CekValue uni fun ann
fun =
  case ArgStackNonEmpty uni fun ann
args of
    LastStackNonEmpty CekValue uni fun ann
arg ->
      Context uni fun ann
-> CekValue uni fun ann
-> CekValue uni fun ann
-> CekM uni fun s (CekState uni fun ann)
forall (uni :: * -> *) fun ann s.
(ThrowableBuiltins uni fun, GivenCekReqs uni fun ann s) =>
Context uni fun ann
-> CekValue uni fun ann
-> CekValue uni fun ann
-> CekM uni fun s (CekState uni fun ann)
applyEvaluate Context uni fun ann
ctx CekValue uni fun ann
fun CekValue uni fun ann
arg
    ConsStackNonEmpty CekValue uni fun ann
arg ArgStackNonEmpty uni fun ann
rest ->
      Context uni fun ann
-> CekValue uni fun ann
-> CekValue uni fun ann
-> CekM uni fun s (CekState uni fun ann)
forall (uni :: * -> *) fun ann s.
(ThrowableBuiltins uni fun, GivenCekReqs uni fun ann s) =>
Context uni fun ann
-> CekValue uni fun ann
-> CekValue uni fun ann
-> CekM uni fun s (CekState uni fun ann)
applyEvaluate (ann
-> ArgStackNonEmpty uni fun ann
-> Context uni fun ann
-> Context uni fun ann
forall (uni :: * -> *) fun ann.
ann
-> ArgStackNonEmpty uni fun ann
-> Context uni fun ann
-> Context uni fun ann
FrameAwaitFunValueN ann
ann ArgStackNonEmpty uni fun ann
rest Context uni fun ann
ctx) CekValue uni fun ann
fun CekValue uni fun ann
arg
-- s , constr I V0 ... Vj-1 _ (Tj+1 ... Tn, ρ) ◅ Vj  ↦  s , constr i V0 ... Vj _ (Tj+2... Tn, ρ)  ; ρ ▻ Tj+1
returnCek (FrameConstr ann
ann CekValEnv uni fun ann
env Word64
i [NTerm uni fun ann]
todo ArgStack uni fun ann
done Context uni fun ann
ctx) CekValue uni fun ann
e = do
  case [NTerm uni fun ann]
todo of
    (NTerm uni fun ann
next : [NTerm uni fun ann]
todo') ->
      CekState uni fun ann -> CekM uni fun s (CekState uni fun ann)
forall a. a -> CekM uni fun s a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (CekState uni fun ann -> CekM uni fun s (CekState uni fun ann))
-> CekState uni fun ann -> CekM uni fun s (CekState uni fun ann)
forall a b. (a -> b) -> a -> b
$ Context uni fun ann
-> CekValEnv uni fun ann
-> NTerm uni fun ann
-> CekState uni fun ann
forall (uni :: * -> *) fun ann.
Context uni fun ann
-> CekValEnv uni fun ann
-> NTerm uni fun ann
-> CekState uni fun ann
Computing (ann
-> CekValEnv uni fun ann
-> Word64
-> [NTerm uni fun ann]
-> ArgStack uni fun ann
-> Context uni fun ann
-> Context uni fun ann
forall (uni :: * -> *) fun ann.
ann
-> CekValEnv uni fun ann
-> Word64
-> [NTerm uni fun ann]
-> ArgStack uni fun ann
-> Context uni fun ann
-> Context uni fun ann
FrameConstr ann
ann CekValEnv uni fun ann
env Word64
i [NTerm uni fun ann]
todo' (CekValue uni fun ann
-> ArgStack uni fun ann -> ArgStack uni fun ann
forall (uni :: * -> *) fun ann.
CekValue uni fun ann
-> ArgStack uni fun ann -> ArgStack uni fun ann
ConsStack CekValue uni fun ann
e ArgStack uni fun ann
done) Context uni fun ann
ctx) CekValEnv uni fun ann
env NTerm uni fun ann
next
    [] ->
      let go :: ArgStackNonEmpty uni fun ann
-> ArgStack uni fun ann -> ArgStackNonEmpty uni fun ann
go ArgStackNonEmpty uni fun ann
acc ArgStack uni fun ann
NilStack = ArgStackNonEmpty uni fun ann
acc
          go ArgStackNonEmpty uni fun ann
acc (ConsStack CekValue uni fun ann
x ArgStack uni fun ann
xs) = ArgStackNonEmpty uni fun ann
-> ArgStack uni fun ann -> ArgStackNonEmpty uni fun ann
go (CekValue uni fun ann
-> ArgStackNonEmpty uni fun ann -> ArgStackNonEmpty uni fun ann
forall (uni :: * -> *) fun ann.
CekValue uni fun ann
-> ArgStackNonEmpty uni fun ann -> ArgStackNonEmpty uni fun ann
ConsStackNonEmpty CekValue uni fun ann
x ArgStackNonEmpty uni fun ann
acc) ArgStack uni fun ann
xs
       in CekState uni fun ann -> CekM uni fun s (CekState uni fun ann)
forall a. a -> CekM uni fun s a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (CekState uni fun ann -> CekM uni fun s (CekState uni fun ann))
-> CekState uni fun ann -> CekM uni fun s (CekState uni fun ann)
forall a b. (a -> b) -> a -> b
$ Context uni fun ann -> CekValue uni fun ann -> CekState uni fun ann
forall (uni :: * -> *) fun ann.
Context uni fun ann -> CekValue uni fun ann -> CekState uni fun ann
Returning Context uni fun ann
ctx (CekValue uni fun ann -> CekState uni fun ann)
-> CekValue uni fun ann -> CekState uni fun ann
forall a b. (a -> b) -> a -> b
$ Word64 -> EmptyOrMultiStack uni fun ann -> CekValue uni fun ann
forall (uni :: * -> *) fun ann.
Word64 -> EmptyOrMultiStack uni fun ann -> CekValue uni fun ann
VConstr Word64
i (ArgStackNonEmpty uni fun ann -> EmptyOrMultiStack uni fun ann
forall (uni :: * -> *) fun ann.
ArgStackNonEmpty uni fun ann -> EmptyOrMultiStack uni fun ann
MultiStack (ArgStackNonEmpty uni fun ann -> EmptyOrMultiStack uni fun ann)
-> ArgStackNonEmpty uni fun ann -> EmptyOrMultiStack uni fun ann
forall a b. (a -> b) -> a -> b
$ ArgStackNonEmpty uni fun ann
-> ArgStack uni fun ann -> ArgStackNonEmpty uni fun ann
forall {uni :: * -> *} {fun} {ann}.
ArgStackNonEmpty uni fun ann
-> ArgStack uni fun ann -> ArgStackNonEmpty uni fun ann
go (CekValue uni fun ann -> ArgStackNonEmpty uni fun ann
forall (uni :: * -> *) fun ann.
CekValue uni fun ann -> ArgStackNonEmpty uni fun ann
LastStackNonEmpty CekValue uni fun ann
e) ArgStack uni fun ann
done)
-- s , case _ (C0 ... CN, ρ) ◅ constr i V1 .. Vm  ↦  s , [_ V1 ... Vm] ; ρ ▻ Ci
returnCek (FrameCases ann
ann CekValEnv uni fun ann
env Vector (NTerm uni fun ann)
cs Context uni fun ann
ctx) CekValue uni fun ann
e = case CekValue uni fun ann
e of
  -- If the index is larger than the max bound of an Int, or negative, then it's a bad index
  -- As it happens, this will currently never trigger, since i is a Word64, and the largest
  -- Word64 value wraps to -1 as an Int64. So you can't wrap around enough to get an
  -- "apparently good" value.
  (VConstr Word64
i EmptyOrMultiStack uni fun ann
_)
    | forall a b. (Integral a, Num b) => a -> b
fromIntegral @_ @Integer Word64
i Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
> forall a b. (Integral a, Num b) => a -> b
fromIntegral @Int @Integer Int
forall a. Bounded a => a
maxBound ->
        EvaluationError (MachineError fun) CekUserError
-> CekValue uni fun ann -> CekM uni fun s (CekState uni fun ann)
forall (uni :: * -> *) fun ann s x.
ThrowableBuiltins uni fun =>
EvaluationError (MachineError fun) CekUserError
-> CekValue uni fun ann -> CekM uni fun s x
throwErrorDischarged (MachineError fun -> EvaluationError (MachineError fun) CekUserError
forall structural operational.
structural -> EvaluationError structural operational
StructuralError (MachineError fun
 -> EvaluationError (MachineError fun) CekUserError)
-> MachineError fun
-> EvaluationError (MachineError fun) CekUserError
forall a b. (a -> b) -> a -> b
$ Word64 -> MachineError fun
forall fun. Word64 -> MachineError fun
MissingCaseBranchMachineError Word64
i) CekValue uni fun ann
e
  (VConstr Word64
i EmptyOrMultiStack uni fun ann
args) -> case Vector (NTerm uni fun ann) -> Int -> Maybe (NTerm uni fun ann)
forall a. Vector a -> Int -> Maybe a
(V.!?) Vector (NTerm uni fun ann)
cs (Word64 -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Word64
i) of
    Just NTerm uni fun ann
t ->
      case EmptyOrMultiStack uni fun ann
args of
        EmptyOrMultiStack uni fun ann
EmptyStack -> Context uni fun ann
-> CekValEnv uni fun ann
-> NTerm uni fun ann
-> CekM uni fun s (CekState uni fun ann)
forall (uni :: * -> *) fun ann s.
(ThrowableBuiltins uni fun, GivenCekReqs uni fun ann s) =>
Context uni fun ann
-> CekValEnv uni fun ann
-> NTerm uni fun ann
-> CekM uni fun s (CekState uni fun ann)
computeCek Context uni fun ann
ctx CekValEnv uni fun ann
env NTerm uni fun ann
t
        MultiStack ArgStackNonEmpty uni fun ann
rest -> Context uni fun ann
-> CekValEnv uni fun ann
-> NTerm uni fun ann
-> CekM uni fun s (CekState uni fun ann)
forall (uni :: * -> *) fun ann s.
(ThrowableBuiltins uni fun, GivenCekReqs uni fun ann s) =>
Context uni fun ann
-> CekValEnv uni fun ann
-> NTerm uni fun ann
-> CekM uni fun s (CekState uni fun ann)
computeCek (ann
-> ArgStackNonEmpty uni fun ann
-> Context uni fun ann
-> Context uni fun ann
forall (uni :: * -> *) fun ann.
ann
-> ArgStackNonEmpty uni fun ann
-> Context uni fun ann
-> Context uni fun ann
FrameAwaitFunValueN ann
ann ArgStackNonEmpty uni fun ann
rest Context uni fun ann
ctx) CekValEnv uni fun ann
env NTerm uni fun ann
t
    Maybe (NTerm uni fun ann)
Nothing -> EvaluationError (MachineError fun) CekUserError
-> CekValue uni fun ann -> CekM uni fun s (CekState uni fun ann)
forall (uni :: * -> *) fun ann s x.
ThrowableBuiltins uni fun =>
EvaluationError (MachineError fun) CekUserError
-> CekValue uni fun ann -> CekM uni fun s x
throwErrorDischarged (MachineError fun -> EvaluationError (MachineError fun) CekUserError
forall structural operational.
structural -> EvaluationError structural operational
StructuralError (MachineError fun
 -> EvaluationError (MachineError fun) CekUserError)
-> MachineError fun
-> EvaluationError (MachineError fun) CekUserError
forall a b. (a -> b) -> a -> b
$ Word64 -> MachineError fun
forall fun. Word64 -> MachineError fun
MissingCaseBranchMachineError Word64
i) CekValue uni fun ann
e
  VCon Some (ValueOf uni)
val -> case CaserBuiltin uni
-> forall term.
   (UniOf term ~ uni) =>
   Some (ValueOf uni)
   -> Vector term -> HeadSpine Text term (Some (ValueOf uni))
forall (uni :: * -> *).
CaserBuiltin uni
-> forall term.
   (UniOf term ~ uni) =>
   Some (ValueOf uni)
   -> Vector term -> HeadSpine Text term (Some (ValueOf uni))
unCaserBuiltin ?cekCaserBuiltin::CaserBuiltin uni
CaserBuiltin uni
?cekCaserBuiltin Some (ValueOf uni)
val Vector (NTerm uni fun ann)
cs of
    HeadError Text
err -> EvaluationError (MachineError fun) CekUserError
-> CekValue uni fun ann -> CekM uni fun s (CekState uni fun ann)
forall (uni :: * -> *) fun ann s x.
ThrowableBuiltins uni fun =>
EvaluationError (MachineError fun) CekUserError
-> CekValue uni fun ann -> CekM uni fun s x
throwErrorDischarged (CekUserError -> EvaluationError (MachineError fun) CekUserError
forall structural operational.
operational -> EvaluationError structural operational
OperationalError (CekUserError -> EvaluationError (MachineError fun) CekUserError)
-> CekUserError -> EvaluationError (MachineError fun) CekUserError
forall a b. (a -> b) -> a -> b
$ Text -> CekUserError
CekCaseBuiltinError Text
err) CekValue uni fun ann
e
    HeadOnly NTerm uni fun ann
fX -> CekState uni fun ann -> CekM uni fun s (CekState uni fun ann)
forall a. a -> CekM uni fun s a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (CekState uni fun ann -> CekM uni fun s (CekState uni fun ann))
-> CekState uni fun ann -> CekM uni fun s (CekState uni fun ann)
forall a b. (a -> b) -> a -> b
$ Context uni fun ann
-> CekValEnv uni fun ann
-> NTerm uni fun ann
-> CekState uni fun ann
forall (uni :: * -> *) fun ann.
Context uni fun ann
-> CekValEnv uni fun ann
-> NTerm uni fun ann
-> CekState uni fun ann
Computing Context uni fun ann
ctx CekValEnv uni fun ann
env NTerm uni fun ann
fX
    HeadSpine NTerm uni fun ann
f Spine (Some (ValueOf uni))
xs -> CekState uni fun ann -> CekM uni fun s (CekState uni fun ann)
forall a. a -> CekM uni fun s a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (CekState uni fun ann -> CekM uni fun s (CekState uni fun ann))
-> CekState uni fun ann -> CekM uni fun s (CekState uni fun ann)
forall a b. (a -> b) -> a -> b
$ Context uni fun ann
-> CekValEnv uni fun ann
-> NTerm uni fun ann
-> CekState uni fun ann
forall (uni :: * -> *) fun ann.
Context uni fun ann
-> CekValEnv uni fun ann
-> NTerm uni fun ann
-> CekState uni fun ann
Computing (ann
-> Spine (Some (ValueOf uni))
-> Context uni fun ann
-> Context uni fun ann
forall (uni :: * -> *) fun ann.
ann
-> Spine (Some (ValueOf uni))
-> Context uni fun ann
-> Context uni fun ann
FrameAwaitFunConN ann
ann Spine (Some (ValueOf uni))
xs Context uni fun ann
ctx) CekValEnv uni fun ann
env NTerm uni fun ann
f
  CekValue uni fun ann
_ -> EvaluationError (MachineError fun) CekUserError
-> CekValue uni fun ann -> CekM uni fun s (CekState uni fun ann)
forall (uni :: * -> *) fun ann s x.
ThrowableBuiltins uni fun =>
EvaluationError (MachineError fun) CekUserError
-> CekValue uni fun ann -> CekM uni fun s x
throwErrorDischarged (MachineError fun -> EvaluationError (MachineError fun) CekUserError
forall structural operational.
structural -> EvaluationError structural operational
StructuralError MachineError fun
forall fun. MachineError fun
NonConstrScrutinizedMachineError) CekValue uni fun ann
e

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

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

-- MAYBE: runCekDeBruijn can be shared between original&debug ceks by passing a `enterComputeCek` func.
runCekDeBruijn
  :: ThrowableBuiltins uni fun
  => MachineParameters CekMachineCosts fun (CekValue uni fun ann)
  -> ExBudgetMode cost uni fun
  -> EmitterMode uni fun
  -> NTerm uni fun ann
  -> CekReport cost NamedDeBruijn uni fun
runCekDeBruijn :: forall (uni :: * -> *) fun ann cost.
ThrowableBuiltins uni fun =>
MachineParameters CekMachineCosts fun (CekValue uni fun ann)
-> ExBudgetMode cost uni fun
-> EmitterMode uni fun
-> NTerm uni fun ann
-> CekReport cost NamedDeBruijn uni fun
runCekDeBruijn MachineParameters CekMachineCosts fun (CekValue uni fun ann)
params ExBudgetMode cost uni fun
mode EmitterMode uni fun
emitMode NTerm uni fun ann
term =
  MachineParameters CekMachineCosts fun (CekValue uni fun ann)
-> ExBudgetMode cost uni fun
-> EmitterMode uni fun
-> (forall {s}.
    GivenCekReqs uni fun ann s =>
    CekM uni fun s (DischargeResult uni fun))
-> CekReport cost NamedDeBruijn uni fun
forall cost (uni :: * -> *) fun ann.
ThrowableBuiltins uni fun =>
MachineParameters CekMachineCosts fun (CekValue uni fun ann)
-> ExBudgetMode cost uni fun
-> EmitterMode uni fun
-> (forall s.
    GivenCekReqs uni fun ann s =>
    CekM uni fun s (DischargeResult uni fun))
-> CekReport cost NamedDeBruijn uni fun
runCekM MachineParameters CekMachineCosts fun (CekValue uni fun ann)
params ExBudgetMode cost uni fun
mode EmitterMode uni fun
emitMode ((forall {s}.
  GivenCekReqs uni fun ann s =>
  CekM uni fun s (DischargeResult uni fun))
 -> CekReport cost NamedDeBruijn uni fun)
-> (forall {s}.
    GivenCekReqs uni fun ann s =>
    CekM uni fun s (DischargeResult uni fun))
-> CekReport cost NamedDeBruijn uni fun
forall a b. (a -> b) -> a -> b
$ do
    ExBudgetCategory fun -> ExBudget -> CekM uni fun s ()
forall (uni :: * -> *) fun s.
GivenCekSpender uni fun s =>
ExBudgetCategory fun -> ExBudget -> CekM uni fun s ()
spendBudget ExBudgetCategory fun
forall fun. ExBudgetCategory fun
BStartup (ExBudget -> CekM uni fun s ()) -> ExBudget -> CekM uni fun s ()
forall a b. (a -> b) -> a -> b
$ Identity ExBudget -> ExBudget
forall a. Identity a -> a
runIdentity (Identity ExBudget -> ExBudget) -> Identity ExBudget -> ExBudget
forall a b. (a -> b) -> a -> b
$ CekMachineCosts -> Identity ExBudget
forall (f :: * -> *). CekMachineCostsBase f -> f ExBudget
cekStartupCost GivenCekCosts
CekMachineCosts
?cekCosts
    Context uni fun ann
-> CekValEnv uni fun ann
-> NTerm uni fun ann
-> CekM uni fun s (DischargeResult uni fun)
forall (uni :: * -> *) fun ann s.
(ThrowableBuiltins uni fun, GivenCekReqs uni fun ann s) =>
Context uni fun ann
-> CekValEnv uni fun ann
-> NTerm uni fun ann
-> CekM uni fun s (DischargeResult uni fun)
enterComputeCek Context uni fun ann
forall (uni :: * -> *) fun ann. Context uni fun ann
NoFrame CekValEnv uni fun ann
forall e. RandomAccessList e => e
Env.empty NTerm uni fun ann
term

-- See Note [Compilation peculiarities].
-- | The entering point to the CEK machine's engine.
enterComputeCek
  :: forall uni fun ann s
   . (ThrowableBuiltins uni fun, GivenCekReqs uni fun ann s)
  => Context uni fun ann
  -> CekValEnv uni fun ann
  -> NTerm uni fun ann
  -> CekM uni fun s (DischargeResult uni fun)
enterComputeCek :: forall (uni :: * -> *) fun ann s.
(ThrowableBuiltins uni fun, GivenCekReqs uni fun ann s) =>
Context uni fun ann
-> CekValEnv uni fun ann
-> NTerm uni fun ann
-> CekM uni fun s (DischargeResult uni fun)
enterComputeCek Context uni fun ann
ctx CekValEnv uni fun ann
env NTerm uni fun ann
term = CekState uni fun ann -> CekM uni fun s (DischargeResult uni fun)
iterToFinalState (CekState uni fun ann -> CekM uni fun s (DischargeResult uni fun))
-> CekState uni fun ann -> CekM uni fun s (DischargeResult uni fun)
forall a b. (a -> b) -> a -> b
$ Context uni fun ann
-> CekValEnv uni fun ann
-> NTerm uni fun ann
-> CekState uni fun ann
forall (uni :: * -> *) fun ann.
Context uni fun ann
-> CekValEnv uni fun ann
-> NTerm uni fun ann
-> CekState uni fun ann
Computing Context uni fun ann
ctx CekValEnv uni fun ann
env NTerm uni fun ann
term
  where
    iterToFinalState :: CekState uni fun ann -> CekM uni fun s (DischargeResult uni fun)
    iterToFinalState :: CekState uni fun ann -> CekM uni fun s (DischargeResult uni fun)
iterToFinalState =
      CekTrans uni fun ann s
forall (uni :: * -> *) fun ann s.
(ThrowableBuiltins uni fun, GivenCekReqs uni fun ann s) =>
CekTrans uni fun ann s
cekTrans
        CekTrans uni fun ann s
-> (CekState uni fun ann
    -> CekM uni fun s (DischargeResult uni fun))
-> CekState uni fun ann
-> CekM uni fun s (DischargeResult uni fun)
forall (m :: * -> *) a b c.
Monad m =>
(a -> m b) -> (b -> m c) -> a -> m c
>=> \case
          Terminating DischargeResult uni fun
t -> DischargeResult uni fun -> CekM uni fun s (DischargeResult uni fun)
forall a. a -> CekM uni fun s a
forall (f :: * -> *) a. Applicative f => a -> f a
pure DischargeResult uni fun
t
          CekState uni fun ann
x -> CekState uni fun ann -> CekM uni fun s (DischargeResult uni fun)
iterToFinalState CekState uni fun ann
x

{-| A CEK parameter that turns the slippage optimization *off*.

This is needed in the case of the debugger, where the accounting/budgeting costs
must be *live* updated. -}
nilSlippage :: Slippage
-- Setting the slippage to 1 would also work and turn off slippage optimization.
nilSlippage :: Slippage
nilSlippage = Slippage
0

-- the type of our state transition function, `s -> m s` , aka `Kleisli m a a`
type Trans m state = state -> m state
type CekTrans uni fun ann s = Trans (CekM uni fun s) (CekState uni fun ann)

-- | The state transition function of the machine.
cekTrans
  :: forall uni fun ann s
   . (ThrowableBuiltins uni fun, GivenCekReqs uni fun ann s)
  => CekTrans uni fun ann s
cekTrans :: forall (uni :: * -> *) fun ann s.
(ThrowableBuiltins uni fun, GivenCekReqs uni fun ann s) =>
CekTrans uni fun ann s
cekTrans = \case
  Starting NTerm uni fun ann
term -> CekState uni fun ann -> CekM uni fun s (CekState uni fun ann)
forall a. a -> CekM uni fun s a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (CekState uni fun ann -> CekM uni fun s (CekState uni fun ann))
-> CekState uni fun ann -> CekM uni fun s (CekState uni fun ann)
forall a b. (a -> b) -> a -> b
$ Context uni fun ann
-> CekValEnv uni fun ann
-> NTerm uni fun ann
-> CekState uni fun ann
forall (uni :: * -> *) fun ann.
Context uni fun ann
-> CekValEnv uni fun ann
-> NTerm uni fun ann
-> CekState uni fun ann
Computing Context uni fun ann
forall (uni :: * -> *) fun ann. Context uni fun ann
NoFrame CekValEnv uni fun ann
forall e. RandomAccessList e => e
Env.empty NTerm uni fun ann
term
  Computing Context uni fun ann
ctx CekValEnv uni fun ann
env NTerm uni fun ann
term -> Context uni fun ann
-> CekValEnv uni fun ann
-> NTerm uni fun ann
-> CekM uni fun s (CekState uni fun ann)
forall (uni :: * -> *) fun ann s.
(ThrowableBuiltins uni fun, GivenCekReqs uni fun ann s) =>
Context uni fun ann
-> CekValEnv uni fun ann
-> NTerm uni fun ann
-> CekM uni fun s (CekState uni fun ann)
computeCek Context uni fun ann
ctx CekValEnv uni fun ann
env NTerm uni fun ann
term
  Returning Context uni fun ann
ctx CekValue uni fun ann
val -> Context uni fun ann
-> CekValue uni fun ann -> CekM uni fun s (CekState uni fun ann)
forall (uni :: * -> *) fun ann s.
(ThrowableBuiltins uni fun, GivenCekReqs uni fun ann s) =>
Context uni fun ann
-> CekValue uni fun ann -> CekM uni fun s (CekState uni fun ann)
returnCek Context uni fun ann
ctx CekValue uni fun ann
val
  self :: CekState uni fun ann
self@Terminating {} -> CekState uni fun ann -> CekM uni fun s (CekState uni fun ann)
forall a. a -> CekM uni fun s a
forall (f :: * -> *) a. Applicative f => a -> f a
pure CekState uni fun ann
self -- FINAL STATE, idempotent

{-| Based on the supplied arguments, initialize the CEK environment and
construct a state transition function.
Returns the constructed transition function paired with the methods to live access the running budget. -}
mkCekTrans
  :: forall cost uni fun ann m s
   . ( ThrowableBuiltins uni fun
     , PrimMonad m
     , s ~ PrimState m -- the outer monad that initializes the transition function
     )
  => MachineParameters CekMachineCosts fun (CekValue uni fun ann)
  -> ExBudgetMode cost uni fun
  -> EmitterMode uni fun
  -> Slippage
  -> m (CekTrans uni fun ann s, ExBudgetInfo cost uni fun s)
mkCekTrans :: forall cost (uni :: * -> *) fun ann (m :: * -> *) s.
(ThrowableBuiltins uni fun, PrimMonad m, s ~ PrimState m) =>
MachineParameters CekMachineCosts fun (CekValue uni fun ann)
-> ExBudgetMode cost uni fun
-> EmitterMode uni fun
-> Slippage
-> m (CekTrans uni fun ann s, ExBudgetInfo cost uni fun s)
mkCekTrans
  (MachineParameters CaserBuiltin (UniOf (CekValue uni fun ann))
caser (MachineVariantParameters CekMachineCosts
costs BuiltinsRuntime fun (CekValue uni fun ann)
runtime))
  (ExBudgetMode forall s. ST s (ExBudgetInfo cost uni fun s)
getExBudgetInfo)
  (EmitterMode forall s. ST s ExBudget -> ST s (CekEmitterInfo uni fun s)
getEmitterMode)
  Slippage
slippage = do
    exBudgetInfo :: ExBudgetInfo cost uni fun s
exBudgetInfo@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 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)
-> m (ExBudgetInfo cost uni fun s)
forall (m1 :: * -> *) (m2 :: * -> *) a.
(PrimBase m1, PrimMonad m2, PrimState m1 ~ PrimState m2) =>
m1 a -> m2 a
liftPrim 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 (CekEmitterInfo uni fun s) -> m (CekEmitterInfo uni fun s)
forall (m1 :: * -> *) (m2 :: * -> *) a.
(PrimBase m1, PrimMonad m2, PrimState m1 ~ PrimState m2) =>
m1 a -> m2 a
liftPrim (ST s (CekEmitterInfo uni fun s) -> m (CekEmitterInfo uni fun s))
-> ST s (CekEmitterInfo uni fun s) -> m (CekEmitterInfo uni fun s)
forall a b. (a -> b) -> a -> b
$ ST s ExBudget -> ST s (CekEmitterInfo uni fun s)
forall s. ST s ExBudget -> ST s (CekEmitterInfo uni fun s)
getEmitterMode ST s ExBudget
_exBudgetModeGetCumulative
    StepCounter 10 s
ctr <- Proxy 10 -> m (StepCounter 10 (PrimState m))
forall (n :: Nat) (m :: * -> *).
(KnownNat n, PrimMonad m) =>
Proxy n -> m (StepCounter n (PrimState m))
newCounter (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @CounterSize)
    let ?cekRuntime = ?cekRuntime::BuiltinsRuntime fun (CekValue uni fun ann)
BuiltinsRuntime fun (CekValue uni fun ann)
runtime
        ?cekCaserBuiltin = ?cekCaserBuiltin::CaserBuiltin uni
CaserBuiltin uni
CaserBuiltin (UniOf (CekValue uni fun ann))
caser
        ?cekEmitter = ?cekEmitter::CekEmitter uni fun s
CekEmitter uni fun s
_cekEmitterInfoEmit
        ?cekBudgetSpender = ?cekBudgetSpender::CekBudgetSpender uni fun s
CekBudgetSpender uni fun s
_exBudgetModeSpender
        ?cekCosts = GivenCekCosts
CekMachineCosts
costs
        ?cekSlippage = GivenCekSlippage
Slippage
slippage
        ?cekStepCounter = ?cekStepCounter::StepCounter 10 s
StepCounter 10 s
ctr
     in (CekTrans uni fun ann s, ExBudgetInfo cost uni fun s)
-> m (CekTrans uni fun ann s, ExBudgetInfo cost uni fun s)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (CekTrans uni fun ann s
forall (uni :: * -> *) fun ann s.
(ThrowableBuiltins uni fun, GivenCekReqs uni fun ann s) =>
CekTrans uni fun ann s
cekTrans, ExBudgetInfo cost uni fun s
exBudgetInfo)

-- note that we do not call the final budget&emit getters like in `runCekM`,
-- since we do not need it for our usecase.

-- * Helpers

------------

-- | Lift a CEK computation to a primitive.PrimMonad m
liftCek :: (PrimMonad m, PrimState m ~ s) => CekM uni fun s a -> m a
liftCek :: forall (m :: * -> *) s (uni :: * -> *) fun a.
(PrimMonad m, PrimState m ~ s) =>
CekM uni fun s a -> m a
liftCek = ST s a -> m a
forall (m1 :: * -> *) (m2 :: * -> *) a.
(PrimBase m1, PrimMonad m2, PrimState m1 ~ PrimState m2) =>
m1 a -> m2 a
liftPrim (ST s a -> m a)
-> (CekM uni fun s a -> ST s a) -> CekM uni fun s a -> m 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

cekStateContext :: Traversal' (CekState uni fun ann) (Context uni fun ann)
cekStateContext :: forall (uni :: * -> *) fun ann (f :: * -> *).
Applicative f =>
(Context uni fun ann -> f (Context uni fun ann))
-> CekState uni fun ann -> f (CekState uni fun ann)
cekStateContext Context uni fun ann -> f (Context uni fun ann)
f = \case
  Computing Context uni fun ann
k CekValEnv uni fun ann
e NTerm uni fun ann
t -> Context uni fun ann
-> CekValEnv uni fun ann
-> NTerm uni fun ann
-> CekState uni fun ann
forall (uni :: * -> *) fun ann.
Context uni fun ann
-> CekValEnv uni fun ann
-> NTerm uni fun ann
-> CekState uni fun ann
Computing (Context uni fun ann
 -> CekValEnv uni fun ann
 -> NTerm uni fun ann
 -> CekState uni fun ann)
-> f (Context uni fun ann)
-> f (CekValEnv uni fun ann
      -> NTerm uni fun ann -> CekState uni fun ann)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Context uni fun ann -> f (Context uni fun ann)
f Context uni fun ann
k f (CekValEnv uni fun ann
   -> NTerm uni fun ann -> CekState uni fun ann)
-> f (CekValEnv uni fun ann)
-> f (NTerm uni fun ann -> CekState uni fun ann)
forall a b. f (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> CekValEnv uni fun ann -> f (CekValEnv uni fun ann)
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure CekValEnv uni fun ann
e f (NTerm uni fun ann -> CekState uni fun ann)
-> f (NTerm uni fun ann) -> f (CekState uni fun ann)
forall a b. f (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> NTerm uni fun ann -> f (NTerm uni fun ann)
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure NTerm uni fun ann
t
  Returning Context uni fun ann
k CekValue uni fun ann
v -> Context uni fun ann -> CekValue uni fun ann -> CekState uni fun ann
forall (uni :: * -> *) fun ann.
Context uni fun ann -> CekValue uni fun ann -> CekState uni fun ann
Returning (Context uni fun ann
 -> CekValue uni fun ann -> CekState uni fun ann)
-> f (Context uni fun ann)
-> f (CekValue uni fun ann -> CekState uni fun ann)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Context uni fun ann -> f (Context uni fun ann)
f Context uni fun ann
k f (CekValue uni fun ann -> CekState uni fun ann)
-> f (CekValue uni fun ann) -> f (CekState uni fun ann)
forall a b. f (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> CekValue uni fun ann -> f (CekValue uni fun ann)
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure CekValue uni fun ann
v
  CekState uni fun ann
x -> CekState uni fun ann -> f (CekState uni fun ann)
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure CekState uni fun ann
x

cekStateAnn :: CekState uni fun ann -> Maybe ann
cekStateAnn :: forall (uni :: * -> *) fun ann. CekState uni fun ann -> Maybe ann
cekStateAnn = \case
  Computing Context uni fun ann
_ CekValEnv uni fun ann
_ NTerm uni fun ann
t -> ann -> Maybe ann
forall a. a -> Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (ann -> Maybe ann) -> ann -> Maybe ann
forall a b. (a -> b) -> a -> b
$ NTerm uni fun ann -> ann
forall name (uni :: * -> *) fun ann. Term name uni fun ann -> ann
termAnn NTerm uni fun ann
t
  Returning Context uni fun ann
ctx CekValue uni fun ann
_ -> Context uni fun ann -> Maybe ann
forall (uni :: * -> *) fun ann. Context uni fun ann -> Maybe ann
contextAnn Context uni fun ann
ctx
  CekState uni fun ann
_ -> Maybe ann
forall a. Maybe a
forall (f :: * -> *) a. Alternative f => f a
empty

contextAnn :: Context uni fun ann -> Maybe ann
contextAnn :: forall (uni :: * -> *) fun ann. Context uni fun ann -> Maybe ann
contextAnn = \case
  FrameAwaitArg ann
ann CekValue uni fun ann
_ Context uni fun ann
_ -> ann -> Maybe ann
forall a. a -> Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ann
ann
  FrameAwaitFunTerm ann
ann CekValEnv uni fun ann
_ NTerm uni fun ann
_ Context uni fun ann
_ -> ann -> Maybe ann
forall a. a -> Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ann
ann
  FrameAwaitFunConN ann
ann Spine (Some (ValueOf uni))
_ Context uni fun ann
_ -> ann -> Maybe ann
forall a. a -> Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ann
ann
  FrameAwaitFunValueN ann
ann ArgStackNonEmpty uni fun ann
_ Context uni fun ann
_ -> ann -> Maybe ann
forall a. a -> Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ann
ann
  FrameForce ann
ann Context uni fun ann
_ -> ann -> Maybe ann
forall a. a -> Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ann
ann
  FrameConstr ann
ann CekValEnv uni fun ann
_ Word64
_ [NTerm uni fun ann]
_ ArgStack uni fun ann
_ Context uni fun ann
_ -> ann -> Maybe ann
forall a. a -> Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ann
ann
  FrameCases ann
ann CekValEnv uni fun ann
_ Vector (NTerm uni fun ann)
_ Context uni fun ann
_ -> ann -> Maybe ann
forall a. a -> Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ann
ann
  Context uni fun ann
NoFrame -> Maybe ann
forall a. Maybe a
forall (f :: * -> *) a. Alternative f => f a
empty

lenContext :: Context uni fun ann -> Word
lenContext :: forall (uni :: * -> *) fun ann. Context uni fun ann -> Word
lenContext = Word -> Context uni fun ann -> Word
forall (uni :: * -> *) fun ann. Word -> Context uni fun ann -> Word
go Word
0
  where
    go :: Word -> Context uni fun ann -> Word
    go :: forall (uni :: * -> *) fun ann. Word -> Context uni fun ann -> Word
go !Word
n = \case
      FrameAwaitArg ann
_ CekValue uni fun ann
_ Context uni fun ann
k -> Word -> Context uni fun ann -> Word
forall (uni :: * -> *) fun ann. Word -> Context uni fun ann -> Word
go (Word
n Word -> Word -> Word
forall a. Num a => a -> a -> a
+ Word
1) Context uni fun ann
k
      FrameAwaitFunTerm ann
_ CekValEnv uni fun ann
_ NTerm uni fun ann
_ Context uni fun ann
k -> Word -> Context uni fun ann -> Word
forall (uni :: * -> *) fun ann. Word -> Context uni fun ann -> Word
go (Word
n Word -> Word -> Word
forall a. Num a => a -> a -> a
+ Word
1) Context uni fun ann
k
      FrameAwaitFunConN ann
_ Spine (Some (ValueOf uni))
_ Context uni fun ann
k -> Word -> Context uni fun ann -> Word
forall (uni :: * -> *) fun ann. Word -> Context uni fun ann -> Word
go (Word
n Word -> Word -> Word
forall a. Num a => a -> a -> a
+ Word
1) Context uni fun ann
k
      FrameAwaitFunValueN ann
_ ArgStackNonEmpty uni fun ann
_ Context uni fun ann
k -> Word -> Context uni fun ann -> Word
forall (uni :: * -> *) fun ann. Word -> Context uni fun ann -> Word
go (Word
n Word -> Word -> Word
forall a. Num a => a -> a -> a
+ Word
1) Context uni fun ann
k
      FrameForce ann
_ Context uni fun ann
k -> Word -> Context uni fun ann -> Word
forall (uni :: * -> *) fun ann. Word -> Context uni fun ann -> Word
go (Word
n Word -> Word -> Word
forall a. Num a => a -> a -> a
+ Word
1) Context uni fun ann
k
      FrameConstr ann
_ CekValEnv uni fun ann
_ Word64
_ [NTerm uni fun ann]
_ ArgStack uni fun ann
_ Context uni fun ann
k -> Word -> Context uni fun ann -> Word
forall (uni :: * -> *) fun ann. Word -> Context uni fun ann -> Word
go (Word
n Word -> Word -> Word
forall a. Num a => a -> a -> a
+ Word
1) Context uni fun ann
k
      FrameCases ann
_ CekValEnv uni fun ann
_ Vector (NTerm uni fun ann)
_ Context uni fun ann
k -> Word -> Context uni fun ann -> Word
forall (uni :: * -> *) fun ann. Word -> Context uni fun ann -> Word
go (Word
n Word -> Word -> Word
forall a. Num a => a -> a -> a
+ Word
1) Context uni fun ann
k
      Context uni fun ann
NoFrame -> Word
0

-- * Duplicated functions from Cek.Internal module

-- FIXME (https://github.com/IntersectMBO/plutus-private/issues/1879):
-- share these functions with Cek.Internal
-- preliminary testing shows that sharing slows down original cek

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

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

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

{-| Take a possibly partial builtin application and

- either create a 'CekValue' by evaluating the application if it's saturated (emitting logs, if
   any, along the way), potentially failing evaluation
- or create a partial builtin application otherwise

and proceed with the returning phase of the CEK machine. -}
evalBuiltinApp
  :: (ThrowableBuiltins uni fun, GivenCekReqs uni fun ann s)
  => Context uni fun ann
  -> fun
  -> NTerm uni fun ()
  -> BuiltinRuntime (CekValue uni fun ann)
  -> CekM uni fun s (CekState uni fun ann)
evalBuiltinApp :: forall (uni :: * -> *) fun ann s.
(ThrowableBuiltins uni fun, GivenCekReqs uni fun ann s) =>
Context uni fun ann
-> fun
-> NTerm uni fun ()
-> BuiltinRuntime (CekValue uni fun ann)
-> CekM uni fun s (CekState uni fun ann)
evalBuiltinApp Context uni fun ann
ctx fun
fun NTerm uni fun ()
term BuiltinRuntime (CekValue uni fun ann)
runtime = case BuiltinRuntime (CekValue uni fun ann)
runtime of
  BuiltinCostedResult ExBudgetStream
budgets0 BuiltinResult (CekValue uni fun ann)
getFXs -> do
    let exCat :: ExBudgetCategory fun
exCat = fun -> ExBudgetCategory fun
forall fun. fun -> ExBudgetCategory fun
BBuiltinApp fun
fun
        spendBudgets :: ExBudgetStream -> CekM uni fun s ()
spendBudgets (ExBudgetLast ExBudget
budget) = ExBudgetCategory fun -> ExBudget -> CekM uni fun s ()
forall (uni :: * -> *) fun s.
GivenCekSpender uni fun s =>
ExBudgetCategory fun -> ExBudget -> CekM uni fun s ()
spendBudget ExBudgetCategory fun
exCat ExBudget
budget
        spendBudgets (ExBudgetCons ExBudget
budget ExBudgetStream
budgets) =
          ExBudgetCategory fun -> ExBudget -> CekM uni fun s ()
forall (uni :: * -> *) fun s.
GivenCekSpender uni fun s =>
ExBudgetCategory fun -> ExBudget -> CekM uni fun s ()
spendBudget ExBudgetCategory fun
exCat ExBudget
budget CekM uni fun s () -> CekM uni fun s () -> CekM uni fun s ()
forall a b.
CekM uni fun s a -> CekM uni fun s b -> CekM uni fun s b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> ExBudgetStream -> CekM uni fun s ()
spendBudgets ExBudgetStream
budgets
    ExBudgetStream -> CekM uni fun s ()
spendBudgets ExBudgetStream
budgets0
    case BuiltinResult (CekValue uni fun ann)
getFXs of
      BuiltinSuccess CekValue uni fun ann
y ->
        Context uni fun ann
-> CekValue uni fun ann -> CekM uni fun s (CekState uni fun ann)
forall (uni :: * -> *) fun ann s.
(ThrowableBuiltins uni fun, GivenCekReqs uni fun ann s) =>
Context uni fun ann
-> CekValue uni fun ann -> CekM uni fun s (CekState uni fun ann)
returnCek Context uni fun ann
ctx CekValue uni fun ann
y
      BuiltinSuccessWithLogs DList Text
logs CekValue uni fun ann
y -> do
        ?cekEmitter::DList Text -> CekM uni fun s ()
DList Text -> CekM uni fun s ()
?cekEmitter DList Text
logs
        Context uni fun ann
-> CekValue uni fun ann -> CekM uni fun s (CekState uni fun ann)
forall (uni :: * -> *) fun ann s.
(ThrowableBuiltins uni fun, GivenCekReqs uni fun ann s) =>
Context uni fun ann
-> CekValue uni fun ann -> CekM uni fun s (CekState uni fun ann)
returnCek Context uni fun ann
ctx CekValue uni fun ann
y
      BuiltinFailure DList Text
logs BuiltinError
err -> do
        ?cekEmitter::DList Text -> CekM uni fun s ()
DList Text -> CekM uni fun s ()
?cekEmitter DList Text
logs
        NTerm uni fun ()
-> BuiltinError -> CekM uni fun s (CekState uni fun ann)
forall structural operational cause (m :: * -> *) void.
(MonadError (EvaluationException structural operational cause) m,
 BuiltinErrorToEvaluationError structural operational) =>
cause -> BuiltinError -> m void
throwBuiltinErrorWithCause NTerm uni fun ()
term BuiltinError
err
  BuiltinRuntime (CekValue uni fun ann)
_ -> Context uni fun ann
-> CekValue uni fun ann -> CekM uni fun s (CekState uni fun ann)
forall (uni :: * -> *) fun ann s.
(ThrowableBuiltins uni fun, GivenCekReqs uni fun ann s) =>
Context uni fun ann
-> CekValue uni fun ann -> CekM uni fun s (CekState uni fun ann)
returnCek Context uni fun ann
ctx (CekValue uni fun ann -> CekM uni fun s (CekState uni fun ann))
-> CekValue uni fun ann -> CekM uni fun s (CekState uni fun ann)
forall a b. (a -> b) -> a -> b
$ fun
-> NTerm uni fun ()
-> BuiltinRuntime (CekValue uni fun ann)
-> CekValue uni fun ann
forall (uni :: * -> *) fun ann.
fun
-> NTerm uni fun ()
-> BuiltinRuntime (CekValue uni fun ann)
-> CekValue uni fun ann
VBuiltin fun
fun NTerm uni fun ()
term BuiltinRuntime (CekValue uni fun ann)
runtime
{-# INLINE evalBuiltinApp #-}

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

-- | Spend the budget that has been accumulated for a number of machine steps.
spendAccumulatedBudget :: GivenCekReqs uni fun ann s => CekM uni fun s ()
spendAccumulatedBudget :: forall (uni :: * -> *) fun ann s.
GivenCekReqs uni fun ann s =>
CekM uni fun s ()
spendAccumulatedBudget = do
  let ctr :: StepCounter 10 s
ctr = ?cekStepCounter::StepCounter 10 s
StepCounter 10 s
?cekStepCounter
  StepCounter 10 (PrimState (CekM uni fun s))
-> (Int -> Slippage -> CekM uni fun s ()) -> CekM uni fun s ()
forall (m :: * -> *) (n :: Nat).
(UpwardsM m (NatToPeano n), PrimMonad m) =>
StepCounter n (PrimState m) -> (Int -> Slippage -> m ()) -> m ()
iforCounter_ StepCounter 10 s
StepCounter 10 (PrimState (CekM uni fun s))
ctr Int -> Slippage -> CekM uni fun s ()
forall {b} {uni :: * -> *} {fun} {s}.
(Integral b, ?cekBudgetSpender::CekBudgetSpender uni fun s,
 GivenCekCosts) =>
Int -> b -> CekM uni fun s ()
spend
  StepCounter 10 (PrimState (CekM uni fun s)) -> CekM uni fun s ()
forall (n :: Nat) (m :: * -> *).
(KnownNat n, PrimMonad m) =>
StepCounter n (PrimState m) -> m ()
resetCounter StepCounter 10 s
StepCounter 10 (PrimState (CekM uni fun s))
ctr
  where
    -- 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
== (Nat -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Nat -> Int) -> Nat -> Int
forall a b. (a -> b) -> a -> b
$ Proxy 9 -> Nat
forall (n :: Nat) (proxy :: Nat -> *). KnownNat n => proxy n -> Nat
natVal (Proxy 9 -> Nat) -> Proxy 9 -> Nat
forall a b. (a -> b) -> a -> b
$ forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @TotalCountIndex)) (CekM uni fun s () -> CekM uni fun s ())
-> CekM uni fun s () -> CekM uni fun s ()
forall a b. (a -> b) -> a -> b
$
        let kind :: StepKind
kind = Int -> StepKind
forall a. Enum a => Int -> a
toEnum Int
i in ExBudgetCategory fun -> ExBudget -> CekM uni fun s ()
forall (uni :: * -> *) fun s.
GivenCekSpender uni fun s =>
ExBudgetCategory fun -> ExBudget -> CekM uni fun s ()
spendBudget (StepKind -> ExBudgetCategory fun
forall fun. StepKind -> ExBudgetCategory fun
BStep StepKind
kind) (b -> ExBudget -> ExBudget
forall b. Integral b => b -> ExBudget -> ExBudget
forall a b. (Semigroup a, Integral b) => b -> a -> a
stimes b
w (CekMachineCosts -> StepKind -> ExBudget
cekStepCost GivenCekCosts
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 :: GivenCekReqs uni fun ann s => StepKind -> CekM uni fun s ()
stepAndMaybeSpend :: forall (uni :: * -> *) fun ann s.
GivenCekReqs uni fun ann s =>
StepKind -> CekM uni fun s ()
stepAndMaybeSpend !StepKind
kind = do
  -- See Note [Structure of the step counter]
  -- This generates let-expressions in GHC Core, however all of them bind unboxed things and
  -- so they don't survive further compilation, see https://stackoverflow.com/a/14090277
  let !counterIndex :: Int
counterIndex = StepKind -> Int
forall a. Enum a => a -> Int
fromEnum StepKind
kind
      ctr :: StepCounter 10 s
ctr = ?cekStepCounter::StepCounter 10 s
StepCounter 10 s
?cekStepCounter
      !totalStepIndex :: Int
totalStepIndex = Nat -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Nat -> Int) -> Nat -> Int
forall a b. (a -> b) -> a -> b
$ Proxy 9 -> Nat
forall (n :: Nat) (proxy :: Nat -> *). KnownNat n => proxy n -> Nat
natVal (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @TotalCountIndex)
  !Slippage
unbudgetedStepsTotal <- Int
-> (Slippage -> Slippage)
-> StepCounter 10 (PrimState (CekM uni fun s))
-> CekM uni fun s Slippage
forall (m :: * -> *) (n :: Nat).
PrimMonad m =>
Int
-> (Slippage -> Slippage)
-> StepCounter n (PrimState m)
-> m Slippage
modifyCounter Int
totalStepIndex (Slippage -> Slippage -> Slippage
forall a. Num a => a -> a -> a
+ Slippage
1) StepCounter 10 s
StepCounter 10 (PrimState (CekM uni fun s))
ctr
  Slippage
_ <- Int
-> (Slippage -> Slippage)
-> StepCounter 10 (PrimState (CekM uni fun s))
-> CekM uni fun s Slippage
forall (m :: * -> *) (n :: Nat).
PrimMonad m =>
Int
-> (Slippage -> Slippage)
-> StepCounter n (PrimState m)
-> m Slippage
modifyCounter Int
counterIndex (Slippage -> Slippage -> Slippage
forall a. Num a => a -> a -> a
+ Slippage
1) StepCounter 10 s
StepCounter 10 (PrimState (CekM uni fun s))
ctr
  -- There's no risk of overflow here, since we only ever increment the total
  -- steps by 1 and then check this condition.
  Bool -> CekM uni fun s () -> CekM uni fun s ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Slippage
unbudgetedStepsTotal Slippage -> Slippage -> Bool
forall a. Ord a => a -> a -> Bool
>= GivenCekSlippage
Slippage
?cekSlippage) CekM uni fun s ()
forall (uni :: * -> *) fun ann s.
GivenCekReqs uni fun ann s =>
CekM uni fun s ()
spendAccumulatedBudget