-- editorconfig-checker-disable-file
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeOperators #-}

-- | The API parameterized over some machine.
module UntypedPlutusCore.Evaluation.Machine.CommonAPI
  ( -- * 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
  , logWithCallTraceEmitter

    -- * Misc
  , CekValue (..)
  , readKnownCek
  , Hashable
  , ThrowableBuiltins
  )
where

import PlutusPrelude

import UntypedPlutusCore.Core
import UntypedPlutusCore.DeBruijn
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 PlutusCore.Builtin
import PlutusCore.Evaluation.Machine.MachineParameters
import PlutusCore.Name.Unique
import PlutusCore.Quote

import Control.Monad.Except
import Control.Monad.State
import Data.Text (Text)

-- The type of the machine (runner function).
type MachineRunner cost uni fun ann =
  MachineParameters CekMachineCosts fun (CekValue uni fun ann)
  -> ExBudgetMode cost uni fun
  -> EmitterMode uni fun
  -> NTerm uni fun ann
  -> CekReport cost NamedDeBruijn uni fun

{- Note [CEK runners naming convention]
A function whose name ends in @NoEmit@ does not perform logging and so does not return any logs.
A function whose name starts with @unsafe@ throws exceptions instead of returning them purely.
A function from the @runCek@ family takes an 'ExBudgetMode' parameter and returns the final
'CekExBudgetState' (and possibly logs). Note that 'runCek' is defined in @...Cek.Internal@ for
reasons explained in Note [Compilation peculiarities].
A function from the @evaluateCek@ family does not return the final 'ExBudgetMode', nor does it
allow one to specify an 'ExBudgetMode'. I.e. such functions are only for fully evaluating programs
(and possibly returning logs). See also haddocks of 'enormousBudget'.
-}

{-| Evaluate a term using a 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
  :: 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
runCek :: 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
runCek MachineRunner cost uni fun ann
runner MachineParameters CekMachineCosts fun (CekValue uni fun ann)
params ExBudgetMode cost uni fun
mode EmitterMode uni fun
emitMode Term Name uni fun ann
term =
  -- translating input
  case forall e a. Except e a -> Either e a
runExcept @FreeVariableError (Except FreeVariableError (Term NamedDeBruijn uni fun ann)
 -> Either FreeVariableError (Term NamedDeBruijn uni fun ann))
-> Except FreeVariableError (Term NamedDeBruijn uni fun ann)
-> Either FreeVariableError (Term NamedDeBruijn uni fun ann)
forall a b. (a -> b) -> a -> b
$ Term Name uni fun ann
-> Except FreeVariableError (Term NamedDeBruijn uni fun ann)
forall (m :: * -> *) (uni :: * -> *) fun ann.
MonadError FreeVariableError m =>
Term Name uni fun ann -> m (Term NamedDeBruijn uni fun ann)
deBruijnTerm Term Name uni fun ann
term of
    Left FreeVariableError
fvError -> FreeVariableError -> CekReport cost Name uni fun
forall a e. Exception e => e -> a
throw FreeVariableError
fvError
    Right Term NamedDeBruijn uni fun ann
dbt -> do
      -- Don't use 'let': https://github.com/IntersectMBO/plutus/issues/3876
      case MachineRunner cost uni fun ann
runner MachineParameters CekMachineCosts fun (CekValue uni fun ann)
params ExBudgetMode cost uni fun
mode EmitterMode uni fun
emitMode Term NamedDeBruijn uni fun ann
dbt of
        -- translating back the output
        CekReport CekResult NamedDeBruijn uni fun
res cost
cost' [Text]
logs ->
          CekResult Name uni fun
-> cost -> [Text] -> CekReport cost Name uni fun
forall cost name (uni :: * -> *) fun.
CekResult name uni fun
-> cost -> [Text] -> CekReport cost name uni fun
CekReport ((Term NamedDeBruijn uni fun () -> Term Name uni fun ())
-> CekResult NamedDeBruijn uni fun -> CekResult Name uni fun
forall name (uni :: * -> *) fun name'.
(Term name uni fun () -> Term name' uni fun ())
-> CekResult name uni fun -> CekResult name' uni fun
mapTermCekResult Term NamedDeBruijn uni fun () -> Term Name uni fun ()
forall (uni :: * -> *) fun.
Term NamedDeBruijn uni fun () -> Term Name uni fun ()
gracefulUnDeBruijn CekResult NamedDeBruijn uni fun
res) cost
cost' [Text]
logs
  where
    -- \*GRACEFULLY* undebruijnifies: a) the error-cause-term (if it exists) or b) the success
    -- \*value-term.
    -- 'Graceful' means that the (a) && (b) undebruijnifications do not throw an error upon a free
    -- variable encounter: free debruijn indices will be turned to free, consistent uniques
    gracefulUnDeBruijn :: Term NamedDeBruijn uni fun () -> Term Name uni fun ()
    gracefulUnDeBruijn :: forall (uni :: * -> *) fun.
