{-# LANGUAGE GADTs               #-}
{-# LANGUAGE LambdaCase          #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications    #-}
{-# LANGUAGE TypeOperators       #-}
module PlutusIR.Purity (isPure) where

import PlutusIR

import PlutusCore.Builtin

-- | An argument taken by a builtin: could be a term of a type.
data Arg tyname name uni fun a = TypeArg (Type tyname uni a) | TermArg (Term tyname name uni fun a)

-- | A (not necessarily saturated) builtin application, consisting of the builtin and the arguments it has been applied to.
data BuiltinApp tyname name uni fun a = BuiltinApp fun [Arg tyname name uni fun a]

saturatesScheme ::  [Arg tyname name uni fun a] -> TypeScheme val args res -> Maybe Bool
-- We've passed enough arguments that the builtin will reduce. Note that this also accepts over-applied builtins.
saturatesScheme :: [Arg tyname name uni fun a]
-> TypeScheme val args res -> Maybe Bool
saturatesScheme [Arg tyname name uni fun a]
_ TypeSchemeResult{}                     = Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
True
-- Consume one argument
saturatesScheme (TermArg Term tyname name uni fun a
_ : [Arg tyname name uni fun a]
args) (TypeSchemeArrow TypeScheme val args res
sch) = [Arg tyname name uni fun a]
-> TypeScheme val args res -> Maybe Bool
forall tyname name (uni :: * -> *) fun a val (args :: [*]) res.
[Arg tyname name uni fun a]
-> TypeScheme val args res -> Maybe Bool
saturatesScheme [Arg tyname name uni fun a]
args TypeScheme val args res
sch
saturatesScheme (TypeArg Type tyname uni a
_ : [Arg tyname name uni fun a]
args) (TypeSchemeAll Proxy '(text, uniq, kind)
_ TypeScheme val args res
sch) = [Arg tyname name uni fun a]
-> TypeScheme val args res -> Maybe Bool
forall tyname name (uni :: * -> *) fun a val (args :: [*]) res.
[Arg tyname name uni fun a]
-> TypeScheme val args res -> Maybe Bool
saturatesScheme [Arg tyname name uni fun a]
args TypeScheme val args res
sch
-- Under-applied, not saturated
saturatesScheme [] TypeSchemeArrow{}                     = Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
False
saturatesScheme [] TypeSchemeAll{}                       = Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
False
-- These cases are only possible in case we have an ill-typed builtin application, so we can't give an answer.
saturatesScheme (TypeArg Type tyname uni a
_ : [Arg tyname name uni fun a]
_) TypeSchemeArrow{}        = Maybe Bool
forall a. Maybe a
Nothing
saturatesScheme (TermArg Term tyname name uni fun a
_ : [Arg tyname name uni fun a]
_) TypeSchemeAll{}          = Maybe Bool
forall a. Maybe a
Nothing

-- | Is the given 'BuiltinApp' saturated? Returns 'Nothing' if something is badly wrong and we can't tell.
isSaturated
    :: forall tyname name uni fun a
    . ToBuiltinMeaning uni fun
    => BuiltinApp tyname name uni fun a
    -> Maybe Bool
isSaturated :: BuiltinApp tyname name uni fun a -> Maybe Bool
isSaturated (BuiltinApp fun
fun [Arg tyname name uni fun a]
args) =
    case fun
-> BuiltinMeaning
     (Term TyName Name uni fun ()) (CostingPart uni fun)
forall (uni :: * -> *) fun val.
(ToBuiltinMeaning uni fun, HasConstantIn uni val) =>
fun -> BuiltinMeaning val (CostingPart uni fun)
toBuiltinMeaning @uni @fun @(Term TyName Name uni fun ()) fun
fun of
        BuiltinMeaning TypeScheme (Term TyName Name uni fun ()) args res
sch FoldArgs args res
_ BuiltinRuntimeOptions
  (Length args) (Term TyName Name uni fun ()) (CostingPart uni fun)
_ -> [Arg tyname name uni fun a]
-> TypeScheme (Term TyName Name uni fun ()) args res -> Maybe Bool
forall tyname name (uni :: * -> *) fun a val (args :: [*]) res.
[Arg tyname name uni fun a]
-> TypeScheme val args res -> Maybe Bool
saturatesScheme [Arg tyname name uni fun a]
args TypeScheme (Term TyName Name uni fun ()) args res
sch

-- | View a 'Term' as a 'BuiltinApp' if possible.
asBuiltinApp :: Term tyname name uni fun a -> Maybe (BuiltinApp tyname name uni fun a)
asBuiltinApp :: Term tyname name uni fun a
-> Maybe (BuiltinApp tyname name uni fun a)
asBuiltinApp = [Arg tyname name uni fun a]
-> Term tyname name uni fun a
-> Maybe (BuiltinApp tyname name uni fun a)
forall tyname name (uni :: * -> *) fun a.
[Arg tyname name uni fun a]
-> Term tyname name uni fun a
-> Maybe (BuiltinApp tyname name uni fun a)
go []
    where
        go :: [Arg tyname name uni fun a]
-> Term tyname name uni fun a
-> Maybe (BuiltinApp tyname name uni fun a)
go [Arg tyname name uni fun a]
argsSoFar = \case
            Apply a
_ Term tyname name uni fun a
t Term tyname name uni fun a
arg  -> [Arg tyname name uni fun a]
-> Term tyname name uni fun a
-> Maybe (BuiltinApp tyname name uni fun a)
go (Term tyname name uni fun a -> Arg tyname name uni fun a
forall tyname name (uni :: * -> *) fun a.
Term tyname name uni fun a -> Arg tyname name uni fun a
TermArg Term tyname name uni fun a
argArg tyname name uni fun a
-> [Arg tyname name uni fun a] -> [Arg tyname name uni fun a]
forall a. a -> [a] -> [a]
:[Arg tyname name uni fun a]
argsSoFar) Term tyname name uni fun a
t
            TyInst a
_ Term tyname name uni fun a
t Type tyname uni a
arg -> [Arg tyname name uni fun a]
-> Term tyname name uni fun a
-> Maybe (BuiltinApp tyname name uni fun a)
go (Type tyname uni a -> Arg tyname name uni fun a
forall tyname name (uni :: * -> *) fun a.
Type tyname uni a -> Arg tyname name uni fun a
TypeArg Type tyname uni a
argArg tyname name uni fun a
-> [Arg tyname name uni fun a] -> [Arg tyname name uni fun a]
forall a. a -> [a] -> [a]
:[Arg tyname name uni fun a]
argsSoFar) Term tyname name uni fun a
t
            Builtin a
_ fun
b    -> BuiltinApp tyname name uni fun a
-> Maybe (BuiltinApp tyname name uni fun a)
forall a. a -> Maybe a
Just (BuiltinApp tyname name uni fun a
 -> Maybe (BuiltinApp tyname name uni fun a))
-> BuiltinApp tyname name uni fun a
-> Maybe (BuiltinApp tyname name uni fun a)
forall a b. (a -> b) -> a -> b
$ fun
-> [Arg tyname name uni fun a] -> BuiltinApp tyname name uni fun a
forall tyname name (uni :: * -> *) fun a.
fun
-> [Arg tyname name uni fun a] -> BuiltinApp tyname name uni fun a
BuiltinApp fun
b [Arg tyname name uni fun a]
argsSoFar
            Term tyname name uni fun a
_              -> Maybe (BuiltinApp tyname name uni fun a)
forall a. Maybe a
Nothing

{- Note [Purity, strictness, and variables]
Variables in PLC won't have effects: they can have something else substituted for them, but those will be fully evaluated already.
However, in PIR we have non-strict variable bindings. References to non-strict variables *can* have effects - after all,
they compile into an application.

So we need to take this into account in our purity calculation. We require the user to tell us which variables are strict, this
must be *conservative* (i.e. if you don't know, it's non-strict).
-}

-- | Will evaluating this term have side effects (looping or error)?. This is slightly wider than the definition of a value, as
-- it includes things that can't be returned from the machine (as they'd be ill-scoped).
isPure
    :: ToBuiltinMeaning uni fun
    => (name -> Strictness) -> Term tyname name uni fun a -> Bool
isPure :: (name -> Strictness) -> Term tyname name uni fun a -> Bool
isPure name -> Strictness
varStrictness = Term tyname name uni fun a -> Bool
go
    where
        go :: Term tyname name uni fun a -> Bool
go = \case
            -- See Note [Purity, strictness, and variables]
            Var a
_ name
n -> case name -> Strictness
varStrictness name
n of
                Strictness
Strict    -> Bool
True
                Strictness
NonStrict -> Bool
False
            -- These are syntactically values that won't reduce further
            LamAbs {} -> Bool
True
            TyAbs {} -> Bool
True
            Constant {} -> Bool
True
            IWrap a
_ Type tyname uni a
_ Type tyname uni a
_ Term tyname name uni fun a
t -> Term tyname name uni fun a -> Bool
go Term tyname name uni fun a
t

            Term tyname name uni fun a
x | Just bapp :: BuiltinApp tyname name uni fun a
bapp@(BuiltinApp fun
_ [Arg tyname name uni fun a]
args) <- Term tyname name uni fun a
-> Maybe (BuiltinApp tyname name uni fun a)
forall tyname name (uni :: * -> *) fun a.
Term tyname name uni fun a
-> Maybe (BuiltinApp tyname name uni fun a)
asBuiltinApp Term tyname name uni fun a
x ->
                -- Pure only if we can tell that the builtin application is not saturated
                (case BuiltinApp tyname name uni fun a -> Maybe Bool
forall tyname name (uni :: * -> *) fun a.
ToBuiltinMeaning uni fun =>
BuiltinApp tyname name uni fun a -> Maybe Bool
isSaturated BuiltinApp tyname name uni fun a
bapp of { Just Bool
b -> Bool -> Bool
not Bool
b; Maybe Bool
Nothing -> Bool
False; })
                Bool -> Bool -> Bool
&&
                -- But all the arguments need to also be effect-free, since they will be evaluated
                -- when we evaluate the application.
                (Arg tyname name uni fun a -> Bool)
-> [Arg tyname name uni fun a] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (\case { TermArg Term tyname name uni fun a
arg -> Term tyname name uni fun a -> Bool
go Term tyname name uni fun a
arg; TypeArg Type tyname uni a
_ -> Bool
True }) [Arg tyname name uni fun a]
args

            Term tyname name uni fun a
_ -> Bool
False