hydra.hoisting module

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

hydra.hoisting.augment_bindings_with_new_free_vars(cx: Graph, bound_vars: Set[Name], bindings: Sequence[Binding]) → tuple[Sequence[Binding], TermSubst]

Augment bindings with new free variables introduced by substitution, wrapping with lambdas after any type lambdas.

hydra.hoisting.binding_is_polymorphic(binding: Binding) → bool

Check if a binding has a polymorphic type (non-empty list of type scheme variables).

hydra.hoisting.binding_uses_context_type_vars(cx: Graph, binding: Binding) → bool

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).

hydra.hoisting.count_var_occurrences(name: Name, term: Term) → int

Count the number of occurrences of a variable name in a term. Assumes no variable shadowing.

hydra.hoisting.hoist_all_let_bindings(let0: Let) → Let

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.

hydra.hoisting.hoist_case_statements(v1: Graph, v2: Term) → Term

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.

hydra.hoisting.hoist_case_statements_in_graph(bindings: Sequence[Binding]) → Sequence[Binding]

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.

hydra.hoisting.hoist_let_bindings_with_context(is_parent_binding: Callable[[Binding], bool], cx: Graph, let0: Let) → Let

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.

hydra.hoisting.hoist_let_bindings_with_predicate(is_parent_binding: Callable[[Binding], bool], should_hoist_binding: Callable[[Graph, Binding], bool], cx0: Graph, let0: Let) → Let

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.

hydra.hoisting.hoist_polymorphic_let_bindings(is_parent_binding: Callable[[Binding], bool], let0: Let) → Let

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.

hydra.hoisting.hoist_subterms(should_hoist: Callable[[tuple[Sequence[SubtermStep], Term]], bool], cx0: Graph, term0: Term) → Term

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.

hydra.hoisting.is_application_function(acc: SubtermStep) → bool

Check whether a SubtermStep is the applicationFunction step.

hydra.hoisting.is_lambda_body(acc: SubtermStep) → bool

Check whether a SubtermStep is the lambdaBody step.

hydra.hoisting.is_union_elimination(term: Term) → bool

Check if a term is a union elimination (case statement).

hydra.hoisting.is_union_elimination_application(term: Term) → bool

Check if a term is an application of a union elimination (case statement applied to an argument).

hydra.hoisting.normalize_path_for_hoisting(path: Sequence[SubtermStep]) → Sequence[SubtermStep]

Normalize a path for hoisting by treating immediately-applied lambdas as let bindings. Replaces [applicationFunction, lambdaBody, …] with [letBody, …].

hydra.hoisting.should_hoist_all(_: T0, _2: T1) → bool

Predicate that always returns True, for hoisting all bindings unconditionally.

hydra.hoisting.should_hoist_case_statement(path_and_term: tuple[Sequence[SubtermStep], Term]) → bool

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.

hydra.hoisting.should_hoist_polymorphic(cx: Graph, binding: Binding) → bool

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.

hydra.hoisting.update_hoist_state(accessor: SubtermStep, state: tuple[bool, bool]) → tuple[bool, bool]

Update hoisting state when traversing an accessor. State is (atTopLevel, usedAppLHS). Returns updated state.