feat: Show inductive constructors properly

Closes: #2

DocGen4/Output/Base.lean

@@ -3,14 +3,15 @@ Copyright (c) 2021 Henrik Böving. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Henrik Böving
 -/
-import Lean
 import DocGen4.Process
 import DocGen4.IncludeStr
+import DocGen4.ToHtmlFormat
 
 namespace DocGen4
 namespace Output
 
-open Lean System
+open scoped DocGen4.Jsx
+open Lean System Widget Elab
 
 structure SiteContext where
   root : String
@@ -49,5 +50,38 @@ section Static
   def navJs : String := include_str "./static/nav.js"
 end Static
 
+def declNameToLink (name : Name) : HtmlM String := do
+  let res ← getResult
+  let module := res.moduleNames[res.name2ModIdx.find! name]
+  (←moduleNameToLink module) ++ "#" ++ name.toString
+
+def splitWhitespaces (s : String) : (String × String × String) := Id.run do
+  let front := "".pushn ' ' (s.find (!Char.isWhitespace ·))
+  let mut s := s.trimLeft
+  let back := "".pushn ' ' (s.length - s.offsetOfPos (s.find Char.isWhitespace))
+  s:= s.trimRight
+  (front, s, back)
+
+partial def infoFormatToHtml (i : CodeWithInfos) : HtmlM (Array Html) := do
+  match i with
+  | TaggedText.text t => return #[t]
+  | TaggedText.append tt => tt.foldlM (λ acc t => do acc ++ (←infoFormatToHtml t)) #[]
+  | TaggedText.tag a t =>
+    match a.info.val.info with
+    | Info.ofTermInfo i =>
+      match i.expr.consumeMData with
+      | Expr.const name _ _ =>
+         match t with
+         | TaggedText.text t =>
+           let (front, t, back) := splitWhitespaces t
+           let elem := Html.element "a" true #[("href", ←declNameToLink name)] #[t]
+           #[Html.text front, elem, Html.text back]
+         | _ =>
+           -- TODO: Is this ever reachable?
+           #[Html.element "a" true #[("href", ←declNameToLink name)] (←infoFormatToHtml t)]
+      | _ =>
+         #[Html.element "span" true #[("class", "fn")] (←infoFormatToHtml t)]
+    | _ => #[Html.element "span" true #[("class", "fn")] (←infoFormatToHtml t)]
+
 end Output
 end DocGen4

DocGen4/Output/Inductive.lean

@@ -0,0 +1,17 @@
+import DocGen4.Output.Template
+
+namespace DocGen4
+namespace Output
+
+open scoped DocGen4.Jsx
+
+
+def ctorToHtml (i : NameInfo) : HtmlM Html := do
+  let name := i.name.components'.head!.toString
+  return <li «class»="constructor" id={name}>{name} : [←infoFormatToHtml i.type]</li>
+
+def inductiveToHtml (i : InductiveInfo) : HtmlM (Array Html) := do
+  #[Html.element "ul" false #[("class", "constructors")] (←i.ctors.toArray.mapM ctorToHtml)]
+
+end Output
+end DocGen4

DocGen4/Output/Module.lean

@@ -3,51 +3,14 @@ Copyright (c) 2021 Henrik Böving. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Henrik Böving
 -/
-import Lean
-import Lean.PrettyPrinter
-import Lean.Widget.TaggedText
-
-import DocGen4.ToHtmlFormat
 import DocGen4.Output.Template
+import DocGen4.Output.Inductive
 
 namespace DocGen4
 namespace Output
 
 open scoped DocGen4.Jsx
