{-# 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 (..)
  , WorkFreedom (..)
  , termEvaluationOrder
  ) where

import Data.DList qualified as DList
import Data.Typeable (Proxy (..))
import PlutusCore.Arity (Param (..), builtinArity)
import PlutusCore.Builtin.Meaning (ToBuiltinMeaning (..))
import PlutusCore.Pretty (Pretty (pretty), PrettyBy (prettyBy))
import Prettyprinter (vsep, (<+>))
import Universe.Core (Closed, Everywhere, GShow)
import UntypedPlutusCore.Contexts (AppCtx (..), fillAppCtx, splitAppCtx)
import UntypedPlutusCore.Core (Term (..))
import UntypedPlutusCore.Core.Instance.Eq ()

-- | Is this pure? Either yes, or maybe not.
data Purity = MaybeImpure | Pure
  deriving stock (Purity -> Purity -> Bool
(Purity -> Purity -> Bool)
-> (Purity -> Purity -> Bool) -> Eq Purity
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Purity -> Purity -> Bool
== :: Purity -> Purity -> Bool
$c/= :: Purity -> Purity -> Bool
/= :: Purity -> Purity -> Bool
Eq, Int -> Purity -> ShowS
[Purity] -> ShowS
Purity -> String
(Int -> Purity -> ShowS)
-> (Purity -> String) -> ([Purity] -> ShowS) -> Show Purity
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Purity -> ShowS
showsPrec :: Int -> Purity -> ShowS
$cshow :: Purity -> String
show :: Purity -> String
$cshowList :: [Purity] -> ShowS
showList :: [Purity] -> ShowS
Show)

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
  deriving stock (WorkFreedom -> WorkFreedom -> Bool
(WorkFreedom -> WorkFreedom -> Bool)
-> (WorkFreedom -> WorkFreedom -> Bool) -> Eq WorkFreedom
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: WorkFreedom -> WorkFreedom -> Bool
== :: WorkFreedom -> WorkFreedom -> Bool
$c/= :: WorkFreedom -> WorkFreedom -> Bool
/= :: WorkFreedom -> WorkFreedom -> Bool
Eq, Int -> WorkFreedom -> ShowS
[WorkFreedom] -> ShowS
WorkFreedom -> String
(Int -> WorkFreedom -> ShowS)
-> (WorkFreedom -> String)
-> ([WorkFreedom] -> ShowS)
-> Show WorkFreedom
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> WorkFreedom -> ShowS
showsPrec :: Int -> WorkFreedom -> ShowS
$cshow :: WorkFreedom -> String
show :: WorkFreedom -> String
$cshowList :: [WorkFreedom] -> ShowS
showList :: [WorkFreedom] -> ShowS
Show)

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
 ( Show name
 , Everywhere uni Show
 , Show fun
 , Show a
 , GShow uni
 , Closed uni
 ) => Show (EvalTerm name uni fun a) where
  show :: EvalTerm name uni fun a -> String
show = \case
    EvalTerm name uni fun a
Unknown -> String
"<unknown>"
    EvalTerm Purity
purity WorkFreedom
work Term name uni fun a
t ->
      String
"EvalTerm " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> Purity -> String
forall a. Show a => a -> String
show Purity
purity String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
" " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> WorkFreedom -> String
forall a. Show a => a -> String
show WorkFreedom
work String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
" " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> Term name uni fun a -> String
forall a. Show a => a -> String
show Term name uni fun a
t

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

instance Eq (Term name uni fun a) => Eq (EvalTerm name uni fun a) where
  EvalTerm name uni fun a
Unknown == :: EvalTerm name uni fun a -> EvalTerm name uni fun a -> Bool
== EvalTerm name uni fun a
Unknown                         = Bool
True
  (EvalTerm Purity
p1 WorkFreedom
w1 Term name uni fun a
t1) == (EvalTerm Purity
p2 WorkFreedom
w2 Term name uni fun a
t2) = Purity
p1 Purity -> Purity -> Bool
forall a. Eq a => a -> a -> Bool
== Purity
p2 Bool -> Bool -> Bool
&& WorkFreedom
w1 WorkFreedom -> WorkFreedom -> Bool
forall a. Eq a => a -> a -> Bool
== WorkFreedom
w2 Bool -> Bool -> Bool
&& Term name uni fun a
t1 Term name uni fun a -> Term name uni fun a -> Bool
forall a. Eq a => a -> a -> Bool
== Term name uni fun a
t2
  EvalTerm name uni fun a
_ == EvalTerm name uni fun a
_                                     = Bool
False

