r
/
bookshelf-doc
mirror of https://github.com/jrpotter/bookshelf-doc
1
Fork 0
Code Issues Packages Projects Releases Wiki Activity

Merge pull request #18 from leanprover/constructor-links 

Fix links to inductive constructors and structure fields
main
Henrik Böving 2022-01-09 14:10:25 +01:00 committed by GitHub
parent b90644cfd2 0754b43873
commit 0751cea667
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
3 changed files with 9 additions and 6 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

5
DocGen4/Output/Inductive.lean
View File

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

4
DocGen4/Output/Structure.lean
View File

@ -6,7 +6,9 @@ namespace Output
open scoped DocGen4.Jsx open scoped DocGen4.Jsx
def fieldToHtml (f : NameInfo) : HtmlM Html := do def fieldToHtml (f : NameInfo) : HtmlM Html := do
return <li «class»="structure_field" id={f.name.toString}>{s!"{f.name} : "} [←infoFormatToHtml f.type]</li> let shortName := f.name.components'.head!.toString
let name := f.name.toString
return <li «class»="structure_field" id={name}>{shortName} : [←infoFormatToHtml f.type]</li>
def structureToHtml (i : StructureInfo) : HtmlM (Array Html) := do def structureToHtml (i : StructureInfo) : HtmlM (Array Html) := do
#[Html.element "ul" false #[("class", "structure_fields"), ("id", s!"{i.name.toString}.mk")] (←i.fieldInfo.mapM fieldToHtml)] #[Html.element "ul" false #[("class", "structure_fields"), ("id", s!"{i.name.toString}.mk")] (←i.fieldInfo.mapM fieldToHtml)]

6
DocGen4/Process.lean
View File

@ -182,13 +182,13 @@ def dropArgs (type : Expr) (n : Nat) : (Expr × List (Name × Expr)) :=
{ next with snd := (name, type) :: next.snd} { next with snd := (name, type) :: next.snd}
| e, x + 1 => panic! s!"No forallE left" | e, x + 1 => panic! s!"No forallE left"
def getFieldTypes (ctor : ConstructorVal) (parents : Nat) : MetaM (Array NameInfo) := do def getFieldTypes (struct : Name) (ctor : ConstructorVal) (parents : Nat) : MetaM (Array NameInfo) := do
let type := ctor.type let type := ctor.type
let (field_function, params) := dropArgs type (ctor.numParams + parents) let (field_function, params) := dropArgs type (ctor.numParams + parents)
let (_, fields) := dropArgs field_function (ctor.numFields - parents) let (_, fields) := dropArgs field_function (ctor.numFields - parents)
let mut field_infos := #[] let mut field_infos := #[]
for (name, type) in fields do for (name, type) in fields do
field_infos := field_infos.push { name := name, type := ←prettyPrintTerm type} field_infos := field_infos.push { name := struct.append name, type := ←prettyPrintTerm type}
field_infos field_infos
def StructureInfo.ofInductiveVal (v : InductiveVal) : MetaM StructureInfo := do def StructureInfo.ofInductiveVal (v : InductiveVal) : MetaM StructureInfo := do
@ -200,7 +200,7 @@ def StructureInfo.ofInductiveVal (v : InductiveVal) : MetaM StructureInfo := do
match getStructureInfo? env v.name with match getStructureInfo? env v.name with
| some i => | some i =>
if i.fieldNames.size - parents.size > 0 then if i.fieldNames.size - parents.size > 0 then
return StructureInfo.mk info (←getFieldTypes ctor parents.size) parents ⟨ctor.name, ctorType⟩ return StructureInfo.mk info (←getFieldTypes v.name ctor parents.size) parents ⟨ctor.name, ctorType⟩
else else
return StructureInfo.mk info #[] parents ⟨ctor.name, ctorType⟩ return StructureInfo.mk info #[] parents ⟨ctor.name, ctorType⟩
| none => panic! s!"{v.name} is not a structure" | none => panic! s!"{v.name} is not a structure"