Skip to content

Commit

Permalink
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
fix: use declared syntax for all Verso syntax
Browse files Browse the repository at this point in the history
All of the syntax declarations used for Verso are now used for
pattern-matching in the main elaborator, which is reason to believe
that they're now reasonably comprehensive. This should make it much
easier for others to use them to write Verso extensions.

Closes #257
david-christiansen committed Jan 6, 2025

Verified

This commit was created on GitHub.com and signed with GitHub’s verified signature.
1 parent b84e7f6 commit 3162464
Showing 11 changed files with 579 additions and 166 deletions.
2 changes: 1 addition & 1 deletion examples/custom-genre/SimplePage.lean
Original file line number Diff line number Diff line change
@@ -196,7 +196,7 @@ instance : GenreHtml SimplePage IO where
part recur metadata | (.mk title titleString _ content subParts) => do
let incoming := (← HtmlT.state).refTargets[metadata.tag]?
let content' := if let some i := incoming then
let links := i.toArray.map fun t => ListItem.mk 0 #[Doc.Block.para #[Doc.Inline.link #[.text "(link)"] s!"#link-{t}"]]
let links := i.toArray.map fun t => ListItem.mk #[Doc.Block.para #[Doc.Inline.link #[.text "(link)"] s!"#link-{t}"]]
#[Doc.Block.para #[.text "Incoming links:"], Doc.Block.ul links] ++ content
else content
-- It's important that this not include the metadata in the recursive call, or the generator
2 changes: 1 addition & 1 deletion src/verso-blog/VersoBlog/Basic.lean
Original file line number Diff line number Diff line change
@@ -261,7 +261,7 @@ partial defmethod Inline.wordCount : Inline genre → Nat
partial defmethod Block.wordCount : Block genre → Nat
| .para contents => sumArrayWith (·.wordCount) contents
| .ul items
| .ol _ items => sumArrayWith (fun_, bs⟩ => sumArrayWith wordCount bs) items
| .ol _ items => sumArrayWith (fun ⟨bs⟩ => sumArrayWith wordCount bs) items
| .dl items => sumArrayWith (fun ⟨is, bs⟩ => sumArrayWith (·.wordCount) is + sumArrayWith wordCount bs) items
| .blockquote items
| .concat items => sumArrayWith wordCount items
2 changes: 1 addition & 1 deletion src/verso-manual/VersoManual/Markdown.lean
Original file line number Diff line number Diff line change
@@ -157,7 +157,7 @@ private partial def blockFromMarkdownAux' : MD4Lean.Block → MDT (Except String
where
itemFromMarkdown (item : MD4Lean.Li MD4Lean.Block) : MDT (Except String) (Doc.Block g) (Doc.Inline g) (Doc.ListItem _) := do
if item.isTask then .error "Tasks unsupported"
else .mk 0 <$> item.contents.mapM blockFromMarkdownAux'
else .mk <$> item.contents.mapM blockFromMarkdownAux'


def blockFromMarkdown'
2 changes: 1 addition & 1 deletion src/verso-manual/VersoManual/WordCount.lean
Original file line number Diff line number Diff line change
@@ -77,7 +77,7 @@ instance [WordCount α] [WordCount β] : WordCount (DescItem α β) where
countWords skip | ⟨dt, dd⟩ => countWords skip dt + countWords skip dd

instance [WordCount α] : WordCount (ListItem α) where
countWords skip | ⟨_, item⟩ => countWords skip item
countWords skip | ⟨item⟩ => countWords skip item

partial instance : WordCount (Verso.Doc.Block Manual) where
countWords skip b := blockWordCount skip b
11 changes: 5 additions & 6 deletions src/verso/Verso/Doc.lean
Original file line number Diff line number Diff line change
@@ -260,12 +260,11 @@ def Arg.syntax : Arg → Syntax
| .named stx _ _ => stx

structure ListItem (α : Type u) where
indent : Nat
contents : Array α
deriving Repr, BEq, Inhabited