Term NamedDeBruijn uni fun () -> Term Name uni fun ()
gracefulUnDeBruijn Term NamedDeBruijn uni fun ()
t =
      Quote (Term Name uni fun ()) -> Term Name uni fun ()
forall a. Quote a -> a
runQuote
        (Quote (Term Name uni fun ()) -> Term Name uni fun ())
-> (StateT
      (Map Level Unique) (QuoteT Identity) (Term Name uni fun ())
    -> Quote (Term Name uni fun ()))
-> StateT
     (Map Level Unique) (QuoteT Identity) (Term Name uni fun ())
-> Term Name uni fun ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (StateT (Map Level Unique) (QuoteT Identity) (Term Name uni fun ())
 -> Map Level Unique -> Quote (Term Name uni fun ()))
-> Map Level Unique
-> StateT
     (Map Level Unique) (QuoteT Identity) (Term Name uni fun ())
-> Quote (Term Name uni fun ())
forall a b c. (a -> b -> c) -> b -> a -> c
flip StateT (Map Level Unique) (QuoteT Identity) (Term Name uni fun ())
-> Map Level Unique -> Quote (Term Name uni fun ())
forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m a
evalStateT Map Level Unique
forall a. Monoid a => a
mempty
        (StateT (Map Level Unique) (QuoteT Identity) (Term Name uni fun ())
 -> Term Name uni fun ())
-> StateT
     (Map Level Unique) (QuoteT Identity) (Term Name uni fun ())
-> Term Name uni fun ()
forall a b. (a -> b) -> a -> b
$ (Index
 -> ReaderT
      LevelInfo (StateT (Map Level Unique) (QuoteT Identity)) Unique)
-> Term NamedDeBruijn uni fun ()
-> StateT
     (Map Level Unique) (QuoteT Identity) (Term Name uni fun ())
forall (m :: * -> *) (uni :: * -> *) fun ann.
MonadQuote m =>
(Index -> ReaderT LevelInfo m Unique)
-> Term NamedDeBruijn uni fun ann -> m (Term Name uni fun ann)
unDeBruijnTermWith Index
-> ReaderT
     LevelInfo (StateT (Map Level Unique) (QuoteT Identity)) Unique
forall (m :: * -> *).
(MonadReader LevelInfo m, MonadState (Map Level Unique) m,
 MonadQuote m) =>
Index -> m Unique
freeIndexAsConsistentLevel Term NamedDeBruijn uni fun ()
t

{-| Evaluate a term using a machine with logging disabled and keep track of costing.
*THIS FUNCTION IS PARTIAL if the input term contains free variables* -}
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)
runCekNoEmit :: 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)
runCekNoEmit MachineRunner cost uni fun ann
runner MachineParameters CekMachineCosts fun (CekValue uni fun ann)
params ExBudgetMode cost uni fun
mode =
  -- throw away the logs
  (\(CekReport CekResult Name uni fun
res cost
cost [Text]
_logs) -> (CekResult Name uni fun
-> Either
     (CekEvaluationException Name uni fun) (Term Name uni fun ())
forall name (uni :: * -> *) fun.
CekResult name uni fun
-> Either
     (CekEvaluationException name uni fun) (Term name uni fun ())
cekResultToEither CekResult Name uni fun
res, cost
cost))
    (CekReport cost Name uni fun
 -> (Either
       (CekEvaluationException Name uni fun) (Term Name uni fun ()),
     cost))
-> (Term Name uni fun ann -> CekReport cost Name uni fun)
-> Term Name uni fun ann
-> (Either
      (CekEvaluationException Name uni fun) (Term Name uni fun ()),
    cost)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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
runCek MachineRunner cost uni fun ann
runner MachineParameters CekMachineCosts fun (CekValue uni fun ann)
params ExBudgetMode cost uni fun
mode EmitterMode uni fun
forall (uni :: * -> *) fun. EmitterMode uni fun
noEmitter

{-| Evaluate a term using a machine with logging enabled.
*THIS FUNCTION IS PARTIAL if the input term contains free variables* -}
evaluateCek
  :: 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])
