{-# LANGUAGE TypeOperators #-}

-- | The API to the CEK machine.
module UntypedPlutusCore.Evaluation.Machine.Cek
  ( -- * 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
  , monoidalBudgeting
  , counting
  , tallying
  , restricting
  , restrictingLarge
  , restrictingEnormous
  , enormousBudget

    -- * Emitter modes
  , noEmitter
  , logEmitter
  , logWithTimeEmitter
  , logWithBudgetEmitter
  , logWithCallTraceEmitter

    -- * Misc
  , BuiltinsRuntime (..)
  , CekResult (..)
  , CekReport (..)
  , cekResultToEither
  , CekValue (..)
  , DischargeResult (..)
  , dischargeResultToTerm
  , 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.Cek.Internal
import UntypedPlutusCore.Evaluation.Machine.CommonAPI qualified as Common

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

import Data.Text (Text)

{-| Evaluate a term using the 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
  -> CekReport cost Name uni fun
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
-> CekReport cost Name uni fun
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
-> CekReport cost Name uni fun
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
-> CekReport cost Name uni fun
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
-> CekReport cost NamedDeBruijn uni fun
runCekDeBruijn

{-| Evaluate a term using the 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
-> CekReport cost NamedDeBruijn uni fun
runCekDeBruijn

{-| Evaluate a term using the 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
-> CekReport cost NamedDeBruijn uni fun
runCekDeBruijn

{-| Evaluate a term using the 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
-> CekReport cost NamedDeBruijn uni fun
runCekDeBruijn

{-| Unlift a value using the 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
-> CekReport cost NamedDeBruijn uni fun
runCekDeBruijn