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

-- Stripped-down version of PlutusIR.Purity
module UntypedPlutusCore.Purity
  ( isPure
  , isWorkFree
  , EvalOrder
  , unEvalOrder
  , EvalTerm (..)
  , Purity (..)
  , termEvaluationOrder
  ) where

import Data.DList qualified as DList
import Data.Typeable (Proxy (..))
import PlutusCore.Arity (builtinArity)
import PlutusCore.Builtin.Meaning (ToBuiltinMeaning (..))
import PlutusCore.Pretty (Pretty (pretty), PrettyBy (prettyBy))
import Prettyprinter (vsep, (<+>))
import UntypedPlutusCore.Core (splitApplication)
import UntypedPlutusCore.Core.Type (Term (..))

-- | 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 name uni fun a
  = Unknown
  | EvalTerm Purity WorkFreedom (Term name uni fun a)

instance
  (PrettyBy config (Term name uni fun a))
  => PrettyBy config (EvalTerm name uni fun a)
  where
  prettyBy :: forall ann. config -> EvalTerm name uni fun a -> Doc ann
prettyBy config
_ EvalTerm name uni fun a
Unknown                    = Doc ann
"<unknown>"
  prettyBy config
config (EvalTerm Purity
eff WorkFreedom
work Term 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 name uni fun a -> Doc ann
forall ann. config -> Term name uni fun a -> Doc ann
forall config a ann. PrettyBy config a => config -> a -> Doc ann
prettyBy config
config Term name uni fun a
t

-- We use a DList here for efficient and lazy concatenation

-- | The order in which terms get evaluated, along with their purities.
newtype EvalOrder name uni fun a = EvalOrder (DList.DList (EvalTerm name uni fun a))
  deriving newtype (NonEmpty (EvalOrder name uni fun a) -> EvalOrder name uni fun a
EvalOrder name uni fun a
-> EvalOrder name uni fun a -> EvalOrder name uni fun a
(EvalOrder name uni fun a
 -> EvalOrder name uni fun a -> EvalOrder name uni fun a)
-> (NonEmpty (EvalOrder name uni fun a)
    -> EvalOrder name uni fun a)
-> (forall b.
    Integral b =>
    b -> EvalOrder name uni fun a -> EvalOrder name uni fun a)
-> Semigroup (EvalOrder name uni fun a)
forall b.
Integral b =>
b -> EvalOrder name uni fun a -> EvalOrder name uni fun a
forall a.
(a -> a -> a)
-> (NonEmpty a -> a)
-> (forall b. Integral b => b -> a -> a)
-> Semigroup a
forall name (uni :: * -> *) fun a.
NonEmpty (EvalOrder name uni fun a) -> EvalOrder name uni fun a
forall name (uni :: * -> *) fun a.
EvalOrder name uni fun a
-> EvalOrder name uni fun a -> EvalOrder name uni fun a
forall name (uni :: * -> *) fun a b.
Integral b =>
b -> EvalOrder name uni fun a -> EvalOrder name uni fun a
$c<> :: forall name (uni :: * -> *) fun a.
EvalOrder name uni fun a
-> EvalOrder name uni fun a -> EvalOrder name uni fun a
<> :: EvalOrder name uni fun a
-> EvalOrder name uni fun a -> EvalOrder name uni fun a
$csconcat :: forall name (uni :: * -> *) fun a.
NonEmpty (EvalOrder name uni fun a) -> EvalOrder name uni fun a
sconcat :: NonEmpty (EvalOrder name uni fun a) -> EvalOrder name uni fun a
$cstimes :: forall name (uni :: * -> *) fun a b.
Integral b =>
b -> EvalOrder name uni fun a -> EvalOrder name uni fun a
stimes :: forall b.
Integral b =>
b -> EvalOrder name uni fun a -> EvalOrder name uni fun a
Semigroup, Semigroup (EvalOrder name uni fun a)
EvalOrder name uni fun a
Semigroup (EvalOrder name uni fun a) =>
EvalOrder name uni fun a
-> (EvalOrder name uni fun a
    -> EvalOrder name uni fun a -> EvalOrder name uni fun a)
-> ([EvalOrder name uni fun a] -> EvalOrder name uni fun a)
-> Monoid (EvalOrder name uni fun a)
[EvalOrder name uni fun a] -> EvalOrder name uni fun a
EvalOrder name uni fun a
-> EvalOrder name uni fun a -> EvalOrder name uni fun a
forall a.
Semigroup a =>
a -> (a -> a -> a) -> ([a] -> a) -> Monoid a
forall name (uni :: * -> *) fun a.
Semigroup (EvalOrder name uni fun a)
forall name (uni :: * -> *) fun a. EvalOrder name uni fun a
forall name (uni :: * -> *) fun a.
[EvalOrder name uni fun a] -> EvalOrder name uni fun a
forall name (uni :: * -> *) fun a.
EvalOrder name uni fun a
-> EvalOrder name uni fun a -> EvalOrder name uni fun a
$cmempty :: forall name (uni :: * -> *) fun a. EvalOrder name uni fun a
mempty :: EvalOrder name uni fun a
$cmappend :: forall name (uni :: * -> *) fun a.
EvalOrder name uni fun a
-> EvalOrder name uni fun a -> EvalOrder name uni fun a
mappend :: EvalOrder name uni fun a
-> EvalOrder name uni fun a -> EvalOrder name uni fun a
$cmconcat :: forall name (uni :: * -> *) fun a.
[EvalOrder name uni fun a] -> EvalOrder name uni fun a
mconcat :: [EvalOrder name uni fun a] -> EvalOrder 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 name uni fun a -> [EvalTerm name uni fun a]
unEvalOrder :: forall name (uni :: * -> *) fun a.
EvalOrder name uni fun a -> [EvalTerm name uni fun a]
unEvalOrder (EvalOrder DList (EvalTerm 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 name uni fun a -> Bool)
-> [EvalTerm name uni fun a] -> [EvalTerm name uni fun a]
forall a. (a -> Bool) -> [a] -> [a]
takeWhileInclusive (\case EvalTerm name uni fun a
Unknown -> Bool
False; EvalTerm name uni fun a
_ -> Bool
True) (DList (EvalTerm name uni fun a) -> [EvalTerm name uni fun a]
forall a. DList a -> [a]
DList.toList DList (EvalTerm 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 name uni fun a -> EvalOrder name uni fun a
evalThis :: forall name (uni :: * -> *) fun a.
EvalTerm name uni fun a -> EvalOrder name uni fun a
evalThis = DList (EvalTerm name uni fun a) -> EvalOrder name uni fun a
forall name (uni :: * -> *) fun a.
DList (EvalTerm name uni fun a) -> EvalOrder name uni fun a
EvalOrder (DList (EvalTerm name uni fun a) -> EvalOrder name uni fun a)
-> (EvalTerm name uni fun a -> DList (EvalTerm name uni fun a))
-> EvalTerm name uni fun a
-> EvalOrder name uni fun a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. EvalTerm name uni fun a -> DList (EvalTerm name uni fun a)
forall a. a -> DList a
DList.singleton

instance (PrettyBy config (Term name uni fun a)) => PrettyBy config (EvalOrder name uni fun a) where
  prettyBy :: forall ann. config -> EvalOrder name uni fun a -> Doc ann
prettyBy config
config EvalOrder 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 name uni fun a -> Doc ann)
-> [EvalTerm 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 name uni fun a -> Doc ann
forall ann. config -> EvalTerm name uni fun a -> Doc ann
forall config a ann. PrettyBy config a => config -> a -> Doc ann
prettyBy config
config) (EvalOrder name uni fun a -> [EvalTerm name uni fun a]
forall name (uni :: * -> *) fun a.
EvalOrder name uni fun a -> [EvalTerm name uni fun a]
unEvalOrder EvalOrder 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 name uni fun a
   . (ToBuiltinMeaning uni fun)
  => BuiltinSemanticsVariant fun
  -> Term name uni fun a
  -> EvalOrder name uni fun a
termEvaluationOrder :: forall name (uni :: * -> *) fun a.
ToBuiltinMeaning uni fun =>
BuiltinSemanticsVariant fun
-> Term name uni fun a -> EvalOrder name uni fun a
termEvaluationOrder BuiltinSemanticsVariant fun
builtinSemanticsVariant = Term name uni fun a -> EvalOrder name uni fun a
goTerm
 where
  goTerm :: Term name uni fun a -> EvalOrder name uni fun a
goTerm = \case
    t :: Term name uni fun a
t@(Term name uni fun a
-> (Term name uni fun a, [(a, Term name uni fun a)])
forall name (uni :: * -> *) fun a.
Term name uni fun a
-> (Term name uni fun a, [(a, Term name uni fun a)])
splitApplication -> (Builtin a
_ann fun
fun, [(a, Term name uni fun a)]
args)) ->
      ((a, Term name uni fun a) -> EvalOrder name uni fun a)
-> [(a, Term name uni fun a)] -> EvalOrder 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 name uni fun a -> EvalOrder name uni fun a
goTerm (Term name uni fun a -> EvalOrder name uni fun a)
-> ((a, Term name uni fun a) -> Term name uni fun a)
-> (a, Term name uni fun a)
-> EvalOrder name uni fun a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a, Term name uni fun a) -> Term name uni fun a
forall a b. (a, b) -> b
snd) [(a, Term name uni fun a)]
args EvalOrder name uni fun a
-> EvalOrder name uni fun a -> EvalOrder name uni fun a
forall a. Semigroup a => a -> a -> a
<> EvalOrder name uni fun a
evalOrder
     where
      evalOrder :: EvalOrder name uni fun a
evalOrder =
        if [(a, Term name uni fun a)] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [(a, Term name uni fun a)]
args Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< [Param] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (forall (uni :: * -> *) fun.
ToBuiltinMeaning uni fun =>
Proxy uni -> BuiltinSemanticsVariant fun -> fun -> [Param]
builtinArity @uni @fun (forall {k} (t :: k). Proxy t
forall (t :: * -> *). Proxy t
Proxy @uni) BuiltinSemanticsVariant fun
builtinSemanticsVariant fun
fun)
          then -- If it's unsaturated, we definitely don't do any work
            EvalTerm name uni fun a -> EvalOrder name uni fun a
forall name (uni :: * -> *) fun a.
EvalTerm name uni fun a -> EvalOrder name uni fun a
evalThis (Purity
-> WorkFreedom -> Term name uni fun a -> EvalTerm name uni fun a
forall name (uni :: * -> *) fun a.
Purity
-> WorkFreedom -> Term name uni fun a -> EvalTerm name uni fun a
EvalTerm Purity
Pure WorkFreedom
WorkFree Term name uni fun a
t)
          else -- If it's saturated or oversaturated, we might have an effect here
            EvalTerm name uni fun a -> EvalOrder name uni fun a
forall name (uni :: * -> *) fun a.
EvalTerm name uni fun a -> EvalOrder name uni fun a
evalThis (Purity
-> WorkFreedom -> Term name uni fun a -> EvalTerm name uni fun a
forall name (uni :: * -> *) fun a.
Purity
-> WorkFreedom -> Term name uni fun a -> EvalTerm name uni fun a
EvalTerm Purity
MaybeImpure WorkFreedom
MaybeWork Term name uni fun a
t)
    t :: Term name uni fun a
t@(Apply a
_ Term name uni fun a
fun Term name uni fun a
arg) ->
      -- first the function
      Term name uni fun a -> EvalOrder name uni fun a
goTerm Term name uni fun a
fun
        -- then the arg
        EvalOrder name uni fun a
-> EvalOrder name uni fun a -> EvalOrder name uni fun a
forall a. Semigroup a => a -> a -> a
<> Term name uni fun a -> EvalOrder name uni fun a
goTerm Term name uni fun a
arg
        -- then the whole term, which means environment manipulation, so work
        EvalOrder name uni fun a
-> EvalOrder name uni fun a -> EvalOrder name uni fun a
forall a. Semigroup a => a -> a -> a
<> EvalTerm name uni fun a -> EvalOrder name uni fun a
forall name (uni :: * -> *) fun a.
EvalTerm name uni fun a -> EvalOrder name uni fun a
evalThis (Purity
-> WorkFreedom -> Term name uni fun a -> EvalTerm name uni fun a
forall name (uni :: * -> *) fun a.
Purity
-> WorkFreedom -> Term name uni fun a -> EvalTerm name uni fun a
EvalTerm Purity
Pure WorkFreedom
MaybeWork Term name uni fun a
t)
        EvalOrder name uni fun a
-> EvalOrder name uni fun a -> EvalOrder name uni fun a
forall a. Semigroup a => a -> a -> a
<> case Term name uni fun a
fun of
          -- known function body
          LamAbs a
_ name
_ Term name uni fun a
body -> Term name uni fun a -> EvalOrder name uni fun a
goTerm Term name uni fun a
body
          -- unknown function body
          Term name uni fun a
_               -> EvalTerm name uni fun a -> EvalOrder name uni fun a
forall name (uni :: * -> *) fun a.
EvalTerm name uni fun a -> EvalOrder name uni fun a
evalThis EvalTerm name uni fun a
forall name (uni :: * -> *) fun a. EvalTerm name uni fun a
Unknown
    t :: Term name uni fun a
t@(Force a
_ Term name uni fun a
dterm) ->
      -- first delayed term
      Term name uni fun a -> EvalOrder name uni fun a
goTerm Term name uni fun a
dterm
        -- then the whole term, which will mean forcing, so work
        EvalOrder name uni fun a
-> EvalOrder name uni fun a -> EvalOrder name uni fun a
forall a. Semigroup a => a -> a -> a
<> EvalTerm name uni fun a -> EvalOrder name uni fun a
forall name (uni :: * -> *) fun a.
EvalTerm name uni fun a -> EvalOrder name uni fun a
evalThis (Purity
-> WorkFreedom -> Term name uni fun a -> EvalTerm name uni fun a
forall name (uni :: * -> *) fun a.
Purity
-> WorkFreedom -> Term name uni fun a -> EvalTerm name uni fun a
EvalTerm Purity
Pure WorkFreedom
MaybeWork Term name uni fun a
t)
        EvalOrder name uni fun a
-> EvalOrder name uni fun a -> EvalOrder name uni fun a
forall a. Semigroup a => a -> a -> a
<> case Term name uni fun a
dterm of
          -- known delayed term
          Delay a
_ Term name uni fun a
body -> Term name uni fun a -> EvalOrder name uni fun a
goTerm Term name uni fun a
body
          -- unknown delayed term
          Term name uni fun a
_            -> EvalTerm name uni fun a -> EvalOrder name uni fun a
forall name (uni :: * -> *) fun a.
EvalTerm name uni fun a -> EvalOrder name uni fun a
evalThis EvalTerm name uni fun a
forall name (uni :: * -> *) fun a. EvalTerm name uni fun a
Unknown
    t :: Term name uni fun a
t@(Constr a
_ Word64
_ [Term name uni fun a]
ts) ->
      -- first the arguments, in left-to-right order
      (Term name uni fun a -> EvalOrder name uni fun a)
-> [Term name uni fun a] -> EvalOrder 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 name uni fun a -> EvalOrder name uni fun a
goTerm [Term name uni fun a]
ts
        -- then the whole term, which means constructing the value, so work
        EvalOrder name uni fun a
-> EvalOrder name uni fun a -> EvalOrder name uni fun a
forall a. Semigroup a => a -> a -> a
<> EvalTerm name uni fun a -> EvalOrder name uni fun a
forall name (uni :: * -> *) fun a.
EvalTerm name uni fun a -> EvalOrder name uni fun a
evalThis (Purity
-> WorkFreedom -> Term name uni fun a -> EvalTerm name uni fun a
forall name (uni :: * -> *) fun a.
Purity
-> WorkFreedom -> Term name uni fun a -> EvalTerm name uni fun a
EvalTerm Purity
Pure WorkFreedom
MaybeWork Term name uni fun a
t)
    t :: Term name uni fun a
t@(Case a
_ Term name uni fun a
scrut Vector (Term name uni fun a)
_) ->
      -- first the scrutinee
      Term name uni fun a -> EvalOrder name uni fun a
goTerm Term name uni fun a
scrut
        -- then the whole term, which means finding the case so work
        EvalOrder name uni fun a
-> EvalOrder name uni fun a -> EvalOrder name uni fun a
forall a. Semigroup a => a -> a -> a
<> EvalTerm name uni fun a -> EvalOrder name uni fun a
forall name (uni :: * -> *) fun a.
EvalTerm name uni fun a -> EvalOrder name uni fun a
evalThis (Purity
-> WorkFreedom -> Term name uni fun a -> EvalTerm name uni fun a
forall name (uni :: * -> *) fun a.
Purity
-> WorkFreedom -> Term name uni fun a -> EvalTerm name uni fun a
EvalTerm Purity
Pure WorkFreedom
MaybeWork Term name uni fun a
t)
        -- then we go to an unknown scrutinee
        EvalOrder name uni fun a
-> EvalOrder name uni fun a -> EvalOrder name uni fun a
forall a. Semigroup a => a -> a -> a
<> EvalTerm name uni fun a -> EvalOrder name uni fun a
forall name (uni :: * -> *) fun a.
EvalTerm name uni fun a -> EvalOrder name uni fun a
evalThis EvalTerm name uni fun a
forall name (uni :: * -> *) fun a. EvalTerm name uni fun a
Unknown
    -- Leaf terms
    t :: Term name uni fun a
t@Var{} ->
      EvalTerm name uni fun a -> EvalOrder name uni fun a
forall name (uni :: * -> *) fun a.
EvalTerm name uni fun a -> EvalOrder name uni fun a
evalThis (Purity
-> WorkFreedom -> Term name uni fun a -> EvalTerm name uni fun a
forall name (uni :: * -> *) fun a.
Purity
-> WorkFreedom -> Term name uni fun a -> EvalTerm name uni fun a
EvalTerm Purity
Pure WorkFreedom
WorkFree Term name uni fun a
t)
    t :: Term name uni fun a
t@Error{} ->
      -- definitely effectful! but not relevant from a work perspective
      EvalTerm name uni fun a -> EvalOrder name uni fun a
forall name (uni :: * -> *) fun a.
EvalTerm name uni fun a -> EvalOrder name uni fun a
evalThis (Purity
-> WorkFreedom -> Term name uni fun a -> EvalTerm name uni fun a
forall name (uni :: * -> *) fun a.
Purity
-> WorkFreedom -> Term name uni fun a -> EvalTerm name uni fun a
EvalTerm Purity
MaybeImpure WorkFreedom
WorkFree Term name uni fun a
t)
        -- program terminates
        EvalOrder name uni fun a
-> EvalOrder name uni fun a -> EvalOrder name uni fun a
forall a. Semigroup a => a -> a -> a
<> EvalTerm name uni fun a -> EvalOrder name uni fun a
forall name (uni :: * -> *) fun a.
EvalTerm name uni fun a -> EvalOrder name uni fun a
evalThis EvalTerm name uni fun a
forall name (uni :: * -> *) fun a. EvalTerm name uni fun a
Unknown
    t :: Term name uni fun a
t@Builtin{} ->
      EvalTerm name uni fun a -> EvalOrder name uni fun a
forall name (uni :: * -> *) fun a.
EvalTerm name uni fun a -> EvalOrder name uni fun a
evalThis (Purity
-> WorkFreedom -> Term name uni fun a -> EvalTerm name uni fun a
forall name (uni :: * -> *) fun a.
Purity
-> WorkFreedom -> Term name uni fun a -> EvalTerm name uni fun a
EvalTerm Purity
Pure WorkFreedom
WorkFree Term name uni fun a
t)
    t :: Term name uni fun a
t@Delay{} ->
      EvalTerm name uni fun a -> EvalOrder name uni fun a
forall name (uni :: * -> *) fun a.
EvalTerm name uni fun a -> EvalOrder name uni fun a
evalThis (Purity
-> WorkFreedom -> Term name uni fun a -> EvalTerm name uni fun a
forall name (uni :: * -> *) fun a.
Purity
-> WorkFreedom -> Term name uni fun a -> EvalTerm name uni fun a
EvalTerm Purity
Pure WorkFreedom
WorkFree Term name uni fun a
t)
    t :: Term name uni fun a
t@LamAbs{} ->
      EvalTerm name uni fun a -> EvalOrder name uni fun a
forall name (uni :: * -> *) fun a.
EvalTerm name uni fun a -> EvalOrder name uni fun a
evalThis (Purity
-> WorkFreedom -> Term name uni fun a -> EvalTerm name uni fun a
forall name (uni :: * -> *) fun a.
Purity
-> WorkFreedom -> Term name uni fun a -> EvalTerm name uni fun a
EvalTerm Purity
Pure WorkFreedom
WorkFree Term name uni fun a
t)
    t :: Term name uni fun a
t@Constant{} ->
      EvalTerm name uni fun a -> EvalOrder name uni fun a
forall name (uni :: * -> *) fun a.
EvalTerm name uni fun a -> EvalOrder name uni fun a
evalThis (Purity
-> WorkFreedom -> Term name uni fun a -> EvalTerm name uni fun a
forall name (uni :: * -> *) fun a.
Purity
-> WorkFreedom -> Term name uni fun a -> EvalTerm name uni fun a
EvalTerm Purity
Pure WorkFreedom
WorkFree Term name uni fun a
t)

{- | 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)
  => BuiltinSemanticsVariant fun
  -> Term name uni fun a
  -> Bool
isPure :: forall (uni :: * -> *) fun name a.
ToBuiltinMeaning uni fun =>
BuiltinSemanticsVariant fun -> Term name uni fun a -> Bool
isPure BuiltinSemanticsVariant fun
builtinSemanticsVariant Term name uni fun a
term =
  -- 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 name uni fun a] -> Bool
forall name (uni :: * -> *) fun a.
[EvalTerm name uni fun a] -> Bool
go (EvalOrder name uni fun a -> [EvalTerm name uni fun a]
forall name (uni :: * -> *) fun a.
EvalOrder name uni fun a -> [EvalTerm name uni fun a]
unEvalOrder (BuiltinSemanticsVariant fun
-> Term name uni fun a -> EvalOrder name uni fun a
forall name (uni :: * -> *) fun a.
ToBuiltinMeaning uni fun =>
BuiltinSemanticsVariant fun
-> Term name uni fun a -> EvalOrder name uni fun a
termEvaluationOrder BuiltinSemanticsVariant fun
builtinSemanticsVariant Term name uni fun a
term))
 where
  go :: [EvalTerm name uni fun a] -> Bool
  go :: forall name (uni :: * -> *) fun a.
[EvalTerm name uni fun a] -> Bool
go [] = Bool
True
  go (EvalTerm name uni fun a
et : [EvalTerm name uni fun a]
rest) = case EvalTerm name uni fun a
et of
    -- Might be an effect here!
    EvalTerm Purity
MaybeImpure WorkFreedom
_ Term name uni fun a
_ -> Bool
False
    -- This term is fine, what about the rest?
    EvalTerm Purity
Pure WorkFreedom
_ Term name uni fun a
_        -> [EvalTerm name uni fun a] -> Bool
forall name (uni :: * -> *) fun a.
[EvalTerm name uni fun a] -> Bool
go [EvalTerm name uni fun a]
rest
    -- We don't know what will happen, so be conservative
    EvalTerm 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)
  => BuiltinSemanticsVariant fun
  -> Term name uni fun a
  -> Bool
isWorkFree :: forall (uni :: * -> *) fun name a.
ToBuiltinMeaning uni fun =>
BuiltinSemanticsVariant fun -> Term name uni fun a -> Bool
isWorkFree BuiltinSemanticsVariant fun
builtinSemanticsVariant Term name uni fun a
term =
  -- 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 name uni fun a] -> Bool
