Skip to content
Closed
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
The table of contents is too big for display.
Diff view
Diff view
  •  
  •  
  •  
2 changes: 1 addition & 1 deletion .gitignore
Original file line number Diff line number Diff line change
Expand Up @@ -7,4 +7,4 @@
_out
*.olean
/.verso/
/src/tests/parser/*/*.output
/src/tests/parser/**/*.output
34 changes: 33 additions & 1 deletion src/tests/TestMain.lean
Original file line number Diff line number Diff line change
Expand Up @@ -29,8 +29,40 @@ def testStemmer (_ : Config) : IO Unit := do
IO.eprintln s!"{x} --> {s} (wanted '{y}')"
throw <| IO.userError "Stemmer tests failed"

def testParser (dir : System.FilePath) (fn : Lean.Parser.ParserFn) : Config → IO Unit := fun config =>
Verso.GoldenTest.runTests {
testDir := ("src/tests/parser" : System.FilePath) / dir,
runTest := fn.test,
updateExpected := config.updateExpected
}

open Lean.Parser in
open Verso.Parser in
def tests := [
testStemmer
testStemmer,
testParser "metadataBlock" metadataBlock,
testParser "val" val,
testParser "arg" arg,
testParser "args" args,
testParser "nameAndArgs" nameAndArgs,
testParser "inlineTextChar" inlineTextChar,
testParser "manyInlineTextChar" (asStringFn (many1Fn inlineTextChar)),
testParser "inline/text" text,
testParser "inline/emph" (emph {}),
testParser "inline/code" code,
testParser "inline/role" (role {}),
testParser "inline" (inline {}),
testParser "block/code" (codeBlock {}),
testParser "block/header" (header {}),
testParser "block/blocks" (blocks {}),
testParser "block/recover" (recoverBlock (block {})),
testParser "blocks/recover" (recoverBlock (blocks {})),
testParser "block/directive" (directive {}),
testParser "block/opener" (ignoreFn blockOpener),
testParser "block/ulIndicator" (lookaheadUnorderedListIndicator {} (fun type => fakeAtom s! "{repr type}")),
testParser "block/olIndicator" (lookaheadOrderedListIndicator {} (fun type i => fakeAtom s! "{repr type} {i}")),
testParser "block/" (block {}),
testParser "document" document,
]

