Package hydra

Interface Reduction

public interface Reduction

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

Method Summary

Static Methods

Modifier and Type	Method	Description
static Term	alphaConvert(Name vold, Name vnew, Term term)
static Either<InContext<Error_>,Type>	betaReduceType(Context cx, Graph graph, Type typ)
static <T0> Either<InContext<Error_>,Type>	betaReduceType_mapExpr(java.util.function.Function<ApplicationType,Either<InContext<Error_>,Type>> reduceApp, java.util.function.Function<T0,Either<InContext<Error_>,Type>> recurse, T0 t)
static Term	contractTerm(Term term)
static <T0> Term	contractTerm_rewrite(java.util.function.Function<Term,Term> hydra_rewriting_deannotateTerm2, java.util.function.Function<Name,java.util.function.Function<Term,java.lang.Boolean>> hydra_rewriting_isFreeVariableInTerm2, java.util.function.Function<Name,java.util.function.Function<Term,java.util.function.Function<Term,Term>>> hydra_rewriting_replaceFreeTermVariable2, java.util.function.Function<T0,Term> recurse, T0 t)
static java.lang.Boolean	countPrimitiveInvocations()
static Term	etaExpandTerm(Graph graph, Term term)
static Term	etaExpandTermNew(Graph tx0, Term term0)
static Either<InContext<Error_>,Term>	etaExpandTypedTerm(Context cx, Graph tx0, Term term0)
static java.lang.Integer	etaExpansionArity(Graph graph, Term term)
static Term	etaReduceTerm(Term term)
static Either<InContext<Error_>,Term>	reduceTerm(Context cx, Graph graph, java.lang.Boolean eager, Term term)
static java.lang.Boolean	termIsClosed(Term term)
static java.lang.Boolean	termIsValue(Term term)

Method Detail

alphaConvert

static Term alphaConvert(Name vold,
                         Name vnew,
                         Term term)

betaReduceType

static Either<InContext<Error_>,Type> betaReduceType(Context cx,
                                                           Graph graph,
                                                           Type typ)

betaReduceType_mapExpr

static <T0> Either<InContext<Error_>,Type> betaReduceType_mapExpr(java.util.function.Function<ApplicationType,Either<InContext<Error_>,Type>> reduceApp,
                                                                        java.util.function.Function<T0,Either<InContext<Error_>,Type>> recurse,
                                                                        T0 t)

contractTerm

static Term contractTerm(Term term)

contractTerm_rewrite

static <T0> Term contractTerm_rewrite(java.util.function.Function<Term,Term> hydra_rewriting_deannotateTerm2,
                                      java.util.function.Function<Name,java.util.function.Function<Term,java.lang.Boolean>> hydra_rewriting_isFreeVariableInTerm2,
                                      java.util.function.Function<Name,java.util.function.Function<Term,java.util.function.Function<Term,Term>>> hydra_rewriting_replaceFreeTermVariable2,
                                      java.util.function.Function<T0,Term> recurse,
                                      T0 t)

countPrimitiveInvocations

static java.lang.Boolean countPrimitiveInvocations()

etaExpandTerm

static Term etaExpandTerm(Graph graph,
                          Term term)

etaExpandTermNew

static Term etaExpandTermNew(Graph tx0,
                             Term term0)

etaExpandTypedTerm

static Either<InContext<Error_>,Term> etaExpandTypedTerm(Context cx,
                                                               Graph tx0,
                                                               Term term0)

etaExpansionArity

static java.lang.Integer etaExpansionArity(Graph graph,
                                           Term term)

etaReduceTerm

static Term etaReduceTerm(Term term)

reduceTerm

static Either<InContext<Error_>,Term> reduceTerm(Context cx,
                                                       Graph graph,
                                                       java.lang.Boolean eager,
                                                       Term term)

termIsClosed

static java.lang.Boolean termIsClosed(Term term)

termIsValue

static java.lang.Boolean termIsValue(Term term)