{-# LANGUAGE LambdaCase          #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE ViewPatterns        #-}
-- | A pass that tries to evaluate builtin applications in the program.
--
-- This functions as a generic constant-folding pass, but which handles
-- arbitrary builtins.
module PlutusIR.Transform.EvaluateBuiltins
    ( evaluateBuiltins
    , evaluateBuiltinsPass
    ) where

import PlutusCore.Builtin
import PlutusCore.MkPlc (headSpineToTerm)
import PlutusIR.Contexts
import PlutusIR.Core

import Control.Lens (transformOf, (^.))
import Data.Functor (void)
import PlutusCore qualified as PLC
import PlutusIR.Analysis.Builtins
import PlutusIR.Pass
import PlutusIR.TypeCheck qualified as TC

evaluateBuiltinsPass :: (PLC.Typecheckable uni fun, PLC.GEq uni, Applicative m)
  => TC.PirTCConfig uni fun
  -> Bool
  -- ^ Whether to be conservative and try to retain logging behaviour.
  -> BuiltinsInfo uni fun
  -> CostingPart uni fun
  -> Pass m TyName Name uni fun a
evaluateBuiltinsPass :: forall (uni :: * -> *) fun (m :: * -> *) a.
(Typecheckable uni fun, GEq uni, Applicative m) =>
PirTCConfig uni fun
-> Bool
-> BuiltinsInfo uni fun
-> CostingPart uni fun
-> Pass m TyName Name uni fun a
evaluateBuiltinsPass PirTCConfig uni fun
tcconfig Bool
preserveLogging BuiltinsInfo uni fun
binfo CostingPart uni fun
costModel =
  String
-> Pass m TyName Name uni fun a -> Pass m TyName Name uni fun a
forall (m :: * -> *) tyname name (uni :: * -> *) fun a.
String
-> Pass m tyname name uni fun a -> Pass m tyname name uni fun a
NamedPass String
"evaluate builtins" (Pass m TyName Name uni fun a -> Pass m TyName Name uni fun a)
-> Pass m TyName Name uni fun a -> Pass m TyName Name uni fun a
forall a b. (a -> b) -> a -> b
$
    (Term TyName Name uni fun a -> m (Term TyName Name uni fun a))
-> [Condition TyName Name uni fun a]
-> [BiCondition TyName Name uni fun a]
-> Pass m TyName Name uni fun a
forall (m :: * -> *) tyname name (uni :: * -> *) fun a.
(Term tyname name uni fun a -> m (Term tyname name uni fun a))
-> [Condition tyname name uni fun a]
-> [BiCondition tyname name uni fun a]
-> Pass m tyname name uni fun a
Pass
      (Term TyName Name uni fun a -> m (Term TyName Name uni fun a)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Term TyName Name uni fun a -> m (Term TyName Name uni fun a))
-> (Term TyName Name uni fun a -> Term TyName Name uni fun a)
-> Term TyName Name uni fun a
-> m (Term TyName Name uni fun a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool
-> BuiltinsInfo uni fun
-> CostingPart uni fun
-> Term TyName Name uni fun a
-> Term TyName Name uni fun a
forall tyname name (uni :: * -> *) fun a.
(ToBuiltinMeaning uni fun, Typeable tyname, Typeable name) =>
Bool
-> BuiltinsInfo uni fun
-> CostingPart uni fun
-> Term tyname name uni fun a
-> Term tyname name uni fun a
evaluateBuiltins Bool
preserveLogging BuiltinsInfo uni fun
binfo CostingPart uni fun
costModel)
      [PirTCConfig uni fun -> Condition TyName Name uni fun a
forall (uni :: * -> *) fun a.
(Typecheckable uni fun, GEq uni) =>
PirTCConfig uni fun -> Condition TyName Name uni fun a
Typechecks PirTCConfig uni fun
tcconfig]
      [Condition TyName Name uni fun a
-> BiCondition TyName Name uni fun a
forall tyname name (uni :: * -> *) fun a.
Condition tyname name uni fun a
-> BiCondition tyname name uni fun a
ConstCondition (PirTCConfig uni fun -> Condition TyName Name uni fun a
forall (uni :: * -> *) fun a.
(Typecheckable uni fun, GEq uni) =>
PirTCConfig uni fun -> Condition TyName Name uni fun a
Typechecks PirTCConfig uni fun
tcconfig)]

evaluateBuiltins
  :: forall tyname name uni fun a
  . (ToBuiltinMeaning uni fun
  , Typeable tyname
  , Typeable name)
  => Bool
  -- ^ Whether to be conservative and try to retain logging behaviour.
  -> BuiltinsInfo uni fun
  -> CostingPart uni fun
  -> Term tyname name uni fun a
  -> Term tyname name uni fun a
evaluateBuiltins :: forall tyname name (uni :: * -> *) fun a.
(ToBuiltinMeaning uni fun, Typeable tyname, Typeable name) =>
Bool
-> BuiltinsInfo uni fun
-> CostingPart uni fun
-> Term tyname name uni fun a
-> Term tyname name uni fun a
evaluateBuiltins Bool
preserveLogging BuiltinsInfo uni fun
binfo CostingPart uni fun
costModel = ASetter
  (Term tyname name uni fun a)
  (Term tyname name uni fun a)
  (Term tyname name uni fun a)
  (Term tyname name uni fun a)
-> (Term tyname name uni fun a -> Term tyname name uni fun a)
-> Term tyname name uni fun a
-> Term tyname name uni fun a
forall a b. ASetter a b a b -> (b -> b) -> a -> b
transformOf ASetter
  (Term tyname name uni fun a)
  (Term tyname name uni fun a)
  (Term tyname name uni fun a)
  (Term tyname name uni fun a)
forall tyname name (uni :: * -> *) fun a (f :: * -> *).
Applicative f =>
(Term tyname name uni fun a -> f (Term tyname name uni fun a))
-> Term tyname name uni fun a -> f (Term tyname name uni fun a)
termSubterms Term tyname name uni fun a -> Term tyname name uni fun a
processTerm
  where
    -- Nothing means "leave the original term as it was"
    eval
      :: BuiltinRuntime (Term tyname name uni fun ())
      -> AppContext tyname name uni fun a
      -> Maybe (Term tyname name uni fun ())
    eval :: BuiltinRuntime (Term tyname name uni fun ())
-> AppContext tyname name uni fun a
-> Maybe (Term tyname name uni fun ())
eval (BuiltinCostedResult ExBudgetStream
_ BuiltinResult (HeadSpine (Term tyname name uni fun ()))
getFXs) AppContext tyname name uni fun a
AppContextEnd =
        case BuiltinResult (HeadSpine (Term tyname name uni fun ()))
getFXs of
            BuiltinSuccess HeadSpine (Term tyname name uni fun ())
fXs -> Term tyname name uni fun () -> Maybe (Term tyname name uni fun ())
forall a. a -> Maybe a
Just (Term tyname name uni fun ()
 -> Maybe (Term tyname name uni fun ()))
-> Term tyname name uni fun ()
-> Maybe (Term tyname name uni fun ())
forall a b. (a -> b) -> a -> b
$ HeadSpine (Term tyname name uni fun ())
-> Term tyname name uni fun ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun.
TermLike term tyname name uni fun =>
HeadSpine (term ()) -> term ()
headSpineToTerm HeadSpine (Term tyname name uni fun ())
fXs
            -- Evaluates successfully, but does logging. If we're being conservative
            -- then we should leave these in, so we don't remove people's logging!
            -- Otherwise `trace "hello" x` is a prime candidate for evaluation!
            BuiltinSuccessWithLogs DList Text
_ HeadSpine (Term tyname name uni fun ())
fXs ->
                if Bool
preserveLogging then Maybe (Term tyname name uni fun ())
forall a. Maybe a
Nothing else Term tyname name uni fun () -> Maybe (Term tyname name uni fun ())
forall a. a -> Maybe a
Just (Term tyname name uni fun ()
 -> Maybe (Term tyname name uni fun ()))
-> Term tyname name uni fun ()
-> Maybe (Term tyname name uni fun ())
forall a b. (a -> b) -> a -> b
$ HeadSpine (Term tyname name uni fun ())
-> Term tyname name uni fun ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun.
TermLike term tyname name uni fun =>
HeadSpine (term ()) -> term ()
headSpineToTerm HeadSpine (Term tyname name uni fun ())
fXs
            -- Evaluation failure. This can mean that the evaluation legitimately
            -- failed (e.g. `divideInteger 1 0`), or that it failed because the
            -- argument terms are not currently in the right form (because they're
            -- not evaluated, we're in the middle of a term here!). Since we can't
            -- distinguish these, we have to assume it's the latter case and just leave
            -- things alone.
            BuiltinFailure{} -> Maybe (Term tyname name uni fun ())
forall a. Maybe a
Nothing
    eval (BuiltinExpectArgument Term tyname name uni fun ()
-> BuiltinRuntime (Term tyname name uni fun ())
toRuntime) (TermAppContext Term tyname name uni fun a
arg a
_ AppContext tyname name uni fun a
ctx) =
        -- Builtin evaluation does not work with annotations, so we have to throw
        -- the argument annotation away here
        BuiltinRuntime (Term tyname name uni fun ())
-> AppContext tyname name uni fun a
-> Maybe (Term tyname name uni fun ())
eval (Term tyname name uni fun ()
-> BuiltinRuntime (Term tyname name uni fun ())
toRuntime (Term tyname name uni fun ()
 -> BuiltinRuntime (Term tyname name uni fun ()))
-> Term tyname name uni fun ()
-> BuiltinRuntime (Term tyname name uni fun ())
forall a b. (a -> b) -> a -> b
$ Term tyname name uni fun a -> Term tyname name uni fun ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void Term tyname name uni fun a
arg) AppContext tyname name uni fun a
ctx
    eval (BuiltinExpectForce BuiltinRuntime (Term tyname name uni fun ())
runtime) (TypeAppContext Type tyname uni a
_ a
_ AppContext tyname name uni fun a
ctx) =
        BuiltinRuntime (Term tyname name uni fun ())
-> AppContext tyname name uni fun a
-> Maybe (Term tyname name uni fun ())
eval BuiltinRuntime (Term tyname name uni fun ())
runtime AppContext tyname name uni fun a
ctx
    -- arg mismatch, including under-application, just leave it alone
    eval BuiltinRuntime (Term tyname name uni fun ())
_ AppContext tyname name uni fun a
_ = Maybe (Term tyname name uni fun ())
forall a. Maybe a
Nothing

    processTerm :: Term tyname name uni fun a -> Term tyname name uni fun a
    -- See Note [Context splitting in a recursive pass]
    processTerm :: Term tyname name uni fun a -> Term tyname name uni fun a
processTerm t :: Term tyname name uni fun a
t@(Term tyname name uni fun a
-> (Term tyname name uni fun a, AppContext tyname name uni fun a)
forall tyname name (uni :: * -> *) fun ann.
Term tyname name uni fun ann
-> (Term tyname name uni fun ann,
    AppContext tyname name uni fun ann)
splitApplication -> (Builtin a
x fun
bn, AppContext tyname name uni fun a
argCtx)) =
      let runtime :: BuiltinRuntime (Term tyname name uni fun ())
runtime = CostingPart uni fun
-> BuiltinMeaning
     (Term tyname name uni fun ()) (CostingPart uni fun)
-> BuiltinRuntime (Term tyname name uni fun ())
forall cost val.
cost -> BuiltinMeaning val cost -> BuiltinRuntime val
toBuiltinRuntime CostingPart uni fun
costModel (BuiltinSemanticsVariant fun
-> fun
-> BuiltinMeaning
     (Term tyname name uni fun ())
     (CostingPart (UniOf (Term tyname name uni fun ())) fun)
forall val.
HasMeaningIn (UniOf (Term tyname name uni fun ())) val =>
BuiltinSemanticsVariant fun
-> fun
-> BuiltinMeaning
     val (CostingPart (UniOf (Term tyname name uni fun ())) fun)
forall (uni :: * -> *) fun val.
(ToBuiltinMeaning uni fun, HasMeaningIn uni val) =>
BuiltinSemanticsVariant fun
-> fun -> BuiltinMeaning val (CostingPart uni fun)
toBuiltinMeaning (BuiltinsInfo uni fun
binfo BuiltinsInfo uni fun
-> Getting
     (BuiltinSemanticsVariant fun)
     (BuiltinsInfo uni fun)
     (BuiltinSemanticsVariant fun)
-> BuiltinSemanticsVariant fun
forall s a. s -> Getting a s a -> a
^. Getting
  (BuiltinSemanticsVariant fun)
  (BuiltinsInfo uni fun)
  (BuiltinSemanticsVariant fun)
forall (uni :: * -> *) fun (f :: * -> *).
Functor f =>
(BuiltinSemanticsVariant fun -> f (BuiltinSemanticsVariant fun))
-> BuiltinsInfo uni fun -> f (BuiltinsInfo uni fun)
biSemanticsVariant) fun
bn)
      in case BuiltinRuntime (Term tyname name uni fun ())
-> AppContext tyname name uni fun a
-> Maybe (Term tyname name uni fun ())
eval BuiltinRuntime (Term tyname name uni fun ())
runtime AppContext tyname name uni fun a
argCtx of
           -- Builtin evaluation gives us a fresh term with no annotation.
           -- Use the annotation of the builtin node, arbitrarily. This is slightly
           -- suboptimal, e.g. in `ifThenElse True x y`, we will get back `x`, but
           -- with the annotation that was on the `ifThenElse` node. But we can't
           -- easily do better.
           -- See Note [Unserializable constants]
           Just Term tyname name uni fun ()
t' | BuiltinsInfo uni fun -> Term tyname name uni fun () -> Bool
forall (uni :: * -> *) fun tyname name a.
BuiltinsInfo uni fun -> Term tyname name uni fun a -> Bool
termIsSerializable BuiltinsInfo uni fun
binfo Term tyname name uni fun ()
t' -> a
x a -> Term tyname name uni fun () -> Term tyname name uni fun a
forall a b.
a -> Term tyname name uni fun b -> Term tyname name uni fun a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Term tyname name uni fun ()
t'
           Maybe (Term tyname name uni fun ())
_                                     -> Term tyname name uni fun a
t
    processTerm Term tyname name uni fun a
t = Term tyname name uni fun a
t