Safe Haskell | Safe-Inferred |
---|---|
Language | Haskell2010 |
Synopsis
- isPure ∷ ToBuiltinMeaning uni fun ⇒ BuiltinSemanticsVariant fun → Term name uni fun a → Bool
- isWorkFree ∷ ToBuiltinMeaning uni fun ⇒ BuiltinSemanticsVariant fun → Term name uni fun a → Bool
- data EvalOrder name uni fun a
- unEvalOrder ∷ EvalOrder name uni fun a → [EvalTerm name uni fun a]
- data EvalTerm name uni fun a
- data Purity
- = MaybeImpure
- | Pure
- termEvaluationOrder ∷ ∀ name uni fun a. ToBuiltinMeaning uni fun ⇒ BuiltinSemanticsVariant fun → Term name uni fun a → EvalOrder name uni fun a
Documentation
isPure ∷ ToBuiltinMeaning uni fun ⇒ BuiltinSemanticsVariant fun → Term name uni fun a → Bool Source #
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).
isWorkFree ∷ ToBuiltinMeaning uni fun ⇒ BuiltinSemanticsVariant fun → Term name uni fun a → Bool Source #
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 name uni fun a Source #
The order in which terms get evaluated, along with their purities.
unEvalOrder ∷ EvalOrder name uni fun a → [EvalTerm name uni fun a] Source #
data EvalTerm name uni fun a Source #
Either the "next" term to be evaluated, along with its Purity
and WorkFreedom
,
or we don't know what comes next.
Is this pure? Either yes, or maybe not.
termEvaluationOrder ∷ ∀ name uni fun a. ToBuiltinMeaning uni fun ⇒ BuiltinSemanticsVariant fun → Term name uni fun a → EvalOrder name uni fun a Source #
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.