Package hydra

Interface Hoisting

  • public interface Hoisting
    Functions for deep term rewriting operations involving hoisting subterms or bindings into enclosing let terms.

    • Method Detail

      • augmentBindingsWithNewFreeVars

        static Pair<java.util.List<Binding>,​TermSubst> augmentBindingsWithNewFreeVars​(Graph cx,
                                                                                    java.util.Set<Name> boundVars,
                                                                                    java.util.List<Binding> bindings)
        Augment bindings with new free variables introduced by substitution, wrapping with lambdas after any type lambdas.

      • bindingIsPolymorphic

        static java.lang.Boolean bindingIsPolymorphic​(Binding binding)
        Check if a binding has a polymorphic type (non-empty list of type scheme variables)

      • bindingUsesContextTypeVars

        static java.lang.Boolean bindingUsesContextTypeVars​(Graph cx,
                                                    Binding binding)
        Check if a binding's type uses any type variables from the given Graph. Returns True if the free type variables in the binding's type intersect with the type variables in scope (graphTypeVariables).

      • countVarOccurrences

        static java.lang.Integer countVarOccurrences​(Name name,
                                             Term term)
        Count the number of occurrences of a variable name in a term. Assumes no variable shadowing.

      • hoistAllLetBindings

        static Let hoistAllLetBindings​(Let let0)
        Transform a let-term by pulling ALL let bindings to the top level. This is useful for targets like Java that don't support nested let expressions at all. If a hoisted binding captures lambda-bound variables from an enclosing scope, the binding is wrapped in lambdas for those variables, and references are replaced with applications. Note: Assumes no variable shadowing; use hydra.rewriting.unshadowVariables first.

      • hoistCaseStatements

        static Term hoistCaseStatements​(Graph v1,
                                Term v2)
        Hoist case statements into local let bindings. This is useful for targets such as Python which only support case statements (match) at the top level. Case statements are hoisted only when they appear at non-top-level positions. Top level = root, or reachable through annotations, let body/binding, lambda bodies, or ONE application LHS. Once through an application LHS, lambda bodies no longer count as pass-through.

      • hoistCaseStatementsInGraph

        static java.util.List<Binding> hoistCaseStatementsInGraph​(java.util.List<Binding> bindings)
        Hoist case statements into local let bindings for a list of bindings. This version operates prior to inference and uses an empty type context. It hoists case statements and their applied arguments into let bindings.

      • hoistLetBindingsWithContext

        static Let hoistLetBindingsWithContext​(java.util.function.Function<Binding,​java.lang.Boolean> isParentBinding,
                                       Graph cx,
                                       Let let0)
        Transform a let-term by pulling polymorphic let bindings to the top level, using Graph. A binding is hoisted if: (1) It is polymorphic (has non-empty typeSchemeVariables), OR (2) Its type uses type variables from the Graph (i.e., from enclosing type lambdas). Bindings which are already at the top level are not hoisted. If a hoisted binding captures lambda-bound or let-bound variables from an enclosing scope, the binding is wrapped in lambdas for those variables, and references are replaced with applications. If a hoisted binding uses type variables from the context, those type variables are added to the binding's type scheme. Note: we assume that there is no variable shadowing; use hydra.rewriting.unshadowVariables first.

      • hoistLetBindingsWithPredicate

        static Let hoistLetBindingsWithPredicate​(java.util.function.Function<Binding,​java.lang.Boolean> isParentBinding,
                                         java.util.function.Function<Graph,​java.util.function.Function<Binding,​java.lang.Boolean>> shouldHoistBinding,
                                         Graph cx0,
                                         Let let0)
        Transform a let-term by pulling let bindings to the top level. The isParentBinding predicate applies to top-level bindings and determines whether their subterm bindings are eligible for hoisting. The shouldHoistBinding predicate takes the Graph and a subterm binding, and returns True if the binding should be hoisted. This is useful for targets like Java that cannot have polymorphic definitions in arbitrary positions. The Graph provides information about type variables and lambda variables in scope. If a hoisted binding captures let-bound or lambda-bound variables from an enclosing scope, the binding is wrapped in lambdas for those variables, and references are replaced with applications. If a hoisted binding captures type variables from an enclosing type lambda scope, those type variables are added to the binding's type scheme, and references are replaced with type applications. Note: we assume that there is no variable shadowing; use hydra.rewriting.unshadowVariables first.

      • hoistLetBindingsWithPredicate_emptyBindingsAndNames

        static <T1,​T3> Pair<java.util.List<T3>,​T1> hoistLetBindingsWithPredicate_emptyBindingsAndNames​(Pair<java.util.List<Binding>,​T1> bindingsAndNames)

      • hoistLetBindingsWithPredicate_init

        static <T0> Pair<java.util.List<T0>,​java.util.Set<Name>> hoistLetBindingsWithPredicate_init​(Binding b)

      • hoistLetBindingsWithPredicate_rewrite

        static <T0,​T1,​T2> Pair<Pair<java.util.List<Binding>,​java.util.Set<Name>>,​Term> hoistLetBindingsWithPredicate_rewrite​(java.util.function.Function<java.lang.String,​java.util.function.Function<Graph,​java.util.function.Function<Pair<java.util.List<Pair<Binding,​Term>>,​java.util.Set<Name>>,​java.util.function.Function<Pair<Binding,​java.util.List<Name>>,​Pair<java.util.List<Pair<Binding,​Term>>,​java.util.Set<Name>>>>>> hoistOne,
                                                                                                                                             java.util.function.Function<Graph,​java.util.function.Function<java.util.Set<Name>,​java.util.function.Function<java.util.List<Binding>,​Pair<java.util.List<Binding>,​TermSubst>>>> hydra_hoisting_augmentBindingsWithNewFreeVars,
                                                                                                                                             java.util.function.Function<Binding,​java.lang.Boolean> hydra_hoisting_bindingIsPolymorphic,
                                                                                                                                             java.util.function.Function<Name,​java.util.function.Function<Term,​java.lang.Integer>> hydra_hoisting_countVarOccurrences,
                                                                                                                                             java.util.function.Function<Type,​java.lang.Boolean> hydra_resolution_fTypeIsPolymorphic,
                                                                                                                                             java.util.function.Function<TypeScheme,​Type> hydra_scoping_typeSchemeToFType,
                                                                                                                                             java.util.function.Function<TermSubst,​java.util.function.Function<Binding,​Binding>> hydra_substitution_substituteInBinding,
                                                                                                                                             java.util.function.Function<TermSubst,​java.util.function.Function<Term,​Term>> hydra_substitution_substituteInTerm,
                                                                                                                                             java.util.function.Function<Term,​java.util.Set<Name>> hydra_variables_freeVariablesInTerm,
                                                                                                                                             java.util.function.Function<Graph,​java.util.function.Function<Binding,​java.lang.Boolean>> shouldHoistBinding,
                                                                                                                                             java.lang.String prefix,
                                                                                                                                             java.util.function.Function<Pair<java.util.List<T0>,​T1>,​java.util.function.Function<T2,​Pair<Pair<java.util.List<Binding>,​java.util.Set<Name>>,​Term>>> recurse,
                                                                                                                                             Graph cx,
                                                                                                                                             Pair<java.util.List<Binding>,​T1> bindingsAndNames,
                                                                                                                                             T2 term)

      • hoistPolymorphicLetBindings

        static Let hoistPolymorphicLetBindings​(java.util.function.Function<Binding,​java.lang.Boolean> isParentBinding,
                                       Let let0)
        Transform a let-term by pulling all polymorphic let bindings to the top level. This is useful to ensure that polymorphic bindings are not nested within other terms, which is unsupported by certain targets such as Java. Polymorphic bindings are those with a non-empty list of type scheme variables. If a hoisted binding captures lambda-bound variables from an enclosing scope, the binding is wrapped in lambdas for those variables, and references are replaced with applications. Note: Assumes no variable shadowing; use hydra.rewriting.unshadowVariables first.

      • hoistSubterms

        static Term hoistSubterms​(java.util.function.Function<Pair<java.util.List<SubtermStep>,​Term>,​java.lang.Boolean> shouldHoist,
                          Graph cx0,
                          Term term0)
        Hoist subterms into local let bindings based on a path-aware predicate. The predicate receives a pair of (path, term) where path is the list of SubtermSteps from the root to the current term, and returns True if the term should be hoisted. For each let term found, the immediate subterms (binding values and body) are processed: matching subterms within each immediate subterm are collected and hoisted into a local let that wraps that immediate subterm. If a hoisted term contains free variables that are lambda-bound at an enclosing scope, the hoisted binding is wrapped in lambdas for those variables, and the reference is replaced with an application of those variables.

      • hoistSubterms_newCounter

        static <T1> T1 hoistSubterms_newCounter​(Pair<T1,​Term> recursed)

      • hoistSubterms_processLetTerm

        static <T0> Pair<T0,​Term> hoistSubterms_processLetTerm​(java.util.function.Function<Graph,​java.util.function.Function<java.lang.Integer,​java.util.function.Function<java.lang.String,​java.util.function.Function<java.util.List<SubtermStep>,​java.util.function.Function<Term,​Pair<java.lang.Integer,​Term>>>>>> processImmediateSubterm,
                                                             Graph cx,
                                                             T0 counter,
                                                             java.util.List<SubtermStep> path,
                                                             Let lt)

      • hoistSubterms_recursed

        static <T0,​T1> Pair<T1,​Term> hoistSubterms_recursed​(T0 counter,
                                                                java.util.function.Function<T0,​java.util.function.Function<Term,​Pair<T1,​Term>>> recurse,
                                                                Term term)

      • hoistSubterms_rewrite

        static <T0,​T1> Pair<T1,​Term> hoistSubterms_rewrite​(java.util.function.Function<Graph,​java.util.function.Function<java.lang.Integer,​java.util.function.Function<java.lang.String,​java.util.function.Function<java.util.List<SubtermStep>,​java.util.function.Function<Term,​Pair<java.lang.Integer,​Term>>>>>> processImmediateSubterm,
                                                               java.util.function.Function<T0,​java.util.function.Function<Term,​Pair<T1,​Term>>> recurse,
                                                               java.util.List<SubtermStep> path,
                                                               Graph cx,
                                                               T0 counter,
                                                               Term term)

      • isApplicationFunction

        static java.lang.Boolean isApplicationFunction​(SubtermStep acc)
        Check whether a SubtermStep is the applicationFunction step

      • isLambdaBody

        static java.lang.Boolean isLambdaBody​(SubtermStep acc)
        Check whether a SubtermStep is the lambdaBody step

      • isUnionElimination

        static java.lang.Boolean isUnionElimination​(Term term)
        Check if a term is a union elimination (case statement)

      • isUnionEliminationApplication

        static java.lang.Boolean isUnionEliminationApplication​(Term term)
        Check if a term is an application of a union elimination (case statement applied to an argument)

      • normalizePathForHoisting

        static java.util.List<SubtermStep> normalizePathForHoisting​(java.util.List<SubtermStep> path)
        Normalize a path for hoisting by treating immediately-applied lambdas as let bindings. Replaces [applicationFunction, lambdaBody, ...] with [letBody, ...].

      • shouldHoistAll

        static <T0,​T1> java.lang.Boolean shouldHoistAll​(T0 ignored,
                                                      T1 _2)
        Predicate that always returns True, for hoisting all bindings unconditionally.

      • shouldHoistCaseStatement

        static java.lang.Boolean shouldHoistCaseStatement​(Pair<java.util.List<SubtermStep>,​Term> pathAndTerm)
        Predicate for case statement hoisting. Returns True if term is a union elimination (bare case function) or a case statement application (union elimination applied to an argument) AND not at top level. Top level = reachable through annotations, let body/binding, lambda bodies, or ONE app LHS. Once through an app LHS, lambda bodies no longer pass through.

      • shouldHoistPolymorphic

        static java.lang.Boolean shouldHoistPolymorphic​(Graph cx,
                                                Binding binding)
        Predicate for hoisting polymorphic bindings. Returns True if the binding is polymorphic (has type scheme variables) or if its type uses any type variables from the Graph.

      • updateHoistState

        static Pair<java.lang.Boolean,​java.lang.Boolean> updateHoistState​(SubtermStep accessor,
                                                                        Pair<java.lang.Boolean,​java.lang.Boolean> state)
        Update hoisting state when traversing an accessor. State is (atTopLevel, usedAppLHS). Returns updated state.