From f4227b176999c14d7559b7c8119e058cab78ed33 Mon Sep 17 00:00:00 2001 From: Rob Simmons Date: Sun, 28 Dec 2025 18:32:29 -0500 Subject: [PATCH 1/2] Begin allowing directives to elaborate to Target.Block --- doc/UsersGuide/Markup.lean | 10 ++--- src/verso-blog/VersoBlog.lean | 12 ++--- src/verso-manual/VersoManual.lean | 6 +-- src/verso-manual/VersoManual/Docstring.lean | 6 +-- src/verso/Verso/Doc/Elab.lean | 2 +- src/verso/Verso/Doc/Elab/Monad.lean | 49 +++++++++++++++++---- 6 files changed, 58 insertions(+), 27 deletions(-) diff --git a/doc/UsersGuide/Markup.lean b/doc/UsersGuide/Markup.lean index 33c72b92..29aa0251 100644 --- a/doc/UsersGuide/Markup.lean +++ b/doc/UsersGuide/Markup.lean @@ -282,7 +282,7 @@ open Lean Elab in open Verso.Parser in open Lean.Doc.Syntax in @[directive] -def markupPreview : DirectiveExpanderOf MarkupPreviewConfig +def markupPreview : DirectiveElabOf MarkupPreviewConfig | {title}, contents => do let #[blk1, blk2] := contents.filter nonempty | throwError "Expected precisely two code blocks, got {contents.filter nonempty}" @@ -304,10 +304,10 @@ def markupPreview : DirectiveExpanderOf MarkupPreviewConfig throwErrorAt expected m!"Expected {indentD expected.getString} but got {indentD p}\n{hint}" Hover.addCustomHover contents s!"```\n{p}\n```" - ``(Block.other (MarkupExample $(quote title.getString)) #[ - Block.code $(quote contents.getString), - Block.code $(quote <| toString <| p) - ]) + return .other (← ``(MarkupExample $(quote title.getString))) #[ + .code contents.getString, + .code p + ] where eq (s1 s2 : String) : Bool := let lines1 := s1.trimAscii.split (· == '\n') |>.map (·.trimAsciiEnd) |>.toArray diff --git a/src/verso-blog/VersoBlog.lean b/src/verso-blog/VersoBlog.lean index 1d361988..f310a838 100644 --- a/src/verso-blog/VersoBlog.lean +++ b/src/verso-blog/VersoBlog.lean @@ -60,10 +60,10 @@ def htmlSpan : RoleExpanderOf ClassArgs Wraps the contents in an HTML `
` element with the provided `class`. -/ @[directive] -def htmlDiv : DirectiveExpanderOf ClassArgs +def htmlDiv : DirectiveElabOf ClassArgs | {«class»}, stxs => do - let contents ← stxs.mapM elabBlockTerm - ``(Block.other (Blog.BlockExt.htmlDiv $(quote «class»)) #[ $contents,* ]) + let contents ← stxs.mapM elabBlock' + return .other (← ``(Blog.BlockExt.htmlDiv $(quote «class»))) contents private partial def attrs : ArgParse DocElabM (Array (String × String)) := List.toArray <$> .many attr @@ -80,11 +80,11 @@ instance : FromArgs HtmlArgs DocElabM where @[directive] -def html : DirectiveExpanderOf HtmlArgs +def html : DirectiveElabOf HtmlArgs | {name, attrs}, stxs => do let tag := name.toString (escape := false) - let contents ← stxs.mapM elabBlockTerm - ``(Block.other (Blog.BlockExt.htmlWrapper $(quote tag) $(quote attrs)) #[ $contents,* ]) + let contents ← stxs.mapM elabBlock' + return .other (← ``(Blog.BlockExt.htmlWrapper $(quote tag) $(quote attrs))) contents structure BlobArgs where blobName : Ident diff --git a/src/verso-manual/VersoManual.lean b/src/verso-manual/VersoManual.lean index fefbe59a..68343cb7 100644 --- a/src/verso-manual/VersoManual.lean +++ b/src/verso-manual/VersoManual.lean @@ -161,10 +161,10 @@ paragraph. In HTML output, they are rendered with less space between them, and L a single paragraph (e.g. without extraneous indentation). -/ @[directive] -def paragraph : DirectiveExpanderOf Unit +def paragraph : DirectiveElabOf Unit | (), stxs => do - let args ← stxs.mapM elabBlockTerm - ``(Block.other Block.paragraph #[ $[ $args ],* ]) + let args ← stxs.mapM elabBlock' + return .other (← ``(Block.paragraph)) args structure Config extends HtmlConfig where destination : System.FilePath := "_out" diff --git a/src/verso-manual/VersoManual/Docstring.lean b/src/verso-manual/VersoManual/Docstring.lean index 20214e8b..80bcb51e 100644 --- a/src/verso-manual/VersoManual/Docstring.lean +++ b/src/verso-manual/VersoManual/Docstring.lean @@ -1672,7 +1672,7 @@ private def getTactic? (name : String ⊕ Name) : TermElabM (Option TacticDoc) : return none @[directive] -def tactic : DirectiveExpanderOf TacticDocsOptions +def tactic : DirectiveElabOf TacticDocsOptions | opts, more => do let tactics ← getTacticOverloads opts.name let blame : Syntax := opts.name.elim TSyntax.raw TSyntax.raw @@ -1695,8 +1695,8 @@ def tactic : DirectiveExpanderOf TacticDocsOptions let some mdAst := MD4Lean.parse str | throwError m!"Failed to parse docstring as Markdown. Docstring contents:\n{repr str}" mdAst.blocks.mapM (blockFromMarkdownWithLean []) - let userContents ← more.mapM elabBlockTerm - ``(Verso.Doc.Block.other (Block.tactic $(quote tactic) $(quote opts.show)) #[$(contents ++ userContents),*]) + let userContents ← more.mapM elabBlock' + return .other (← ``(Block.tactic $(quote tactic) $(quote opts.show))) (contents.map .stx ++ userContents) def Inline.tactic : Inline where name := `Verso.Genre.Manual.tacticInline diff --git a/src/verso/Verso/Doc/Elab.lean b/src/verso/Verso/Doc/Elab.lean index c59b35eb..55d1852f 100644 --- a/src/verso/Verso/Doc/Elab.lean +++ b/src/verso/Verso/Doc/Elab.lean @@ -463,7 +463,7 @@ public meta def _root_.Lean.Doc.Syntax.directive.expand : BlockElab try let termStxs ← withFreshMacroScope <| e args contents expanderDocHover nameStx "Directive" name doc? sig? - return .concat (termStxs.map .stx) + return .concat termStxs catch | ex@(.internal id) => if id == unsupportedSyntaxExceptionId then pure () diff --git a/src/verso/Verso/Doc/Elab/Monad.lean b/src/verso/Verso/Doc/Elab/Monad.lean index e843d735..cea569e6 100644 --- a/src/verso/Verso/Doc/Elab/Monad.lean +++ b/src/verso/Verso/Doc/Elab/Monad.lean @@ -799,11 +799,27 @@ public abbrev DirectiveExpander := Array Arg → TSyntaxArray `block → DocElab public abbrev DirectiveExpanderOf α := α → TSyntaxArray `block → DocElabM Term +public abbrev DirectiveElaborator := Array Arg → TSyntaxArray `block → DocElabM (Array Target.Block) + +/-- +The type of directive elaborators. In order to give a declaration of type {lean}`DirectiveElabOf α` +the {lit}`@[directive]` annotation, it must be possible to synthesize {lean}`FromArgs α DocElabM`. +-/ +public abbrev DirectiveElabOf (α : Type) := α → TSyntaxArray `block → DocElabM Target.Block + +public def directiveExpanderToElaborator (expander : DirectiveExpander) : DirectiveElaborator + | args, contents => do return (← expander args contents).map (.stx ·) + initialize directiveExpanderAttr : KeyedDeclsAttribute DirectiveExpander ← mkDocExpanderAttribute `directive_expander ``DirectiveExpander "Indicates that this function is used to implement a given directive" `directiveExpanderAttr -public def toDirective {α : Type} [FromArgs α DocElabM] (expander : α → TSyntaxArray `block → DocElabM Term) : DirectiveExpander := +public def toDirectiveTerm {α : Type} [FromArgs α DocElabM] (expander : α → TSyntaxArray `block → DocElabM Term) : DirectiveElaborator := + fun args blocks => do + let v ← ArgParse.parse args + return #[.stx (← expander v blocks)] + +public def toDirective {α : Type} [FromArgs α DocElabM] (expander : α → TSyntaxArray `block → DocElabM Target.Block) : DirectiveElaborator := fun args blocks => do let v ← ArgParse.parse args return #[← expander v blocks] @@ -838,14 +854,29 @@ unsafe initialize registerBuiltinAttribute { let n ← mkFreshUserName <| declName ++ `directive + -- Find the appropriate adapter for both new (`DirectiveElabOf`) and legacy (`DirectiveExpanderOf`) declarations + let constructor ← match (← getEnv).find? declName |>.map (·.type.getAppFn) with + | some (Expr.const ``DirectiveExpanderOf _) => pure ``toDirectiveTerm + | some (Expr.const ``DirectiveElabOf _) => pure ``toDirective + | some e => + logWarning m!"Declaration tagged with `@[directive]` has type{indentD e}\nwhich is not in \ + one of the expected forms `{.ofConstName ``DirectiveExpanderOf} _` or \ + `{.ofConstName ``DirectiveElabOf} _`" + pure ``toDirective + | none => + logError m!"Unexpected error: definition of `{declName}` not found" + return + let ((e, t), _) ← Meta.MetaM.run (ctx := {}) (s := {}) do - let e ← Meta.mkAppM ``toDirective #[.const declName []] + let e ← Meta.mkAppM constructor #[.const declName []] let e ← instantiateMVars e let t ← Meta.inferType e - match_expr e with - | toDirective ty _ _ => saveSignature n ty + | toDirectiveTerm ty _ _ => + saveSignature n ty + | toDirective ty _ _ => + saveSignature n ty | _ => pure () pure (e, t) @@ -865,10 +896,10 @@ unsafe initialize registerBuiltinAttribute { directiveExpanderExt.addEntry env (directiveName, n) } -private unsafe def directiveExpandersForUnsafe' (x : Name) : DocElabM (Array (DirectiveExpander × Option String × Option SigDoc)) := do +private unsafe def directiveExpandersForUnsafe' (x : Name) : DocElabM (Array (DirectiveElaborator × Option String × Option SigDoc)) := do let expanders := directiveExpanderExt.getState (← getEnv) |>.find? x |>.getD #[] expanders.mapM fun n => do - let e ← evalConst DirectiveExpander n + let e ← evalConst DirectiveElaborator n let doc? ← findDocString? (← getEnv) n let sig := expanderSignatureExt.getState (← getEnv) |>.find? n return (e, doc?, sig) @@ -877,11 +908,11 @@ private unsafe def directiveExpandersForUnsafe'' (x : Name) : DocElabM (Array Di let expanders := directiveExpanderAttr.getEntries (← getEnv) x return expanders.map (·.value) |>.toArray -private unsafe def directiveExpandersForUnsafe (x : Name) : DocElabM (Array (DirectiveExpander × Option String × Option SigDoc)) := do - return (← directiveExpandersForUnsafe' x) ++ (← directiveExpandersForUnsafe'' x).map (·, none, none) +private unsafe def directiveExpandersForUnsafe (x : Name) : DocElabM (Array (DirectiveElaborator × Option String × Option SigDoc)) := do + return (← directiveExpandersForUnsafe' x) ++ (← directiveExpandersForUnsafe'' x).map (directiveExpanderToElaborator ·, none, none) @[implemented_by directiveExpandersForUnsafe] -public opaque directiveExpandersFor (x : Name) : DocElabM (Array (DirectiveExpander × Option String × Option SigDoc)) +public opaque directiveExpandersFor (x : Name) : DocElabM (Array (DirectiveElaborator × Option String × Option SigDoc)) public abbrev BlockCommandExpander := Array Arg → DocElabM (Array (TSyntax `term)) From 540fcb08102f3880f042fac11e312f04c039f03b Mon Sep 17 00:00:00 2001 From: Rob Simmons Date: Mon, 29 Dec 2025 08:23:40 -0500 Subject: [PATCH 2/2] more directive expanders to directive elabs --- src/verso-blog/VersoBlog.lean | 4 ++-- src/verso-manual/VersoManual/Docstring.lean | 6 +++--- .../VersoManual/Docstring/Progress.lean | 4 ++-- src/verso-manual/VersoManual/Draft.lean | 4 ++-- src/verso-manual/VersoManual/Table.lean | 7 ++++--- test-projects/website/DemoSite/About.lean | 14 +++++++------- 6 files changed, 20 insertions(+), 19 deletions(-) diff --git a/src/verso-blog/VersoBlog.lean b/src/verso-blog/VersoBlog.lean index f310a838..45411b8b 100644 --- a/src/verso-blog/VersoBlog.lean +++ b/src/verso-blog/VersoBlog.lean @@ -93,11 +93,11 @@ instance : FromArgs BlobArgs DocElabM where fromArgs := BlobArgs.mk <$> .positional `blobName .ident @[directive] -def blob : DirectiveExpanderOf BlobArgs +def blob : DirectiveElabOf BlobArgs | {blobName}, stxs => do if h : stxs.size > 0 then logErrorAt stxs[0] "Expected no contents" let actualName ← realizeGlobalConstNoOverloadWithInfo blobName - ``(Block.other (Blog.BlockExt.blob ($(mkIdentFrom blobName actualName) : Html)) #[]) + return .other (← ``(Blog.BlockExt.blob ($(mkIdentFrom blobName actualName) : Html))) #[] @[role blob] def inlineBlob : RoleExpanderOf BlobArgs diff --git a/src/verso-manual/VersoManual/Docstring.lean b/src/verso-manual/VersoManual/Docstring.lean index 80bcb51e..7185689f 100644 --- a/src/verso-manual/VersoManual/Docstring.lean +++ b/src/verso-manual/VersoManual/Docstring.lean @@ -1842,7 +1842,7 @@ def getConvTactic (name : StrLit ⊕ Ident) (allowMissing : Option Bool) : TermE throwError m!"Conv tactic not found: {kind}" @[directive] -def conv : DirectiveExpanderOf TacticDocsOptions +def conv : DirectiveElabOf TacticDocsOptions | opts, more => do let tactic ← getConvTactic opts.name opts.allowMissing Doc.PointOfInterest.save (← getRef) tactic.name.toString @@ -1851,10 +1851,10 @@ def conv : DirectiveExpanderOf TacticDocsOptions | throwError "Failed to parse docstring as Markdown" mdAst.blocks.mapM (blockFromMarkdownWithLean []) else pure #[] - let userContents ← more.mapM elabBlockTerm + let userContents ← more.mapM elabBlock' let some toShow := opts.show | throwError "An explicit 'show' is mandatory for conv docs (for now)" - ``(Verso.Doc.Block.other (Block.conv $(quote tactic.name) $(quote toShow) $(quote tactic.docs?)) #[$(contents ++ userContents),*]) + return .other (← ``(Block.conv $(quote tactic.name) $(quote toShow) $(quote tactic.docs?))) (contents.map (.stx ·) ++ userContents) open Verso.Search in def convDomainMapper : DomainMapper := { diff --git a/src/verso-manual/VersoManual/Docstring/Progress.lean b/src/verso-manual/VersoManual/Docstring/Progress.lean index 0234019a..fe511d19 100644 --- a/src/verso-manual/VersoManual/Docstring/Progress.lean +++ b/src/verso-manual/VersoManual/Docstring/Progress.lean @@ -63,7 +63,7 @@ run_cmd do elabCommand <| ← `(private def $(mkIdent `allRootNames) : Array Name := #[$(names.map (quote · : Name → Term)),*]) @[directive] -public def progress : DirectiveExpanderOf Unit +public def progress : DirectiveElabOf Unit | (), blocks => do let mut namespaces : NameSet := {} let mut exceptions : NameSet := {} @@ -111,7 +111,7 @@ public def progress : DirectiveExpanderOf Unit let present' := present.toList.map (fun x => (x.1, String.intercalate " " (x.2.toList.map Name.toString))) let allTactics : Array Name := (← Elab.Tactic.Doc.allTacticDocs).map (fun t => t.internalName) - ``(Verso.Doc.Block.other (Verso.Genre.Manual.Block.progress $(quote namespaces.toArray) $(quote exceptions.toArray) $(quote present') $(quote allTactics)) #[]) + return .other (← ``(Verso.Genre.Manual.Block.progress $(quote namespaces.toArray) $(quote exceptions.toArray) $(quote present') $(quote allTactics))) #[] @[block_extension Block.progress] public def progress.descr : BlockDescr where diff --git a/src/verso-manual/VersoManual/Draft.lean b/src/verso-manual/VersoManual/Draft.lean index 332fdfb7..5aa5c8c1 100644 --- a/src/verso-manual/VersoManual/Draft.lean +++ b/src/verso-manual/VersoManual/Draft.lean @@ -57,6 +57,6 @@ def draft : RoleExpanderOf Unit /-- Hide draft-only content when in not in draft mode -/ @[directive draft] -def draftBlock : DirectiveExpanderOf Unit +def draftBlock : DirectiveElabOf Unit | (), contents => do - ``(Verso.Doc.Block.other Block.draft #[$[$(← contents.mapM elabBlockTerm)],*]) + return .other (← ``(Block.draft)) (← contents.mapM elabBlock') diff --git a/src/verso-manual/VersoManual/Table.lean b/src/verso-manual/VersoManual/Table.lean index 6994de2d..a0dc1092 100644 --- a/src/verso-manual/VersoManual/Table.lean +++ b/src/verso-manual/VersoManual/Table.lean @@ -185,7 +185,7 @@ instance : FromArgs TableConfig m := ⟨TableConfig.parse⟩ end @[directive] -def table : DirectiveExpanderOf TableConfig +def table : DirectiveElabOf TableConfig | cfg, contents => do -- The table should be a list of lists. Extract them! let #[oneBlock] := contents @@ -210,8 +210,9 @@ def table : DirectiveExpanderOf TableConfig throwErrorAt oneBlock s!"Expected all rows to have same number of columns, but got {rows.map (·.size)}" let flattened := rows.flatten - let blocks : Array (Syntax.TSepArray `term ",") ← flattened.mapM (·.mapM elabBlockTerm) - ``(Block.other (Block.table $(quote columns) $(quote cfg.header) $(quote cfg.name) $(quote cfg.alignment)) #[Block.ul #[$[Verso.Doc.ListItem.mk #[$blocks,*]],*]]) + let blocks : Array (Array Target.Block) ← flattened.mapM (·.mapM elabBlock') + return .other (← ``(Block.table $(quote columns) $(quote cfg.header) $(quote cfg.name) $(quote cfg.alignment))) + #[.ul blocks] where getLi : Syntax → DocElabM (TSyntaxArray `block) diff --git a/test-projects/website/DemoSite/About.lean b/test-projects/website/DemoSite/About.lean index db62beae..b0ec0116 100644 --- a/test-projects/website/DemoSite/About.lean +++ b/test-projects/website/DemoSite/About.lean @@ -24,9 +24,9 @@ def redBox : BlockComponent where pure {{
{{← contents.mapM goB}}
}} @[directive redBox] -def redBoxImpl : DirectiveExpanderOf Unit +def redBoxImpl : DirectiveElabOf Unit | (), stxs => do - ``(Block.other (Blog.BlockExt.component $(quote `redBox) Json.null) #[$(← stxs.mapM elabBlockTerm),*]) + return .other (← ``(Blog.BlockExt.component $(quote `redBox) Json.null)) (← stxs.mapM elabBlock') block_component gallery where toHtml id _data _goI goB contents := do @@ -49,17 +49,17 @@ block_component image where @[directive gallery] -def galleryImpl : DirectiveExpanderOf Unit +def galleryImpl : DirectiveElabOf Unit | (), stxs => do let #[stx] := stxs | logErrorAt (mkNullNode stxs) "Expected one block" - return (← `(sorry)) + return .other (← `(sorry)) #[] let `(block| dl{ $item*}) := stx | throwErrorAt stx "Expected definition list" let items ← item.mapM getItem - ``(Block.other (Blog.BlockExt.component $(quote `gallery) Json.null) #[$(items),*]) + return .other (← ``(Blog.BlockExt.component $(quote `gallery) Json.null)) items where - getItem : TSyntax `desc_item → DocElabM Term + getItem : TSyntax `desc_item → DocElabM Target.Block | `(desc_item|: $inls* => $desc $descs*) => do let #[inl] := inls.filter (fun | `(inline|$s:str) => s.getString.any (not ∘ Char.isWhitespace) @@ -67,7 +67,7 @@ where | throwErrorAt (mkNullNode inls) "Expected one inline" let `(inline|image($alt)($url)) := inl | throwErrorAt inl "Expected an image" - `(Block.other (.component $(quote `image) (.arr #[$alt, $url])) #[$(← elabBlockTerm desc), $(← descs.mapM elabBlockTerm),*]) + return .other (← `(.component $(quote `image) (.arr #[$alt, $url]))) (#[← elabBlock' desc] ++ (← descs.mapM elabBlock')) | stx => throwErrorAt stx "Expected an image and description, got {stx}" block_component +directive button' (onclick : String) where