-- | The API to the Steppable CEK machine. Provides the same interface to original CEK machine.
{-# LANGUAGE TypeOperators #-}

module UntypedPlutusCore.Evaluation.Machine.SteppableCek
    (
    -- * Running the machine
    runCek
    , runCekDeBruijn
    , runCekNoEmit
    , evaluateCek
    , evaluateCekNoEmit
    , EvaluationResult(..)
    , splitStructuralOperational
    , unsafeSplitStructuralOperational
    -- * Errors
    , CekUserError(..)
    , ErrorWithCause(..)
    , CekEvaluationException
    , EvaluationError(..)
    -- * Costing
    , ExBudgetCategory(..)
    , CekBudgetSpender(..)
    , ExBudgetMode(..)
    , StepKind(..)
    , CekExTally(..)
    , CountingSt (..)
    , TallyingSt (..)
    , RestrictingSt (..)
    , CekMachineCosts
    -- ** Costing modes
    , counting
    , tallying
    , restricting
    , restrictingEnormous
    , enormousBudget
    -- * Emitter modes
    , noEmitter
    , logEmitter
    , logWithTimeEmitter
    , logWithBudgetEmitter
    -- * Misc
    , CekValue(..)
    , readKnownCek
    , Hashable
    , ThrowableBuiltins
    )
where

import UntypedPlutusCore.Core
import UntypedPlutusCore.Evaluation.Machine.Cek.CekMachineCosts
import UntypedPlutusCore.Evaluation.Machine.Cek.EmitterMode
import UntypedPlutusCore.Evaluation.Machine.Cek.ExBudgetMode
import UntypedPlutusCore.Evaluation.Machine.CommonAPI qualified as Common
import UntypedPlutusCore.Evaluation.Machine.SteppableCek.Internal as S

import PlutusCore.Builtin
import PlutusCore.Evaluation.Machine.MachineParameters
import PlutusCore.Name.Unique

import Data.Text (Text)

{-| Evaluate a term using the Steppable CEK machine with logging enabled and keep track of costing.
A wrapper around the internal runCek to debruijn input and undebruijn output.
*THIS FUNCTION IS PARTIAL if the input term contains free variables*
-}
runCek
    :: ThrowableBuiltins uni fun
    => MachineParameters CekMachineCosts fun (CekValue uni fun ann)
    -> ExBudgetMode cost uni fun
    -> EmitterMode uni fun
    -> Term Name uni fun ann
    -> (Either (CekEvaluationException Name uni fun) (Term Name uni fun ()), cost, [Text])
runCek :: forall (uni :: * -> *) fun ann cost.
ThrowableBuiltins uni fun =>
MachineParameters CekMachineCosts fun (CekValue uni fun ann)
-> ExBudgetMode cost uni fun
-> EmitterMode uni fun
-> Term Name uni fun ann
-> (Either
      (CekEvaluationException Name uni fun) (Term Name uni fun ()),
    cost, [Text])
runCek = MachineRunner cost uni fun ann
-> MachineParameters CekMachineCosts fun (CekValue uni fun ann)
-> ExBudgetMode cost uni fun
-> EmitterMode uni fun
-> Term Name uni fun ann
-> (Either
      (CekEvaluationException Name uni fun) (Term Name uni fun ()),
    cost, [Text])
forall cost (uni :: * -> *) fun ann.
MachineRunner cost uni fun ann
-> MachineParameters CekMachineCosts fun (CekValue uni fun ann)
-> ExBudgetMode cost uni fun
-> EmitterMode uni fun
-> Term Name uni fun ann
-> (Either
      (CekEvaluationException Name uni fun) (Term Name uni fun ()),
    cost, [Text])
Common.runCek MachineRunner cost uni fun ann
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
-> (Either
      (CekEvaluationException NamedDeBruijn uni fun) (NTerm uni fun ()),
    cost, [Text])
S.runCekDeBruijn

-- | Evaluate a term using the Steppable CEK machine with logging disabled and
-- keep track of costing.
-- *THIS FUNCTION IS PARTIAL if the input term contains free variables*
runCekNoEmit
    :: ThrowableBuiltins uni fun
    => MachineParameters CekMachineCosts fun (CekValue uni fun ann)
    -> ExBudgetMode cost uni fun
    -> Term Name uni fun ann
    -> (Either (CekEvaluationException Name uni fun) (Term Name uni fun ()), cost)
runCekNoEmit :: forall (uni :: * -> *) fun ann cost.
ThrowableBuiltins uni fun =>
MachineParameters CekMachineCosts fun (CekValue uni fun ann)
-> ExBudgetMode cost uni fun
-> Term Name uni fun ann
-> (Either
      (CekEvaluationException Name uni fun) (Term Name uni fun ()),
    cost)
runCekNoEmit = MachineRunner cost uni fun ann
-> MachineParameters CekMachineCosts fun (CekValue uni fun ann)
-> ExBudgetMode cost uni fun
-> Term Name uni fun ann
-> (Either
      (CekEvaluationException Name uni fun) (Term Name uni fun ()),
    cost)
forall cost (uni :: * -> *) fun ann.
MachineRunner cost uni fun ann
-> MachineParameters CekMachineCosts fun (CekValue uni fun ann)
-> ExBudgetMode cost uni fun
-> Term Name uni fun ann
-> (Either
      (CekEvaluationException Name uni fun) (Term Name uni fun ()),
    cost)
Common.runCekNoEmit MachineRunner cost uni fun ann
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
-> (Either
      (CekEvaluationException NamedDeBruijn uni fun) (NTerm uni fun ()),
    cost, [Text])
S.runCekDeBruijn

-- | Evaluate a term using the Steppable CEK machine with logging enabled.
-- *THIS FUNCTION IS PARTIAL if the input term contains free variables*
evaluateCek
    :: ThrowableBuiltins uni fun
    => EmitterMode uni fun
    -> MachineParameters CekMachineCosts fun (CekValue uni fun ann)
    -> Term Name uni fun ann
    -> (Either (CekEvaluationException Name uni fun) (Term Name uni fun ()), [Text])
evaluateCek :: forall (uni :: * -> *) fun ann.
ThrowableBuiltins uni fun =>
EmitterMode uni fun
-> MachineParameters CekMachineCosts fun (CekValue uni fun ann)
-> Term Name uni fun ann
-> (Either
      (CekEvaluationException Name uni fun) (Term Name uni fun ()),
    [Text])
evaluateCek = MachineRunner RestrictingSt uni fun ann
-> EmitterMode uni fun
-> MachineParameters CekMachineCosts fun (CekValue uni fun ann)
-> Term Name uni fun ann
-> (Either
      (CekEvaluationException Name uni fun) (Term Name uni fun ()),
    [Text])
forall (uni :: * -> *) fun ann.
ThrowableBuiltins uni fun =>
MachineRunner RestrictingSt uni fun ann
-> EmitterMode uni fun
-> MachineParameters CekMachineCosts fun (CekValue uni fun ann)
-> Term Name uni fun ann
-> (Either
      (CekEvaluationException Name uni fun) (Term Name uni fun ()),
    [Text])
Common.evaluateCek MachineRunner RestrictingSt uni fun ann
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
-> (Either
      (CekEvaluationException NamedDeBruijn uni fun) (NTerm uni fun ()),
    cost, [Text])
S.runCekDeBruijn

-- | Evaluate a term using the Steppable CEK machine with logging disabled.
-- *THIS FUNCTION IS PARTIAL if the input term contains free variables*
evaluateCekNoEmit
    :: ThrowableBuiltins uni fun
    => MachineParameters CekMachineCosts fun (CekValue uni fun ann)
    -> Term Name uni fun ann
    -> Either (CekEvaluationException Name uni fun) (Term Name uni fun ())
evaluateCekNoEmit :: forall (uni :: * -> *) fun ann.
ThrowableBuiltins uni fun =>
MachineParameters CekMachineCosts fun (CekValue uni fun ann)
-> Term Name uni fun ann
-> Either
     (CekEvaluationException Name uni fun) (Term Name uni fun ())
evaluateCekNoEmit = MachineRunner RestrictingSt uni fun ann
-> MachineParameters CekMachineCosts fun (CekValue uni fun ann)
-> Term Name uni fun ann
-> Either
     (CekEvaluationException Name uni fun) (Term Name uni fun ())
forall (uni :: * -> *) fun ann.
ThrowableBuiltins uni fun =>
MachineRunner RestrictingSt uni fun ann
-> MachineParameters CekMachineCosts fun (CekValue uni fun ann)
-> Term Name uni fun ann
-> Either
     (CekEvaluationException Name uni fun) (Term Name uni fun ())
Common.evaluateCekNoEmit MachineRunner RestrictingSt uni fun ann
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
-> (Either
      (CekEvaluationException NamedDeBruijn uni fun) (NTerm uni fun ()),
    cost, [Text])
S.runCekDeBruijn

-- | Unlift a value using the Steppable CEK machine.
-- *THIS FUNCTION IS PARTIAL if the input term contains free variables*
readKnownCek
    :: (ThrowableBuiltins uni fun, ReadKnown (Term Name uni fun ()) a)
    => MachineParameters CekMachineCosts fun (CekValue uni fun ann)
    -> Term Name uni fun ann
    -> Either (CekEvaluationException Name uni fun) a
readKnownCek :: forall (uni :: * -> *) fun a ann.
(ThrowableBuiltins uni fun, ReadKnown (Term Name uni fun ()) a) =>
MachineParameters CekMachineCosts fun (CekValue uni fun ann)
-> Term Name uni fun ann
-> Either (CekEvaluationException Name uni fun) a
readKnownCek = MachineRunner RestrictingSt uni fun ann
-> MachineParameters CekMachineCosts fun (CekValue uni fun ann)
-> Term Name uni fun ann
-> Either (CekEvaluationException Name uni fun) a
forall (uni :: * -> *) fun a ann.
(ThrowableBuiltins uni fun, ReadKnown (Term Name uni fun ()) a) =>
MachineRunner RestrictingSt uni fun ann
-> MachineParameters CekMachineCosts fun (CekValue uni fun ann)
-> Term Name uni fun ann
-> Either (CekEvaluationException Name uni fun) a
Common.readKnownCek MachineRunner RestrictingSt uni fun ann
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
-> (Either
      (CekEvaluationException NamedDeBruijn uni fun) (NTerm uni fun ()),
    cost, [Text])
S.runCekDeBruijn