Merge pull request #14 from leanprover/class

Typeclass and instances handling

DocGen4/Output/Class.lean

@@ -0,0 +1,26 @@
+import DocGen4.Output.Template
+import DocGen4.Output.Structure
+
+namespace DocGen4
+namespace Output
+
+open scoped DocGen4.Jsx
+open Lean
+
+def instanceToHtml (name : Name) : HtmlM Html := do
+  <li><a href={←declNameToLink name}>{name.toString}</a></li>
+
+def instancesToHtml (i : ClassInfo) : HtmlM Html := do
+  let instancesHtml ← i.instances.mapM instanceToHtml
+  return <details «class»="instances">
+        <summary>Instances</summary>
+        <ul>
+          [instancesHtml]
+        </ul>
+    </details>
+
+def classToHtml (i : ClassInfo) : HtmlM (Array Html) := do
+  (←structureToHtml i.toStructureInfo).push (←instancesToHtml i)
+
+end Output
+end DocGen4

DocGen4/Output/Module.lean

@@ -6,6 +6,7 @@ Authors: Henrik Böving
 import DocGen4.Output.Template
 import DocGen4.Output.Inductive
 import DocGen4.Output.Structure
+import DocGen4.Output.Class
 
 namespace DocGen4
 namespace Output
@@ -59,8 +60,11 @@ def docInfoHeader (doc : DocInfo) : HtmlM Html := do
   for arg in doc.getArgs do
     nodes := nodes.push (←argToHtml arg)
 
-  if let DocInfo.structureInfo i := doc then
-    nodes := nodes.append (←structureInfoHeader i)
+  -- TODO: dedup this
+  match doc with
+  | DocInfo.structureInfo i => nodes := nodes.append (←structureInfoHeader i)
+  | DocInfo.classInfo i => nodes := nodes.append (←structureInfoHeader i.toStructureInfo)
+  | _ => nodes := nodes
 
   nodes := nodes.push <span «class»="decl_args">:</span>
   nodes := nodes.push $ Html.element "div" true #[("class", "decl_type")] (←infoFormatToHtml doc.getType)
@@ -70,6 +74,7 @@ def docInfoToHtml (doc : DocInfo) : HtmlM Html := do
   let doc_html ← match doc with
   | DocInfo.inductiveInfo i => inductiveToHtml i
   | DocInfo.structureInfo i => structureToHtml i
+  | DocInfo.classInfo i => classToHtml i
   | _ => #[]
 
   return <div «class»="decl" id={doc.getName.toString}>

DocGen4/Process.lean

@@ -63,8 +63,7 @@ structure StructureInfo extends Info where
   deriving Inhabited
 
 structure ClassInfo extends StructureInfo where
-  hasOutParam : Bool
-  instances : Array CodeWithInfos
+  instances : Array Name
   deriving Inhabited
 
 inductive DocInfo where
@@ -193,8 +192,7 @@ def ClassInfo.ofInductiveVal (v : InductiveVal) : MetaM ClassInfo := do
   let fn ← mkConstWithFreshMVarLevels v.name
   let (xs, _, _) ← forallMetaTelescopeReducing (← inferType fn)
   let insts ← SynthInstance.getInstances (mkAppN fn xs)
-  let insts_stx ← insts.mapM prettyPrintTerm
-  return ClassInfo.mk sinfo (hasOutParams (←getEnv) v.name) insts_stx
+  return ClassInfo.mk sinfo (insts.map Expr.constName!)
 
 namespace DocInfo
 

static/style.css

@@ -359,7 +359,7 @@ main h2, main h3, main h4, main h5, main h6 {
     margin-top: 4rem;
 }
 
-.def {
+.def, .instance {
     border-left: 10px solid #92dce5;
     border-top: 2px solid #92dce5;
 }
@@ -374,7 +374,7 @@ main h2, main h3, main h4, main h5, main h6 {
     border-top: 2px solid #f44708;
 }
 
-.structure, .inductive {
+.structure, .inductive, .class {
     border-left: 10px solid #f0a202;
     border-top: 2px solid #f0a202;
 }
@@ -400,7 +400,7 @@ main h2, main h3, main h4, main h5, main h6 {
     transition: background-color 100ms ease-in-out;
 }
 
-.def .fn:hover {
+.def .fn:hover, .instance .fn:hover {
     background-color: hsla(187, 61%, calc(100% - 5%*var(--fn)));
     box-shadow: 0 0 0 1px hsla(187, 61%, calc(100% - 5%*(var(--fn) + 1)));
     border-radius: 5px;
@@ -415,7 +415,7 @@ main h2, main h3, main h4, main h5, main h6 {
     box-shadow: 0 0 0 1px hsla(16, 94%, calc(100% - 5%*(var(--fn) + 1)));
     border-radius: 5px;
 }
-.structure .fn:hover, .inductive .fn:hover {
+.structure .fn:hover, .inductive .fn:hover, .class .fn:hover {
     background-color: hsla(40, 98%, calc(100% - 5%*var(--fn)));
     box-shadow: 0 0 0 1px hsla(40, 98%, calc(100% - 5%*(var(--fn) + 1)));
     border-radius: 5px;