feat: Implement extends flat

This implements leanprover#2666,
allowing manual tweaking of whether structure inheritance is flat or nested,
without forcing the user to fallback to the `FlatHack` approach in https://arxiv.org/abs/2306.00617.

This is documented via a docstring on the `flat` parser,
which appear as a hover docstring as long as `Lean/Parser/Command` is imported.

src/Lean/Elab/Structure.lean

@@ -476,11 +476,16 @@ where
     if h : i < view.parents.size then
       let parentStx := view.parents.get ⟨i, h⟩
       withRef parentStx do
-      let parentType ← Term.elabType parentStx
+      let mut isFlat := !parentStx[0].isNone
+      let parentType ← Term.elabType parentStx[1]
       let parentStructName ← getStructureName parentType
-      if let some existingFieldName ← findExistingField? infos parentStructName then
-        if structureDiamondWarning.get (← getOptions) then
-          logWarning s!"field '{existingFieldName}' from '{parentStructName}' has already been declared"
+      -- If `flat` was not specified but the fields overlap, behave as though it were specified.
+      if not isFlat then
+        if let some existingFieldName ← findExistingField? infos parentStructName then
+          if structureDiamondWarning.get (← getOptions) then
+            logWarning s!"field '{existingFieldName}' from '{parentStructName}' has already been declared"
+          isFlat := true
+      if isFlat then
         copyNewFieldsFrom view.declName infos parentType fun infos => go (i+1) infos (copiedParents.push parentType)
         -- TODO: if `class`, then we need to create a let-decl that stores the local instance for the `parentStructure`
       else

src/Lean/Parser/Command.lean

@@ -197,8 +197,14 @@ def structureTk          := leading_parser
   "structure "
 def classTk              := leading_parser
   "class "
+/-- Within an `extends` clause of a `structure` or `class`,
+the `flat` modifier forced the fields of a parent structure to be flattened into the current structure.
+This happens automatically even without `flat`,
+if fields of the parent structure overlap with any previous fields. -/
+def flatTk               := leading_parser
+  nonReservedSymbol "flat "
 def «extends»            := leading_parser
-  " extends " >> sepBy1 termParser ", "
+  " extends " >> sepBy1 (optional flatTk >> termParser) ", "
 def «structure»          := leading_parser
     (structureTk <|> classTk) >> declId >>
     ppIndent (many (ppSpace >> Term.bracketedBinder) >> optional «extends» >> Term.optType) >>

tests/lean/run/struct_flat.lean

@@ -0,0 +1,24 @@
+structure AddHom (α) [Add α] where
+  toFun : α → α
+  map_add (a b : α) : toFun (a + b) = toFun a + toFun b
+
+structure MulHom (α) [Mul α] where
+  toFun : α → α
+  map_mul (a b : α) : toFun (a * b) = toFun a * toFun b
+
+structure DistribHom (α) [Add α] [Mul α] extends AddHom α, MulHom α
+structure DistribHomFlatAdd (α) [Add α] [Mul α] extends flat AddHom α, MulHom α
+
+#print DistribHom.mk
+#print DistribHomFlatAdd.mk
+
+-- the flat version has less noise when in a goal view
+set_option pp.proofs.withType false
+#check {toFun := id, map_add := fun _ _ => rfl, map_mul := fun _ _ => rfl : DistribHom Nat}
+#check {toFun := id, map_add := fun _ _ => rfl, map_mul := fun _ _ => rfl : DistribHomFlatAdd Nat}
+
+-- marking `MulHom` as flat makes no difference, since `Add` has already been flattened.
+structure DistribHomFlatMul (α) [Add α] [Mul α] extends AddHom α, flat MulHom α
+structure DistribHomFlatBoth (α) [Add α] [Mul α] extends flat AddHom α, flat MulHom α
+#print DistribHomFlatMul.mk
+#print DistribHomFlatBoth.mk