feat: typed syntax as the target of doc elaboration

src/tests/Tests/VersoManual.lean

@@ -5,3 +5,4 @@ Author: David Thrane Christiansen
 -/
 import Tests.VersoManual.Html
 import Tests.VersoManual.Html.SoftHyphenate
+import Tests.VersoManual.Markdown

src/tests/Tests/VersoManual/Markdown.lean

@@ -8,7 +8,7 @@ import Verso.Doc.Elab.Monad
 import Lean.Elab.Term
 
 open Verso Doc Elab
-open Verso.Genre Manual Markdown
+open Verso.Genre Manual
 open Lean
 
 /--
@@ -38,7 +38,7 @@ def testAddPartFromMarkdown (input : String) : Elab.TermElabM String := do
   let addParts : PartElabM Unit := do
     let mut levels := []
     for block in parsed.blocks do
-      levels ← addPartFromMarkdown block levels
+      levels ← Markdown.addPartFromMarkdown block levels
     closePartsUntil 0 0
   let (_, _, part) ← addParts.run ⟨Syntax.node .none identKind #[], mkConst ``Manual, .always, .none⟩ default default
   part.partContext.priorParts.toList.map displayPartStructure |> String.join |> pure

src/verso-blog/VersoBlog.lean

@@ -62,7 +62,7 @@ Wraps the contents in an HTML `<div>` element with the provided `class`.
 @[directive]
 def htmlDiv : DirectiveExpanderOf ClassArgs
   | {«class»}, stxs => do
