diff --git a/SubDocGen.lean b/SubDocGen.lean new file mode 100644 index 00000000..5c555322 --- /dev/null +++ b/SubDocGen.lean @@ -0,0 +1,161 @@ +/- +Copyright (c) 2025 Anne Baanen. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Anne Baanen +-/ +module + +public meta import Lean.Elab.Command +public import Lean.EnvExtension +public import Lean.Meta.Basic + +/-! +# Library for adding supplementary pages to the DocGen output. + +In addition to the pages listing declarations, DocGen can output supplementary pages. +Each page is made up of an introduction followed by a sequence of sections. +These sections can be added individually through metaprogramming, for example when adding an +attribute to a declaration. + +The main user interface for adding pages and sections can be found in the commands +`register_supplement_page` and `register_supplement_section`; these correspond to +`SubDocGen.registerSupplementPage` and `SubDocGen.registerSupplementSection` respectively. +-/ + +namespace SubDocGen + +open Lean Meta + +/-- A docstring formatted in Markdown. -/ +public abbrev MarkdownDocstring := String + +/-- A section out of a `SupplementPage`. -/ +public structure SupplementSection (textFormat : Type) where + /-- Human-readable title of the section. -/ + name : String + + /-- Main contents of this section. -/ + text : textFormat + + /-- Module where this section is defined. Will be set by `registerSupplementSection`. -/ + definingModule : Option Name + /-- Declaration(s) relating to this section. + + For example, a tactic might link here to its implementation. + -/ + relatedDecls : Array Name +deriving FromJson, ToJson + +/-- +A page to be rendered in addition to the module docs. + +Pages have some introductory text, followed by headered sections. +-/ +public structure SupplementPage (textFormat : Type) where + /-- Human-readable name of the page. -/ + name : String + /-- Page introduction. -/ + intro : textFormat + + /-- Module where this page is defined. Will be set by `registerSupplementPage`. -/ + definingModule : Option Name + /-- Sections of the page. Will be computed by DocGen during processing of the supplement pages. -/ + sections : Array (SupplementSection textFormat) + +/-- A section out of a `SupplementPage`, plus information on where to place the section. -/ +public structure SupplementSectionEntry (textFormat) extends SupplementSection textFormat where + /-- Identifies the page to which this section belongs. -/ + pageKey : String +deriving FromJson, ToJson + +/-- A page to be rendered in addition to the module docs, plus information on +where to find its sections. -/ +public structure SupplementPageEntry (textFormat) extends SupplementPage textFormat where + /-- A unique identifier for this page, used to associate sections declared in downstream modules. -/ + key : String +deriving FromJson, ToJson + +/-- This environment extension allows adding supplement pages that will be rendered by DocGen. +Add entries using the `SubDocGen.registerSupplementPage` function or +`register_supplement_page` command. +-/ +-- Pages are stored as a `HashMap` for easy existence checking. +public meta initialize supplementPageExt : SimplePersistentEnvExtension (SupplementPageEntry MarkdownDocstring) + (Std.HashMap String (SupplementPageEntry MarkdownDocstring)) ← + registerSimplePersistentEnvExtension { + addImportedFn as := as.foldl (fun m as => m.insertMany (as.map fun a => (a.key, a))) {} + addEntryFn m a := m.insert a.key a + } + +/-- This environment extension allows adding sections to supplement pages. +Add entries using the `SubDocGen.registerSupplementSection` function or +`register_supplement_section` command. + +See also `SubDocGen.supplementPageExt`. +-/ +-- Sections are stored as an array since they are all scanned through per-module anyway. +public meta initialize supplementSectionExt : SimplePersistentEnvExtension (SupplementSectionEntry MarkdownDocstring) + (Array (SupplementSectionEntry MarkdownDocstring)) ← + registerSimplePersistentEnvExtension { + addImportedFn as := as.flatten + addEntryFn as a := as.push a + } + +variable {m} [Monad m] [MonadEnv m] [MonadError m] + +/-- Add a page (with perhaps some predefined sections) to the DocGen supplement. +This function is the interface for metaprograms: the command `register_supplement_page` is the +basic wrapper for users. + +Page keys should be unique. If not, this function throws an error. + +Further sections to this page can be added by calling `registerSupplementSection`. +-/ +public meta def registerSupplementPage (page : SupplementPageEntry MarkdownDocstring) : m Unit := do + if (supplementPageExt.getState (← getEnv)).contains page.key then + throwError m!"registerSupplementPage: there is already a page with key `{page.key}`." + modifyEnv (supplementPageExt.addEntry · { page with definingModule := (← getEnv).header.mainModule }) + +/-- Add a section to a page in the DocGen supplement. +This function is the interface for metaprograms: the command `register_supplement_section` is the +basic wrapper for users. + +The page that this section appears in should first be declared using `registerSupplementPage`. +If not, this function throws an error. +-/ +public meta def registerSupplementSection (sec : SupplementSectionEntry MarkdownDocstring) : m Unit := do + if !(supplementPageExt.getState (← getEnv)).contains sec.pageKey then + throwError m!"registerSupplementSection: no page has been declared with key `{sec.pageKey}`." + modifyEnv (supplementSectionExt.addEntry · { sec with definingModule := (← getEnv).header.mainModule }) + +open Elab Command in +/-- `register_supplement_page key "Page Title" /-- Introduction text -/` +adds a page to the DocGen supplement under the given key. + +In metaprograms, you can call `registerSupplementPage` directly. +-/ +elab "register_supplement_page " name:ident ppSpace title:str ppSpace dc:docComment : command => do + registerSupplementPage { + key := name.getId.toString + name := title.getString + intro := dc.getDocString + definingModule := none + sections := #[] + } + +open Elab Command in +/-- `register_supplement_section pageKey "Section Title" /-- Introduction text -/` +adds a section to the `pageKey` page in the DocGen supplement. + +In metaprograms, you can call `registerSupplementSection` directly. +-/ +elab "register_supplement_section " pageKey:ident ppSpace title:str ppSpace dc:docComment : command => do + registerSupplementSection { + pageKey := pageKey.getId.toString + name := title.getString + text := dc.getDocString + definingModule := none + relatedDecls := #[] + } + +end SubDocGen diff --git a/lakefile.lean b/lakefile.lean index 8e61872b..d0d7aaea 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -5,6 +5,9 @@ package «doc-gen4» lean_lib DocGen4 +lean_lib SubDocGen where + leanOptions := #[⟨`experimental.module, true⟩] + @[default_target] lean_exe «doc-gen4» { root := `Main