diff --git a/doc/UsersGuide/Basic.lean b/doc/UsersGuide/Basic.lean
index a45f572ed..550896477 100644
--- a/doc/UsersGuide/Basic.lean
+++ b/doc/UsersGuide/Basic.lean
@@ -1,7 +1,7 @@
import VersoManual
import UsersGuide.Markup
-open Verso.Genre Manual
+open Verso.Genre Manual InlineLean
set_option pp.rawOnError true
@@ -42,7 +42,68 @@ All genres use the same markup syntax, and they can share extensions to the mark
Mixing incompatible features results in an ordinary Lean type error.
:::
-# Docstrings
+# The Manual Genre
+
+## Tables
+
+Tables can be written using the `table` directive.
+```
+:::table
+* * 1, 1
+ * 1, 2
+* * 2, 1
+ * 2, 2
+* * 3, 1
+ * 3, 2
+:::
+```
+produces
+:::table
+* * 1, 1
+ * 1, 2
+* * 2, 1
+ * 2, 2
+* * 3, 1
+ * 3, 2
+:::
+
+## Inline Lean Code
+
+The namespace `Verso.Genre.Manual.InlineLean` contains the `lean` code block:
+
+````
+```lean (name := twoPlusTwo)
+#check 2 + 2
+```
+````
+results in
+```lean (name := twoPlusTwo)
+#check 2 + 2
+```
+
+and
+
+````
+```leanOutput (name := twoPlusTwo)
+#check 2 + 2
+```
+````
+
+results in
+
+````
+```leanOutput twoPlusTwo
+2 + 2 : Nat
+```
+````
+results in
+```leanOutput twoPlusTwo
+2 + 2 : Nat
+```
+
+
+
+## Docstrings
%%%
tag := "docstrings"
%%%
@@ -57,7 +118,7 @@ results in
{docstring List.forM}
-## More Docstring Examples
+### More Docstring Examples
%%%
shortTitle := "More Docstrings"
%%%
@@ -96,7 +157,7 @@ They include heuristic elaboration of code items in their Markdown that attempts
{docstring Thunk}
-# Technical Terminology
+## Technical Terminology
%%%
shortTitle := "Glossary"
tag := "tech-terms"
diff --git a/examples/textbook/DemoTextbook/Meta/Lean.lean b/examples/textbook/DemoTextbook/Meta/Lean.lean
index b6081e137..43510408b 100644
--- a/examples/textbook/DemoTextbook/Meta/Lean.lean
+++ b/examples/textbook/DemoTextbook/Meta/Lean.lean
@@ -8,8 +8,9 @@ import VersoManual
open Verso.Genre Manual
open Verso.Doc Elab
+open DocElabM
open Verso.ArgParse
-open Lean
+open Lean Meta
namespace DemoTextbook
@@ -32,11 +33,14 @@ block_extension Block.savedImport (file : String) (source : String) where
/--
Lean code that is saved to the examples file.
-/
-@[code_block_expander savedLean]
-def savedLean : CodeBlockExpander
+@[code_block_elab savedLean]
+def savedLean : CodeBlockElab
| args, code => do
let underlying ← InlineLean.lean args code
- return #[← ``(Block.other (Block.savedLean $(quote (← getFileName)) $(quote (code.getString))) #[$underlying,*])]
+ let g ← genreExpr
+ let b := mkApp2 (.const ``Block.savedLean []) (toExpr (← getFileName)) (toExpr code.getString)
+ return mkApp3 (.const ``Block.other []) g b (← mkArrayLit (← blockType) [underlying])
+
/--
An import of some other module, to be located in the saved code. Not rendered.
diff --git a/src/multi-verso/MultiVerso/Slug.lean b/src/multi-verso/MultiVerso/Slug.lean
index 84e7ad60a..babde2728 100644
--- a/src/multi-verso/MultiVerso/Slug.lean
+++ b/src/multi-verso/MultiVerso/Slug.lean
@@ -10,7 +10,7 @@ set_option linter.missingDocs true
namespace Verso.Multi
open Verso.Method
-open Lean (ToJson FromJson)
+open Lean (ToJson FromJson ToExpr)
open Std (HashSet)
/-- The characters allowed in slugs. -/
@@ -71,7 +71,7 @@ theorem String.Pos.add_0_eq_size {c : Char} : (0 : String.Pos) + c = ⟨c.utf8Si
show 0 + c.utf8Size = c.utf8Size
simp
-instance : DecidablePred Slug.WF := fun str =>
+instance Slug.WF.decide : DecidablePred Slug.WF := fun str =>
if h : str.toList.all (· ∈ Slug.validChars) then isTrue (by unfold Slug.WF; exact h) else isFalse h
@[simp]
@@ -172,6 +172,11 @@ Converts a string to a slug.
-/
def ofString (str : String) : Slug := str.sluggify
+/--
+Converts a string to a slug, performing no conversion because the string is already a valid slug.
+-/
+def ofString' (str : String) (wf : WF str := by decide) : Slug := ⟨str, wf⟩
+
/--
Returns a slug that's not present in `used`, starting with `slug` and appending consecutive numbers
until it becomes unique.
diff --git a/src/verso-manual/VersoManual.lean b/src/verso-manual/VersoManual.lean
index cc93e73b3..f7fd2ca9f 100644
--- a/src/verso-manual/VersoManual.lean
+++ b/src/verso-manual/VersoManual.lean
@@ -148,12 +148,14 @@ block_extension Block.paragraph where
some <| fun _ go _ _ content => do
pure <| {{{{← content.mapM go}}
}}
-@[directive_expander paragraph]
-def paragraph : DirectiveExpander
+open Lean.Meta in
+@[directive_elab paragraph]
+def paragraph : DirectiveElab
| #[], stxs => do
- let args ← stxs.mapM elabBlock
- let val ← ``(Block.other Block.paragraph #[ $[ $args ],* ])
- pure #[val]
+ let g ← DocElabM.genreExpr
+ let bt ← DocElabM.blockType
+ let args ← stxs.mapM elabBlock'
+ return Lean.mkApp3 (.const ``Block.other []) g (← mkAppM ``Block.paragraph #[]) (← mkArrayLit bt args.toList)
| _, _ => Lean.Elab.throwUnsupportedSyntax
diff --git a/src/verso-manual/VersoManual/Basic.lean b/src/verso-manual/VersoManual/Basic.lean
index 3a7dc896d..7509ed09a 100644
--- a/src/verso-manual/VersoManual/Basic.lean
+++ b/src/verso-manual/VersoManual/Basic.lean
@@ -16,7 +16,9 @@ import Verso.Output.Html
import Verso.Output.TeX
import Verso.BEq
-open Lean (Name Json NameMap ToJson FromJson)
+open Lean (Name Json NameMap ToJson FromJson ToExpr Expr)
+open Lean.ToExpr
+open Lean.Meta
open Std (HashSet HashMap TreeSet)
open Verso.Doc
open Verso.Multi
@@ -59,7 +61,17 @@ instance : ToString Tag where
instance : Coe String Tag where
coe := .provided
-
+def Tag.toExpr (tag : Tag) : MetaM Expr := do
+ match tag with
+ | .provided x => return Expr.app (.const ``Tag.provided []) (ToExpr.toExpr x)
+ | Tag.internal x => return Expr.app (.const ``Tag.internal []) (ToExpr.toExpr x)
+ | Tag.external x =>
+ let str := ToExpr.toExpr x.toString
+ let p := Expr.app (.const ``Slug.WF []) str
+ -- Should always succeed; we just need to run this due to type erasure
+ let prf ← mkDecideProof p
+ let slug := Lean.mkApp2 (.const ``Slug.ofString' []) str prf
+ return Expr.app (.const ``Tag.external []) slug
/-- When rendering multi-page HTML, should splitting pages follow the depth setting? -/
inductive HtmlSplitMode where
diff --git a/src/verso-manual/VersoManual/Docstring.lean b/src/verso-manual/VersoManual/Docstring.lean
index c0a6b5c6c..85c8bfe01 100644
--- a/src/verso-manual/VersoManual/Docstring.lean
+++ b/src/verso-manual/VersoManual/Docstring.lean
@@ -8,6 +8,7 @@ import Std.Data.HashSet
import VersoManual.Basic
import VersoManual.HighlightedCode
import VersoManual.Index
+import VersoManual.InlineLean.Env
import VersoManual.Markdown
import VersoManual.Docstring.Config
import VersoManual.Docstring.Progress
@@ -84,7 +85,7 @@ structure Signature where
wide : Highlighted
/-- The signature formatted for narrower screens, such as mobile displays -/
narrow : Highlighted
-deriving ToJson, FromJson, Quote
+deriving ToJson, FromJson, Quote, ToExpr
namespace Block
@@ -174,17 +175,20 @@ def ppSignature (c : Name) (showNamespace : Bool := true) (openDecls : List Open
return ⟨← ppTerm ⟨stx⟩, infos⟩ -- HACK: not a term
+deriving instance ToExpr for BinderInfo
+deriving instance ToExpr for DefinitionSafety
+deriving instance ToExpr for QuotKind
structure DocName where
name : Name
hlName : Highlighted
signature : Highlighted
docstring? : Option String
-deriving ToJson, FromJson, Repr, Quote
+deriving ToJson, FromJson, Repr, Quote, ToExpr
inductive Visibility where
| «public» | «private» | «protected»
-deriving Inhabited, Repr, ToJson, FromJson, DecidableEq, Ord, Quote
+deriving Inhabited, Repr, ToJson, FromJson, DecidableEq, Ord, Quote, ToExpr
def Visibility.of (env : Environment) (n : Name) : Visibility :=
if isPrivateName n then .private else if isProtected env n then .protected else .public
@@ -204,7 +208,7 @@ structure FieldInfo where
autoParam : Bool
docString? : Option String
visibility : Visibility
-deriving Inhabited, Repr, ToJson, FromJson, Quote
+deriving Inhabited, Repr, ToJson, FromJson, Quote, ToExpr
structure ParentInfo where
@@ -212,7 +216,7 @@ structure ParentInfo where
name : Name
parent : Highlighted
index : Nat
-deriving ToJson, FromJson, Quote
+deriving ToJson, FromJson, Quote, ToExpr
inductive DeclType where
/--
@@ -228,7 +232,7 @@ inductive DeclType where
| recursor (safety : DefinitionSafety)
| quotPrim (kind : QuotKind)
| other
-deriving ToJson, FromJson, Quote
+deriving ToJson, FromJson, Quote, ToExpr
def DeclType.label : DeclType → String
| .structure false .. => "structure"
@@ -1009,26 +1013,34 @@ def tryElabCodeMetavarTermWith (mk : Highlighted → String → DocElabM α) (st
else
throwError "Not a doc metavar: {stx}"
+private def asInline (hl : Highlighted) : DocElabM Expr := do
+ let g ← DocElabM.genreExpr
+ let arr ← Meta.mkArrayLit (.app (.const ``Doc.Inline []) g) [mkApp2 (.const ``Doc.Inline.code []) g (toExpr hl.toString)]
+ return mkApp3 (.const ``Doc.Inline.other []) g (.app (.const ``Inline.leanFromMarkdown []) (toExpr hl)) arr
+
+private def asBlock (hl : Highlighted) : DocElabM Expr := do
+ let g ← DocElabM.genreExpr
+ let arr ← Meta.mkArrayLit (.app (.const ``Doc.Block []) g) [mkApp2 (.const ``Doc.Block.code []) g (toExpr hl.toString)]
+ return mkApp3 (.const ``Doc.Block.other []) g (.app (.const ``Block.leanFromMarkdown []) (toExpr hl)) arr
+
+
open Lean Elab Term in
-def tryElabInlineCodeTerm (str : String) (ignoreElabErrors := false) (identOnly := false) : DocElabM Term :=
- tryElabCodeTermWith (ignoreElabErrors := ignoreElabErrors) (identOnly := identOnly) (fun hls str =>
- ``(Verso.Doc.Inline.other (Inline.leanFromMarkdown $(quote hls)) #[Verso.Doc.Inline.code $(quote str)]))
+def tryElabInlineCodeTerm (str : String) (ignoreElabErrors := false) (identOnly := false) : DocElabM Expr :=
+ tryElabCodeTermWith (ignoreElabErrors := ignoreElabErrors) (identOnly := identOnly) (fun hls _ => asInline hls)
str
open Lean Elab Term in
-def tryElabInlineCodeMetavarTerm (str : String) (ignoreElabErrors := false) : DocElabM Term :=
- tryElabCodeMetavarTermWith (ignoreElabErrors := ignoreElabErrors) (fun hls str =>
- ``(Verso.Doc.Inline.other (Inline.leanFromMarkdown $(quote hls)) #[Verso.Doc.Inline.code $(quote str)]))
+def tryElabInlineCodeMetavarTerm (str : String) (ignoreElabErrors := false) : DocElabM Expr :=
+ tryElabCodeMetavarTermWith (ignoreElabErrors := ignoreElabErrors) (fun hls _ => asInline hls)
str
open Lean Elab Term in
-def tryElabBlockCodeTerm (str : String) (ignoreElabErrors := false) : DocElabM Term :=
- tryElabCodeTermWith (ignoreElabErrors := ignoreElabErrors) (fun hls str =>
- ``(Verso.Doc.Block.other (Block.leanFromMarkdown $(quote hls)) #[Verso.Doc.Block.code $(quote str)]))
+def tryElabBlockCodeTerm (str : String) (ignoreElabErrors := false) : DocElabM Expr :=
+ tryElabCodeTermWith (ignoreElabErrors := ignoreElabErrors) (fun hls _ => asBlock hls)
str
open Lean Elab Term in
-def tryParseInlineCodeTactic (str : String) : DocElabM Term := do
+def tryParseInlineCodeTactic (str : String) : DocElabM Expr := do
let loc := (← getRef).getPos?.map (← getFileMap).utf8PosToLspPos
let src :=
if let some ⟨line, col⟩ := loc then s!""
@@ -1038,25 +1050,22 @@ def tryParseInlineCodeTactic (str : String) : DocElabM Term := do
| .ok stx => DocElabM.withFileMap (.ofString str) <| do
-- TODO try actually running the tactic - if the parameters are simple enough, then it may work
-- and give better highlights
- let hls ← highlight stx #[] (PersistentArray.empty)
- ``(Verso.Doc.Inline.other (Inline.leanFromMarkdown $(quote hls)) #[Verso.Doc.Inline.code $(quote str)])
+ asInline =<< highlight stx #[] (PersistentArray.empty)
open Lean Elab Term in
-def tryInlineOption (str : String) : DocElabM Term := do
+def tryInlineOption (str : String) : DocElabM Expr := do
let optName := str.trim.toName
let optDecl ← getOptionDecl optName
- let hl : Highlighted := optTok optName optDecl.declName optDecl.descr
- ``(Verso.Doc.Inline.other (Inline.leanFromMarkdown $(quote hl)) #[Verso.Doc.Inline.code $(quote str)])
+ asInline <| optTok optName optDecl.declName optDecl.descr
where
optTok (name declName : Name) (descr : String) : Highlighted :=
.token ⟨.option name declName descr, name.toString⟩
open Lean Elab in
-def tryTacticName (tactics : Array Tactic.Doc.TacticDoc) (str : String) : DocElabM Term := do
+def tryTacticName (tactics : Array Tactic.Doc.TacticDoc) (str : String) : DocElabM Expr := do
for t in tactics do
if t.userName == str then
- let hl : Highlighted := tacToken t
- return ← ``(Verso.Doc.Inline.other (Inline.leanFromMarkdown $(quote hl)) #[Verso.Doc.Inline.code $(quote str)])
+ return ← asInline <| tacToken t
throwError "Not a tactic name: {str}"
where
tacToken (t : Lean.Elab.Tactic.Doc.TacticDoc) : Highlighted :=
@@ -1064,7 +1073,7 @@ where
open Lean Elab Term in
open Lean.Parser in
-def tryHighlightKeywords (extraKeywords : Array String) (str : String) : DocElabM Term := do
+def tryHighlightKeywords (extraKeywords : Array String) (str : String) : DocElabM Expr := do
let loc := (← getRef).getPos?.map (← getFileMap).utf8PosToLspPos
let src :=
if let some ⟨line, col⟩ := loc then s!""
@@ -1073,8 +1082,7 @@ def tryHighlightKeywords (extraKeywords : Array String) (str : String) : DocElab
match runParser extraKeywords (← getEnv) (← getOptions) p str src (prec := 0) with
| .error _e => throwError "Not keyword-highlightable"
| .ok stx => DocElabM.withFileMap (.ofString str) <| do
- let hls ← highlight stx #[] (PersistentArray.empty)
- ``(Verso.Doc.Inline.other (Inline.leanFromMarkdown $(quote hls)) #[Verso.Doc.Inline.code $(quote str)])
+ asInline =<< highlight stx #[] (PersistentArray.empty)
where
simpleFn := andthenFn whitespace <| nodeFn nullKind <| manyFn tokenFn
@@ -1111,7 +1119,7 @@ private def getAttr : Syntax → Syntax
| _ => .missing
open Lean Elab Term in
-def tryParseInlineCodeAttribute (validate := true) (str : String) : DocElabM Term := do
+def tryParseInlineCodeAttribute (validate := true) (str : String) : DocElabM Expr := do
let loc := (← getRef).getPos?.map (← getFileMap).utf8PosToLspPos
let src :=
if let some ⟨line, col⟩ := loc then s!""
@@ -1131,11 +1139,9 @@ def tryParseInlineCodeAttribute (validate := true) (str : String) : DocElabM Ter
match getAttributeImpl (← getEnv) attrName with
| .error e => throwError e
| .ok _ =>
- let hls ← highlight stx #[] (PersistentArray.empty)
- ``(Verso.Doc.Inline.other (Inline.leanFromMarkdown $(quote hls)) #[Verso.Doc.Inline.code $(quote str)])
+ asInline =<< highlight stx #[] (PersistentArray.empty)
else
- let hls ← highlight stx #[] (PersistentArray.empty)
- ``(Verso.Doc.Inline.other (Inline.leanFromMarkdown $(quote hls)) #[Verso.Doc.Inline.code $(quote str)])
+ asInline =<< highlight stx #[] (PersistentArray.empty)
private def indentColumn (str : String) : Nat := Id.run do
@@ -1168,7 +1174,7 @@ private def indentColumn (str : String) : Nat := Id.run do
#eval indentColumn " abc\n\n def\n a"
open Lean Elab Term in
-def tryElabBlockCodeCommand (str : String) (ignoreElabErrors := false) : DocElabM Term := do
+def tryElabBlockCodeCommand (str : String) (ignoreElabErrors := false) : DocElabM Expr := do
let loc := (← getRef).getPos?.map (← getFileMap).utf8PosToLspPos
let src :=
if let some ⟨line, col⟩ := loc then s!""
@@ -1201,24 +1207,22 @@ def tryElabBlockCodeCommand (str : String) (ignoreElabErrors := false) : DocElab
if cmdState.messages.hasErrors then
throwError "Errors found in command"
- let hls ← DocElabM.withFileMap (.ofString str) do
+ DocElabM.withFileMap (.ofString str) do
let mut hls := Highlighted.empty
for cmd in cmds do
hls := hls ++ (← highlight cmd cmdState.messages.toArray cmdState.infoState.trees)
- pure <| hls.deIndent (indentColumn str)
+ asBlock <| hls.deIndent (indentColumn str)
- ``(Verso.Doc.Block.other (Block.leanFromMarkdown $(quote hls)) #[Verso.Doc.Block.code $(quote str)])
open Lean Elab Term in
-def tryElabInlineCodeName (str : String) : DocElabM Term := do
+def tryElabInlineCodeName (str : String) : DocElabM Expr := do
let str := str.trim
let x := str.toName
if x.toString == str then
let stx := mkIdent x
let n ← realizeGlobalConstNoOverload stx
- let hl : Highlighted ← constTok n str
- ``(Verso.Doc.Inline.other (Inline.leanFromMarkdown $(quote hl)) #[Verso.Doc.Inline.code $(quote str)])
+ asInline =<< constTok n str
else
throwError "Not a name: '{str}'"
where
@@ -1248,22 +1252,24 @@ private def attempt (str : String) (xs : List (String → DocElabM α)) : DocEla
open Lean Elab Term in
-def tryElabInlineCodeUsing (elabs : List (String → DocElabM Term))
- (priorWord : Option String) (str : String) : DocElabM Term := do
+def tryElabInlineCodeUsing (elabs : List (String → DocElabM Expr))
+ (priorWord : Option String) (str : String) : DocElabM Expr := do
+ let g ← DocElabM.genreExpr
-- Don't try to show Lake commands as terms
- if "lake ".isPrefixOf str then return (← ``(Verso.Doc.Inline.code $(quote str)))
+ let code := mkApp2 (.const ``Verso.Doc.Inline.code []) g (toExpr str)
+ if "lake ".isPrefixOf str then return code
try
attempt str <| wordElab priorWord ++ elabs
catch
| .error ref e =>
logWarningAt ref e
- ``(Verso.Doc.Inline.code $(quote str))
+ return code
| e =>
if isAutoBoundImplicitLocalException? e |>.isSome then
throw e
else
logWarning m!"Internal exception uncaught: {e.toMessageData}"
- ``(Verso.Doc.Inline.code $(quote str))
+ return code
where
wordElab
| some "attribute" => [tryParseInlineCodeAttribute (validate := false)]
@@ -1272,7 +1278,7 @@ where
open Elab in
def tryElabInlineCode (allTactics : Array Tactic.Doc.TacticDoc) (extraKeywords : Array String)
- (priorWord : Option String) (str : String) : DocElabM Term :=
+ (priorWord : Option String) (str : String) : DocElabM Expr :=
tryElabInlineCodeUsing [
tryElabInlineCodeName,
-- When identifiers have the same name as tactics, prefer the identifiers
@@ -1295,7 +1301,7 @@ displaying metavariable-typed terms (e.g., through auto-bound implicits or
elaboration failures).
-/
def tryElabInlineCodeStrict (allTactics : Array Tactic.Doc.TacticDoc) (extraKeywords : Array String)
- (priorWord : Option String) (str : String) : DocElabM Term :=
+ (priorWord : Option String) (str : String) : DocElabM Expr :=
tryElabInlineCodeUsing [
tryElabInlineCodeName,
-- When identifiers have the same name as tactics, prefer the identifiers
@@ -1310,25 +1316,28 @@ def tryElabInlineCodeStrict (allTactics : Array Tactic.Doc.TacticDoc) (extraKeyw
] priorWord str
open Lean Elab Term in
-def tryElabBlockCode (_info? _lang? : Option String) (str : String) : DocElabM Term := do
+def tryElabBlockCode (_info? _lang? : Option String) (str : String) : DocElabM Expr := do
+ let g ← DocElabM.genreExpr
+ let code := mkApp2 (.const ``Verso.Doc.Block.code []) g (mkStrLit str)
try
attempt str [
- tryElabBlockCodeCommand,
- tryElabBlockCodeTerm,
- tryElabBlockCodeCommand (ignoreElabErrors := true),
- withTheReader Term.Context (fun ctx => {ctx with autoBoundImplicit := true}) ∘
- tryElabBlockCodeTerm (ignoreElabErrors := true)
- ]
+ tryElabBlockCodeCommand,
+ tryElabBlockCodeTerm,
+ tryElabBlockCodeCommand (ignoreElabErrors := true),
+ withTheReader Term.Context (fun ctx => {ctx with autoBoundImplicit := true}) ∘
+ tryElabBlockCodeTerm (ignoreElabErrors := true)
+ ]
+
catch
| .error ref e =>
logWarningAt ref e
- ``(Verso.Doc.Block.code $(quote str))
+ return code
| e =>
if isAutoBoundImplicitLocalException? e |>.isSome then
throw e
else
logWarning m!"Internal exception uncaught: {e.toMessageData}"
- ``(Verso.Doc.Block.code $(quote str))
+ return code
open Lean Elab Term in
/--
@@ -1336,9 +1345,10 @@ Heuristically elaborate Lean fragments in Markdown code. The provided names are
from left to right, with the names bound by the signature being available in the local scope in
which the Lean fragments are elaborated.
-/
-def blockFromMarkdownWithLean (names : List Name) (b : MD4Lean.Block) : DocElabM Term := do
+def blockFromMarkdownWithLean (names : List Name) (b : MD4Lean.Block) : DocElabM Expr := do
+ let g ← DocElabM.genreExpr
unless (← Docstring.getElabMarkdown) do
- return (← Markdown.blockFromMarkdown b (handleHeaders := Markdown.strongEmphHeaders))
+ return (← Markdown.blockFromMarkdown'' g b (handleHeaders := Markdown.strongEmphHeaders'' g))
let tactics ← Elab.Tactic.Doc.allTacticDocs
let keywords := tactics.map (·.userName)
try
@@ -1349,13 +1359,13 @@ def blockFromMarkdownWithLean (names : List Name) (b : MD4Lean.Block) : DocElabM
blockFromMarkdownWithLean decls b
| [] =>
-- It'd be silly for some weird edge case to block on this feature...
- let rec loop (max : Nat) (s : SavedState) : DocElabM Term := do
+ let rec loop (max : Nat) (s : SavedState) : DocElabM Expr := do
match max with
| k + 1 =>
try
let res ←
- Markdown.blockFromMarkdown b
- (handleHeaders := Markdown.strongEmphHeaders)
+ Markdown.blockFromMarkdown'' g b
+ (handleHeaders := Markdown.strongEmphHeaders'' g)
(elabInlineCode := tryElabInlineCode tactics keywords)
(elabBlockCode := tryElabBlockCode)
synthesizeSyntheticMVarsUsingDefault
@@ -1377,8 +1387,60 @@ def blockFromMarkdownWithLean (names : List Name) (b : MD4Lean.Block) : DocElabM
finally
(s.restore : TermElabM _)
catch _ =>
- Markdown.blockFromMarkdown b
- (handleHeaders := Markdown.strongEmphHeaders)
+ Markdown.blockFromMarkdown'' g b
+ (handleHeaders := Markdown.strongEmphHeaders'' g)
+
+open Lean Elab Term in
+/--
+Heuristically elaborate Lean fragments in Markdown code. The provided names are used as signatures,
+from left to right, with the names bound by the signature being available in the local scope in
+which the Lean fragments are elaborated.
+-/
+-- TODO: replace Term version completely
+def blockFromMarkdownWithLean' (names : List Name) (b : MD4Lean.Block) : DocElabM Expr := do
+ let g ← DocElabM.genreExpr
+ unless (← Docstring.getElabMarkdown) do
+ return (← Markdown.blockFromMarkdown'' g b (handleHeaders := Markdown.strongEmphHeaders'' g))
+ let tactics ← Elab.Tactic.Doc.allTacticDocs
+ let keywords := tactics.map (·.userName)
+ try
+ match names with
+ | decl :: decls =>
+ -- This brings the parameters into scope, so the term elaboration version catches them!
+ Meta.forallTelescopeReducing (← getConstInfo decl).type fun _ _ =>
+ blockFromMarkdownWithLean' decls b
+ | [] =>
+ -- It'd be silly for some weird edge case to block on this feature...
+ let rec loop (max : Nat) (s : SavedState) : DocElabM Expr := do
+ match max with
+ | k + 1 =>
+ try
+ let res ←
+ Markdown.blockFromMarkdown'' g b
+ (handleHeaders := Markdown.strongEmphHeaders'' g)
+ (elabInlineCode := tryElabInlineCode tactics keywords)
+ (elabBlockCode := tryElabBlockCode)
+ synthesizeSyntheticMVarsUsingDefault
+
+ discard <| addAutoBoundImplicits #[] (inlayHintPos? := none)
+
+ return res
+ catch e =>
+ if let some n := isAutoBoundImplicitLocalException? e then
+ s.restore (restoreInfo := true)
+ Meta.withLocalDecl n .implicit (← Meta.mkFreshTypeMVar) fun x =>
+ withTheReader Term.Context (fun ctx => { ctx with autoBoundImplicits := ctx.autoBoundImplicits.push x } ) do
+ loop k (← (saveState : TermElabM _))
+ else throw e
+ | 0 => throwError "Ran out of local name attempts"
+ let s ← (saveState : TermElabM _)
+ try
+ loop 40 s
+ finally
+ (s.restore : TermElabM _)
+ catch _ =>
+ Markdown.blockFromMarkdown'' g b
+ (handleHeaders := Markdown.strongEmphHeaders'' g)
structure DocstringConfig where
name : Ident × Name
@@ -1407,9 +1469,12 @@ def DocstringConfig.parse : ArgParse m DocstringConfig :=
end
-@[block_role_expander docstring]
-def docstring : BlockRoleExpander
+open DocElabM in
+open Meta in
+@[block_role_elab docstring]
+def docstring : BlockRoleElab
| args, #[] => do
+ let g ← DocElabM.genreExpr
let ⟨(x, name), allowMissing, hideFields, hideCtor, customLabel⟩ ← DocstringConfig.parse.run args
let opts : Options → Options := allowMissing.map (fun b opts => verso.docstring.allowMissing.set opts b) |>.getD id
@@ -1434,50 +1499,66 @@ def docstring : BlockRoleExpander
let signature ← Signature.forName name
let extras ← getExtras name declType
- pure #[← ``(Verso.Doc.Block.other (Verso.Genre.Manual.Block.docstring $(quote name) $(quote declType) $(quote signature) $(quote customLabel)) #[$(blockStx ++ extras),*])]
+ let docBlock := mkApp4 (.const ``Manual.Block.docstring []) (toExpr name) (toExpr declType) (toExpr signature) (toExpr customLabel)
+
+ return mkApp3 (.const ``Verso.Doc.Block.other []) g docBlock (← mkArrayLit (← blockType) (blockStx ++ extras).toList)
| _, more => throwErrorAt more[0]! "Unexpected block argument"
where
- getExtras (name : Name) (declType : Block.Docstring.DeclType) : DocElabM (Array Term) :=
+ getExtras (name : Name) (declType : Block.Docstring.DeclType) : DocElabM (Array Expr) := do
+ let g ← DocElabM.genreExpr
match declType with
| .structure isClass constructor? _ fieldInfo parents _ => do
- let ctorRow : Option Term ← constructor?.mapM fun constructor => do
+ let ctorRow : Option Expr ← constructor?.mapM fun constructor => do
let header := if isClass then "Instance Constructor" else "Constructor"
- let sigDesc : Array Term ←
+ let sigDesc : Array Expr ←
if let some docs := constructor.docstring? then
let some mdAst := MD4Lean.parse docs
| throwError "Failed to parse docstring as Markdown"
mdAst.blocks.mapM (blockFromMarkdownWithLean [name, constructor.name])
- else pure (#[] : Array Term)
- let sig ← `(Verso.Doc.Block.other (Verso.Genre.Manual.Block.internalSignature $(quote constructor.hlName) none) #[$sigDesc,*])
- ``(Verso.Doc.Block.other (Verso.Genre.Manual.Block.docstringSection $(quote header)) #[$sig])
+ else pure (#[] : Array Expr)
+ let sigBlk := mkApp2 (.const ``Block.internalSignature []) (toExpr constructor.hlName) (toExpr (none : Option Highlighted))
+ let sig := mkApp3 (.const ``Verso.Doc.Block.other []) g sigBlk (← Meta.mkArrayLit (← DocElabM.blockType) sigDesc.toList)
+ let sec := .app (.const ``Block.docstringSection []) (toExpr header)
+ return mkApp3 (.const ``Verso.Doc.Block.other []) g sec (← Meta.mkArrayLit (← DocElabM.blockType) [sig])
+
- let parentsRow : Option Term ← do
+ let parentsRow : Option Expr ← do
if parents.isEmpty then pure none
else
let header := "Extends"
- let inh ← ``(Verso.Doc.Block.other (Verso.Genre.Manual.Block.inheritance $(quote name) $(quote parents)) #[])
- some <$> ``(Verso.Doc.Block.other (Verso.Genre.Manual.Block.docstringSection $(quote header)) #[$inh])
+ let sec : Expr := .app (.const ``Block.docstringSection []) (toExpr header)
+ let inh := mkApp2 (.const ``Verso.Genre.Manual.Block.inheritance []) (toExpr name) (toExpr parents)
+ let inh := mkApp3 (.const ``Verso.Doc.Block.other []) g inh (← Meta.mkArrayLit (← DocElabM.blockType) [])
+ pure <| some <| mkApp3 (.const ``Verso.Doc.Block.other []) g sec (← Meta.mkArrayLit (← DocElabM.blockType) [inh])
- let fieldsRow : Option Term ← do
+
+ let fieldsRow : Option Expr ← do
let header := if isClass then "Methods" else "Fields"
let fieldInfo := fieldInfo.filter (·.subobject?.isNone)
- let fieldSigs : Array Term ← fieldInfo.mapM fun i => do
+ let fieldSigs : Array Expr ← fieldInfo.mapM fun i => do
let inheritedFrom : Option Nat :=
i.fieldFrom.head?.bind (fun n => parents.findIdx? (·.name == n.name))
- let sigDesc : Array Term ←
+ let sigDesc : Array Expr ←
if let some docs := i.docString? then
let some mdAst := MD4Lean.parse docs
| throwError "Failed to parse docstring as Markdown"
mdAst.blocks.mapM (blockFromMarkdownWithLean <| name :: (constructor?.map ([·.name])).getD [])
else
- pure (#[] : Array Term)
- ``(Verso.Doc.Block.other (Verso.Genre.Manual.Block.fieldSignature $(quote i.visibility) $(quote i.fieldName) $(quote i.type) $(quote inheritedFrom) $(quote <| parents.map (·.parent))) #[$sigDesc,*])
+ pure (#[] : Array Expr)
+
+ let fieldSig : Expr :=
+ mkApp5 (.const ``Verso.Genre.Manual.Block.fieldSignature [])
+ (toExpr i.visibility) (toExpr i.fieldName) (toExpr i.type) (toExpr inheritedFrom) (toExpr (parents.map (·.parent)))
+ return mkApp3 (.const ``Verso.Doc.Block.other []) g fieldSig (← Meta.mkArrayLit (← DocElabM.blockType) sigDesc.toList)
if fieldSigs.isEmpty then pure none
- else some <$> ``(Verso.Doc.Block.other (Verso.Genre.Manual.Block.docstringSection $(quote header)) #[$fieldSigs,*])
+ -- ``(Verso.Doc.Block.other (Verso.Genre.Manual.Block.docstringSection $(quote header)) #[$fieldSigs,*])
+ else
+ let sec := .app (.const ``Block.docstringSection []) (toExpr header)
+ pure <| some <| mkApp3 (.const ``Verso.Doc.Block.other []) g sec (← Meta.mkArrayLit (← DocElabM.blockType) fieldSigs.toList)
pure <| ctorRow.toArray ++ parentsRow.toArray ++ fieldsRow.toArray
| .inductive ctors .. => do
- let ctorSigs : Array Term ←
+ let ctorSigs : Array Expr ←
-- Elaborate constructor docs in the type's NS
ctors.mapM fun c => withTheReader Core.Context ({· with currNamespace := name}) do
let sigDesc ←
@@ -1485,9 +1566,12 @@ where
let some mdAst := MD4Lean.parse docs
| throwError "Failed to parse docstring as Markdown"
mdAst.blocks.mapM (blockFromMarkdownWithLean [name, c.name])
- else pure (#[] : Array Term)
- ``(Verso.Doc.Block.other (Verso.Genre.Manual.Block.constructorSignature $(quote c.signature)) #[$sigDesc,*])
- pure #[← ``(Verso.Doc.Block.other (Verso.Genre.Manual.Block.docstringSection "Constructors") #[$ctorSigs,*])]
+ else pure (#[] : Array Expr)
+ --``(Verso.Doc.Block.other (Verso.Genre.Manual.Block.constructorSignature $(quote c.signature)) #[$sigDesc,*])
+ let sig := .app (.const ``Block.constructorSignature []) (toExpr c.signature)
+ pure <| mkApp3 (.const ``Verso.Doc.Block.other []) g sig (← mkArrayLit (← blockType) sigDesc.toList)
+ let sec := .app (.const ``Block.docstringSection []) (toExpr "Constructors")
+ pure #[mkApp3 (.const ``Verso.Doc.Block.other []) g sec (← mkArrayLit (← blockType) ctorSigs.toList)]
| _ => pure #[]
section
@@ -1505,16 +1589,19 @@ def IncludeDocstringOpts.parse : ArgParse m IncludeDocstringOpts :=
end
-@[block_role_expander includeDocstring]
-def includeDocstring : BlockRoleExpander
+open DocElabM in
+open Meta in
+@[block_role_elab includeDocstring]
+def includeDocstring : BlockRoleElab
| args, #[] => do
+ let g ← DocElabM.genreExpr
let {name, elaborate} ← IncludeDocstringOpts.parse.run args
let fromMd :=
if elaborate then
blockFromMarkdownWithLean [name]
else
- Markdown.blockFromMarkdown (handleHeaders := Markdown.strongEmphHeaders)
+ Markdown.blockFromMarkdown'' g (handleHeaders := Markdown.strongEmphHeaders'' g)
let blockStx ←
match ← getDocString? (← getEnv) name with
@@ -1524,7 +1611,7 @@ def includeDocstring : BlockRoleExpander
| throwError "Failed to parse docstring as Markdown"
ast.blocks.mapM fromMd
- pure blockStx
+ pure <| mkApp2 (.const ``Verso.Doc.Block.concat []) g (← mkArrayLit (← blockType) blockStx.toList)
| _args, more => throwErrorAt more[0]! "Unexpected block argument"
@@ -1563,8 +1650,10 @@ def highlightDataValue (v : DataValue) : Highlighted :=
| .ofSyntax (v : Syntax) => ⟨.unknown, toString v⟩ -- TODO
-@[block_role_expander optionDocs]
-def optionDocs : BlockRoleExpander
+open DocElabM in
+open Meta in
+@[block_role_elab optionDocs]
+def optionDocs : BlockRoleElab
| args, #[] => do
let #[.anon (.name x)] := args
| throwError "Expected exactly one positional argument that is a name"
@@ -1573,7 +1662,9 @@ def optionDocs : BlockRoleExpander
let some mdAst := MD4Lean.parse optDecl.descr
| throwErrorAt x "Failed to parse docstring as Markdown"
let contents ← mdAst.blocks.mapM (blockFromMarkdownWithLean [])
- pure #[← ``(Verso.Doc.Block.other (Verso.Genre.Manual.Block.optionDocs $(quote x.getId) $(quote <| highlightDataValue optDecl.defValue)) #[$contents,*])]
+ let g ← genreExpr
+ let optDocs := mkApp2 (.const ``Block.optionDocs []) (toExpr x.getId) (toExpr <| some <| highlightDataValue optDecl.defValue)
+ return mkApp3 (.const ``Verso.Doc.Block.other []) g optDocs (← mkArrayLit (← blockType) contents.toList)
| _, more => throwErrorAt more[0]! "Unexpected block argument"
@@ -1672,11 +1763,21 @@ private def getTactic? (name : String ⊕ Name) : TermElabM (Option TacticDoc) :
return some t
return none
-@[directive_expander tactic]
-def tactic : DirectiveExpander
+
+instance : ToExpr NameSet where
+ toTypeExpr := .const ``NameSet []
+ toExpr xs :=
+ mkApp3 (.const ``RBTree.fromList [0]) (.const ``Name []) (toExpr xs.toList) (.const ``Name.quickCmp [])
+
+deriving instance ToExpr for Elab.Tactic.Doc.TacticDoc
+
+open DocElabM in
+open Meta in
+@[directive_elab tactic]
+def tactic : DirectiveElab
| args, more => do
let opts ← TacticDocsOptions.parse.run args
- let tactic ← getTactic opts.name
+ let tactic ← InlineLean.usingExamplesEnv <| getTactic opts.name
Doc.PointOfInterest.save (← getRef) tactic.userName
if tactic.userName == tactic.internalName.toString && opts.show.isNone then
throwError "No `show` option provided, but the tactic has no user-facing token name"
@@ -1686,8 +1787,11 @@ def tactic : DirectiveExpander
let some mdAst := tactic.docString >>= MD4Lean.parse
| throwError "Failed to parse docstring as Markdown"
mdAst.blocks.mapM (blockFromMarkdownWithLean [])
- let userContents ← more.mapM elabBlock
- pure #[← ``(Verso.Doc.Block.other (Block.tactic $(quote tactic) $(quote opts.show)) #[$(contents ++ userContents),*])]
+ let userContents ← more.mapM elabBlock'
+ let g ← genreExpr
+ let tac := mkApp2 (.const ``Block.tactic []) (toExpr tactic) (toExpr opts.show)
+ return mkApp3 (.const ``Verso.Doc.Block.other []) g tac (← mkArrayLit (← blockType) (contents ++ userContents).toList)
+ --pure #[← ``(Verso.Doc.Block.other (Block.tactic $(quote tactic) $(quote opts.show)) #[$(contents ++ userContents),*])]
@@ -1761,7 +1865,9 @@ def tacticInline : RoleExpander
| throwErrorAt arg "Expected code literal with the tactic name"
let tacTok := tac.getString
let tacName := tac.getString.toName
- let some tacticDoc := (← getTactic? (.inl tacTok)) <|> (← getTactic? (.inr tacName))
+ let some tacticDoc :=
+ (← InlineLean.usingExamplesEnv <| getTactic? (.inl tacTok)) <|>
+ (← InlineLean.usingExamplesEnv <| getTactic? (.inr tacName))
| throwErrorAt tac "Didn't find tactic named {tac}"
let hl : Highlighted := tacToken tacticDoc «show»
@@ -1814,8 +1920,10 @@ def getConvTactic (name : String ⊕ Name) (allowMissing : Option Bool) : TermEl
return ⟨k, ← getDocString? (← getEnv) k⟩
throwError m!"Conv tactic not found: {kind}"
-@[directive_expander conv]
-def conv : DirectiveExpander
+open DocElabM in
+open Meta in
+@[directive_elab conv]
+def conv : DirectiveElab
| args, more => do
let opts ← TacticDocsOptions.parse.run args
let tactic ← getConvTactic opts.name opts.allowMissing
@@ -1825,10 +1933,13 @@ def conv : DirectiveExpander
| throwError "Failed to parse docstring as Markdown"
mdAst.blocks.mapM (blockFromMarkdownWithLean [])
else pure #[]
- let userContents ← more.mapM elabBlock
+ let userContents ← more.mapM elabBlock'
let some toShow := opts.show
| throwError "An explicit 'show' is mandatory for conv docs (for now)"
- pure #[← ``(Verso.Doc.Block.other (Block.conv $(quote tactic.name) $(quote toShow) $(quote tactic.docs?)) #[$(contents ++ userContents),*])]
+ let g ← genreExpr
+ let blk := mkApp3 (.const ``Block.conv []) (toExpr tactic.name) (toExpr toShow) (toExpr tactic.docs?)
+ return mkApp3 (.const ``Verso.Doc.Block.other []) g blk (← mkArrayLit (← blockType) (contents ++ userContents).toList)
+
open Verso.Genre.Manual.Markdown in
open Lean Elab Term Parser Tactic Doc in
diff --git a/src/verso-manual/VersoManual/InlineLean.lean b/src/verso-manual/VersoManual/InlineLean.lean
index 92079cdb8..afb2d4921 100644
--- a/src/verso-manual/VersoManual/InlineLean.lean
+++ b/src/verso-manual/VersoManual/InlineLean.lean
@@ -14,6 +14,7 @@ import Verso
import VersoManual.Basic
import VersoManual.InlineLean.Block
+import VersoManual.InlineLean.Env
import VersoManual.InlineLean.IO
import VersoManual.InlineLean.LongLines
import VersoManual.InlineLean.Option
@@ -23,8 +24,8 @@ import VersoManual.InlineLean.Signature
import VersoManual.InlineLean.SyntaxError
-open Lean Elab
-open Verso ArgParse Doc Elab Genre.Manual Html Code Highlighted.WebAssets ExpectString
+open Lean Elab Meta
+open Verso ArgParse Doc Elab Genre.Manual Html Code Highlighted.WebAssets ExpectString DocElabM
open SubVerso.Highlighting Highlighted
open Verso.SyntaxUtils (parserInputString runParserCategory' SyntaxError)
@@ -33,6 +34,8 @@ open Lean.Elab.Tactic.GuardMsgs
namespace Verso.Genre.Manual.InlineLean
+
+
inline_extension Inline.lean (hls : Highlighted) where
data :=
let defined := hls.definedNames.toArray
@@ -162,12 +165,15 @@ def reportMessages {m} [Monad m] [MonadLog m] [MonadError m]
if messages.hasErrors then
throwErrorAt blame "No error expected in code block, one occurred"
+deriving instance ToExpr for Lsp.Position
+deriving instance ToExpr for Lsp.Range
+
/--
Elaborates the provided Lean command in the context of the current Verso module.
-/
-@[code_block_expander lean]
-def lean : CodeBlockExpander
- | args, str => withoutAsync <| do
+@[code_block_elab lean]
+def lean : CodeBlockElab
+ | args, str => withoutAsync <| usingExamplesEnv do
let config ← LeanBlockConfig.parse.run args
PointOfInterest.save (← getRef) ((config.name.map (·.toString)).getD (abbrevFirstLine 20 str.getString))
@@ -224,9 +230,14 @@ def lean : CodeBlockExpander
if config.show.getD true then
let range := Syntax.getRange? str
let range := range.map (← getFileMap).utf8RangeToLspRange
- pure #[← ``(Block.other (Block.lean $(quote hls) (some $(quote (← getFileName))) $(quote range)) #[Block.code $(quote str.getString)])]
+
+ let g ← genreExpr
+ let bt ← blockType
+ let leanBlock := mkApp3 (.const ``Block.lean []) (toExpr hls) (toExpr (some ((← getFileName) : System.FilePath))) (toExpr range)
+ let code := mkApp2 (.const ``Block.code []) g (toExpr str.getString)
+ pure <| mkApp3 (.const ``Block.other []) (← genreExpr) leanBlock (← mkArrayLit bt [code])
else
- pure #[]
+ emptyBlock
finally
if !config.keep.getD true then
setEnv origEnv
@@ -270,7 +281,7 @@ Elaborates the provided Lean term in the context of the current Verso module.
-/
@[code_block_expander leanTerm]
def leanTerm : CodeBlockExpander
- | args, str => withoutAsync <| do
+ | args, str => withoutAsync <| usingExamplesEnv do
let config ← LeanInlineConfig.parse.run args
let altStr ← parserInputString str
@@ -379,7 +390,7 @@ Elaborates the provided Lean term in the context of the current Verso module.
@[role_expander lean]
def leanInline : RoleExpander
-- Async elab is turned off to make sure that info trees and messages are available when highlighting
- | args, inlines => withoutAsync do
+ | args, inlines => withoutAsync <| usingExamplesEnv do
let config ← LeanInlineConfig.parse.run args
let #[arg] := inlines
| throwError "Expected exactly one argument"
@@ -496,7 +507,7 @@ Elaborates the provided term in the current Verso context, then ensures that it'
-/
@[role_expander inst]
def inst : RoleExpander
- | args, inlines => withoutAsync <| do
+ | args, inlines => withoutAsync <| usingExamplesEnv do
let config ← LeanBlockConfig.parse.run args
let #[arg] := inlines
| throwError "Expected exactly one argument"
@@ -639,11 +650,12 @@ where
end
+deriving instance ToExpr for MessageSeverity
open SubVerso.Examples.Messages in
-@[code_block_expander leanOutput]
-def leanOutput : CodeBlockExpander
- | args, str => do
+@[code_block_elab leanOutput]
+def leanOutput : CodeBlockElab
+ | args, str => usingExamplesEnv <| do
let config ← LeanOutputConfig.parser.run args
let col? := (← getRef).getPos? |>.map (← getFileMap).utf8PosToLspPos |>.map (·.character)
@@ -671,9 +683,16 @@ def leanOutput : CodeBlockExpander
if s != sev then
throwErrorAt str s!"Expected severity {sevStr s}, but got {sevStr sev}"
if config.show then
- let content ← `(Block.other {Block.leanOutput with data := ToJson.toJson ($(quote sev), $(quote txt), $(quote config.summarize))} #[Block.code $(quote str.getString)])
- return #[content]
- else return #[]
+ let ⟨name, _, _⟩ := Block.leanOutput
+ let name := toExpr name
+ let noId := .app (.const ``Option.none [0]) (.const ``InternalId [])
+ let data ← mkAppM ``Prod.mk #[toExpr sev, ← mkAppM ``Prod.mk #[toExpr txt, toExpr config.summarize]]
+ let data ← mkAppM ``ToJson.toJson #[data]
+ let out : Expr := mkApp3 (.const ``Manual.Block.mk []) name noId data
+ let g ← genreExpr
+ let codeBlock := mkApp2 (.const ``Block.code []) g (toExpr str.getString)
+ return mkApp3 (.const ``Block.other []) g out (← mkArrayLit (← blockType) [codeBlock])
+ else return (← emptyBlock)
else
let mut best : Option (Nat × String × MessageSeverity × String) := none
for (sev, txt) in msgs do
@@ -693,9 +712,17 @@ def leanOutput : CodeBlockExpander
Log.logSilentInfo m!"Diff is {d} lines:\n{d'}"
if config.show then
- let content ← `(Block.other {Block.leanOutput with data := ToJson.toJson ($(quote sev), $(quote txt), $(quote config.summarize))} #[Block.code $(quote str.getString)])
- return #[content]
- else return #[]
+
+ let ⟨name, _, _⟩ := Block.leanOutput
+ let name := toExpr name
+ let noId := .app (.const ``Option.none [0]) (.const ``InternalId [])
+ let data ← mkAppM ``Prod.mk #[toExpr sev, ← mkAppM ``Prod.mk #[toExpr txt, toExpr config.summarize]]
+ let data ← mkAppM ``ToJson.toJson #[data]
+ let out : Expr := mkApp3 (.const ``Manual.Block.mk []) name noId data
+ let g ← genreExpr
+ let codeBlock := mkApp2 (.const ``Block.code []) g (toExpr str.getString)
+ return mkApp3 (.const ``Block.other []) g out (← mkArrayLit (← blockType) [codeBlock])
+ else return (← emptyBlock)
for (_, m) in msgs do
let m := "".pushn ' ' (col?.getD 0) ++ if m.endsWith "\n" then m else m ++ "\n"
@@ -770,7 +797,7 @@ def constTok [Monad m] [MonadEnv m] [MonadLiftT MetaM m] [MonadLiftT IO m]
@[role_expander name]
def name : RoleExpander
- | args, #[arg] => do
+ | args, #[arg] => usingExamplesEnv do
let cfg ← NameConfig.parse.run args
let `(inline|code( $name:str )) := arg
| throwErrorAt arg "Expected code literal with the example name"
diff --git a/src/verso-manual/VersoManual/InlineLean/Env.lean b/src/verso-manual/VersoManual/InlineLean/Env.lean
new file mode 100644
index 000000000..c6c646d33
--- /dev/null
+++ b/src/verso-manual/VersoManual/InlineLean/Env.lean
@@ -0,0 +1,55 @@
+/-
+Copyright (c) 2025 Lean FRO LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: David Thrane Christiansen
+-/
+import Lean.Environment
+import Lean.Exception
+import Verso.Doc.Elab.Monad
+
+open Lean
+open Verso Doc Elab DocElabM
+
+namespace Verso.Genre.Manual.InlineLean
+
+def envParameter : Name := decl_name%
+
+variable [Monad m] [MonadError m] [MonadReaderOf DocElabContext m] [MonadWithReaderOf DocElabContext m]
+variable [MonadEnv m] [MonadFinally m] [MonadLiftT (ST IO.RealWorld) m] [MonadLiftT BaseIO m]
+
+structure EnvRef where
+ val : IO.Ref Environment
+
+deriving instance TypeName for EnvRef
+
+/--
+If a special examples environment is specified, use it.
+-/
+def usingExamplesEnv (act : m α) : m α := do
+ if let some (envRef : EnvRef) := (← parameterValue? envParameter) then
+ let env ← envRef.val.get
+ let realEnv ← getEnv
+ try
+ modifyEnv (fun _ => env)
+ try
+ act
+ finally
+ let env' ← getEnv
+ envRef.val.set env'
+ finally
+ modifyEnv (fun _ => realEnv)
+ else act
+
+def getExamplesEnv : m Environment := do
+ if let some (envRef : EnvRef) := (← parameterValue? envParameter) then
+ envRef.val.get
+ else getEnv
+
+/--
+Run `act` with the examples environment set to the current environment for rollback.
+-/
+def withIsolatedExamplesEnv (act : m α) : m α := do
+ let env ← getExamplesEnv
+ let ref ← IO.mkRef env
+ let envRef := EnvRef.mk ref
+ withParameter envParameter envRef act
diff --git a/src/verso-manual/VersoManual/InlineLean/IO.lean b/src/verso-manual/VersoManual/InlineLean/IO.lean
index f7e43498b..dfb3f0567 100644
--- a/src/verso-manual/VersoManual/InlineLean/IO.lean
+++ b/src/verso-manual/VersoManual/InlineLean/IO.lean
@@ -231,8 +231,7 @@ private def getSubversoDir : IO System.FilePath := do
else
throw <| IO.userError s!"SubVerso directory {p} not found"
-
-def startExample [Monad m] [MonadEnv m] [MonadError m] [MonadQuotation m] [MonadRef m] : m Unit := do
+def startExample [Monad m] [MonadEnv m] [MonadError m] [MonadLiftT CoreM m] [MonadLiftT MetaM m] [MonadQuotation m] [MonadRef m] : m Unit := do
match ioExampleCtx.getState (← getEnv) with
| some _ => throwError "Can't initialize - already in a context"
| none =>
@@ -240,6 +239,7 @@ def startExample [Monad m] [MonadEnv m] [MonadError m] [MonadQuotation m] [Monad
modifyEnv fun env =>
ioExampleCtx.setState env (some {leanCodeName})
+
def saveLeanCode (src : StrLit) : DocElabM Ident := do
match ioExampleCtx.getState (← getEnv) with
| none => throwError "Can't set Lean code - not in an IO example"
@@ -284,7 +284,8 @@ def saveStderr [Monad m] [MonadEnv m] [MonadError m] (contents : StrLit) : m Uni
| none => throwError "Can't save stderr - not in an IO example"
| some st =>
match st.stderr with
- | none => modifyEnv fun env => ioExampleCtx.setState env (some {st with stderr := some contents})
+ | none =>
+ modifyEnv fun env => ioExampleCtx.setState env (some {st with stderr := some contents})
| some _ => throwError "stderr already specified"
@@ -398,20 +399,26 @@ where
shorten (str : String) : String :=
if str.length < 30 then str else str.take 30 ++ "…"
-def endExample (body : TSyntax `term) : DocElabM (TSyntax `term) := do
+def endExampleSetup : DocElabM Unit:= do
match ioExampleCtx.getState (← getEnv) with
- | none => throwErrorAt body "Can't end example - never started"
+ | none => throwError "Can't end example setup - never started"
| some {code, leanCodeName, inputFiles, outputFiles, stdin, stdout, stderr} => do
- modifyEnv fun env =>
- ioExampleCtx.setState env none
-
let some leanCode := code
- | throwErrorAt body "No code specified"
+ | throwError "No code specified"
let hlLean ← check leanCode leanCodeName.getId inputFiles outputFiles stdin stdout stderr
-
- `(let $leanCodeName : Highlighted := $(quote hlLean)
- $body)
+ addAndCompile <| .defnDecl {
+ name := leanCodeName.getId
+ levelParams := [],
+ type := .const ``Highlighted [],
+ value := toExpr hlLean,
+ hints := .opaque,
+ safety := .safe
+ }
+ if ((← getEnv).find? leanCodeName.getId).isSome then
+ return
+ else
+ throwError "Failed to save highlighted code as {leanCodeName}"
structure Config where
tag : Option String := none
@@ -493,27 +500,86 @@ def stderr : CodeBlockExpander
else
pure #[]
+deriving instance ToExpr for Lsp.Position
+deriving instance ToExpr for Lsp.Range
open IOExample in
-@[code_block_expander ioLean]
-def ioLean : CodeBlockExpander
+@[code_block_elab ioLean]
+def ioLean : CodeBlockElab
| args, str => do
let opts ← Config.parse.run args
let x ← saveLeanCode str
+ let g ← DocElabM.genreExpr
+
if opts.show then
let range := Syntax.getRange? str
let range := range.map (← getFileMap).utf8RangeToLspRange
- pure #[← ``(Block.other (Block.lean $x (some $(quote (← getFileName))) $(quote range)) #[Block.code $(quote str.getString)])]
+ --pure #[← ``(Block.other (Block.lean $x (some $(quote (← getFileName))) $(quote range)) #[Block.code $(quote str.getString)])]
+ let fn := some ((← getFileName) : System.FilePath)
+ let leanBlock : Expr := mkApp3 (.const ``Block.lean []) (.const x.getId []) (toExpr fn) (toExpr range)
+ return mkApp3 (.const ``Block.other []) g leanBlock (← Meta.mkArrayLit (← DocElabM.blockType) [mkApp2 (.const ``Block.code []) g (mkStrLit str.getString)])
else
- pure #[]
-
+ return mkApp2 (.const ``Block.concat []) g (← Meta.mkArrayLit (← DocElabM.blockType) [])
+
+
+private partial def isSpecialBlock : TSyntax `block → DocElabM Bool
+ | `(block|```$nameStx:ident $_args*|$_contents:str```) => do
+ let name ← realizeGlobalConstNoOverloadWithInfo nameStx
+ return name ∈ [``ioLean, ``stdin, ``stdout, ``stderr, ``exampleFile, ``outputFile, ``inputFile]
+ | `(block|:::$_nameStx:ident $_args*{$bs*} ) =>
+ bs.anyM isSpecialBlock
+ | _ => pure false
+
+@[directive_elab ref]
+private def ref : DirectiveElab
+ | args, #[] => do
+ let (x : Ident) ← ArgParse.run (.positional' `name) args
+ Term.elabTerm x (some (← DocElabM.blockType))
+ | _, _ => throwError "Invalid use of `ref`"
+
+private partial def liftSpecialBlocks (stx : Syntax) : StateT (Array (Ident × TSyntax `block)) DocElabM Syntax :=
+ stx.replaceM fun s =>
+ match s with
+ | `(block|```$nameStx:ident $_args*|$_contents:str```) => do
+ let name ← realizeGlobalConstNoOverloadWithInfo nameStx
+ if name ∈ [``ioLean, ``stdin, ``stdout, ``stderr, ``exampleFile, ``outputFile, ``inputFile] then
+ let x ← mkFreshUserName <| name.componentsRev.find? (· matches .str _ _) |>.getD `x
+ let x := mkIdentFrom s x
+ modify (·.push (x, ⟨s⟩))
+ let b' ← `(block|:::ref $x:ident {})
+ pure (some b')
+ else pure none
+ | _ => pure none
+
+-- TODO lift extract special blocks from nested contexts and elaborate that way
open IOExample in
-@[directive_expander ioExample]
-def ioExample : DirectiveExpander
+@[directive_elab ioExample]
+def ioExample : DirectiveElab
| args, blocks => do
ArgParse.done.run args
- startExample
- let body ← blocks.mapM elabBlock
- let body' ← `(Verso.Doc.Block.concat #[$body,*]) >>= endExample
- pure #[body']
+ let g ← DocElabM.genreExpr
+ try
+ startExample
+ let (blocks, lifted) ← StateT.run (blocks.mapM (liftSpecialBlocks ·.raw)) #[]
+ let bt ← DocElabM.blockType
+ -- First elaborate the special blocks, which has a side effect on the environment extension
+ let lifted ← lifted.mapM fun (x, b) => do
+ let b ← elabBlock' b >>= instantiateMVars
+ pure (x, b)
+ -- Use the extension's data to create helper definitions
+ endExampleSetup
+ -- Create definitions for the lifted blocks
+ for (x, b) in lifted do
+ addAndCompile <| .defnDecl {
+ name := x.getId, levelParams := [], type := bt, value := b, hints := .opaque, safety := .safe
+ }
+ -- Block until all helpers are ready before elaborating the final document
+ for (x, _) in lifted do
+ if (← getEnv).find? x.getId |>.isSome then continue else break
+
+ let body ← blocks.mapM (elabBlock' ⟨·⟩)
+ return mkApp2 (.const ``Block.concat []) g (← Meta.mkArrayLit (← DocElabM.blockType) body.toList)
+ finally
+ modifyEnv fun env =>
+ ioExampleCtx.setState env none
diff --git a/src/verso-manual/VersoManual/InlineLean/Scopes.lean b/src/verso-manual/VersoManual/InlineLean/Scopes.lean
index ec60a9994..1f2729ea5 100644
--- a/src/verso-manual/VersoManual/InlineLean/Scopes.lean
+++ b/src/verso-manual/VersoManual/InlineLean/Scopes.lean
@@ -13,7 +13,7 @@ open Lean Elab Command
namespace Verso.Genre.Manual.InlineLean.Scopes
initialize leanSampleScopes : Lean.EnvExtension (List Scope) ←
- Lean.registerEnvExtension (pure [])
+ Lean.registerEnvExtension (pure []) (asyncMode := .sync)
def initScopes [Monad m] [MonadEnv m] [MonadOptions m] [MonadResolveName m] : m Unit := do
if leanSampleScopes.getState (← getEnv) |>.isEmpty then
diff --git a/src/verso-manual/VersoManual/InlineLean/Signature.lean b/src/verso-manual/VersoManual/InlineLean/Signature.lean
index e5bcf5e5c..d8adca1ee 100644
--- a/src/verso-manual/VersoManual/InlineLean/Signature.lean
+++ b/src/verso-manual/VersoManual/InlineLean/Signature.lean
@@ -7,6 +7,7 @@ import Lean.Elab.InfoTree.Types
import Verso
import VersoManual.Basic
+import VersoManual.InlineLean.Env
import SubVerso.Examples
open SubVerso.Highlighting
@@ -54,7 +55,7 @@ def SignatureConfig.parse [Monad m] [MonadError m] [MonadLiftT CoreM m] : ArgPar
@[code_block_expander signature]
def signature : CodeBlockExpander
- | args, str => withoutAsync do
+ | args, str => usingExamplesEnv <| withoutAsync do
let {«show»} ← SignatureConfig.parse.run args
let altStr ← parserInputString str
let col? := (← getRef).getPos? |>.map (← getFileMap).utf8PosToLspPos |>.map (·.character)
diff --git a/src/verso-manual/VersoManual/InlineLean/SyntaxError.lean b/src/verso-manual/VersoManual/InlineLean/SyntaxError.lean
index ea9af9e47..340be2f9f 100644
--- a/src/verso-manual/VersoManual/InlineLean/SyntaxError.lean
+++ b/src/verso-manual/VersoManual/InlineLean/SyntaxError.lean
@@ -7,6 +7,7 @@ import Lean.Elab.InfoTree.Types
import Verso
import VersoManual.Basic
+import VersoManual.InlineLean.Env
import VersoManual.InlineLean.Outputs
import SubVerso.Examples
@@ -130,7 +131,7 @@ def SyntaxErrorConfig.parse [Monad m] [MonadInfoTree m] [MonadLiftT CoreM m] [Mo
open Lean.Parser in
@[code_block_expander syntaxError]
def syntaxError : CodeBlockExpander
- | args, str => withoutAsync do
+ | args, str => withoutAsync <| usingExamplesEnv do
let config ← SyntaxErrorConfig.parse.run args
PointOfInterest.save (← getRef) config.name.toString
diff --git a/src/verso-manual/VersoManual/Markdown.lean b/src/verso-manual/VersoManual/Markdown.lean
index 1fcc962b4..d811c569f 100644
--- a/src/verso-manual/VersoManual/Markdown.lean
+++ b/src/verso-manual/VersoManual/Markdown.lean
@@ -7,6 +7,7 @@ Author: David Thrane Christiansen
import MD4Lean
import Lean.Exception
+import Lean.Meta
import Verso.Doc
@@ -47,6 +48,11 @@ def attr' (val : Array AttrText) : Except String String := do
| .error e => .error e
| .ok s => pure s
+def attr'' [Monad m] [MonadError m] (val : Array AttrText) : m Expr := do
+ match val.mapM attrText |>.map Array.toList |>.map String.join with
+ | .error e => throwError e
+ | .ok s => pure (toExpr s)
+
private structure MDState where
/-- A mapping from document header levels to actual nesting levels -/
inHeaders : List (Nat × Nat) := []
@@ -112,6 +118,54 @@ partial def inlineFromMarkdown' : Text → Except String (Doc.Inline g)
| .img .. => .error s!"Unexpected image in parsed Markdown"
| .wikiLink .. => .error s!"Unexpected wiki-style link in parsed Markdown"
+private def inlineType [Monad m] (g : Expr) : MDT m Expr Expr Expr := do
+ pure <| .app (.const ``Verso.Doc.Inline []) g
+
+private def blockType [Monad m] (g : Expr) : MDT m Expr Expr Expr := do
+ pure <| .app (.const ``Verso.Doc.Block []) g
+
+private def inlineArray [Monad m] [MonadLiftT MetaM m] (g : Expr) (xs : Array Expr) : MDT m Expr Expr Expr := do
+ let it ← inlineType g
+ Meta.mkArrayLit it xs.toList
+
+private def blockArray [Monad m] [MonadLiftT MetaM m] (g : Expr) (xs : Array Expr) : MDT m Expr Expr Expr := do
+ let it ← blockType g
+ Meta.mkArrayLit it xs.toList
+
+partial def inlineFromMarkdown'' [Monad m] [MonadLiftT MetaM m] [MonadQuotation m] [AddMessageContext m] [MonadError m] (g : Expr) : Text → StateT (Option String) (MDT m Expr Expr) Expr
+ | .normal str | .br str | .softbr str => do
+ (lastWord str).forM fun w => do
+ set (some w.toLower)
+ return mkApp2 (.const ``Verso.Doc.Inline.text []) g (toExpr str)
+ | .nullchar => throwError "Unexpected null character in parsed Markdown"
+ | .del _ => throwError "Unexpected strikethrough in parsed Markdown"
+ | .em txt => do
+ let txt ← txt.mapM (inlineFromMarkdown'' g)
+ return mkApp2 (.const ``Verso.Doc.Inline.emph []) g (← inlineArray (m := m) g txt)
+ | .strong txt => do
+ let txt ← txt.mapM (inlineFromMarkdown'' g)
+ return mkApp2 (.const ``Verso.Doc.Inline.bold []) g (← inlineArray (m := m) g txt)
+ | .a href _ _ txt => do
+ let txt ← txt.mapM (inlineFromMarkdown'' g)
+ let txt ← inlineArray (m := m) g txt
+ return mkApp3 (.const ``Verso.Doc.Inline.link []) g txt (← attr'' href)
+ | .latexMath m => do
+ set (none : Option String)
+ return mkApp3 (.const ``Verso.Doc.Inline.math []) g (toExpr Verso.Doc.MathMode.inline) (toExpr (String.join m.toList))
+ | .latexMathDisplay m => do
+ set (none : Option String)
+ return mkApp3 (.const ``Verso.Doc.Inline.math []) g (toExpr Verso.Doc.MathMode.display) (toExpr (String.join m.toList))
+ | .u txt => throwError "Unexpected underline around {repr txt} in parsed Markdown"
+ | .code strs => do
+ let str := String.join strs.toList
+ if let some f := (← read).elabInlineCode then
+ f (← get) str
+ else
+ return mkApp2 (.const ``Verso.Doc.Inline.code []) g (toExpr str)
+ | .entity ent => throwError s!"Unsupported entity {ent} in parsed Markdown"
+ | .img .. => throwError s!"Unexpected image in parsed Markdown"
+ | .wikiLink .. => throwError s!"Unexpected wiki-style link in parsed Markdown"
+
instance [Monad m] [MonadError m] : MonadError (MDT m b i) where
throw ex := fun _ρ _σ => throw ex
tryCatch act handler := fun ρ σ => tryCatch (act ρ σ) (fun e => handler e ρ σ)
@@ -172,6 +226,47 @@ where
if item.isTask then throwError "Tasks unsupported"
else ``(Verso.Doc.ListItem.mk #[$[$(← item.contents.mapM blockFromMarkdownAux)],*])
+private partial def blockFromMarkdownAux'' [Monad m] [MonadLiftT MetaM m] [AddMessageContext m] [MonadQuotation m] [MonadError m] (g : Expr) : MD4Lean.Block → MDT m Expr Expr Expr
+ | .p txt => do
+ let inlines ← (txt.mapM (inlineFromMarkdown'' g ·)).run' none
+ return mkApp2 (.const ``Verso.Doc.Block.para []) g (← inlineArray g inlines)
+ | .blockquote bs => do
+ let bs ← bs.mapM (blockFromMarkdownAux'' g)
+ return mkApp2 (.const ``Verso.Doc.Block.blockquote []) g (← blockArray g bs)
+ | .code info lang _ strs => do
+ let info? := (attr' info).toOption
+ let lang? := (attr' lang).toOption
+ let str := String.join strs.toList
+ if let some f := (← read).elabBlockCode then
+ f info? lang? str
+ else
+ return mkApp2 (.const ``Verso.Doc.Block.code []) g (toExpr str)
+ | .ul _ _ items => do
+ let items ← items.mapM itemFromMarkdown
+ let itemType := .app (.const ``Verso.Doc.ListItem [0]) (← blockType g)
+ return mkApp2 (.const ``Verso.Doc.Block.ul []) g (← Meta.mkArrayLit itemType items.toList)
+ | .ol _ i _ items => do
+ let items ← items.mapM itemFromMarkdown
+ let itemType := .app (.const ``Verso.Doc.ListItem [0]) (← blockType g)
+ return mkApp3 (.const ``Verso.Doc.Block.ol []) g (toExpr (Int.ofNat i)) (← Meta.mkArrayLit itemType items.toList)
+ | .header level txt => do
+ match (← getHeader level) with
+ | .error e => throwError e
+ | .ok h => do
+ let inlines ← (txt.mapM (inlineFromMarkdown'' g ·)).run' none
+ h inlines
+ | .html .. => throwError "Unexpected literal HTML in parsed Markdown"
+ | .hr => throwError "Unexpected horizontal rule (thematic break) in parsed Markdown"
+ | .table .. => throwError "Unexpected table in parsed Markdown"
+where
+ itemFromMarkdown [Monad m] [MonadQuotation m] [MonadError m] (item : MD4Lean.Li MD4Lean.Block) : MDT m Expr Expr Expr := do
+ if item.isTask then throwError "Tasks unsupported"
+ else
+ let items ← item.contents.mapM (blockFromMarkdownAux'' g)
+ let items ← blockArray g items
+ return mkApp2 (.const ``Verso.Doc.ListItem.mk [0]) (← blockType g) items
+
+
def blockFromMarkdown [Monad m] [MonadQuotation m] [MonadError m] [AddMessageContext m]
(md : MD4Lean.Block)
@@ -181,11 +276,31 @@ def blockFromMarkdown [Monad m] [MonadQuotation m] [MonadError m] [AddMessageCon
let ctxt := {headerHandlers := ⟨handleHeaders⟩, elabInlineCode, elabBlockCode}
(·.fst) <$> blockFromMarkdownAux md ctxt {}
+def blockFromMarkdown'' [Monad m] [MonadQuotation m] [MonadError m] [AddMessageContext m] [MonadLiftT MetaM m]
+ (genre : Expr)
+ (md : MD4Lean.Block)
+ (handleHeaders : List (Array Expr → m Expr) := [])
+ (elabInlineCode : Option (Option String → String → m Expr) := none)
+ (elabBlockCode : Option ((info? lang? : Option String) → String → m Expr) := none) : m Expr :=
+ let ctxt := {headerHandlers := ⟨handleHeaders⟩, elabInlineCode, elabBlockCode}
+ (·.fst) <$> blockFromMarkdownAux'' genre md ctxt {}
+
+
def strongEmphHeaders [Monad m] [MonadQuotation m] : List (Array Term → m Term) := [
fun stxs => ``(Verso.Doc.Block.para #[Verso.Doc.Inline.bold #[$stxs,*]]),
fun stxs => ``(Verso.Doc.Block.para #[Verso.Doc.Inline.emph #[$stxs,*]])
]
+def strongEmphHeaders'' [Monad m] [MonadLiftT MetaM m] (genre : Expr) : List (Array Expr → m Expr) :=
+ let it : Expr := .app (.const ``Verso.Doc.Inline []) genre
+ [
+ fun (exprs : Array Expr) => do
+ return mkApp2 (.const ``Verso.Doc.Block.para []) genre (← Meta.mkArrayLit it [mkApp2 (.const ``Verso.Doc.Inline.bold []) genre (← Meta.mkArrayLit it exprs.toList)]),
+ fun (exprs : Array Expr) => do
+ return mkApp2 (.const ``Verso.Doc.Block.para []) genre (← Meta.mkArrayLit it [mkApp2 (.const ``Verso.Doc.Inline.emph []) genre (← Meta.mkArrayLit it exprs.toList)])
+]
+
+
private partial def blockFromMarkdownAux' : MD4Lean.Block → MDT (Except String) (Doc.Block g) (Doc.Inline g) (Doc.Block g)
| .p txt => .para <$> txt.mapM (inlineFromMarkdown' ·)
| .blockquote bs => .blockquote <$> bs.mapM blockFromMarkdownAux'
diff --git a/src/verso-manual/VersoManual/Table.lean b/src/verso-manual/VersoManual/Table.lean
index ce262d939..a1d1cf83f 100644
--- a/src/verso-manual/VersoManual/Table.lean
+++ b/src/verso-manual/VersoManual/Table.lean
@@ -10,6 +10,7 @@ import Verso.Doc.ArgParse
open Verso Doc Elab
open Verso.Genre Manual
open Verso.ArgParse
+open DocElabM
open Lean Elab
@@ -19,7 +20,7 @@ namespace Verso.Genre.Manual
inductive TableConfig.Alignment where
| left | right | center
-deriving ToJson, FromJson, DecidableEq, Repr, Ord
+deriving ToJson, FromJson, DecidableEq, Repr, Ord, ToExpr
open Syntax in
open TableConfig.Alignment in
@@ -149,8 +150,11 @@ where
}
-@[directive_expander table]
-def table : DirectiveExpander
+/--
+Constructs a table from a list of lists. Each item in the outer list is a row, and each inner list is the contents of the row.
+-/
+@[directive_elab table]
+def table : DirectiveElab
| args, contents => do
let cfg ← TableConfig.parse.run args
-- The table should be a list of lists. Extract them!
@@ -174,9 +178,17 @@ def table : DirectiveExpander
if rows.any (·.size != columns) then
throwErrorAt oneBlock s!"Expected all rows to have same number of columns, but got {rows.map (·.size)}"
+ let g ← genreExpr
+ let bt ← blockType
+
let flattened := rows.flatten
- let blocks : Array (Syntax.TSepArray `term ",") ← flattened.mapM (·.mapM elabBlock)
- pure #[← ``(Block.other (Block.table $(quote columns) $(quote cfg.header) $(quote cfg.name) $(quote cfg.alignment)) #[Block.ul #[$[Verso.Doc.ListItem.mk #[$blocks,*]],*]])]
+ let rows : Array Expr ← flattened.mapM fun r => do
+ let cells ← r.mapM elabBlock'
+ pure <| mkApp2 (.const ``Doc.ListItem.mk [0]) bt (← Meta.mkArrayLit bt cells.toList)
+ let noTag : Expr := .app (.const ``Option.none [0]) (.const ``Tag [])
+ let table ← Meta.mkAppM ``Block.table #[toExpr columns, toExpr cfg.header, toExpr cfg.name, toExpr cfg.alignment, noTag]
+ let ul := mkApp2 (.const ``Block.ul []) g (← Meta.mkArrayLit (.app (.const ``Doc.ListItem [0]) bt) rows.toList)
+ return mkApp3 (.const ``Block.other []) g table (← Meta.mkArrayLit bt [ul])
where
getLi
diff --git a/src/verso/Verso/Code/Highlighted.lean b/src/verso/Verso/Code/Highlighted.lean
index 46f15bf0f..1954aa47f 100644
--- a/src/verso/Verso/Code/Highlighted.lean
+++ b/src/verso/Verso/Code/Highlighted.lean
@@ -49,6 +49,14 @@ where
| .point p s => return .point p s
| .tactics gs x y hl => .tactics gs x y <$> remove hl
+deriving instance Lean.ToExpr for Lean.LevelMVarId
+deriving instance Lean.ToExpr for Lean.Level
+deriving instance Lean.ToExpr for Token.Kind
+deriving instance Lean.ToExpr for Token
+deriving instance Lean.ToExpr for Highlighted.Span.Kind
+deriving instance Lean.ToExpr for Highlighted.Goal
+deriving instance Lean.ToExpr for Highlighted
+
end SubVerso.Highlighting
diff --git a/src/verso/Verso/Doc.lean b/src/verso/Verso/Doc.lean
index 48701f366..e750d7e05 100644
--- a/src/verso/Verso/Doc.lean
+++ b/src/verso/Verso/Doc.lean
@@ -5,6 +5,7 @@ Author: David Thrane Christiansen
-/
import Lean.Data.Json
+import Lean.ToExpr
import Verso.Doc.Name
namespace Verso
@@ -12,7 +13,7 @@ namespace Verso
namespace Doc
open Std (Format)
-open Lean (Name Json ToJson FromJson)
+open Lean (Name Json ToJson FromJson ToExpr)
open Lean.Json (getObj?)
structure Genre : Type 1 where
@@ -34,7 +35,7 @@ instance : Repr Genre.none.PartMetadata where
reprPrec e _ := nomatch e
inductive MathMode where | inline | display
-deriving Repr, BEq, Hashable, Ord, ToJson, FromJson
+deriving Repr, BEq, Hashable, Ord, ToJson, FromJson, ToExpr
private def arrayEq (eq : α → α → Bool) (xs ys : Array α) : Bool := Id.run do
if h : xs.size = ys.size then
diff --git a/src/verso/Verso/Doc/Concrete.lean b/src/verso/Verso/Doc/Concrete.lean
index 0eaeb7a49..35d189ec0 100644
--- a/src/verso/Verso/Doc/Concrete.lean
+++ b/src/verso/Verso/Doc/Concrete.lean
@@ -91,7 +91,7 @@ elab "#docs" "(" genre:term ")" n:ident title:str ":=" ":::::::" text:document "
let mut docState := st
for hook in (← documentFinishedHooks) do
- let ((), docState') ← runTermElabM fun _ => hook ⟨genre, g⟩ st' docState
+ let ((), docState') ← runTermElabM fun _ => hook ⟨genre, g, {}⟩ st' docState
docState := docState'
elab "#doc" "(" genre:term ")" title:str "=>" text:completeDocument eoi : term => open Lean Elab Term PartElabM DocElabM in do
@@ -211,7 +211,7 @@ def finishDoc (genre : Term) (title : StrLit) : CommandElabM Unit:= do
let mut docState := docStateExt.getState (← getEnv)
let genreExpr ← runTermElabM fun _ => Term.elabTerm genre (some (.const ``Doc.Genre [])) >>= instantiateExprMVars
for hook in (← documentFinishedHooks) do
- let ((), docState') ← runTermElabM fun _ => hook ⟨genre, genreExpr⟩ partState docState
+ let ((), docState') ← runTermElabM fun _ => hook ⟨genre, genreExpr, {}⟩ partState docState
docState := docState'
syntax (name := replaceDoc) "#doc" "(" term ")" str "=>" : command
@@ -301,7 +301,7 @@ elab (name := completeDoc) "#old_doc" "(" genre:term ")" title:str "=>" text:com
elabCommand (← `($titleStr:docComment def $docName : Part $genre := $(← finished.toSyntax' genre)))
let mut docState := st
for hook in (← documentFinishedHooks) do
- let ((), docState') ← runTermElabM fun _ => hook ⟨genre, g⟩ st' docState
+ let ((), docState') ← runTermElabM fun _ => hook ⟨genre, g, {}⟩ st' docState
docState := docState')
-- The heartbeat count is reset for each top-level Verso block because they are analogous to Lean commands.
diff --git a/src/verso/Verso/Doc/Concrete/InlineString.lean b/src/verso/Verso/Doc/Concrete/InlineString.lean
index 8696719ec..7f9c9e7a0 100644
--- a/src/verso/Verso/Doc/Concrete/InlineString.lean
+++ b/src/verso/Verso/Doc/Concrete/InlineString.lean
@@ -12,6 +12,8 @@ import Verso.Doc.Lsp
import Verso.Parser
import Verso.SyntaxUtils
+set_option guard_msgs.diff true
+
namespace Verso.Doc.Concrete
open Lean Parser
@@ -30,9 +32,8 @@ elab_rules : term
| `(inlines!%$tk$s) => do
let inls ← stringToInlines s
let g ← Meta.mkFreshExprMVar (some (.const ``Verso.Doc.Genre []))
- let (tms, _) ← DocElabM.run tk g {} (.init (← `(foo))) <| inls.mapM (elabInline ⟨·⟩)
- elabTerm (← `(term|Inline.concat #[ $[$tms],* ] )) none
-
+ let (tms, _) ← DocElabM.run tk g {} (.init (← `(foo))) <| inls.mapM (elabInline' ⟨·⟩)
+ Meta.mkAppM ``Inline.concat #[← Meta.mkArrayLit (.app (.const ``Inline []) g) tms.toList]
set_option pp.rawOnError true
diff --git a/src/verso/Verso/Doc/Elab.lean b/src/verso/Verso/Doc/Elab.lean
index 14195fa2d..3fda927d0 100644
--- a/src/verso/Verso/Doc/Elab.lean
+++ b/src/verso/Verso/Doc/Elab.lean
@@ -17,6 +17,47 @@ open Verso.Syntax
def throwUnexpected [Monad m] [MonadError m] (stx : Syntax) : m α :=
throwErrorAt stx "unexpected syntax{indentD stx}"
+partial def elabInline' (inline : TSyntax `inline) : DocElabM Expr :=
+ withRef inline <| withFreshMacroScope <| withIncRecDepth <| do
+ let t ← inlineType
+ match inline.raw with
+ | .missing =>
+ Meta.mkLabeledSorry t true true
+ | stx@(.node _ kind _) =>
+ let env ← getEnv
+ let result ← match (← liftMacroM (expandMacroImpl? env stx)) with
+ | some (_decl, stxNew?) => -- TODO terminfo here? Right now, we suppress most uses of it.
+ let stxNew ← liftMacroM <| liftExcept stxNew?
+ withMacroExpansionInfo stx stxNew <|
+ withRef stxNew <|
+ elabInline' ⟨stxNew⟩
+ | none =>
+ let exp ← inlineExpandersFor kind
+ for e in exp do
+ try
+ let termStx ← withFreshMacroScope <| e stx
+ return (← Term.elabTerm termStx (some t))
+ catch
+ | ex@(.internal id) =>
+ if id == unsupportedSyntaxExceptionId then pure ()
+ else throw ex
+ | ex => throw ex
+
+ let exp ← inlineElabsFor kind
+ for e in exp do
+ try
+ let expr ← withFreshMacroScope <| e stx
+ return expr
+ catch
+ | ex@(.internal id) =>
+ if id == unsupportedSyntaxExceptionId then pure ()
+ else throw ex
+ | ex => throw ex
+
+ throwUnexpected stx
+ | other =>
+ throwUnexpected other
+
partial def elabInline (inline : TSyntax `inline) : DocElabM (TSyntax `term) :=
withRef inline <| withFreshMacroScope <| withIncRecDepth <| do
match inline.raw with
@@ -41,40 +82,54 @@ partial def elabInline (inline : TSyntax `inline) : DocElabM (TSyntax `term) :=
if id == unsupportedSyntaxExceptionId then pure ()
else throw ex
| ex => throw ex
+
+ let exp ← inlineElabsFor kind
+ for e in exp do
+ try
+ let expr ← withFreshMacroScope <| e stx
+ let n ← defineInline expr
+ return mkIdentFrom stx n
+ catch
+ | ex@(.internal id) =>
+ if id == unsupportedSyntaxExceptionId then pure ()
+ else throw ex
+ | ex => throw ex
+
throwUnexpected stx
| other =>
throwUnexpected other
-@[inline_expander Verso.Syntax.text]
-partial def _root_.Verso.Syntax.text.expand : InlineExpander := fun x =>
+private def mkInline (ctor : Name) : DocElabM Expr := do
+ let g ← genreExpr
+ return .app (.const ctor []) g
+
+private def mkInlineArr (ctor : Name) (xs : Array Expr) : DocElabM Expr := do
+ let g ← genreExpr
+ return mkApp2 (.const ctor []) g (← Meta.mkArrayLit (← inlineType) xs.toList)
+
+@[inline_elab Verso.Syntax.text]
+partial def _root_.Verso.Syntax.text.elab : InlineElab := fun x =>
match x with
| `(inline| $s:str) => do
- -- Erase the source locations from the string literal to prevent unwanted hover info
- ``(Inline.text $(⟨deleteInfo s.raw⟩))
+ return .app (← mkInline ``Inline.text) (toExpr s.getString)
| _ => throwUnsupportedSyntax
- where
- deleteInfo : Syntax → Syntax
- | .node _ k args => .node .none k (args.map deleteInfo)
- | .atom _ val => .atom .none val
- | .ident _ rawVal val preres => .ident .none rawVal val preres
- | .missing => .missing
-
-@[inline_expander Verso.Syntax.linebreak]
-def _root_.linebreak.expand : InlineExpander
- | `(inline|line! $s:str) =>
- ``(Inline.linebreak $(quote s.getString))
+
+@[inline_elab Verso.Syntax.linebreak]
+def _root_.linebreak.elab : InlineElab
+ | `(inline|line! $s:str) => do
+ return .app (← mkInline ``Inline.linebreak) (toExpr s.getString)
| _ => throwUnsupportedSyntax
-@[inline_expander Verso.Syntax.emph]
-def _root_.Verso.Syntax.emph.expand : InlineExpander
+@[inline_elab Verso.Syntax.emph]
+def _root_.Verso.Syntax.emph.elab : InlineElab
| `(inline| _[ $args* ]) => do
- ``(Inline.emph #[$[$(← args.mapM elabInline)],*])
+ mkInlineArr ``Inline.emph (← args.mapM elabInline')
| _ => throwUnsupportedSyntax
-@[inline_expander Verso.Syntax.bold]
-def _root_.Verso.Syntax.bold.expand : InlineExpander
+@[inline_elab Verso.Syntax.bold]
+def _root_.Verso.Syntax.bold.elab : InlineElab
| `(inline| *[ $args* ]) => do
- ``(Inline.bold #[$[$(← args.mapM elabInline)],*])
+ mkInlineArr ``Inline.bold (← args.mapM elabInline')
| _ => throwUnsupportedSyntax
def parseArgVal (val : TSyntax `arg_val) : DocElabM ArgVal := do
@@ -119,44 +174,60 @@ def appFallback
f (.node .none nullKind <| arrArg ++ argStx)
return ⟨appStx⟩
+
+
open Lean.Parser.Term in
-@[inline_expander Verso.Syntax.role]
-def _root_.Verso.Syntax.role.expand : InlineExpander
+@[inline_elab Verso.Syntax.role]
+def _root_.Verso.Syntax.role.elab : InlineElab
| inline@`(inline| role{$name $args*} [$subjects*]) => do
withRef inline <| withFreshMacroScope <| withIncRecDepth <| do
- let ⟨genre, _⟩ ← readThe DocElabContext
+ let ⟨genre, _, _⟩ ← readThe DocElabContext
+ let it ← inlineType
let resolvedName ← realizeGlobalConstNoOverloadWithInfo name
let exp ← roleExpandersFor resolvedName
+ let exp' ← roleElabsFor resolvedName
let argVals ← parseArgs args
- if exp.isEmpty then
+ if exp.isEmpty && exp'.isEmpty then
-- If no expanders are registered, then try elaborating just as a
-- function application node
- return ← appFallback inline name resolvedName argVals subjects
+ let appStx ← appFallback inline name resolvedName argVals subjects
+ return (← Term.elabTerm appStx (some it))
+
for e in exp do
try
let termStxs ← withFreshMacroScope <| e argVals subjects
let termStxs ← termStxs.mapM fun t => (``(($t : Inline $(⟨genre⟩))))
- return (← ``(Inline.concat (genre := $(⟨genre⟩)) #[$[$termStxs],*]))
+ return (← Term.elabTerm (← ``(Inline.concat (genre := $(⟨genre⟩)) #[$[$termStxs],*])) (some it))
catch
| ex@(.internal id) =>
if id == unsupportedSyntaxExceptionId then pure ()
else throw ex
| ex => throw ex
+
+ for e in exp' do
+ try
+ return (← withFreshMacroScope <| e argVals subjects)
+ catch
+ | ex@(.internal id) =>
+ if id == unsupportedSyntaxExceptionId then pure ()
+ else throw ex
+ | ex => throw ex
+
throwUnsupportedSyntax
| _ => throwUnsupportedSyntax
-@[inline_expander Verso.Syntax.link]
-def _root_.Verso.Syntax.link.expand : InlineExpander
+@[inline_elab Verso.Syntax.link]
+def _root_.Verso.Syntax.link.expand : InlineElab
| `(inline| link[ $txt* ] $dest:link_target) => do
- let url : TSyntax `term ←
+ let url : Expr ←
match dest with
| `(link_target| ( $url )) =>
- pure (↑ url)
+ Term.elabTerm (↑ url) none
| `(link_target| [ $ref ]) => do
-- Round-trip through quote to get rid of source locations, preventing unwanted IDE info
- addLinkRef ref
+ Term.elabTerm (← addLinkRef ref) none
| _ => throwErrorAt dest "Couldn't parse link destination"
- ``(Inline.link #[$[$(← txt.mapM elabInline)],*] $url)
+ return .app (← mkInlineArr ``Inline.link (← txt.mapM elabInline')) url
| _ => throwUnsupportedSyntax
@[inline_expander Verso.Syntax.footnote]
@@ -207,6 +278,50 @@ def decorateClosing : TSyntax `block → DocElabM Unit
| `(block|%%%%$s $_* %%%%$e) => closes s e
| _ => pure ()
+open Lean.Elab.Term in
+partial def elabBlock' (block : TSyntax `block) : DocElabM Expr :=
+ withTraceNode `Elab.Verso.block (fun _ => pure m!"Block {block}") <|
+ withRef block <| withFreshMacroScope <| withIncRecDepth <| do
+ let g ← genreExpr
+ let type : Expr := .app (.const ``Doc.Block []) g
+ decorateClosing block
+ match block.raw with
+ | .missing =>
+ Meta.mkSorry type true
+ | stx@(.node _ kind _) =>
+ let env ← getEnv
+ let result ← match (← liftMacroM (expandMacroImpl? env stx)) with
+ | some (_decl, stxNew?) => -- TODO terminfo here? Right now, we suppress most uses of it.
+ let stxNew ← liftMacroM <| liftExcept stxNew?
+ withMacroExpansionInfo stx stxNew <|
+ withRef stxNew <|
+ elabBlock' ⟨stxNew⟩
+ | none =>
+ let exp ← blockExpandersFor kind
+ for e in exp do
+ try
+ let termStx ← withFreshMacroScope <| e stx
+ return (← elabTerm termStx (some type))
+ catch
+ | ex@(.internal id) =>
+ if id == unsupportedSyntaxExceptionId then continue
+ else throw ex
+ | ex => throw ex
+ let exp ← blockElabsFor kind
+ for e in exp do
+ try
+ let b ← withFreshMacroScope <| e stx
+ return b
+ catch
+ | ex@(.internal id) =>
+ if id == unsupportedSyntaxExceptionId then continue
+ else throw ex
+ | ex => throw ex
+
+ throwUnexpected block
+ | _ =>
+ throwUnexpected block
+
open Lean.Elab.Term in
partial def elabBlock (block : TSyntax `block) : DocElabM (TSyntax `term) :=
withTraceNode `Elab.Verso.block (fun _ => pure m!"Block {block}") <|
@@ -234,6 +349,17 @@ partial def elabBlock (block : TSyntax `block) : DocElabM (TSyntax `term) :=
if id == unsupportedSyntaxExceptionId then continue
else throw ex
| ex => throw ex
+ let exp ← blockElabsFor kind
+ for e in exp do
+ try
+ let b ← withFreshMacroScope <| e stx
+ let n ← defineBlock b
+ return mkIdentFrom stx n
+ catch
+ | ex@(.internal id) =>
+ if id == unsupportedSyntaxExceptionId then continue
+ else throw ex
+ | ex => throw ex
throwUnexpected block
| _ =>
throwUnexpected block
@@ -260,8 +386,8 @@ where
fallback : PartElabM Unit := do
if (← getThe PartElabM.State).partContext.priorParts.size > 0 then
throwErrorAt cmd "Unexpected block"
- let blk ← liftDocElabM <| elabBlock cmd
- addBlock blk
+ let blk ← liftDocElabM <| elabBlock' cmd
+ addBlockExpr blk
@[part_command Verso.Syntax.footnote_ref]
partial def _root_.Verso.Syntax.footnote_ref.command : PartCommand
@@ -354,55 +480,61 @@ def includeSection : PartCommand
where
resolved id := mkIdentFrom id <$> realizeGlobalConstNoOverloadWithInfo (mkIdentFrom id (docName id.getId))
-@[block_expander Verso.Syntax.block_role]
-def _root_.Verso.Syntax.block_role.expand : BlockExpander := fun block =>
+@[block_elab Verso.Syntax.block_role]
+def _root_.Verso.Syntax.block_role.elab : BlockElab := fun block =>
match block with
| `(block|block_role{$name $args*}) => do
withTraceNode `Elab.Verso.block (fun _ => pure m!"Block role {name}") <|
withRef block <| withFreshMacroScope <| withIncRecDepth <| do
- let ⟨genre, _⟩ ← readThe DocElabContext
+ let ⟨genre, _, _⟩ ← readThe DocElabContext
let resolvedName ← realizeGlobalConstNoOverloadWithInfo name
let exp ← blockRoleExpandersFor resolvedName
+ let elabs ← blockRoleElabsFor resolvedName
let argVals ← parseArgs args
- if exp.isEmpty then
- return ← appFallback block name resolvedName argVals none
+ if exp.isEmpty && elabs.isEmpty then
+ return (← Term.elabTerm (← appFallback block name resolvedName argVals none) (some (← blockType)))
for e in exp do
try
let termStxs ← withFreshMacroScope <| e argVals #[]
- return (← ``(Block.concat (genre := $(⟨genre⟩)) #[$[$termStxs],*]))
+ return (← Term.elabTerm (← ``(Block.concat (genre := $(⟨genre⟩)) #[$[$termStxs],*])) (some (← blockType)))
catch
| ex@(.internal id) =>
if id == unsupportedSyntaxExceptionId then pure ()
else throw ex
| ex => throw ex
+ for e in elabs do
+ try
+ return (← withFreshMacroScope <| e argVals #[])
+ catch
+ | ex@(.internal id) =>
+ if id == unsupportedSyntaxExceptionId then pure ()
+ else throw ex
+ | ex => throw ex
+
throwUnsupportedSyntax
| _ => throwUnsupportedSyntax
-@[block_expander Verso.Syntax.para]
-partial def _root_.Verso.Syntax.para.expand : BlockExpander
+@[block_elab Verso.Syntax.para]
+partial def _root_.Verso.Syntax.para.elab : BlockElab
| `(block| para[ $args:inline* ]) => do
- let ⟨genre, _⟩ ← readThe DocElabContext
- ``(Block.para (genre := $(⟨genre⟩)) #[$[$(← args.mapM elabInline)],*])
+ Meta.mkAppM ``Block.para #[← Meta.mkArrayLit (← inlineType) (← args.mapM elabInline').toList]
| _ =>
throwUnsupportedSyntax
-
-def elabLi (block : Syntax) : DocElabM (Syntax × TSyntax `term) :=
+def elabLi (block : Syntax) : DocElabM (Syntax × Expr) :=
withRef block <|
match block with
| `(list_item|*%$dot $contents:block*) => do
- let ⟨genre, _⟩ ← readThe DocElabContext
- let item ← ``(ListItem.mk (α := Block $(⟨genre⟩)) #[$[$(← contents.mapM elabBlock)],*])
+ let item ← Meta.mkAppM ``ListItem.mk #[(← Meta.mkArrayLit (← DocElabM.blockType) (← contents.mapM elabBlock').toList)]
pure (dot, item)
| _ =>
throwUnsupportedSyntax
-@[block_expander Verso.Syntax.ul]
-def _root_.Verso.Syntax.ul.expand : BlockExpander
+@[block_elab Verso.Syntax.ul]
+def _root_.Verso.Syntax.ul.elab : BlockElab
| `(block|ul{$itemStxs*}) => do
- let ⟨genre, _⟩ ← readThe DocElabContext
let mut bullets : Array Syntax := #[]
- let mut items : Array (TSyntax `term) := #[]
+ let mut items : Array Expr := #[]
for i in itemStxs do
let (b, item) ← elabLi i
bullets := bullets.push b
@@ -410,16 +542,16 @@ def _root_.Verso.Syntax.ul.expand : BlockExpander
let info := DocListInfo.mk bullets itemStxs
for b in bullets do
pushInfoLeaf <| .ofCustomInfo {stx := b, value := Dynamic.mk info}
- ``(Block.ul (genre := $(⟨genre⟩)) #[$items,*])
+ let t ← Meta.mkAppM ``ListItem #[← DocElabM.blockType]
+ Meta.mkAppM ``Block.ul #[← Meta.mkArrayLit t items.toList]
| _ =>
throwUnsupportedSyntax
-@[block_expander Verso.Syntax.ol]
-def _root_.Verso.Syntax.ol.expand : BlockExpander
+@[block_elab Verso.Syntax.ol]
+def _root_.Verso.Syntax.ol.elab : BlockElab
| `(block|ol($start:num){$itemStxs*}) => do
- let ⟨genre, _⟩ ← readThe DocElabContext
let mut bullets : Array Syntax := #[]
- let mut items : Array (TSyntax `term) := #[]
+ let mut items : Array Expr := #[]
for i in itemStxs do
let (b, item) ← elabLi i
bullets := bullets.push b
@@ -427,26 +559,29 @@ def _root_.Verso.Syntax.ol.expand : BlockExpander
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,*])
+ let t ← Meta.mkAppM ``ListItem #[← DocElabM.blockType]
+ Meta.mkAppM ``Block.ol #[toExpr (Int.ofNat start.getNat), ← Meta.mkArrayLit t items.toList]
| _ =>
throwUnsupportedSyntax
-def elabDesc (block : Syntax) : DocElabM (Syntax × TSyntax `term) :=
+def elabDesc (block : Syntax) : DocElabM (Syntax × Expr) :=
withRef block <|
match block with
| `(desc_item|:%$colon $dts* => $dds*) => do
- let ⟨genre, _⟩ ← readThe DocElabContext
- let item ← ``(DescItem.mk (α := Inline $(⟨genre⟩)) (β := Block $(⟨genre⟩)) #[$[$(← dts.mapM elabInline)],*] #[$[$(← dds.mapM elabBlock)],*])
+ let g ← genreExpr
+ let it := .app (.const ``Inline []) g
+ let bt := .app (.const ``Block []) g
+ let item := mkApp4 (.const ``DescItem.mk [0, 0]) it bt (← Meta.mkArrayLit it (← dts.mapM elabInline').toList) (← Meta.mkArrayLit bt (← dds.mapM elabBlock').toList)
pure (colon, item)
| _ =>
throwUnsupportedSyntax
-@[block_expander Verso.Syntax.dl]
-def _root_.Verso.Syntax.dl.expand : BlockExpander
+@[block_elab Verso.Syntax.dl]
+def _root_.Verso.Syntax.dl.elab : BlockElab
| `(block|dl{$itemStxs*}) => do
- let ⟨genre, _⟩ ← readThe DocElabContext
+ let g ← genreExpr
let mut colons : Array Syntax := #[]
- let mut items : Array (TSyntax `term) := #[]
+ let mut items : Array Expr := #[]
for i in itemStxs do
let (b, item) ← elabDesc i
colons := colons.push b
@@ -454,57 +589,91 @@ def _root_.Verso.Syntax.dl.expand : BlockExpander
let info := DocListInfo.mk colons itemStxs
for b in colons do
pushInfoLeaf <| .ofCustomInfo {stx := b, value := Dynamic.mk info}
- ``(Block.dl (genre := $(⟨genre⟩)) #[$[$items],*])
+ let it := .app (.const ``Inline []) g
+ let bt := .app (.const ``Block []) g
+ let itemType := mkApp2 (.const ``DescItem [0, 0]) it bt
+ return mkApp2 (.const ``Block.dl []) g (← Meta.mkArrayLit itemType items.toList)
| _ =>
throwUnsupportedSyntax
-@[block_expander Verso.Syntax.blockquote]
-def _root_.Verso.Syntax.blockquote.expand : BlockExpander
+@[block_elab Verso.Syntax.blockquote]
+def _root_.Verso.Syntax.blockquote.elab : BlockElab
| `(block|> $innerBlocks*) => do
- ``(Block.blockquote #[$[$(← innerBlocks.mapM elabBlock)],*])
+ let g ← genreExpr
+ let bt ← blockType
+ return mkApp2 (.const ``Block.blockquote []) g (← Meta.mkArrayLit bt (← innerBlocks.mapM elabBlock').toList)
| _ =>
throwUnsupportedSyntax
-@[block_expander Verso.Syntax.codeblock]
-def _root_.Verso.Syntax.codeblock.expand : BlockExpander
+@[block_elab Verso.Syntax.codeblock]
+def _root_.Verso.Syntax.codeblock.expand : BlockElab
| `(block|``` $nameStx:ident $argsStx* | $contents:str ```) => do
- let ⟨genre, _⟩ ← readThe DocElabContext
+ let g ← genreExpr
let name ← realizeGlobalConstNoOverloadWithInfo nameStx
- let exp ← codeBlockExpandersFor name
-- TODO typed syntax here
let args ← parseArgs <| argsStx.map (⟨·⟩)
+ let bt ← blockType
+
+ let exp ← codeBlockExpandersFor name
for e in exp do
try
let termStxs ← withFreshMacroScope <| e args contents
- return (← ``(Block.concat (genre := $(⟨genre⟩)) #[$[$termStxs],*]))
+ let blks ← termStxs.mapM (Term.elabTerm · (some bt))
+ return mkApp2 (.const ``Block.concat []) g (← Meta.mkArrayLit bt blks.toList)
catch
| ex@(.internal id) =>
if id == unsupportedSyntaxExceptionId then pure ()
else throw ex
| ex => throw ex
+
+ let exp ← codeBlockElabsFor name
+ for e in exp do
+ try
+ let blk ← withFreshMacroScope <| e args contents
+ return blk
+ 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))
+ let g ← genreExpr
+ return mkApp2 (.const ``Block.code []) g (toExpr contents.getString)
| _ =>
throwUnsupportedSyntax
-@[block_expander Verso.Syntax.directive]
-def _root_.Verso.Syntax.directive.expand : BlockExpander
+@[block_elab Verso.Syntax.directive]
+def _root_.Verso.Syntax.directive.expand : BlockElab
| `(block| ::: $nameStx:ident $argsStx* { $contents:block* } ) => do
- let ⟨genre, _⟩ ← readThe DocElabContext
+
+ let ⟨genre, _, _⟩ ← readThe DocElabContext
let name ← realizeGlobalConstNoOverloadWithInfo nameStx
- let exp ← directiveExpandersFor name
let args ← parseArgs argsStx
+
+ let exp ← directiveExpandersFor name
for e in exp do
try
let termStxs ← withFreshMacroScope <| e args contents
- return (← ``(Block.concat (genre := $(⟨genre⟩)) #[$[$termStxs],*]))
+ return (← Term.elabTerm (← ``(Block.concat (genre := $(⟨genre⟩)) #[$[$termStxs],*])) (← blockType))
+ catch
+ | ex@(.internal id) =>
+ if id == unsupportedSyntaxExceptionId then pure ()
+ else throw ex
+ | ex => throw ex
+
+ let exp ← directiveElabsFor name
+ for e in exp do
+ try
+ return (← withFreshMacroScope <| e args contents)
catch
| ex@(.internal id) =>
if id == unsupportedSyntaxExceptionId then pure ()
else throw ex
| ex => throw ex
+
throwUnsupportedSyntax
| _ =>
throwUnsupportedSyntax
diff --git a/src/verso/Verso/Doc/Elab/Monad.lean b/src/verso/Verso/Doc/Elab/Monad.lean
index 6c5b75a9c..810a4d27f 100644
--- a/src/verso/Verso/Doc/Elab/Monad.lean
+++ b/src/verso/Verso/Doc/Elab/Monad.lean
@@ -91,9 +91,54 @@ def headerStxToString (env : Environment) : Syntax → String
| headerStx => dbg_trace "didn't understand {headerStx} for string"
""
+/-- Parameters that have dynamic extent with respect to Verso elaboration. -/
+structure DocElabParameters where
+ parameters : NameMap Dynamic := {}
+
structure DocElabContext where
genreSyntax : Syntax
genre : Expr
+ parameters : DocElabParameters := {}
+
+section
+variable [Monad m] [MonadError m] [MonadReaderOf DocElabContext m] [MonadWithReaderOf DocElabContext m] [TypeName α]
+
+def withModifiedParameter (x : Name) (f : α → α) (act : m β) : m β := do
+ let ⟨params⟩ := (← read).parameters
+ if let some v := params.find? x then
+ if let some v := v.get? α then
+ withReader ({ · with parameters := ⟨params.insert x (.mk (f v))⟩ }) act
+ else throwError m!"Internal error: expected a {TypeName.typeName α} for {x}, but got a {v.typeName}"
+ else throwError m!"Internal error: no value for parameter {x} of type {TypeName.typeName α}"
+
+def withParameter (x : Name) (value : α) (act : m β) : m β := do
+ let ⟨params⟩ := (← read).parameters
+ if let some v := params.find? x then
+ if v.typeName ≠ TypeName.typeName α then
+ throwError m!"Internal error: expected a {TypeName.typeName α} for {x}, but a {v.typeName} was already present."
+ withReader ({ · with parameters := ⟨params.insert x (.mk value)⟩ }) act
+
+def parameterValue! (x : Name) : m α := do
+ let ⟨params⟩ := (← read).parameters
+ if let some v := params.find? x then
+ if let some v := v.get? α then
+ return v
+ else
+ throwError m!"Internal error: expected a {TypeName.typeName α} for {x}, but found a {v.typeName}."
+ else
+ throwError m!"Internal error: no value for {x}. Expected a {TypeName.typeName α} but no value was present."
+
+def parameterValue? (x : Name) : m (Option α) := do
+ let ⟨params⟩ := (← read).parameters
+ if let some v := params.find? x then
+ if let some v := v.get? α then
+ return (some v)
+ else
+ throwError m!"Internal error: expected a {TypeName.typeName α} for {x}, but found a {v.typeName}."
+ else
+ return none
+
+end
/-- References that must be local to the current blob of concrete document syntax -/
structure DocDef (α : Type) where
@@ -281,8 +326,11 @@ def PartElabM.State.init (title : Syntax) (expandedTitle : Option (String × Arr
def PartElabM (α : Type) : Type := ReaderT DocElabContext (StateT DocElabM.State (StateT PartElabM.State TermElabM)) α
-def PartElabM.run (genreSyntax : Syntax) (genre : Expr) (st : DocElabM.State) (st' : PartElabM.State) (act : PartElabM α) : TermElabM (α × DocElabM.State × PartElabM.State) := do
- let ((res, st), st') ← act ⟨genreSyntax, genre⟩ st st'
+def PartElabM.run (genreSyntax : Syntax) (genre : Expr)
+ (st : DocElabM.State) (st' : PartElabM.State)
+ (act : PartElabM α)
+ (params : DocElabParameters := {}) : TermElabM (α × DocElabM.State × PartElabM.State) := do
+ let ((res, st), st') ← act ⟨genreSyntax, genre, params⟩ st st'
pure (res, st, st')
instance : Alternative PartElabM := inferInstanceAs <| Alternative (ReaderT DocElabContext (StateT DocElabM.State (StateT PartElabM.State TermElabM)))
@@ -316,13 +364,19 @@ instance : MonadWithReaderOf Term.Context PartElabM := inferInstanceAs <| MonadW
instance : MonadReaderOf DocElabContext PartElabM := inferInstanceAs <| MonadReaderOf DocElabContext (ReaderT DocElabContext (StateT DocElabM.State (StateT PartElabM.State TermElabM)))
+instance : MonadWithReaderOf DocElabContext PartElabM := inferInstanceAs <| MonadWithReaderOf DocElabContext (ReaderT DocElabContext (StateT DocElabM.State (StateT PartElabM.State TermElabM)))
+
+
def PartElabM.withFileMap (fileMap : FileMap) (act : PartElabM α) : PartElabM α :=
fun ρ ρ' σ ctxt σ' mctxt rw cctxt => act ρ ρ' σ ctxt σ' mctxt rw {cctxt with fileMap := fileMap}
def DocElabM (α : Type) : Type := ReaderT DocElabContext (ReaderT PartElabM.State (StateT DocElabM.State TermElabM)) α
-def DocElabM.run (genreSyntax : Syntax) (genre : Expr) (st : DocElabM.State) (st' : PartElabM.State) (act : DocElabM α) : TermElabM (α × DocElabM.State) := do
- StateT.run (act ⟨genreSyntax, genre⟩ st') st
+def DocElabM.run (genreSyntax : Syntax) (genre : Expr)
+ (st : DocElabM.State) (st' : PartElabM.State)
+ (act : DocElabM α)
+ (params : DocElabParameters := {}) : TermElabM (α × DocElabM.State) := do
+ StateT.run (act ⟨genreSyntax, genre, params⟩ st') st
instance : Inhabited (DocElabM α) := ⟨fun _ _ _ => default⟩
@@ -375,6 +429,8 @@ instance : MonadWithReaderOf Term.Context DocElabM := inferInstanceAs <| MonadWi
instance : MonadReaderOf DocElabContext DocElabM := inferInstanceAs <| MonadReaderOf DocElabContext (ReaderT DocElabContext (ReaderT PartElabM.State (StateT DocElabM.State TermElabM)))
+instance : MonadWithReaderOf DocElabContext DocElabM := inferInstanceAs <| MonadWithReaderOf DocElabContext (ReaderT DocElabContext (ReaderT PartElabM.State (StateT DocElabM.State TermElabM)))
+
instance : MonadReaderOf PartElabM.State DocElabM := inferInstanceAs <| MonadReaderOf PartElabM.State (ReaderT DocElabContext (ReaderT PartElabM.State (StateT DocElabM.State TermElabM)))
def DocElabM.withFileMap (fileMap : FileMap) (act : DocElabM α) : DocElabM α :=
@@ -386,7 +442,7 @@ instance : MonadRecDepth DocElabM where
getMaxRecDepth := fun _ _ st' => do return (← MonadRecDepth.getMaxRecDepth, st')
def PartElabM.liftDocElabM (act : DocElabM α) : PartElabM α := do
- let ⟨gStx, g⟩ ← readThe DocElabContext
+ let ⟨gStx, g, _⟩ ← readThe DocElabContext
let (out, st') ← act.run gStx g (← getThe DocElabM.State) (← getThe PartElabM.State)
set st'
pure out
@@ -410,14 +466,78 @@ def findLinksAndNotes : Expr → MetaM (Array (Expr × Expr))
| .mdata _ e | .proj _ _ e => findLinksAndNotes e
| .sort .. | .fvar .. | .bvar .. | .const .. | .lit .. => pure #[]
+def DocElabM.genreExpr : DocElabM Expr := do
+ let ⟨_, g, _⟩ ← read
+ return g
+
+def DocElabM.blockType : DocElabM Expr := do
+ let g ← genreExpr
+ return .app (.const ``Doc.Block []) g
+
+def DocElabM.blockArray (blocks : Array Expr) : DocElabM Expr := do
+ let bt ← blockType
+ Meta.mkArrayLit bt blocks.toList
+
+
+def DocElabM.inlineType : DocElabM Expr := do
+ let g ← genreExpr
+ return .app (.const ``Doc.Inline []) g
+
+def DocElabM.inlineArray (inlines : Array Expr) : DocElabM Expr := do
+ let bt ← inlineType
+ Meta.mkArrayLit bt inlines.toList
+
+def DocElabM.emptyBlock : DocElabM Expr := do
+ pure <| mkApp2 (.const ``Block.concat []) (← genreExpr) (← Meta.mkArrayLit (← blockType) [])
+
open Lean Meta Elab Term in
-def PartElabM.addBlock (block : TSyntax `term) : PartElabM Unit := withRef block <| do
- let ⟨_, g⟩ ← readThe DocElabContext
+def DocElabM.defineInline (inline : Expr) : DocElabM Name := do
+ let g ← genreExpr
+
+ let n ← mkFreshUserName `inline
+
+ let type : Expr := .app (.const ``Doc.Inline []) g
+ let t ← ensureHasType (some type) inline
+ let t ← instantiateMVars t
+ let links ← findLinksAndNotes t
+ let t ← links.foldrM (init := t) fun (mv, mvty) t =>
+ (.lam `inst mvty · .instImplicit) <$> t.abstractM #[mv]
+ let t ← instantiateMVars t
+
+ let xs ← Term.addAutoBoundImplicits #[] none
+ let type ← instantiateMVars type
+ let type ← mkForallFVars (links.map (·.1)) type (binderInfoForMVars := .instImplicit)
+ let type ← mkForallFVars xs type
+ let type ← levelMVarToParam type
+ let usedParams := collectLevelParams {} type |>.params
+
+ match sortDeclLevelParams [] [] usedParams with
+ | Except.error msg => throwError msg
+ | Except.ok levelParams =>
+ synthesizeSyntheticMVarsNoPostponing
+ let t ← instantiateMVars t
+ let type ← instantiateMVars type
+ let t ← ensureHasType (some type) t
+ let decl := Declaration.defnDecl {
+ name := n,
+ levelParams := levelParams,
+ type := type,
+ value := t,
+ hints := .abbrev,
+ safety := .safe
+ }
+ Term.ensureNoUnassignedMVars decl
+ addAndCompile decl
+ return n
+
+open Lean Meta Elab Term in
+def DocElabM.defineBlock (block : Expr) : DocElabM Name := do
+ let g ← genreExpr
let n ← mkFreshUserName `block
let type : Expr := .app (.const ``Doc.Block []) g
- let t ← elabTerm block (some type)
+ let t ← ensureHasType (some type) block
let t ← instantiateMVars t
let links ← findLinksAndNotes t
let t ← links.foldrM (init := t) fun (mv, mvty) t =>
@@ -432,7 +552,7 @@ def PartElabM.addBlock (block : TSyntax `term) : PartElabM Unit := withRef block
let usedParams := collectLevelParams {} type |>.params
match sortDeclLevelParams [] [] usedParams with
- | Except.error msg => throwErrorAt block msg
+ | Except.error msg => throwError msg
| Except.ok levelParams =>
synthesizeSyntheticMVarsNoPostponing
let t ← instantiateMVars t
@@ -448,9 +568,22 @@ def PartElabM.addBlock (block : TSyntax `term) : PartElabM Unit := withRef block
}
Term.ensureNoUnassignedMVars decl
addAndCompile decl
+ return n
+
+open Lean Meta Elab Term in
+def PartElabM.addBlockExpr (block : Expr) : PartElabM Unit := do
+ let n ← DocElabM.defineBlock block
modifyThe State fun st =>
{ st with partContext.blocks := st.partContext.blocks.push (mkIdent n) }
+open Lean Meta Elab Term in
+def PartElabM.addBlock (block : TSyntax `term) : PartElabM Unit := withRef block <| do
+ let g ← DocElabM.genreExpr
+ let type : Expr := .app (.const ``Doc.Block []) g
+ let t ← elabTerm block (some type)
+ addBlockExpr t
+
+
def PartElabM.addPart (finished : FinishedPart) : PartElabM Unit := modifyThe State fun st =>
{st with partContext.priorParts := st.partContext.priorParts.push finished}
@@ -489,7 +622,7 @@ def DocElabM.addLinkRef (refName : TSyntax `str) : DocElabM (TSyntax `term) := d
def PartElabM.addFootnoteDef (refName : TSyntax `str) (content : Array (TSyntax `term)) : PartElabM Unit := do
let strName := refName.getString
let docName ← currentDocName
- let ⟨_, genre⟩ ← readThe DocElabContext
+ let ⟨_, genre, _⟩ ← readThe DocElabContext
match (← getThe State).footnoteDefs[strName]? with
| none =>
let t := mkApp3 (.const ``HasNote []) (toExpr strName) (toExpr docName) genre
@@ -512,7 +645,7 @@ def PartElabM.addFootnoteDef (refName : TSyntax `str) (content : Array (TSyntax
def DocElabM.addFootnoteRef (refName : TSyntax `str) : DocElabM (TSyntax `term) := do
let strName := refName.getString
- let ⟨genre, _⟩ ← readThe DocElabContext
+ let ⟨genre, _, _⟩ ← readThe DocElabContext
match (← getThe State).footnoteRefs[strName]? with
| none =>
modifyThe State fun st => {st with footnoteRefs := st.footnoteRefs.insert strName ⟨#[refName]⟩}
@@ -549,6 +682,46 @@ def closes (openTok closeTok : Syntax) : DocElabM Unit := do
let lineStr := if lineStr.startsWith "`" || lineStr.endsWith "`" then " " ++ lineStr ++ " " else lineStr
Hover.addCustomHover closeTok (.markdown s!"Closes line {line + 1}: ``````````{lineStr}``````````")
+/--
+Elaborates those values selected by `prioritize`, then runs `between`, and finally elaborates the
+rest.
+
+They are returned in their original order.
+-/
+def prioritizedElab [Monad m]
+ (prioritize : α → m Bool) (act : α → m β)
+ (between : m Unit)
+ (xs : Array α) : m (Array β) := do
+ let mut out := #[]
+ let mut later := #[]
+
+ for h:i in [0:xs.size] do
+ let x := xs[i]
+ if ← prioritize x then
+ out := out.push (i, (← act x))
+ else later := later.push (i, x)
+
+ between
+
+ for (i, x) in later do
+ out := out.push (i, (← act x))
+
+ out := out.qsort (fun (i, _) (j, _) => i < j)
+ return out.map (·.2)
+
+
+abbrev InlineElab := Syntax → DocElabM Expr
+
+initialize inlineElabAttr : KeyedDeclsAttribute InlineElab ←
+ mkDocExpanderAttribute `inline_elab ``InlineElab "Indicates that this function elaborates inline elements of a given name" `inlineElabAttr
+
+unsafe def inlineElabsForUnsafe (x : Name) : DocElabM (Array InlineElab) := do
+ let expanders := inlineElabAttr.getEntries (← getEnv) x
+ return expanders.map (·.value) |>.toArray
+
+@[implemented_by inlineElabsForUnsafe]
+opaque inlineElabsFor (x : Name) : DocElabM (Array InlineElab)
+
abbrev InlineExpander := Syntax → DocElabM (TSyntax `term)
@@ -563,6 +736,18 @@ unsafe def inlineExpandersForUnsafe (x : Name) : DocElabM (Array InlineExpander)
opaque inlineExpandersFor (x : Name) : DocElabM (Array InlineExpander)
+abbrev BlockElab := Syntax → DocElabM Expr
+
+initialize blockElabAttr : KeyedDeclsAttribute BlockElab ←
+ mkDocExpanderAttribute `block_elab ``BlockElab "Indicates that this function expands block elements of a given name" `blockElabAttr
+
+unsafe def blockElabsForUnsafe (x : Name) : DocElabM (Array BlockElab) := do
+ let expanders := blockElabAttr.getEntries (← getEnv) x
+ return expanders.map (·.value) |>.toArray
+
+@[implemented_by blockElabsForUnsafe]
+opaque blockElabsFor (x : Name) : DocElabM (Array BlockElab)
+
abbrev BlockExpander := Syntax → DocElabM (TSyntax `term)
@@ -591,6 +776,19 @@ unsafe def partCommandsForUnsafe (x : Name) : PartElabM (Array PartCommand) := d
opaque partCommandsFor (x : Name) : PartElabM (Array PartCommand)
+abbrev RoleElab := Array Arg → TSyntaxArray `inline → DocElabM Expr
+
+initialize roleElabAttr : KeyedDeclsAttribute RoleElab ←
+ mkDocExpanderAttribute `role_elab ``RoleElab "Indicates that this function is used to elaborate a given role" `roleElabAttr
+
+unsafe def roleElabsForUnsafe (x : Name) : DocElabM (Array RoleElab) := do
+ let elabs := roleElabAttr.getEntries (← getEnv) x
+ return elabs.map (·.value) |>.toArray
+
+@[implemented_by roleElabsForUnsafe]
+opaque roleElabsFor (x : Name) : DocElabM (Array RoleElab)
+
+
abbrev RoleExpander := Array Arg → TSyntaxArray `inline → DocElabM (Array (TSyntax `term))
initialize roleExpanderAttr : KeyedDeclsAttribute RoleExpander ←
@@ -604,6 +802,19 @@ unsafe def roleExpandersForUnsafe (x : Name) : DocElabM (Array RoleExpander) :=
opaque roleExpandersFor (x : Name) : DocElabM (Array RoleExpander)
+abbrev CodeBlockElab := Array Arg → TSyntax `str → DocElabM Expr
+
+initialize codeBlockElabAttr : KeyedDeclsAttribute CodeBlockElab ←
+ mkDocExpanderAttribute `code_block_elab ``CodeBlockElab "Indicates that this function is used to elaborate a given code block" `codeBlockElabAttr
+
+unsafe def codeBlockElabsForUnsafe (x : Name) : DocElabM (Array CodeBlockElab) := do
+ let elabs := codeBlockElabAttr.getEntries (← getEnv) x
+ return elabs.map (·.value) |>.toArray
+
+@[implemented_by codeBlockElabsForUnsafe]
+opaque codeBlockElabsFor (x : Name) : DocElabM (Array CodeBlockElab)
+
+
abbrev CodeBlockExpander := Array Arg → TSyntax `str → DocElabM (Array (TSyntax `term))
initialize codeBlockExpanderAttr : KeyedDeclsAttribute CodeBlockExpander ←
@@ -617,6 +828,18 @@ unsafe def codeBlockExpandersForUnsafe (x : Name) : DocElabM (Array CodeBlockExp
opaque codeBlockExpandersFor (x : Name) : DocElabM (Array CodeBlockExpander)
+abbrev DirectiveElab := Array Arg → TSyntaxArray `block → DocElabM Expr
+
+initialize directiveElabAttr : KeyedDeclsAttribute DirectiveElab ←
+ mkDocExpanderAttribute `directive_elab ``DirectiveElab "Indicates that this function is used to elaborate a given directive" `directiveElabAttr
+
+unsafe def directiveElabsForUnsafe (x : Name) : DocElabM (Array DirectiveElab) := do
+ let expanders := directiveElabAttr.getEntries (← getEnv) x
+ return expanders.map (·.value) |>.toArray
+
+@[implemented_by directiveElabsForUnsafe]
+opaque directiveElabsFor (x : Name) : DocElabM (Array DirectiveElab)
+
abbrev DirectiveExpander := Array Arg → TSyntaxArray `block → DocElabM (Array (TSyntax `term))
@@ -631,6 +854,19 @@ unsafe def directiveExpandersForUnsafe (x : Name) : DocElabM (Array DirectiveExp
opaque directiveExpandersFor (x : Name) : DocElabM (Array DirectiveExpander)
+abbrev BlockRoleElab := Array Arg → Array Syntax → DocElabM Expr
+
+initialize blockRoleElabAttr : KeyedDeclsAttribute BlockRoleElab ←
+ mkDocExpanderAttribute `block_role_elab ``BlockRoleElab "Indicates that this function is used to implement a given blockRole" `blockRoleElabAttr
+
+unsafe def blockRoleElabsForUnsafe (x : Name) : DocElabM (Array BlockRoleElab) := do
+ let elabs := blockRoleElabAttr.getEntries (← getEnv) x
+ return elabs.map (·.value) |>.toArray
+
+@[implemented_by blockRoleElabsForUnsafe]
+opaque blockRoleElabsFor (x : Name) : DocElabM (Array BlockRoleElab)
+
+
abbrev BlockRoleExpander := Array Arg → Array Syntax → DocElabM (Array (TSyntax `term))