feat: add new compiler entry point function

src/Lean/Compiler.lean

@@ -15,4 +15,6 @@ import Lean.Compiler.CSimpAttr
 import Lean.Compiler.FFI
 import Lean.Compiler.NoncomputableAttr
 import Lean.Compiler.CompilerM
-import Lean.Compiler.LCNF
+import Lean.Compiler.LCNF
+import Lean.Compiler.Decl
+import Lean.Compiler.Main

src/Lean/Compiler/Decl.lean

@@ -0,0 +1,61 @@
+/-
+Copyright (c) 2022 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+import Lean.Meta.Transform
+import Lean.Compiler.LCNF
+
+namespace Lean.Compiler
+
+/--
+Declaration being processed by the Lean to Lean compiler passes.
+-/
+structure Decl where
+  name  : Name
+  type  : Expr
+  value : Expr
+
+/--
+Inline constants tagged with the `[macroInline]` attribute occurring in `e`.
+-/
+def macroInline (e : Expr) : CoreM Expr :=
+  Core.transform e fun e => do
+    let .const declName us := e.getAppFn | return .visit e
+    unless hasMacroInlineAttribute (← getEnv) declName do return .visit e
+    let val ← Core.instantiateValueLevelParams (← getConstInfo declName) us
+    return .visit <| val.beta e.getAppArgs
+
+/--
+Replace nested occurrences of `unsafeRec` names with the safe ones.
+-/
+private def replaceUnsafeRecNames (value : Expr) : CoreM Expr :=
+  Core.transform value fun e =>
+    match e with
+    | .const declName us =>
+      if let some safeDeclName := isUnsafeRecName? declName then
+        return .done (.const safeDeclName us)
+      else
+        return .done e
+    | _ => return .visit e
+
+/--
+Convert the given declaration from the Lean environment into `Decl`.
+
+Remarks:
+- If the declaration has an unsafe-rec version, we use it.
+- We eta-expand the declaration value.
+- We expand declarations tagged with the `[MacroInline]` attribute
+-/
+def toDecl (declName : Name) : CoreM Decl := do
+  let env ← getEnv
+  let some info := env.find? (mkUnsafeRecName declName) <|> env.find? declName | throwError "declaration `{declName}` not found"
+  let some value := info.value? | throwError "declaration `{declName}` does not have a value"
+  Meta.MetaM.run' do
+    let value ← Meta.lambdaTelescope value fun xs body => do Meta.mkLambdaFVars xs (← Meta.etaExpand body)
+    let value ← replaceUnsafeRecNames value
+    let value ← macroInline value
+    let value ← toLCNF {} value
+    return { name := declName, type := info.type, value }
+
+end Lean.Compiler

src/Lean/Compiler/LCNF.lean

@@ -47,16 +47,6 @@ change in the future when we add support for debugging information
 def isCompilerRelevantMData (_mdata : MData) : Bool :=
   false
 
-/--
-Inline constants tagged with the `[macroInline]` attribute occurring in `e`.
--/
-def macroInline (e : Expr) : CoreM Expr :=
-  Core.transform e fun e => do
-    let .const declName us := e.getAppFn | return .visit e
-    unless hasMacroInlineAttribute (← getEnv) declName do return .visit e
-    let val ← Core.instantiateValueLevelParams (← getConstInfo declName) us
-    return .visit <| val.beta e.getAppArgs
-
 namespace ToLCNF
 
 structure Context where
@@ -147,4 +137,6 @@ where
 
 end ToLCNF
 
+export ToLCNF (toLCNF)
+
 end Lean.Compiler

src/Lean/Compiler/Main.lean

@@ -0,0 +1,41 @@
+/-
+Copyright (c) 2022 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+import Lean.Compiler.LCNF
+import Lean.Compiler.Decl
+
+namespace Lean.Compiler
+
+/--
+We do not generate code for `declName` if
+- Its type is a proposition.
+- Its type is a type former.
+- It is tagged as `[macroInline]`.
+- It is matcher auxiliary function.
+- It is a type class instance.
+
+Remark: we still generate code for declarations tagged as `[inline]`
+and `[specialize]` since they can be partially applied.
+-/
+def shouldGenerateCode (declName : Name) : CoreM Bool := do
+  if (← isCompIrrelevant |>.run') then return false
+  if (← Meta.isMatcher declName) then return false
+  if hasMacroInlineAttribute (← getEnv) declName then return false
+  -- TODO: check if type class instance
+  return true
+where
+  isCompIrrelevant : MetaM Bool := do
+    let info ← getConstInfo declName
+    Meta.isProp info.type <||> Meta.isTypeFormerType info.type
+
+def compile (declNames : Array Name) : CoreM Unit := do
+  let declNames ← declNames.filterM shouldGenerateCode
+  let decls ← declNames.mapM toDecl
+  -- WIP
+  for decl in decls do
+    trace[Meta.debug] "{decl.name} := {decl.value}"
+    pure ()
+
+end Lean.Compiler

tests/lean/run/lcnf1.lean

@@ -2,9 +2,6 @@ import Lean
 
 open Lean Compiler Meta
 
-def test (declName : Name) : MetaM Unit := do
-  let .defnInfo info ← getConstInfo declName | throwError "definition expected"
-  let val ← ToLCNF.toLCNF {} (← macroInline info.value)
-  IO.println (← ppExpr val)
-
-#eval test ``Lean.Elab.Term.synthesizeInstMVarCore
+set_option trace.Meta.debug true
+set_option pp.funBinderTypes true
+#eval Compiler.compile #[``List.map]