Hydra.Reduction

Functions for reducing terms and types, i.e. performing computations

Documentation

alphaConvert :: Ord m => Variable -> Term m -> Term m -> Term m

countPrimitiveFunctionInvocations :: Bool

betaReduceTerm :: (Ord m, Show m) => Term m -> GraphFlow m (Term m)

A beta reduction function which is designed for safety, not speed. This function does not assume that term to be evaluated is in a normal form, and will provide an informative error message if evaluation fails. Type checking is assumed to have already occurred.

betaReduceType :: (Ord m, Show m) => Type m -> GraphFlow m (Type m)

contractTerm :: Ord m => Term m -> Term m

Apply the special rules: ((x.e1) e2) == e1, where x does not appear free in e1 and ((x.e1) e2) = e1[x/e2] These are both limited forms of beta reduction which help to "clean up" a term without fully evaluating it.

etaReduceTerm :: Term m -> Term m

termIsClosed :: Term m -> Bool

Whether a term is closed, i.e. represents a complete program

termIsOpaque :: EvaluationStrategy -> Term m -> Bool

Whether a term is opaque to reduction, i.e. need not be reduced

termIsValue :: Context m -> EvaluationStrategy -> Term m -> Bool

Whether a term has been fully reduced to a "value"