Safe Haskell	Safe-Inferred
Language	Haskell2010

PlutusIR.Purity

Synopsis

isPure :: (TermUnique) => BuiltinsInfo uni fun -> VarsInfo tyname name uni a -> Term tyname name uni fun a -> Bool #
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).

isSaturated :: forall tyname name uni fun a. TermUnique) => BuiltinsInfo uni fun -> VarsInfo tyname name uni a -> Term tyname name uni fun a -> Bool #

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.

data EvalOrder tyname name uni fun a #

The order in which terms get evaluated, along with their purities. We use a DList here for efficient and lazy concatenation

Instances

Instances details

Doc ann #
Monoid (EvalOrder tyname name uni fun a) #
Instance details Defined in PlutusIR.Purity Methods mempty :: 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 # mconcat :: [EvalOrder tyname name uni fun a] -> EvalOrder tyname name uni fun a #
Semigroup (EvalOrder tyname name uni fun a) #
Instance details Defined in PlutusIR.Purity Methods (<>) :: EvalOrder tyname name uni fun a -> 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 # stimes :: Integral b => b -> EvalOrder tyname name uni fun a -> EvalOrder tyname name uni fun a #

unEvalOrder :: EvalOrder tyname name uni fun a -> [EvalTerm tyname name uni fun a] #

Get the evaluation order as a list of EvalTerms. 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.

data EvalTerm tyname name uni fun a #

Either the "next" term to be evaluated, along with its Purity and WorkFreedom, or we don't know what comes next.

Constructors

Unknown
EvalTerm Purity WorkFreedom (Term tyname name uni fun a)

Instances

Instances details

TermUnique) => BuiltinsInfo uni fun -> VarsInfo tyname name uni a -> Term tyname name uni fun a -> EvalOrder tyname name uni fun a #

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.