def getConfig (config : Config) : List String → IO Config
Expand Down
4 changes: 4 additions & 0 deletions src/tests/parser/arg/arg_0001.expected
Original file line number Diff line number Diff line change
@@ -0,0 +1,4 @@
Success! Final stack:
(Lean.Doc.Syntax.anon
(Lean.Doc.Syntax.arg_ident `x))
All input consumed.
1 change: 1 addition & 0 deletions src/tests/parser/arg/arg_0001.input
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
x
6 changes: 6 additions & 0 deletions src/tests/parser/arg/arg_0002.expected
Original file line number Diff line number Diff line change
@@ -0,0 +1,6 @@
Success! Final stack:
(Lean.Doc.Syntax.named_no_paren
`x
":="
(Lean.Doc.Syntax.arg_num (num "1")))
All input consumed.
1 change: 1 addition & 0 deletions src/tests/parser/arg/arg_0002.input
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
x:=1
8 changes: 8 additions & 0 deletions src/tests/parser/arg/arg_0003.expected
Original file line number Diff line number Diff line change
@@ -0,0 +1,8 @@
Success! Final stack:
(Lean.Doc.Syntax.named
"("
`x
":="
(Lean.Doc.Syntax.arg_num (num "1"))
")")
All input consumed.
1 change: 1 addition & 0 deletions src/tests/parser/arg/arg_0003.input
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
(x:=1)
5 changes: 5 additions & 0 deletions src/tests/parser/arg/arg_0004.expected
Original file line number Diff line number Diff line change
@@ -0,0 +1,5 @@
Failure @0 (⟨1, 0⟩): '
'; expected '(', '+', '-', identifier or numeral
Final stack:
(Lean.Doc.Syntax.arg_str <missing>)
Remaining: "\n(x:=1)"
2 changes: 2 additions & 0 deletions src/tests/parser/arg/arg_0004.input
Original file line number Diff line number Diff line change
@@ -0,0 +1,2 @@

(x:=1)
3 changes: 3 additions & 0 deletions src/tests/parser/arg/arg_0005.expected
Original file line number Diff line number Diff line change
@@ -0,0 +1,3 @@
Success! Final stack:
(Lean.Doc.Syntax.flag_on "+" `foo)
All input consumed.
1 change: 1 addition & 0 deletions src/tests/parser/arg/arg_0005.input
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
+foo
3 changes: 3 additions & 0 deletions src/tests/parser/arg/arg_0006.expected
Original file line number Diff line number Diff line change
@@ -0,0 +1,3 @@
Success! Final stack:
(Lean.Doc.Syntax.flag_off "-" `other)
All input consumed.
1 change: 1 addition & 0 deletions src/tests/parser/arg/arg_0006.input
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
-other
4 changes: 4 additions & 0 deletions src/tests/parser/arg/arg_0007.expected
Original file line number Diff line number Diff line change
@@ -0,0 +1,4 @@
Failure @2 (⟨1, 2⟩): expected no space before
Final stack:
(Lean.Doc.Syntax.flag_off "-" `other)
Remaining: "other"
1 change: 1 addition & 0 deletions src/tests/parser/arg/arg_0007.input
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
- other
9 changes: 9 additions & 0 deletions src/tests/parser/arg/arg_0008.expected
Original file line number Diff line number Diff line change
@@ -0,0 +1,9 @@
Success! Final stack:
(Lean.Doc.Syntax.named
"("
`x
":="
(Lean.Doc.Syntax.arg_num (num "1"))
")")
Remaining:
"\n"
1 change: 1 addition & 0 deletions src/tests/parser/arg/arg_0008.input
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
(x:=1)
6 changes: 6 additions & 0 deletions src/tests/parser/arg/arg_0009.expected
Original file line number Diff line number Diff line change
@@ -0,0 +1,6 @@
Success! Final stack:
(Lean.Doc.Syntax.named_no_paren
`x
":="
(Lean.Doc.Syntax.arg_ident `y))
All input consumed.
1 change: 1 addition & 0 deletions src/tests/parser/arg/arg_0009.input
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
x:=y
8 changes: 8 additions & 0 deletions src/tests/parser/arg/arg_0010.expected
Original file line number Diff line number Diff line change
@@ -0,0 +1,8 @@
Success! Final stack:
(Lean.Doc.Syntax.named
"("
`x
":="
(Lean.Doc.Syntax.arg_ident `y)
")")
All input consumed.
1 change: 1 addition & 0 deletions src/tests/parser/arg/arg_0010.input
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
(x:=y)
6 changes: 6 additions & 0 deletions src/tests/parser/arg/arg_0011.expected
Original file line number Diff line number Diff line change
@@ -0,0 +1,6 @@
Success! Final stack:
(Lean.Doc.Syntax.named_no_paren
`x
":="
(Lean.Doc.Syntax.arg_str (str "\"y\"")))
All input consumed.
1 change: 1 addition & 0 deletions src/tests/parser/arg/arg_0011.input
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
x:="y"
7 changes: 7 additions & 0 deletions src/tests/parser/arg/arg_0012.expected
Original file line number Diff line number Diff line change
@@ -0,0 +1,7 @@
Failure @3 (⟨1, 3⟩): unterminated string literal; expected identifier or numeral
Final stack:
• `x
• ":="
• (Lean.Doc.Syntax.arg_str <missing>)

Remaining: "\"y"
1 change: 1 addition & 0 deletions src/tests/parser/arg/arg_0012.input
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
x:="y
13 changes: 13 additions & 0 deletions src/tests/parser/arg/arg_0013.expected
Original file line number Diff line number Diff line change
@@ -0,0 +1,13 @@
2 failures:
@7 (⟨1, 7⟩): expected ')'
""
@7 (⟨1, 7⟩): unterminated string literal; expected identifier or numeral
""

Final stack:
(Lean.Doc.Syntax.named
"("
`x
":="
(Lean.Doc.Syntax.arg_str <missing>)
<missing>)
1 change: 1 addition & 0 deletions src/tests/parser/arg/arg_0013.input
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
(x:="y)
4 changes: 4 additions & 0 deletions src/tests/parser/arg/arg_0014.expected
Original file line number Diff line number Diff line change
@@ -0,0 +1,4 @@
Success! Final stack:
(Lean.Doc.Syntax.anon
(Lean.Doc.Syntax.arg_num (num "42")))
All input consumed.
1 change: 1 addition & 0 deletions src/tests/parser/arg/arg_0014.input
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
42
17 changes: 17 additions & 0 deletions src/tests/parser/arg/arg_0015.expected
Original file line number Diff line number Diff line change
@@ -0,0 +1,17 @@
4 failures:
@4 (⟨1, 4⟩): expected ')'
""
@4 (⟨1, 4⟩): expected ':='
""
@4 (⟨1, 4⟩): expected argument name
""
@4 (⟨1, 4⟩): unexpected end of input; expected identifier, numeral or string literal
""

Final stack:
(Lean.Doc.Syntax.named
"("
<missing>
<missing>
(Lean.Doc.Syntax.arg_str <missing>)
<missing>)
1 change: 1 addition & 0 deletions src/tests/parser/arg/arg_0015.input
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
(42)
15 changes: 15 additions & 0 deletions src/tests/parser/arg/arg_0016.expected
Original file line number Diff line number Diff line change
@@ -0,0 +1,15 @@
3 failures:
@6 (⟨1, 6⟩): expected ')'
""
@6 (⟨1, 6⟩): expected ':='
""
@6 (⟨1, 6⟩): unexpected end of input; expected identifier, numeral or string literal
""

Final stack:
(Lean.Doc.Syntax.named
"("
`x
<missing>
(Lean.Doc.Syntax.arg_str <missing>)
<missing>)
1 change: 1 addition & 0 deletions src/tests/parser/arg/arg_0016.input
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
(x 42)
9 changes: 9 additions & 0 deletions src/tests/parser/arg/arg_0017.expected
Original file line number Diff line number Diff line change
@@ -0,0 +1,9 @@
Failure @8 (⟨1, 8⟩): expected ')'
Final stack:
(Lean.Doc.Syntax.named
"("
`x
":="
(Lean.Doc.Syntax.arg_num (num "42"))
<missing>)
Remaining: "\n)"
2 changes: 2 additions & 0 deletions src/tests/parser/arg/arg_0017.input
Original file line number Diff line number Diff line change
@@ -0,0 +1,2 @@
(x := 42
)
9 changes: 9 additions & 0 deletions src/tests/parser/arg/arg_0018.expected
Original file line number Diff line number Diff line change
@@ -0,0 +1,9 @@
Failure @8 (⟨1, 8⟩): expected ')'
Final stack:
(Lean.Doc.Syntax.named
"("
`x
":="
(Lean.Doc.Syntax.arg_num (num "42"))
<missing>)
Remaining: "\na"
2 changes: 2 additions & 0 deletions src/tests/parser/arg/arg_0018.input
Original file line number Diff line number Diff line change
@@ -0,0 +1,2 @@
(x := 42
a
5 changes: 5 additions & 0 deletions src/tests/parser/args/args_0001.expected
Original file line number Diff line number Diff line change
@@ -0,0 +1,5 @@
Success! Final stack:
[(Lean.Doc.Syntax.anon
(Lean.Doc.Syntax.arg_num (num "43")))]
Remaining:
"\n\"foo\""
2 changes: 2 additions & 0 deletions src/tests/parser/args/args_0001.input
Original file line number Diff line number Diff line change
@@ -0,0 +1,2 @@
43
"foo"
9 changes: 9 additions & 0 deletions src/tests/parser/args/args_0002.expected
Original file line number Diff line number Diff line change
@@ -0,0 +1,9 @@
Success! Final stack:
[(Lean.Doc.Syntax.named_no_paren
`dialect
":="
(Lean.Doc.Syntax.arg_str (str "\"chicken\"")))
(Lean.Doc.Syntax.anon
(Lean.Doc.Syntax.arg_num (num "43")))]
Remaining:
"\nfoo"
2 changes: 2 additions & 0 deletions src/tests/parser/args/args_0002.input
Original file line number Diff line number Diff line change
@@ -0,0 +1,2 @@
dialect:="chicken" 43
foo
9 changes: 9 additions & 0 deletions src/tests/parser/args/args_0003.expected
Original file line number Diff line number Diff line change
@@ -0,0 +1,9 @@
Success! Final stack:
[(Lean.Doc.Syntax.named_no_paren
`dialect
":="
(Lean.Doc.Syntax.arg_str (str "\"chicken\"")))
(Lean.Doc.Syntax.anon
(Lean.Doc.Syntax.arg_num (num "43")))]
Remaining:
"\n(foo)"
2 changes: 2 additions & 0 deletions src/tests/parser/args/args_0003.input
Original file line number Diff line number Diff line change
@@ -0,0 +1,2 @@
dialect:="chicken" 43
(foo)
36 changes: 36 additions & 0 deletions src/tests/parser/block/block_0001.expected
Original file line number Diff line number Diff line change
@@ -0,0 +1,36 @@
Success! Final stack:
(Lean.Doc.Syntax.ul
"ul{"
[(Lean.Doc.Syntax.li
"*"
[(Lean.Doc.Syntax.para
"para{"
[(Lean.Doc.Syntax.text
(str "\"Here's a bullet\""))]
"}")])
(Lean.Doc.Syntax.li
"*"
[(Lean.Doc.Syntax.para
"para{"
[(Lean.Doc.Syntax.text
(str
"\"and another with some code in it\""))]
"}")
(Lean.Doc.Syntax.codeblock
"````"
[`lean []]
"\n"
(str "\"hey\\n\\nthere\\n\"")
"````")])
(Lean.Doc.Syntax.li
"*"
[(Lean.Doc.Syntax.para
"para{"
[(Lean.Doc.Syntax.text
(str "\"and another one\""))
(Lean.Doc.Syntax.linebreak
"line!"
(str "\"\\n\""))]
"}")])]
"}")
All input consumed.
8 changes: 8 additions & 0 deletions src/tests/parser/block/block_0001.input
Original file line number Diff line number Diff line change
@@ -0,0 +1,8 @@
* Here's a bullet
* and another with some code in it
````lean
hey

