feat: show parents' parameters for structures (#234)

Pretty prints parents in the `extends` clause to include parameters.

Fixes a whitespace bug for the `extends` list. Now it's `extends A, B, C` instead of `extends A , B , C`. Also fixes a bug introduced in #232 where the links to inherited fields were incorrect.

DocGen4/Output/Module.lean

@@ -41,13 +41,12 @@ def structureInfoHeader (s : Process.StructureInfo) : HtmlM (Array Html) := do
   let mut nodes := #[]
   if s.parents.size > 0 then
     nodes := nodes.push <span class="decl_extends">extends</span>
-    let mut parents := #[]
-    for parent in s.parents do
-      let link ← declNameToHtmlBreakWithinLink parent
-      let inner := <span class="fn">{link}</span>
-      let html:= Html.element "span" false #[("class", "decl_parent")] #[inner]
-      parents := parents.push html
-    nodes := nodes.append (parents.toList.intersperse (Html.text ", ")).toArray
+    let mut parents := #[Html.text " "]
+    for parent in s.parents, i in [0:s.parents.size] do
+      if i > 0 then
+        parents := parents.push (Html.text ", ")
+      parents := parents ++ (← infoFormatToHtml parent.type)
+    nodes := nodes ++ parents
   return nodes
 
 /--

DocGen4/Output/Structure.lean

@@ -29,7 +29,7 @@ def fieldToHtml (f : Process.FieldInfo) : HtmlM Html := do
   else
     pure
       <li class="structure_field inherited_field">
-        <div class="structure_field_info"><a href={s!"#{name}"}>{s!"{shortName}"}</a>{" "}: [← infoFormatToHtml f.type]</div>
+        <div class="structure_field_info"><a href={← declNameToLink f.name}>{s!"{shortName}"}</a>{" "}: [← infoFormatToHtml f.type]</div>
       </li>
 
 /--

DocGen4/Process/Base.lean

@@ -16,7 +16,7 @@ structure NameInfo where
   /--
   The name that has this info attached.
   -/
-  name  : Name
+  name : Name
   /--
   The pretty printed type of this name.
   -/
@@ -27,7 +27,13 @@ structure NameInfo where
   doc : Option String
   deriving Inhabited
 
+/--
+Stores information about a structure field.
+-/
 structure FieldInfo extends NameInfo where
+  /--
+  Whether or not this field is new to this structure, or instead whether it was inherited from a parent.
+  -/
   isDirect : Bool
 
 /--
@@ -122,6 +128,15 @@ structure InductiveInfo extends Info where
   isUnsafe : Bool
   deriving Inhabited
 
+/--
+Information about a `structure` parent.
+-/
+structure StructureParentInfo where
+  /-- Name of the projection function. -/
+  projFn : Name
+  /-- Pretty printed type. -/
+  type : CodeWithInfos
+
 /--
 Information about a `structure` declaration.
 -/
@@ -133,7 +148,7 @@ structure StructureInfo extends Info where
   /--
   All the structures this one inherited from.
   -/
-  parents : Array Name
+  parents : Array StructureParentInfo
   /--
   The constructor of the structure.
   -/

DocGen4/Process/StructureInfo.lean

@@ -13,39 +13,49 @@ namespace DocGen4.Process
 open Lean Meta
 
 /--
-  Execute `k` with an array containing pairs `(fieldName, fieldType)`.
+  Execute `k` with an array containing pairs `(parentName, projFn, parentType)`
+  and an array containing pairs `(fieldName, fieldType)`.
   `k` is executed in an updated local context which contains local declarations for the `structName` parameters.
 -/
-def withFields (info : InductiveVal) (k : Array (Name × Expr) → MetaM α) : MetaM α := do
+def withFields (info : InductiveVal) (k : Array (Name × Name × Expr) → Array (Name × Expr) → MetaM α) : MetaM α := do
   let structName := info.name
   let us := info.levelParams.map mkLevelParam
   forallTelescopeReducing info.type fun params _ =>
   withLocalDeclD `self (mkAppN (mkConst structName us) params) fun s => do
-    let mut info := #[]
+    let mut parents := #[]
+    for parent in getStructureParentInfo (← getEnv) structName do
+      let proj := mkApp (mkAppN (mkConst parent.projFn us) params) s
+      parents := parents.push (parent.structName, parent.projFn, ← inferType proj)
+    let mut fields := #[]
     for fieldName in getStructureFieldsFlattened (← getEnv) structName (includeSubobjectFields := false) do
       let proj ← mkProjection s fieldName
-      info := info.push (fieldName, (← inferType proj))
-    k info
+      fields := fields.push (fieldName, (← inferType proj))
+    k parents fields
 
-def getFieldTypes (parents : Array Name) (v : InductiveVal) : MetaM (Array FieldInfo) := do
+def getFieldTypes (v : InductiveVal) : MetaM (Array StructureParentInfo × Array FieldInfo) := do
   let env ← getEnv
-  withFields v fun fields =>
-    fields.foldlM (init := #[]) (fun acc (name, type) => do
+  withFields v fun parents fields => do
+    let mut parentInfo : Array StructureParentInfo := #[]
+    let mut fieldInfo : Array FieldInfo := #[]
+    for (_, projFn, type) in parents do
+      parentInfo := parentInfo.push { projFn, type := ← prettyPrintTerm type }
+    for (name, type) in fields do
       let some structForField := findField? env v.name name | unreachable!
       -- We can't simply do `structForField == v.name` since the field might be from a parent that overlapped with another.
-      let isDirect := structForField == v.name && !parents.any fun parent => (getFieldInfo? env parent name).isSome
+      let isDirect := structForField == v.name && !parents.any fun (parent, _) => (getFieldInfo? env parent name).isSome
       let some fi := getFieldInfo? env structForField name | unreachable!
-      return acc.push { ← NameInfo.ofTypedName fi.projFn type with isDirect })
+      fieldInfo := fieldInfo.push { ← NameInfo.ofTypedName fi.projFn type with isDirect }
+    return (parentInfo, fieldInfo)
 
 def StructureInfo.ofInductiveVal (v : InductiveVal) : MetaM StructureInfo := do
   let info ← Info.ofConstantVal v.toConstantVal
   let env ← getEnv
-  let parents := (getStructureParentInfo env v.name).map fun parent => parent.structName
   let ctorVal := getStructureCtor env v.name
   let ctor ← NameInfo.ofTypedName ctorVal.name ctorVal.type
+  let (parents, fieldInfo) ← getFieldTypes v
   return {
     toInfo := info,
-    fieldInfo := ← getFieldTypes parents v,
+    fieldInfo,
     parents,
     ctor
   }