scalus.compiler.sir.transform

Boolean-algebra simplification on SIR, run before lowering.

Every rule here must be semantics preserving, not just truth-table preserving: in UPLC a subterm can Error or trace, so a rule may never drop an operand that the original expression would have evaluated. And/Or/Not all lower to SIR.IfThenElse (scalus.compiler.sir.lowering.Lowering):

And(a, b) => if a then b     else false
Or(a, b)  => if a then true  else b
Not(a)    => if a then false else true

so a is always evaluated and b only conditionally. That asymmetry decides which folds are legal - see mkAnd/mkOr.

Implemented rules:

• double negation: Not(Not(a)) => a
• conditional negation: If(Not(c), t, f) => If(c, f, t) (saves one Case/ifThenElse)
• reverse De Morgan (one node fewer): Or(Not(a), Not(b)) => Not(And(a, b)) and And(Not(a), Not(b)) => Not(Or(a, b))
• constant folding of Not, and of If with a constant condition
• identity/annihilation folds that do not drop an evaluated operand

Deliberately NOT implemented, because they drop an operand the original evaluates: a && !a => false, a || !a => true, And(a, false) => false, Or(a, true) => true, If(c, t, t) => t. Idempotence (a && a => a) is out for the same reason: it evaluates a once where the original evaluates it twice, halving a duplicated trace.

The pass is a single bottom-up rebuild: children are optimized first, then the smart constructors apply the rules to already-optimized children. Rules never re-enter a full traversal, so the cost is linear in the tree size.

Static-argument transformation (T1 of docs/internal/CODEGEN_IMPROVEMENT_PLAN.md).

A parameter of a single-binding recursive Let is static when every self-call passes exactly that parameter's own variable in the same position. Static parameters are bound once by a wrapper lambda, and the inner recursion re-passes only the changing ones:

 let rec f = λp1...pn. body                     // some pi static in every self-call
 -->
 let f = λp1...pn.
     let rec f$sat = λq1...qk. body[ f e1...en := f$sat e_q1...e_qk ]
     in f$sat q1...qk                           // q = changing params, in source order

When the static parameters form a prefix (the common case, e.g. go f n acc with an invariant f) a leaner shape is used instead - the wrapper binds only the static prefix and returns the fixpoint itself, so the changing parameters are consumed by f$sat directly:

 let f = λp1...pj. let rec f$sat = λq1...qk. body' in f$sat

The wrapper keeps the original name, arity and type, so external uses of f (partial applications, higher-order uses, eta-lets) are unaffected. The fixpoint is built once per entry into f instead of once per iteration, and each iteration saves one Apply per lifted argument.

The transform is skipped (input returned unchanged) when it cannot be proven safe:

• multi-binding recursive Lets (mutual-recursion groups) and lazy lets;
• a rhs that is not a lambda, or has duplicate parameter names;
• any self-reference that is not the head of a self-call saturated to full arity (a bare reference or a partial application could observe the original arity);
• no static parameter at all.

If every parameter is static the last one is demoted to changing, because a nullary strict letrec would diverge.

Runs only when optimization is enabled - see scalus.compiler.sir.lowering.UplcPipeline.run, which is the single place this pass is invoked from. It runs after MutualRecursionElimination, so the peers-as-params static arguments that pass introduces (a $mutrec peer re-passing f1 .. f(i-1) unchanged on every self-call) are lifted here too.