{-# 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 PlutusIR.Contexts
import PlutusIR.Core

import Control.Lens (transformOf, (^.))
import Data.Functor (void)
import PlutusCore qualified as PLC
import PlutusCore.Name.Unique (HasUnique, TermUnique, TypeUnique)
import PlutusIR.Analysis.Builtins
import PlutusIR.Analysis.VarInfo (VarsInfo, termVarInfo)
import PlutusIR.Pass
import PlutusIR.Purity (isPure)
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,
 HasUnique name TermUnique, HasUnique tyname TypeUnique) =>
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
     , HasUnique name TermUnique
     , HasUnique tyname TypeUnique
     )
  => 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,
 HasUnique name TermUnique, HasUnique tyname TypeUnique) =>
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 Term tyname name uni fun a
term = 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 Term tyname name uni fun a
term
  where
    vinfo :: VarsInfo tyname name uni a
    vinfo :: VarsInfo tyname name uni a
vinfo = Term tyname name uni fun a -> VarsInfo tyname name uni a
forall name tyname (uni :: * -> *) fun a.
(HasUnique name TermUnique, HasUnique tyname TypeUnique) =>
Term tyname name uni fun a -> VarsInfo tyname name uni a
termVarInfo Term tyname name uni fun a
term

    -- 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 (Term tyname name uni fun ())
getFXs) AppContext tyname name uni fun a
AppContextEnd =
      case BuiltinResult (Term tyname name uni fun ())
getFXs of
        BuiltinSuccess Term tyname name uni fun ()
y -> Term tyname name uni fun () -> Maybe (Term tyname name uni fun ())
forall a. a -> Maybe a
Just Term tyname name uni fun ()
y
        -- 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
_ Term tyname name uni fun ()
y -> 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 ()
y
        -- 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
    -- See Note [Evaluating builtins with impure arguments]
    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)
      | BuiltinsInfo uni fun
-> VarsInfo tyname name uni a -> Term tyname name uni fun a -> Bool
forall (uni :: * -> *) fun name tyname a.
(ToBuiltinMeaning uni fun, HasUnique name TermUnique) =>
BuiltinsInfo uni fun
-> VarsInfo tyname name uni a -> Term tyname name uni fun a -> Bool
isPure BuiltinsInfo uni fun
binfo VarsInfo tyname name uni a
vinfo Term tyname name uni fun a
arg =
          -- 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

{- Note [Evaluating builtins with impure arguments]

Some builtins take opaque arguments (for documentation on what "opaque" means,
see Note [How to add a built-in function: complicated cases]). By definition,
the values of these arguments are not inspected when evaluating the builtin,
therefore applying the denotation of the builtin will succeed regardless of the
actual values of the arguments. Evaluation order is handled externally, in the
CEK machine, and not in the builtin machinery. Since UPLC is strict, the CEK
machine takes care of evaluating arguments first.

For example, when evaluating `ifThenElse True 7 (divideInteger 1 x)`, the CEK
machine will attempt to evaluate `divideInteger 1 x` before applying `ifThenElse`.
Of course, when `x` is `0` evaluation fails and the program reduces to `error`.

However, when constant folding at compile time, there may not be a concrete
value for `x` yet. Since a builtin taking opaque arguments does not inspect them,
applying its denotation will succeed regardless of their actual values.
This is not sound in a strict language, and we can preserve the correct order of
side effects by only folding a builtin when its arguments are pure.
-}