private def ListItem.toJson (blockToJson : ToJson α) : ListItem α → Json
| ⟨i, xs⟩ => json% {"indent": $i, "contents": $(xs.map blockToJson.toJson)}
| ⟨xs⟩ => json% {"contents": $(xs.map blockToJson.toJson)}

instance [inst : ToJson α] : ToJson (ListItem α) := ⟨ListItem.toJson inst⟩

@@ -310,8 +309,8 @@ instance [ToJson genre.Inline] [ToJson genre.Block] : ToJson (Block genre) :=
partial def Block.beq [BEq genre.Inline] [BEq genre.Block] : Block genre → Block genre → Bool
| .para c1, .para c2 => c1 == c2
| .code c1, .code c2 => c1 == c2
| .ul i1, .ul i2 => arrayEq (fun | ⟨indent1, c1⟩, ⟨indent2, c2⟩ => indent1 == indent2 && arrayEq beq c1 c2) i1 i2
| .ol n1 i1, .ol n2 i2 => n1 == n2 && arrayEq (fun | ⟨indent1, c1⟩, ⟨indent2, c2⟩ => indent1 == indent2 && arrayEq beq c1 c2) i1 i2
| .ul i1, .ul i2 => arrayEq (fun | ⟨c1⟩, ⟨c2⟩ => arrayEq beq c1 c2) i1 i2
| .ol n1 i1, .ol n2 i2 => n1 == n2 && arrayEq (fun | ⟨c1⟩, ⟨c2⟩ => arrayEq beq c1 c2) i1 i2
| .dl i1, .dl i2 =>
arrayEq (fun | ⟨t1, d1⟩, ⟨t2, d2⟩ => t1 == t2 && arrayEq beq d1 d2) i1 i2
| .blockquote i1, .blockquote i2 => arrayEq beq i1 i2
@@ -456,9 +455,9 @@ where
match b with
| .para contents => .para <$> contents.mapM inline
| .ul items => .ul <$> items.mapM fun
| ListItem.mk n contents => ListItem.mk n <$> contents.mapM block
| ListItem.mk contents => ListItem.mk <$> contents.mapM block
| .ol start items => .ol start <$> items.mapM fun
| ListItem.mk n contents => ListItem.mk n <$> contents.mapM block
| ListItem.mk contents => ListItem.mk <$> contents.mapM block
| .dl items => .dl <$> items.mapM fun
| DescItem.mk t d => DescItem.mk <$> t.mapM inline <*> d.mapM block
| .blockquote items => .blockquote <$> items.mapM block
41 changes: 20 additions & 21 deletions src/verso/Verso/Doc/Elab.lean
Original file line number Diff line number Diff line change
@@ -275,19 +275,19 @@ partial def closePartsUntil (outer : Nat) (endPos : String.Pos) : PartElabM Unit

