feat: show structure field argument names (#252)

DocGen4/Output/Structure.lean

@@ -1,3 +1,4 @@
+import DocGen4.Output.Arg
 import DocGen4.Output.Template
 import DocGen4.Output.DocString
 import DocGen4.Process
@@ -14,6 +15,7 @@ Render a single field consisting of its documentation, its name and its type as
 def fieldToHtml (f : Process.FieldInfo) : HtmlM Html := do
   let shortName := f.name.componentsRev.head!.toString
   let name := f.name.toString
+  let args ← f.args.mapM argToHtml
   if f.isDirect then
     let doc : Array HTML ←
       if let some doc := f.doc then
@@ -23,13 +25,13 @@ def fieldToHtml (f : Process.FieldInfo) : HtmlM Html := do
         pure #[]
     pure
       <li id={name} class="structure_field">
-        <div class="structure_field_info">{s!"{shortName} "} : [← infoFormatToHtml f.type]</div>
+        <div class="structure_field_info">{shortName} [args] {" : "} [← infoFormatToHtml f.type]</div>
         [doc]
       </li>
   else
     pure
       <li class="structure_field inherited_field">
-        <div class="structure_field_info"><a href={← declNameToLink f.name}>{s!"{shortName}"}</a>{" "}: [← infoFormatToHtml f.type]</div>
+        <div class="structure_field_info"><a href={← declNameToLink f.name}>{shortName}</a> [args] {" : "} [← infoFormatToHtml f.type]</div>
       </li>
 
 /--

DocGen4/Process/Base.lean

@@ -27,15 +27,6 @@ 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
-
 /--
 An argument to a declaration, e.g. the `(x : Nat)` in `def foo (x : Nat) := x`.
 -/
@@ -129,6 +120,15 @@ structure InductiveInfo extends Info where
   isUnsafe : Bool
   deriving Inhabited
 
+/--
+Stores information about a structure field.
+-/
+structure FieldInfo extends Info where
+  /--
+  Whether or not this field is new to this structure, or instead whether it was inherited from a parent.
+  -/
+  isDirect : Bool
+
 /--
 Information about a `structure` parent.
 -/

DocGen4/Process/NameInfo.lean

@@ -46,29 +46,32 @@ private def prettyPrintTermStx (stx : Term) (infos : SubExpr.PosMap Elab.Info) :
   }
   return Widget.tagCodeInfos ctx infos tt
 
-def Info.ofConstantVal (v : ConstantVal) : MetaM Info := do
-  let e := Expr.const v.name (v.levelParams.map mkLevelParam)
+def Info.ofTypedName (n : Name) (t : Expr) : MetaM Info := do
   -- Use the main signature delaborator. We need to run sanitization, parenthesization, and formatting ourselves
   -- to be able to extract the pieces of the signature right before they are formatted
   -- and then format them individually.
-  let (sigStx, infos) ← PrettyPrinter.delabCore e (delab := PrettyPrinter.Delaborator.delabConstWithSignature)
+  let (sigStx, infos) ← PrettyPrinter.delabCore t (delab := PrettyPrinter.Delaborator.delabConstWithSignature.delabParams {} default #[])
   let sigStx := (sanitizeSyntax sigStx).run' { options := (← getOptions) }
   let sigStx ← PrettyPrinter.parenthesize PrettyPrinter.Delaborator.declSigWithId.parenthesizer sigStx
   let `(PrettyPrinter.Delaborator.declSigWithId| $_:term $binders* : $type) := sigStx
-    | throwError "signature pretty printer failure for {v.name}"
+    | throwError "signature pretty printer failure for {n}"
   let args ← binders.mapM fun binder => do
     let fmt ← prettyPrintBinder binder infos
     return Arg.mk fmt (!binder.isOfKind ``Parser.Term.explicitBinder)
   let type ← prettyPrintTermStx type infos
-  match ← findDeclarationRanges? v.name with
+  match ← findDeclarationRanges? n with
   -- TODO: Maybe selection range is more relevant? Figure this out in the future
   | some range =>
     return {
-      toNameInfo := { name := v.name, type, doc := ← findDocString? (← getEnv) v.name},
+      toNameInfo := { name := n, type, doc := ← findDocString? (← getEnv) n},
       args,
       declarationRange := range.range,
-      attrs := ← getAllAttributes v.name
+      attrs := ← getAllAttributes n
     }
-  | none => panic! s!"{v.name} is a declaration without position"
+  | none => panic! s!"{n} is a declaration without position"
+
+def Info.ofConstantVal (v : ConstantVal) : MetaM Info := do
+  let e := Expr.const v.name (v.levelParams.map mkLevelParam)
+  ofTypedName v.name (← inferType e)
 
 end DocGen4.Process

DocGen4/Process/StructureInfo.lean

@@ -54,7 +54,7 @@ def getFieldTypes (v : InductiveVal) : MetaM (Array StructureParentInfo × Array
       parentInfo := parentInfo.push { projFn, type := ← prettyPrintTerm type }
     for (name, type) in fields do
       let (isDirect, projFn) ← getFieldOrigin v.name name
-      fieldInfo := fieldInfo.push { ← NameInfo.ofTypedName projFn type with isDirect }
+      fieldInfo := fieldInfo.push { ← Info.ofTypedName projFn type with isDirect }
     return (parentInfo, fieldInfo)
 
 def StructureInfo.ofInductiveVal (v : InductiveVal) : MetaM StructureInfo := do

static/style.css

@@ -753,7 +753,9 @@ a:hover {
     transition: opacity 300ms ease-in;
 }
 
-.decl_header:not(:hover) .impl_arg, .constructor:not(:hover) .impl_arg {
+.decl_header:not(:hover) .impl_arg,
+        .constructor:not(:hover) .impl_arg,
+        .structure_field_info:not(:hover) .impl_arg {
     opacity: 30%;
     transition: opacity 1000ms ease-out;
 }