there
````
* and another one
4 changes: 4 additions & 0 deletions src/tests/parser/block/block_0002.expected
Original file line number Diff line number Diff line change
@@ -0,0 +1,4 @@
Success! Final stack:
(Lean.Doc.Syntax.command "{" `test [] "}")
Remaining:
"Here's a paragraph."
2 changes: 2 additions & 0 deletions src/tests/parser/block/block_0002.input
Original file line number Diff line number Diff line change
@@ -0,0 +1,2 @@
{test}
Here's a paragraph.
4 changes: 4 additions & 0 deletions src/tests/parser/block/block_0003.expected
Original file line number Diff line number Diff line change
@@ -0,0 +1,4 @@
Success! Final stack:
(Lean.Doc.Syntax.command "{" `test [] "}")
Remaining:
" Here's a paragraph."
2 changes: 2 additions & 0 deletions src/tests/parser/block/block_0003.input
Original file line number Diff line number Diff line change
@@ -0,0 +1,2 @@
{test}
Here's a paragraph.
4 changes: 4 additions & 0 deletions src/tests/parser/block/block_0004.expected
Original file line number Diff line number Diff line change
@@ -0,0 +1,4 @@
Success! Final stack:
(Lean.Doc.Syntax.command "{" `test [] "}")
Remaining:
" Here's a paragraph."
2 changes: 2 additions & 0 deletions src/tests/parser/block/block_0004.input
Original file line number Diff line number Diff line change
@@ -0,0 +1,2 @@
{test}
Here's a paragraph.
4 changes: 4 additions & 0 deletions src/tests/parser/block/block_0005.expected
Original file line number Diff line number Diff line change
@@ -0,0 +1,4 @@
Success! Final stack:
(Lean.Doc.Syntax.command "{" `test [] "}")
Remaining:
"Here's a paragraph."
Loading