-- | The API to the CEK machine.

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

module UntypedPlutusCore.Evaluation.Machine.Cek
    (
    -- * Running the machine
    runCek
    , runCekDeBruijn
    , runCekNoEmit
    , unsafeRunCekNoEmit
    , evaluateCek
    , evaluateCekNoEmit
    , unsafeEvaluateCek
    , unsafeEvaluateCekNoEmit
    , EvaluationResult(..)
    , extractEvaluationResult
    , unsafeExtractEvaluationResult
    -- * 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
    , PrettyUni
    )
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.ExMemory
import PlutusCore.Evaluation.Machine.Exception
import PlutusCore.Evaluation.Machine.MachineParameters
import PlutusCore.Name
import PlutusCore.Pretty
import PlutusCore.Quote

import Control.Monad.Except
import Control.Monad.State
import Data.Bifunctor
import Data.Ix (Ix)
import Data.Text (Text)
import Universe

{- 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 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
    :: (uni `Everywhere` ExMemoryUsage, Ix fun, PrettyUni uni fun)
    => MachineParameters CekMachineCosts CekValue uni fun
    -> ExBudgetMode cost uni fun
    -> EmitterMode uni fun
    -> Term Name uni fun ()
    -> (Either (CekEvaluationException Name uni fun) (Term Name uni fun ()), cost, [Text])
runCek :: MachineParameters CekMachineCosts CekValue uni fun
-> ExBudgetMode cost uni fun
-> EmitterMode uni fun
-> Term Name uni fun ()
-> (Either
      (CekEvaluationException Name uni fun) (Term Name uni fun ()),
    cost, [Text])
runCek MachineParameters CekMachineCosts CekValue uni fun
params ExBudgetMode cost uni fun
mode EmitterMode uni fun
emitMode Term Name uni fun ()
term =
    -- translating input
    case forall a. Except FreeVariableError a -> Either FreeVariableError a
forall e a. Except e a -> Either e a
runExcept @FreeVariableError (Except FreeVariableError (Term NamedDeBruijn uni fun ())
 -> Either FreeVariableError (Term NamedDeBruijn uni fun ()))
-> Except FreeVariableError (Term NamedDeBruijn uni fun ())
-> Either FreeVariableError (Term NamedDeBruijn uni fun ())
forall a b. (a -> b) -> a -> b
$ Term Name uni fun ()
-> Except FreeVariableError (Term NamedDeBruijn uni fun ())
forall e (m :: * -> *) (uni :: * -> *) fun ann.
(AsFreeVariableError e, MonadError e m) =>
Term Name uni fun ann -> m (Term NamedDeBruijn uni fun ann)
deBruijnTerm Term Name uni fun ()
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 ()
dbt -> do
            -- Don't use 'let': https://github.com/input-output-hk/plutus/issues/3876
            case MachineParameters CekMachineCosts CekValue uni fun
-> ExBudgetMode cost uni fun
-> EmitterMode uni fun
-> Term NamedDeBruijn uni fun ()
-> (Either
      (CekEvaluationException NamedDeBruijn uni fun)
      (Term NamedDeBruijn uni fun ()),
    cost, [Text])
forall (uni :: * -> *) fun cost.
(Everywhere uni ExMemoryUsage, Ix fun, PrettyUni uni fun) =>
MachineParameters CekMachineCosts CekValue uni fun
-> ExBudgetMode cost uni fun
-> EmitterMode uni fun
-> Term NamedDeBruijn uni fun ()
-> (Either
      (CekEvaluationException NamedDeBruijn uni fun)
      (Term NamedDeBruijn uni fun ()),
    cost, [Text])
runCekDeBruijn MachineParameters CekMachineCosts CekValue uni fun
params ExBudgetMode cost uni fun
mode EmitterMode uni fun
emitMode Term NamedDeBruijn uni fun ()
dbt of
                -- translating back the output
                (Either
  (CekEvaluationException NamedDeBruijn uni fun)
  (Term NamedDeBruijn uni fun ())
res, cost
cost', [Text]
logs) -> (Either
  (CekEvaluationException NamedDeBruijn uni fun)
  (Term NamedDeBruijn 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)
  (Term 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.
    unDeBruijnResult :: Either (CekEvaluationException NamedDeBruijn uni fun) (Term NamedDeBruijn uni fun ())
                     -> Either (CekEvaluationException Name uni fun) (Term Name uni fun ())
    unDeBruijnResult :: 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 (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 (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 :: 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
      Levels (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 Levels m Unique)
-> Term NamedDeBruijn uni fun ann -> m (Term Name uni fun ann)
unDeBruijnTermWith Index
-> ReaderT
     Levels (StateT (Map Level Unique) (QuoteT Identity)) Unique
forall (m :: * -> *).
(MonadReader Levels m, MonadState (Map Level Unique) m,
 MonadQuote m) =>
Index -> m Unique
freeIndexAsConsistentLevel Term NamedDeBruijn uni fun ()
t

-- | 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
    :: (uni `Everywhere` ExMemoryUsage, Ix fun, PrettyUni uni fun)
    => MachineParameters CekMachineCosts CekValue uni fun
    -> ExBudgetMode cost uni fun
    -> Term Name uni fun ()
    -> (Either (CekEvaluationException Name uni fun) (Term Name uni fun ()), cost)
runCekNoEmit :: MachineParameters CekMachineCosts CekValue uni fun
-> ExBudgetMode cost uni fun
-> Term Name uni fun ()
-> (Either
      (CekEvaluationException Name uni fun) (Term Name uni fun ()),
    cost)
runCekNoEmit MachineParameters CekMachineCosts CekValue uni fun
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 ()
    -> (Either
          (CekEvaluationException Name uni fun) (Term Name uni fun ()),
        cost, [Text]))
-> Term Name uni fun ()
-> (Either
      (CekEvaluationException Name uni fun) (Term Name uni fun ()),
    cost)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MachineParameters CekMachineCosts CekValue uni fun
-> ExBudgetMode cost uni fun
-> EmitterMode uni fun
-> Term Name uni fun ()
-> (Either
      (CekEvaluationException Name uni fun) (Term Name uni fun ()),
    cost, [Text])
forall (uni :: * -> *) fun cost.
(Everywhere uni ExMemoryUsage, Ix fun, PrettyUni uni fun) =>
MachineParameters CekMachineCosts CekValue uni fun
-> ExBudgetMode cost uni fun
-> EmitterMode uni fun
-> Term Name uni fun ()
-> (Either
      (CekEvaluationException Name uni fun) (Term Name uni fun ()),
    cost, [Text])
runCek MachineParameters CekMachineCosts CekValue uni fun
params ExBudgetMode cost uni fun
mode EmitterMode uni fun
forall (uni :: * -> *) fun. EmitterMode uni fun
noEmitter

{-| Unsafely evaluate a term using the CEK machine with logging disabled and keep track of costing.
May throw a 'CekMachineException'.
*THIS FUNCTION IS PARTIAL if the input term contains free variables*
-}
unsafeRunCekNoEmit
    :: ( GShow uni, Typeable uni
       , Closed uni, uni `EverywhereAll` '[ExMemoryUsage, PrettyConst]
       , Ix fun, Pretty fun, Typeable fun
       )
    => MachineParameters CekMachineCosts CekValue uni fun
    -> ExBudgetMode cost uni fun
    -> Term Name uni fun ()
    -> (EvaluationResult (Term Name uni fun ()), cost)
unsafeRunCekNoEmit :: MachineParameters CekMachineCosts CekValue uni fun
-> ExBudgetMode cost uni fun
-> Term Name uni fun ()
-> (EvaluationResult (Term Name uni fun ()), cost)
unsafeRunCekNoEmit MachineParameters CekMachineCosts CekValue uni fun
params ExBudgetMode cost uni fun
mode =
    -- Don't use 'first': https://github.com/input-output-hk/plutus/issues/3876
    (\(Either
  (EvaluationException
     CekUserError (MachineError fun) (Term Name uni fun ()))
  (Term Name uni fun ())
e, cost
l) -> (Either
  (EvaluationException
     CekUserError (MachineError fun) (Term Name uni fun ()))
  (Term Name uni fun ())
-> EvaluationResult (Term Name uni fun ())
forall internal term user a.
(PrettyPlc internal, PrettyPlc term, Typeable internal,
 Typeable term) =>
Either (EvaluationException user internal term) a
-> EvaluationResult a
unsafeExtractEvaluationResult Either
  (EvaluationException
     CekUserError (MachineError fun) (Term Name uni fun ()))
  (Term Name uni fun ())
e, cost
l)) ((Either
    (EvaluationException
       CekUserError (MachineError fun) (Term Name uni fun ()))
    (Term Name uni fun ()),
  cost)
 -> (EvaluationResult (Term Name uni fun ()), cost))
-> (Term Name uni fun ()
    -> (Either
          (EvaluationException
             CekUserError (MachineError fun) (Term Name uni fun ()))
          (Term Name uni fun ()),
        cost))
-> Term Name uni fun ()
-> (EvaluationResult (Term Name uni fun ()), cost)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MachineParameters CekMachineCosts CekValue uni fun
-> ExBudgetMode cost uni fun
-> Term Name uni fun ()
-> (Either
      (EvaluationException
         CekUserError (MachineError fun) (Term Name uni fun ()))
      (Term Name uni fun ()),
    cost)
forall (uni :: * -> *) fun cost.
(Everywhere uni ExMemoryUsage, Ix fun, PrettyUni uni fun) =>
MachineParameters CekMachineCosts CekValue uni fun
-> ExBudgetMode cost uni fun
-> Term Name uni fun ()
-> (Either
      (CekEvaluationException Name uni fun) (Term Name uni fun ()),
    cost)
runCekNoEmit MachineParameters CekMachineCosts CekValue uni fun
params ExBudgetMode cost uni fun
mode

-- | Evaluate a term using the CEK machine with logging enabled.
-- *THIS FUNCTION IS PARTIAL if the input term contains free variables*
evaluateCek
    :: ( uni `Everywhere` ExMemoryUsage, Ix fun, PrettyUni uni fun)
    => EmitterMode uni fun
    -> MachineParameters CekMachineCosts CekValue uni fun
    -> Term Name uni fun ()
    -> (Either (CekEvaluationException Name uni fun) (Term Name uni fun ()), [Text])
evaluateCek :: EmitterMode uni fun
-> MachineParameters CekMachineCosts CekValue uni fun
-> Term Name uni fun ()
-> (Either
      (CekEvaluationException Name uni fun) (Term Name uni fun ()),
    [Text])
evaluateCek EmitterMode uni fun
emitMode MachineParameters CekMachineCosts CekValue uni fun
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 ()
    -> (Either
          (CekEvaluationException Name uni fun) (Term Name uni fun ()),
        RestrictingSt, [Text]))
-> Term Name uni fun ()
-> (Either
      (CekEvaluationException Name uni fun) (Term Name uni fun ()),
    [Text])
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MachineParameters CekMachineCosts CekValue uni fun
-> ExBudgetMode RestrictingSt uni fun
-> EmitterMode uni fun
-> Term Name uni fun ()
-> (Either
      (CekEvaluationException Name uni fun) (Term Name uni fun ()),
    RestrictingSt, [Text])
forall (uni :: * -> *) fun cost.
(Everywhere uni ExMemoryUsage, Ix fun, PrettyUni uni fun) =>
MachineParameters CekMachineCosts CekValue uni fun
-> ExBudgetMode cost uni fun
-> EmitterMode uni fun
-> Term Name uni fun ()
-> (Either
      (CekEvaluationException Name uni fun) (Term Name uni fun ()),
    cost, [Text])
runCek MachineParameters CekMachineCosts CekValue uni fun
params ExBudgetMode RestrictingSt uni fun
forall (uni :: * -> *) fun.
PrettyUni uni fun =>
ExBudgetMode RestrictingSt uni fun
restrictingEnormous EmitterMode uni fun
emitMode

-- | Evaluate a term using the CEK machine with logging disabled.
-- *THIS FUNCTION IS PARTIAL if the input term contains free variables*
evaluateCekNoEmit
    :: ( uni `Everywhere` ExMemoryUsage, Ix fun, PrettyUni uni fun)
    => MachineParameters CekMachineCosts CekValue uni fun
    -> Term Name uni fun ()
    -> Either (CekEvaluationException Name uni fun) (Term Name uni fun ())
evaluateCekNoEmit :: MachineParameters CekMachineCosts CekValue uni fun
-> Term Name uni fun ()
-> Either
     (CekEvaluationException Name uni fun) (Term Name uni fun ())
evaluateCekNoEmit MachineParameters CekMachineCosts CekValue uni fun
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 ()
    -> (Either
          (CekEvaluationException Name uni fun) (Term Name uni fun ()),
        RestrictingSt))
-> Term Name uni fun ()
-> Either
     (CekEvaluationException Name uni fun) (Term Name uni fun ())
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MachineParameters CekMachineCosts CekValue uni fun
-> ExBudgetMode RestrictingSt uni fun
-> Term Name uni fun ()
-> (Either
      (CekEvaluationException Name uni fun) (Term Name uni fun ()),
    RestrictingSt)
forall (uni :: * -> *) fun cost.
(Everywhere uni ExMemoryUsage, Ix fun, PrettyUni uni fun) =>
MachineParameters CekMachineCosts CekValue uni fun
-> ExBudgetMode cost uni fun
-> Term Name uni fun ()
-> (Either
      (CekEvaluationException Name uni fun) (Term Name uni fun ()),
    cost)
runCekNoEmit MachineParameters CekMachineCosts CekValue uni fun
params ExBudgetMode RestrictingSt uni fun
forall (uni :: * -> *) fun.
PrettyUni uni fun =>
ExBudgetMode RestrictingSt uni fun
restrictingEnormous

-- | Evaluate a term using the CEK machine with logging enabled. May throw a 'CekMachineException'.
-- *THIS FUNCTION IS PARTIAL if the input term contains free variables*
unsafeEvaluateCek
    :: ( GShow uni, Typeable uni
       , Closed uni, uni `EverywhereAll` '[ExMemoryUsage, PrettyConst]
       , Ix fun, Pretty fun, Typeable fun
       )
    => EmitterMode uni fun
    -> MachineParameters CekMachineCosts CekValue uni fun
    -> Term Name uni fun ()
    -> (EvaluationResult (Term Name uni fun ()), [Text])
unsafeEvaluateCek :: EmitterMode uni fun
-> MachineParameters CekMachineCosts CekValue uni fun
-> Term Name uni fun ()
-> (EvaluationResult (Term Name uni fun ()), [Text])
unsafeEvaluateCek EmitterMode uni fun
emitTime MachineParameters CekMachineCosts CekValue uni fun
params =
    -- Don't use 'first': https://github.com/input-output-hk/plutus/issues/3876
    (\(Either
  (EvaluationException
     CekUserError (MachineError fun) (Term Name uni fun ()))
  (Term Name uni fun ())
e, [Text]
l) -> (Either
  (EvaluationException
     CekUserError (MachineError fun) (Term Name uni fun ()))
  (Term Name uni fun ())
-> EvaluationResult (Term Name uni fun ())
forall internal term user a.
(PrettyPlc internal, PrettyPlc term, Typeable internal,
 Typeable term) =>
Either (EvaluationException user internal term) a
-> EvaluationResult a
unsafeExtractEvaluationResult Either
  (EvaluationException
     CekUserError (MachineError fun) (Term Name uni fun ()))
  (Term Name uni fun ())
e, [Text]
l)) ((Either
    (EvaluationException
       CekUserError (MachineError fun) (Term Name uni fun ()))
    (Term Name uni fun ()),
  [Text])
 -> (EvaluationResult (Term Name uni fun ()), [Text]))
-> (Term Name uni fun ()
    -> (Either
          (EvaluationException
             CekUserError (MachineError fun) (Term Name uni fun ()))
          (Term Name uni fun ()),
        [Text]))
-> Term Name uni fun ()
-> (EvaluationResult (Term Name uni fun ()), [Text])
forall b c a. (b -> c) -> (a -> b) -> a -> c
. EmitterMode uni fun
-> MachineParameters CekMachineCosts CekValue uni fun
-> Term Name uni fun ()
-> (Either
      (EvaluationException
         CekUserError (MachineError fun) (Term Name uni fun ()))
      (Term Name uni fun ()),
    [Text])
forall (uni :: * -> *) fun.
(Everywhere uni ExMemoryUsage, Ix fun, PrettyUni uni fun) =>
EmitterMode uni fun
-> MachineParameters CekMachineCosts CekValue uni fun
-> Term Name uni fun ()
-> (Either
      (CekEvaluationException Name uni fun) (Term Name uni fun ()),
    [Text])
evaluateCek EmitterMode uni fun
emitTime MachineParameters CekMachineCosts CekValue uni fun
params

-- | Evaluate a term using the CEK machine with logging disabled. May throw a 'CekMachineException'.
-- *THIS FUNCTION IS PARTIAL if the input term contains free variables*
unsafeEvaluateCekNoEmit
    :: ( GShow uni, Typeable uni
       , Closed uni, uni `EverywhereAll` '[ExMemoryUsage, PrettyConst]
       , Ix fun, Pretty fun, Typeable fun
       )
    => MachineParameters CekMachineCosts CekValue uni fun
    -> Term Name uni fun ()
    -> EvaluationResult (Term Name uni fun ())
unsafeEvaluateCekNoEmit :: MachineParameters CekMachineCosts CekValue uni fun
-> Term Name uni fun () -> EvaluationResult (Term Name uni fun ())
unsafeEvaluateCekNoEmit MachineParameters CekMachineCosts CekValue uni fun
params = Either
  (EvaluationException
     CekUserError (MachineError fun) (Term Name uni fun ()))
  (Term Name uni fun ())
-> EvaluationResult (Term Name uni fun ())
forall internal term user a.
(PrettyPlc internal, PrettyPlc term, Typeable internal,
 Typeable term) =>
Either (EvaluationException user internal term) a
-> EvaluationResult a
unsafeExtractEvaluationResult (Either
   (EvaluationException
      CekUserError (MachineError fun) (Term Name uni fun ()))
   (Term Name uni fun ())
 -> EvaluationResult (Term Name uni fun ()))
-> (Term Name uni fun ()
    -> Either
         (EvaluationException
            CekUserError (MachineError fun) (Term Name uni fun ()))
         (Term Name uni fun ()))
-> Term Name uni fun ()
-> EvaluationResult (Term Name uni fun ())
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MachineParameters CekMachineCosts CekValue uni fun
-> Term Name uni fun ()
-> Either
     (EvaluationException
        CekUserError (MachineError fun) (Term Name uni fun ()))
     (Term Name uni fun ())
forall (uni :: * -> *) fun.
(Everywhere uni ExMemoryUsage, Ix fun, PrettyUni uni fun) =>
MachineParameters CekMachineCosts CekValue uni fun
-> Term Name uni fun ()
-> Either
     (CekEvaluationException Name uni fun) (Term Name uni fun ())
evaluateCekNoEmit MachineParameters CekMachineCosts CekValue uni fun
params

-- | Unlift a value using the CEK machine.
-- *THIS FUNCTION IS PARTIAL if the input term contains free variables*
readKnownCek
    :: ( uni `Everywhere` ExMemoryUsage
       , ReadKnown (Term Name uni fun ()) a
       , Ix fun, PrettyUni uni fun
       )
    => MachineParameters CekMachineCosts CekValue uni fun
    -> Term Name uni fun ()
    -> Either (CekEvaluationException Name uni fun) a
readKnownCek :: MachineParameters CekMachineCosts CekValue uni fun
-> Term Name uni fun ()
-> Either (CekEvaluationException Name uni fun) a
readKnownCek MachineParameters CekMachineCosts CekValue uni fun
params = MachineParameters CekMachineCosts CekValue uni fun
-> Term Name uni fun ()
-> Either
     (CekEvaluationException Name uni fun) (Term Name uni fun ())
forall (uni :: * -> *) fun.
(Everywhere uni ExMemoryUsage, Ix fun, PrettyUni uni fun) =>
MachineParameters CekMachineCosts CekValue uni fun
-> Term Name uni fun ()
-> Either
     (CekEvaluationException Name uni fun) (Term Name uni fun ())
evaluateCekNoEmit MachineParameters CekMachineCosts CekValue uni fun
params (Term Name uni fun ()
 -> Either
      (CekEvaluationException Name uni fun) (Term Name uni fun ()))
-> (Term Name uni fun ()
    -> Either (CekEvaluationException Name uni fun) a)
-> Term Name uni fun ()
-> 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 err.
(ReadKnown val a, AsUnliftingError err, AsEvaluationFailure err) =>
val -> Either (ErrorWithCause err val) a
readKnownSelf