refactor: behavior of inline annotations in the compiler (#12344)

This PR changes the semantics of `inline` annotations in the compiler.
The behavior of the original `@[inline]` attribute remains the same but
the function `inline` now comes with a restriction that it can only use
declarations that are local to the current module. This comes as a
preparation to pulling the compiler out into a separate process.

Closes: #12334

src/Lean/Compiler/LCNF/Simp/InlineCandidate.lean

@@ -40,9 +40,19 @@ def inlineCandidate? (e : LetValue .pure) : SimpM (Option InlineCandidateInfo) :
   let mut e := e
   let mut mustInline := false
   if let .const ``inline _ #[_, .fvar argFVarId] := e then
-    let some decl ← findLetDecl? argFVarId | return none
-    e := decl.value
     mustInline := true
+    if let some decl ← findFunDecl'? (pu := .pure) argFVarId then
+      e := .fvar decl.fvarId #[]
+    else if let some decl ← findLetDecl? argFVarId then
+      e := decl.value
+      if let .const declName _ _ := e then
+        if (← isCtor? declName).isSome then
+          throwError m!"`inline` applied to constructor '{declName}' is invalid"
+        else if (← getLocalDecl? declName).isNone then
+          throwError m!"`inline` applied to non-local declaration '{declName}' is invalid"
+    else
+      assert! (← findParam? (pu := .pure) argFVarId).isSome
+      throwError m!"`inline` applied to parameters is invalid"
   if let .const declName us args := e then
     unless (← read).config.inlineDefs do
       return none
@@ -101,7 +111,7 @@ def inlineCandidate? (e : LetValue .pure) : SimpM (Option InlineCandidateInfo) :
     }
   else if let .fvar f args := e then
     let some decl ← findFunDecl'? f | return none
-    unless args.size > 0 do return none -- It is not worth to inline a local function that does not take any arguments
+    unless mustInline || args.size > 0 do return none -- It is not worth to inline a local function that does not take any arguments
     unless mustInline || (← shouldInlineLocal decl) do return none
     -- Remark: we inline local function declarations even if they are partial applied
     incInlineLocal

src/lake/Lake/Build/Fetch.lean

@@ -48,7 +48,7 @@ public abbrev RecBuildT (m : Type → Type) :=
 
 /-- Build cycle error message. -/
 public def buildCycleError (cycle : Cycle BuildKey) : String :=
-  s!"build cycle detected:\n{inline <| formatCycle cycle}"
+  s!"build cycle detected:\n{formatCycle cycle}"
 
 public instance [Monad m] [MonadError m] : MonadCycleOf BuildKey (RecBuildT m) where
   throwCycle cycle := error (buildCycleError cycle)

src/lake/Lake/Build/Trace.lean

@@ -143,7 +143,7 @@ public def hex (self : Hash) : String :=
   lpad (String.ofList <| Nat.toDigits 16 self.val.toNat) '0' 16
 
 public def ofDecimal? (s : String) : Option Hash :=
-  (inline s.toNat?).map ofNat
+  s.toNat?.map ofNat
 
 @[inline] public def ofString? (s : String) : Option Hash :=
   ofHex? s

src/lake/Lake/Config/LeanConfig.lean

@@ -9,6 +9,7 @@ prelude
 public import Lake.Build.Target.Basic
 public import Lake.Config.Dynlib
 public import Lake.Config.MetaClasses
+public import Init.Data.String.Modify
 meta import all Lake.Config.Meta
 import Lake.Util.Name
 import Init.Data.String.Modify
@@ -43,6 +44,7 @@ namespace Backend
 
 public instance : Inhabited Backend := ⟨.default⟩
 
+@[inline]
 public def ofString? (s : String) : Option Backend :=
   match s with
   | "c" => some .c
@@ -118,6 +120,7 @@ public def leancArgs : BuildType → Array String
 | minSizeRel => #["-Os", "-DNDEBUG"]
 | release => #["-O3", "-DNDEBUG"]
 
+@[inline]
 public def ofString? (s : String) : Option BuildType :=
   match s.decapitalize with
   | "debug" => some .debug

src/lake/Lake/Load/Resolve.lean

@@ -94,7 +94,7 @@ abbrev ResolveT m := DepStackT <| StateT Workspace m
   (root := ws.root) (stack : DepStack  := {})
 : m Workspace := do
   let (_, ws) ← ResolveT.run ws (stack := stack) do
-    inline <| recFetchAcyclic (·.baseName) go root
+    recFetchAcyclic (·.baseName) go root
   return ws
 
 /-

src/lake/Lake/Load/Toml.lean

@@ -137,14 +137,14 @@ public protected def LeanOption.decodeToml (v : Value) : EDecodeM LeanOption :=
 public instance : DecodeToml LeanOption := ⟨LeanOption.decodeToml⟩
 
 public protected def BuildType.decodeToml (v : Value) : EDecodeM BuildType := do
-  match inline <| BuildType.ofString? (← v.decodeString) with
+  match BuildType.ofString? (← v.decodeString) with
   | some v => return v
   | none => throwDecodeErrorAt v.ref "expected one of 'debug', 'relWithDebInfo', 'minSizeRel', 'release'"
 
 public instance : DecodeToml BuildType := ⟨(BuildType.decodeToml ·)⟩
 
 public protected def Backend.decodeToml (v : Value) : EDecodeM Backend := do
-  match inline <| Backend.ofString? (← v.decodeString) with
+  match Backend.ofString? (← v.decodeString) with
   | some v => return v
   | none => throwDecodeErrorAt v.ref "expected one of 'c', 'llvm', or 'default'"
 

tests/lean/run/12334.lean

@@ -0,0 +1,24 @@
+import Std.Data.HashMap
+
+/-! Test some basic behavior related to `inline` discovered in #12334 -/
+
+#guard_msgs in
+def foo {n : Nat} (m : Std.HashMap Nat (Fin n)) : Std.HashMap Nat (Fin (n + 1)) :=
+  m.map <| inline fun _ ↦ Fin.castSucc
+
+/-- error: `inline` applied to parameters is invalid -/
+#guard_msgs in
+def params (n : Nat) : Nat := inline n
+
+#guard_msgs in
+def inlineLocal {n : Nat} (m : Std.HashMap Nat (Fin n)) : Std.HashMap Nat (Fin (n + 1)) :=
+  inline <| foo m
+
+/-- error: `inline` applied to constructor 'List.cons' is invalid -/
+#guard_msgs in
+def inlineCtor (x : Nat) (xs : List Nat) := inline <| List.cons x xs
+
+/-- error: `inline` applied to non-local declaration 'Lean.Name.mkStr3' is invalid -/
+#guard_msgs in
+def inlineNonLocal (s1 s2 s3 : String) :=
+  inline <| Lean.Name.mkStr3 s1 s2 s3