EtaReduce

Performs eta-reduction on a term.

Eta-reduction is the process of removing redundant lambda abstractions from a term. For example, the term λx. f x can be eta-reduced to f but only if

• x is not free in f
• f is a pure expression

Purity checking is handled by TermAnalysis.isPure. A term is pure if it does not contain any side effects, such as Error, Force of non-delayed terms, or saturated builtin applications. See TermAnalysis.isPure for comprehensive documentation on purity semantics.

On top of the syntactic purity check, the pass tracks a value-arity environment for [(lam x body) rhs] let-bindings: when rhs provably evaluates to a lambda of arity n (counting the self-application fixpoint encoding [(lam f [f f]) (lam f (lam a ... body))] produced for recursive functions), a partial application x a1 ... ak with k < n pure arguments is itself a pure expression, so multi-argument eta-wrappers like λa. λb. f a b reduce to f. This removes the wrapper the compiler emits around a multi-parameter recursive entry point ([(lam f (lam a (lam b [f a b]))) fix] becomes [(lam f f) fix], which the Inliner then collapses to fix). The same wrapper in the case-constr application encoding — (lam a (lam b (case (constr 0 a b) f))) as produced by CaseConstrApply — reduces too, see caseConstrEtaRedex.

'''Precondition: named terms only.''' Every analysis here — the arities environment, the capture checks via TermAnalysis.freeVars, and the field matching in caseConstrEtaRedex — identifies variables by NAME and ignores NamedDeBruijn.index, so scope is whatever the binder nesting says it is. That is the representation the compiler pipeline produces: UplcPipeline hands optimizers a named term and de Bruijn indices are only assigned later, at Program.deBruijnedProgram. Do not run this pass on an already-de-Bruijned term (one whose Var indices are meaningful — the CEK requires that form, see lookupVarName, which rejects index 0): there, two distinct binders may share a name, and name-based scoping would conflate them.