feat: improvements to structure output (#232)

- Now the precise list of parent structures is shown, now that Lean records this information. Closes #223
- Fixes an issue where fields of a structure wouldn't be shown. Closes #229
- Grays out inherited fields and gives them a link to their definitions.
- Fixes an issue where inherited fields would have an id attribute with a synthetic name, which could cause links to go to the wrong place. Now inherited fields don't have an id attribute.

DocGen4/Output/Structure.lean

@@ -11,20 +11,25 @@ open Lean
 /--
 Render a single field consisting of its documentation, its name and its type as HTML.
 -/
-def fieldToHtml (f : Process.NameInfo) : HtmlM Html := do
+def fieldToHtml (f : Process.FieldInfo) : HtmlM Html := do
   let shortName := f.name.componentsRev.head!.toString
   let name := f.name.toString
-  if let some doc := f.doc then
-    let renderedDoc ← docStringToHtml doc name
+  if f.isDirect then
+    let doc : Array HTML ←
+      if let some doc := f.doc then
+        let renderedDoc ← docStringToHtml doc name
+        pure #[<div class="structure_field_doc">[renderedDoc]</div>]
+      else
+        pure #[]
     pure
       <li id={name} class="structure_field">
         <div class="structure_field_info">{s!"{shortName} "} : [← infoFormatToHtml f.type]</div>
-        <div class="structure_field_doc">[renderedDoc]</div>
+        [doc]
       </li>
   else
     pure
-      <li id={name} class="structure_field">
-        <div class="structure_field_info">{s!"{shortName} "} : [← infoFormatToHtml f.type]</div>
+      <li class="structure_field inherited_field">
+        <div class="structure_field_info"><a href={s!"#{name}"}>{s!"{shortName}"}</a>{" "}: [← infoFormatToHtml f.type]</div>
       </li>
 
 /--

DocGen4/Process/Base.lean

@@ -27,6 +27,8 @@ structure NameInfo where
   doc : Option String
   deriving Inhabited
 
+structure FieldInfo extends NameInfo where
+  isDirect : Bool
 
 /--
 An argument to a declaration, e.g. the `(x : Nat)` in `def foo (x : Nat) := x`.
@@ -127,7 +129,7 @@ structure StructureInfo extends Info where
   /--
   Information about all the fields of the structure.
   -/
-  fieldInfo : Array NameInfo
+  fieldInfo : Array FieldInfo
   /--
   All the structures this one inherited from.
   -/

DocGen4/Process/DocInfo.lean

@@ -130,20 +130,14 @@ def isBlackListed (declName : Name) : MetaM Bool := do
   -- TODO: Evaluate whether filtering out declarations without range is sensible
   | none => return true
 
--- TODO: Is this actually the best way?
+/-- Returns `true` if `declName` is a field projection or a parent projection for a structure. -/
 def isProjFn (declName : Name) : MetaM Bool := do
   let env ← getEnv
   match declName with
   | Name.str parent name =>
-    if isStructure env parent then
-      match getStructureInfo? env parent with
-      | some i =>
-        match i.fieldNames.find? (·.toString == name) with
-        | some _ => return true
-        | none => return false
-      | none => panic! s!"{parent} is not a structure"
-    else
-      return false
+    let some si := getStructureInfo? env parent | return false
+    return getProjFnForField? env parent (Name.mkSimple name) == declName
+      || (si.parentInfo.any fun pi => pi.projFn == declName)
   | _ => return false
 
 def ofConstant : (Name × ConstantInfo) → MetaM (Option DocInfo) := fun (name, info) => do

DocGen4/Process/StructureInfo.lean

@@ -16,43 +16,38 @@ open Lean Meta
   Execute `k` with 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 α) (includeSubobjectFields : Bool := false) : MetaM α := do
+def withFields (info : InductiveVal) (k : 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 := #[]
-    for fieldName in getStructureFieldsFlattened (← getEnv) structName includeSubobjectFields do
+    for fieldName in getStructureFieldsFlattened (← getEnv) structName (includeSubobjectFields := false) do
       let proj ← mkProjection s fieldName
       info := info.push (fieldName, (← inferType proj))
     k info
 
-def getFieldTypes (v : InductiveVal) : MetaM (Array NameInfo) := do
+def getFieldTypes (parents : Array Name) (v : InductiveVal) : MetaM (Array FieldInfo) := do
+  let env ← getEnv
   withFields v fun fields =>
-    fields.foldlM (init := #[]) (fun acc (name, type) => do return acc.push (← NameInfo.ofTypedName (v.name.append name) type))
+    fields.foldlM (init := #[]) (fun acc (name, type) => 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 some fi := getFieldInfo? env structForField name | unreachable!
+      return acc.push { ← NameInfo.ofTypedName fi.projFn type with isDirect })
 
 def StructureInfo.ofInductiveVal (v : InductiveVal) : MetaM StructureInfo := do
   let info ← Info.ofConstantVal v.toConstantVal
   let env ← getEnv
-  let parents ← getAllParentStructures v.name
+  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
-  match getStructureInfo? env v.name with
-  | some i =>
-    if i.fieldNames.size - parents.size > 0 then
-      return {
-        toInfo := info,
-        fieldInfo := ← getFieldTypes v,
-        parents,
-        ctor
-      }
-    else
-      return {
-        toInfo := info,
-        fieldInfo := #[],
-        parents,
-        ctor
-      }
-  | none => panic! s!"{v.name} is not a structure"
+  return {
+    toInfo := info,
+    fieldInfo := ← getFieldTypes parents v,
+    parents,
+    ctor
+  }
 
 end DocGen4.Process

static/style.css

@@ -757,6 +757,15 @@ a:hover {
     transition: opacity 1000ms ease-out;
 }
 
+.inherited_field {
+    transition: opacity 300ms ease-in;
+}
+
+.structure_fields:not(:hover) .inherited_field {
+    opacity: 30%;
+    transition: opacity 1000ms ease-out;
+}
+
 .gh_link {
     float: right;
     margin-left: 10px;