fix: expose getCtorLayout from Lean to unbreak test

Author: nomeata

src/Lean/Compiler/IR/CtorLayout.lean

@@ -35,8 +35,15 @@ structure CtorLayout where
   numUSize   : Nat
   scalarSize : Nat
 
-@[extern "lean_ir_get_ctor_layout"]
 opaque getCtorLayout (env : @& Environment) (ctorName : @& Name) : Except String CtorLayout
 
 end IR
+
+-- Expose `getCtorLayout` in the `Lean` namespace to make it available for the benefit of
+-- the test `lean/ctor_layout.lean`
+-- Can be removed once we no longer have to limit the number of exported symbols and
+-- can use `Lean.IR` from the interpreter.
+@[extern "lean_ir_get_ctor_layout"]
+def getCtorLayout := IR.getCtorLayout
+
 end Lean

tests/lean/ctor_layout.lean

@@ -0,0 +1,17 @@
+import Lean.Compiler.IR
+
+open Lean
+
+unsafe def main : IO Unit :=
+withImportModules #[{module := `Lean.Compiler.IR.Basic}] {} 0 fun env => do
+   let ctorLayout ← IO.ofExcept $ getCtorLayout env `Lean.IR.Expr.reuse;
+   ctorLayout.fieldInfo.forM $ fun finfo => IO.println (format finfo);
+   IO.println "---";
+   let ctorLayout ← IO.ofExcept $ getCtorLayout env `Lean.EnvironmentHeader.mk;
+   ctorLayout.fieldInfo.forM $ fun finfo => IO.println (format finfo);
+   IO.println "---";
+   let ctorLayout ← IO.ofExcept $ getCtorLayout env `Subtype.mk;
+   ctorLayout.fieldInfo.forM $ fun finfo => IO.println (format finfo);
+   pure ()
+
+#eval main

tests/lean/ctor_layout.lean.expected.out

@@ -0,0 +1,15 @@
+obj@0
+obj@1
+scalar#1@0:u8
+obj@2
+---
+scalar#4@0:u32
+scalar#1@4:u8
+obj@0
+obj@1
+obj@2
+obj@3
+obj@4
+---
+obj@0
+◾