From e4f0f4b794610e13c72f87f53db1c8545a8a90e4 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 23 Sep 2022 14:25:48 -0700
Subject: [PATCH] fix: `shouldGenerateCode` fix for `axiom`

---
 src/Lean/Compiler/LCNF/Main.lean   |  3 ++-
 src/Lean/Compiler/LCNF/ToDecl.lean | 12 ++++++++++--
 src/Lean/Compiler/LCNF/Util.lean   |  1 -
 3 files changed, 12 insertions(+), 4 deletions(-)

diff --git a/src/Lean/Compiler/LCNF/Main.lean b/src/Lean/Compiler/LCNF/Main.lean
index e2b33b9372..793b2c2299 100644
--- a/src/Lean/Compiler/LCNF/Main.lean
+++ b/src/Lean/Compiler/LCNF/Main.lean
@@ -27,7 +27,8 @@ and `[specialize]` since they can be partially applied.
 -/
 def shouldGenerateCode (declName : Name) : CoreM Bool := do
   if (← isCompIrrelevant |>.run') then return false
-  unless (← getConstInfo declName).hasValue do return false
+  let some info ← getDeclInfo? declName | return false
+  unless info.hasValue do return false
   let env ← getEnv
   if hasMacroInlineAttribute env declName then return false
   if (← Meta.isMatcher declName) then return false
diff --git a/src/Lean/Compiler/LCNF/ToDecl.lean b/src/Lean/Compiler/LCNF/ToDecl.lean
index 6aef643267..642ea09b3d 100644
--- a/src/Lean/Compiler/LCNF/ToDecl.lean
+++ b/src/Lean/Compiler/LCNF/ToDecl.lean
@@ -74,6 +74,15 @@ private def replaceUnsafeRecNames (value : Expr) : CoreM Expr :=
         return .done e
     | _ => return .continue
 
+/--
+Return the declaration `ConstantInfo` for the code generator.
+
+Remark: the unsafe recursive version is tried first.
+-/
+def getDeclInfo? (declName : Name) : CoreM (Option ConstantInfo) := do
+  let env ← getEnv
+  return env.find? (mkUnsafeRecName declName) <|> env.find? declName
+
 /--
 Convert the given declaration from the Lean environment into `Decl`.
 The steps for this are roughly:
@@ -84,8 +93,7 @@ The steps for this are roughly:
 - turn the resulting term into LCNF declaration
 -/
 def toDecl (declName : Name) : CompilerM Decl := do
-  let env ← getEnv
-  let some info := env.find? (mkUnsafeRecName declName) <|> env.find? declName | throwError "declaration `{declName}` not found"
+  let some info ← getDeclInfo? declName | throwError "declaration `{declName}` not found"
   let some value := info.value? | throwError "declaration `{declName}` does not have a value"
   let (type, value) ← Meta.MetaM.run' do
     let type  ← toLCNFType info.type
diff --git a/src/Lean/Compiler/LCNF/Util.lean b/src/Lean/Compiler/LCNF/Util.lean
index e325246f4d..a1c7f82c00 100644
--- a/src/Lean/Compiler/LCNF/Util.lean
+++ b/src/Lean/Compiler/LCNF/Util.lean
@@ -8,7 +8,6 @@ import Lean.MonadEnv
 import Lean.Util.Recognizers
 
 namespace Lean.Compiler.LCNF
-
 /--
 Return `true` if `mdata` should be preserved.
 Right now, we don't preserve any `MData`, but this may