feat: record all structure parents in StructureInfo

Followup to #5841. Makes the `structure` command populate the new `parentInfo` field.

This will require a stage0 update to fully take effect.

Breaking change: now `getParentStructures` is `getStructureSubobjects`. Adds `getStructureParentInfo` for getting all the immediate parents. Note that the set of subobjects is neither a subset nor a superset of the immediate parents.

Closes #1881

src/Lean/Elab/App.lean

@@ -1150,7 +1150,7 @@ private partial def findMethod? (env : Environment) (structName fieldName : Name
     | some _ => some (structName, fullNamePrv)
     | none   =>
       if isStructure env structName then
-        (getParentStructures env structName).findSome? fun parentStructName => findMethod? env parentStructName fieldName
+        (getStructureSubobjects env structName).findSome? fun parentStructName => findMethod? env parentStructName fieldName
       else
         none
 

src/Lean/Elab/Structure.lean

@@ -46,10 +46,12 @@ structure StructFieldView where
   modifiers  : Modifiers
   binderInfo : BinderInfo
   declName   : Name
-  /-- ref for the field name -/
+  /-- Ref for the field name -/
   nameId     : Syntax
-  name       : Name -- The field name as it is going to be registered in the kernel. It does not include macroscopes.
-  rawName    : Name -- Same as `name` but including macroscopes.
+  /-- The name of the field. (Without macro scopes.) -/
+  name       : Name
+  /-- Same as `name` but includes macro scopes. Used for field elaboration. -/
+  rawName    : Name
   binders    : Syntax
   type?      : Option Syntax
   value?     : Option Syntax
@@ -79,13 +81,17 @@ structure StructParentInfo where
   deriving Inhabited
 
 inductive StructFieldKind where
-  | newField | copiedField | fromParent | subobject
+  | newField | copiedField | fromParent
+  /-- The field is an embedded parent. -/
+  | subobject (structName : Name)
   deriving Inhabited, DecidableEq, Repr
 
 structure StructFieldInfo where
   ref      : Syntax
   name     : Name
-  declName : Name -- Remark: for `fromParent` fields, `declName` is only relevant in the generation of auxiliary "default value" functions.
+  /-- Name of projection function.
+  Remark: for `fromParent` fields, `declName` is only relevant in the generation of auxiliary "default value" functions. -/
+  declName : Name
   fvar     : Expr
   kind     : StructFieldKind
   value?   : Option Expr := none
@@ -99,6 +105,7 @@ structure ElabStructHeaderResult where
   params           : Array Expr
   type             : Expr
   parents          : Array StructParentInfo
+  /-- Field infos from parents. -/
   parentFieldInfos : Array StructFieldInfo
   deriving Inhabited
 
@@ -108,9 +115,7 @@ def StructFieldInfo.isFromParent (info : StructFieldInfo) : Bool :=
   | _                          => false
 
 def StructFieldInfo.isSubobject (info : StructFieldInfo) : Bool :=
-  match info.kind with
-  | StructFieldKind.subobject => true
-  | _                         => false
+  info.kind matches StructFieldKind.subobject ..
 
 private def defaultCtorName := `mk
 
@@ -475,7 +480,7 @@ where
                                         name := fieldName, declName := fieldDeclName, fvar := fieldFVar, value?,
                                         kind := StructFieldKind.copiedField }
               copy (i+1) infos fieldMap expandedStructNames
-          if fieldInfo.subobject?.isSome then
+          if let some parentParentStructName := fieldInfo.subobject? then
             let fieldParentStructName ← getStructureName fieldType
             if (← findExistingField? infos fieldParentStructName).isSome then
               -- See comment at `copyDefaultValue?`
@@ -489,7 +494,7 @@ where
               withLocalDecl fieldName fieldInfo.binderInfo fieldType fun parentFVar => do
                 let infos := infos.push { ref := (← getRef)
                                           name := fieldName, declName := structDeclName ++ fieldName, fvar := parentFVar,
-                                          kind := StructFieldKind.subobject }
+                                          kind := StructFieldKind.subobject parentParentStructName }
                 processSubfields structDeclName parentFVar fieldParentStructName subfieldNames infos fun infos =>
                   copy (i+1) infos (fieldMap.insert fieldName parentFVar) expandedStructNames
           else
@@ -537,6 +542,8 @@ where
       let type ← Term.elabType parent
       let parentType ← whnf type
       let parentStructName ← getStructureName parentType
+      if parents.any (fun info => info.structName == parentStructName) then
+        logWarningAt parent m!"duplicate parent structure '{parentStructName}'"
       if let some existingFieldName ← findExistingField? infos parentStructName then
         if structureDiamondWarning.get (← getOptions) then
           logWarning s!"field '{existingFieldName}' from '{parentStructName}' has already been declared"
@@ -551,7 +558,7 @@ where
         withLocalDecl toParentName binfo parentType fun parentFVar =>
           let infos := infos.push { ref := parent,
                                     name := toParentName, declName := view.declName ++ toParentName, fvar := parentFVar,
-                                    kind := StructFieldKind.subobject }
+                                    kind := StructFieldKind.subobject parentStructName }
           let parents := parents.push { ref := parent, fvar? := parentFVar, subobject := true, structName := parentStructName, type := parentType }
           processSubfields view.declName parentFVar parentStructName subfieldNames infos fun infos => go (i+1) infos parents
     else
@@ -631,7 +638,7 @@ where
               go (i+1) defaultValsOverridden infos
         match info.kind with
         | StructFieldKind.newField    => throwError "field '{view.name}' has already been declared"
-        | StructFieldKind.subobject   => throwError "unexpected subobject field reference" -- improve error message
+        | StructFieldKind.subobject n => throwError "unexpected reference to subobject field '{n}'" -- improve error message
         | StructFieldKind.copiedField => updateDefaultValue
         | StructFieldKind.fromParent  => updateDefaultValue
     else
@@ -773,34 +780,24 @@ private opaque mkProjections (env : Environment) (structName : Name) (projs : Li
 
 private def addProjections (r : ElabStructHeaderResult) (fieldInfos : Array StructFieldInfo) : TermElabM Unit := do
   if r.type.isProp then
-    if let some fieldInfo ← fieldInfos.findM? fun fieldInfo => not <$> Meta.isProof fieldInfo.fvar then
+    if let some fieldInfo ← fieldInfos.findM? (not <$> Meta.isProof ·.fvar) then
       throwErrorAt fieldInfo.ref m!"failed to generate projections for 'Prop' structure, field '{format fieldInfo.name}' is not a proof"
-  let projNames := (fieldInfos.filter fun (info : StructFieldInfo) => !info.isFromParent).toList.map fun (info : StructFieldInfo) => info.declName
+  let projNames := fieldInfos |>.filter (!·.isFromParent) |>.map (·.declName)
   let env ← getEnv
-  let env ← ofExceptKernelException (mkProjections env r.view.declName projNames r.view.isClass)
+  let env ← ofExceptKernelException (mkProjections env r.view.declName projNames.toList r.view.isClass)
   setEnv env
 
 private def registerStructure (structName : Name) (infos : Array StructFieldInfo) : TermElabM Unit := do
   let fields ← infos.filterMapM fun info => do
       if info.kind == StructFieldKind.fromParent then
         return none
       else
-        let env ← getEnv
         return some {
           fieldName  := info.name
           projFn     := info.declName
           binderInfo := (← getFVarLocalDecl info.fvar).binderInfo
           autoParam? := (← inferType info.fvar).getAutoParamTactic?
-          subobject? :=
-            if info.kind == StructFieldKind.subobject then
-              match env.find? info.declName with
-              | some info =>
-                match info.type.getForallBody.getAppFn with
-                | Expr.const parentName .. => some parentName
-                | _ => panic! "ill-formed structure"
-              | _ => panic! "ill-formed environment"
-            else
-              none
+          subobject? := if let .subobject parentName := info.kind then parentName else none
         }
   modifyEnv fun env => Lean.registerStructure env { structName, fields }
 
@@ -841,7 +838,10 @@ private def setSourceInstImplicit (type : Expr) : Expr :=
       type.updateForall! .instImplicit d b
   | _ => unreachable!
 
-private partial def mkCoercionToCopiedParent (levelParams : List Name) (params : Array Expr) (view : StructView) (parentStructName : Name) (parentType : Expr) : MetaM Unit := do
+/--
+Creates a projection function to a non-subobject parent.
+-/
+private partial def mkCoercionToCopiedParent (levelParams : List Name) (params : Array Expr) (view : StructView) (parentStructName : Name) (parentType : Expr) : MetaM StructureParentInfo := do
   let env ← getEnv
   let structName := view.declName
   let sourceFieldNames := getStructureFieldsFlattened env structName
@@ -883,6 +883,7 @@ private partial def mkCoercionToCopiedParent (levelParams : List Name) (params :
       addInstance declName AttributeKind.global (eval_prio default)
     else
       setReducibleAttribute declName
+    return { structName := parentStructName, subobject := false, projFn := declName }
 
 private def elabStructHeader (view : StructView) : TermElabM ElabStructHeaderResult :=
   Term.withAutoBoundImplicitForbiddenPred (fun n => view.shortDeclName == n) do
@@ -995,9 +996,13 @@ def mkStructureDecl (vars : Array Expr) (view : StructView) : TermElabM Unit :=
             Term.applyAttributesAt view.declName view.modifiers.attrs AttributeApplicationTime.afterTypeChecking
           let projInstances := instParents.toList.map fun info => info.declName
           projInstances.forM fun declName => addInstance declName AttributeKind.global (eval_prio default)
-          r.parents.forM fun parent => do
-            if !parent.subobject then
+          let parentInfos ← r.parents.mapM fun parent => do
+            if parent.subobject then
+              let some info := fieldInfos.find? (·.kind == .subobject parent.structName) | unreachable!
+              pure { structName := parent.structName, subobject := true, projFn := info.declName }
+            else
               mkCoercionToCopiedParent levelParams params view parent.structName parent.type
+          setStructureParents view.declName parentInfos
           let lctx ← getLCtx
           /- The `lctx` and `defaultAuxDecls` are used to create the auxiliary "default value" declarations
             The parameters `params` for these definitions must be marked as implicit, and all others as explicit. -/

src/Lean/Structure.lean

@@ -61,8 +61,8 @@ structure StructureInfo where
   fieldNames  : Array Name := #[]
   /-- Information about the structure fields, sorted by `fieldName`. -/
   fieldInfo   : Array StructureFieldInfo := #[]
-  /-- (Unimplemented) Information about structure parents. These are in the order they appear in the `extends` clause. -/
-  private parentInfo  : Array StructureParentInfo := #[]
+  /-- Information about structure parents. These are in the order they appear in the `extends` clause. -/
+  parentInfo  : Array StructureParentInfo := #[]
   deriving Inhabited
 
 def StructureInfo.lt (i₁ i₂ : StructureInfo) : Bool :=
@@ -117,11 +117,22 @@ def setStructureParents [Monad m] [MonadEnv m] [MonadError m] (structName : Name
     | throwError "cannot set structure parents for '{structName}', structure not defined in current module"
   modifyEnv fun env => structureExt.addEntry env { info with parentInfo }
 
+/-- Gets the `StructureInfo` if `structName` has been declared as a structure to the elaborator. -/
 def getStructureInfo? (env : Environment) (structName : Name) : Option StructureInfo :=
   match env.getModuleIdxFor? structName with
   | some modIdx => structureExt.getModuleEntries env modIdx |>.binSearch { structName } StructureInfo.lt
   | none        => structureExt.getState env |>.map.find? structName
 
+/--
+Gets the `StructureInfo` for `structName`, which is assumed to have been declared as a structure to the elaborator.
+Panics on failure.
+-/
+def getStructureInfo (env : Environment) (structName : Name) : StructureInfo :=
+  if let some info := getStructureInfo? env structName then
+    info
+  else
+    panic! "structure expected"
+
 def getStructureCtor (env : Environment) (constName : Name) : ConstructorVal :=
   match env.find? constName with
   | some (.inductInfo { isRec := false, ctors := [ctorName], .. }) =>
@@ -130,49 +141,61 @@ def getStructureCtor (env : Environment) (constName : Name) : ConstructorVal :=
     | _ => panic! "ill-formed environment"
   | _ => panic! "structure expected"
 
-/-- Get direct field names for the given structure. -/
+/-- Gets the direct field names for the given structure, including subobject fields. -/
 def getStructureFields (env : Environment) (structName : Name) : Array Name :=
-  if let some info := getStructureInfo? env structName then
-    info.fieldNames
-  else
-    panic! "structure expected"
+  (getStructureInfo env structName).fieldNames
 
 def getFieldInfo? (env : Environment) (structName : Name) (fieldName : Name) : Option StructureFieldInfo :=
   if let some info := getStructureInfo? env structName then
     info.fieldInfo.binSearch { fieldName := fieldName, projFn := default, subobject? := none, binderInfo := default } StructureFieldInfo.lt
   else
     none
 
-/-- If `fieldName` represents the relation to a parent structure `S`, return `S` -/
+/-- If `fieldName` is a subobject (that it, if it is an embedded parent structure), then returns the name of that parent structure. -/
 def isSubobjectField? (env : Environment) (structName : Name) (fieldName : Name) : Option Name :=
   if let some fieldInfo := getFieldInfo? env structName fieldName then
     fieldInfo.subobject?
   else
     none
 
-/-- Return immediate parent structures -/
-def getParentStructures (env : Environment) (structName : Name) : Array Name :=
+/-- Get information for all the parents that appear in the `extends` clause. -/
+def getStructureParentInfo (env : Environment) (structName : Name) : Array StructureParentInfo :=
+  (getStructureInfo env structName).parentInfo
+
+/--
+Return the parent structures that are embedded in the structure.
+This is the array of all results from `Lean.isSubobjectField?` in order.
+
+Note: this is *not* a subset of the parents from `getStructureParentInfo`.
+If a direct parent cannot itself be represented as a subobject,
+sometimes one of its parents (or one of their parents, etc.) can.
+-/
+def getStructureSubobjects (env : Environment) (structName : Name) : Array Name :=
   let fieldNames := getStructureFields env structName;
   fieldNames.foldl (init := #[]) fun acc fieldName =>
       match isSubobjectField? env structName fieldName with
       | some parentStructName => acc.push parentStructName
       | none                  => acc
 
+-- TODO: use actual parents, not just subobjects.
 /-- Return all parent structures -/
 partial def getAllParentStructures (env : Environment) (structName : Name) : Array Name :=
   visit structName |>.run #[] |>.2
 where
   visit (structName : Name) : StateT (Array Name) Id Unit := do
-    for p in getParentStructures env structName do
+    for p in getStructureSubobjects env structName do
       modify fun s => s.push p
       visit p
 
-/-- `findField? env S fname`. If `fname` is defined in a parent `S'` of `S`, return `S'` -/
+/--
+Return the name of the structure that contains the field relative to structure `structName`.
+If `structName` contains the field itself, returns that,
+and otherwise recursively looks into parents that are subobjects. -/
 partial def findField? (env : Environment) (structName : Name) (fieldName : Name) : Option Name :=
   if (getStructureFields env structName).contains fieldName then
     some structName
   else
-    getParentStructures env structName |>.findSome? fun parentStructName => findField? env parentStructName fieldName
+    getStructureSubobjects env structName |>.findSome? fun parentStructName => findField? env parentStructName fieldName
 
 private partial def getStructureFieldsFlattenedAux (env : Environment) (structName : Name) (fullNames : Array Name) (includeSubobjectFields : Bool) : Array Name :=
   (getStructureFields env structName).foldl (init := fullNames) fun fullNames fieldName =>
@@ -182,24 +205,28 @@ private partial def getStructureFieldsFlattenedAux (env : Environment) (structNa
       getStructureFieldsFlattenedAux env parentStructName fullNames includeSubobjectFields
     | none                  => fullNames.push fieldName
 
-/-- Return field names for the given structure, including "flattened" fields from parent
-structures. To omit `toParent` projections, set `includeSubobjectFields := false`.
+/--
+Returns the full set of field names for the given structure,
+"flattening" all the parent structures that are subobject fields.
+If `includeSubobjectFields` is true, then subobject `toParent` projections are included,
+and otherwise they are omitted.
 
 For example, given `Bar` such that
 ```lean
 structure Foo where a : Nat
 structure Bar extends Foo where b : Nat
 ```
-return `#[toFoo,a,b]` or `#[a,b]` with subobject fields omitted. -/
+this returns ``#[`toFoo, `a, `b]``, or ``#[`a, `b]`` when `includeSubobjectFields := false`.
+-/
 def getStructureFieldsFlattened (env : Environment) (structName : Name) (includeSubobjectFields := true) : Array Name :=
   getStructureFieldsFlattenedAux env structName #[] includeSubobjectFields
 
 /--
-  Return true if `constName` is the name of an inductive datatype
-  created using the `structure` or `class` commands.
+Return true if `constName` is the name of an inductive datatype
+created using the `structure` or `class` commands.
 
-  We perform the check by testing whether auxiliary projection functions
-  have been created. -/
+See also `Lean.getStructureInfo?`.
+-/
 def isStructure (env : Environment) (constName : Name) : Bool :=
   getStructureInfo? env constName |>.isSome
 
@@ -215,6 +242,7 @@ def getProjFnInfoForField? (env : Environment) (structName : Name) (fieldName :
   else
     none
 
+/-- Get the name of the auxiliary definition that would have the default value for the structure field. -/
 def mkDefaultFnOfProjFn (projFn : Name) : Name :=
   projFn ++ `_default