-    let contents ← stxs.mapM elabBlock
+    let contents ← stxs.mapM elabBlockTerm
     ``(Block.other (Blog.BlockExt.htmlDiv $(quote «class»)) #[ $contents,* ])
 
 
@@ -83,7 +83,7 @@ instance : FromArgs HtmlArgs DocElabM where
 def html : DirectiveExpanderOf HtmlArgs
   | {name, attrs}, stxs => do
     let tag := name.toString (escape := false)
-    let contents ← stxs.mapM elabBlock
+    let contents ← stxs.mapM elabBlockTerm
     ``(Block.other (Blog.BlockExt.htmlWrapper $(quote tag) $(quote attrs)) #[ $contents,* ])
 
 structure BlobArgs where

src/verso-blog/VersoBlog/Component.lean

@@ -312,7 +312,7 @@ elab_rules : command
         `(command|
           @[directive $x]
           def $dirName : DirectiveExpanderOf T
-            | $argPat, blocks => do `($qArgs #[$$(← blocks.mapM elabBlock),*]))
+            | $argPat, blocks => do `($qArgs #[$$(← blocks.mapM elabBlockTerm),*]))
       elabCommand cmd3
 
 

src/verso-manual/VersoManual.lean

@@ -163,7 +163,7 @@ a single paragraph (e.g. without extraneous indentation).
 @[directive]
 def paragraph : DirectiveExpanderOf Unit
   | (), stxs => do
-    let args ← stxs.mapM elabBlock
+    let args ← stxs.mapM elabBlockTerm
     ``(Block.other Block.paragraph #[ $[ $args ],* ])
 
 structure Config extends HtmlConfig where

src/verso-manual/VersoManual/Docstring.lean

@@ -1695,7 +1695,7 @@ 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 elabBlock
+    let userContents ← more.mapM elabBlockTerm
     ``(Verso.Doc.Block.other (Block.tactic $(quote tactic) $(quote opts.show)) #[$(contents ++ userContents),*])
 
 def Inline.tactic : Inline where
@@ -1851,7 +1851,7 @@ def conv : DirectiveExpanderOf TacticDocsOptions
           | throwError "Failed to parse docstring as Markdown"
         mdAst.blocks.mapM (blockFromMarkdownWithLean [])
       else pure #[]
-    let userContents ← more.mapM elabBlock
+    let userContents ← more.mapM elabBlockTerm
     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),*])

src/verso-manual/VersoManual/Draft.lean

@@ -59,4 +59,4 @@ def draft : RoleExpanderOf Unit
 @[directive draft]
 def draftBlock : DirectiveExpanderOf Unit
   | (), contents => do
-    ``(Verso.Doc.Block.other Block.draft #[$[$(← contents.mapM elabBlock)],*])
+    ``(Verso.Doc.Block.other Block.draft #[$[$(← contents.mapM elabBlockTerm)],*])

src/verso-manual/VersoManual/InlineLean.lean

@@ -536,7 +536,7 @@ def leanSection : DirectiveExpander
     let start ← `(block|```lean $arg | $(quote code) ```)
     let code := name?.map (s!"end {·}") |>.getD "end"
     let «end» ← `(block|```lean $arg | $(quote code) ```)
-    return #[← elabBlock start] ++ (← contents.mapM elabBlock) ++ #[← elabBlock «end»]
+    return #[← elabBlockTerm start] ++ (← contents.mapM elabBlockTerm) ++ #[← elabBlockTerm «end»]
 
 private def getClass : MessageSeverity → String
   | .error => "error"

src/verso-manual/VersoManual/InlineLean/IO.lean

@@ -545,5 +545,5 @@ open IOExample in
 def ioExample : DirectiveExpanderOf Unit
  | (), blocks => do
     startExample
-    let body ← blocks.mapM elabBlock
+    let body ← blocks.mapM elabBlockTerm
     ``(Verso.Doc.Block.concat #[$body,*]) >>= endExample

src/verso-manual/VersoManual/Table.lean

@@ -210,7 +210,7 @@ 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 elabBlock)
+      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,*]],*]])
 
 where

src/verso/Verso/Doc/Elab.lean

@@ -136,7 +136,7 @@ public meta def _root_.Lean.Doc.Syntax.role.expand : InlineExpander
           try
             let termStxs ← withFreshMacroScope <| e argVals subjects
             expanderDocHover name "Role" resolvedName doc? sig?
-            let termStxs ← termStxs.mapM fun t => (``(($t : Inline $(⟨genre⟩))))
+            let termStxs ← termStxs.mapM fun t => (``(($t : Doc.Inline $(⟨genre⟩))))
             if h : termStxs.size = 1 then return termStxs[0]
             else return (← ``(Inline.concat (genre := $(⟨genre⟩)) #[$[$termStxs],*]))
           catch
@@ -234,7 +234,7 @@ where
       throwErrorAt cmd "{msg}\n{note}"
     let hygenicName := some <| mkIdent (← mkFreshUserName `docReconstInBlock)
     let blk ← withTheReader DocElabContext ({ · with docReconstructionPlaceholder := hygenicName }) <|
-      elabBlock cmd
+      elabBlockTerm cmd
     addBlock blk (blockInternalDocReconstructionPlaceholder := hygenicName)
 
 @[part_command Lean.Doc.Syntax.footnote_ref]
@@ -327,23 +327,22 @@ public meta def includeSection : PartCommand
 where
  resolved id := mkIdentFrom id <$> realizeGlobalConstNoOverloadWithInfo (mkIdentFrom id (docName id.getId))
 
-@[block_expander Lean.Doc.Syntax.command]
-public meta def _root_.Lean.Doc.Syntax.command.expand : BlockExpander := fun block =>
+@[block_elab Lean.Doc.Syntax.command]
+public meta def _root_.Lean.Doc.Syntax.command.expand : BlockElab := fun block =>
   match block with
   | `(block|command{$name $args*}) => do
     withTraceNode `Elab.Verso.block (fun _ => pure m!"Block role {name}") <|
     withRef block <| withFreshMacroScope <| withIncRecDepth <| do
-      let genre := (← readThe DocElabContext).genreSyntax
       let resolvedName ← realizeGlobalConstNoOverloadWithInfo name
       let exp ← blockCommandExpandersFor resolvedName
       let argVals ← parseArgs args
       if exp.isEmpty then
-        return ← appFallback block name resolvedName argVals none
+        return .stx (← appFallback block name resolvedName argVals none)
       for (e, doc?, sig?) in exp do
         try
           let termStxs ← withFreshMacroScope <| e argVals
           expanderDocHover name "Command" resolvedName doc? sig?
-          return (← ``(Block.concat (genre := $(⟨genre⟩)) #[$[$termStxs],*]))
+          return .concat (termStxs.map .stx)
         catch
           | ex@(.internal id) =>
             if id == unsupportedSyntaxExceptionId then pure ()
@@ -352,98 +351,88 @@ public meta def _root_.Lean.Doc.Syntax.command.expand : BlockExpander := fun blo
       throwUnsupportedSyntax
   | _ => throwUnsupportedSyntax
 
-@[block_expander Lean.Doc.Syntax.para]
-public meta partial def _root_.Lean.Doc.Syntax.para.expand : BlockExpander
+@[block_elab Lean.Doc.Syntax.para]
+public meta partial def _root_.Lean.Doc.Syntax.para.expand : BlockElab
   | `(block| para[ $args:inline* ]) => do
-    let genre := (← readThe DocElabContext).genreSyntax
-    ``(Block.para (genre := $(⟨genre⟩)) #[$[$(← args.mapM elabInline)],*])
+    return .para (← args.mapM elabInline)
   | _ =>
     throwUnsupportedSyntax
 
-
-meta def elabLi (block : Syntax) : DocElabM (Syntax × TSyntax `term) :=
+meta def elabLi (block : Syntax) : DocElabM (Syntax × Array Target.Block) :=
   withRef block <|
   match block with
   | `(list_item|*%$dot $contents:block*) => do
-    let genre := (← readThe DocElabContext).genreSyntax
-    let item ← ``(ListItem.mk (α := Block $(⟨genre⟩)) #[$[$(← contents.mapM elabBlock)],*])
-    pure (dot, item)
+    pure (dot, ← contents.mapM elabBlock')
   | _ =>
     throwUnsupportedSyntax
 
-@[block_expander Lean.Doc.Syntax.ul]
-public meta def _root_.Lean.Doc.Syntax.ul.expand : BlockExpander
+@[block_elab Lean.Doc.Syntax.ul]
+public meta def _root_.Lean.Doc.Syntax.ul.expand : BlockElab
   | `(block|ul{$itemStxs*}) => do
-    let genre := (← readThe DocElabContext).genreSyntax
     let mut bullets : Array Syntax := #[]
-    let mut items : Array (TSyntax `term) := #[]
+    let mut items : Array (Array Target.Block) := #[]
     for i in itemStxs do
       let (b, item) ← elabLi i
       bullets := bullets.push b
       items := items.push item
     let info := DocListInfo.mk bullets itemStxs
     for b in bullets do
       pushInfoLeaf <| .ofCustomInfo {stx := b, value := Dynamic.mk info}
-    ``(Block.ul (genre := $(⟨genre⟩)) #[$items,*])
+    return .ul items
   | _ =>
     throwUnsupportedSyntax
 
-@[block_expander Lean.Doc.Syntax.ol]
-public meta def _root_.Lean.Doc.Syntax.ol.expand : BlockExpander
+@[block_elab Lean.Doc.Syntax.ol]
+public meta def _root_.Lean.Doc.Syntax.ol.expand : BlockElab
   | `(block|ol($start:num){$itemStxs*}) => do
-    let genre := (← readThe DocElabContext).genreSyntax
     let mut bullets : Array Syntax := #[]
-    let mut items : Array (TSyntax `term) := #[]
+    let mut items : Array (Array Target.Block) := #[]
     for i in itemStxs do
       let (b, item) ← elabLi i
       bullets := bullets.push b
       items := items.push item
     let info := DocListInfo.mk bullets itemStxs
     for b in bullets do
       pushInfoLeaf <| .ofCustomInfo {stx := b, value := Dynamic.mk info}
-    ``(Block.ol (genre := $(⟨genre⟩)) $start #[$items,*])
+    return .ol start.getNat items
   | _ =>
     throwUnsupportedSyntax
 
-meta def elabDesc (block : Syntax) : DocElabM (Syntax × TSyntax `term) :=
+meta def elabDesc (block : Syntax) : DocElabM (Syntax × Array Target.Inline × Array Target.Block) :=
   withRef block <|
   match block with
   | `(desc_item|:%$colon $dts* => $dds*) => do
-    let genre := (← readThe DocElabContext).genreSyntax
-    let item ← ``(DescItem.mk (α := Inline $(⟨genre⟩)) (β := Block $(⟨genre⟩))  #[$[$(← dts.mapM elabInline)],*] #[$[$(← dds.mapM elabBlock)],*])
-    pure (colon, item)
+    return (colon, ← dts.mapM elabInline, ← dds.mapM elabBlock')
   | _ =>
     throwUnsupportedSyntax
 
-@[block_expander Lean.Doc.Syntax.dl]
-public meta def _root_.Lean.Doc.Syntax.dl.expand : BlockExpander
+@[block_elab Lean.Doc.Syntax.dl]
+public meta def _root_.Lean.Doc.Syntax.dl.expand : BlockElab
   | `(block|dl{$itemStxs*}) => do
-    let genre := (← readThe DocElabContext).genreSyntax
     let mut colons : Array Syntax := #[]
-    let mut items : Array (TSyntax `term) := #[]
+    let mut items : Array (Array Target.Inline × Array Target.Block) := #[]
     for i in itemStxs do
-      let (b, item) ← elabDesc i
+      let (b, term, desc) ← elabDesc i
       colons := colons.push b
-      items := items.push item
+      items := items.push (term, desc)
     let info := DocListInfo.mk colons itemStxs
     for b in colons do
       pushInfoLeaf <| .ofCustomInfo {stx := b, value := Dynamic.mk info}
-    ``(Block.dl (genre := $(⟨genre⟩)) #[$[$items],*])
+    return .dl items
   | _ =>
     throwUnsupportedSyntax
 
-@[block_expander Lean.Doc.Syntax.blockquote]
-public meta def _root_.Lean.Doc.Syntax.blockquote.expand : BlockExpander
+@[block_elab Lean.Doc.Syntax.blockquote]
+public meta def _root_.Lean.Doc.Syntax.blockquote.expand : BlockElab
   | `(block|> $innerBlocks*) => do
-    ``(Block.blockquote #[$[$(← innerBlocks.mapM elabBlock)],*])
+    return .blockquote (← innerBlocks.mapM elabBlock')
   | _ =>
     throwUnsupportedSyntax
 
 
-@[block_expander Lean.Doc.Syntax.codeblock]
-public meta def _root_.Lean.Doc.Syntax.codeblock.expand : BlockExpander
+@[block_elab Lean.Doc.Syntax.codeblock]
+public meta def _root_.Lean.Doc.Syntax.codeblock.expand : BlockElab
   | `(block|``` $nameStx:ident $argsStx* | $contents:str ```) => do
-    let genre := (← readThe DocElabContext).genreSyntax
     let name ← realizeGlobalConstNoOverloadWithInfo nameStx
     let exp ← codeBlockExpandersFor name
     -- TODO typed syntax here
@@ -452,30 +441,29 @@ public meta def _root_.Lean.Doc.Syntax.codeblock.expand : BlockExpander
       try
         let termStxs ← withFreshMacroScope <| e args contents
         expanderDocHover nameStx "Code block" name doc? sig?
-        return (← ``(Block.concat (genre := $(⟨genre⟩)) #[$[$termStxs],*]))
+        return .concat (termStxs.map .stx)
       catch
         | ex@(.internal id) =>
           if id == unsupportedSyntaxExceptionId then pure ()
           else throw ex
         | ex => throw ex
     throwUnsupportedSyntax
-  | `(block|``` | $contents:str ```) => do
-    ``(Block.code $(quote contents.getString))
+  | `(block|``` | $contents:str ```) =>
+    pure <| .code contents.getString
   | _ =>
     throwUnsupportedSyntax
 
-@[block_expander Lean.Doc.Syntax.directive]
-public meta def _root_.Lean.Doc.Syntax.directive.expand : BlockExpander
+@[block_elab Lean.Doc.Syntax.directive]
+public meta def _root_.Lean.Doc.Syntax.directive.expand : BlockElab
   | `(block| ::: $nameStx:ident $argsStx* { $contents:block* } ) => do
-    let genre := (← readThe DocElabContext).genreSyntax
     let name ← realizeGlobalConstNoOverloadWithInfo nameStx
     let exp ← directiveExpandersFor name
     let args ← parseArgs argsStx
     for (e, doc?, sig?) in exp do
       try
         let termStxs ← withFreshMacroScope <| e args contents
         expanderDocHover nameStx "Directive" name doc? sig?
-        return (← ``(Block.concat (genre := $(⟨genre⟩)) #[$[$termStxs],*]))
+        return .concat (termStxs.map .stx)
       catch
         | ex@(.internal id) =>
           if id == unsupportedSyntaxExceptionId then pure ()