From 5ab6766eb17a118ed490216305de2a7651e9ebf8 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Henrik=20B=C3=B6ving?= Date: Thu, 16 Feb 2023 19:51:35 +0100 Subject: [PATCH] fix: #113 --- DocGen4/Output/DocString.lean | 2 +- DocGen4/Output/Module.lean | 5 +++-- DocGen4/Output/ToJson.lean | 2 +- DocGen4/Process/Analyze.lean | 6 +++++- DocGen4/Process/Base.lean | 11 +++++++++++ DocGen4/Process/DocInfo.lean | 28 ++++++++++++++++++++++++++-- 6 files changed, 47 insertions(+), 7 deletions(-) diff --git a/DocGen4/Output/DocString.lean b/DocGen4/Output/DocString.lean index 82ef367..758b317 100644 --- a/DocGen4/Output/DocString.lean +++ b/DocGen4/Output/DocString.lean @@ -78,7 +78,7 @@ def nameToLink? (s : String) : HtmlM (Option String) := do else match (← getCurrentName) with | some currentName => - match res.moduleInfo.find! currentName |>.members |> filterMapDocInfo |>.find? (sameEnd ·.getName name) with + match res.moduleInfo.find! currentName |>.members |> filterDocInfo |>.find? (sameEnd ·.getName name) with | some info => declNameToLink info.getName | _ => return none diff --git a/DocGen4/Output/Module.lean b/DocGen4/Output/Module.lean index f7bf551..3437bd2 100644 --- a/DocGen4/Output/Module.lean +++ b/DocGen4/Output/Module.lean @@ -205,8 +205,9 @@ def internalNav (members : Array Name) (moduleName : Name) : HtmlM Html := do The main entry point to rendering the HTML for an entire module. -/ def moduleToHtml (module : Process.Module) : HtmlM Html := withTheReader SiteBaseContext (setCurrentName module.name) do - let memberDocs ← module.members.mapM (moduleMemberToHtml module.name ·) - let memberNames := filterMapDocInfo module.members |>.map DocInfo.getName + let relevantMembers := module.members.filter Process.ModuleMember.shouldRender + let memberDocs ← relevantMembers.mapM (moduleMemberToHtml module.name) + let memberNames := filterDocInfo relevantMembers |>.map DocInfo.getName templateLiftExtends (baseHtmlGenerator module.name.toString) <| pure #[ ← internalNav memberNames module.name, Html.element "main" false #[] memberDocs diff --git a/DocGen4/Output/ToJson.lean b/DocGen4/Output/ToJson.lean index 0692c8c..a641f67 100644 --- a/DocGen4/Output/ToJson.lean +++ b/DocGen4/Output/ToJson.lean @@ -86,7 +86,7 @@ def DocInfo.toJson (module : Name) (info : Process.DocInfo) : HtmlM JsonDeclarat def Process.Module.toJson (module : Process.Module) : HtmlM Json := do let mut jsonDecls := [] let mut instances := #[] - let declInfo := Process.filterMapDocInfo module.members + let declInfo := Process.filterDocInfo module.members for decl in declInfo do jsonDecls := (← DocInfo.toJson module.name decl) :: jsonDecls if let .instanceInfo i := decl then diff --git a/DocGen4/Process/Analyze.lean b/DocGen4/Process/Analyze.lean index 29229ca..b071997 100644 --- a/DocGen4/Process/Analyze.lean +++ b/DocGen4/Process/Analyze.lean @@ -77,6 +77,10 @@ def getDocString : ModuleMember → Option String | docInfo i => i.getDocString | modDoc i => i.doc +def shouldRender : ModuleMember → Bool +| docInfo i => i.shouldRender +| modDoc _ => true + end ModuleMember inductive AnalyzeTask where @@ -144,7 +148,7 @@ def process (task : AnalyzeTask) : MetaM (AnalyzerResult × Hierarchy) := do } return (analysis, hierarchy) -def filterMapDocInfo (ms : Array ModuleMember) : Array DocInfo := +def filterDocInfo (ms : Array ModuleMember) : Array DocInfo := ms.filterMap filter where filter : ModuleMember → Option DocInfo diff --git a/DocGen4/Process/Base.lean b/DocGen4/Process/Base.lean index e1c52fc..c5908ce 100644 --- a/DocGen4/Process/Base.lean +++ b/DocGen4/Process/Base.lean @@ -60,6 +60,10 @@ structure Info extends NameInfo where A list of (known) attributes that are attached to the declaration. -/ attrs : Array String + /-- + Whether this info item should be rendered + -/ + render : Bool := true deriving Inhabited /-- @@ -147,6 +151,12 @@ 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. -/ @@ -160,6 +170,7 @@ inductive DocInfo where | structureInfo (info : StructureInfo) : DocInfo | classInfo (info : ClassInfo) : DocInfo | classInductiveInfo (info : ClassInductiveInfo) : DocInfo +| ctorInfo (info : ConstructorInfo) : DocInfo deriving Inhabited /-- diff --git a/DocGen4/Process/DocInfo.lean b/DocGen4/Process/DocInfo.lean index 0d81b98..8985ab8 100644 --- a/DocGen4/Process/DocInfo.lean +++ b/DocGen4/Process/DocInfo.lean @@ -31,6 +31,7 @@ def getDeclarationRange : DocInfo → DeclarationRange | structureInfo i => i.declarationRange | classInfo i => i.declarationRange | classInductiveInfo i => i.declarationRange +| ctorInfo i => i.declarationRange def getName : DocInfo → Name | axiomInfo i => i.name @@ -42,6 +43,7 @@ def getName : DocInfo → Name | structureInfo i => i.name | classInfo i => i.name | classInductiveInfo i => i.name +| ctorInfo i => i.name def getKind : DocInfo → String | axiomInfo _ => "axiom" @@ -53,6 +55,7 @@ def getKind : DocInfo → String | structureInfo _ => "structure" | classInfo _ => "class" | classInductiveInfo _ => "class" +| ctorInfo _ => "ctor" -- TODO: kind ctor support in js def getType : DocInfo → CodeWithInfos | axiomInfo i => i.type @@ -64,6 +67,7 @@ def getType : DocInfo → CodeWithInfos | structureInfo i => i.type | classInfo i => i.type | classInductiveInfo i => i.type +| ctorInfo i => i.type def getArgs : DocInfo → Array Arg | axiomInfo i => i.args @@ -75,6 +79,7 @@ def getArgs : DocInfo → Array Arg | structureInfo i => i.args | classInfo i => i.args | classInductiveInfo i => i.args +| ctorInfo i => i.args def getAttrs : DocInfo → Array String | axiomInfo i => i.attrs @@ -86,6 +91,7 @@ def getAttrs : DocInfo → Array String | structureInfo i => i.attrs | classInfo i => i.attrs | classInductiveInfo i => i.attrs +| ctorInfo i => i.attrs def getDocString : DocInfo → Option String | axiomInfo i => i.doc @@ -97,6 +103,19 @@ def getDocString : DocInfo → Option String | structureInfo i => i.doc | classInfo i => i.doc | classInductiveInfo i => i.doc +| ctorInfo i => i.doc + +def shouldRender : DocInfo → Bool +| axiomInfo i => i.render +| theoremInfo i => i.render +| opaqueInfo i => i.render +| definitionInfo i => i.render +| instanceInfo i => i.render +| inductiveInfo i => i.render +| structureInfo i => i.render +| classInfo i => i.render +| classInductiveInfo i => i.render +| ctorInfo i => i.render def isBlackListed (declName : Name) : MetaM Bool := do match ← findDeclarationRanges? declName with @@ -135,7 +154,8 @@ def ofConstant : (Name × ConstantInfo) → MetaM (Option DocInfo) := fun (name, | ConstantInfo.opaqueInfo i => return some <| opaqueInfo (← OpaqueInfo.ofOpaqueVal i) | ConstantInfo.defnInfo i => if ← isProjFn i.name then - return none + let info ← DefinitionInfo.ofDefinitionVal i + return some <| definitionInfo { info with render := false } else if ← isInstance i.name then let info ← InstanceInfo.ofDefinitionVal i @@ -155,8 +175,11 @@ def ofConstant : (Name × ConstantInfo) → MetaM (Option DocInfo) := fun (name, return some <| classInductiveInfo (← ClassInductiveInfo.ofInductiveVal i) else return some <| inductiveInfo (← InductiveInfo.ofInductiveVal i) + | ConstantInfo.ctorInfo i => + let info ← Info.ofConstantVal i.toConstantVal + return some <| ctorInfo { info with render := false } -- we ignore these for now - | ConstantInfo.ctorInfo _ | ConstantInfo.recInfo _ | ConstantInfo.quotInfo _ => return none + | ConstantInfo.recInfo _ | ConstantInfo.quotInfo _ => return none def getKindDescription : DocInfo → String | axiomInfo i => if i.isUnsafe then "unsafe axiom" else "axiom" @@ -191,6 +214,7 @@ def getKindDescription : DocInfo → String | structureInfo _ => "structure" | classInfo _ => "class" | classInductiveInfo _ => "class inductive" +| ctorInfo _ => "constructor" end DocInfo