From a34441f40521ff081c5149e8a06db9474198ee91 Mon Sep 17 00:00:00 2001
From: Parth Shastri <31370288+cppio@users.noreply.github.com>
Date: Mon, 16 Dec 2024 16:56:27 -0500
Subject: [PATCH 1/2] feat: show inductive constructor argument names
---
DocGen4/Output/Inductive.lean | 20 +++++++++++++++++---
DocGen4/Output/Module.lean | 13 -------------
DocGen4/Process/Base.lean | 12 ++++++------
DocGen4/Process/InductiveInfo.lean | 8 +-------
static/style.css | 2 +-
5 files changed, 25 insertions(+), 30 deletions(-)
diff --git a/DocGen4/Output/Inductive.lean b/DocGen4/Output/Inductive.lean
index ead0e067..916c5da8 100644
--- a/DocGen4/Output/Inductive.lean
+++ b/DocGen4/Output/Inductive.lean
@@ -8,6 +8,19 @@ namespace Output
open scoped DocGen4.Jsx
open Lean
+/--
+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 := [node]
+ let html := Html.element "span" false #[("class", "decl_args")] #[inner]
+ if arg.implicit then
+ return {html}
+ else
+ return html
+
def instancesForToHtml (typeName : Name) : BaseHtmlM Html := do
pure
@@ -15,20 +28,21 @@ def instancesForToHtml (typeName : Name) : BaseHtmlM Html := do
-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
- {shortName} : [← infoFormatToHtml c.type]
+ {shortName} [args] {" : "} [← infoFormatToHtml c.type]
[renderedDoc]
else
pure
- {shortName} : [← infoFormatToHtml c.type]
+ {shortName} [args] {" : "} [← infoFormatToHtml c.type]
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 := [node]
- let html := Html.element "span" false #[("class", "decl_args")] #[inner]
- if arg.implicit then
- return {html}
- 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;
}
From 7cd7193b8d99bf5aa34c09ee4446a23775ab19cb Mon Sep 17 00:00:00 2001
From: Parth Shastri <31370288+cppio@users.noreply.github.com>
Date: Tue, 17 Dec 2024 08:11:30 -0500
Subject: [PATCH 2/2] refactor: move argToHtml to DocGen4.Output.Arg
---
DocGen4/Output/Arg.lean | 22 ++++++++++++++++++++++
DocGen4/Output/Inductive.lean | 14 +-------------
2 files changed, 23 insertions(+), 13 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 := [node]
+ let html := Html.element "span" false #[("class", "decl_args")] #[inner]
+ if arg.implicit then
+ return {html}
+ else
+ return html
+
+end Output
+end DocGen4
diff --git a/DocGen4/Output/Inductive.lean b/DocGen4/Output/Inductive.lean
index 916c5da8..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
@@ -8,19 +9,6 @@ namespace Output
open scoped DocGen4.Jsx
open Lean
-/--
-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 := [node]
- let html := Html.element "span" false #[("class", "decl_args")] #[inner]
- if arg.implicit then
- return {html}
- else
- return html
-
def instancesForToHtml (typeName : Name) : BaseHtmlM Html := do
pure