evaluateCek :: 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])
evaluateCek MachineRunner RestrictingSt uni fun ann
runner EmitterMode uni fun
emitMode MachineParameters CekMachineCosts fun (CekValue uni fun ann)
params =
  -- throw away the cost
  (\(CekReport CekResult Name uni fun
res RestrictingSt
_cost [Text]
logs) -> (CekResult Name uni fun
-> Either
     (CekEvaluationException Name uni fun) (Term Name uni fun ())
forall name (uni :: * -> *) fun.
CekResult name uni fun
-> Either
     (CekEvaluationException name uni fun) (Term name uni fun ())
cekResultToEither CekResult Name uni fun
res, [Text]
logs))
    (CekReport RestrictingSt Name uni fun
 -> (Either
       (CekEvaluationException Name uni fun) (Term Name uni fun ()),
     [Text]))
-> (Term Name uni fun ann -> CekReport RestrictingSt Name uni fun)
-> Term Name uni fun ann
-> (Either
      (CekEvaluationException Name uni fun) (Term Name uni fun ()),
    [Text])
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MachineRunner RestrictingSt uni fun ann
-> MachineParameters CekMachineCosts fun (CekValue uni fun ann)
-> ExBudgetMode RestrictingSt uni fun
-> EmitterMode uni fun
-> Term Name uni fun ann
-> CekReport RestrictingSt 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
runCek MachineRunner RestrictingSt uni fun ann
runner MachineParameters CekMachineCosts fun (CekValue uni fun ann)
params ExBudgetMode RestrictingSt uni fun
forall (uni :: * -> *) fun.
ThrowableBuiltins uni fun =>
ExBudgetMode RestrictingSt uni fun
restrictingEnormous EmitterMode uni fun
emitMode

{-| Evaluate a term using a machine with logging disabled.
*THIS FUNCTION IS PARTIAL if the input term contains free variables* -}
evaluateCekNoEmit
  :: 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 ())
evaluateCekNoEmit :: 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 ())
evaluateCekNoEmit MachineRunner RestrictingSt uni fun ann
runner MachineParameters CekMachineCosts fun (CekValue uni fun ann)
params = (Either
   (CekEvaluationException Name uni fun) (Term Name uni fun ()),
 RestrictingSt)
-> Either
     (CekEvaluationException Name uni fun) (Term Name uni fun ())
forall a b. (a, b) -> a
fst ((Either
    (CekEvaluationException Name uni fun) (Term Name uni fun ()),
  RestrictingSt)
 -> Either
      (CekEvaluationException Name uni fun) (Term Name uni fun ()))
-> (Term Name uni fun ann
    -> (Either
          (CekEvaluationException Name uni fun) (Term Name uni fun ()),
        RestrictingSt))
-> Term Name uni fun ann
-> Either
     (CekEvaluationException Name uni fun) (Term Name uni fun ())
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MachineRunner RestrictingSt uni fun ann
-> MachineParameters CekMachineCosts fun (CekValue uni fun ann)
-> ExBudgetMode RestrictingSt uni fun
-> Term Name uni fun ann
-> (Either
      (CekEvaluationException Name uni fun) (Term Name uni fun ()),
    RestrictingSt)
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)
runCekNoEmit MachineRunner RestrictingSt uni fun ann
runner MachineParameters CekMachineCosts fun (CekValue uni fun ann)
params ExBudgetMode RestrictingSt uni fun
forall (uni :: * -> *) fun.
ThrowableBuiltins uni fun =>
ExBudgetMode RestrictingSt uni fun
restrictingEnormous

{-| Unlift a value using a machine.
*THIS FUNCTION IS PARTIAL if the input term contains free variables* -}
readKnownCek
  :: (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
readKnownCek :: 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
readKnownCek MachineRunner RestrictingSt uni fun ann
runner MachineParameters CekMachineCosts fun (CekValue uni fun ann)
params = 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 ())
evaluateCekNoEmit MachineRunner RestrictingSt uni fun ann
runner MachineParameters CekMachineCosts fun (CekValue uni fun ann)
params (Term Name uni fun ann
 -> Either
      (CekEvaluationException Name uni fun) (Term Name uni fun ()))
-> (Term Name uni fun ()
    -> Either (CekEvaluationException Name uni fun) a)
-> Term Name uni fun ann
-> Either (CekEvaluationException Name uni fun) a
forall (m :: * -> *) a b c.
Monad m =>
(a -> m b) -> (b -> m c) -> a -> m c
>=> Term Name uni fun ()
-> Either (CekEvaluationException Name uni fun) a
forall val a structural operational.
(ReadKnown val a,
 BuiltinErrorToEvaluationError structural operational) =>
val
-> Either
     (ErrorWithCause (EvaluationError structural operational) val) a
readKnownSelf