{-# 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
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
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
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
saturatesScheme TypeAppContext{} TypeSchemeArrow{} = Maybe Bool
forall a. Maybe a
Nothing
saturatesScheme TermAppContext{} TypeSchemeAll{} = Maybe Bool
forall a. Maybe a
Nothing
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
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 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
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)
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) =
(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)
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) ->
[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)
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
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
_ ->
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
(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
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)
t :: Term tyname name uni fun a
t@(Apply a
_ Term tyname name uni fun a
fun Term tyname name uni fun a
arg) ->
Term tyname name uni fun a -> EvalOrder tyname name uni fun a
goTerm Term tyname name uni fun a
fun
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
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)
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
_) ->
Term tyname name uni fun a -> EvalOrder tyname name uni fun a
goTerm Term tyname name uni fun a
ta
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)
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) ->
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) ->
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@(Constr a
_ Type tyname uni a
_ Word64
_ [Term tyname name uni fun a]
ts) ->
(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
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]
_) ->
Term tyname name uni fun a -> EvalOrder tyname name uni fun a
goTerm Term tyname name uni fun a
scrut
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)
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@(Var a
_ name
name) ->
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
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{} ->
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)
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
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
Just Saturation
Saturated -> EvalOrder tyname name uni fun a
maybeImpureWork
Just Saturation
Oversaturated -> EvalOrder tyname name uni fun a
maybeImpureWork
Just Saturation
Undersaturated -> EvalOrder tyname name uni fun a
pureWorkFree
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
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 =
[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
EvalTerm Purity
MaybeImpure WorkFreedom
_ Term tyname name uni fun a
_ -> Bool
False
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
EvalTerm tyname name uni fun a
Unknown -> Bool
False
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 =
[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
EvalTerm Purity
_ WorkFreedom
MaybeWork Term tyname name uni fun a
_ -> Bool
False
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
EvalTerm tyname name uni fun a
Unknown -> Bool
False