hydra-0.1.0: Type-aware transformations for data and functional programs
Safe HaskellSafe-Inferred
LanguageHaskell2010

Hydra.Reduction

Synopsis

Documentation

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

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

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) Source #

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

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.

termIsClosed :: Term m -> Bool Source #

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

termIsOpaque :: EvaluationStrategy -> Term m -> Bool Source #

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

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

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