From 3adb8e71d15ee1a0829fc6d2e787e1d102ff30c6 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Henrik=20B=C3=B6ving?= Date: Mon, 3 Jan 2022 18:22:12 +0100 Subject: [PATCH] feat: Show inductive constructors properly Closes: #2 --- DocGen4/Output/Base.lean | 38 +++++++++++++++++++++++++-- DocGen4/Output/Inductive.lean | 17 ++++++++++++ DocGen4/Output/Module.lean | 49 ++++++----------------------------- DocGen4/Process.lean | 8 +----- 4 files changed, 62 insertions(+), 50 deletions(-) create mode 100644 DocGen4/Output/Inductive.lean diff --git a/DocGen4/Output/Base.lean b/DocGen4/Output/Base.lean index 92deae9..2eddfbc 100644 --- a/DocGen4/Output/Base.lean +++ b/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 diff --git a/DocGen4/Output/Inductive.lean b/DocGen4/Output/Inductive.lean new file mode 100644 index 0000000..521c42c --- /dev/null +++ b/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
  • {name} : [←infoFormatToHtml i.type]
    • + +def inductiveToHtml (i : InductiveInfo) : HtmlM (Array Html) := do + #[Html.element "ul" false #[("class", "constructors")] (←i.ctors.toArray.mapM ctorToHtml)] + +end Output +end DocGen4 diff --git a/DocGen4/Output/Module.lean b/DocGen4/Output/Module.lean index b467935..5990f89 100644 --- a/DocGen4/Output/Module.lean +++ b/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
    [nodes]
    def docInfoToHtml (doc : DocInfo) : HtmlM Html := do -
    + let doc_html := match doc with + | DocInfo.inductiveInfo i => inductiveToHtml i + | _ => #[] + + return
    -- TODO: Put the proper source link @@ -95,7 +62,7 @@ def docInfoToHtml (doc : DocInfo) : HtmlM Html := do
    -- TODO: Attributes {←docInfoHeader doc} - -- TODO: The actual type information we are here for + [←doc_html]
    diff --git a/DocGen4/Process.lean b/DocGen4/Process.lean index 7de63ac..51020b3 100644 --- a/DocGen4/Process.lean +++ b/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