feat: update fieldMap with composite field

src/Lean/Elab/Structure.lean

@@ -396,8 +396,9 @@ where
             let fieldParentStructName ← getStructureName fieldType
             if (← findExistingField? infos fieldParentStructName).isSome then
               copyFields infos fieldType fun nestedFieldMap infos => do
-                -- TODO: update fieldMap
-                copy (i+1) fieldMap infos
+                let fieldVal ← mkCompositeField fieldType nestedFieldMap
+                trace[Meta.debug] "composite, {fieldName} := {fieldVal}"
+                copy (i+1) (fieldMap.insert fieldName fieldVal) infos
             else
               addNewField
           else
@@ -413,6 +414,17 @@ where
       | some value => return { info with value? := value }
       | none       => return info
 
+  mkCompositeField (parentType : Expr) (fieldMap : FieldMap) : TermElabM Expr := do
+    let env ← getEnv
+    let Expr.const parentStructName us _ ← pure parentType.getAppFn | unreachable!
+    let parentCtor := getStructureCtor env parentStructName
+    let mut result := mkAppN (mkConst parentCtor.name us) parentType.getAppArgs
+    for fieldName in getStructureFields env parentStructName do
+      match fieldMap.find? fieldName with
+      | some val => result := mkApp result val
+      | none => throwError "failed to copied fields from parent structure{indentExpr parentType}" -- TODO improve error message
+    return result
+
 private def mkToParentName (parentStructName : Name) : Name :=
   Name.mkSimple $ "to" ++ parentStructName.eraseMacroScopes.getString! -- erase macro scopes?
 

tests/lean/run/diamond3.lean

@@ -39,3 +39,20 @@ def f'' (a b d e : Nat) : D'' :=
 
 theorem ex3 (a b d e: Nat) : (f'' a b d e |>.c) = a :=
   rfl
+
+structure B1 where
+  a : Nat
+  b : Nat
+
+structure C1 extends B1 where
+  d : Nat
+  e : Nat
+  c : Nat := b + e
+
+structure D1 extends A, C1
+
+def f1 (a b d e : Nat) : D1 :=
+  { a, b, d, e }
+
+theorem ex4 (a b d e: Nat) : (f1 a b d e |>.c) = b + e :=
+  rfl