Skip to content

Commit

Permalink
chore: add tests for Verso sytnax quasiquotes
Browse files Browse the repository at this point in the history
  • Loading branch information
@david-christiansen
david-christiansen committed Jan 7, 2025
1 parent 3fc72ba commit 53a352c
Show file tree
Hide file tree
Showing 2 changed files with 359 additions and 16 deletions.
373 changes: 358 additions & 15 deletions src/verso/Verso/Parser.lean
View file
Original file line number Diff line number Diff line change
Expand Up @@ -3033,21 +3033,6 @@ All input consumed.
#guard_msgs in
#eval blocks {} |>.test! "## Header!\n"
-- Test that the antiquote for headers matches parser output
/--
info: 1
---
info: "Header!"
-/
#guard_msgs in
open Lean Elab Command in
#eval show CommandElabM Unit from do
let stx : TSyntax `block := ⟨← block {} |>.parseString "## Header!\n"⟩
if let `(block|header($n){$inlines}) := stx then
logInfo n
logInfo inlines
else logError "Didn't match"
/--
info: Success! Final stack:
[(Verso.Syntax.blockquote
Expand Down Expand Up @@ -4350,3 +4335,361 @@ Error recovery tests:
a paragraph with [a bad link syntax](http://example.com
is OK. The rest *works*.
"#
section
-- Test that the antiquotes match the parser's output
open Lean Elab Command
set_option pp.rawOnError true
/--
info: "This is a paragraph."
---
info: line!"\n"
---
info: "Two lines."
-/
#guard_msgs in
#eval show CommandElabM Unit from do
let stx : TSyntax `block := ⟨← block {} |>.parseString "This is a paragraph.\nTwo lines."⟩
if let `(block|para[$txt*]) := stx then
for t in txt do logInfo t
else logError m!"Didn't match {stx}"
/--
info: [Error pretty printing syntax: format: uncaught backtrack exception. Falling back to raw printer.]
(Verso.Syntax.li "*" [(Verso.Syntax.para "para{" [(Verso.Syntax.text (str "\"One\""))] "}")])
---
info: [Error pretty printing syntax: format: uncaught backtrack exception. Falling back to raw printer.]
(Verso.Syntax.li
"*"
[(Verso.Syntax.para "para{" [(Verso.Syntax.text (str "\"Two\""))] "}")
(Verso.Syntax.ul
"ul{"
[(Verso.Syntax.li "*" [(Verso.Syntax.para "para{" [(Verso.Syntax.text (str "\"A\""))] "}")])]
"}")])
-/
#guard_msgs in
#eval show CommandElabM Unit from do
let stx : TSyntax `block := ⟨← block {} |>.parseString "* One\n* Two\n * A"⟩
if let `(block|ul{$items*}) := stx then
for t in items do logInfo t
else logError m!"Didn't match {stx}"
/--
info: 1
---
info: [Error pretty printing syntax: format: uncaught backtrack exception. Falling back to raw printer.]
(Verso.Syntax.li "1." [(Verso.Syntax.para "para{" [(Verso.Syntax.text (str "\"One\""))] "}")])
---
info: [Error pretty printing syntax: format: uncaught backtrack exception. Falling back to raw printer.]
(Verso.Syntax.li
"2."
[(Verso.Syntax.para "para{" [(Verso.Syntax.text (str "\"Two\""))] "}")
(Verso.Syntax.ol
"ol("
(num "1")
")"
"{"
[(Verso.Syntax.li "1)" [(Verso.Syntax.para "para{" [(Verso.Syntax.text (str "\"A\""))] "}")])]
"}")])
-/
#guard_msgs in
#eval show CommandElabM Unit from do
let stx : TSyntax `block := ⟨← block {} |>.parseString "1. One\n2. Two\n 1) A"⟩
if let `(block|ol($n){$items*}) := stx then
logInfo n
for t in items do logInfo t
else logError m!"Didn't match {stx}"
/--
info: [Error pretty printing syntax: format: uncaught backtrack exception. Falling back to raw printer.]
(Verso.Syntax.desc
":"
[(Verso.Syntax.text (str "\" One\""))]
"=>"
[(Verso.Syntax.para "para{" [(Verso.Syntax.text (str "\"En\""))] "}")])
---
info: [Error pretty printing syntax: format: uncaught backtrack exception. Falling back to raw printer.]
(Verso.Syntax.desc
":"
[(Verso.Syntax.text (str "\" Two\""))]
"=>"
[(Verso.Syntax.para "para{" [(Verso.Syntax.text (str "\"To\""))] "}")])
-/
#guard_msgs in
#eval show CommandElabM Unit from do
let stx : TSyntax `block := ⟨← block {} |>.parseString ": One\n\n En\n\n: Two\n\n To"⟩
if let `(block|dl{$items*}) := stx then
for t in items do logInfo t
else logError m!"Didn't match {stx}"
/-- info: "Code\n" -/
#guard_msgs in
#eval show CommandElabM Unit from do
let stx : TSyntax `block := ⟨← block {} |>.parseString "```\nCode\n```\n"⟩
if let `(block|``` | $s ```) := stx then
logInfo s
else logError m!"Didn't match {stx}"
/--
info: lean
---
info: hasArg:=true
---
info: "Code\n"
-/
#guard_msgs in
#eval show CommandElabM Unit from do
let stx : TSyntax `block := ⟨← block {} |>.parseString "```lean (hasArg := true)\nCode\n```\n"⟩
if let `(block|``` $n $args* | $s ```) := stx then
logInfo n
for a in args do logInfo a
logInfo s
else logError m!"Didn't match {stx}"
/--
info: [Error pretty printing syntax: format: uncaught backtrack exception. Falling back to raw printer.]
(Verso.Syntax.ul
"ul{"
[(Verso.Syntax.li "*" [(Verso.Syntax.para "para{" [(Verso.Syntax.text (str "\"Abc\""))] "}")])]
"}")
-/
#guard_msgs in
#eval show CommandElabM Unit from do
let stx : TSyntax `block := ⟨← block {} |>.parseString "> * Abc"⟩
if let `(block|> $blks*) := stx then
for b in blks do logInfo b
else logError m!"Didn't match {stx}"
/--
info: "lean"
---
info: "https://lean-lang.org"
-/
#guard_msgs in
#eval show CommandElabM Unit from do
let stx : TSyntax `block := ⟨← block {} |>.parseString "[lean]: https://lean-lang.org"⟩
if let `(block|[$x]: $url) := stx then
logInfo x
logInfo url
else logError m!"Didn't match {stx}"
/--
info: "lean"
---
info: "see "
---
info: [Error pretty printing syntax: format: uncaught backtrack exception. Falling back to raw printer.]
(Verso.Syntax.link
"["
[(Verso.Syntax.text (str "\"the website\""))]
"]"
(Verso.Syntax.url "(" (str "\"https://lean-lang.org\"") ")"))
-/
#guard_msgs in
#eval show CommandElabM Unit from do
let stx : TSyntax `block := ⟨← block {} |>.parseString "[^lean]: see [the website](https://lean-lang.org)"⟩
if let `(block|[^$name]: $txt*) := stx then
logInfo name
for t in txt do logInfo t
else logError m!"Didn't match {stx}"
/--
info: paragraph
---
info: [Error pretty printing syntax: format: uncaught backtrack exception. Falling back to raw printer.]
(Verso.Syntax.para "para{" [(Verso.Syntax.text (str "\"blah blah:\""))] "}")
---
info: [Error pretty printing syntax: format: uncaught backtrack exception. Falling back to raw printer.]
(Verso.Syntax.ul
"ul{"
[(Verso.Syntax.li
"*"
[(Verso.Syntax.para
"para{"
[(Verso.Syntax.text (str "\"List\""))
(Verso.Syntax.linebreak "line!" (str "\"\\n\""))
(Verso.Syntax.text (str "\"More\""))]
"}")])]
"}")
-/
#guard_msgs in
#eval show CommandElabM Unit from do
let stx : TSyntax `block := ⟨← block {} |>.parseString ":::paragraph\nblah blah:\n * List\nMore\n:::"⟩
if let `(block|:::$x $args* {$bs*}) := stx then
logInfo x
for a in args do logInfo a
for b in bs do logInfo b
else logError m!"Didn't match {stx}"
/--
info: 1
---
info: "Header!"
-/
#guard_msgs in
#eval show CommandElabM Unit from do
let stx : TSyntax `block := ⟨← block {} |>.parseString "## Header!\n"⟩
if let `(block|header($n){$inlines}) := stx then
logInfo n
logInfo inlines
else logError "Didn't match"
-- Inlines
/-- info: "abc" -/
#guard_msgs in
#eval show CommandElabM Unit from do
let stx : TSyntax `block := ⟨← inline {} |>.parseString "abc"⟩
if let `(inline|$s:str) := stx then
logInfo s
else logError m!"Didn't match {stx}"
/-- info: "abc" -/
#guard_msgs in
#eval show CommandElabM Unit from do
let stx : TSyntax `block := ⟨← inline {} |>.parseString "_abc_"⟩
if let `(inline|_[$i*]) := stx then
for x in i do logInfo x
else logError m!"Didn't match {stx}"
/-- info: "abc" -/
#guard_msgs in
#eval show CommandElabM Unit from do
let stx : TSyntax `block := ⟨← inline {} |>.parseString "*abc*"⟩
if let `(inline|*[$i*]) := stx then
for x in i do logInfo x
else logError m!"Didn't match {stx}"
/--
info: "abc"
---
info: "http://lean-lang.org"
-/
#guard_msgs in
#eval show CommandElabM Unit from do
let stx : TSyntax `block := ⟨← inline {} |>.parseString "[abc](http://lean-lang.org)"⟩
if let `(inline|link[$i*]($url)) := stx then
for x in i do logInfo x
logInfo url
else logError m!"Didn't match {stx}"
/--
info: "abc"
---
info: "lean"
-/
#guard_msgs in
#eval show CommandElabM Unit from do
let stx : TSyntax `block := ⟨← inline {} |>.parseString "[abc][lean]"⟩
if let `(inline|link[$i*][$ref]) := stx then
for x in i do logInfo x
logInfo ref
else logError m!"Didn't match {stx}"
/-- info: "note" -/
#guard_msgs in
#eval show CommandElabM Unit from do
let stx : TSyntax `block := ⟨← inline {} |>.parseString "[^note]"⟩
if let `(inline|footnote($ref)) := stx then
logInfo ref
else logError m!"Didn't match {stx}"
/-- info: "\n" -/
#guard_msgs in
#eval show CommandElabM Unit from do
let stx : TSyntax `block := ⟨← inline {} |>.parseString "\n"⟩
if let `(inline|line! $s) := stx then
logInfo s
else logError m!"Didn't match {stx}"
/-- info: "abc" -/
#guard_msgs in
#eval show CommandElabM Unit from do
let stx : TSyntax `block := ⟨← inline {} |>.parseString "`abc`"⟩
if let `(inline|code($s)) := stx then
logInfo s
else logError m!"Didn't match {stx}"
/--
info: role
---
info: [Error pretty printing syntax: format: uncaught backtrack exception. Falling back to raw printer.]
(Verso.Syntax.code "`" (str "\"abc\"") "`")
-/
#guard_msgs in
#eval show CommandElabM Unit from do
let stx : TSyntax `block := ⟨← inline {} |>.parseString "{role}`abc`"⟩
if let `(inline|role{$x $args*}[$is*]) := stx then
logInfo x
for arg in args do logInfo arg
for i in is do logInfo i
else logError m!"Didn't match {stx}"
/--
info: role
---
info: 1
---
info: 2
---
info: [Error pretty printing syntax: format: uncaught backtrack exception. Falling back to raw printer.]
(Verso.Syntax.emph "_" [(Verso.Syntax.text (str "\"abc\""))] "_")
-/
#guard_msgs in
#eval show CommandElabM Unit from do
let stx : TSyntax `block := ⟨← inline {} |>.parseString "{role 1 2}_abc_"⟩
if let `(inline|role{$x $args*}[$is*]) := stx then
logInfo x
for arg in args do logInfo arg
for i in is do logInfo i
else logError m!"Didn't match {stx}"
/--
info: role
---
info: "abc "
---
info: [Error pretty printing syntax: format: uncaught backtrack exception. Falling back to raw printer.]
(Verso.Syntax.link "[" [(Verso.Syntax.text (str "\"abc\""))] "]" (Verso.Syntax.url "(" (str "\"url\"") ")"))
---
info: " abc"
-/
#guard_msgs in
#eval show CommandElabM Unit from do
let stx : TSyntax `block := ⟨← inline {} |>.parseString "{role}[abc [abc](url) abc]"⟩
if let `(inline|role{$x $args*}[$is*]) := stx then
logInfo x
for arg in args do logInfo arg
for i in is do logInfo i
else logError m!"Didn't match {stx}"
/-- info: "2+s" -/
#guard_msgs in
#eval show CommandElabM Unit from do
let stx : TSyntax `block := ⟨← inline {} |>.parseString "$`2+s`"⟩
if let `(inline|\math code($s)) := stx then
logInfo s
else logError m!"Didn't match {stx}"
/-- info: "2+s" -/
#guard_msgs in
#eval show CommandElabM Unit from do
let stx : TSyntax `block := ⟨← inline {} |>.parseString "$$`2+s`"⟩
if let `(inline|\displaymath code($s)) := stx then
logInfo s
else logError m!"Didn't match {stx}"
-- List items
#guard_msgs in
#eval show CommandElabM Unit from do
let stx : TSyntax `block := ⟨← block {} |>.parseString "* A\n* B"⟩
if let `(block|ul{ * $as* * $bs*}) := stx then
for x in as do logInfo x
for x in bs do logInfo x
else logError m!"Didn't match {stx}"
end
2 changes: 1 addition & 1 deletion src/verso/Verso/Syntax.lean
View file
Original file line number Diff line number Diff line change
Expand Up @@ -93,7 +93,7 @@ syntax (name:=linebreak) "line!" str : inline
character, then the resulting string has a single space stripped from each end.-/
syntax (name:=code) "code(" str ")" : inline
/-- A _role_: an extension to the Verso document language in an inline position -/
syntax (name:=role) "role{" ident argument* "}" "[" inline "]" : inline
syntax (name:=role) "role{" ident argument* "}" "[" inline* "]" : inline
/-- Inline mathematical notation (equivalent to LaTeX's `$` notation) -/
syntax (name:=inline_math) "\\math" code : inline
/-- Display-mode mathematical notation -/
Expand Down

0 comments on commit 53a352c

Please sign in to comment.