-open Lean PrettyPrinter Widget Elab
-
-def declNameToLink (name : Name) : HtmlM String := do
-  let res ← getResult
-  let module := res.moduleNames[res.name2ModIdx.find! name]
-  (←moduleNameToLink module) ++ "#" ++ name.toString
-
-def splitWhitespaces (s : String) : (String × String × String) := Id.run do
-  let front := "".pushn ' ' (s.find (!Char.isWhitespace ·))
-  let mut s := s.trimLeft
-  let back := "".pushn ' ' (s.length - s.offsetOfPos (s.find Char.isWhitespace))
-  s:= s.trimRight
-  (front, s, back)
-
-partial def infoFormatToHtml (i : CodeWithInfos) : HtmlM (Array Html) := do
-  match i with
-  | TaggedText.text t => return #[t]
-  | TaggedText.append tt => tt.foldlM (λ acc t => do acc ++ (←infoFormatToHtml t)) #[]
-  | TaggedText.tag a t =>
-    match a.info.val.info with
-    | Info.ofTermInfo i =>
-      match i.expr.consumeMData with
-      | Expr.const name _ _ =>
-         match t with
-         | TaggedText.text t =>
-           let (front, t, back) := splitWhitespaces t
-           let elem := Html.element "a" true #[("href", ←declNameToLink name)] #[t]
-           #[Html.text front, elem, Html.text back]
-         | _ =>
-           -- TODO: Is this ever reachable?
-           #[Html.element "a" true #[("href", ←declNameToLink name)] (←infoFormatToHtml t)]
-      | _ =>
-         #[Html.element "span" true #[("class", "fn")] (←infoFormatToHtml t)]
-    | _ => #[Html.element "span" true #[("class", "fn")] (←infoFormatToHtml t)]
+open Lean
 
 def argToHtml (arg : Arg) : HtmlM Html := do
   let (l, r, implicit) := match arg.binderInfo with
@@ -87,7 +50,11 @@ def docInfoHeader (doc : DocInfo) : HtmlM Html := do
   return <div «class»="decl_header"> [nodes] </div>
 
 def docInfoToHtml (doc : DocInfo) : HtmlM Html := do
-  <div «class»="decl" id={doc.getName.toString}>
+  let doc_html := match doc with
+  | DocInfo.inductiveInfo i => inductiveToHtml i
+  | _ => #[]
+
+  return <div «class»="decl" id={doc.getName.toString}>
     <div «class»={doc.getKind}>
       <div «class»="gh_link">
         -- TODO: Put the proper source link
@@ -95,7 +62,7 @@ def docInfoToHtml (doc : DocInfo) : HtmlM Html := do
       </div>
       -- TODO: Attributes
       {←docInfoHeader doc}
-      -- TODO: The actual type information we are here for
+      [←doc_html]
     </div>
   </div>
 

DocGen4/Process.lean

@@ -52,14 +52,8 @@ structure DefinitionInfo extends Info where
 abbrev InstanceInfo := DefinitionInfo
 
 structure InductiveInfo extends Info where
-  numParams : Nat     -- Number of parameters
-  numIndices : Nat    -- Number of indices
-  all : List Name     -- List of all (including this one) inductive datatypes in the mutual declaration containing this one
   ctors : List NameInfo   -- List of all constructors and their type for this inductive datatype
-  isRec : Bool        -- `true` Iff it is recursive
   isUnsafe : Bool
-  isReflexive : Bool
-  isNested : Bool
   deriving Inhabited
 
 structure FieldInfo extends NameInfo where
@@ -166,7 +160,7 @@ def InductiveInfo.ofInductiveVal (v : InductiveVal) : MetaM InductiveInfo := do
   let info ← Info.ofConstantVal v.toConstantVal
   let env ← getEnv
   let ctors ← v.ctors.mapM (λ name => do NameInfo.mk name (←getConstructorType name))
-  return InductiveInfo.mk info v.numParams v.numIndices v.all ctors v.isRec v.isUnsafe v.isReflexive v.isNested
+  return InductiveInfo.mk info ctors v.isUnsafe
 
 def getFieldTypeAux (type : Expr) (vars : List Name) : (Expr × List Name) :=
   match type with