refactor: add a CtorFieldInfo.object field for the object type (#9390)

src/Lean/Compiler/IR/ToIR.lean

@@ -90,7 +90,7 @@ inductive TranslatedProj where
 def lowerProj (base : VarId) (ctorInfo : CtorInfo) (field : CtorFieldInfo)
     : TranslatedProj × IRType :=
   match field with
-  | .object i => ⟨.expr (.proj i base), .object⟩
+  | .object i irType => ⟨.expr (.proj i base), irType⟩
   | .usize i => ⟨.expr (.uproj i base), .usize⟩
   | .scalar _ offset irType => ⟨.expr (.sproj (ctorInfo.size + ctorInfo.usize) offset base), irType⟩
   | .erased => ⟨.erased, .erased⟩

src/Lean/Compiler/IR/ToIRType.lean

@@ -78,7 +78,7 @@ def toIRType (type : Lean.Expr) : CoreM IRType := do
 
 inductive CtorFieldInfo where
   | erased
-  | object (i : Nat)
+  | object (i : Nat) (type : IRType)
   | usize  (i : Nat)
   | scalar (sz : Nat) (offset : Nat) (type : IRType)
   deriving Inhabited
@@ -87,7 +87,7 @@ namespace CtorFieldInfo
 
 def format : CtorFieldInfo → Format
   | erased => "◾"
-  | object i   => f!"obj@{i}"
+  | object i type => f!"obj@{i}:{type}"
   | usize i    => f!"usize@{i}"
   | scalar sz offset type => f!"scalar#{sz}@{offset}:{type}"
 
@@ -123,11 +123,12 @@ where fillCache := do
       let fieldType ← field.fvarId!.getType
       let lcnfFieldType ← LCNF.toLCNFType fieldType
       let monoFieldType ← LCNF.toMonoType lcnfFieldType
-      let ctorField ← match (← toIRType monoFieldType) with
+      let irFieldType ← toIRType monoFieldType
+      let ctorField ← match irFieldType with
       | .object | .tobject => do
         let i := nextIdx
         nextIdx := nextIdx + 1
-        pure <| .object i
+        pure <| .object i irFieldType
       | .usize => pure <| .usize 0
       | .erased => .pure <| .erased
       | .uint8 =>
@@ -156,7 +157,7 @@ where fillCache := do
       | .usize _ => do
         let i ← modifyGet fun nextIdx => (nextIdx, nextIdx + 1)
         return .usize i
-      | .object _ | .scalar .. | .erased => return field
+      | .object .. | .scalar .. | .erased => return field
     let numUSize := nextIdx - numObjs
     let adjustScalarsForSize (fields : Array CtorFieldInfo) (size : Nat) (nextOffset : Nat)
         : Array CtorFieldInfo × Nat :=
@@ -168,7 +169,7 @@ where fillCache := do
             return .scalar sz offset type
           else
             return field
-        | .object _ | .usize _ | .erased => return field
+        | .object .. | .usize _ | .erased => return field
     let mut nextOffset := 0
     if has8BScalar then
       ⟨fields, nextOffset⟩ := adjustScalarsForSize fields 8 nextOffset

tests/lean/ctor_layout.lean.expected.out

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