forall name (uni :: * -> *) fun a.
[EvalTerm name uni fun a] -> Bool
go (EvalOrder name uni fun a -> [EvalTerm name uni fun a]
forall name (uni :: * -> *) fun a.
EvalOrder name uni fun a -> [EvalTerm name uni fun a]
unEvalOrder (BuiltinSemanticsVariant fun
-> Term name uni fun a -> EvalOrder name uni fun a
forall name (uni :: * -> *) fun a.
ToBuiltinMeaning uni fun =>
BuiltinSemanticsVariant fun
-> Term name uni fun a -> EvalOrder name uni fun a
termEvaluationOrder BuiltinSemanticsVariant fun
builtinSemanticsVariant Term name uni fun a
term))
 where
  go :: [EvalTerm name uni fun a] -> Bool
  go :: forall name (uni :: * -> *) fun a.
[EvalTerm name uni fun a] -> Bool
go [] = Bool
True
  go (EvalTerm name uni fun a
et : [EvalTerm name uni fun a]
rest) = case EvalTerm name uni fun a
et of
    -- Might be an effect here!
    EvalTerm Purity
_ WorkFreedom
MaybeWork Term name uni fun a
_ -> Bool
False
    -- This term is fine, what about the rest?
    EvalTerm Purity
_ WorkFreedom
WorkFree Term name uni fun a
_  -> [EvalTerm name uni fun a] -> Bool
forall name (uni :: * -> *) fun a.
[EvalTerm name uni fun a] -> Bool
go [EvalTerm name uni fun a]
rest
    -- We don't know what will happen, so be conservative
    EvalTerm name uni fun a
Unknown                -> Bool
False