{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE ViewPatterns #-}
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 (..))
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"
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"
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
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)
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) =
(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)
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
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
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) ->
Term name uni fun a -> EvalOrder name uni fun a
goTerm Term name uni fun a
fun
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
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
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
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) ->
Term name uni fun a -> EvalOrder name uni fun a
goTerm Term name uni fun a
dterm
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
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
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) ->
(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
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)
_) ->
Term name uni fun a -> EvalOrder name uni fun a
goTerm Term name uni fun a
scrut
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
<> 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@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{} ->
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)
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)
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 =
[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
EvalTerm Purity
MaybeImpure WorkFreedom
_ Term name uni fun a
_ -> Bool
False
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
EvalTerm name uni fun a
Unknown -> Bool
False
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 =
[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
EvalTerm Purity
_ WorkFreedom
MaybeWork Term name uni fun a
_ -> Bool
False
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
EvalTerm name uni fun a
Unknown -> Bool
False