{-# LANGUAGE ImpredicativeTypes #-}

module Plutarch.Evaluate (
  E.evalScript,
  E.evalScriptHuge,
  E.evalScript',
  E.evalScriptUnlimited,
  evalTerm,
  evalTerm',
  unsafeEvalTerm,
  applyArguments,
) where

import Control.Lens.Combinators (over)
import Data.Kind (Type)
import Data.Text (Text)
import Plutarch.Internal.Evaluate qualified as E
import Plutarch.Internal.Term (
  Config,
  RawTerm (RCompiled),
  S,
  Term (..),
  TermResult (TermResult),
  compile,
 )
import Plutarch.Script (Script (Script))
import PlutusCore qualified as PLC (DefaultFun, DefaultUni, NamedDeBruijn)
import PlutusCore.Evaluation.Machine.ExBudget (ExBudget)
import PlutusCore.MkPlc (mkConstant, mkIterAppNoAnn)
import PlutusLedgerApi.Common (Data)
import UntypedPlutusCore qualified as UPLC
import UntypedPlutusCore.Evaluation.Machine.Cek qualified as Cek (CekEvaluationException)

-- | Compile and evaluate term.
evalTerm ::
  forall (a :: S -> Type).
  Config ->
  (forall (s0 :: S). Term s0 a) ->
  Either Text (Either (Cek.CekEvaluationException PLC.NamedDeBruijn PLC.DefaultUni PLC.DefaultFun) (forall (s1 :: S). Term s1 a), ExBudget, [Text])
evalTerm :: forall (a :: S -> Type).
Config
-> (forall (s0 :: S). Term s0 a)
-> Either
     Text
     (Either
        (CekEvaluationException NamedDeBruijn DefaultUni DefaultFun)
        (forall (s0 :: S). Term s0 a),
      ExBudget, [Text])
evalTerm Config
config forall (s0 :: S). Term s0 a
term =
  case Config -> (forall (s0 :: S). Term s0 a) -> Either Text Script
forall (a :: S -> Type).
Config -> (forall (s :: S). Term s a) -> Either Text Script
compile Config
config Term s a
forall (s0 :: S). Term s0 a
term of
    Right Script
script ->
      let (Either
  (CekEvaluationException NamedDeBruijn DefaultUni DefaultFun) Script
s, ExBudget
b, [Text]
t) = Script
-> (Either
      (CekEvaluationException NamedDeBruijn DefaultUni DefaultFun)
      Script,
    ExBudget, [Text])
E.evalScriptHuge Script
script
       in (Either
   (CekEvaluationException NamedDeBruijn DefaultUni DefaultFun)
   (forall (s0 :: S). Term s0 a),
 ExBudget, [Text])
-> Either
     Text
     (Either
        (CekEvaluationException NamedDeBruijn DefaultUni DefaultFun)
        (forall (s0 :: S). Term s0 a),
      ExBudget, [Text])
forall a b. b -> Either a b
Right (Script -> forall (s0 :: S). Term s0 a
fromScript (Script -> forall (s0 :: S). Term s0 a)
-> Either
     (CekEvaluationException NamedDeBruijn DefaultUni DefaultFun) Script
-> Either
     (CekEvaluationException NamedDeBruijn DefaultUni DefaultFun)
     (forall (s0 :: S). Term s0 a)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Either
  (CekEvaluationException NamedDeBruijn DefaultUni DefaultFun) Script
s, ExBudget
b, [Text]
t)
    Left Text
a -> Text
-> Either
     Text
     (Either
        (CekEvaluationException NamedDeBruijn DefaultUni DefaultFun)
        (forall (s0 :: S). Term s0 a),
      ExBudget, [Text])
forall a b. a -> Either a b
Left Text
a
  where
    fromScript :: Script -> (forall (s2 :: S). Term s2 a)
    fromScript :: Script -> forall (s0 :: S). Term s0 a
fromScript (Script Program DeBruijn DefaultUni DefaultFun ()
script) =
      (Word64 -> TermMonad TermResult) -> Term s2 a
forall (s :: S) (a :: S -> Type).
(Word64 -> TermMonad TermResult) -> Term s a
Term ((Word64 -> TermMonad TermResult) -> Term s2 a)
-> (Word64 -> TermMonad TermResult) -> Term s2 a
forall a b. (a -> b) -> a -> b
$ TermMonad TermResult -> Word64 -> TermMonad TermResult
forall a b. a -> b -> a
const (TermMonad TermResult -> Word64 -> TermMonad TermResult)
-> TermMonad TermResult -> Word64 -> TermMonad TermResult
forall a b. (a -> b) -> a -> b
$ TermResult -> TermMonad TermResult
forall a. a -> TermMonad a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (TermResult -> TermMonad TermResult)
-> TermResult -> TermMonad TermResult
forall a b. (a -> b) -> a -> b
$ RawTerm -> [HoistedTerm] -> TermResult
TermResult (Term DeBruijn DefaultUni DefaultFun () -> RawTerm
RCompiled (Term DeBruijn DefaultUni DefaultFun () -> RawTerm)
-> Term DeBruijn DefaultUni DefaultFun () -> RawTerm
forall a b. (a -> b) -> a -> b
$ Program DeBruijn DefaultUni DefaultFun ()
-> Term DeBruijn DefaultUni DefaultFun ()
forall name (uni :: Type -> Type) fun ann.
Program name uni fun ann -> Term name uni fun ann
UPLC._progTerm Program DeBruijn DefaultUni DefaultFun ()
script) []

-- | Same as `evalTerm` but without error handling
evalTerm' :: forall (a :: S -> Type). Config -> (forall (s0 :: S). Term s0 a) -> (forall (s1 :: S). Term s1 a)
evalTerm' :: forall (a :: S -> Type).
Config
-> (forall (s0 :: S). Term s0 a) -> forall (s0 :: S). Term s0 a
evalTerm' Config
config forall (s0 :: S). Term s0 a
term =
  case Config
-> (forall (s0 :: S). Term s0 a)
-> Either
     Text
     (Either
        (CekEvaluationException NamedDeBruijn DefaultUni DefaultFun)
        (forall (s0 :: S). Term s0 a),
      ExBudget, [Text])
forall (a :: S -> Type).
Config
-> (forall (s0 :: S). Term s0 a)
-> Either
     Text
     (Either
        (CekEvaluationException NamedDeBruijn DefaultUni DefaultFun)
        (forall (s0 :: S). Term s0 a),
      ExBudget, [Text])
evalTerm Config
config Term s0 a
forall (s0 :: S). Term s0 a
term of
    Right (Right forall (s0 :: S). Term s0 a
t, ExBudget
_, [Text]
_) -> Term s1 a
forall (s0 :: S). Term s0 a
t
    Left Text
err -> [Char] -> Term s1 a
forall a. HasCallStack => [Char] -> a
error ([Char] -> Term s1 a) -> [Char] -> Term s1 a
forall a b. (a -> b) -> a -> b
$ [Char]
"evalTerm' failed: " [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> Text -> [Char]
forall a. Show a => a -> [Char]
show Text
err
    Either
  Text
  (Either
     (CekEvaluationException NamedDeBruijn DefaultUni DefaultFun)
     (forall (s0 :: S). Term s0 a),
   ExBudget, [Text])
_ -> [Char] -> Term s1 a
forall a. HasCallStack => [Char] -> a
error [Char]
"evalTerm' failed"

{- | Compile and evaluate a closed term
Useful for pre-evaluating terms so that they can be used as constants in
an onchain script. Consider the following:
 _________________________________________________________________________
     term :: Term _ PInteger
     term = unsafeEvalTerm NoTracing foo

     foo :: Term s PInteger
     foo = (pconstant 1 #+ pconstant 5) #* pconstant 3

     bar :: Term s (PInteger :--> PInteger)
     bar = plam \x ->
       x + foo

     bar2 :: Term s (PInteger :--> PInteger)
     bar2 = plam \x ->
       x + term


    PI.compile PI.NoTracing bar
    Right (Script {unScript = Program {_progAnn = (), _progVer = Version {_versionMajor = 1, _versionMinor = 0, _versionPatch = 0}, _progTerm = LamAbs () (DeBruijn {dbnIndex = 0}) (Apply () (Apply () (Builtin () AddInteger) (Var () (DeBruijn {dbnIndex = 1}))) (Apply () (Apply () (Builtin () MultiplyInteger) (Apply () (Apply () (Builtin () AddInteger) (Constant () (Some (ValueOf DefaultUniInteger 1)))) (Constant () (Some (ValueOf DefaultUniInteger 5))))) (Constant () (Some (ValueOf DefaultUniInteger 3)))))}})
    PI.compile PI.NoTracing bar2
    Right (Script {unScript = Program {_progAnn = (), _progVer = Version {_versionMajor = 1, _versionMinor = 0, _versionPatch = 0}, _progTerm = LamAbs () (DeBruijn {dbnIndex = 0}) (Apply () (Apply () (Builtin () AddInteger) (Var () (DeBruijn {dbnIndex = 1}))) (Constant () (Some (ValueOf DefaultUniInteger 18))))}})
 _________________________________________________________________________

In bar, foo is an unevaluated term and thus must be evaluated. In bar2, foo has been
pre-evaluated with `unsafeEvalTerm` and thus appears as a constant.

Error if the compilation or evaluation fails.
-}
unsafeEvalTerm :: forall (a :: S -> Type). Config -> (forall (s0 :: S). Term s0 a) -> (forall (s1 :: S). Term s1 a)
unsafeEvalTerm :: forall (a :: S -> Type).
Config
-> (forall (s0 :: S). Term s0 a) -> forall (s0 :: S). Term s0 a
unsafeEvalTerm Config
c forall (s0 :: S). Term s0 a
t = Either
  Text
  (Either
     (CekEvaluationException NamedDeBruijn DefaultUni DefaultFun)
     (forall (s0 :: S). Term s0 a),
   ExBudget, [Text])
-> forall (s0 :: S). Term s0 a
extractResult (Either
   Text
   (Either
      (CekEvaluationException NamedDeBruijn DefaultUni DefaultFun)
      (forall (s0 :: S). Term s0 a),
    ExBudget, [Text])
 -> forall (s0 :: S). Term s0 a)
-> Either
     Text
     (Either
        (CekEvaluationException NamedDeBruijn DefaultUni DefaultFun)
        (forall (s0 :: S). Term s0 a),
      ExBudget, [Text])
-> forall (s0 :: S). Term s0 a
forall a b. (a -> b) -> a -> b
$ Config
-> (forall (s0 :: S). Term s0 a)
-> Either
     Text
     (Either
        (CekEvaluationException NamedDeBruijn DefaultUni DefaultFun)
        (forall (s0 :: S). Term s0 a),
      ExBudget, [Text])
forall (a :: S -> Type).
Config
-> (forall (s0 :: S). Term s0 a)
-> Either
     Text
     (Either
        (CekEvaluationException NamedDeBruijn DefaultUni DefaultFun)
        (forall (s0 :: S). Term s0 a),
      ExBudget, [Text])
evalTerm Config
c Term s0 a
forall (s0 :: S). Term s0 a
t
  where
    extractResult :: Either Text (Either (Cek.CekEvaluationException PLC.NamedDeBruijn PLC.DefaultUni PLC.DefaultFun) (forall (s2 :: S). Term s2 a), ExBudget, [Text]) -> (forall (s3 :: S). Term s3 a)
    extractResult :: Either
  Text
  (Either
     (CekEvaluationException NamedDeBruijn DefaultUni DefaultFun)
     (forall (s0 :: S). Term s0 a),
   ExBudget, [Text])
-> forall (s0 :: S). Term s0 a
extractResult (Right (Right forall (s0 :: S). Term s0 a
term, ExBudget
_, [Text]
_)) = Term s3 a
forall (s0 :: S). Term s0 a
term
    extractResult Either
  Text
  (Either
     (CekEvaluationException NamedDeBruijn DefaultUni DefaultFun)
     (forall (s0 :: S). Term s0 a),
   ExBudget, [Text])
_ = [Char] -> Term s3 a
forall a. HasCallStack => [Char] -> a
error [Char]
"unsafeEvalTerm: failed to evaluate or compile the term."

{- | Given a compiled 'Script' representing a function that takes arguments, and
a list of those 'Data'-encoded arguments, produce a new script with those
arguments applied.

@since 1.8.1
-}
applyArguments :: Script -> [Data] -> Script
applyArguments :: Script -> [Data] -> Script
applyArguments (Script Program DeBruijn DefaultUni DefaultFun ()
p) [Data]
args =
  let termArgs :: [Term DeBruijn DefaultUni DefaultFun ()]
termArgs = () -> Data -> Term DeBruijn DefaultUni DefaultFun ()
forall a (uni :: Type -> Type) fun (term :: Type -> Type) tyname
       name ann.
(TermLike term tyname name uni fun, HasTermLevel @Type uni a) =>
ann -> a -> term ann
mkConstant () (Data -> Term DeBruijn DefaultUni DefaultFun ())
-> [Data] -> [Term DeBruijn DefaultUni DefaultFun ()]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> [Data]
args
      applied :: Term DeBruijn DefaultUni DefaultFun ()
-> Term DeBruijn DefaultUni DefaultFun ()
applied Term DeBruijn DefaultUni DefaultFun ()
t = Term DeBruijn DefaultUni DefaultFun ()
-> [Term DeBruijn DefaultUni DefaultFun ()]
-> Term DeBruijn DefaultUni DefaultFun ()
forall (term :: Type -> Type) tyname name (uni :: Type -> Type)
       fun.
TermLike term tyname name uni fun =>
term () -> [term ()] -> term ()
mkIterAppNoAnn Term DeBruijn DefaultUni DefaultFun ()
t [Term DeBruijn DefaultUni DefaultFun ()]
termArgs
   in Program DeBruijn DefaultUni DefaultFun () -> Script
Script (Program DeBruijn DefaultUni DefaultFun () -> Script)
-> Program DeBruijn DefaultUni DefaultFun () -> Script
forall a b. (a -> b) -> a -> b
$ ASetter
  (Program DeBruijn DefaultUni DefaultFun ())
  (Program DeBruijn DefaultUni DefaultFun ())
  (Term DeBruijn DefaultUni DefaultFun ())
  (Term DeBruijn DefaultUni DefaultFun ())
-> (Term DeBruijn DefaultUni DefaultFun ()
    -> Term DeBruijn DefaultUni DefaultFun ())
-> Program DeBruijn DefaultUni DefaultFun ()
-> Program DeBruijn DefaultUni DefaultFun ()
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
over ASetter
  (Program DeBruijn DefaultUni DefaultFun ())
  (Program DeBruijn DefaultUni DefaultFun ())
  (Term DeBruijn DefaultUni DefaultFun ())
  (Term DeBruijn DefaultUni DefaultFun ())
forall name1 (uni1 :: Type -> Type) fun1 ann name2
       (uni2 :: Type -> Type) fun2 (f :: Type -> Type).
Functor f =>
(Term name1 uni1 fun1 ann -> f (Term name2 uni2 fun2 ann))
-> Program name1 uni1 fun1 ann -> f (Program name2 uni2 fun2 ann)
UPLC.progTerm Term DeBruijn DefaultUni DefaultFun ()
-> Term DeBruijn DefaultUni DefaultFun ()
applied Program DeBruijn DefaultUni DefaultFun ()
p