@[part_command Verso.Syntax.header]
partial def _root_.Verso.Syntax.header.command : PartCommand
| stx@(`<low|(Verso.Syntax.header ~(.atom info hashes ) ~(.node _ `null inlines) ) >) => do
| stx@`(block|header($headerLevel){$inlines*}) => do
let titleBits ← liftDocElabM <| inlines.mapM elabInline
let titleString := headerStxToString (← getEnv) stx
let headerLevel := hashes.length
let ambientLevel ← currentLevel
if headerLevel > ambientLevel + 1 then throwErrorAt stx "Wrong header nesting"
let headerLevel := headerLevel.getNat + 1
if headerLevel > ambientLevel + 1 then throwErrorAt stx "Wrong header nesting - got {headerLevel} but expected at most {ambientLevel}"
-- New subheader?
if headerLevel == ambientLevel + 1 then
-- Prelude is done!
pure ()
else
if let none := info.getPos? then dbg_trace "No start position for {stx}"
closePartsUntil headerLevel info.getPos!
if let none := stx.getPos? then dbg_trace "No start position for {stx}"
closePartsUntil headerLevel stx.getPos!

-- Start a new subpart
push {
@@ -365,16 +365,16 @@ partial def _root_.Verso.Syntax.para.expand : BlockExpander
def elabLi (block : Syntax) : DocElabM (Syntax × TSyntax `term) :=
withRef block <|
match block with
| `<low|(Verso.Syntax.li (bullet (column ~(.atom _ n)) ~dot) ~(.node _ `null args) )> => do
let item ← ``(ListItem.mk $(Syntax.mkNumLit n) #[$[$(← args.mapM elabBlock)],*])
| `(list_item|*%$dot $contents:inline*) => do
let item ← ``(ListItem.mk #[$[$(← contents.mapM elabBlock)],*])
pure (dot, item)
| _ =>
dbg_trace "unexpected block {block}"
throwUnsupportedSyntax

@[block_expander Verso.Syntax.ul]
def _root_.Verso.Syntax.ul.expand : BlockExpander
| `<low|(Verso.Syntax.ul ~(.node _ `null itemStxs) )> => do
| `(block|ul{$itemStxs*}) => do
let mut bullets : Array Syntax := #[]
let mut items : Array (TSyntax `term) := #[]
for i in itemStxs do
@@ -384,13 +384,13 @@ 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 #[$[$items],*])
``(Block.ul #[$items,*])
| _ =>
throwUnsupportedSyntax

@[block_expander Verso.Syntax.ol]
def _root_.Verso.Syntax.ol.expand : BlockExpander
| `<low|(Verso.Syntax.ol (num ~start) ~(.node _ `null itemStxs) )> => do
| `(block|ol{ $start:num $itemStxs*}) => do
let mut bullets : Array Syntax := #[]
let mut items : Array (TSyntax `term) := #[]
for i in itemStxs do
@@ -400,14 +400,14 @@ 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 $(Syntax.mkNumLit start.getAtomVal) #[$[$items],*])
``(Block.ol $start #[$items,*])
| _ =>
throwUnsupportedSyntax

def elabDesc (block : Syntax) : DocElabM (Syntax × TSyntax `term) :=
withRef block <|
match block with
| `<low|(Verso.Syntax.desc ~colon ~(.node _ `null dts) ~_ ~(.node _ `null dds))> => do
| `(desc_item|:%$colon $dts* => $dds*) => do
let item ← ``(DescItem.mk #[$[$(← dts.mapM elabInline)],*] #[$[$(← dds.mapM elabBlock)],*])
pure (colon, item)
| _ =>
@@ -416,7 +416,7 @@ def elabDesc (block : Syntax) : DocElabM (Syntax × TSyntax `term) :=

@[block_expander Verso.Syntax.dl]
def _root_.Verso.Syntax.dl.expand : BlockExpander
| `<low|(Verso.Syntax.dl ~(.node _ `null itemStxs) )> => do
| `(block|dl{$itemStxs*}) => do
let mut colons : Array Syntax := #[]
let mut items : Array (TSyntax `term) := #[]
for i in itemStxs do
@@ -432,22 +432,22 @@ def _root_.Verso.Syntax.dl.expand : BlockExpander

@[block_expander Verso.Syntax.blockquote]
def _root_.Verso.Syntax.blockquote.expand : BlockExpander
| `<low|(Verso.Syntax.blockquote ~_ ~(.node _ `null innerBlocks) )> => do
| `(block|blockquote{$innerBlocks*}) => do
``(Block.blockquote #[$[$(← innerBlocks.mapM elabBlock)],*])
| _ =>
throwUnsupportedSyntax


@[block_expander Verso.Syntax.codeblock]
def _root_.Verso.Syntax.codeblock.expand : BlockExpander
| `<low|(Verso.Syntax.codeblock (column ~(.atom _ _col)) ~_open ~(.node _ `null #[nameStx, .node _ `null argsStx]) ~(.atom info contents) ~_close )> => do
| `(block|``` $nameStx:ident $argsStx* | $contents:str ```) => do
let name ← realizeGlobalConstNoOverloadWithInfo nameStx
let exp ← codeBlockExpandersFor name
-- TODO typed syntax here
let args ← parseArgs <| argsStx.map (⟨·⟩)
for e in exp do
try
let termStxs ← withFreshMacroScope <| e args (Syntax.mkStrLit (info:=info) contents)
let termStxs ← withFreshMacroScope <| e args contents
return (← ``(Block.concat #[$[$termStxs],*]))
catch
| ex@(.internal id) =>
@@ -456,18 +456,17 @@ def _root_.Verso.Syntax.codeblock.expand : BlockExpander
| ex => throw ex
dbg_trace "No code block expander for '{nameStx}' ---> '{name}'"
throwUnsupportedSyntax
| `<low|(Verso.Syntax.codeblock (column ~(.atom _ _col)) ~_open ~(.node _ `null #[]) ~(.atom _info contents) ~_close )> =>
``(Block.code $(quote contents))
| `(block|``` | $contents:str ```) =>
``(Block.code $(quote contents.getString))
| _ =>
throwUnsupportedSyntax

@[block_expander Verso.Syntax.directive]
def _root_.Verso.Syntax.directive.expand : BlockExpander
| `<low|(Verso.Syntax.directive ~_open ~nameStx ~(.node _ `null argsStx) ~_fake ~_fake' ~(.node _ `null contents) ~_close )> => do
| `(block|directive{$nameStx $argsStx*}[$contents*]) => do
let name ← realizeGlobalConstNoOverloadWithInfo nameStx
let exp ← directiveExpandersFor name
-- TODO typed syntax here
let args ← parseArgs <| argsStx.map (⟨·⟩)
let args ← parseArgs argsStx
for e in exp do
try
let termStxs ← withFreshMacroScope <| e args contents
2 changes: 1 addition & 1 deletion src/verso/Verso/Doc/Elab/Monad.lean
Original file line number Diff line number Diff line change
@@ -77,7 +77,7 @@ def inlineSyntaxToString (env : Environment) (inlines : Syntax) : String :=
"<missing>"

def headerStxToString (env : Environment) : Syntax → String
| `<low|(Verso.Syntax.header ~(.atom _ _hashes ) ~(.node _ `null inlines) ) > => inlinesToString env inlines
| `(block|header($_){$inlines*}) => inlinesToString env inlines
| headerStx => dbg_trace "didn't understand {headerStx} for string"
"<missing>"

3 changes: 2 additions & 1 deletion src/verso/Verso/Doc/Lsp.lean
Original file line number Diff line number Diff line change
@@ -501,7 +501,8 @@ where
| ``Verso.Syntax.emph | ``Verso.Syntax.bold =>
mkTok text .keyword stx[0] ++ go snap text stx[1] ++ mkTok text .keyword stx[2]
| ``Verso.Syntax.header =>
mkTok text .keyword stx[0] ++ go snap text stx[1]
-- "header(" level ")" "{" contents "}", with source info for hash marks on "header(" token
mkTok text .keyword stx[0] ++ go snap text stx[4]
| ``Verso.Syntax.link =>
mkTok text .keyword stx[0] ++ go snap text stx[1] ++ mkTok text .keyword stx[2] ++
mkTok text .keyword stx[3][0] ++ mkTok text .keyword stx[3][2]
109 changes: 100 additions & 9 deletions src/verso/Verso/Examples.lean
Original file line number Diff line number Diff line change
@@ -51,8 +51,7 @@ info: Verso.Doc.Part.mk
#[Verso.Doc.Inline.text "My title here"]
"My title here"
none
#[Verso.Doc.Block.ul
#[{ indent := 0, contents := #[Verso.Doc.Block.para #[Verso.Doc.Inline.text "Just a list with one item"]] }]]
#[Verso.Doc.Block.ul #[{ contents := #[Verso.Doc.Block.para #[Verso.Doc.Inline.text "Just a list with one item"]] }]]
#[]
-/
#guard_msgs in
@@ -121,17 +120,110 @@ info: Verso.Doc.Part.mk
none
#[Verso.Doc.Block.para #[Verso.Doc.Inline.text "More text:"],
Verso.Doc.Block.ul
#[{ indent := 0, contents := #[Verso.Doc.Block.para #[Verso.Doc.Inline.text "and a list"]] },
{ indent := 0,
contents := #[Verso.Doc.Block.para #[Verso.Doc.Inline.text "with two"],
#[{ contents := #[Verso.Doc.Block.para #[Verso.Doc.Inline.text "and a list"]] },
{ contents := #[Verso.Doc.Block.para #[Verso.Doc.Inline.text "with two"],
Verso.Doc.Block.ul
#[{ indent := 1,
contents := #[Verso.Doc.Block.para #[Verso.Doc.Inline.text "and nested"]] }]] }]]
#[{ contents := #[Verso.Doc.Block.para #[Verso.Doc.Inline.text "and nested"]] }]] }]]
#[]]]
-/
#guard_msgs in
#eval c

#docs (.none) c' "My title here" :=
:::::::

# Section 1

a paragraph

## Section 1.1

More text:

1. and a list
2. with two
* and nested



:::::::

/--
info: Verso.Doc.Part.mk
#[Verso.Doc.Inline.text "My title here"]
"My title here"
none
#[]
#[Verso.Doc.Part.mk
#[Verso.Doc.Inline.text "Section 1"]
"Section 1"
none
#[Verso.Doc.Block.para #[Verso.Doc.Inline.text "a paragraph"]]
#[Verso.Doc.Part.mk
#[Verso.Doc.Inline.text "Section 1.1"]
"Section 1.1"
none
#[Verso.Doc.Block.para #[Verso.Doc.Inline.text "More text:"],
Verso.Doc.Block.ol
1
#[{ contents := #[Verso.Doc.Block.para #[Verso.Doc.Inline.text "and a list"]] },
{ contents := #[Verso.Doc.Block.para #[Verso.Doc.Inline.text "with two"]] }],
Verso.Doc.Block.ul #[{ contents := #[Verso.Doc.Block.para #[Verso.Doc.Inline.text "and nested"]] }]]
#[]]]
-/
#guard_msgs in
#eval c'

#docs (.none) c'' "My title here" :=
:::::::

# Section 1

a paragraph

## Section 1.1

More text:

: A list

a list

: With stuff

* and nested


:::::::

/--
info: Verso.Doc.Part.mk
#[Verso.Doc.Inline.text "My title here"]
"My title here"
none
#[]
#[Verso.Doc.Part.mk
#[Verso.Doc.Inline.text "Section 1"]
"Section 1"
none
#[Verso.Doc.Block.para #[Verso.Doc.Inline.text "a paragraph"]]
#[Verso.Doc.Part.mk
#[Verso.Doc.Inline.text "Section 1.1"]
"Section 1.1"
none
#[Verso.Doc.Block.para #[Verso.Doc.Inline.text "More text:"],
Verso.Doc.Block.dl
#[{ term := #[Verso.Doc.Inline.text " A list"],
desc := #[Verso.Doc.Block.para #[Verso.Doc.Inline.text "a list"]] },
{ term := #[Verso.Doc.Inline.text " With stuff"],
desc := #[Verso.Doc.Block.ul
#[{ contents := #[Verso.Doc.Block.para #[Verso.Doc.Inline.text "and nested"]] }]] }]]
#[]]]
-/
#guard_msgs in
#eval c''


#docs (.none) d "More writing" :=
:::::::

@@ -160,8 +252,7 @@ info: Verso.Doc.Part.mk
Verso.Doc.Block.blockquote
#[(Verso.Doc.Block.para #[Verso.Doc.Inline.text "I like quotes"]),
(Verso.Doc.Block.ul
#[{ indent := 2,
contents := #[Verso.Doc.Block.para #[Verso.Doc.Inline.text "Also with lists in them"]] }])],
#[{ contents := #[Verso.Doc.Block.para #[Verso.Doc.Inline.text "Also with lists in them"]] }])],
Verso.Doc.Block.para #[Verso.Doc.Inline.text "Also, 2 > 3."]]
#[]]
-/
Loading

0 comments on commit 3162464

Please sign in to comment.