{-# LANGUAGE DataKinds        #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE TypeOperators    #-}

module Evaluation.Builtins.Common
    ( unsafeSplitStructuralOperational
    , evaluateCek
    , evaluateCekNoEmit
    , readKnownCek
    , typecheckAnd
    , typecheckEvaluateCek
    , typecheckEvaluateCekNoEmit
    , typecheckReadKnownCek
    ) where

import PlutusCore qualified as TPLC
import PlutusCore.Builtin
import PlutusCore.Compiler.Erase qualified as TPLC
import PlutusCore.Default
import PlutusCore.Evaluation.Machine.ExBudgetingDefaults
import PlutusCore.Evaluation.Machine.ExMemoryUsage
import PlutusCore.Evaluation.Machine.MachineParameters
import PlutusCore.Name.Unique
import PlutusCore.Pretty
import PlutusCore.TypeCheck

import UntypedPlutusCore qualified as UPLC
import UntypedPlutusCore.Evaluation.Machine.Cek

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

-- | Type check and evaluate a term.
typecheckAnd
    :: ( MonadError (TPLC.Error uni fun ()) m, TPLC.Typecheckable uni fun, GEq uni
       , Closed uni, uni `Everywhere` ExMemoryUsage
       )
    => BuiltinSemanticsVariant fun
    -> (MachineParameters CekMachineCosts fun (CekValue uni fun ()) ->
            UPLC.Term Name uni fun () -> a)
    -> CostingPart uni fun -> TPLC.Term TyName Name uni fun () -> m a
typecheckAnd :: forall (uni :: * -> *) fun (m :: * -> *) a.
(MonadError (Error uni fun ()) m, Typecheckable uni fun, GEq uni,
 Closed uni, Everywhere uni ExMemoryUsage) =>
BuiltinSemanticsVariant fun
-> (MachineParameters CekMachineCosts fun (CekValue uni fun ())
    -> Term Name uni fun () -> a)
-> CostingPart uni fun
-> Term TyName Name uni fun ()
-> m a
typecheckAnd BuiltinSemanticsVariant fun
semvar MachineParameters CekMachineCosts fun (CekValue uni fun ())
-> Term Name uni fun () -> a
action CostingPart uni fun
costingPart Term TyName Name uni fun ()
term = QuoteT m a -> m a
forall (m :: * -> *) a. Monad m => QuoteT m a -> m a
TPLC.runQuoteT (QuoteT m a -> m a) -> QuoteT m a -> m a
forall a b. (a -> b) -> a -> b
$ do
    -- Here we don't use 'getDefTypeCheckConfig', to cover the absurd case where
    -- builtins can change their type according to their 'BuiltinSemanticsVariant'.
    TypeCheckConfig uni fun
tcConfig <- KindCheckConfig -> BuiltinTypes uni fun -> TypeCheckConfig uni fun
forall (uni :: * -> *) fun.
KindCheckConfig -> BuiltinTypes uni fun -> TypeCheckConfig uni fun
TypeCheckConfig KindCheckConfig
defKindCheckConfig (BuiltinTypes uni fun -> TypeCheckConfig uni fun)
-> QuoteT m (BuiltinTypes uni fun)
-> QuoteT m (TypeCheckConfig uni fun)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> BuiltinSemanticsVariant fun
-> () -> QuoteT m (BuiltinTypes uni fun)
forall err term (uni :: * -> *) fun ann (m :: * -> *).
(MonadKindCheck err term uni fun ann m, Typecheckable uni fun) =>
BuiltinSemanticsVariant fun -> ann -> m (BuiltinTypes uni fun)
builtinMeaningsToTypes BuiltinSemanticsVariant fun
semvar ()
    Normalized (Type TyName uni ())
_ <- TypeCheckConfig uni fun
-> Term TyName Name uni fun ()
-> QuoteT m (Normalized (Type TyName uni ()))
forall err (uni :: * -> *) fun ann (m :: * -> *).
MonadTypeCheckPlc err uni fun ann m =>
TypeCheckConfig uni fun
-> Term TyName Name uni fun ann
-> m (Normalized (Type TyName uni ()))
TPLC.inferType TypeCheckConfig uni fun
tcConfig Term TyName Name uni fun ()
term
    a -> QuoteT m a
forall a. a -> QuoteT m a
forall (m :: * -> *) a. Monad m => a -> m a
return (a -> QuoteT m a)
-> (Term Name uni fun () -> a)
-> Term Name uni fun ()
-> QuoteT m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MachineParameters CekMachineCosts fun (CekValue uni fun ())
-> Term Name uni fun () -> a
action MachineParameters CekMachineCosts fun (CekValue uni fun ())
runtime (Term Name uni fun () -> QuoteT m a)
-> Term Name uni fun () -> QuoteT m a
forall a b. (a -> b) -> a -> b
$ Term TyName Name uni fun () -> Term Name uni fun ()
forall name tyname (uni :: * -> *) fun ann.
HasUnique name TermUnique =>
Term tyname name uni fun ann -> Term name uni fun ann
TPLC.eraseTerm Term TyName Name uni fun ()
term
    where
      runtime :: MachineParameters CekMachineCosts fun (CekValue uni fun ())
runtime = BuiltinSemanticsVariant fun
-> CostModel
     CekMachineCosts (CostingPart (UniOf (CekValue uni fun ())) fun)
-> MachineParameters CekMachineCosts fun (CekValue uni fun ())
forall (uni :: * -> *) fun builtincosts val machinecosts.
(CostingPart uni fun ~ builtincosts, HasMeaningIn uni val,
 ToBuiltinMeaning uni fun) =>
BuiltinSemanticsVariant fun
-> CostModel machinecosts builtincosts
-> MachineParameters machinecosts fun val
mkMachineParameters BuiltinSemanticsVariant fun
semvar (CostModel
   CekMachineCosts (CostingPart (UniOf (CekValue uni fun ())) fun)
 -> MachineParameters CekMachineCosts fun (CekValue uni fun ()))
-> CostModel
     CekMachineCosts (CostingPart (UniOf (CekValue uni fun ())) fun)
-> MachineParameters CekMachineCosts fun (CekValue uni fun ())
forall a b. (a -> b) -> a -> b
$
                -- FIXME: make sure we have the the correct cost model for the semantics variant.
                   CekMachineCosts
-> CostingPart (UniOf (CekValue uni fun ())) fun
-> CostModel
     CekMachineCosts (CostingPart (UniOf (CekValue uni fun ())) fun)
forall machinecosts builtincosts.
machinecosts -> builtincosts -> CostModel machinecosts builtincosts
CostModel CekMachineCosts
defaultCekMachineCostsForTesting CostingPart uni fun
CostingPart (UniOf (CekValue uni fun ())) fun
costingPart

-- | Type check and evaluate a term, logging enabled.
typecheckEvaluateCek
    :: ( MonadError (TPLC.Error uni fun ()) m, TPLC.Typecheckable uni fun, GEq uni
       , uni `Everywhere` ExMemoryUsage, PrettyUni uni, Pretty fun
       )
    => BuiltinSemanticsVariant fun
    -> CostingPart uni fun
    -> TPLC.Term TyName Name uni fun ()
    -> m (EvaluationResult (UPLC.Term Name uni fun ()), [Text])
typecheckEvaluateCek :: forall (uni :: * -> *) fun (m :: * -> *).
(MonadError (Error uni fun ()) m, Typecheckable uni fun, GEq uni,
 Everywhere uni ExMemoryUsage, PrettyUni uni, Pretty fun) =>
BuiltinSemanticsVariant fun
-> CostingPart uni fun
-> Term TyName Name uni fun ()
-> m (EvaluationResult (Term Name uni fun ()), [Text])
typecheckEvaluateCek BuiltinSemanticsVariant fun
semvar =
    BuiltinSemanticsVariant fun
-> (MachineParameters CekMachineCosts fun (CekValue uni fun ())
    -> Term Name uni fun ()
    -> (EvaluationResult (Term Name uni fun ()), [Text]))
-> CostingPart uni fun
-> Term TyName Name uni fun ()
-> m (EvaluationResult (Term Name uni fun ()), [Text])
forall (uni :: * -> *) fun (m :: * -> *) a.
(MonadError (Error uni fun ()) m, Typecheckable uni fun, GEq uni,
 Closed uni, Everywhere uni ExMemoryUsage) =>
BuiltinSemanticsVariant fun
-> (MachineParameters CekMachineCosts fun (CekValue uni fun ())
    -> Term Name uni fun () -> a)
-> CostingPart uni fun
-> Term TyName Name uni fun ()
-> m a
typecheckAnd BuiltinSemanticsVariant fun
semvar ((MachineParameters CekMachineCosts fun (CekValue uni fun ())
  -> Term Name uni fun ()
  -> (EvaluationResult (Term Name uni fun ()), [Text]))
 -> CostingPart uni fun
 -> Term TyName Name uni fun ()
 -> m (EvaluationResult (Term Name uni fun ()), [Text]))
-> (MachineParameters CekMachineCosts fun (CekValue uni fun ())
    -> Term Name uni fun ()
    -> (EvaluationResult (Term Name uni fun ()), [Text]))
-> CostingPart uni fun
-> Term TyName Name uni fun ()
-> m (EvaluationResult (Term Name uni fun ()), [Text])
forall a b. (a -> b) -> a -> b
$ \MachineParameters CekMachineCosts fun (CekValue uni fun ())
params ->
        (Either
   (EvaluationException
      (MachineError fun) CekUserError (Term Name uni fun ()))
   (Term Name uni fun ())
 -> EvaluationResult (Term Name uni fun ()))
-> (Either
      (EvaluationException
         (MachineError fun) CekUserError (Term Name uni fun ()))
      (Term Name uni fun ()),
    [Text])
-> (EvaluationResult (Term Name uni fun ()), [Text])
forall a b c. (a -> b) -> (a, c) -> (b, c)
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first Either
  (EvaluationException
     (MachineError fun) CekUserError (Term Name uni fun ()))
  (Term Name uni fun ())
-> EvaluationResult (Term Name uni fun ())
forall structural term operational a.
(PrettyPlc structural, PrettyPlc term, Typeable structural,
 Typeable term) =>
Either (EvaluationException structural operational term) a
-> EvaluationResult a
unsafeSplitStructuralOperational ((Either
    (EvaluationException
       (MachineError fun) CekUserError (Term Name uni fun ()))
    (Term Name uni fun ()),
  [Text])
 -> (EvaluationResult (Term Name uni fun ()), [Text]))
-> (Term Name uni fun ()
    -> (Either
          (EvaluationException
             (MachineError fun) CekUserError (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 fun (CekValue uni fun ())
-> Term Name uni fun ()
-> (Either
      (EvaluationException
         (MachineError fun) CekUserError (Term Name uni fun ()))
      (Term Name uni fun ()),
    [Text])
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 EmitterMode uni fun
forall (uni :: * -> *) fun. EmitterMode uni fun
logEmitter MachineParameters CekMachineCosts fun (CekValue uni fun ())
params

-- | Type check and evaluate a term, logging disabled.
typecheckEvaluateCekNoEmit
    :: ( MonadError (TPLC.Error uni fun ()) m, TPLC.Typecheckable uni fun, GEq uni
       , uni `Everywhere` ExMemoryUsage, PrettyUni uni, Pretty fun
       )
    => BuiltinSemanticsVariant fun
    -> CostingPart uni fun
    -> TPLC.Term TyName Name uni fun ()
    -> m (EvaluationResult (UPLC.Term Name uni fun ()))
typecheckEvaluateCekNoEmit :: forall (uni :: * -> *) fun (m :: * -> *).
(MonadError (Error uni fun ()) m, Typecheckable uni fun, GEq uni,
 Everywhere uni ExMemoryUsage, PrettyUni uni, Pretty fun) =>
BuiltinSemanticsVariant fun
-> CostingPart uni fun
-> Term TyName Name uni fun ()
-> m (EvaluationResult (Term Name uni fun ()))
typecheckEvaluateCekNoEmit BuiltinSemanticsVariant fun
semvar =
    BuiltinSemanticsVariant fun
-> (MachineParameters CekMachineCosts fun (CekValue uni fun ())
    -> Term Name uni fun () -> EvaluationResult (Term Name uni fun ()))
-> CostingPart uni fun
-> Term TyName Name uni fun ()
-> m (EvaluationResult (Term Name uni fun ()))
forall (uni :: * -> *) fun (m :: * -> *) a.
(MonadError (Error uni fun ()) m, Typecheckable uni fun, GEq uni,
 Closed uni, Everywhere uni ExMemoryUsage) =>
BuiltinSemanticsVariant fun
-> (MachineParameters CekMachineCosts fun (CekValue uni fun ())
    -> Term Name uni fun () -> a)
-> CostingPart uni fun
-> Term TyName Name uni fun ()
-> m a
typecheckAnd BuiltinSemanticsVariant fun
semvar ((MachineParameters CekMachineCosts fun (CekValue uni fun ())
  -> Term Name uni fun () -> EvaluationResult (Term Name uni fun ()))
 -> CostingPart uni fun
 -> Term TyName Name uni fun ()
 -> m (EvaluationResult (Term Name uni fun ())))
-> (MachineParameters CekMachineCosts fun (CekValue uni fun ())
    -> Term Name uni fun () -> EvaluationResult (Term Name uni fun ()))
-> CostingPart uni fun
-> Term TyName Name uni fun ()
-> m (EvaluationResult (Term Name uni fun ()))
forall a b. (a -> b) -> a -> b
$ \MachineParameters CekMachineCosts fun (CekValue uni fun ())
params ->
        Either
  (EvaluationException
     (MachineError fun) CekUserError (Term Name uni fun ()))
  (Term Name uni fun ())
-> EvaluationResult (Term Name uni fun ())
forall structural term operational a.
(PrettyPlc structural, PrettyPlc term, Typeable structural,
 Typeable term) =>
Either (EvaluationException structural operational term) a
-> EvaluationResult a
unsafeSplitStructuralOperational (Either
   (EvaluationException
      (MachineError fun) CekUserError (Term Name uni fun ()))
   (Term Name uni fun ())
 -> EvaluationResult (Term Name uni fun ()))
-> (Term Name uni fun ()
    -> Either
         (EvaluationException
            (MachineError fun) CekUserError (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 fun (CekValue uni fun ())
-> Term Name uni fun ()
-> Either
     (EvaluationException
        (MachineError fun) CekUserError (Term Name uni fun ()))
     (Term Name uni fun ())
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 MachineParameters CekMachineCosts fun (CekValue uni fun ())
params

-- | Type check and convert a Plutus Core term to a Haskell value.
typecheckReadKnownCek
    :: ( MonadError (TPLC.Error uni fun ()) m, TPLC.Typecheckable uni fun, GEq uni
       , uni `Everywhere` ExMemoryUsage, PrettyUni uni, Pretty fun
       , ReadKnown (UPLC.Term Name uni fun ()) a
       )
    => BuiltinSemanticsVariant fun
    -> CostingPart uni fun
    -> TPLC.Term TyName Name uni fun ()
    -> m (Either (CekEvaluationException Name uni fun) a)
typecheckReadKnownCek :: forall (uni :: * -> *) fun (m :: * -> *) a.
(MonadError (Error uni fun ()) m, Typecheckable uni fun, GEq uni,
 Everywhere uni ExMemoryUsage, PrettyUni uni, Pretty fun,
 ReadKnown (Term Name uni fun ()) a) =>
BuiltinSemanticsVariant fun
-> CostingPart uni fun
-> Term TyName Name uni fun ()
-> m (Either (CekEvaluationException Name uni fun) a)
typecheckReadKnownCek BuiltinSemanticsVariant fun
semvar =
    BuiltinSemanticsVariant fun
-> (MachineParameters CekMachineCosts fun (CekValue uni fun ())
    -> Term Name uni fun ()
    -> Either (CekEvaluationException Name uni fun) a)
-> CostingPart uni fun
-> Term TyName Name uni fun ()
-> m (Either (CekEvaluationException Name uni fun) a)
forall (uni :: * -> *) fun (m :: * -> *) a.
(MonadError (Error uni fun ()) m, Typecheckable uni fun, GEq uni,
 Closed uni, Everywhere uni ExMemoryUsage) =>
BuiltinSemanticsVariant fun
-> (MachineParameters CekMachineCosts fun (CekValue uni fun ())
    -> Term Name uni fun () -> a)
-> CostingPart uni fun
-> Term TyName Name uni fun ()
-> m a
typecheckAnd BuiltinSemanticsVariant fun
semvar MachineParameters CekMachineCosts fun (CekValue uni fun ())
-> Term Name uni fun ()
-> Either (CekEvaluationException Name uni fun) a
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