-- editorconfig-checker-disable-file
-- | The API parameterized over some machine.

{-# LANGUAGE DataKinds        #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeOperators    #-}

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
    -- * 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.Bifunctor
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
    -> (Either (CekEvaluationException NamedDeBruijn uni fun) (NTerm uni fun ()), cost, [Text])

{- 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
    -> (Either (CekEvaluationException Name uni fun) (Term Name uni fun ()), cost, [Text])
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
-> (Either
      (CekEvaluationException Name uni fun) (Term Name uni fun ()),
    cost, [Text])
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
-> (Either
      (CekEvaluationException Name uni fun) (Term Name uni fun ()),
    cost, [Text])
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
                (Either
  (CekEvaluationException NamedDeBruijn uni fun) (NTerm uni fun ())
res, cost
cost', [Text]
logs) -> (Either
  (CekEvaluationException NamedDeBruijn uni fun) (NTerm uni fun ())
-> Either
     (CekEvaluationException Name uni fun) (Term Name uni fun ())
forall (uni :: * -> *) fun.
Either
  (CekEvaluationException NamedDeBruijn uni fun)
  (Term NamedDeBruijn uni fun ())
-> Either
     (CekEvaluationException Name uni fun) (Term Name uni fun ())
unDeBruijnResult Either
  (CekEvaluationException NamedDeBruijn uni fun) (NTerm 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.
    unDeBruijnResult :: Either (CekEvaluationException NamedDeBruijn uni fun) (Term NamedDeBruijn uni fun ())
                     -> Either (CekEvaluationException Name uni fun) (Term Name uni fun ())
    unDeBruijnResult :: forall (uni :: * -> *) fun.
Either
  (CekEvaluationException NamedDeBruijn uni fun)
  (Term NamedDeBruijn uni fun ())
-> Either
     (CekEvaluationException Name uni fun) (Term Name uni fun ())
unDeBruijnResult = (CekEvaluationException NamedDeBruijn uni fun
 -> CekEvaluationException Name uni fun)
-> (Term NamedDeBruijn uni fun () -> Term Name uni fun ())
-> Either
     (CekEvaluationException NamedDeBruijn uni fun)
     (Term NamedDeBruijn uni fun ())
-> Either
     (CekEvaluationException Name uni fun) (Term Name uni fun ())
forall a b c d. (a -> b) -> (c -> d) -> Either a c -> Either b d
forall (p :: * -> * -> *) a b c d.
Bifunctor p =>
(a -> b) -> (c -> d) -> p a c -> p b d
bimap ((Term NamedDeBruijn uni fun () -> Term Name uni fun ())
-> CekEvaluationException NamedDeBruijn uni fun
-> CekEvaluationException Name uni fun
forall a b.
(a -> b)
-> ErrorWithCause
     (EvaluationError (MachineError fun) CekUserError) a
-> ErrorWithCause
     (EvaluationError (MachineError fun) CekUserError) b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Term NamedDeBruijn uni fun () -> Term Name uni fun ()
forall (uni :: * -> *) fun.
Term NamedDeBruijn uni fun () -> Term Name uni fun ()
gracefulUnDeBruijn) Term NamedDeBruijn uni fun () -> Term Name uni fun ()
forall (uni :: * -> *) fun.
Term NamedDeBruijn uni fun () -> Term Name uni fun ()
gracefulUnDeBruijn

    -- 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
    (\(Either (CekEvaluationException Name uni fun) (Term Name uni fun ())
res, cost
cost, [Text]
_logs) -> (Either (CekEvaluationException Name uni fun) (Term Name uni fun ())
res, cost
cost)) ((Either
    (CekEvaluationException Name uni fun) (Term Name uni fun ()),
  cost, [Text])
 -> (Either
       (CekEvaluationException Name uni fun) (Term Name uni fun ()),
     cost))
-> (Term Name uni fun ann
    -> (Either
          (CekEvaluationException Name uni fun) (Term Name uni fun ()),
        cost, [Text]))
-> 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
-> (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])
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
    (\(Either (CekEvaluationException Name uni fun) (Term Name uni fun ())
res, RestrictingSt
_cost, [Text]
logs) -> (Either (CekEvaluationException Name uni fun) (Term Name uni fun ())
res, [Text]
logs)) ((Either
    (CekEvaluationException Name uni fun) (Term Name uni fun ()),
  RestrictingSt, [Text])
 -> (Either
       (CekEvaluationException Name uni fun) (Term Name uni fun ()),
     [Text]))
-> (Term Name uni fun ann
    -> (Either
          (CekEvaluationException Name uni fun) (Term Name uni fun ()),
        RestrictingSt, [Text]))
-> 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
-> (Either
      (CekEvaluationException Name uni fun) (Term Name uni fun ()),
    RestrictingSt, [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])
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