From acd2836cb583f0f2bba62c0bb84145cb14310ebc Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 6 Oct 2022 07:24:30 -0700
Subject: [PATCH] feat: add `saveMono` pass to normalize mono phase free
 variable ids

Motivation: control .olean size
---
 src/Lean/Compiler/LCNF/Passes.lean | 7 ++++++-
 1 file changed, 6 insertions(+), 1 deletion(-)

diff --git a/src/Lean/Compiler/LCNF/Passes.lean b/src/Lean/Compiler/LCNF/Passes.lean
index b7f4f655f8..d8062de059 100644
--- a/src/Lean/Compiler/LCNF/Passes.lean
+++ b/src/Lean/Compiler/LCNF/Passes.lean
@@ -36,6 +36,9 @@ def normalizeFVarIds (decl : Decl) : CoreM Decl := do
 def saveBase : Pass :=
   .mkPerDeclaration `saveBase (fun decl => do (← normalizeFVarIds decl).saveBase; return decl) .base
 
+def saveMono : Pass :=
+  .mkPerDeclaration `saveMono (fun decl => do (← normalizeFVarIds decl).saveMono; return decl) .mono
+
 def builtinPassManager : PassManager := {
   passes := #[
     init,
@@ -51,7 +54,9 @@ def builtinPassManager : PassManager := {
     simp (occurrence := 2),
     cse,
     saveBase, -- End of base phase
-    toMono
+    toMono,
+    -- TODO: lambda lifting, reduce function arity
+    saveMono  -- End of mono phase
   ]
 }