fix: enforce implicit invariants in EmitC stronger (#11381)

This PR fixes a bug where the closed term extraction does not respect
the implicit invariant of the
c emitter to have closed term decls first, other decls second, within an
SCC. This bug has not yet
been triggered in the wild but was unearthed during work on upcoming
modifications of the
specializer.

Author: hargoniX

src/Lean/Compiler/LCNF/ExtractClosed.lean

@@ -141,17 +141,27 @@ def visitDecl (decl : Decl) : M Decl := do
 
 end ExtractClosed
 
-partial def Decl.extractClosed (decl : Decl) (sccDecls : Array Decl) : CompilerM (Array Decl) := do
+partial def Decl.extractClosed (decl : Decl) (sccDecls : Array Decl) : CompilerM (Decl × Array Decl) := do
   let ⟨decl, s⟩ ← ExtractClosed.visitDecl decl |>.run { baseName := decl.name, sccDecls } |>.run {}
-  return s.decls.push decl
+  return (decl, s.decls)
 
 def extractClosed : Pass where
   phase := .mono
   name := `extractClosed
   run := fun decls => do
     if (← getConfig).extractClosed then
-      decls.foldlM (init := #[]) fun newDecls decl =>
-        return newDecls ++ (← decl.extractClosed decls)
+      let mut changedDecls := Array.emptyWithCapacity decls.size
+      let mut closedDecls := #[]
+      for decl in decls do
+        let (change, new) ← decl.extractClosed decls
+        changedDecls := changedDecls.push change
+        closedDecls := closedDecls ++ new
+
+      /-
+      EmitC later relies on the fact that within an SCC the closed term declarations come first,
+      then the declarations that rely on them.
+      -/
+      return closedDecls ++ changedDecls
     else
       return decls
 

tests/lean/run/emptyLcnf.lean

@@ -11,17 +11,7 @@ trace: [Compiler.result] size: 0
     def f x : Nat :=
       ⊥
 ---
-trace: [Compiler.result] size: 5
-    def _private.lean.run.emptyLcnf.0._eval._lam_0 _x.1 _x.2 _y.3 _y.4 _y.5 _y.6 _y.7 _y.8 _y.9 : EST.Out Lean.Exception
-      lcAny PUnit :=
-      let _x.10 := Lean.Compiler.compile _x.1 _y.7 _y.8 _y.9;
-      cases _x.10 : EST.Out Lean.Exception lcAny PUnit
-      | EST.Out.ok a.11 a.12 =>
-        let _x.13 := @EST.Out.ok ◾ ◾ ◾ _x.2 a.12;
-        return _x.13
-      | EST.Out.error a.14 a.15 =>
-        return _x.10
-[Compiler.result] size: 1
+trace: [Compiler.result] size: 1
     def _private.lean.run.emptyLcnf.0._eval._closed_0 : String :=
       let _x.1 := "f";
       return _x.1
@@ -41,6 +31,16 @@ trace: [Compiler.result] size: 5
       let _x.2 := _eval._closed_2.2;
       let _x.3 := Array.push ◾ _x.2 _x.1;
       return _x.3
+[Compiler.result] size: 5
+    def _private.lean.run.emptyLcnf.0._eval._lam_0 _x.1 _x.2 _y.3 _y.4 _y.5 _y.6 _y.7 _y.8 _y.9 : EST.Out Lean.Exception
+      lcAny PUnit :=
+      let _x.10 := Lean.Compiler.compile _x.1 _y.7 _y.8 _y.9;
+      cases _x.10 : EST.Out Lean.Exception lcAny PUnit
+      | EST.Out.ok a.11 a.12 =>
+        let _x.13 := @EST.Out.ok ◾ ◾ ◾ _x.2 a.12;
+        return _x.13
+      | EST.Out.error a.14 a.15 =>
+        return _x.10
 [Compiler.result] size: 8
     def _private.lean.run.emptyLcnf.0._eval a.1 a.2 a.3 : EST.Out Lean.Exception lcAny PUnit :=
       let _x.4 := _eval._closed_0.2;

tests/lean/run/erased.lean

@@ -25,18 +25,7 @@ trace: [Compiler.result] size: 1
       let _x.1 : PSigma lcErased lcAny := PSigma.mk ◾ ◾ ◾ ◾;
       return _x.1
 ---
-trace: [Compiler.result] size: 5
-    def _private.lean.run.erased.0._eval._lam_0 (_x.1 : Array
-       Lean.Name) (_x.2 : PUnit) (_y.3 : Lean.Elab.Term.Context) (_y.4 : lcAny) (_y.5 : Lean.Meta.Context) (_y.6 : lcAny) (_y.7 : Lean.Core.Context) (_y.8 : lcAny) (_y.9 : lcVoid) : EST.Out
-      Lean.Exception lcAny PUnit :=
-      let _x.10 : EST.Out Lean.Exception lcAny PUnit := compile _x.1 _y.7 _y.8 _y.9;
-      cases _x.10 : EST.Out Lean.Exception lcAny PUnit
-      | EST.Out.ok (a.11 : PUnit) (a.12 : lcVoid) =>
-        let _x.13 : EST.Out Lean.Exception lcAny PUnit := @EST.Out.ok ◾ ◾ ◾ _x.2 a.12;
-        return _x.13
-      | EST.Out.error (a.14 : Lean.Exception) (a.15 : lcVoid) =>
-        return _x.10
-[Compiler.result] size: 1
+trace: [Compiler.result] size: 1
     def _private.lean.run.erased.0._eval._closed_0 : String :=
       let _x.1 : String := "Erased";
       return _x.1
@@ -61,6 +50,17 @@ trace: [Compiler.result] size: 5
       let _x.2 : Array Lean.Name := _eval._closed_3.2;
       let _x.3 : Array Lean.Name := Array.push ◾ _x.2 _x.1;
       return _x.3
+[Compiler.result] size: 5
+    def _private.lean.run.erased.0._eval._lam_0 (_x.1 : Array
+       Lean.Name) (_x.2 : PUnit) (_y.3 : Lean.Elab.Term.Context) (_y.4 : lcAny) (_y.5 : Lean.Meta.Context) (_y.6 : lcAny) (_y.7 : Lean.Core.Context) (_y.8 : lcAny) (_y.9 : lcVoid) : EST.Out
+      Lean.Exception lcAny PUnit :=
+      let _x.10 : EST.Out Lean.Exception lcAny PUnit := compile _x.1 _y.7 _y.8 _y.9;
+      cases _x.10 : EST.Out Lean.Exception lcAny PUnit
+      | EST.Out.ok (a.11 : PUnit) (a.12 : lcVoid) =>
+        let _x.13 : EST.Out Lean.Exception lcAny PUnit := @EST.Out.ok ◾ ◾ ◾ _x.2 a.12;
+        return _x.13
+      | EST.Out.error (a.14 : Lean.Exception) (a.15 : lcVoid) =>
+        return _x.10
 [Compiler.result] size: 9
     def _private.lean.run.erased.0._eval (a.1 : Lean.Elab.Command.Context) (a.2 : lcAny) (a.3 : lcVoid) : EST.Out
       Lean.Exception lcAny PUnit :=