{-# LANGUAGE FlexibleInstances     #-}
{-# LANGUAGE GADTs                 #-}
{-# LANGUAGE LambdaCase            #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE OverloadedStrings     #-}
{-# LANGUAGE ScopedTypeVariables   #-}
{-# LANGUAGE TypeApplications      #-}
{-# LANGUAGE UndecidableInstances  #-}
{-# LANGUAGE ViewPatterns          #-}

module PlutusIR.Purity
  ( isPure
  , isSaturated
  , isWorkFree
  , EvalOrder
  , unEvalOrder
  , EvalTerm (..)
  , Purity (..)
  , termEvaluationOrder
  ) where

import Control.Lens ((^.))
import Data.DList qualified as DList
import Data.List.NonEmpty qualified as NE
import PlutusCore.Builtin (BuiltinMeaning (..), ToBuiltinMeaning (..), TypeScheme (..))
import PlutusCore.Name.Unique qualified as PLC
import PlutusCore.Pretty (Pretty (pretty), PrettyBy (prettyBy))
import PlutusIR (Binding (TermBind), Name, Recursivity (NonRec, Rec),
                 Strictness (NonStrict, Strict), Term (..), TyName)
import PlutusIR.Analysis.Builtins (BuiltinsInfo, biSemanticsVariant, builtinArityInfo)
import PlutusIR.Analysis.VarInfo (VarInfo (DatatypeConstructor), VarsInfo, lookupVarInfo,
                                  varInfoStrictness)
import PlutusIR.Contexts (AppContext (..), Saturation (Oversaturated, Saturated, Undersaturated),
                          fillAppContext, saturates, splitApplication)
import Prettyprinter (vsep, (<+>))

saturatesScheme :: AppContext 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 :: forall tyname name (uni :: * -> *) fun a val (args :: [*]) res.
AppContext tyname name uni fun a
-> TypeScheme val args res -> Maybe Bool
saturatesScheme AppContext tyname name uni fun a
_ TypeSchemeResult{}                            = Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
True
-- Consume one argument
saturatesScheme (TermAppContext Term tyname name uni fun a
_ a
_ AppContext tyname name uni fun a
args) (TypeSchemeArrow TypeScheme val args1 res
sch) = AppContext tyname name uni fun a
-> TypeScheme val args1 res -> Maybe Bool
forall tyname name (uni :: * -> *) fun a val (args :: [*]) res.
AppContext tyname name uni fun a
-> TypeScheme val args res -> Maybe Bool
saturatesScheme AppContext tyname name uni fun a
args TypeScheme val args1 res
sch
saturatesScheme (TypeAppContext Type tyname uni a
_ a
_ AppContext tyname name uni fun a
args) (TypeSchemeAll Proxy '(text, uniq, kind)
_ TypeScheme val args res
sch) = AppContext tyname name uni fun a
-> TypeScheme val args res -> Maybe Bool
forall tyname name (uni :: * -> *) fun a val (args :: [*]) res.
AppContext tyname name uni fun a
-> TypeScheme val args res -> Maybe Bool
saturatesScheme AppContext tyname name uni fun a
args TypeScheme val args res
sch
-- Under-applied, not saturated
saturatesScheme AppContext tyname name uni fun a
AppContextEnd TypeSchemeArrow{}                 = Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
False
saturatesScheme AppContext tyname name uni fun a
AppContextEnd 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 TypeAppContext{} TypeSchemeArrow{}              = Maybe Bool
forall a. Maybe a
Nothing
saturatesScheme TermAppContext{} TypeSchemeAll{}                = Maybe Bool
forall a. Maybe a
Nothing

-- | Is the given application saturated? Returns 'Nothing' if we can't tell.
isSaturated
  :: forall tyname name uni fun a
   . (ToBuiltinMeaning uni fun)
  => BuiltinsInfo uni fun
  -> fun
  -> AppContext tyname name uni fun a
  -> Maybe Bool
isSaturated :: forall tyname name (uni :: * -> *) fun a.
ToBuiltinMeaning uni fun =>
BuiltinsInfo uni fun
-> fun -> AppContext tyname name uni fun a -> Maybe Bool
isSaturated BuiltinsInfo uni fun
binfo fun
fun AppContext tyname name uni fun a
args =
  let semvar :: BuiltinSemanticsVariant fun
semvar = 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
   in case forall (uni :: * -> *) fun val.
(ToBuiltinMeaning uni fun, HasMeaningIn uni val) =>
BuiltinSemanticsVariant fun
-> fun -> BuiltinMeaning val (CostingPart uni fun)
toBuiltinMeaning @uni @fun @(Term TyName Name uni fun ()) BuiltinSemanticsVariant fun
semvar fun
fun of
        BuiltinMeaning TypeScheme (Term TyName Name uni fun ()) args res
sch FoldArgs args res
_ CostingPart uni fun -> BuiltinRuntime (Term TyName Name uni fun ())
_ -> AppContext tyname name uni fun a
-> TypeScheme (Term TyName Name uni fun ()) args res -> Maybe Bool
forall tyname name (uni :: * -> *) fun a val (args :: [*]) res.
AppContext tyname name uni fun a
-> TypeScheme val args res -> Maybe Bool
saturatesScheme AppContext tyname name uni fun a
args TypeScheme (Term TyName Name uni fun ()) args res
sch

-- | Is this pure? Either yes, or maybe not.
data Purity = MaybeImpure | Pure

instance Pretty Purity where
  pretty :: forall ann. Purity -> Doc ann
pretty Purity
MaybeImpure = Doc ann
"impure?"
  pretty Purity
Pure        = Doc ann
"pure"

-- | Is this term essentially work-free? Either yes, or maybe not.
data WorkFreedom = MaybeWork | WorkFree

instance Pretty WorkFreedom where
  pretty :: forall ann. WorkFreedom -> Doc ann
pretty WorkFreedom
MaybeWork = Doc ann
"maybe work?"
  pretty WorkFreedom
WorkFree  = Doc ann
"work-free"

{- | Either the "next" term to be evaluated, along with its 'Purity' and 'WorkFreedom',
or we don't know what comes next.
-}
data EvalTerm tyname name uni fun a
  = Unknown
  | EvalTerm Purity WorkFreedom (Term tyname name uni fun a)

instance
  (PrettyBy config (Term tyname name uni fun a))
  => PrettyBy config (EvalTerm tyname name uni fun a)
  where
  prettyBy :: forall ann. config -> EvalTerm tyname name uni fun a -> Doc ann
prettyBy config
_ EvalTerm tyname name uni fun a
Unknown                    = Doc ann
"<unknown>"
  prettyBy config
config (EvalTerm Purity
eff WorkFreedom
work Term tyname name uni fun a
t) = Purity -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Purity -> Doc ann
pretty Purity
eff Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> WorkFreedom -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. WorkFreedom -> Doc ann
pretty WorkFreedom
work Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> Doc ann
":" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> config -> Term tyname name uni fun a -> Doc ann
forall ann. config -> Term tyname name uni fun a -> Doc ann
forall config a ann. PrettyBy config a => config -> a -> Doc ann
prettyBy config
config Term tyname name uni fun a
t

{- | The order in which terms get evaluated, along with their purities.
We use a DList here for efficient and lazy concatenation
-}
newtype EvalOrder tyname name uni fun a = EvalOrder (DList.DList (EvalTerm tyname name uni fun a))
  deriving newtype (NonEmpty (EvalOrder tyname name uni fun a)
-> EvalOrder tyname name uni fun a
EvalOrder tyname name uni fun a
-> EvalOrder tyname name uni fun a
-> EvalOrder tyname name uni fun a
(EvalOrder tyname name uni fun a
 -> EvalOrder tyname name uni fun a
 -> EvalOrder tyname name uni fun a)
-> (NonEmpty (EvalOrder tyname name uni fun a)
    -> EvalOrder tyname name uni fun a)
-> (forall b.
    Integral b =>
    b
    -> EvalOrder tyname name uni fun a
    -> EvalOrder tyname name uni fun a)
-> Semigroup (EvalOrder tyname name uni fun a)
forall b.
Integral b =>
b
-> EvalOrder tyname name uni fun a
-> EvalOrder tyname name uni fun a
forall a.
(a -> a -> a)
-> (NonEmpty a -> a)
-> (forall b. Integral b => b -> a -> a)
-> Semigroup a
forall tyname name (uni :: * -> *) fun a.
NonEmpty (EvalOrder tyname name uni fun a)
-> EvalOrder tyname name uni fun a
forall tyname name (uni :: * -> *) fun a.
EvalOrder tyname name uni fun a
-> EvalOrder tyname name uni fun a
-> EvalOrder tyname name uni fun a
forall tyname name (uni :: * -> *) fun a b.
Integral b =>
b
-> EvalOrder tyname name uni fun a
-> EvalOrder tyname name uni fun a
$c<> :: forall tyname name (uni :: * -> *) fun a.
EvalOrder tyname name uni fun a
-> EvalOrder tyname name uni fun a
-> EvalOrder tyname name uni fun a
<> :: EvalOrder tyname name uni fun a
-> EvalOrder tyname name uni fun a
-> EvalOrder tyname name uni fun a
$csconcat :: forall tyname name (uni :: * -> *) fun a.
NonEmpty (EvalOrder tyname name uni fun a)
-> EvalOrder tyname name uni fun a
sconcat :: NonEmpty (EvalOrder tyname name uni fun a)
-> EvalOrder tyname name uni fun a
$cstimes :: forall tyname name (uni :: * -> *) fun a b.
Integral b =>
b
-> EvalOrder tyname name uni fun a
-> EvalOrder tyname name uni fun a
stimes :: forall b.
Integral b =>
b
-> EvalOrder tyname name uni fun a
-> EvalOrder tyname name uni fun a
Semigroup, Semigroup (EvalOrder tyname name uni fun a)
EvalOrder tyname name uni fun a
Semigroup (EvalOrder tyname name uni fun a) =>
EvalOrder tyname name uni fun a
-> (EvalOrder tyname name uni fun a
    -> EvalOrder tyname name uni fun a
    -> EvalOrder tyname name uni fun a)
-> ([EvalOrder tyname name uni fun a]
    -> EvalOrder tyname name uni fun a)
-> Monoid (EvalOrder tyname name uni fun a)
[EvalOrder tyname name uni fun a]
-> EvalOrder tyname name uni fun a
EvalOrder tyname name uni fun a
-> EvalOrder tyname name uni fun a
-> EvalOrder tyname name uni fun a
forall a.
Semigroup a =>
a -> (a -> a -> a) -> ([a] -> a) -> Monoid a
forall tyname name (uni :: * -> *) fun a.
Semigroup (EvalOrder tyname name uni fun a)
forall tyname name (uni :: * -> *) fun a.
EvalOrder tyname name uni fun a
forall tyname name (uni :: * -> *) fun a.
[EvalOrder tyname name uni fun a]
-> EvalOrder tyname name uni fun a
forall tyname name (uni :: * -> *) fun a.
EvalOrder tyname name uni fun a
-> EvalOrder tyname name uni fun a
-> EvalOrder tyname name uni fun a
$cmempty :: forall tyname name (uni :: * -> *) fun a.
EvalOrder tyname name uni fun a
mempty :: EvalOrder tyname name uni fun a
$cmappend :: forall tyname name (uni :: * -> *) fun a.
EvalOrder tyname name uni fun a
-> EvalOrder tyname name uni fun a
-> EvalOrder tyname name uni fun a
mappend :: EvalOrder tyname name uni fun a
-> EvalOrder tyname name uni fun a
-> EvalOrder tyname name uni fun a
$cmconcat :: forall tyname name (uni :: * -> *) fun a.
[EvalOrder tyname name uni fun a]
-> EvalOrder tyname name uni fun a
mconcat :: [EvalOrder tyname name uni fun a]
-> EvalOrder tyname name uni fun a
Monoid)

{- | Get the evaluation order as a list of 'EvalTerm's. Either terminates in a single
'Unknown', which means that we got to a point where evaluation continues but we don't
know where; or terminates normally, in which case we actually got to the end of the
evaluation order for the term.
-}
unEvalOrder :: EvalOrder tyname name uni fun a -> [EvalTerm tyname name uni fun a]
unEvalOrder :: forall tyname name (uni :: * -> *) fun a.
EvalOrder tyname name uni fun a -> [EvalTerm tyname name uni fun a]
unEvalOrder (EvalOrder DList (EvalTerm tyname name uni fun a)
ts) =
  -- This is where we avoid traversing the whole program beyond the first Unknown,
  -- since DList is lazy and we convert to a lazy list and then filter it.
  (EvalTerm tyname name uni fun a -> Bool)
-> [EvalTerm tyname name uni fun a]
-> [EvalTerm tyname name uni fun a]
forall a. (a -> Bool) -> [a] -> [a]
takeWhileInclusive (\case EvalTerm tyname name uni fun a
Unknown -> Bool
False; EvalTerm tyname name uni fun a
_ -> Bool
True) (DList (EvalTerm tyname name uni fun a)
-> [EvalTerm tyname name uni fun a]
forall a. DList a -> [a]
DList.toList DList (EvalTerm tyname name uni fun a)
ts)
 where
  takeWhileInclusive :: (a -> Bool) -> [a] -> [a]
  takeWhileInclusive :: forall a. (a -> Bool) -> [a] -> [a]
takeWhileInclusive a -> Bool
p = (a -> [a] -> [a]) -> [a] -> [a] -> [a]
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\a
x [a]
ys -> if a -> Bool
p a
x then a
x a -> [a] -> [a]
forall a. a -> [a] -> [a]
: [a]
ys else [a
x]) []

evalThis :: EvalTerm tyname name uni fun a -> EvalOrder tyname name uni fun a
evalThis :: forall tyname name (uni :: * -> *) fun a.
EvalTerm tyname name uni fun a -> EvalOrder tyname name uni fun a
evalThis EvalTerm tyname name uni fun a
tm = DList (EvalTerm tyname name uni fun a)
-> EvalOrder tyname name uni fun a
forall tyname name (uni :: * -> *) fun a.
DList (EvalTerm tyname name uni fun a)
-> EvalOrder tyname name uni fun a
EvalOrder (EvalTerm tyname name uni fun a
-> DList (EvalTerm tyname name uni fun a)
forall a. a -> DList a
DList.singleton EvalTerm tyname name uni fun a
tm)

instance
  (PrettyBy config (Term tyname name uni fun a))
  => PrettyBy config (EvalOrder tyname name uni fun a)
  where
  prettyBy :: forall ann. config -> EvalOrder tyname name uni fun a -> Doc ann
prettyBy config
config EvalOrder tyname name uni fun a
eo = [Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
vsep ([Doc ann] -> Doc ann) -> [Doc ann] -> Doc ann
forall a b. (a -> b) -> a -> b
$ (EvalTerm tyname name uni fun a -> Doc ann)
-> [EvalTerm tyname name uni fun a] -> [Doc ann]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (config -> EvalTerm tyname name uni fun a -> Doc ann
forall ann. config -> EvalTerm tyname name uni fun a -> Doc ann
forall config a ann. PrettyBy config a => config -> a -> Doc ann
prettyBy config
config) (EvalOrder tyname name uni fun a -> [EvalTerm tyname name uni fun a]
forall tyname name (uni :: * -> *) fun a.
EvalOrder tyname name uni fun a -> [EvalTerm tyname name uni fun a]
unEvalOrder EvalOrder tyname name uni fun a
eo)

{- | Given a term, return the order in which it and its sub-terms will be evaluated.

This aims to be a sound under-approximation: if we don't know, we just say 'Unknown'.
Typically there will be a sequence of terms that we do know, which will terminate
in 'Unknown' once we do something like call a function.

This makes some assumptions about the evaluator, in particular about the order in
which we evaluate sub-terms, but these match the current evaluator and we are not
planning on changing it.
-}
termEvaluationOrder
  :: forall tyname name uni fun a
   . (ToBuiltinMeaning uni fun, PLC.HasUnique name PLC.TermUnique)
  => BuiltinsInfo uni fun
  -> VarsInfo tyname name uni a
  -> Term tyname name uni fun a
  -> EvalOrder tyname name uni fun a
termEvaluationOrder :: forall tyname name (uni :: * -> *) fun a.
(ToBuiltinMeaning uni fun, HasUnique name TermUnique) =>
BuiltinsInfo uni fun
-> VarsInfo tyname name uni a
-> Term tyname name uni fun a
-> EvalOrder tyname name uni fun a
termEvaluationOrder BuiltinsInfo uni fun
binfo VarsInfo tyname name uni a
vinfo = Term tyname name uni fun a -> EvalOrder tyname name uni fun a
goTerm
 where
  goTerm :: Term tyname name uni fun a -> EvalOrder tyname name uni fun a
  goTerm :: Term tyname name uni fun a -> EvalOrder tyname name uni fun a
goTerm = \case
    t :: Term tyname name uni fun a
t@(Let a
_ Recursivity
NonRec NonEmpty (Binding tyname name uni fun a)
bs Term tyname name uni fun a
b) ->
      -- first the bindings, in order
      [Binding tyname name uni fun a] -> EvalOrder tyname name uni fun a
goBindings (NonEmpty (Binding tyname name uni fun a)
-> [Binding tyname name uni fun a]
forall a. NonEmpty a -> [a]
NE.toList NonEmpty (Binding tyname name uni fun a)
bs)
        -- then the body
        EvalOrder tyname name uni fun a
-> EvalOrder tyname name uni fun a
-> EvalOrder tyname name uni fun a
forall a. Semigroup a => a -> a -> a
<> Term tyname name uni fun a -> EvalOrder tyname name uni fun a
goTerm Term tyname name uni fun a
b
        -- then the whole term, which will lead to applications (so work)
        EvalOrder tyname name uni fun a
-> EvalOrder tyname name uni fun a
-> EvalOrder tyname name uni fun a
forall a. Semigroup a => a -> a -> a
<> EvalTerm tyname name uni fun a -> EvalOrder tyname name uni fun a
forall tyname name (uni :: * -> *) fun a.
EvalTerm tyname name uni fun a -> EvalOrder tyname name uni fun a
evalThis (Purity
-> WorkFreedom
-> Term tyname name uni fun a
-> EvalTerm tyname name uni fun a
forall tyname name (uni :: * -> *) fun a.
Purity
-> WorkFreedom
-> Term tyname name uni fun a
-> EvalTerm tyname name uni fun a
EvalTerm Purity
Pure WorkFreedom
MaybeWork Term tyname name uni fun a
t)
    Let a
_ Recursivity
Rec NonEmpty (Binding tyname name uni fun a)
_ Term tyname name uni fun a
_ ->
      -- Hard to know what gets evaluated first in a recursive let-binding,
      -- just give up
      EvalTerm tyname name uni fun a -> EvalOrder tyname name uni fun a
forall tyname name (uni :: * -> *) fun a.
EvalTerm tyname name uni fun a -> EvalOrder tyname name uni fun a
evalThis EvalTerm tyname name uni fun a
forall tyname name (uni :: * -> *) fun a.
EvalTerm tyname name uni fun a
Unknown
    -- If we can view as a builtin application, then handle that specially
    (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
a fun
fun, AppContext tyname name uni fun a
args)) -> a
-> fun
-> AppContext tyname name uni fun a
-> EvalOrder tyname name uni fun a
goBuiltinApp a
a fun
fun AppContext tyname name uni fun a
args
    -- If we can view as a constructor application, then handle that specially.
    -- Constructor applications are always pure: if under-applied they don't
    -- reduce; if fully-applied they are pure; if over-applied it's going to be
    -- a type error since they never return a function. So we can ignore the arity
    -- in this case!
    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 -> (h :: Term tyname name uni fun a
h@(Var a
_ name
n), AppContext tyname name uni fun a
args))
      | Just (DatatypeConstructor{}) <- name
-> VarsInfo tyname name uni a -> Maybe (VarInfo tyname name uni a)
forall name tyname (uni :: * -> *) a.
HasUnique name TermUnique =>
name
-> VarsInfo tyname name uni a -> Maybe (VarInfo tyname name uni a)
lookupVarInfo name
n VarsInfo tyname name uni a
vinfo ->
          EvalTerm tyname name uni fun a -> EvalOrder tyname name uni fun a
forall tyname name (uni :: * -> *) fun a.
EvalTerm tyname name uni fun a -> EvalOrder tyname name uni fun a
evalThis (Purity
-> WorkFreedom
-> Term tyname name uni fun a
-> EvalTerm tyname name uni fun a
forall tyname name (uni :: * -> *) fun a.
Purity
-> WorkFreedom
-> Term tyname name uni fun a
-> EvalTerm tyname name uni fun a
EvalTerm Purity
Pure WorkFreedom
MaybeWork Term tyname name uni fun a
h)
            EvalOrder tyname name uni fun a
-> EvalOrder tyname name uni fun a
-> EvalOrder tyname name uni fun a
forall a. Semigroup a => a -> a -> a
<> AppContext tyname name uni fun a -> EvalOrder tyname name uni fun a
appContextEvalOrder AppContext tyname name uni fun a
args
            EvalOrder tyname name uni fun a
-> EvalOrder tyname name uni fun a
-> EvalOrder tyname name uni fun a
forall a. Semigroup a => a -> a -> a
<> EvalTerm tyname name uni fun a -> EvalOrder tyname name uni fun a
forall tyname name (uni :: * -> *) fun a.
EvalTerm tyname name uni fun a -> EvalOrder tyname name uni fun a
evalThis (Purity
-> WorkFreedom
-> Term tyname name uni fun a
-> EvalTerm tyname name uni fun a
forall tyname name (uni :: * -> *) fun a.
Purity
-> WorkFreedom
-> Term tyname name uni fun a
-> EvalTerm tyname name uni fun a
EvalTerm Purity
Pure WorkFreedom
MaybeWork Term tyname name uni fun a
t)
    -- No Unknown: we go to a known pure place, but we can't show it,
    -- so we just skip it here. This has the effect of making constructor
    -- applications pure

    -- We could handle functions and type abstractions with *known* bodies
    -- here. But there's not much point: beta reduction will immediately
    -- turn those into let-bindings, which we do see through already.
    t :: Term tyname name uni fun a
t@(Apply a
_ Term tyname name uni fun a
fun Term tyname name uni fun a
arg) ->
      -- first the function
      Term tyname name uni fun a -> EvalOrder tyname name uni fun a
goTerm Term tyname name uni fun a
fun
        -- then the arg
        EvalOrder tyname name uni fun a
-> EvalOrder tyname name uni fun a
-> EvalOrder tyname name uni fun a
forall a. Semigroup a => a -> a -> a
<> Term tyname name uni fun a -> EvalOrder tyname name uni fun a
goTerm Term tyname name uni fun a
arg
        -- then the whole term, which means environment manipulation, so work
        EvalOrder tyname name uni fun a
-> EvalOrder tyname name uni fun a
-> EvalOrder tyname name uni fun a
forall a. Semigroup a => a -> a -> a
<> EvalTerm tyname name uni fun a -> EvalOrder tyname name uni fun a
forall tyname name (uni :: * -> *) fun a.
EvalTerm tyname name uni fun a -> EvalOrder tyname name uni fun a
evalThis (Purity
-> WorkFreedom
-> Term tyname name uni fun a
-> EvalTerm tyname name uni fun a
forall tyname name (uni :: * -> *) fun a.
Purity
-> WorkFreedom
-> Term tyname name uni fun a
-> EvalTerm tyname name uni fun a
EvalTerm Purity
Pure WorkFreedom
MaybeWork Term tyname name uni fun a
t)
        -- then we go to the unknown function body
        EvalOrder tyname name uni fun a
-> EvalOrder tyname name uni fun a
-> EvalOrder tyname name uni fun a
forall a. Semigroup a => a -> a -> a
<> EvalTerm tyname name uni fun a -> EvalOrder tyname name uni fun a
forall tyname name (uni :: * -> *) fun a.
EvalTerm tyname name uni fun a -> EvalOrder tyname name uni fun a
evalThis EvalTerm tyname name uni fun a
forall tyname name (uni :: * -> *) fun a.
EvalTerm tyname name uni fun a
Unknown
    t :: Term tyname name uni fun a
t@(TyInst a
_ Term tyname name uni fun a
ta Type tyname uni a
_) ->
      -- first the type abstraction
      Term tyname name uni fun a -> EvalOrder tyname name uni fun a
goTerm Term tyname name uni fun a
ta
        -- then the whole term, which will mean forcing, so work
        EvalOrder tyname name uni fun a
-> EvalOrder tyname name uni fun a
-> EvalOrder tyname name uni fun a
forall a. Semigroup a => a -> a -> a
<> EvalTerm tyname name uni fun a -> EvalOrder tyname name uni fun a
forall tyname name (uni :: * -> *) fun a.
EvalTerm tyname name uni fun a -> EvalOrder tyname name uni fun a
evalThis (Purity
-> WorkFreedom
-> Term tyname name uni fun a
-> EvalTerm tyname name uni fun a
forall tyname name (uni :: * -> *) fun a.
Purity
-> WorkFreedom
-> Term tyname name uni fun a
-> EvalTerm tyname name uni fun a
EvalTerm Purity
Pure WorkFreedom
MaybeWork Term tyname name uni fun a
t)
        -- then we go to the unknown body of the type abstraction
        EvalOrder tyname name uni fun a
-> EvalOrder tyname name uni fun a
-> EvalOrder tyname name uni fun a
forall a. Semigroup a => a -> a -> a
<> EvalTerm tyname name uni fun a -> EvalOrder tyname name uni fun a
forall tyname name (uni :: * -> *) fun a.
EvalTerm tyname name uni fun a -> EvalOrder tyname name uni fun a
evalThis EvalTerm tyname name uni fun a
forall tyname name (uni :: * -> *) fun a.
EvalTerm tyname name uni fun a
Unknown
    t :: Term tyname name uni fun a
t@(IWrap a
_ Type tyname uni a
_ Type tyname uni a
_ Term tyname name uni fun a
b) ->
      -- first the body
      Term tyname name uni fun a -> EvalOrder tyname name uni fun a
goTerm Term tyname name uni fun a
b
        EvalOrder tyname name uni fun a
-> EvalOrder tyname name uni fun a
-> EvalOrder tyname name uni fun a
forall a. Semigroup a => a -> a -> a
<> EvalTerm tyname name uni fun a -> EvalOrder tyname name uni fun a
forall tyname name (uni :: * -> *) fun a.
EvalTerm tyname name uni fun a -> EvalOrder tyname name uni fun a
evalThis (Purity
-> WorkFreedom
-> Term tyname name uni fun a
-> EvalTerm tyname name uni fun a
forall tyname name (uni :: * -> *) fun a.
Purity
-> WorkFreedom
-> Term tyname name uni fun a
-> EvalTerm tyname name uni fun a
EvalTerm Purity
Pure WorkFreedom
WorkFree Term tyname name uni fun a
t)
    t :: Term tyname name uni fun a
t@(Unwrap a
_ Term tyname name uni fun a
b) ->
      -- first the body
      Term tyname name uni fun a -> EvalOrder tyname name uni fun a
goTerm Term tyname name uni fun a
b
        -- then the whole term, but this is erased so it is work-free
        EvalOrder tyname name uni fun a
-> EvalOrder tyname name uni fun a
-> EvalOrder tyname name uni fun a
forall a. Semigroup a => a -> a -> a
<> EvalTerm tyname name uni fun a -> EvalOrder tyname name uni fun a
forall tyname name (uni :: * -> *) fun a.
EvalTerm tyname name uni fun a -> EvalOrder tyname name uni fun a
evalThis (Purity
-> WorkFreedom
-> Term tyname name uni fun a
-> EvalTerm tyname name uni fun a
forall tyname name (uni :: * -> *) fun a.
Purity
-> WorkFreedom
-> Term tyname name uni fun a
-> EvalTerm tyname name uni fun a
EvalTerm Purity
Pure WorkFreedom
WorkFree Term tyname name uni fun a
t)
    t :: Term tyname name uni fun a
t@(Constr a
_ Type tyname uni a
_ Word64
_ [Term tyname name uni fun a]
ts) ->
      -- first the arguments, in left-to-right order
      (Term tyname name uni fun a -> EvalOrder tyname name uni fun a)
-> [Term tyname name uni fun a] -> EvalOrder tyname name uni fun a
forall m a. Monoid m => (a -> m) -> [a] -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap Term tyname name uni fun a -> EvalOrder tyname name uni fun a
goTerm [Term tyname name uni fun a]
ts
        -- then the whole term, which means constructing the value, so work
        EvalOrder tyname name uni fun a
-> EvalOrder tyname name uni fun a
-> EvalOrder tyname name uni fun a
forall a. Semigroup a => a -> a -> a
<> EvalTerm tyname name uni fun a -> EvalOrder tyname name uni fun a
forall tyname name (uni :: * -> *) fun a.
EvalTerm tyname name uni fun a -> EvalOrder tyname name uni fun a
evalThis (Purity
-> WorkFreedom
-> Term tyname name uni fun a
-> EvalTerm tyname name uni fun a
forall tyname name (uni :: * -> *) fun a.
Purity
-> WorkFreedom
-> Term tyname name uni fun a
-> EvalTerm tyname name uni fun a
EvalTerm Purity
Pure WorkFreedom
MaybeWork Term tyname name uni fun a
t)
    t :: Term tyname name uni fun a
t@(Case a
_ Type tyname uni a
_ Term tyname name uni fun a
scrut [Term tyname name uni fun a]
_) ->
      -- first the scrutinee
      Term tyname name uni fun a -> EvalOrder tyname name uni fun a
goTerm Term tyname name uni fun a
scrut
        -- then the whole term, which means finding the case so work
        EvalOrder tyname name uni fun a
-> EvalOrder tyname name uni fun a
-> EvalOrder tyname name uni fun a
forall a. Semigroup a => a -> a -> a
<> EvalTerm tyname name uni fun a -> EvalOrder tyname name uni fun a
forall tyname name (uni :: * -> *) fun a.
EvalTerm tyname name uni fun a -> EvalOrder tyname name uni fun a
evalThis (Purity
-> WorkFreedom
-> Term tyname name uni fun a
-> EvalTerm tyname name uni fun a
forall tyname name (uni :: * -> *) fun a.
Purity
-> WorkFreedom
-> Term tyname name uni fun a
-> EvalTerm tyname name uni fun a
EvalTerm Purity
Pure WorkFreedom
MaybeWork Term tyname name uni fun a
t)
        -- then we go to an unknown scrutinee
        EvalOrder tyname name uni fun a
-> EvalOrder tyname name uni fun a
-> EvalOrder tyname name uni fun a
forall a. Semigroup a => a -> a -> a
<> EvalTerm tyname name uni fun a -> EvalOrder tyname name uni fun a
forall tyname name (uni :: * -> *) fun a.
EvalTerm tyname name uni fun a -> EvalOrder tyname name uni fun a
evalThis EvalTerm tyname name uni fun a
forall tyname name (uni :: * -> *) fun a.
EvalTerm tyname name uni fun a
Unknown
    -- Leaf terms
    t :: Term tyname name uni fun a
t@(Var a
_ name
name) ->
      -- See Note [Purity, strictness, and variables]
      let purity :: Purity
purity = case VarInfo tyname name uni a -> Strictness
forall tyname name (uni :: * -> *) a.
VarInfo tyname name uni a -> Strictness
varInfoStrictness (VarInfo tyname name uni a -> Strictness)
-> Maybe (VarInfo tyname name uni a) -> Maybe Strictness
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> name
-> VarsInfo tyname name uni a -> Maybe (VarInfo tyname name uni a)
forall name tyname (uni :: * -> *) a.
HasUnique name TermUnique =>
name
-> VarsInfo tyname name uni a -> Maybe (VarInfo tyname name uni a)
lookupVarInfo name
name VarsInfo tyname name uni a
vinfo of
            Just Strictness
Strict    -> Purity
Pure
            Just Strictness
NonStrict -> Purity
MaybeImpure
            Maybe Strictness
_              -> Purity
MaybeImpure
       in -- looking up the variable is work
          EvalTerm tyname name uni fun a -> EvalOrder tyname name uni fun a
forall tyname name (uni :: * -> *) fun a.
EvalTerm tyname name uni fun a -> EvalOrder tyname name uni fun a
evalThis (Purity
-> WorkFreedom
-> Term tyname name uni fun a
-> EvalTerm tyname name uni fun a
forall tyname name (uni :: * -> *) fun a.
Purity
-> WorkFreedom
-> Term tyname name uni fun a
-> EvalTerm tyname name uni fun a
EvalTerm Purity
purity WorkFreedom
MaybeWork Term tyname name uni fun a
t)
    t :: Term tyname name uni fun a
t@Error{} ->
      -- definitely effectful! but not relevant from a work perspective
      EvalTerm tyname name uni fun a -> EvalOrder tyname name uni fun a
forall tyname name (uni :: * -> *) fun a.
EvalTerm tyname name uni fun a -> EvalOrder tyname name uni fun a
evalThis (Purity
-> WorkFreedom
-> Term tyname name uni fun a
-> EvalTerm tyname name uni fun a
forall tyname name (uni :: * -> *) fun a.
Purity
-> WorkFreedom
-> Term tyname name uni fun a
-> EvalTerm tyname name uni fun a
EvalTerm Purity
MaybeImpure WorkFreedom
WorkFree Term tyname name uni fun a
t)
        -- program terminates
        EvalOrder tyname name uni fun a
-> EvalOrder tyname name uni fun a
-> EvalOrder tyname name uni fun a
forall a. Semigroup a => a -> a -> a
<> EvalTerm tyname name uni fun a -> EvalOrder tyname name uni fun a
forall tyname name (uni :: * -> *) fun a.
EvalTerm tyname name uni fun a -> EvalOrder tyname name uni fun a
evalThis EvalTerm tyname name uni fun a
forall tyname name (uni :: * -> *) fun a.
EvalTerm tyname name uni fun a
Unknown
    t :: Term tyname name uni fun a
t@Builtin{} ->
      EvalTerm tyname name uni fun a -> EvalOrder tyname name uni fun a
forall tyname name (uni :: * -> *) fun a.
EvalTerm tyname name uni fun a -> EvalOrder tyname name uni fun a
evalThis (Purity
-> WorkFreedom
-> Term tyname name uni fun a
-> EvalTerm tyname name uni fun a
forall tyname name (uni :: * -> *) fun a.
Purity
-> WorkFreedom
-> Term tyname name uni fun a
-> EvalTerm tyname name uni fun a
EvalTerm Purity
Pure WorkFreedom
WorkFree Term tyname name uni fun a
t)
    t :: Term tyname name uni fun a
t@TyAbs{} ->
      EvalTerm tyname name uni fun a -> EvalOrder tyname name uni fun a
forall tyname name (uni :: * -> *) fun a.
EvalTerm tyname name uni fun a -> EvalOrder tyname name uni fun a
evalThis (Purity
-> WorkFreedom
-> Term tyname name uni fun a
-> EvalTerm tyname name uni fun a
forall tyname name (uni :: * -> *) fun a.
Purity
-> WorkFreedom
-> Term tyname name uni fun a
-> EvalTerm tyname name uni fun a
EvalTerm Purity
Pure WorkFreedom
WorkFree Term tyname name uni fun a
t)
    t :: Term tyname name uni fun a
t@LamAbs{} ->
      EvalTerm tyname name uni fun a -> EvalOrder tyname name uni fun a
forall tyname name (uni :: * -> *) fun a.
EvalTerm tyname name uni fun a -> EvalOrder tyname name uni fun a
evalThis (Purity
-> WorkFreedom
-> Term tyname name uni fun a
-> EvalTerm tyname name uni fun a
forall tyname name (uni :: * -> *) fun a.
Purity
-> WorkFreedom
-> Term tyname name uni fun a
-> EvalTerm tyname name uni fun a
EvalTerm Purity
Pure WorkFreedom
WorkFree Term tyname name uni fun a
t)
    t :: Term tyname name uni fun a
t@Constant{} ->
      EvalTerm tyname name uni fun a -> EvalOrder tyname name uni fun a
forall tyname name (uni :: * -> *) fun a.
EvalTerm tyname name uni fun a -> EvalOrder tyname name uni fun a
evalThis (Purity
-> WorkFreedom
-> Term tyname name uni fun a
-> EvalTerm tyname name uni fun a
forall tyname name (uni :: * -> *) fun a.
Purity
-> WorkFreedom
-> Term tyname name uni fun a
-> EvalTerm tyname name uni fun a
EvalTerm Purity
Pure WorkFreedom
WorkFree Term tyname name uni fun a
t)

  goBindings :: [Binding tyname name uni fun a] -> EvalOrder tyname name uni fun a
  goBindings :: [Binding tyname name uni fun a] -> EvalOrder tyname name uni fun a
goBindings [] = EvalOrder tyname name uni fun a
forall a. Monoid a => a
mempty
  goBindings (Binding tyname name uni fun a
b : [Binding tyname name uni fun a]
bs) = case Binding tyname name uni fun a
b of
    -- Only strict term bindings get evaluated at this point
    TermBind a
_ Strictness
Strict VarDecl tyname name uni a
_ Term tyname name uni fun a
rhs -> Term tyname name uni fun a -> EvalOrder tyname name uni fun a
goTerm Term tyname name uni fun a
rhs
    Binding tyname name uni fun a
_                       -> [Binding tyname name uni fun a] -> EvalOrder tyname name uni fun a
goBindings [Binding tyname name uni fun a]
bs

  goBuiltinApp :: a -> fun -> AppContext tyname name uni fun a -> EvalOrder tyname name uni fun a
  goBuiltinApp :: a
-> fun
-> AppContext tyname name uni fun a
-> EvalOrder tyname name uni fun a
goBuiltinApp a
a fun
fun AppContext tyname name uni fun a
appContext = AppContext tyname name uni fun a -> EvalOrder tyname name uni fun a
appContextEvalOrder AppContext tyname name uni fun a
appContext EvalOrder tyname name uni fun a
-> EvalOrder tyname name uni fun a
-> EvalOrder tyname name uni fun a
forall a. Semigroup a => a -> a -> a
<> EvalOrder tyname name uni fun a
evalOrder
   where
    evalOrder :: EvalOrder tyname name uni fun a
    evalOrder :: EvalOrder tyname name uni fun a
evalOrder = case AppContext tyname name uni fun a -> Arity -> Maybe Saturation
forall tyname name (uni :: * -> *) fun a.
AppContext tyname name uni fun a -> Arity -> Maybe Saturation
saturates AppContext tyname name uni fun a
appContext (BuiltinsInfo uni fun -> fun -> Arity
forall (uni :: * -> *) fun.
ToBuiltinMeaning uni fun =>
BuiltinsInfo uni fun -> fun -> Arity
builtinArityInfo BuiltinsInfo uni fun
binfo fun
fun) of
      -- If it's saturated or oversaturated, we might have an effect here
      Just Saturation
Saturated      -> EvalOrder tyname name uni fun a
maybeImpureWork
      Just Saturation
Oversaturated  -> EvalOrder tyname name uni fun a
maybeImpureWork
      -- TODO: previous definition of work-free included this, it's slightly
      -- unclear if we should do since we do update partial builtin meanings
      -- etc.
      -- If it's unsaturated, we definitely don't do any work
      Just Saturation
Undersaturated -> EvalOrder tyname name uni fun a
pureWorkFree
      -- Don't know, be conservative
      Maybe Saturation
Nothing             -> EvalOrder tyname name uni fun a
maybeImpureWork

    maybeImpureWork :: EvalOrder tyname name uni fun a
    maybeImpureWork :: EvalOrder tyname name uni fun a
maybeImpureWork = EvalTerm tyname name uni fun a -> EvalOrder tyname name uni fun a
forall tyname name (uni :: * -> *) fun a.
EvalTerm tyname name uni fun a -> EvalOrder tyname name uni fun a
evalThis (Purity
-> WorkFreedom
-> Term tyname name uni fun a
-> EvalTerm tyname name uni fun a
forall tyname name (uni :: * -> *) fun a.
Purity
-> WorkFreedom
-> Term tyname name uni fun a
-> EvalTerm tyname name uni fun a
EvalTerm Purity
MaybeImpure WorkFreedom
MaybeWork Term tyname name uni fun a
reconstructed)

    pureWorkFree :: EvalOrder tyname name uni fun a
    pureWorkFree :: EvalOrder tyname name uni fun a
pureWorkFree = EvalTerm tyname name uni fun a -> EvalOrder tyname name uni fun a
forall tyname name (uni :: * -> *) fun a.
EvalTerm tyname name uni fun a -> EvalOrder tyname name uni fun a
evalThis (Purity
-> WorkFreedom
-> Term tyname name uni fun a
-> EvalTerm tyname name uni fun a
forall tyname name (uni :: * -> *) fun a.
Purity
-> WorkFreedom
-> Term tyname name uni fun a
-> EvalTerm tyname name uni fun a
EvalTerm Purity
Pure WorkFreedom
WorkFree Term tyname name uni fun a
reconstructed)

    reconstructed :: Term tyname name uni fun a
    reconstructed :: Term tyname name uni fun a
reconstructed = Term tyname name uni fun a
-> AppContext tyname name uni fun a -> Term tyname name uni fun a
forall tyname name (uni :: * -> *) fun ann.
Term tyname name uni fun ann
-> AppContext tyname name uni fun ann
-> Term tyname name uni fun ann
fillAppContext (a -> fun -> Term tyname name uni fun a
forall tyname name (uni :: * -> *) fun a.
a -> fun -> Term tyname name uni fun a
Builtin a
a fun
fun) AppContext tyname name uni fun a
appContext

  appContextEvalOrder :: AppContext tyname name uni fun a -> EvalOrder tyname name uni fun a
  appContextEvalOrder :: AppContext tyname name uni fun a -> EvalOrder tyname name uni fun a
appContextEvalOrder = \case
    AppContext tyname name uni fun a
AppContextEnd -> EvalOrder tyname name uni fun a
forall a. Monoid a => a
mempty
    TermAppContext Term tyname name uni fun a
t a
_ AppContext tyname name uni fun a
rest -> Term tyname name uni fun a -> EvalOrder tyname name uni fun a
goTerm Term tyname name uni fun a
t EvalOrder tyname name uni fun a
-> EvalOrder tyname name uni fun a
-> EvalOrder tyname name uni fun a
forall a. Semigroup a => a -> a -> a
<> AppContext tyname name uni fun a -> EvalOrder tyname name uni fun a
appContextEvalOrder AppContext tyname name uni fun a
rest
    TypeAppContext Type tyname uni a
_ a
_ AppContext tyname name uni fun a
rest -> AppContext tyname name uni fun a -> EvalOrder tyname name uni fun a
appContextEvalOrder AppContext tyname name uni fun a
rest

{- | Will evaluating this term have side effects (looping or error)?
This is slightly wider than the definition of a value, as
it includes applications that are known to be pure, as well as
things that can't be returned from the machine (as they'd be ill-scoped).
-}
isPure
  :: (ToBuiltinMeaning uni fun, PLC.HasUnique name PLC.TermUnique)
  => BuiltinsInfo uni fun
  -> VarsInfo tyname name uni a
  -> Term tyname name uni fun a
  -> Bool
isPure :: 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
t =
  -- to work out if the term is pure, we see if we can look through
  -- the whole evaluation order without hitting something that might be
  -- effectful
  [EvalTerm tyname name uni fun a] -> Bool
forall tyname name (uni :: * -> *) fun a.
[EvalTerm tyname name uni fun a] -> Bool
go ([EvalTerm tyname name uni fun a] -> Bool)
-> [EvalTerm tyname name uni fun a] -> Bool
forall a b. (a -> b) -> a -> b
$ EvalOrder tyname name uni fun a -> [EvalTerm tyname name uni fun a]
forall tyname name (uni :: * -> *) fun a.
EvalOrder tyname name uni fun a -> [EvalTerm tyname name uni fun a]
unEvalOrder (BuiltinsInfo uni fun
-> VarsInfo tyname name uni a
-> Term tyname name uni fun a
-> EvalOrder tyname name uni fun a
forall tyname name (uni :: * -> *) fun a.
(ToBuiltinMeaning uni fun, HasUnique name TermUnique) =>
BuiltinsInfo uni fun
-> VarsInfo tyname name uni a
-> Term tyname name uni fun a
-> EvalOrder tyname name uni fun a
termEvaluationOrder BuiltinsInfo uni fun
binfo VarsInfo tyname name uni a
vinfo Term tyname name uni fun a
t)
 where
  go :: [EvalTerm tyname name uni fun a] -> Bool
  go :: forall tyname name (uni :: * -> *) fun a.
[EvalTerm tyname name uni fun a] -> Bool
go [] = Bool
True
  go (EvalTerm tyname name uni fun a
et : [EvalTerm tyname name uni fun a]
rest) = case EvalTerm tyname name uni fun a
et of
    -- Might be an effect here!
    EvalTerm Purity
MaybeImpure WorkFreedom
_ Term tyname name uni fun a
_ -> Bool
False
    -- This term is fine, what about the rest?
    EvalTerm Purity
Pure WorkFreedom
_ Term tyname name uni fun a
_        -> [EvalTerm tyname name uni fun a] -> Bool
forall tyname name (uni :: * -> *) fun a.
[EvalTerm tyname name uni fun a] -> Bool
go [EvalTerm tyname name uni fun a]
rest
    -- We don't know what will happen, so be conservative
    EvalTerm tyname name uni fun a
Unknown                  -> Bool
False

{- | Is the given term 'work-free'?

Note: The definition of 'work-free' is a little unclear, but the idea is that
evaluating this term should do very a trivial amount of work.
-}
isWorkFree
  :: (ToBuiltinMeaning uni fun, PLC.HasUnique name PLC.TermUnique)
  => BuiltinsInfo uni fun
  -> VarsInfo tyname name uni a
  -> Term tyname name uni fun a
  -> Bool
isWorkFree :: 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
isWorkFree BuiltinsInfo uni fun
binfo VarsInfo tyname name uni a
vinfo Term tyname name uni fun a
t =
  -- to work out if the term is pure, we see if we can look through
  -- the whole evaluation order without hitting something that might be
  -- effectful
  [EvalTerm tyname name uni fun a] -> Bool
forall tyname name (uni :: * -> *) fun a.
[EvalTerm tyname name uni fun a] -> Bool
go ([EvalTerm tyname name uni fun a] -> Bool)
-> [EvalTerm tyname name uni fun a] -> Bool
forall a b. (a -> b) -> a -> b
$ EvalOrder tyname name uni fun a -> [EvalTerm tyname name uni fun a]
forall tyname name (uni :: * -> *) fun a.
EvalOrder tyname name uni fun a -> [EvalTerm tyname name uni fun a]
unEvalOrder (BuiltinsInfo uni fun
-> VarsInfo tyname name uni a
-> Term tyname name uni fun a
-> EvalOrder tyname name uni fun a
forall tyname name (uni :: * -> *) fun a.
(ToBuiltinMeaning uni fun, HasUnique name TermUnique) =>
BuiltinsInfo uni fun
-> VarsInfo tyname name uni a
-> Term tyname name uni fun a
-> EvalOrder tyname name uni fun a
termEvaluationOrder BuiltinsInfo uni fun
binfo VarsInfo tyname name uni a
vinfo Term tyname name uni fun a
t)
 where
  go :: [EvalTerm tyname name uni fun a] -> Bool
  go :: forall tyname name (uni :: * -> *) fun a.
[EvalTerm tyname name uni fun a] -> Bool
go [] = Bool
True
  go (EvalTerm tyname name uni fun a
et : [EvalTerm tyname name uni fun a]
rest) = case EvalTerm tyname name uni fun a
et of
    -- Might be an effect here!
    EvalTerm Purity
_ WorkFreedom
MaybeWork Term tyname name uni fun a
_ -> Bool
False
    -- This term is fine, what about the rest?
    EvalTerm Purity
_ WorkFreedom
WorkFree Term tyname name uni fun a
_  -> [EvalTerm tyname name uni fun a] -> Bool
forall tyname name (uni :: * -> *) fun a.
[EvalTerm tyname name uni fun a] -> Bool
go [EvalTerm tyname name uni fun a]
rest
    -- We don't know what will happen, so be conservative
    EvalTerm tyname name uni fun a
Unknown                -> Bool
False

{- 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).
-}