From e47321100938852afffd41c3c882ba637662d354 Mon Sep 17 00:00:00 2001
From: Parth Shastri <31370288+cppio@users.noreply.github.com>
Date: Tue, 17 Dec 2024 08:46:50 -0500
Subject: [PATCH] feat: show inductive constructor argument names (#249)

* feat: show inductive constructor argument names

* refactor: move argToHtml to DocGen4.Output.Arg
---
 DocGen4/Output/Arg.lean            | 22 ++++++++++++++++++++++
 DocGen4/Output/Inductive.lean      |  8 +++++---
 DocGen4/Output/Module.lean         | 13 -------------
 DocGen4/Process/Base.lean          | 12 ++++++------
 DocGen4/Process/InductiveInfo.lean |  8 +-------
 static/style.css                   |  2 +-
 6 files changed, 35 insertions(+), 30 deletions(-)
 create mode 100644 DocGen4/Output/Arg.lean

diff --git a/DocGen4/Output/Arg.lean b/DocGen4/Output/Arg.lean
new file mode 100644
index 00000000..3d1c66c5
--- /dev/null
+++ b/DocGen4/Output/Arg.lean
@@ -0,0 +1,22 @@
+import DocGen4.Output.Base
+
+namespace DocGen4
+namespace Output
+
+open scoped DocGen4.Jsx
+
+/--
+Render an `Arg` as HTML, adding opacity effects etc. depending on what
+type of binder it has.
+-/
+def argToHtml (arg : Process.Arg) : HtmlM Html := do
+  let node ← infoFormatToHtml arg.binder
+  let inner := <span class="fn">[node]</span>
+  let html := Html.element "span" false #[("class", "decl_args")] #[inner]
+  if arg.implicit then
+    return <span class="impl_arg">{html}</span>
+  else
+    return html
+
+end Output
+end DocGen4
diff --git a/DocGen4/Output/Inductive.lean b/DocGen4/Output/Inductive.lean
index ead0e067..042c8aa5 100644
--- a/DocGen4/Output/Inductive.lean
+++ b/DocGen4/Output/Inductive.lean
@@ -1,3 +1,4 @@
+import DocGen4.Output.Arg
 import DocGen4.Output.Template
 import DocGen4.Output.DocString
 import DocGen4.Process
@@ -15,20 +16,21 @@ def instancesForToHtml (typeName : Name) : BaseHtmlM Html := do
         <ul class="instances-for-enum"></ul>
     </details>
 
-def ctorToHtml (c : Process.NameInfo) : HtmlM Html := do
+def ctorToHtml (c : Process.ConstructorInfo) : HtmlM Html := do
   let shortName := c.name.componentsRev.head!.toString
   let name := c.name.toString
+  let args ← c.args.mapM argToHtml
   if let some doc := c.doc then
     let renderedDoc ← docStringToHtml doc name
     pure
       <li class="constructor" id={name}>
-        {shortName} : [← infoFormatToHtml c.type]
+        {shortName} [args] {" : "} [← infoFormatToHtml c.type]
         <div class="inductive_ctor_doc">[renderedDoc]</div>
       </li>
   else
     pure
       <li class="constructor" id={name}>
-        {shortName} : [← infoFormatToHtml c.type]
+        {shortName} [args] {" : "} [← infoFormatToHtml c.type]
       </li>
 
 def inductiveToHtml (i : Process.InductiveInfo) : HtmlM (Array Html) := do
diff --git a/DocGen4/Output/Module.lean b/DocGen4/Output/Module.lean
index 71b52785..3386e6ce 100644
--- a/DocGen4/Output/Module.lean
+++ b/DocGen4/Output/Module.lean
@@ -20,19 +20,6 @@ namespace Output
 open scoped DocGen4.Jsx
 open Lean Process
 
-/--
-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 node ← infoFormatToHtml arg.binder
-  let inner := <span class="fn">[node]</span>
-  let html := Html.element "span" false #[("class", "decl_args")] #[inner]
-  if arg.implicit then
-    return <span class="impl_arg">{html}</span>
-  else
-    return html
-
 /--
 Render the structures this structure extends from as HTML so it can be
 added to the top level.
diff --git a/DocGen4/Process/Base.lean b/DocGen4/Process/Base.lean
index 9e395ebc..6395f2f6 100644
--- a/DocGen4/Process/Base.lean
+++ b/DocGen4/Process/Base.lean
@@ -117,6 +117,11 @@ structure InstanceInfo extends DefinitionInfo where
   typeNames : Array Name
   deriving Inhabited
 
+/--
+Information about a constructor of an inductive type
+-/
+abbrev ConstructorInfo := Info
+
 /--
 Information about an `inductive` declaration
 -/
@@ -124,7 +129,7 @@ structure InductiveInfo extends Info where
   /--
   List of all constructors of this inductive type.
   -/
-  ctors : List NameInfo
+  ctors : List ConstructorInfo
   isUnsafe : Bool
   deriving Inhabited
 
@@ -166,11 +171,6 @@ Information about a `class inductive` declaration.
 abbrev ClassInductiveInfo := InductiveInfo
 
 
-/--
-Information about a constructor of an inductive type
--/
-abbrev ConstructorInfo := Info
-
 /--
 A general type for informations about declarations.
 -/
diff --git a/DocGen4/Process/InductiveInfo.lean b/DocGen4/Process/InductiveInfo.lean
index 1c27a1d0..ebd111a4 100644
--- a/DocGen4/Process/InductiveInfo.lean
+++ b/DocGen4/Process/InductiveInfo.lean
@@ -12,15 +12,9 @@ namespace DocGen4.Process
 
 open Lean Meta 
 
-def getConstructorType (ctor : Name) : MetaM Expr := do
-  let env ← getEnv
-  match env.find? ctor with
-  | some (ConstantInfo.ctorInfo i) => pure i.type
-  | _ => panic! s!"Constructor {ctor} was requested but does not exist"
-
 def InductiveInfo.ofInductiveVal (v : InductiveVal) : MetaM InductiveInfo := do
   let info ← Info.ofConstantVal v.toConstantVal
-  let ctors ← v.ctors.mapM (fun name => do NameInfo.ofTypedName name (← getConstructorType name))
+  let ctors ← v.ctors.mapM (fun name => do Info.ofConstantVal (← getConstInfoCtor name).toConstantVal)
   return {
     toInfo := info,
     ctors,
diff --git a/static/style.css b/static/style.css
index 5817520e..1e7c1da9 100644
--- a/static/style.css
+++ b/static/style.css
@@ -753,7 +753,7 @@ a:hover {
     transition: opacity 300ms ease-in;
 }
 
-.decl_header:not(:hover) .impl_arg {
+.decl_header:not(:hover) .impl_arg, .constructor:not(:hover) .impl_arg {
     opacity: 30%;
     transition: opacity 1000ms ease-out;
 }