feat: Show arguments of types of decls separately

DocGen4/Output/Module.lean

@@ -49,6 +49,24 @@ partial def infoFormatToHtml (i : CodeWithInfos) : HtmlM (Array Html) := do
          #[Html.element "span" true #[("class", "fn")] (←infoFormatToHtml t)]
     | _ => #[Html.element "span" true #[("class", "fn")] (←infoFormatToHtml t)]
 
+def argToHtml (arg : Arg) : HtmlM Html := do
+  let (l, r, implicit) := match arg.binderInfo with
+  | BinderInfo.default => ("(", ")", false)
+  | BinderInfo.implicit => ("{", "}", true)
+  | BinderInfo.strictImplicit => ("⦃", "⦄", true)
+  | BinderInfo.instImplicit => ("[", "]", true)
+  -- TODO: Can this ever be reached here? What does it mean?
+  | BinderInfo.auxDecl => unreachable!
+  let mut nodes := #[Html.text s!"{l}{arg.name.toString} : "]
+  nodes := nodes.append (←infoFormatToHtml arg.type)
+  nodes := nodes.push r
+  let inner := Html.element "span" true #[("class", "fn")] nodes
+  let html := Html.element "span" false #[("class", "decl_args")] #[inner]
+  if implicit then
+    <span «class»="impl_arg">{html}</span>
+  else
+    html
+
 def docInfoHeader (doc : DocInfo) : HtmlM Html := do
   let mut nodes := #[]
   -- TODO: noncomputable, partial
@@ -61,7 +79,8 @@ def docInfoHeader (doc : DocInfo) : HtmlM Html := do
         {doc.getName.toString}
       </a>
     </span>
-  -- TODO: Figure out how we can get explicit, implicit and TC args and put them here
+  for arg in doc.getArgs do
+    nodes := nodes.push (←argToHtml arg)
   nodes := nodes.push <span «class»="decl_args">:</span>
   nodes := nodes.push $ Html.element "div" true #[("class", "decl_type")] (←infoFormatToHtml doc.getType)
   -- TODO: The final type of the declaration

DocGen4/Process.lean

@@ -20,7 +20,13 @@ structure NameInfo where
   type : CodeWithInfos
   deriving Inhabited
 
+structure Arg where
+  name : Name
+  type : CodeWithInfos
+  binderInfo : BinderInfo
+
 structure Info extends NameInfo where
+  args : Array Arg
   doc : Option String
   declarationRange : DeclarationRange
   deriving Inhabited
@@ -89,6 +95,20 @@ structure Module where
   members : Array DocInfo
   deriving Inhabited
 
+partial def typeToArgsType (e : Expr) : (Array (Name × Expr × BinderInfo) × Expr) :=
+  match e.consumeMData with
+  | Expr.lam name type body data =>
+    let name := name.eraseMacroScopes
+    let arg := (name, type, data.binderInfo)
+    let (args, final) := typeToArgsType (Expr.instantiate1 body (mkFVar ⟨name⟩))
+    (#[arg] ++ args, final)
+  | Expr.forallE name type body data =>
+    let name := name.eraseMacroScopes
+    let arg := (name, type, data.binderInfo)
+    let (args, final) := typeToArgsType (Expr.instantiate1 body (mkFVar ⟨name⟩))
+    (#[arg] ++ args, final)
+  | _ => (#[], e)
+
 def prettyPrintTerm (expr : Expr) : MetaM CodeWithInfos := do
   let (fmt, infos) ← formatInfos expr
   let tt := TaggedText.prettyTagged fmt
@@ -104,11 +124,13 @@ def prettyPrintTerm (expr : Expr) : MetaM CodeWithInfos := do
 
 def Info.ofConstantVal (v : ConstantVal) : MetaM Info := do
   let env ← getEnv
-  let t ← prettyPrintTerm v.type
+  let (args, type) := typeToArgsType v.type
+  let type ← prettyPrintTerm type
+  let args ← args.mapM (λ (n, e, b) => do Arg.mk n (←prettyPrintTerm e) b)
   let doc ← findDocString? env v.name
   match ←findDeclarationRanges? v.name with
   -- TODO: Maybe selection range is more relevant? Figure this out in the future
-  | some range => return Info.mk ⟨v.name, t⟩ doc range.range
+  | some range => return Info.mk ⟨v.name, type⟩ args doc range.range
   | none => panic! s!"{v.name} is a declaration without position"
 
 def AxiomInfo.ofAxiomVal (v : AxiomVal) : MetaM AxiomInfo := do
@@ -274,6 +296,16 @@ def getType : DocInfo → CodeWithInfos
 | structureInfo i => i.type
 | classInfo i => i.type
 
+def getArgs : DocInfo → Array Arg
+| axiomInfo i => i.args
+| theoremInfo i => i.args
+| opaqueInfo i => i.args
+| definitionInfo i => i.args
+| instanceInfo i => i.args
+| inductiveInfo i => i.args
+| structureInfo i => i.args
+| classInfo i => i.args
+
 end DocInfo
 
 structure AnalyzerResult where