Commit 2025-12-05 13:19 55bbac04

feat(translate): refactor applyReplacementFun and more (#32176) This PR cleans up a lot of the to_additive implementation. applyReplacementFun is cleaned up:

• Instead of running shouldTranslate at every single constant appliaction, we now only run it on constant applications where the head constant can actually be translated
• The option for translating numerals was mistakenly not actually looked at. This means that to_dual would translate the numeral 1 to 0. This is fixed.
• We remove the Expr.proj handling, because these are already handled by expand.
• The if gf.isBVar && x.isLit is now not needed anymore and is removed.
• It now uses memoFix instead of Lean.Expr.replaceRec, which will is more transparent, and will allow us to change the monad in the future if needed. Some more cleanups:
• transformDecl has been removed/inlined since it is a small function only used once.
• transformDeclAux has been renamed to transformDeclRec (as it recursively transforms the declarations appearing inside the declaration). It now recursively calls itself with an empty reorder and dontTranslate, which helps avoid a case split.
• In ToAdditive and ToDual, an unused piece of syntax has been removed.
• memoFix has been reimplemented to actually use pointer equality.