feat: use the core signature delaborator (#231)

This PR makes use of the core signature delaborator to pretty print signatures. This fixes some bugs and brings the output in line with `#check`.

For example:
- Now binders are grouped.
- Now it uses the same heuristics for what comes before and after the colon.
- Now it the bug [reported in this Zulip thread](https://leanprover.zulipchat.com/#narrow/channel/113488-general/topic/docgen.20strange.20daggers/near/481964331) is fixed, where daggers appeared in the incorrect positions.

DocGen4/Output/Module.lean

@@ -25,20 +25,10 @@ Render an `Arg` as HTML, adding opacity effects etc. depending on what
 type of binder it has.
 -/
 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)
-  let mut nodes :=
-    match arg.name with
-    | some name => #[Html.text s!"{l}{name.toString} : "]
-    | none => #[Html.text s!"{l}"]
-  nodes := nodes.append (← infoFormatToHtml arg.type)
-  nodes := nodes.push r
-  let inner := <span class="fn">[nodes]</span>
+  let node ← infoFormatToHtml arg.binder
+  let inner := <span class="fn">[node]</span>
   let html := Html.element "span" false #[("class", "decl_args")] #[inner]
-  if implicit then
+  if arg.implicit then
     return <span class="impl_arg">{html}</span>
   else
     return html

DocGen4/Process/Base.lean

@@ -33,18 +33,13 @@ An argument to a declaration, e.g. the `(x : Nat)` in `def foo (x : Nat) := x`.
 -/
 structure Arg where
   /--
-  The name of the argument. For auto generated argument names like `[Monad α]`
-  this is none
+  The pretty printed binder syntax itself.
   -/
-  name : Option Name
+  binder : CodeWithInfos
   /--
-  The pretty printed type of the argument.
+  Whether the binder is implicit.
   -/
-  type : CodeWithInfos
-  /--
-  What kind of binder was used for the argument.
-  -/
-  binderInfo : BinderInfo
+  implicit : Bool
 
 /--
 A base structure for information about a declaration.

DocGen4/Process/NameInfo.lean

@@ -15,42 +15,60 @@ def NameInfo.ofTypedName (n : Name) (t : Expr) : MetaM NameInfo := do
   let env ← getEnv
   return { name := n, type := ← prettyPrintTerm t, doc := ← findDocString? env n}
 
-partial def argTypeTelescope {α : Type} (e : Expr) (k : Array ((Option Name) × Expr × BinderInfo) → Expr → MetaM α) : MetaM α :=
-  go e #[]
-where
-  go (e : Expr) (args : Array ((Option Name) × Expr × BinderInfo)) : MetaM α := do
-    let helper := fun name type body bi =>
-      -- Once we hit a name with a macro scope we stop traversing the expression
-      -- and print what is left after the : instead. The only exception
-      -- to this is instances since these almost never have a name
-      -- but should still be printed as arguments instead of after the :.
-      if bi.isInstImplicit && name.hasMacroScopes then
-        let arg := (none, type, bi)
-        Meta.withLocalDecl name bi type fun fvar => do
-          go (Expr.instantiate1 body fvar) (args.push arg)
-      else if name.hasMacroScopes then
-        k args e
-      else
-        let arg := (some name, type, bi)
-        Meta.withLocalDecl name bi type fun fvar => do
-          go (Expr.instantiate1 body fvar) (args.push arg)
-    match e.consumeMData with
-    | Expr.forallE name type body binderInfo => helper name type body binderInfo
-    | _ => k args e
+/--
+Pretty prints a `Lean.Parser.Term.bracketedBinder`.
+-/
+private def prettyPrintBinder (stx : Syntax) (infos : SubExpr.PosMap Elab.Info) : MetaM Widget.CodeWithInfos := do
+  let fmt ← PrettyPrinter.format Parser.Term.bracketedBinder.formatter stx
+  let tt := Widget.TaggedText.prettyTagged fmt
+  let ctx := {
+    env := ← getEnv
+    mctx := ← getMCtx
+    options := ← getOptions
+    currNamespace := ← getCurrNamespace
+    openDecls := ← getOpenDecls
+    fileMap := default,
+    ngen := ← getNGen
+  }
+  return Widget.tagCodeInfos ctx infos tt
+
+private def prettyPrintTermStx (stx : Term) (infos : SubExpr.PosMap Elab.Info) : MetaM Widget.CodeWithInfos := do
+  let fmt ← PrettyPrinter.formatTerm stx
+  let tt := Widget.TaggedText.prettyTagged fmt
+  let ctx := {
+    env := ← getEnv
+    mctx := ← getMCtx
+    options := ← getOptions
+    currNamespace := ← getCurrNamespace
+    openDecls := ← getOpenDecls
+    fileMap := default,
+    ngen := ← getNGen
+  }
+  return Widget.tagCodeInfos ctx infos tt
 
 def Info.ofConstantVal (v : ConstantVal) : MetaM Info := do
-  argTypeTelescope v.type fun args type => do
-    let args ← args.mapM (fun (n, e, b) => do return Arg.mk n (← prettyPrintTerm e) b)
-    let nameInfo ← NameInfo.ofTypedName v.name type
-    match ← findDeclarationRanges? v.name with
-    -- TODO: Maybe selection range is more relevant? Figure this out in the future
-    | some range =>
-      return {
-        toNameInfo := nameInfo,
-        args,
-        declarationRange := range.range,
-        attrs := ← getAllAttributes v.name
-      }
-    | none => panic! s!"{v.name} is a declaration without position"
+  let e := Expr.const v.name (v.levelParams.map mkLevelParam)
+  -- 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 := (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}"
+  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
+  -- 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},
+      args,
+      declarationRange := range.range,
+      attrs := ← getAllAttributes v.name
+    }
+  | none => panic! s!"{v.name} is a declaration without position"
 
 end DocGen4.Process