-- 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 :: Term name uni fun a -> EvalOrder name uni fun a
goTerm = \case
    (Term name uni fun a -> (Term name uni fun a, AppCtx name uni fun a)
forall nam (uni :: * -> *) fun a.
Term nam uni fun a -> (Term nam uni fun a, AppCtx nam uni fun a)
splitAppCtx -> (builtin :: Term name uni fun a
builtin@(Builtin a
_ann fun
fun), AppCtx name uni fun a
appCtx)) ->
      AppCtx name uni fun a -> EvalOrder name uni fun a
appCtxEvalOrder AppCtx name uni fun a
appCtx EvalOrder name uni fun a
-> EvalOrder name uni fun a -> EvalOrder name uni fun a
forall a. Semigroup a => a -> a -> a
<> [Param] -> AppCtx name uni fun a -> EvalOrder name uni fun a
go [Param]
arity AppCtx name uni fun a
appCtx
     where
      arity :: [Param]
arity = 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

      appCtxEvalOrder :: AppCtx name uni fun a -> EvalOrder name uni fun a
      appCtxEvalOrder :: AppCtx name uni fun a -> EvalOrder name uni fun a
appCtxEvalOrder = \case
        AppCtx name uni fun a
AppCtxEnd -> EvalOrder name uni fun a
forall a. Monoid a => a
mempty
        AppCtxTerm a
_ Term name uni fun a
t AppCtx name uni fun a
rest -> Term name uni fun a -> EvalOrder name uni fun a
goTerm 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
<> AppCtx name uni fun a -> EvalOrder name uni fun a
appCtxEvalOrder AppCtx name uni fun a
rest
        AppCtxType a
_ AppCtx name uni fun a
rest -> AppCtx name uni fun a -> EvalOrder name uni fun a
appCtxEvalOrder AppCtx name uni fun a
rest

      go :: [Param] -> AppCtx name uni fun a -> EvalOrder name uni fun a
      go :: [Param] -> AppCtx name uni fun a -> EvalOrder name uni fun a
go [Param]
parameters AppCtx name uni fun a
appContext =
        case [Param]
parameters of
          -- All builtin parameters have been applied,
          -- (such term is considered impure).
          [] -> EvalOrder name uni fun a
maybeImpureWork

          -- A term parameter is waiting to be applied
          Param
TermParam : [Param]
otherParams ->
            case AppCtx name uni fun a
appContext of
              AppCtx name uni fun a
AppCtxEnd ->
                -- Builtin is not fully saturated with term arguments, thus pure.
                EvalOrder name uni fun a
pureWorkFree
              AppCtxType a
_ann AppCtx name uni fun a
_remainingAppCtx ->
                -- Term parameter expected, type argument applied.
                -- Error is impure.
                EvalOrder name uni fun a
maybeImpureWork
              AppCtxTerm a
_ann Term name uni fun a
_argTerm AppCtx name uni fun a
remainingAppCtx ->
                [Param] -> AppCtx name uni fun a -> EvalOrder name uni fun a
go [Param]
otherParams AppCtx name uni fun a
remainingAppCtx

          -- A type parameter is waiting to be forced
          Param
TypeParam : [Param]
otherParams ->
            case AppCtx name uni fun a
appContext of
              AppCtx name uni fun a
AppCtxEnd ->
                -- Builtin is not fully saturated with type arguments, thus pure.
                EvalOrder name uni fun a
pureWorkFree
              AppCtxTerm a
_ann Term name uni fun a
_term AppCtx name uni fun a
_remainingAppCtx ->
                -- Type parameter expected, term argument applied.
                -- Error is impure.
                EvalOrder name uni fun a
maybeImpureWork
              AppCtxType a
_ann AppCtx name uni fun a
remainingAppCtx ->
                [Param] -> AppCtx name uni fun a -> EvalOrder name uni fun a
go [Param]
otherParams AppCtx name uni fun a
remainingAppCtx

        where
        maybeImpureWork :: EvalOrder name uni fun a
        maybeImpureWork :: EvalOrder name uni fun a
maybeImpureWork = 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
reconstructed)

        pureWorkFree :: EvalOrder name uni fun a
        pureWorkFree :: EvalOrder name uni fun a
pureWorkFree = 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
reconstructed)

        reconstructed :: Term name uni fun a
        reconstructed :: Term name uni fun a
reconstructed = Term name uni fun a -> AppCtx name uni fun a -> Term name uni fun a
forall name (uni :: * -> *) fun ann.
Term name uni fun ann
-> AppCtx name uni fun ann -> Term name uni fun ann
fillAppCtx Term name uni fun a
builtin AppCtx name uni fun a
appCtx

    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, unless there's no
        -- arguments, in which case it's not more work than evaluating, say, a @Delay@ node
        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 (if [Term name uni fun a] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Term name uni fun a]
ts then WorkFreedom
WorkFree else 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