diff --git a/DocGen4/Output/Class.lean b/DocGen4/Output/Class.lean new file mode 100644 index 0000000..d69f311 --- /dev/null +++ b/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 +
  • {name.toString}
  • + +def instancesToHtml (i : ClassInfo) : HtmlM Html := do + let instancesHtml ← i.instances.mapM instanceToHtml + return
    + Instances + +
    + +def classToHtml (i : ClassInfo) : HtmlM (Array Html) := do + (←structureToHtml i.toStructureInfo).push (←instancesToHtml i) + +end Output +end DocGen4 diff --git a/DocGen4/Output/Module.lean b/DocGen4/Output/Module.lean index 37fade1..3f8a34e 100644 --- a/DocGen4/Output/Module.lean +++ b/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 : 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
    diff --git a/DocGen4/Process.lean b/DocGen4/Process.lean index cc62467..19f6c2a 100644 --- a/DocGen4/Process.lean +++ b/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 diff --git a/static/style.css b/static/style.css index e930689..727ba48 100644 --- a/static/style.css +++ b/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;