diff --git a/.gitignore b/.gitignore index 98d45bb4c..4b856025b 100644 --- a/.gitignore +++ b/.gitignore @@ -7,4 +7,4 @@ _out *.olean /.verso/ -/src/tests/parser/*/*.output +/src/tests/parser/**/*.output diff --git a/src/tests/TestMain.lean b/src/tests/TestMain.lean index 86056bf61..832634b9a 100644 --- a/src/tests/TestMain.lean +++ b/src/tests/TestMain.lean @@ -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 diff --git a/src/tests/parser/arg/arg_0001.expected b/src/tests/parser/arg/arg_0001.expected new file mode 100644 index 000000000..e3baa4533 --- /dev/null +++ b/src/tests/parser/arg/arg_0001.expected @@ -0,0 +1,4 @@ +Success! Final stack: + (Lean.Doc.Syntax.anon + (Lean.Doc.Syntax.arg_ident `x)) +All input consumed. \ No newline at end of file diff --git a/src/tests/parser/arg/arg_0001.input b/src/tests/parser/arg/arg_0001.input new file mode 100644 index 000000000..c1b0730e0 --- /dev/null +++ b/src/tests/parser/arg/arg_0001.input @@ -0,0 +1 @@ +x \ No newline at end of file diff --git a/src/tests/parser/arg/arg_0002.expected b/src/tests/parser/arg/arg_0002.expected new file mode 100644 index 000000000..415949d8d --- /dev/null +++ b/src/tests/parser/arg/arg_0002.expected @@ -0,0 +1,6 @@ +Success! Final stack: + (Lean.Doc.Syntax.named_no_paren + `x + ":=" + (Lean.Doc.Syntax.arg_num (num "1"))) +All input consumed. \ No newline at end of file diff --git a/src/tests/parser/arg/arg_0002.input b/src/tests/parser/arg/arg_0002.input new file mode 100644 index 000000000..a07f3e468 --- /dev/null +++ b/src/tests/parser/arg/arg_0002.input @@ -0,0 +1 @@ +x:=1 \ No newline at end of file diff --git a/src/tests/parser/arg/arg_0003.expected b/src/tests/parser/arg/arg_0003.expected new file mode 100644 index 000000000..2f1c0fd65 --- /dev/null +++ b/src/tests/parser/arg/arg_0003.expected @@ -0,0 +1,8 @@ +Success! Final stack: + (Lean.Doc.Syntax.named + "(" + `x + ":=" + (Lean.Doc.Syntax.arg_num (num "1")) + ")") +All input consumed. \ No newline at end of file diff --git a/src/tests/parser/arg/arg_0003.input b/src/tests/parser/arg/arg_0003.input new file mode 100644 index 000000000..3ee9ce405 --- /dev/null +++ b/src/tests/parser/arg/arg_0003.input @@ -0,0 +1 @@ +(x:=1) \ No newline at end of file diff --git a/src/tests/parser/arg/arg_0004.expected b/src/tests/parser/arg/arg_0004.expected new file mode 100644 index 000000000..37b2f8400 --- /dev/null +++ b/src/tests/parser/arg/arg_0004.expected @@ -0,0 +1,5 @@ +Failure @0 (⟨1, 0⟩): ' +'; expected '(', '+', '-', identifier or numeral +Final stack: + (Lean.Doc.Syntax.arg_str ) +Remaining: "\n(x:=1)" \ No newline at end of file diff --git a/src/tests/parser/arg/arg_0004.input b/src/tests/parser/arg/arg_0004.input new file mode 100644 index 000000000..938e7b08b --- /dev/null +++ b/src/tests/parser/arg/arg_0004.input @@ -0,0 +1,2 @@ + +(x:=1) \ No newline at end of file diff --git a/src/tests/parser/arg/arg_0005.expected b/src/tests/parser/arg/arg_0005.expected new file mode 100644 index 000000000..8b83361a0 --- /dev/null +++ b/src/tests/parser/arg/arg_0005.expected @@ -0,0 +1,3 @@ +Success! Final stack: + (Lean.Doc.Syntax.flag_on "+" `foo) +All input consumed. \ No newline at end of file diff --git a/src/tests/parser/arg/arg_0005.input b/src/tests/parser/arg/arg_0005.input new file mode 100644 index 000000000..debda609a --- /dev/null +++ b/src/tests/parser/arg/arg_0005.input @@ -0,0 +1 @@ ++foo \ No newline at end of file diff --git a/src/tests/parser/arg/arg_0006.expected b/src/tests/parser/arg/arg_0006.expected new file mode 100644 index 000000000..8e2455ac9 --- /dev/null +++ b/src/tests/parser/arg/arg_0006.expected @@ -0,0 +1,3 @@ +Success! Final stack: + (Lean.Doc.Syntax.flag_off "-" `other) +All input consumed. \ No newline at end of file diff --git a/src/tests/parser/arg/arg_0006.input b/src/tests/parser/arg/arg_0006.input new file mode 100644 index 000000000..5fff7bd97 --- /dev/null +++ b/src/tests/parser/arg/arg_0006.input @@ -0,0 +1 @@ +-other \ No newline at end of file diff --git a/src/tests/parser/arg/arg_0007.expected b/src/tests/parser/arg/arg_0007.expected new file mode 100644 index 000000000..35abac62b --- /dev/null +++ b/src/tests/parser/arg/arg_0007.expected @@ -0,0 +1,4 @@ +Failure @2 (⟨1, 2⟩): expected no space before +Final stack: + (Lean.Doc.Syntax.flag_off "-" `other) +Remaining: "other" \ No newline at end of file diff --git a/src/tests/parser/arg/arg_0007.input b/src/tests/parser/arg/arg_0007.input new file mode 100644 index 000000000..88dc55e4a --- /dev/null +++ b/src/tests/parser/arg/arg_0007.input @@ -0,0 +1 @@ +- other \ No newline at end of file diff --git a/src/tests/parser/arg/arg_0008.expected b/src/tests/parser/arg/arg_0008.expected new file mode 100644 index 000000000..271999b4a --- /dev/null +++ b/src/tests/parser/arg/arg_0008.expected @@ -0,0 +1,9 @@ +Success! Final stack: + (Lean.Doc.Syntax.named + "(" + `x + ":=" + (Lean.Doc.Syntax.arg_num (num "1")) + ")") +Remaining: +"\n" \ No newline at end of file diff --git a/src/tests/parser/arg/arg_0008.input b/src/tests/parser/arg/arg_0008.input new file mode 100644 index 000000000..0970bcbc5 --- /dev/null +++ b/src/tests/parser/arg/arg_0008.input @@ -0,0 +1 @@ +(x:=1) diff --git a/src/tests/parser/arg/arg_0009.expected b/src/tests/parser/arg/arg_0009.expected new file mode 100644 index 000000000..53aa69cfe --- /dev/null +++ b/src/tests/parser/arg/arg_0009.expected @@ -0,0 +1,6 @@ +Success! Final stack: + (Lean.Doc.Syntax.named_no_paren + `x + ":=" + (Lean.Doc.Syntax.arg_ident `y)) +All input consumed. \ No newline at end of file diff --git a/src/tests/parser/arg/arg_0009.input b/src/tests/parser/arg/arg_0009.input new file mode 100644 index 000000000..14d0b3f1a --- /dev/null +++ b/src/tests/parser/arg/arg_0009.input @@ -0,0 +1 @@ +x:=y \ No newline at end of file diff --git a/src/tests/parser/arg/arg_0010.expected b/src/tests/parser/arg/arg_0010.expected new file mode 100644 index 000000000..84a495bdf --- /dev/null +++ b/src/tests/parser/arg/arg_0010.expected @@ -0,0 +1,8 @@ +Success! Final stack: + (Lean.Doc.Syntax.named + "(" + `x + ":=" + (Lean.Doc.Syntax.arg_ident `y) + ")") +All input consumed. \ No newline at end of file diff --git a/src/tests/parser/arg/arg_0010.input b/src/tests/parser/arg/arg_0010.input new file mode 100644 index 000000000..0d6154770 --- /dev/null +++ b/src/tests/parser/arg/arg_0010.input @@ -0,0 +1 @@ +(x:=y) \ No newline at end of file diff --git a/src/tests/parser/arg/arg_0011.expected b/src/tests/parser/arg/arg_0011.expected new file mode 100644 index 000000000..1d893bf95 --- /dev/null +++ b/src/tests/parser/arg/arg_0011.expected @@ -0,0 +1,6 @@ +Success! Final stack: + (Lean.Doc.Syntax.named_no_paren + `x + ":=" + (Lean.Doc.Syntax.arg_str (str "\"y\""))) +All input consumed. \ No newline at end of file diff --git a/src/tests/parser/arg/arg_0011.input b/src/tests/parser/arg/arg_0011.input new file mode 100644 index 000000000..e90562385 --- /dev/null +++ b/src/tests/parser/arg/arg_0011.input @@ -0,0 +1 @@ +x:="y" \ No newline at end of file diff --git a/src/tests/parser/arg/arg_0012.expected b/src/tests/parser/arg/arg_0012.expected new file mode 100644 index 000000000..035ea4ed1 --- /dev/null +++ b/src/tests/parser/arg/arg_0012.expected @@ -0,0 +1,7 @@ +Failure @3 (⟨1, 3⟩): unterminated string literal; expected identifier or numeral +Final stack: + • `x + • ":=" + • (Lean.Doc.Syntax.arg_str ) + +Remaining: "\"y" \ No newline at end of file diff --git a/src/tests/parser/arg/arg_0012.input b/src/tests/parser/arg/arg_0012.input new file mode 100644 index 000000000..a94983251 --- /dev/null +++ b/src/tests/parser/arg/arg_0012.input @@ -0,0 +1 @@ +x:="y \ No newline at end of file diff --git a/src/tests/parser/arg/arg_0013.expected b/src/tests/parser/arg/arg_0013.expected new file mode 100644 index 000000000..289e11307 --- /dev/null +++ b/src/tests/parser/arg/arg_0013.expected @@ -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 ) + ) \ No newline at end of file diff --git a/src/tests/parser/arg/arg_0013.input b/src/tests/parser/arg/arg_0013.input new file mode 100644 index 000000000..45cb12c92 --- /dev/null +++ b/src/tests/parser/arg/arg_0013.input @@ -0,0 +1 @@ +(x:="y) \ No newline at end of file diff --git a/src/tests/parser/arg/arg_0014.expected b/src/tests/parser/arg/arg_0014.expected new file mode 100644 index 000000000..fa5d18aee --- /dev/null +++ b/src/tests/parser/arg/arg_0014.expected @@ -0,0 +1,4 @@ +Success! Final stack: + (Lean.Doc.Syntax.anon + (Lean.Doc.Syntax.arg_num (num "42"))) +All input consumed. \ No newline at end of file diff --git a/src/tests/parser/arg/arg_0014.input b/src/tests/parser/arg/arg_0014.input new file mode 100644 index 000000000..f70d7bba4 --- /dev/null +++ b/src/tests/parser/arg/arg_0014.input @@ -0,0 +1 @@ +42 \ No newline at end of file diff --git a/src/tests/parser/arg/arg_0015.expected b/src/tests/parser/arg/arg_0015.expected new file mode 100644 index 000000000..7e5eadbb8 --- /dev/null +++ b/src/tests/parser/arg/arg_0015.expected @@ -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 + "(" + + + (Lean.Doc.Syntax.arg_str ) + ) \ No newline at end of file diff --git a/src/tests/parser/arg/arg_0015.input b/src/tests/parser/arg/arg_0015.input new file mode 100644 index 000000000..93022ef3e --- /dev/null +++ b/src/tests/parser/arg/arg_0015.input @@ -0,0 +1 @@ +(42) \ No newline at end of file diff --git a/src/tests/parser/arg/arg_0016.expected b/src/tests/parser/arg/arg_0016.expected new file mode 100644 index 000000000..a9100b217 --- /dev/null +++ b/src/tests/parser/arg/arg_0016.expected @@ -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 + + (Lean.Doc.Syntax.arg_str ) + ) \ No newline at end of file diff --git a/src/tests/parser/arg/arg_0016.input b/src/tests/parser/arg/arg_0016.input new file mode 100644 index 000000000..b4e4f9554 --- /dev/null +++ b/src/tests/parser/arg/arg_0016.input @@ -0,0 +1 @@ +(x 42) \ No newline at end of file diff --git a/src/tests/parser/arg/arg_0017.expected b/src/tests/parser/arg/arg_0017.expected new file mode 100644 index 000000000..166a8bb2d --- /dev/null +++ b/src/tests/parser/arg/arg_0017.expected @@ -0,0 +1,9 @@ +Failure @8 (⟨1, 8⟩): expected ')' +Final stack: + (Lean.Doc.Syntax.named + "(" + `x + ":=" + (Lean.Doc.Syntax.arg_num (num "42")) + ) +Remaining: "\n)" \ No newline at end of file diff --git a/src/tests/parser/arg/arg_0017.input b/src/tests/parser/arg/arg_0017.input new file mode 100644 index 000000000..f4bad7dba --- /dev/null +++ b/src/tests/parser/arg/arg_0017.input @@ -0,0 +1,2 @@ +(x := 42 +) \ No newline at end of file diff --git a/src/tests/parser/arg/arg_0018.expected b/src/tests/parser/arg/arg_0018.expected new file mode 100644 index 000000000..c59c669b8 --- /dev/null +++ b/src/tests/parser/arg/arg_0018.expected @@ -0,0 +1,9 @@ +Failure @8 (⟨1, 8⟩): expected ')' +Final stack: + (Lean.Doc.Syntax.named + "(" + `x + ":=" + (Lean.Doc.Syntax.arg_num (num "42")) + ) +Remaining: "\na" \ No newline at end of file diff --git a/src/tests/parser/arg/arg_0018.input b/src/tests/parser/arg/arg_0018.input new file mode 100644 index 000000000..50b0fa2b5 --- /dev/null +++ b/src/tests/parser/arg/arg_0018.input @@ -0,0 +1,2 @@ +(x := 42 +a \ No newline at end of file diff --git a/src/tests/parser/args/args_0001.expected b/src/tests/parser/args/args_0001.expected new file mode 100644 index 000000000..8cf69af3b --- /dev/null +++ b/src/tests/parser/args/args_0001.expected @@ -0,0 +1,5 @@ +Success! Final stack: + [(Lean.Doc.Syntax.anon + (Lean.Doc.Syntax.arg_num (num "43")))] +Remaining: +"\n\"foo\"" \ No newline at end of file diff --git a/src/tests/parser/args/args_0001.input b/src/tests/parser/args/args_0001.input new file mode 100644 index 000000000..4c37dc640 --- /dev/null +++ b/src/tests/parser/args/args_0001.input @@ -0,0 +1,2 @@ +43 +"foo" \ No newline at end of file diff --git a/src/tests/parser/args/args_0002.expected b/src/tests/parser/args/args_0002.expected new file mode 100644 index 000000000..81bd7bc6f --- /dev/null +++ b/src/tests/parser/args/args_0002.expected @@ -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" \ No newline at end of file diff --git a/src/tests/parser/args/args_0002.input b/src/tests/parser/args/args_0002.input new file mode 100644 index 000000000..d504d62b7 --- /dev/null +++ b/src/tests/parser/args/args_0002.input @@ -0,0 +1,2 @@ +dialect:="chicken" 43 +foo \ No newline at end of file diff --git a/src/tests/parser/args/args_0003.expected b/src/tests/parser/args/args_0003.expected new file mode 100644 index 000000000..6edb3eea0 --- /dev/null +++ b/src/tests/parser/args/args_0003.expected @@ -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)" \ No newline at end of file diff --git a/src/tests/parser/args/args_0003.input b/src/tests/parser/args/args_0003.input new file mode 100644 index 000000000..cc8949933 --- /dev/null +++ b/src/tests/parser/args/args_0003.input @@ -0,0 +1,2 @@ +dialect:="chicken" 43 +(foo) \ No newline at end of file diff --git a/src/tests/parser/block/block_0001.expected b/src/tests/parser/block/block_0001.expected new file mode 100644 index 000000000..755ffd97c --- /dev/null +++ b/src/tests/parser/block/block_0001.expected @@ -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. \ No newline at end of file diff --git a/src/tests/parser/block/block_0001.input b/src/tests/parser/block/block_0001.input new file mode 100644 index 000000000..4df9d39f7 --- /dev/null +++ b/src/tests/parser/block/block_0001.input @@ -0,0 +1,8 @@ + * Here's a bullet + * and another with some code in it + ````lean + hey + + there + ```` + * and another one diff --git a/src/tests/parser/block/block_0002.expected b/src/tests/parser/block/block_0002.expected new file mode 100644 index 000000000..f1b9ec73b --- /dev/null +++ b/src/tests/parser/block/block_0002.expected @@ -0,0 +1,4 @@ +Success! Final stack: + (Lean.Doc.Syntax.command "{" `test [] "}") +Remaining: +"Here's a paragraph." \ No newline at end of file diff --git a/src/tests/parser/block/block_0002.input b/src/tests/parser/block/block_0002.input new file mode 100644 index 000000000..fd9bf99e3 --- /dev/null +++ b/src/tests/parser/block/block_0002.input @@ -0,0 +1,2 @@ +{test} +Here's a paragraph. \ No newline at end of file diff --git a/src/tests/parser/block/block_0003.expected b/src/tests/parser/block/block_0003.expected new file mode 100644 index 000000000..7af7884e3 --- /dev/null +++ b/src/tests/parser/block/block_0003.expected @@ -0,0 +1,4 @@ +Success! Final stack: + (Lean.Doc.Syntax.command "{" `test [] "}") +Remaining: +" Here's a paragraph." \ No newline at end of file diff --git a/src/tests/parser/block/block_0003.input b/src/tests/parser/block/block_0003.input new file mode 100644 index 000000000..abea64d71 --- /dev/null +++ b/src/tests/parser/block/block_0003.input @@ -0,0 +1,2 @@ +{test} + Here's a paragraph. \ No newline at end of file diff --git a/src/tests/parser/block/block_0004.expected b/src/tests/parser/block/block_0004.expected new file mode 100644 index 000000000..7af7884e3 --- /dev/null +++ b/src/tests/parser/block/block_0004.expected @@ -0,0 +1,4 @@ +Success! Final stack: + (Lean.Doc.Syntax.command "{" `test [] "}") +Remaining: +" Here's a paragraph." \ No newline at end of file diff --git a/src/tests/parser/block/block_0004.input b/src/tests/parser/block/block_0004.input new file mode 100644 index 000000000..abea64d71 --- /dev/null +++ b/src/tests/parser/block/block_0004.input @@ -0,0 +1,2 @@ +{test} + Here's a paragraph. \ No newline at end of file diff --git a/src/tests/parser/block/block_0005.expected b/src/tests/parser/block/block_0005.expected new file mode 100644 index 000000000..f1b9ec73b --- /dev/null +++ b/src/tests/parser/block/block_0005.expected @@ -0,0 +1,4 @@ +Success! Final stack: + (Lean.Doc.Syntax.command "{" `test [] "}") +Remaining: +"Here's a paragraph." \ No newline at end of file diff --git a/src/tests/parser/block/block_0005.input b/src/tests/parser/block/block_0005.input new file mode 100644 index 000000000..fd9bf99e3 --- /dev/null +++ b/src/tests/parser/block/block_0005.input @@ -0,0 +1,2 @@ +{test} +Here's a paragraph. \ No newline at end of file diff --git a/src/tests/parser/block/block_0006.expected b/src/tests/parser/block/block_0006.expected new file mode 100644 index 000000000..44c01444d --- /dev/null +++ b/src/tests/parser/block/block_0006.expected @@ -0,0 +1,4 @@ +Success! Final stack: + (Lean.Doc.Syntax.command "{" `test [] "}") +Remaining: +"> Here's a blockquote\n\n with multiple paras\n\nthat ends" \ No newline at end of file diff --git a/src/tests/parser/block/block_0006.input b/src/tests/parser/block/block_0006.input new file mode 100644 index 000000000..64bb700af --- /dev/null +++ b/src/tests/parser/block/block_0006.input @@ -0,0 +1,6 @@ +{test} +> Here's a blockquote + + with multiple paras + +that ends \ No newline at end of file diff --git a/src/tests/parser/block/block_0007.expected b/src/tests/parser/block/block_0007.expected new file mode 100644 index 000000000..da8e1f2e9 --- /dev/null +++ b/src/tests/parser/block/block_0007.expected @@ -0,0 +1,15 @@ +2 failures: + @36 (⟨3, 28⟩): expected token + "" + @36 (⟨3, 28⟩): unexpected end of input; expected '![', '$$', '$', '[' or '[^' + "" + +Final stack: + (Lean.Doc.Syntax.para + "para{" + [(Lean.Doc.Syntax.role + "{" + + "[" + [(Lean.Doc.Syntax.footnote )] + "]")]) \ No newline at end of file diff --git a/src/tests/parser/block/block_0007.input b/src/tests/parser/block/block_0007.input new file mode 100644 index 000000000..90abe7906 --- /dev/null +++ b/src/tests/parser/block/block_0007.input @@ -0,0 +1,3 @@ +{ +test} +Here's a modified paragraph. \ No newline at end of file diff --git a/src/tests/parser/block/block_0008.expected b/src/tests/parser/block/block_0008.expected new file mode 100644 index 000000000..e16be6660 --- /dev/null +++ b/src/tests/parser/block/block_0008.expected @@ -0,0 +1,15 @@ +2 failures: + @37 (⟨3, 28⟩): expected token + "" + @37 (⟨3, 28⟩): unexpected end of input; expected '![', '$$', '$', '[' or '[^' + "" + +Final stack: + (Lean.Doc.Syntax.para + "para{" + [(Lean.Doc.Syntax.role + "{" + + "[" + [(Lean.Doc.Syntax.footnote )] + "]")]) \ No newline at end of file diff --git a/src/tests/parser/block/block_0008.input b/src/tests/parser/block/block_0008.input new file mode 100644 index 000000000..997a2d049 --- /dev/null +++ b/src/tests/parser/block/block_0008.input @@ -0,0 +1,3 @@ +{ + test} +Here's a modified paragraph. \ No newline at end of file diff --git a/src/tests/parser/block/block_0009.expected b/src/tests/parser/block/block_0009.expected new file mode 100644 index 000000000..593ab4154 --- /dev/null +++ b/src/tests/parser/block/block_0009.expected @@ -0,0 +1,15 @@ +2 failures: + @44 (⟨4, 28⟩): expected token + "" + @44 (⟨4, 28⟩): unexpected end of input; expected '![', '$$', '$', '[' or '[^' + "" + +Final stack: + (Lean.Doc.Syntax.para + "para{" + [(Lean.Doc.Syntax.role + "{" + + "[" + [(Lean.Doc.Syntax.footnote )] + "]")]) \ No newline at end of file diff --git a/src/tests/parser/block/block_0009.input b/src/tests/parser/block/block_0009.input new file mode 100644 index 000000000..261c6bc86 --- /dev/null +++ b/src/tests/parser/block/block_0009.input @@ -0,0 +1,4 @@ +{ + test +arg} +Here's a modified paragraph. \ No newline at end of file diff --git a/src/tests/parser/block/block_0010.expected b/src/tests/parser/block/block_0010.expected new file mode 100644 index 000000000..9b0169141 --- /dev/null +++ b/src/tests/parser/block/block_0010.expected @@ -0,0 +1,15 @@ +2 failures: + @45 (⟨4, 28⟩): expected token + "" + @45 (⟨4, 28⟩): unexpected end of input; expected '![', '$$', '$', '[' or '[^' + "" + +Final stack: + (Lean.Doc.Syntax.para + "para{" + [(Lean.Doc.Syntax.role + "{" + + "[" + [(Lean.Doc.Syntax.footnote )] + "]")]) \ No newline at end of file diff --git a/src/tests/parser/block/block_0010.input b/src/tests/parser/block/block_0010.input new file mode 100644 index 000000000..a6bccc014 --- /dev/null +++ b/src/tests/parser/block/block_0010.input @@ -0,0 +1,4 @@ +{ + test + arg} +Here's a modified paragraph. \ No newline at end of file diff --git a/src/tests/parser/block/block_0011.expected b/src/tests/parser/block/block_0011.expected new file mode 100644 index 000000000..98d23d662 --- /dev/null +++ b/src/tests/parser/block/block_0011.expected @@ -0,0 +1,15 @@ +2 failures: + @19 (⟨6, 0⟩): '{'; expected '![', '$$', '$', '[' or '[^' + "Here's a paragraph." + @19 (⟨6, 0⟩): expected token + "Here's a paragraph." + +Final stack: + (Lean.Doc.Syntax.para + "para{" + [(Lean.Doc.Syntax.role + "{" + + "[" + [(Lean.Doc.Syntax.footnote )] + "]")]) \ No newline at end of file diff --git a/src/tests/parser/block/block_0011.input b/src/tests/parser/block/block_0011.input new file mode 100644 index 000000000..7594e9a0a --- /dev/null +++ b/src/tests/parser/block/block_0011.input @@ -0,0 +1,6 @@ +{ + test + arg} + + +Here's a paragraph. \ No newline at end of file diff --git a/src/tests/parser/block/block_0012.expected b/src/tests/parser/block/block_0012.expected new file mode 100644 index 000000000..5ae56c0c7 --- /dev/null +++ b/src/tests/parser/block/block_0012.expected @@ -0,0 +1,84 @@ +Success! Final stack: + (Lean.Doc.Syntax.ul + "ul{" + [(Lean.Doc.Syntax.li + "*" + [(Lean.Doc.Syntax.para + "para{" + [(Lean.Doc.Syntax.code + "`" + (str "\"structure\"") + "`") + (Lean.Doc.Syntax.text (str "\" and \"")) + (Lean.Doc.Syntax.code + "`" + (str "\"inductive\"") + "`") + (Lean.Doc.Syntax.text + (str "\" commands\""))] + "}") + (Lean.Doc.Syntax.ul + "ul{" + [(Lean.Doc.Syntax.li + "*" + [(Lean.Doc.Syntax.para + "para{" + [(Lean.Doc.Syntax.link + "[" + [(Lean.Doc.Syntax.text + (str "\"#5842\""))] + "]" + (Lean.Doc.Syntax.url + "(" + (str + "\"https://github.com/leanprover/lean4/pull/5842\"") + ")")) + (Lean.Doc.Syntax.text + (str "\" and \"")) + (Lean.Doc.Syntax.link + "[" + [(Lean.Doc.Syntax.text + (str "\"#5783\""))] + "]" + (Lean.Doc.Syntax.url + "(" + (str + "\"https://github.com/leanprover/lean4/pull/5783\"") + ")")) + (Lean.Doc.Syntax.text + (str + "\" implement a feature where the \"")) + (Lean.Doc.Syntax.code + "`" + (str "\"structure\"") + "`") + (Lean.Doc.Syntax.text + (str + "\" command can now define recursive inductive types:\""))] + "}") + (Lean.Doc.Syntax.codeblock + "```" + [`lean []] + "\n" + (str + "\"structure Tree where\\n n : Nat\\n children : Fin n → Tree\\n\\ndef Tree.size : Tree → Nat\\n | {n, children} => Id.run do\\n let mut s := 0\\n for h : i in [0 : n] do\\n s := s + (children ⟨i, h.2⟩).size\\n pure s\\n\"") + "```")]) + (Lean.Doc.Syntax.li + "*" + [(Lean.Doc.Syntax.para + "para{" + [(Lean.Doc.Syntax.link + "[" + [(Lean.Doc.Syntax.text + (str "\"#5814\""))] + "]" + (Lean.Doc.Syntax.url + "(" + (str + "\"https://github.com/leanprover/lean4/pull/5814\"") + ")")) + (Lean.Doc.Syntax.text (str "\" \""))] + "}")])] + "}")])] + "}") +All input consumed. \ No newline at end of file diff --git a/src/tests/parser/block/block_0012.input b/src/tests/parser/block/block_0012.input new file mode 100644 index 000000000..0262cfe75 --- /dev/null +++ b/src/tests/parser/block/block_0012.input @@ -0,0 +1,15 @@ +* `structure` and `inductive` commands + * [#5842](https://github.com/leanprover/lean4/pull/5842) and [#5783](https://github.com/leanprover/lean4/pull/5783) implement a feature where the `structure` command can now define recursive inductive types: + ```lean + structure Tree where + n : Nat + children : Fin n → Tree + + def Tree.size : Tree → Nat + | {n, children} => Id.run do + let mut s := 0 + for h : i in [0 : n] do + s := s + (children ⟨i, h.2⟩).size + pure s + ``` + * [#5814](https://github.com/leanprover/lean4/pull/5814) \ No newline at end of file diff --git a/src/tests/parser/block/blocks/blocks_0001.expected b/src/tests/parser/block/blocks/blocks_0001.expected new file mode 100644 index 000000000..f9979cd6f --- /dev/null +++ b/src/tests/parser/block/blocks/blocks_0001.expected @@ -0,0 +1,12 @@ +Success! Final stack: + [(Lean.Doc.Syntax.para + "para{" + [(Lean.Doc.Syntax.text + (str + "\"This is just some textual content. How is it?\""))] + "}") + (Lean.Doc.Syntax.para + "para{" + [(Lean.Doc.Syntax.text (str "\"More?\""))] + "}")] +All input consumed. \ No newline at end of file diff --git a/src/tests/parser/block/blocks/blocks_0001.input b/src/tests/parser/block/blocks/blocks_0001.input new file mode 100644 index 000000000..969555e23 --- /dev/null +++ b/src/tests/parser/block/blocks/blocks_0001.input @@ -0,0 +1,3 @@ +This is just some textual content. How is it? + +More? \ No newline at end of file diff --git a/src/tests/parser/block/blocks/blocks_0002.expected b/src/tests/parser/block/blocks/blocks_0002.expected new file mode 100644 index 000000000..5c9f66c66 --- /dev/null +++ b/src/tests/parser/block/blocks/blocks_0002.expected @@ -0,0 +1,12 @@ +Success! Final stack: + [(Lean.Doc.Syntax.para + "para{" + [(Lean.Doc.Syntax.text + (str "\"Newlines are preserved\"")) + (Lean.Doc.Syntax.linebreak + "line!" + (str "\"\\n\"")) + (Lean.Doc.Syntax.text + (str "\"in paragraphs.\""))] + "}")] +All input consumed. \ No newline at end of file diff --git a/src/tests/parser/block/blocks/blocks_0002.input b/src/tests/parser/block/blocks/blocks_0002.input new file mode 100644 index 000000000..299045673 --- /dev/null +++ b/src/tests/parser/block/blocks/blocks_0002.input @@ -0,0 +1,2 @@ +Newlines are preserved +in paragraphs. \ No newline at end of file diff --git a/src/tests/parser/block/blocks/blocks_0003.expected b/src/tests/parser/block/blocks/blocks_0003.expected new file mode 100644 index 000000000..e332c41af --- /dev/null +++ b/src/tests/parser/block/blocks/blocks_0003.expected @@ -0,0 +1,23 @@ +Success! Final stack: + [(Lean.Doc.Syntax.para + "para{" + [(Lean.Doc.Syntax.text + (str + "\"I can describe lists like this one:\""))] + "}") + (Lean.Doc.Syntax.ul + "ul{" + [(Lean.Doc.Syntax.li + "*" + [(Lean.Doc.Syntax.para + "para{" + [(Lean.Doc.Syntax.text (str "\"a\""))] + "}")]) + (Lean.Doc.Syntax.li + "*" + [(Lean.Doc.Syntax.para + "para{" + [(Lean.Doc.Syntax.text (str "\"b\""))] + "}")])] + "}")] +All input consumed. \ No newline at end of file diff --git a/src/tests/parser/block/blocks/blocks_0003.input b/src/tests/parser/block/blocks/blocks_0003.input new file mode 100644 index 000000000..d6a59d7b0 --- /dev/null +++ b/src/tests/parser/block/blocks/blocks_0003.input @@ -0,0 +1,4 @@ +I can describe lists like this one: + +* a +* b \ No newline at end of file diff --git a/src/tests/parser/block/blocks/blocks_0004.expected b/src/tests/parser/block/blocks/blocks_0004.expected new file mode 100644 index 000000000..2d0cd8c73 --- /dev/null +++ b/src/tests/parser/block/blocks/blocks_0004.expected @@ -0,0 +1,47 @@ +Success! Final stack: + [(Lean.Doc.Syntax.ul + "ul{" + [(Lean.Doc.Syntax.li + "*" + [(Lean.Doc.Syntax.ul + "ul{" + [(Lean.Doc.Syntax.li + "*" + [(Lean.Doc.Syntax.para + "para{" + [(Lean.Doc.Syntax.text + (str "\"A1\""))] + "}")]) + (Lean.Doc.Syntax.li + "*" + [(Lean.Doc.Syntax.para + "para{" + [(Lean.Doc.Syntax.text + (str "\"A2\""))] + "}")])] + "}")]) + (Lean.Doc.Syntax.li + "*" + [(Lean.Doc.Syntax.para + "para{" + [(Lean.Doc.Syntax.text (str "\"B\""))] + "}") + (Lean.Doc.Syntax.ul + "ul{" + [(Lean.Doc.Syntax.li + "*" + [(Lean.Doc.Syntax.para + "para{" + [(Lean.Doc.Syntax.text + (str "\"B1\""))] + "}")]) + (Lean.Doc.Syntax.li + "*" + [(Lean.Doc.Syntax.para + "para{" + [(Lean.Doc.Syntax.text + (str "\"B2\""))] + "}")])] + "}")])] + "}")] +All input consumed. \ No newline at end of file diff --git a/src/tests/parser/block/blocks/blocks_0004.input b/src/tests/parser/block/blocks/blocks_0004.input new file mode 100644 index 000000000..01fd606d6 --- /dev/null +++ b/src/tests/parser/block/blocks/blocks_0004.input @@ -0,0 +1,5 @@ +* * A1 + * A2 +* B + * B1 + * B2 \ No newline at end of file diff --git a/src/tests/parser/block/blocks/blocks_0005.expected b/src/tests/parser/block/blocks/blocks_0005.expected new file mode 100644 index 000000000..af10e3c5e --- /dev/null +++ b/src/tests/parser/block/blocks/blocks_0005.expected @@ -0,0 +1,38 @@ +Success! Final stack: + [(Lean.Doc.Syntax.ul + "ul{" + [(Lean.Doc.Syntax.li + "*" + [(Lean.Doc.Syntax.ul + "ul{" + [(Lean.Doc.Syntax.li + "*" + [(Lean.Doc.Syntax.para + "para{" + [(Lean.Doc.Syntax.text + (str "\"A1\""))] + "}")]) + (Lean.Doc.Syntax.li + "*" + [(Lean.Doc.Syntax.para + "para{" + [(Lean.Doc.Syntax.text (str "\"A2\"")) + (Lean.Doc.Syntax.linebreak + "line!" + (str "\"\\n\""))] + "}")])] + "}")]) + (Lean.Doc.Syntax.li + "*" + [(Lean.Doc.Syntax.ul + "ul{" + [(Lean.Doc.Syntax.li + "*" + [(Lean.Doc.Syntax.para + "para{" + [(Lean.Doc.Syntax.text + (str "\"B1\""))] + "}")])] + "}")])] + "}")] +All input consumed. \ No newline at end of file diff --git a/src/tests/parser/block/blocks/blocks_0005.input b/src/tests/parser/block/blocks/blocks_0005.input new file mode 100644 index 000000000..ec098bb68 --- /dev/null +++ b/src/tests/parser/block/blocks/blocks_0005.input @@ -0,0 +1,5 @@ +* + * A1 + * A2 +* + * B1 \ No newline at end of file diff --git a/src/tests/parser/block/blocks/blocks_0006.expected b/src/tests/parser/block/blocks/blocks_0006.expected new file mode 100644 index 000000000..af10e3c5e --- /dev/null +++ b/src/tests/parser/block/blocks/blocks_0006.expected @@ -0,0 +1,38 @@ +Success! Final stack: + [(Lean.Doc.Syntax.ul + "ul{" + [(Lean.Doc.Syntax.li + "*" + [(Lean.Doc.Syntax.ul + "ul{" + [(Lean.Doc.Syntax.li + "*" + [(Lean.Doc.Syntax.para + "para{" + [(Lean.Doc.Syntax.text + (str "\"A1\""))] + "}")]) + (Lean.Doc.Syntax.li + "*" + [(Lean.Doc.Syntax.para + "para{" + [(Lean.Doc.Syntax.text (str "\"A2\"")) + (Lean.Doc.Syntax.linebreak + "line!" + (str "\"\\n\""))] + "}")])] + "}")]) + (Lean.Doc.Syntax.li + "*" + [(Lean.Doc.Syntax.ul + "ul{" + [(Lean.Doc.Syntax.li + "*" + [(Lean.Doc.Syntax.para + "para{" + [(Lean.Doc.Syntax.text + (str "\"B1\""))] + "}")])] + "}")])] + "}")] +All input consumed. \ No newline at end of file diff --git a/src/tests/parser/block/blocks/blocks_0006.input b/src/tests/parser/block/blocks/blocks_0006.input new file mode 100644 index 000000000..922dac70e --- /dev/null +++ b/src/tests/parser/block/blocks/blocks_0006.input @@ -0,0 +1,5 @@ +* + * A1 + * A2 +* + * B1 \ No newline at end of file diff --git a/src/tests/parser/block/blocks/blocks_0007.expected b/src/tests/parser/block/blocks/blocks_0007.expected new file mode 100644 index 000000000..863b919e9 --- /dev/null +++ b/src/tests/parser/block/blocks/blocks_0007.expected @@ -0,0 +1,11 @@ +Failure @2 (⟨2, 0⟩): ':'; expected %%% (at line beginning) or expected column at least 1 +Final stack: + [(Lean.Doc.Syntax.ul + "ul{" + [(Lean.Doc.Syntax.li + "*" + [(Lean.Doc.Syntax.metadata_block + + ) + ])])] +Remaining: "abc" \ No newline at end of file diff --git a/src/tests/parser/block/blocks/blocks_0007.input b/src/tests/parser/block/blocks/blocks_0007.input new file mode 100644 index 000000000..c869ff73c --- /dev/null +++ b/src/tests/parser/block/blocks/blocks_0007.input @@ -0,0 +1,2 @@ +* +abc \ No newline at end of file diff --git a/src/tests/parser/block/blocks/blocks_0008.expected b/src/tests/parser/block/blocks/blocks_0008.expected new file mode 100644 index 000000000..84bad49bb --- /dev/null +++ b/src/tests/parser/block/blocks/blocks_0008.expected @@ -0,0 +1,15 @@ +Success! Final stack: + [(Lean.Doc.Syntax.ul + "ul{" + [(Lean.Doc.Syntax.li + "*" + [(Lean.Doc.Syntax.para + "para{" + [(Lean.Doc.Syntax.text (str "\"abc\""))] + "}") + (Lean.Doc.Syntax.para + "para{" + [(Lean.Doc.Syntax.text (str "\"def\""))] + "}")])] + "}")] +All input consumed. \ No newline at end of file diff --git a/src/tests/parser/block/blocks/blocks_0008.input b/src/tests/parser/block/blocks/blocks_0008.input new file mode 100644 index 000000000..3f9863c17 --- /dev/null +++ b/src/tests/parser/block/blocks/blocks_0008.input @@ -0,0 +1,4 @@ +* + abc + + def \ No newline at end of file diff --git a/src/tests/parser/block/blocks/blocks_0009.expected b/src/tests/parser/block/blocks/blocks_0009.expected new file mode 100644 index 000000000..63bb41db6 --- /dev/null +++ b/src/tests/parser/block/blocks/blocks_0009.expected @@ -0,0 +1,15 @@ +Success! Final stack: + [(Lean.Doc.Syntax.ul + "ul{" + [(Lean.Doc.Syntax.li + "*" + [(Lean.Doc.Syntax.para + "para{" + [(Lean.Doc.Syntax.text (str "\"abc\""))] + "}")])] + "}") + (Lean.Doc.Syntax.para + "para{" + [(Lean.Doc.Syntax.text (str "\"def\""))] + "}")] +All input consumed. \ No newline at end of file diff --git a/src/tests/parser/block/blocks/blocks_0009.input b/src/tests/parser/block/blocks/blocks_0009.input new file mode 100644 index 000000000..c5c569ead --- /dev/null +++ b/src/tests/parser/block/blocks/blocks_0009.input @@ -0,0 +1,4 @@ +* + abc + +def \ No newline at end of file diff --git a/src/tests/parser/block/blocks/blocks_0010.expected b/src/tests/parser/block/blocks/blocks_0010.expected new file mode 100644 index 000000000..1df295971 --- /dev/null +++ b/src/tests/parser/block/blocks/blocks_0010.expected @@ -0,0 +1,20 @@ +Success! Final stack: + [(Lean.Doc.Syntax.ul + "ul{" + [(Lean.Doc.Syntax.li + "*" + [(Lean.Doc.Syntax.para + "para{" + [(Lean.Doc.Syntax.text (str "\"foo\""))] + "}")]) + (Lean.Doc.Syntax.li + "*" + [(Lean.Doc.Syntax.para + "para{" + [(Lean.Doc.Syntax.text (str "\"bar\"")) + (Lean.Doc.Syntax.linebreak + "line!" + (str "\"\\n\""))] + "}")])] + "}")] +All input consumed. \ No newline at end of file diff --git a/src/tests/parser/block/blocks/blocks_0010.input b/src/tests/parser/block/blocks/blocks_0010.input new file mode 100644 index 000000000..0beb3ff0d --- /dev/null +++ b/src/tests/parser/block/blocks/blocks_0010.input @@ -0,0 +1,2 @@ +* foo +* bar diff --git a/src/tests/parser/block/blocks/blocks_0011.expected b/src/tests/parser/block/blocks/blocks_0011.expected new file mode 100644 index 000000000..83fdaf55d --- /dev/null +++ b/src/tests/parser/block/blocks/blocks_0011.expected @@ -0,0 +1,13 @@ +Success! Final stack: + [(Lean.Doc.Syntax.blockquote + ">" + [(Lean.Doc.Syntax.ul + "ul{" + [(Lean.Doc.Syntax.li + "*" + [(Lean.Doc.Syntax.para + "para{" + [(Lean.Doc.Syntax.text (str "\"foo\""))] + "}")])] + "}")])] +All input consumed. \ No newline at end of file diff --git a/src/tests/parser/block/blocks/blocks_0011.input b/src/tests/parser/block/blocks/blocks_0011.input new file mode 100644 index 000000000..64c346a42 --- /dev/null +++ b/src/tests/parser/block/blocks/blocks_0011.input @@ -0,0 +1 @@ +> * foo \ No newline at end of file diff --git a/src/tests/parser/block/blocks/blocks_0012.expected b/src/tests/parser/block/blocks/blocks_0012.expected new file mode 100644 index 000000000..20e487547 --- /dev/null +++ b/src/tests/parser/block/blocks/blocks_0012.expected @@ -0,0 +1,16 @@ +Success! Final stack: + [(Lean.Doc.Syntax.blockquote + ">" + [(Lean.Doc.Syntax.ol + "ol(" + (num "1") + ")" + "{" + [(Lean.Doc.Syntax.li + "1." + [(Lean.Doc.Syntax.para + "para{" + [(Lean.Doc.Syntax.text (str "\"foo\""))] + "}")])] + "}")])] +All input consumed. \ No newline at end of file diff --git a/src/tests/parser/block/blocks/blocks_0012.input b/src/tests/parser/block/blocks/blocks_0012.input new file mode 100644 index 000000000..52b2693d0 --- /dev/null +++ b/src/tests/parser/block/blocks/blocks_0012.input @@ -0,0 +1 @@ +> 1. foo \ No newline at end of file diff --git a/src/tests/parser/block/blocks/blocks_0013.expected b/src/tests/parser/block/blocks/blocks_0013.expected new file mode 100644 index 000000000..f156ea4e2 --- /dev/null +++ b/src/tests/parser/block/blocks/blocks_0013.expected @@ -0,0 +1,22 @@ +Success! Final stack: + [(Lean.Doc.Syntax.blockquote + ">" + [(Lean.Doc.Syntax.ul + "ul{" + [(Lean.Doc.Syntax.li + "*" + [(Lean.Doc.Syntax.para + "para{" + [(Lean.Doc.Syntax.text (str "\"foo\""))] + "}")])] + "}") + (Lean.Doc.Syntax.ul + "ul{" + [(Lean.Doc.Syntax.li + "*" + [(Lean.Doc.Syntax.para + "para{" + [(Lean.Doc.Syntax.text (str "\"foo\""))] + "}")])] + "}")])] +All input consumed. \ No newline at end of file diff --git a/src/tests/parser/block/blocks/blocks_0013.input b/src/tests/parser/block/blocks/blocks_0013.input new file mode 100644 index 000000000..d8da76684 --- /dev/null +++ b/src/tests/parser/block/blocks/blocks_0013.input @@ -0,0 +1,4 @@ +> * foo + + + * foo \ No newline at end of file diff --git a/src/tests/parser/block/blocks/blocks_0014.expected b/src/tests/parser/block/blocks/blocks_0014.expected new file mode 100644 index 000000000..f5aedb1ea --- /dev/null +++ b/src/tests/parser/block/blocks/blocks_0014.expected @@ -0,0 +1,23 @@ +Success! Final stack: + [(Lean.Doc.Syntax.blockquote + ">" + [(Lean.Doc.Syntax.para + "para{" + [(Lean.Doc.Syntax.text + (str "\"I like quotes\""))] + "}") + (Lean.Doc.Syntax.ul + "ul{" + [(Lean.Doc.Syntax.li + "*" + [(Lean.Doc.Syntax.para + "para{" + [(Lean.Doc.Syntax.text + (str "\"Also with lists in them\""))] + "}")])] + "}")]) + (Lean.Doc.Syntax.para + "para{" + [(Lean.Doc.Syntax.text (str "\"Abc\""))] + "}")] +All input consumed. \ No newline at end of file diff --git a/src/tests/parser/block/blocks/blocks_0014.input b/src/tests/parser/block/blocks/blocks_0014.input new file mode 100644 index 000000000..d79b1d807 --- /dev/null +++ b/src/tests/parser/block/blocks/blocks_0014.input @@ -0,0 +1,4 @@ +> I like quotes + * Also with lists in them + +Abc \ No newline at end of file diff --git a/src/tests/parser/block/blocks/blocks_0015.expected b/src/tests/parser/block/blocks/blocks_0015.expected new file mode 100644 index 000000000..e29e740c8 --- /dev/null +++ b/src/tests/parser/block/blocks/blocks_0015.expected @@ -0,0 +1,19 @@ +Success! Final stack: + [(Lean.Doc.Syntax.blockquote + ">" + [(Lean.Doc.Syntax.ul + "ul{" + [(Lean.Doc.Syntax.li + "*" + [(Lean.Doc.Syntax.para + "para{" + [(Lean.Doc.Syntax.text (str "\"foo\""))] + "}")]) + (Lean.Doc.Syntax.li + "*" + [(Lean.Doc.Syntax.para + "para{" + [(Lean.Doc.Syntax.text (str "\"foo\""))] + "}")])] + "}")])] +All input consumed. \ No newline at end of file diff --git a/src/tests/parser/block/blocks/blocks_0015.input b/src/tests/parser/block/blocks/blocks_0015.input new file mode 100644 index 000000000..01bc81c9d --- /dev/null +++ b/src/tests/parser/block/blocks/blocks_0015.input @@ -0,0 +1,4 @@ +> * foo + + + * foo \ No newline at end of file diff --git a/src/tests/parser/block/blocks/blocks_0016.expected b/src/tests/parser/block/blocks/blocks_0016.expected new file mode 100644 index 000000000..13ff9a0f2 --- /dev/null +++ b/src/tests/parser/block/blocks/blocks_0016.expected @@ -0,0 +1,25 @@ +Success! Final stack: + [(Lean.Doc.Syntax.blockquote + ">" + [(Lean.Doc.Syntax.blockquote + ">" + [(Lean.Doc.Syntax.ul + "ul{" + [(Lean.Doc.Syntax.li + "*" + [(Lean.Doc.Syntax.para + "para{" + [(Lean.Doc.Syntax.text + (str "\"foo\""))] + "}")])] + "}")]) + (Lean.Doc.Syntax.ul + "ul{" + [(Lean.Doc.Syntax.li + "*" + [(Lean.Doc.Syntax.para + "para{" + [(Lean.Doc.Syntax.text (str "\"foo\""))] + "}")])] + "}")])] +All input consumed. \ No newline at end of file diff --git a/src/tests/parser/block/blocks/blocks_0016.input b/src/tests/parser/block/blocks/blocks_0016.input new file mode 100644 index 000000000..463d4206b --- /dev/null +++ b/src/tests/parser/block/blocks/blocks_0016.input @@ -0,0 +1,4 @@ +> > * foo + + + * foo \ No newline at end of file diff --git a/src/tests/parser/block/blocks/blocks_0017.expected b/src/tests/parser/block/blocks/blocks_0017.expected new file mode 100644 index 000000000..b2ef0b8f8 --- /dev/null +++ b/src/tests/parser/block/blocks/blocks_0017.expected @@ -0,0 +1,22 @@ +Success! Final stack: + [(Lean.Doc.Syntax.blockquote + ">" + [(Lean.Doc.Syntax.ul + "ul{" + [(Lean.Doc.Syntax.li + "*" + [(Lean.Doc.Syntax.para + "para{" + [(Lean.Doc.Syntax.text (str "\"foo\""))] + "}")])] + "}")]) + (Lean.Doc.Syntax.ul + "ul{" + [(Lean.Doc.Syntax.li + "*" + [(Lean.Doc.Syntax.para + "para{" + [(Lean.Doc.Syntax.text (str "\"foo\""))] + "}")])] + "}")] +All input consumed. \ No newline at end of file diff --git a/src/tests/parser/block/blocks/blocks_0017.input b/src/tests/parser/block/blocks/blocks_0017.input new file mode 100644 index 000000000..3c07cef11 --- /dev/null +++ b/src/tests/parser/block/blocks/blocks_0017.input @@ -0,0 +1,4 @@ +> * foo + + +* foo \ No newline at end of file diff --git a/src/tests/parser/block/blocks/blocks_0018.expected b/src/tests/parser/block/blocks/blocks_0018.expected new file mode 100644 index 000000000..dde213295 --- /dev/null +++ b/src/tests/parser/block/blocks/blocks_0018.expected @@ -0,0 +1,17 @@ +Success! Final stack: + [(Lean.Doc.Syntax.ul + "ul{" + [(Lean.Doc.Syntax.li + "*" + [(Lean.Doc.Syntax.para + "para{" + [(Lean.Doc.Syntax.text (str "\"foo\"")) + (Lean.Doc.Syntax.linebreak + "line!" + (str "\"\\n\"")) + (Lean.Doc.Syntax.text + (str "\" thing\""))] + "}")])] + "}")] +Remaining: +"* bar\n" \ No newline at end of file diff --git a/src/tests/parser/block/blocks/blocks_0018.input b/src/tests/parser/block/blocks/blocks_0018.input new file mode 100644 index 000000000..d4e4b0971 --- /dev/null +++ b/src/tests/parser/block/blocks/blocks_0018.input @@ -0,0 +1,2 @@ +* foo + thing* bar diff --git a/src/tests/parser/block/blocks/blocks_0019.expected b/src/tests/parser/block/blocks/blocks_0019.expected new file mode 100644 index 000000000..822d174bc --- /dev/null +++ b/src/tests/parser/block/blocks/blocks_0019.expected @@ -0,0 +1,20 @@ +Success! Final stack: + [(Lean.Doc.Syntax.ul + "ul{" + [(Lean.Doc.Syntax.li + "+" + [(Lean.Doc.Syntax.para + "para{" + [(Lean.Doc.Syntax.text (str "\"foo\""))] + "}")]) + (Lean.Doc.Syntax.li + "+" + [(Lean.Doc.Syntax.para + "para{" + [(Lean.Doc.Syntax.text (str "\"bar\"")) + (Lean.Doc.Syntax.linebreak + "line!" + (str "\"\\n\""))] + "}")])] + "}")] +All input consumed. \ No newline at end of file diff --git a/src/tests/parser/block/blocks/blocks_0019.input b/src/tests/parser/block/blocks/blocks_0019.input new file mode 100644 index 000000000..85270e40a --- /dev/null +++ b/src/tests/parser/block/blocks/blocks_0019.input @@ -0,0 +1,2 @@ ++ foo ++ bar diff --git a/src/tests/parser/block/blocks/blocks_0020.expected b/src/tests/parser/block/blocks/blocks_0020.expected new file mode 100644 index 000000000..1df295971 --- /dev/null +++ b/src/tests/parser/block/blocks/blocks_0020.expected @@ -0,0 +1,20 @@ +Success! Final stack: + [(Lean.Doc.Syntax.ul + "ul{" + [(Lean.Doc.Syntax.li + "*" + [(Lean.Doc.Syntax.para + "para{" + [(Lean.Doc.Syntax.text (str "\"foo\""))] + "}")]) + (Lean.Doc.Syntax.li + "*" + [(Lean.Doc.Syntax.para + "para{" + [(Lean.Doc.Syntax.text (str "\"bar\"")) + (Lean.Doc.Syntax.linebreak + "line!" + (str "\"\\n\""))] + "}")])] + "}")] +All input consumed. \ No newline at end of file diff --git a/src/tests/parser/block/blocks/blocks_0020.input b/src/tests/parser/block/blocks/blocks_0020.input new file mode 100644 index 000000000..d642871e5 --- /dev/null +++ b/src/tests/parser/block/blocks/blocks_0020.input @@ -0,0 +1,3 @@ +* foo + +* bar diff --git a/src/tests/parser/block/blocks/blocks_0021.expected b/src/tests/parser/block/blocks/blocks_0021.expected new file mode 100644 index 000000000..7bc24e656 --- /dev/null +++ b/src/tests/parser/block/blocks/blocks_0021.expected @@ -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 "\"foo\"")) + (Lean.Doc.Syntax.linebreak + "line!" + (str "\"\\n\"")) + (Lean.Doc.Syntax.text + (str "\" stuff\""))] + "}") + (Lean.Doc.Syntax.blockquote + ">" + [(Lean.Doc.Syntax.para + "para{" + [(Lean.Doc.Syntax.text + (str "\"more \""))] + "}")]) + (Lean.Doc.Syntax.para + "para{" + [(Lean.Doc.Syntax.text (str "\"abc\""))] + "}")]) + (Lean.Doc.Syntax.li + "*" + [(Lean.Doc.Syntax.para + "para{" + [(Lean.Doc.Syntax.text (str "\"bar\"")) + (Lean.Doc.Syntax.linebreak + "line!" + (str "\"\\n\""))] + "}")])] + "}")] +All input consumed. \ No newline at end of file diff --git a/src/tests/parser/block/blocks/blocks_0021.input b/src/tests/parser/block/blocks/blocks_0021.input new file mode 100644 index 000000000..f19eabdd3 --- /dev/null +++ b/src/tests/parser/block/blocks/blocks_0021.input @@ -0,0 +1,9 @@ +* foo + stuff + + > more + + abc + + +* bar diff --git a/src/tests/parser/block/blocks/blocks_0022.expected b/src/tests/parser/block/blocks/blocks_0022.expected new file mode 100644 index 000000000..2b538eabf --- /dev/null +++ b/src/tests/parser/block/blocks/blocks_0022.expected @@ -0,0 +1,28 @@ +Success! Final stack: + [(Lean.Doc.Syntax.ul + "ul{" + [(Lean.Doc.Syntax.li + "*" + [(Lean.Doc.Syntax.para + "para{" + [(Lean.Doc.Syntax.text (str "\"foo\""))] + "}") + (Lean.Doc.Syntax.ul + "ul{" + [(Lean.Doc.Syntax.li + "*" + [(Lean.Doc.Syntax.para + "para{" + [(Lean.Doc.Syntax.text + (str "\"bar\""))] + "}")])] + "}")]) + (Lean.Doc.Syntax.li + "*" + [(Lean.Doc.Syntax.para + "para{" + [(Lean.Doc.Syntax.text + (str "\"more outer\""))] + "}")])] + "}")] +All input consumed. \ No newline at end of file diff --git a/src/tests/parser/block/blocks/blocks_0022.input b/src/tests/parser/block/blocks/blocks_0022.input new file mode 100644 index 000000000..54bc72892 --- /dev/null +++ b/src/tests/parser/block/blocks/blocks_0022.input @@ -0,0 +1,3 @@ +* foo + * bar +* more outer \ No newline at end of file diff --git a/src/tests/parser/block/blocks/blocks_0023.expected b/src/tests/parser/block/blocks/blocks_0023.expected new file mode 100644 index 000000000..6fafea3f2 --- /dev/null +++ b/src/tests/parser/block/blocks/blocks_0023.expected @@ -0,0 +1,18 @@ +Failure @35 (⟨2, 15⟩): unexpected end of input; expected %%% (at line beginning), '![', '$$', '$', '[', '[^', beginning of line at ⟨2, 15⟩ or beginning of line or sequence of nestable block openers at ⟨2, 15⟩ +Final stack: + [(Lean.Doc.Syntax.dl + "dl{" + [(Lean.Doc.Syntax.desc + ":" + [(Lean.Doc.Syntax.text + (str "\" an excellent idea\"")) + (Lean.Doc.Syntax.linebreak + "line!" + (str "\"\\n\"")) + (Lean.Doc.Syntax.text + (str "\"Let's say more!\""))] + "=>" + [(Lean.Doc.Syntax.metadata_block ) + ])] + "}")] +Remaining: "" \ No newline at end of file diff --git a/src/tests/parser/block/blocks/blocks_0023.input b/src/tests/parser/block/blocks/blocks_0023.input new file mode 100644 index 000000000..4b00c1d1a --- /dev/null +++ b/src/tests/parser/block/blocks/blocks_0023.input @@ -0,0 +1,2 @@ +: an excellent idea +Let's say more! \ No newline at end of file diff --git a/src/tests/parser/block/blocks/blocks_0024.expected b/src/tests/parser/block/blocks/blocks_0024.expected new file mode 100644 index 000000000..de0467157 --- /dev/null +++ b/src/tests/parser/block/blocks/blocks_0024.expected @@ -0,0 +1,15 @@ +Success! Final stack: + [(Lean.Doc.Syntax.dl + "dl{" + [(Lean.Doc.Syntax.desc + ":" + [(Lean.Doc.Syntax.text + (str "\" an excellent idea\""))] + "=>" + [(Lean.Doc.Syntax.para + "para{" + [(Lean.Doc.Syntax.text + (str "\"Let's say more!\""))] + "}")])] + "}")] +All input consumed. \ No newline at end of file diff --git a/src/tests/parser/block/blocks/blocks_0024.input b/src/tests/parser/block/blocks/blocks_0024.input new file mode 100644 index 000000000..87fb7f1ce --- /dev/null +++ b/src/tests/parser/block/blocks/blocks_0024.input @@ -0,0 +1,3 @@ +: an excellent idea + + Let's say more! \ No newline at end of file diff --git a/src/tests/parser/block/blocks/blocks_0025.expected b/src/tests/parser/block/blocks/blocks_0025.expected new file mode 100644 index 000000000..875fa0646 --- /dev/null +++ b/src/tests/parser/block/blocks/blocks_0025.expected @@ -0,0 +1,21 @@ +Failure @47 (⟨7, 0⟩): expected indentation at least 1 +Final stack: + [(Lean.Doc.Syntax.dl + "dl{" + [(Lean.Doc.Syntax.desc + ":" + [(Lean.Doc.Syntax.text + (str "\" an excellent idea\""))] + "=>" + [(Lean.Doc.Syntax.para + "para{" + [(Lean.Doc.Syntax.text + (str "\"Let's say more!\""))] + "}")]) + (Lean.Doc.Syntax.desc + ":" + [(Lean.Doc.Syntax.text (str "\" more\""))] + "=>" + )] + "}")] +Remaining: "" \ No newline at end of file diff --git a/src/tests/parser/block/blocks/blocks_0025.input b/src/tests/parser/block/blocks/blocks_0025.input new file mode 100644 index 000000000..853f9c9f1 --- /dev/null +++ b/src/tests/parser/block/blocks/blocks_0025.input @@ -0,0 +1,6 @@ +: an excellent idea + + Let's say more! + +: more + diff --git a/src/tests/parser/block/blocks/blocks_0026.expected b/src/tests/parser/block/blocks/blocks_0026.expected new file mode 100644 index 000000000..22b3cd79e --- /dev/null +++ b/src/tests/parser/block/blocks/blocks_0026.expected @@ -0,0 +1,24 @@ +Success! Final stack: + [(Lean.Doc.Syntax.dl + "dl{" + [(Lean.Doc.Syntax.desc + ":" + [(Lean.Doc.Syntax.text + (str "\" an excellent idea\""))] + "=>" + [(Lean.Doc.Syntax.para + "para{" + [(Lean.Doc.Syntax.text + (str "\"Let's say more!\""))] + "}")]) + (Lean.Doc.Syntax.desc + ":" + [(Lean.Doc.Syntax.text (str "\" more\""))] + "=>" + [(Lean.Doc.Syntax.para + "para{" + [(Lean.Doc.Syntax.text + (str "\"even more!\""))] + "}")])] + "}")] +All input consumed. \ No newline at end of file diff --git a/src/tests/parser/block/blocks/blocks_0026.input b/src/tests/parser/block/blocks/blocks_0026.input new file mode 100644 index 000000000..565be32b5 --- /dev/null +++ b/src/tests/parser/block/blocks/blocks_0026.input @@ -0,0 +1,10 @@ +: an excellent idea + + Let's say more! + + + + +: more + + even more! \ No newline at end of file diff --git a/src/tests/parser/block/blocks/blocks_0027.expected b/src/tests/parser/block/blocks/blocks_0027.expected new file mode 100644 index 000000000..c7cc6f676 --- /dev/null +++ b/src/tests/parser/block/blocks/blocks_0027.expected @@ -0,0 +1,23 @@ +Success! Final stack: + [(Lean.Doc.Syntax.dl + "dl{" + [(Lean.Doc.Syntax.desc + ":" + [(Lean.Doc.Syntax.text + (str "\" an excellent idea\""))] + "=>" + [(Lean.Doc.Syntax.para + "para{" + [(Lean.Doc.Syntax.text + (str "\"Let's say more!\""))] + "}")]) + (Lean.Doc.Syntax.desc + ":" + [(Lean.Doc.Syntax.text (str "\" more\""))] + "=>" + [(Lean.Doc.Syntax.para + "para{" + [(Lean.Doc.Syntax.text (str "\"stuff\""))] + "}")])] + "}")] +All input consumed. \ No newline at end of file diff --git a/src/tests/parser/block/blocks/blocks_0027.input b/src/tests/parser/block/blocks/blocks_0027.input new file mode 100644 index 000000000..246e961dc --- /dev/null +++ b/src/tests/parser/block/blocks/blocks_0027.input @@ -0,0 +1,7 @@ +: an excellent idea + + Let's say more! + +: more + + stuff \ No newline at end of file diff --git a/src/tests/parser/block/blocks/blocks_0028.expected b/src/tests/parser/block/blocks/blocks_0028.expected new file mode 100644 index 000000000..6387eca66 --- /dev/null +++ b/src/tests/parser/block/blocks/blocks_0028.expected @@ -0,0 +1,21 @@ +Failure @21 (⟨3, 0⟩): expected indentation at least 1 +Final stack: + [(Lean.Doc.Syntax.dl + "dl{" + [(Lean.Doc.Syntax.desc + ":" + [(Lean.Doc.Syntax.text + (str "\" an excellent idea\""))] + "=>" + )] + "}") + (Lean.Doc.Syntax.para + "para{" + [(Lean.Doc.Syntax.text + (str "\"Let's say more!\""))] + "}") + (Lean.Doc.Syntax.para + "para{" + [(Lean.Doc.Syntax.text (str "\"hello\""))] + "}")] +Remaining: "Let's say more!\n\nhello" \ No newline at end of file diff --git a/src/tests/parser/block/blocks/blocks_0028.input b/src/tests/parser/block/blocks/blocks_0028.input new file mode 100644 index 000000000..b57d0e425 --- /dev/null +++ b/src/tests/parser/block/blocks/blocks_0028.input @@ -0,0 +1,5 @@ +: an excellent idea + +Let's say more! + +hello \ No newline at end of file diff --git a/src/tests/parser/block/blocks/blocks_0029.expected b/src/tests/parser/block/blocks/blocks_0029.expected new file mode 100644 index 000000000..b0e31ac37 --- /dev/null +++ b/src/tests/parser/block/blocks/blocks_0029.expected @@ -0,0 +1,20 @@ +Success! Final stack: + [(Lean.Doc.Syntax.ol + "ol(" + (num "1") + ")" + "{" + [(Lean.Doc.Syntax.li + "1." + [(Lean.Doc.Syntax.para + "para{" + [(Lean.Doc.Syntax.text (str "\"Hello\""))] + "}")]) + (Lean.Doc.Syntax.li + "2." + [(Lean.Doc.Syntax.para + "para{" + [(Lean.Doc.Syntax.text (str "\"World\""))] + "}")])] + "}")] +All input consumed. \ No newline at end of file diff --git a/src/tests/parser/block/blocks/blocks_0029.input b/src/tests/parser/block/blocks/blocks_0029.input new file mode 100644 index 000000000..0300bf11f --- /dev/null +++ b/src/tests/parser/block/blocks/blocks_0029.input @@ -0,0 +1,3 @@ +1. Hello + +2. World \ No newline at end of file diff --git a/src/tests/parser/block/blocks/blocks_0030.expected b/src/tests/parser/block/blocks/blocks_0030.expected new file mode 100644 index 000000000..72c633500 --- /dev/null +++ b/src/tests/parser/block/blocks/blocks_0030.expected @@ -0,0 +1,14 @@ +Success! Final stack: + [(Lean.Doc.Syntax.ol + "ol(" + (num "1") + ")" + "{" + [(Lean.Doc.Syntax.li + "1." + [(Lean.Doc.Syntax.para + "para{" + [(Lean.Doc.Syntax.text (str "\"Hello\""))] + "}")])] + "}")] +All input consumed. \ No newline at end of file diff --git a/src/tests/parser/block/blocks/blocks_0030.input b/src/tests/parser/block/blocks/blocks_0030.input new file mode 100644 index 000000000..2a0b5fc7a --- /dev/null +++ b/src/tests/parser/block/blocks/blocks_0030.input @@ -0,0 +1 @@ +1. Hello \ No newline at end of file diff --git a/src/tests/parser/block/blocks/blocks_0031.expected b/src/tests/parser/block/blocks/blocks_0031.expected new file mode 100644 index 000000000..ac1238881 --- /dev/null +++ b/src/tests/parser/block/blocks/blocks_0031.expected @@ -0,0 +1,26 @@ +Success! Final stack: + [(Lean.Doc.Syntax.ol + "ol(" + (num "1") + ")" + "{" + [(Lean.Doc.Syntax.li + "1." + [(Lean.Doc.Syntax.para + "para{" + [(Lean.Doc.Syntax.text (str "\"Hello\""))] + "}")])] + "}") + (Lean.Doc.Syntax.ol + "ol(" + (num "2") + ")" + "{" + [(Lean.Doc.Syntax.li + "2." + [(Lean.Doc.Syntax.para + "para{" + [(Lean.Doc.Syntax.text (str "\"World\""))] + "}")])] + "}")] +All input consumed. \ No newline at end of file diff --git a/src/tests/parser/block/blocks/blocks_0031.input b/src/tests/parser/block/blocks/blocks_0031.input new file mode 100644 index 000000000..67c8df282 --- /dev/null +++ b/src/tests/parser/block/blocks/blocks_0031.input @@ -0,0 +1,3 @@ +1. Hello + + 2. World \ No newline at end of file diff --git a/src/tests/parser/block/blocks/blocks_0032.expected b/src/tests/parser/block/blocks/blocks_0032.expected new file mode 100644 index 000000000..b0e31ac37 --- /dev/null +++ b/src/tests/parser/block/blocks/blocks_0032.expected @@ -0,0 +1,20 @@ +Success! Final stack: + [(Lean.Doc.Syntax.ol + "ol(" + (num "1") + ")" + "{" + [(Lean.Doc.Syntax.li + "1." + [(Lean.Doc.Syntax.para + "para{" + [(Lean.Doc.Syntax.text (str "\"Hello\""))] + "}")]) + (Lean.Doc.Syntax.li + "2." + [(Lean.Doc.Syntax.para + "para{" + [(Lean.Doc.Syntax.text (str "\"World\""))] + "}")])] + "}")] +All input consumed. \ No newline at end of file diff --git a/src/tests/parser/block/blocks/blocks_0032.input b/src/tests/parser/block/blocks/blocks_0032.input new file mode 100644 index 000000000..78893485c --- /dev/null +++ b/src/tests/parser/block/blocks/blocks_0032.input @@ -0,0 +1,3 @@ + 1. Hello + + 2. World \ No newline at end of file diff --git a/src/tests/parser/block/blocks/blocks_0033.expected b/src/tests/parser/block/blocks/blocks_0033.expected new file mode 100644 index 000000000..8845597f0 --- /dev/null +++ b/src/tests/parser/block/blocks/blocks_0033.expected @@ -0,0 +1,11 @@ +Success! Final stack: + [(Lean.Doc.Syntax.blockquote + ">" + [(Lean.Doc.Syntax.para + "para{" + [(Lean.Doc.Syntax.text (str "\"hey\"")) + (Lean.Doc.Syntax.linebreak + "line!" + (str "\"\\n\""))] + "}")])] +All input consumed. \ No newline at end of file diff --git a/src/tests/parser/block/blocks/blocks_0033.input b/src/tests/parser/block/blocks/blocks_0033.input new file mode 100644 index 000000000..5111d8b08 --- /dev/null +++ b/src/tests/parser/block/blocks/blocks_0033.input @@ -0,0 +1 @@ +> hey diff --git a/src/tests/parser/block/blocks/blocks_0034.expected b/src/tests/parser/block/blocks/blocks_0034.expected new file mode 100644 index 000000000..bf7af691d --- /dev/null +++ b/src/tests/parser/block/blocks/blocks_0034.expected @@ -0,0 +1,6 @@ +Success! Final stack: + [(Lean.Doc.Syntax.para + "para{" + [(Lean.Doc.Syntax.text (str "\"n*k \""))] + "}")] +All input consumed. \ No newline at end of file diff --git a/src/tests/parser/block/blocks/blocks_0034.input b/src/tests/parser/block/blocks/blocks_0034.input new file mode 100644 index 000000000..9885d3e1c --- /dev/null +++ b/src/tests/parser/block/blocks/blocks_0034.input @@ -0,0 +1 @@ +n\*k \ No newline at end of file diff --git a/src/tests/parser/block/blocks/blocks_0035.expected b/src/tests/parser/block/blocks/blocks_0035.expected new file mode 100644 index 000000000..2a2d253a4 --- /dev/null +++ b/src/tests/parser/block/blocks/blocks_0035.expected @@ -0,0 +1,17 @@ +Failure @16 (⟨1, 16⟩): '_' +Final stack: + [(Lean.Doc.Syntax.para + "para{" + [(Lean.Doc.Syntax.bold + "*" + [(Lean.Doc.Syntax.text (str "\"This is \"")) + (Lean.Doc.Syntax.emph + "_" + [(Lean.Doc.Syntax.text + (str "\"strong\""))] + )] + "*") + (Lean.Doc.Syntax.text + (str "\" not regular\""))] + "}")] +Remaining: "* not regular_ emphasis" \ No newline at end of file diff --git a/src/tests/parser/block/blocks/blocks_0035.input b/src/tests/parser/block/blocks/blocks_0035.input new file mode 100644 index 000000000..7ffdc2355 --- /dev/null +++ b/src/tests/parser/block/blocks/blocks_0035.input @@ -0,0 +1 @@ +*This is _strong* not regular_ emphasis \ No newline at end of file diff --git a/src/tests/parser/block/blocks/blocks_0036.expected b/src/tests/parser/block/blocks/blocks_0036.expected new file mode 100644 index 000000000..44e76edec --- /dev/null +++ b/src/tests/parser/block/blocks/blocks_0036.expected @@ -0,0 +1,9 @@ +Success! Final stack: + [(Lean.Doc.Syntax.header + "header(" + (num "0") + ")" + "{" + [(Lean.Doc.Syntax.text (str "\"Header!\""))] + "}")] +All input consumed. \ No newline at end of file diff --git a/src/tests/parser/block/blocks/blocks_0036.input b/src/tests/parser/block/blocks/blocks_0036.input new file mode 100644 index 000000000..db23e08da --- /dev/null +++ b/src/tests/parser/block/blocks/blocks_0036.input @@ -0,0 +1 @@ +# Header! \ No newline at end of file diff --git a/src/tests/parser/block/blocks/blocks_0037.expected b/src/tests/parser/block/blocks/blocks_0037.expected new file mode 100644 index 000000000..bc03584f0 --- /dev/null +++ b/src/tests/parser/block/blocks/blocks_0037.expected @@ -0,0 +1,9 @@ +Success! Final stack: + [(Lean.Doc.Syntax.header + "header(" + (num "1") + ")" + "{" + [(Lean.Doc.Syntax.text (str "\"Header!\""))] + "}")] +All input consumed. \ No newline at end of file diff --git a/src/tests/parser/block/blocks/blocks_0037.input b/src/tests/parser/block/blocks/blocks_0037.input new file mode 100644 index 000000000..38c82f4c9 --- /dev/null +++ b/src/tests/parser/block/blocks/blocks_0037.input @@ -0,0 +1 @@ +## Header! \ No newline at end of file diff --git a/src/tests/parser/block/blocks/blocks_0038.expected b/src/tests/parser/block/blocks/blocks_0038.expected new file mode 100644 index 000000000..56b8a9459 --- /dev/null +++ b/src/tests/parser/block/blocks/blocks_0038.expected @@ -0,0 +1,14 @@ +Success! Final stack: + [(Lean.Doc.Syntax.blockquote + ">" + [(Lean.Doc.Syntax.para + "para{" + [(Lean.Doc.Syntax.text + (str "\"Quotation\"")) + (Lean.Doc.Syntax.linebreak + "line!" + (str "\"\\n\"")) + (Lean.Doc.Syntax.text + (str "\"and contained\""))] + "}")])] +All input consumed. \ No newline at end of file diff --git a/src/tests/parser/block/blocks/blocks_0038.input b/src/tests/parser/block/blocks/blocks_0038.input new file mode 100644 index 000000000..2d642bff6 --- /dev/null +++ b/src/tests/parser/block/blocks/blocks_0038.input @@ -0,0 +1,2 @@ +> Quotation +and contained \ No newline at end of file diff --git a/src/tests/parser/block/blocks/blocks_0039.expected b/src/tests/parser/block/blocks/blocks_0039.expected new file mode 100644 index 000000000..9599c03b8 --- /dev/null +++ b/src/tests/parser/block/blocks/blocks_0039.expected @@ -0,0 +1,29 @@ +Failure @65 (⟨4, 0⟩): expected '`' to close inline code +Final stack: + [(Lean.Doc.Syntax.para + "para{" + [(Lean.Doc.Syntax.text + (str "\"Attention:\""))] + "}") + (Lean.Doc.Syntax.para + "para{" + [(Lean.Doc.Syntax.text + (str + "\"Here is a paragraph with an unterminated \"")) + (Lean.Doc.Syntax.code + "`" + (str "\"code block\"") + ) + (Lean.Doc.Syntax.text + (str + "\"that would be super annoying without error recovery in the\"")) + (Lean.Doc.Syntax.linebreak + "line!" + (str "\"\\n\"")) + (Lean.Doc.Syntax.text (str "\"parser.\""))] + "}") + (Lean.Doc.Syntax.para + "para{" + [(Lean.Doc.Syntax.text (str "\"Yep.\""))] + "}")] +Remaining: "that would be super annoying without error recovery in the\nparser.\n\nYep." \ No newline at end of file diff --git a/src/tests/parser/block/blocks/blocks_0039.input b/src/tests/parser/block/blocks/blocks_0039.input new file mode 100644 index 000000000..d1af6cc9b --- /dev/null +++ b/src/tests/parser/block/blocks/blocks_0039.input @@ -0,0 +1,7 @@ +Attention: + +Here is a paragraph with an unterminated `code block +that would be super annoying without error recovery in the +parser. + +Yep. \ No newline at end of file diff --git a/src/tests/parser/block/blocks/blocks_0040.expected b/src/tests/parser/block/blocks/blocks_0040.expected new file mode 100644 index 000000000..f3937c886 --- /dev/null +++ b/src/tests/parser/block/blocks/blocks_0040.expected @@ -0,0 +1,36 @@ +3 failures: + @73 (⟨9, 3⟩): expected directive name (identifier) + "\n" + @74 (⟨10, 0⟩): expected closing ':::' for directive from line 9 + "" + @74 (⟨10, 0⟩): expected closing '::::' for directive from line 3 + "" + +Final stack: + [(Lean.Doc.Syntax.para + "para{" + [(Lean.Doc.Syntax.text + (str + "\"Here's some error recovery for directives.\""))] + "}") + (Lean.Doc.Syntax.directive + "::::" + `foo + [] + "\n" + [(Lean.Doc.Syntax.para + "para{" + [(Lean.Doc.Syntax.text (str "\"Indeed.\""))] + "}") + (Lean.Doc.Syntax.para + "para{" + [(Lean.Doc.Syntax.text (str "\"It is.\""))] + "}") + (Lean.Doc.Syntax.directive + ":::" + + [] + "\n" + [] + )] + )] \ No newline at end of file diff --git a/src/tests/parser/block/blocks/blocks_0040.input b/src/tests/parser/block/blocks/blocks_0040.input new file mode 100644 index 000000000..4fe94fa8e --- /dev/null +++ b/src/tests/parser/block/blocks/blocks_0040.input @@ -0,0 +1,9 @@ +Here's some error recovery for directives. + +::::foo + +Indeed. + +It is. + +::: diff --git a/src/tests/parser/block/blocks/blocks_0041.expected b/src/tests/parser/block/blocks/blocks_0041.expected new file mode 100644 index 000000000..5bbc26730 --- /dev/null +++ b/src/tests/parser/block/blocks/blocks_0041.expected @@ -0,0 +1,36 @@ +3 failures: + @68 (⟨8, 0⟩): expected closing ':::' from directive on line 3 at column 0, but it's at column 1 + " :::\n" + @72 (⟨8, 4⟩): expected directive name (identifier) + "\n" + @73 (⟨9, 0⟩): expected closing ':::' for directive from line 8 + "" + +Final stack: + [(Lean.Doc.Syntax.para + "para{" + [(Lean.Doc.Syntax.text + (str + "\"Here's some error recovery for directives.\""))] + "}") + (Lean.Doc.Syntax.directive + ":::" + `foo + [] + "\n" + [(Lean.Doc.Syntax.para + "para{" + [(Lean.Doc.Syntax.text (str "\"Indeed.\""))] + "}") + (Lean.Doc.Syntax.para + "para{" + [(Lean.Doc.Syntax.text (str "\"It is.\""))] + "}")] + ) + (Lean.Doc.Syntax.directive + ":::" + + [] + "\n" + [] + )] \ No newline at end of file diff --git a/src/tests/parser/block/blocks/blocks_0041.input b/src/tests/parser/block/blocks/blocks_0041.input new file mode 100644 index 000000000..0086cc6f8 --- /dev/null +++ b/src/tests/parser/block/blocks/blocks_0041.input @@ -0,0 +1,8 @@ +Here's some error recovery for directives. + +:::foo + +Indeed. + +It is. + ::: diff --git a/src/tests/parser/block/blocks/blocks_0042.expected b/src/tests/parser/block/blocks/blocks_0042.expected new file mode 100644 index 000000000..e814adc21 --- /dev/null +++ b/src/tests/parser/block/blocks/blocks_0042.expected @@ -0,0 +1,41 @@ +2 failures: + @71 (⟨8, 0⟩): expected closing '::::' for directive from line 3 + ":::: a\n\nx\n" + @81 (⟨11, 0⟩): expected closing '::::' for directive from line 8 + "" + +Final stack: + [(Lean.Doc.Syntax.para + "para{" + [(Lean.Doc.Syntax.text + (str + "\"Here's some error recovery for directives.\""))] + "}") + (Lean.Doc.Syntax.directive + "::::" + `foo + [(Lean.Doc.Syntax.anon + (Lean.Doc.Syntax.arg_num (num "5")))] + "\n" + [(Lean.Doc.Syntax.para + "para{" + [(Lean.Doc.Syntax.text (str "\"Indeed.\""))] + "}") + (Lean.Doc.Syntax.para + "para{" + [(Lean.Doc.Syntax.text (str "\"It is.\""))] + "}")] + ) + (Lean.Doc.Syntax.directive + "::::" + `a + [] + "\n" + [(Lean.Doc.Syntax.para + "para{" + [(Lean.Doc.Syntax.text (str "\"x\"")) + (Lean.Doc.Syntax.linebreak + "line!" + (str "\"\\n\""))] + "}")] + )] \ No newline at end of file diff --git a/src/tests/parser/block/blocks/blocks_0042.input b/src/tests/parser/block/blocks/blocks_0042.input new file mode 100644 index 000000000..91852404e --- /dev/null +++ b/src/tests/parser/block/blocks/blocks_0042.input @@ -0,0 +1,10 @@ +Here's some error recovery for directives. + +::::foo 5 + +Indeed. + +It is. +:::: a + +x diff --git a/src/tests/parser/block/blocks/blocks_0043.expected b/src/tests/parser/block/blocks/blocks_0043.expected new file mode 100644 index 000000000..0e48c54b6 --- /dev/null +++ b/src/tests/parser/block/blocks/blocks_0043.expected @@ -0,0 +1,14 @@ +Success! Final stack: + [(Lean.Doc.Syntax.blockquote + ">" + [(Lean.Doc.Syntax.para + "para{" + [(Lean.Doc.Syntax.text + (str "\"Quotation\""))] + "}") + (Lean.Doc.Syntax.para + "para{" + [(Lean.Doc.Syntax.text + (str "\"and contained\""))] + "}")])] +All input consumed. \ No newline at end of file diff --git a/src/tests/parser/block/blocks/blocks_0043.input b/src/tests/parser/block/blocks/blocks_0043.input new file mode 100644 index 000000000..eb68de8fb --- /dev/null +++ b/src/tests/parser/block/blocks/blocks_0043.input @@ -0,0 +1,3 @@ +> Quotation + + and contained \ No newline at end of file diff --git a/src/tests/parser/block/blocks/blocks_0044.expected b/src/tests/parser/block/blocks/blocks_0044.expected new file mode 100644 index 000000000..e74ce250b --- /dev/null +++ b/src/tests/parser/block/blocks/blocks_0044.expected @@ -0,0 +1,14 @@ +Success! Final stack: + [(Lean.Doc.Syntax.blockquote + ">" + [(Lean.Doc.Syntax.para + "para{" + [(Lean.Doc.Syntax.text + (str "\"Quotation\""))] + "}")]) + (Lean.Doc.Syntax.para + "para{" + [(Lean.Doc.Syntax.text + (str "\"and not contained\""))] + "}")] +All input consumed. \ No newline at end of file diff --git a/src/tests/parser/block/blocks/blocks_0044.input b/src/tests/parser/block/blocks/blocks_0044.input new file mode 100644 index 000000000..d3369a58e --- /dev/null +++ b/src/tests/parser/block/blocks/blocks_0044.input @@ -0,0 +1,3 @@ +> Quotation + +and not contained \ No newline at end of file diff --git a/src/tests/parser/block/blocks/blocks_0045.expected b/src/tests/parser/block/blocks/blocks_0045.expected new file mode 100644 index 000000000..3d4c9d1d1 --- /dev/null +++ b/src/tests/parser/block/blocks/blocks_0045.expected @@ -0,0 +1,8 @@ +Success! Final stack: + [(Lean.Doc.Syntax.command "{" `test [] "}") + (Lean.Doc.Syntax.para + "para{" + [(Lean.Doc.Syntax.text + (str "\"Here's a paragraph.\""))] + "}")] +All input consumed. \ No newline at end of file diff --git a/src/tests/parser/block/blocks/blocks_0045.input b/src/tests/parser/block/blocks/blocks_0045.input new file mode 100644 index 000000000..fd9bf99e3 --- /dev/null +++ b/src/tests/parser/block/blocks/blocks_0045.input @@ -0,0 +1,2 @@ +{test} +Here's a paragraph. \ No newline at end of file diff --git a/src/tests/parser/block/blocks/blocks_0046.expected b/src/tests/parser/block/blocks/blocks_0046.expected new file mode 100644 index 000000000..cafc29d7c --- /dev/null +++ b/src/tests/parser/block/blocks/blocks_0046.expected @@ -0,0 +1,19 @@ +Success! Final stack: + [(Lean.Doc.Syntax.command "{" `test [] "}") + (Lean.Doc.Syntax.blockquote + ">" + [(Lean.Doc.Syntax.para + "para{" + [(Lean.Doc.Syntax.text + (str "\"Here's a blockquote\""))] + "}") + (Lean.Doc.Syntax.para + "para{" + [(Lean.Doc.Syntax.text + (str "\"with multiple paras\""))] + "}")]) + (Lean.Doc.Syntax.para + "para{" + [(Lean.Doc.Syntax.text (str "\"that ends\""))] + "}")] +All input consumed. \ No newline at end of file diff --git a/src/tests/parser/block/blocks/blocks_0046.input b/src/tests/parser/block/blocks/blocks_0046.input new file mode 100644 index 000000000..64bb700af --- /dev/null +++ b/src/tests/parser/block/blocks/blocks_0046.input @@ -0,0 +1,6 @@ +{test} +> Here's a blockquote + + with multiple paras + +that ends \ No newline at end of file diff --git a/src/tests/parser/block/blocks/blocks_0047.expected b/src/tests/parser/block/blocks/blocks_0047.expected new file mode 100644 index 000000000..8bfe1f7c8 --- /dev/null +++ b/src/tests/parser/block/blocks/blocks_0047.expected @@ -0,0 +1,4 @@ +Success! Final stack: + [(Lean.Doc.Syntax.command "{" `abc [] "}") + (Lean.Doc.Syntax.command "{" `def [] "}")] +All input consumed. \ No newline at end of file diff --git a/src/tests/parser/block/blocks/blocks_0047.input b/src/tests/parser/block/blocks/blocks_0047.input new file mode 100644 index 000000000..b94927cf9 --- /dev/null +++ b/src/tests/parser/block/blocks/blocks_0047.input @@ -0,0 +1,2 @@ +{abc} +{def} \ No newline at end of file diff --git a/src/tests/parser/block/blocks/blocks_0048.expected b/src/tests/parser/block/blocks/blocks_0048.expected new file mode 100644 index 000000000..57c0dcb00 --- /dev/null +++ b/src/tests/parser/block/blocks/blocks_0048.expected @@ -0,0 +1,20 @@ +Success! Final stack: + [(Lean.Doc.Syntax.metadata_block + "%%%" + (Term.structInstFields + [(Term.structInstField + (Term.structInstLVal `foo []) + [[] + [] + (Term.structInstFieldDef + ":=" + [] + (num "53"))]) + []]) + "%%%") + (Lean.Doc.Syntax.para + "para{" + [(Lean.Doc.Syntax.text + (str "\"Text/paragraph!\""))] + "}")] +All input consumed. \ No newline at end of file diff --git a/src/tests/parser/block/blocks/blocks_0048.input b/src/tests/parser/block/blocks/blocks_0048.input new file mode 100644 index 000000000..abb9bab81 --- /dev/null +++ b/src/tests/parser/block/blocks/blocks_0048.input @@ -0,0 +1,4 @@ +%%% +foo := 53 +%%% +Text/paragraph! \ No newline at end of file diff --git a/src/tests/parser/block/blocks/blocks_0049.expected b/src/tests/parser/block/blocks/blocks_0049.expected new file mode 100644 index 000000000..6c761e9f8 --- /dev/null +++ b/src/tests/parser/block/blocks/blocks_0049.expected @@ -0,0 +1,24 @@ +Success! Final stack: + [(Lean.Doc.Syntax.para + "para{" + [(Lean.Doc.Syntax.link + "[" + [(Lean.Doc.Syntax.text + (str "\"[link A]\""))] + "]" + (Lean.Doc.Syntax.url + "(" + (str "\"https://example.com\"") + ")")) + (Lean.Doc.Syntax.text (str "\" \"")) + (Lean.Doc.Syntax.link + "[" + [(Lean.Doc.Syntax.text + (str "\"[link B]\""))] + "]" + (Lean.Doc.Syntax.url + "(" + (str "\"https://more.example.com\"") + ")"))] + "}")] +All input consumed. \ No newline at end of file diff --git a/src/tests/parser/block/blocks/blocks_0049.input b/src/tests/parser/block/blocks/blocks_0049.input new file mode 100644 index 000000000..d3e16272d --- /dev/null +++ b/src/tests/parser/block/blocks/blocks_0049.input @@ -0,0 +1 @@ +[\[link A\]](https://example.com) [\[link B\]](https://more.example.com) \ No newline at end of file diff --git a/src/tests/parser/block/blocks/blocks_0050.expected b/src/tests/parser/block/blocks/blocks_0050.expected new file mode 100644 index 000000000..5b90de958 --- /dev/null +++ b/src/tests/parser/block/blocks/blocks_0050.expected @@ -0,0 +1,18 @@ +Success! Final stack: + [(Lean.Doc.Syntax.para + "para{" + [(Lean.Doc.Syntax.link + "[" + [(Lean.Doc.Syntax.text (str "\"My link\""))] + "]" + (Lean.Doc.Syntax.ref + "[" + (str "\"lean\"") + "]"))] + "}") + (Lean.Doc.Syntax.link_ref + "[" + (str "\"lean\"") + "]:" + (str "\"https://lean-lang.org\""))] +All input consumed. \ No newline at end of file diff --git a/src/tests/parser/block/blocks/blocks_0050.input b/src/tests/parser/block/blocks/blocks_0050.input new file mode 100644 index 000000000..47813a544 --- /dev/null +++ b/src/tests/parser/block/blocks/blocks_0050.input @@ -0,0 +1,3 @@ +[My link][lean] + +[lean]: https://lean-lang.org \ No newline at end of file diff --git a/src/tests/parser/block/blocks/blocks_0051.expected b/src/tests/parser/block/blocks/blocks_0051.expected new file mode 100644 index 000000000..2a79d1aa8 --- /dev/null +++ b/src/tests/parser/block/blocks/blocks_0051.expected @@ -0,0 +1,22 @@ +Failure @45 (⟨2, 29⟩): expected '(' or '[' +Final stack: + [(Lean.Doc.Syntax.para + "para{" + [(Lean.Doc.Syntax.link + "[" + [(Lean.Doc.Syntax.text (str "\"My link\""))] + "]" + (Lean.Doc.Syntax.ref + "[" + (str "\"lean\"") + "]")) + (Lean.Doc.Syntax.linebreak + "line!" + (str "\"\\n\"")) + (Lean.Doc.Syntax.link + "[" + [(Lean.Doc.Syntax.text (str "\"lean\""))] + "]" + (Lean.Doc.Syntax.url ))] + "}")] +Remaining: "" \ No newline at end of file diff --git a/src/tests/parser/block/blocks/blocks_0051.input b/src/tests/parser/block/blocks/blocks_0051.input new file mode 100644 index 000000000..e1709ab1e --- /dev/null +++ b/src/tests/parser/block/blocks/blocks_0051.input @@ -0,0 +1,2 @@ +[My link][lean] +[lean]: https://lean-lang.org \ No newline at end of file diff --git a/src/tests/parser/block/blocks/blocks_0052.expected b/src/tests/parser/block/blocks/blocks_0052.expected new file mode 100644 index 000000000..ef4f90aae --- /dev/null +++ b/src/tests/parser/block/blocks/blocks_0052.expected @@ -0,0 +1,22 @@ +Success! Final stack: + [(Lean.Doc.Syntax.para + "para{" + [(Lean.Doc.Syntax.link + "[" + [(Lean.Doc.Syntax.text (str "\"My link\""))] + "]" + (Lean.Doc.Syntax.ref + "[" + (str "\"lean\"") + "]"))] + "}") + (Lean.Doc.Syntax.link_ref + "[" + (str "\"lean\"") + "]:" + (str "\"https://lean-lang.org\"")) + (Lean.Doc.Syntax.para + "para{" + [(Lean.Doc.Syntax.text (str "\"hello\""))] + "}")] +All input consumed. \ No newline at end of file diff --git a/src/tests/parser/block/blocks/blocks_0052.input b/src/tests/parser/block/blocks/blocks_0052.input new file mode 100644 index 000000000..03650fc12 --- /dev/null +++ b/src/tests/parser/block/blocks/blocks_0052.input @@ -0,0 +1,4 @@ +[My link][lean] + +[lean]: https://lean-lang.org +hello \ No newline at end of file diff --git a/src/tests/parser/block/blocks/blocks_0053.expected b/src/tests/parser/block/blocks/blocks_0053.expected new file mode 100644 index 000000000..dc22d30e4 --- /dev/null +++ b/src/tests/parser/block/blocks/blocks_0053.expected @@ -0,0 +1,16 @@ +Success! Final stack: + [(Lean.Doc.Syntax.para + "para{" + [(Lean.Doc.Syntax.text (str "\"Blah blah\"")) + (Lean.Doc.Syntax.footnote + "[^" + (str "\"1\"") + "]")] + "}") + (Lean.Doc.Syntax.footnote_ref + "[^" + (str "\"1\"") + "]:" + [(Lean.Doc.Syntax.text + (str "\"More can be said\""))])] +All input consumed. \ No newline at end of file diff --git a/src/tests/parser/block/blocks/blocks_0053.input b/src/tests/parser/block/blocks/blocks_0053.input new file mode 100644 index 000000000..a2c99c13c --- /dev/null +++ b/src/tests/parser/block/blocks/blocks_0053.input @@ -0,0 +1,3 @@ +Blah blah[^1] + +[^1]: More can be said \ No newline at end of file diff --git a/src/tests/parser/block/blocks/blocks_0054.expected b/src/tests/parser/block/blocks/blocks_0054.expected new file mode 100644 index 000000000..3639662ae --- /dev/null +++ b/src/tests/parser/block/blocks/blocks_0054.expected @@ -0,0 +1,180 @@ +10 failures: + @38 (⟨4, 14⟩): expected ']' + "\n\n* [busted\n link\n\n* [busted\n _italics\n link\n\n\n* [busted destination](hey\n\n* ![busted image alt text\n\n* ![busted image link](image.png\n\n* a *bold choice\n\n* very _italic *and bold, onto many\n lines is OK* but don't forget...\n\na paragraph with [a bad link syntax](http://example.com\nis OK. The rest *works*.\n" + @57 (⟨7, 7⟩): expected ']' + "\n\n* [busted\n _italics\n link\n\n\n* [busted destination](hey\n\n* ![busted image alt text\n\n* ![busted image link](image.png\n\n* a *bold choice\n\n* very _italic *and bold, onto many\n lines is OK* but don't forget...\n\na paragraph with [a bad link syntax](http://example.com\nis OK. The rest *works*.\n" + @88 (⟨11, 7⟩): '_' + "\n\n\n* [busted destination](hey\n\n* ![busted image alt text\n\n* ![busted image link](image.png\n\n* a *bold choice\n\n* very _italic *and bold, onto many\n lines is OK* but don't forget...\n\na paragraph with [a bad link syntax](http://example.com\nis OK. The rest *works*.\n" + @88 (⟨11, 7⟩): expected ']' + "\n\n\n* [busted destination](hey\n\n* ![busted image alt text\n\n* ![busted image link](image.png\n\n* a *bold choice\n\n* very _italic *and bold, onto many\n lines is OK* but don't forget...\n\na paragraph with [a bad link syntax](http://example.com\nis OK. The rest *works*.\n" + @117 (⟨14, 26⟩): expected ')' + "\n\n* ![busted image alt text\n\n* ![busted image link](image.png\n\n* a *bold choice\n\n* very _italic *and bold, onto many\n lines is OK* but don't forget...\n\na paragraph with [a bad link syntax](http://example.com\nis OK. The rest *works*.\n" + @144 (⟨16, 25⟩): expected ']' + "\n\n* ![busted image link](image.png\n\n* a *bold choice\n\n* very _italic *and bold, onto many\n lines is OK* but don't forget...\n\na paragraph with [a bad link syntax](http://example.com\nis OK. The rest *works*.\n" + @178 (⟨18, 32⟩): expected ')' + "\n\n* a *bold choice\n\n* very _italic *and bold, onto many\n lines is OK* but don't forget...\n\na paragraph with [a bad link syntax](http://example.com\nis OK. The rest *works*.\n" + @196 (⟨20, 16⟩): '*' + "\n\n* very _italic *and bold, onto many\n lines is OK* but don't forget...\n\na paragraph with [a bad link syntax](http://example.com\nis OK. The rest *works*.\n" + @269 (⟨23, 35⟩): '_' + "\n\na paragraph with [a bad link syntax](http://example.com\nis OK. The rest *works*.\n" + @326 (⟨25, 55⟩): expected ')' + "\nis OK. The rest *works*.\n" + +Final stack: + [(Lean.Doc.Syntax.para + "para{" + [(Lean.Doc.Syntax.linebreak + "line!" + (str "\"\\n\"")) + (Lean.Doc.Syntax.text + (str "\"Error recovery tests:\""))] + "}") + (Lean.Doc.Syntax.ul + "ul{" + [(Lean.Doc.Syntax.li + "*" + [(Lean.Doc.Syntax.para + "para{" + [(Lean.Doc.Syntax.link + "[" + [(Lean.Doc.Syntax.text + (str "\"busted link\""))] + )] + "}")]) + (Lean.Doc.Syntax.li + "*" + [(Lean.Doc.Syntax.para + "para{" + [(Lean.Doc.Syntax.link + "[" + [(Lean.Doc.Syntax.text + (str "\"busted\"")) + (Lean.Doc.Syntax.linebreak + "line!" + (str "\"\\n\"")) + (Lean.Doc.Syntax.text + (str "\" link\""))] + )] + "}")]) + (Lean.Doc.Syntax.li + "*" + [(Lean.Doc.Syntax.para + "para{" + [(Lean.Doc.Syntax.link + "[" + [(Lean.Doc.Syntax.text + (str "\"busted\"")) + (Lean.Doc.Syntax.linebreak + "line!" + (str "\"\\n\"")) + (Lean.Doc.Syntax.text (str "\" \"")) + (Lean.Doc.Syntax.emph + "_" + [(Lean.Doc.Syntax.text + (str "\"italics\"")) + (Lean.Doc.Syntax.linebreak + "line!" + (str "\"\\n\"")) + (Lean.Doc.Syntax.text + (str "\" link\""))] + )] + )] + "}")]) + (Lean.Doc.Syntax.li + "*" + [(Lean.Doc.Syntax.para + "para{" + [(Lean.Doc.Syntax.link + "[" + [(Lean.Doc.Syntax.text + (str "\"busted destination\""))] + "]" + (Lean.Doc.Syntax.url + "(" + (str "\"hey\"") + ))] + "}")]) + (Lean.Doc.Syntax.li + "*" + [(Lean.Doc.Syntax.para + "para{" + [(Lean.Doc.Syntax.image + "![" + (str "\"busted image alt text\"") + )] + "}")]) + (Lean.Doc.Syntax.li + "*" + [(Lean.Doc.Syntax.para + "para{" + [(Lean.Doc.Syntax.image + "![" + (str "\"busted image link\"") + "]" + (Lean.Doc.Syntax.url + "(" + (str "\"image.png\"") + ))] + "}")]) + (Lean.Doc.Syntax.li + "*" + [(Lean.Doc.Syntax.para + "para{" + [(Lean.Doc.Syntax.text (str "\"a \"")) + (Lean.Doc.Syntax.bold + "*" + [(Lean.Doc.Syntax.text + (str "\"bold choice\""))] + )] + "}")]) + (Lean.Doc.Syntax.li + "*" + [(Lean.Doc.Syntax.para + "para{" + [(Lean.Doc.Syntax.text (str "\"very \"")) + (Lean.Doc.Syntax.emph + "_" + [(Lean.Doc.Syntax.text + (str "\"italic \"")) + (Lean.Doc.Syntax.bold + "*" + [(Lean.Doc.Syntax.text + (str "\"and bold, onto many\"")) + (Lean.Doc.Syntax.linebreak + "line!" + (str "\"\\n\"")) + (Lean.Doc.Syntax.text + (str "\" lines is OK\""))] + "*") + (Lean.Doc.Syntax.text + (str "\" but don't forget...\""))] + )] + "}")])] + "}") + (Lean.Doc.Syntax.para + "para{" + [(Lean.Doc.Syntax.text + (str "\"a paragraph with \"")) + (Lean.Doc.Syntax.link + "[" + [(Lean.Doc.Syntax.text + (str "\"a bad link syntax\""))] + "]" + (Lean.Doc.Syntax.url + "(" + (str "\"http://example.com\"") + )) + (Lean.Doc.Syntax.linebreak + "line!" + (str "\"\\n\"")) + (Lean.Doc.Syntax.text + (str "\"is OK. The rest \"")) + (Lean.Doc.Syntax.bold + "*" + [(Lean.Doc.Syntax.text (str "\"works\""))] + "*") + (Lean.Doc.Syntax.text (str "\".\"")) + (Lean.Doc.Syntax.linebreak + "line!" + (str "\"\\n\""))] + "}")] \ No newline at end of file diff --git a/src/tests/parser/block/blocks/blocks_0054.input b/src/tests/parser/block/blocks/blocks_0054.input new file mode 100644 index 000000000..de5a45d35 --- /dev/null +++ b/src/tests/parser/block/blocks/blocks_0054.input @@ -0,0 +1,26 @@ + +Error recovery tests: + +* [busted link + +* [busted + link + +* [busted + _italics + link + + +* [busted destination](hey + +* ![busted image alt text + +* ![busted image link](image.png + +* a *bold choice + +* very _italic *and bold, onto many + lines is OK* but don't forget... + +a paragraph with [a bad link syntax](http://example.com +is OK. The rest *works*. diff --git a/src/tests/parser/block/code/codeBlock_0001.expected b/src/tests/parser/block/code/codeBlock_0001.expected new file mode 100644 index 000000000..c53fe6fcf --- /dev/null +++ b/src/tests/parser/block/code/codeBlock_0001.expected @@ -0,0 +1,8 @@ +Success! Final stack: + (Lean.Doc.Syntax.codeblock + "```" + [`scheme []] + "\n" + (str "\"(define x 4)\\nx\\n\"") + "```") +All input consumed. \ No newline at end of file diff --git a/src/tests/parser/block/code/codeBlock_0001.input b/src/tests/parser/block/code/codeBlock_0001.input new file mode 100644 index 000000000..dc36ef62e --- /dev/null +++ b/src/tests/parser/block/code/codeBlock_0001.input @@ -0,0 +1,4 @@ + ``` scheme + (define x 4) + x + ``` diff --git a/src/tests/parser/block/code/codeBlock_0002.expected b/src/tests/parser/block/code/codeBlock_0002.expected new file mode 100644 index 000000000..c043b3019 --- /dev/null +++ b/src/tests/parser/block/code/codeBlock_0002.expected @@ -0,0 +1,8 @@ +Success! Final stack: + (Lean.Doc.Syntax.codeblock + "```" + [`scheme []] + "\n" + (str "\" (define x 4)\\n x\\n\"") + "```") +All input consumed. \ No newline at end of file diff --git a/src/tests/parser/block/code/codeBlock_0002.input b/src/tests/parser/block/code/codeBlock_0002.input new file mode 100644 index 000000000..f07886f27 --- /dev/null +++ b/src/tests/parser/block/code/codeBlock_0002.input @@ -0,0 +1,4 @@ +``` scheme + (define x 4) + x +``` \ No newline at end of file diff --git a/src/tests/parser/block/code/codeBlock_0003.expected b/src/tests/parser/block/code/codeBlock_0003.expected new file mode 100644 index 000000000..9092953fa --- /dev/null +++ b/src/tests/parser/block/code/codeBlock_0003.expected @@ -0,0 +1,8 @@ +Success! Final stack: + (Lean.Doc.Syntax.codeblock + "```" + [] + "\n" + (str "\"(define x 4)\\nx\\n\"") + "```") +All input consumed. \ No newline at end of file diff --git a/src/tests/parser/block/code/codeBlock_0003.input b/src/tests/parser/block/code/codeBlock_0003.input new file mode 100644 index 000000000..f1530288c --- /dev/null +++ b/src/tests/parser/block/code/codeBlock_0003.input @@ -0,0 +1,4 @@ + ``` + (define x 4) + x + ``` diff --git a/src/tests/parser/block/code/codeBlock_0004.expected b/src/tests/parser/block/code/codeBlock_0004.expected new file mode 100644 index 000000000..9092953fa --- /dev/null +++ b/src/tests/parser/block/code/codeBlock_0004.expected @@ -0,0 +1,8 @@ +Success! Final stack: + (Lean.Doc.Syntax.codeblock + "```" + [] + "\n" + (str "\"(define x 4)\\nx\\n\"") + "```") +All input consumed. \ No newline at end of file diff --git a/src/tests/parser/block/code/codeBlock_0004.input b/src/tests/parser/block/code/codeBlock_0004.input new file mode 100644 index 000000000..b68d97987 --- /dev/null +++ b/src/tests/parser/block/code/codeBlock_0004.input @@ -0,0 +1,4 @@ + ``` + (define x 4) + x + ``` diff --git a/src/tests/parser/block/code/codeBlock_0005.expected b/src/tests/parser/block/code/codeBlock_0005.expected new file mode 100644 index 000000000..c043b3019 --- /dev/null +++ b/src/tests/parser/block/code/codeBlock_0005.expected @@ -0,0 +1,8 @@ +Success! Final stack: + (Lean.Doc.Syntax.codeblock + "```" + [`scheme []] + "\n" + (str "\" (define x 4)\\n x\\n\"") + "```") +All input consumed. \ No newline at end of file diff --git a/src/tests/parser/block/code/codeBlock_0005.input b/src/tests/parser/block/code/codeBlock_0005.input new file mode 100644 index 000000000..f07886f27 --- /dev/null +++ b/src/tests/parser/block/code/codeBlock_0005.input @@ -0,0 +1,4 @@ +``` scheme + (define x 4) + x +``` \ No newline at end of file diff --git a/src/tests/parser/block/code/codeBlock_0006.expected b/src/tests/parser/block/code/codeBlock_0006.expected new file mode 100644 index 000000000..c53fe6fcf --- /dev/null +++ b/src/tests/parser/block/code/codeBlock_0006.expected @@ -0,0 +1,8 @@ +Success! Final stack: + (Lean.Doc.Syntax.codeblock + "```" + [`scheme []] + "\n" + (str "\"(define x 4)\\nx\\n\"") + "```") +All input consumed. \ No newline at end of file diff --git a/src/tests/parser/block/code/codeBlock_0006.input b/src/tests/parser/block/code/codeBlock_0006.input new file mode 100644 index 000000000..c91cfd1f6 --- /dev/null +++ b/src/tests/parser/block/code/codeBlock_0006.input @@ -0,0 +1,4 @@ +``` scheme +(define x 4) +x +``` \ No newline at end of file diff --git a/src/tests/parser/block/code/codeBlock_0007.expected b/src/tests/parser/block/code/codeBlock_0007.expected new file mode 100644 index 000000000..4109389b5 --- /dev/null +++ b/src/tests/parser/block/code/codeBlock_0007.expected @@ -0,0 +1,9 @@ +Failure @32 (⟨5, 0⟩): expected column 0 +Final stack: + (Lean.Doc.Syntax.codeblock + "```" + [`scheme []] + "\n" + (str "\"(define x 4)\\nx\\n\"") + ) +Remaining: "more" \ No newline at end of file diff --git a/src/tests/parser/block/code/codeBlock_0007.input b/src/tests/parser/block/code/codeBlock_0007.input new file mode 100644 index 000000000..8b124f80a --- /dev/null +++ b/src/tests/parser/block/code/codeBlock_0007.input @@ -0,0 +1,5 @@ +``` scheme +(define x 4) +x + ```` +more \ No newline at end of file diff --git a/src/tests/parser/block/code/codeBlock_0008.expected b/src/tests/parser/block/code/codeBlock_0008.expected new file mode 100644 index 000000000..5bb5a3913 --- /dev/null +++ b/src/tests/parser/block/code/codeBlock_0008.expected @@ -0,0 +1,9 @@ +Failure @25 (⟨3, 0⟩): expected column 1 +Final stack: + (Lean.Doc.Syntax.codeblock + "```" + [`scheme []] + "\n" + (str "\"\\n\"") + ) +Remaining: "x\n```" \ No newline at end of file diff --git a/src/tests/parser/block/code/codeBlock_0008.input b/src/tests/parser/block/code/codeBlock_0008.input new file mode 100644 index 000000000..036053708 --- /dev/null +++ b/src/tests/parser/block/code/codeBlock_0008.input @@ -0,0 +1,4 @@ + ``` scheme +(define x 4) +x +``` \ No newline at end of file diff --git a/src/tests/parser/block/code/codeBlock_0009.expected b/src/tests/parser/block/code/codeBlock_0009.expected new file mode 100644 index 000000000..224612461 --- /dev/null +++ b/src/tests/parser/block/code/codeBlock_0009.expected @@ -0,0 +1,9 @@ +Failure @32 (⟨4, 3⟩): expected column 1 +Final stack: + (Lean.Doc.Syntax.codeblock + "```" + [`scheme []] + "\n" + (str "\"(define x 4)\\nx\\n\"") + ) +Remaining: "" \ No newline at end of file diff --git a/src/tests/parser/block/code/codeBlock_0009.input b/src/tests/parser/block/code/codeBlock_0009.input new file mode 100644 index 000000000..946bd5816 --- /dev/null +++ b/src/tests/parser/block/code/codeBlock_0009.input @@ -0,0 +1,4 @@ + ``` scheme + (define x 4) + x +``` \ No newline at end of file diff --git a/src/tests/parser/block/code/codeBlock_0010.expected b/src/tests/parser/block/code/codeBlock_0010.expected new file mode 100644 index 000000000..ac290ed14 --- /dev/null +++ b/src/tests/parser/block/code/codeBlock_0010.expected @@ -0,0 +1,9 @@ +Failure @25 (⟨4, 3⟩): expected column 1 +Final stack: + (Lean.Doc.Syntax.codeblock + "```" + [] + "\n" + (str "\"(define x 4)\\nx\\n\"") + ) +Remaining: "" \ No newline at end of file diff --git a/src/tests/parser/block/code/codeBlock_0010.input b/src/tests/parser/block/code/codeBlock_0010.input new file mode 100644 index 000000000..9aaa5b01f --- /dev/null +++ b/src/tests/parser/block/code/codeBlock_0010.input @@ -0,0 +1,4 @@ + ``` + (define x 4) + x +``` \ No newline at end of file diff --git a/src/tests/parser/block/code/codeBlock_0011.expected b/src/tests/parser/block/code/codeBlock_0011.expected new file mode 100644 index 000000000..c71422ee6 --- /dev/null +++ b/src/tests/parser/block/code/codeBlock_0011.expected @@ -0,0 +1,9 @@ +Failure @28 (⟨4, 3⟩): expected column 1 +Final stack: + (Lean.Doc.Syntax.codeblock + "```" + [] + "\n" + (str "\"(define x 4)\\nx\\n\"") + ) +Remaining: "" \ No newline at end of file diff --git a/src/tests/parser/block/code/codeBlock_0011.input b/src/tests/parser/block/code/codeBlock_0011.input new file mode 100644 index 000000000..25afaa302 --- /dev/null +++ b/src/tests/parser/block/code/codeBlock_0011.input @@ -0,0 +1,4 @@ + ``` + (define x 4) + x +``` \ No newline at end of file diff --git a/src/tests/parser/block/code/codeBlock_0012.expected b/src/tests/parser/block/code/codeBlock_0012.expected new file mode 100644 index 000000000..2d816c0be --- /dev/null +++ b/src/tests/parser/block/code/codeBlock_0012.expected @@ -0,0 +1,15 @@ +Success! Final stack: + (Lean.Doc.Syntax.codeblock + "```" + [`scheme + [(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")))]] + "\n" + (str "\"(define x 4)\\nx\\n\"") + "```") +All input consumed. \ No newline at end of file diff --git a/src/tests/parser/block/code/codeBlock_0012.input b/src/tests/parser/block/code/codeBlock_0012.input new file mode 100644 index 000000000..1776232fc --- /dev/null +++ b/src/tests/parser/block/code/codeBlock_0012.input @@ -0,0 +1,4 @@ +``` scheme dialect:="chicken" 43 +(define x 4) +x +``` \ No newline at end of file diff --git a/src/tests/parser/block/code/codeBlock_0013.expected b/src/tests/parser/block/code/codeBlock_0013.expected new file mode 100644 index 000000000..d2496c6ef --- /dev/null +++ b/src/tests/parser/block/code/codeBlock_0013.expected @@ -0,0 +1,15 @@ +Success! Final stack: + (Lean.Doc.Syntax.codeblock + "```" + [`scheme + [(Lean.Doc.Syntax.named + "(" + `dialect + ":=" + (Lean.Doc.Syntax.arg_str + (str "\"chicken\"")) + ")")]] + "\n" + (str "\"(define x 4)\\nx\\n\"") + "```") +All input consumed. \ No newline at end of file diff --git a/src/tests/parser/block/code/codeBlock_0013.input b/src/tests/parser/block/code/codeBlock_0013.input new file mode 100644 index 000000000..f11acdb95 --- /dev/null +++ b/src/tests/parser/block/code/codeBlock_0013.input @@ -0,0 +1,4 @@ +``` scheme (dialect:="chicken") +(define x 4) +x +``` \ No newline at end of file diff --git a/src/tests/parser/block/code/codeBlock_0014.expected b/src/tests/parser/block/code/codeBlock_0014.expected new file mode 100644 index 000000000..988255269 --- /dev/null +++ b/src/tests/parser/block/code/codeBlock_0014.expected @@ -0,0 +1,16 @@ +Failure @30 (⟨1, 30⟩): expected ')' +Final stack: + (Lean.Doc.Syntax.codeblock + "```" + [`scheme + [(Lean.Doc.Syntax.named + "(" + `dialect + ":=" + (Lean.Doc.Syntax.arg_str + (str "\"chicken\"")) + )]] + "\n" + (str "\"(define x 4)\\nx\\n\"") + "```") +Remaining: "\n(define x 4)\nx\n```" \ No newline at end of file diff --git a/src/tests/parser/block/code/codeBlock_0014.input b/src/tests/parser/block/code/codeBlock_0014.input new file mode 100644 index 000000000..bd497fdc2 --- /dev/null +++ b/src/tests/parser/block/code/codeBlock_0014.input @@ -0,0 +1,4 @@ +``` scheme (dialect:="chicken" +(define x 4) +x +``` \ No newline at end of file diff --git a/src/tests/parser/block/directive/directive_0001.expected b/src/tests/parser/block/directive/directive_0001.expected new file mode 100644 index 000000000..5c3341cce --- /dev/null +++ b/src/tests/parser/block/directive/directive_0001.expected @@ -0,0 +1,12 @@ +Success! Final stack: + (Lean.Doc.Syntax.directive + "::::" + `multiPara + [] + "\n" + [(Lean.Doc.Syntax.para + "para{" + [(Lean.Doc.Syntax.text (str "\"foo\""))] + "}")] + "::::") +All input consumed. \ No newline at end of file diff --git a/src/tests/parser/block/directive/directive_0001.input b/src/tests/parser/block/directive/directive_0001.input new file mode 100644 index 000000000..b6878d607 --- /dev/null +++ b/src/tests/parser/block/directive/directive_0001.input @@ -0,0 +1,3 @@ +:::: multiPara +foo +:::: \ No newline at end of file diff --git a/src/tests/parser/block/directive/directive_0002.expected b/src/tests/parser/block/directive/directive_0002.expected new file mode 100644 index 000000000..5c3341cce --- /dev/null +++ b/src/tests/parser/block/directive/directive_0002.expected @@ -0,0 +1,12 @@ +Success! Final stack: + (Lean.Doc.Syntax.directive + "::::" + `multiPara + [] + "\n" + [(Lean.Doc.Syntax.para + "para{" + [(Lean.Doc.Syntax.text (str "\"foo\""))] + "}")] + "::::") +All input consumed. \ No newline at end of file diff --git a/src/tests/parser/block/directive/directive_0002.input b/src/tests/parser/block/directive/directive_0002.input new file mode 100644 index 000000000..07b217bbb --- /dev/null +++ b/src/tests/parser/block/directive/directive_0002.input @@ -0,0 +1,5 @@ +:::: multiPara + + +foo +:::: \ No newline at end of file diff --git a/src/tests/parser/block/directive/directive_0003.expected b/src/tests/parser/block/directive/directive_0003.expected new file mode 100644 index 000000000..fc9e47de4 --- /dev/null +++ b/src/tests/parser/block/directive/directive_0003.expected @@ -0,0 +1,16 @@ +Success! Final stack: + (Lean.Doc.Syntax.directive + ":::" + `multiPara + [(Lean.Doc.Syntax.named_no_paren + `greatness + ":=" + (Lean.Doc.Syntax.arg_str + (str "\"amazing!\"")))] + "\n" + [(Lean.Doc.Syntax.para + "para{" + [(Lean.Doc.Syntax.text (str "\"foo\""))] + "}")] + ":::") +All input consumed. \ No newline at end of file diff --git a/src/tests/parser/block/directive/directive_0003.input b/src/tests/parser/block/directive/directive_0003.input new file mode 100644 index 000000000..847d73799 --- /dev/null +++ b/src/tests/parser/block/directive/directive_0003.input @@ -0,0 +1,3 @@ + ::: multiPara greatness:="amazing!" + foo + ::: diff --git a/src/tests/parser/block/directive/directive_0004.expected b/src/tests/parser/block/directive/directive_0004.expected new file mode 100644 index 000000000..54c523dad --- /dev/null +++ b/src/tests/parser/block/directive/directive_0004.expected @@ -0,0 +1,22 @@ +Success! Final stack: + (Lean.Doc.Syntax.directive + ":::" + `multiPara + [] + "\n" + [(Lean.Doc.Syntax.para + "para{" + [(Lean.Doc.Syntax.text (str "\"foo\""))] + "}") + (Lean.Doc.Syntax.ul + "ul{" + [(Lean.Doc.Syntax.li + "*" + [(Lean.Doc.Syntax.para + "para{" + [(Lean.Doc.Syntax.text + (str "\"List item \""))] + "}")])] + "}")] + ":::") +All input consumed. \ No newline at end of file diff --git a/src/tests/parser/block/directive/directive_0004.input b/src/tests/parser/block/directive/directive_0004.input new file mode 100644 index 000000000..9ab71c6ee --- /dev/null +++ b/src/tests/parser/block/directive/directive_0004.input @@ -0,0 +1,7 @@ + ::: multiPara + foo + + + + * List item + ::: diff --git a/src/tests/parser/block/directive/directive_0005.expected b/src/tests/parser/block/directive/directive_0005.expected new file mode 100644 index 000000000..b59c7b716 --- /dev/null +++ b/src/tests/parser/block/directive/directive_0005.expected @@ -0,0 +1,23 @@ +Success! Final stack: + (Lean.Doc.Syntax.directive + ":::" + `multiPara + [(Lean.Doc.Syntax.anon + (Lean.Doc.Syntax.arg_ident `thing))] + "\n" + [(Lean.Doc.Syntax.para + "para{" + [(Lean.Doc.Syntax.text (str "\"foo\""))] + "}") + (Lean.Doc.Syntax.ul + "ul{" + [(Lean.Doc.Syntax.li + "*" + [(Lean.Doc.Syntax.para + "para{" + [(Lean.Doc.Syntax.text + (str "\"List item \""))] + "}")])] + "}")] + ":::") +All input consumed. \ No newline at end of file diff --git a/src/tests/parser/block/directive/directive_0005.input b/src/tests/parser/block/directive/directive_0005.input new file mode 100644 index 000000000..2d7abfb0b --- /dev/null +++ b/src/tests/parser/block/directive/directive_0005.input @@ -0,0 +1,7 @@ + ::: multiPara thing + foo + + + + * List item + ::: diff --git a/src/tests/parser/block/directive/directive_0006.expected b/src/tests/parser/block/directive/directive_0006.expected new file mode 100644 index 000000000..54c523dad --- /dev/null +++ b/src/tests/parser/block/directive/directive_0006.expected @@ -0,0 +1,22 @@ +Success! Final stack: + (Lean.Doc.Syntax.directive + ":::" + `multiPara + [] + "\n" + [(Lean.Doc.Syntax.para + "para{" + [(Lean.Doc.Syntax.text (str "\"foo\""))] + "}") + (Lean.Doc.Syntax.ul + "ul{" + [(Lean.Doc.Syntax.li + "*" + [(Lean.Doc.Syntax.para + "para{" + [(Lean.Doc.Syntax.text + (str "\"List item \""))] + "}")])] + "}")] + ":::") +All input consumed. \ No newline at end of file diff --git a/src/tests/parser/block/directive/directive_0006.input b/src/tests/parser/block/directive/directive_0006.input new file mode 100644 index 000000000..e281f1f5b --- /dev/null +++ b/src/tests/parser/block/directive/directive_0006.input @@ -0,0 +1,5 @@ + ::: multiPara + foo + + * List item + ::: diff --git a/src/tests/parser/block/header/header_0001.expected b/src/tests/parser/block/header/header_0001.expected new file mode 100644 index 000000000..0170d4860 --- /dev/null +++ b/src/tests/parser/block/header/header_0001.expected @@ -0,0 +1,9 @@ +Success! Final stack: + (Lean.Doc.Syntax.header + "header(" + (num "0") + ")" + "{" + [(Lean.Doc.Syntax.text (str "\"Header!\""))] + "}") +All input consumed. \ No newline at end of file diff --git a/src/tests/parser/block/header/header_0001.input b/src/tests/parser/block/header/header_0001.input new file mode 100644 index 000000000..db23e08da --- /dev/null +++ b/src/tests/parser/block/header/header_0001.input @@ -0,0 +1 @@ +# Header! \ No newline at end of file diff --git a/src/tests/parser/block/olIndicator/lookaheadOrderedListIndicator_0001.expected b/src/tests/parser/block/olIndicator/lookaheadOrderedListIndicator_0001.expected new file mode 100644 index 000000000..b40ba2c60 --- /dev/null +++ b/src/tests/parser/block/olIndicator/lookaheadOrderedListIndicator_0001.expected @@ -0,0 +1,6 @@ +Success! Final stack: + • (num "1") + • "Verso.Parser.OrderedListType.numDot 1" + +Remaining: +"1. " \ No newline at end of file diff --git a/src/tests/parser/block/olIndicator/lookaheadOrderedListIndicator_0001.input b/src/tests/parser/block/olIndicator/lookaheadOrderedListIndicator_0001.input new file mode 100644 index 000000000..1f2b81dae --- /dev/null +++ b/src/tests/parser/block/olIndicator/lookaheadOrderedListIndicator_0001.input @@ -0,0 +1 @@ +1. \ No newline at end of file diff --git a/src/tests/parser/block/olIndicator/lookaheadOrderedListIndicator_0002.expected b/src/tests/parser/block/olIndicator/lookaheadOrderedListIndicator_0002.expected new file mode 100644 index 000000000..8b0339787 --- /dev/null +++ b/src/tests/parser/block/olIndicator/lookaheadOrderedListIndicator_0002.expected @@ -0,0 +1,6 @@ +Success! Final stack: + • (num "2") + • "Verso.Parser.OrderedListType.numDot 2" + +Remaining: +"2. " \ No newline at end of file diff --git a/src/tests/parser/block/olIndicator/lookaheadOrderedListIndicator_0002.input b/src/tests/parser/block/olIndicator/lookaheadOrderedListIndicator_0002.input new file mode 100644 index 000000000..03b8252c5 --- /dev/null +++ b/src/tests/parser/block/olIndicator/lookaheadOrderedListIndicator_0002.input @@ -0,0 +1 @@ +2. \ No newline at end of file diff --git a/src/tests/parser/block/olIndicator/lookaheadOrderedListIndicator_0003.expected b/src/tests/parser/block/olIndicator/lookaheadOrderedListIndicator_0003.expected new file mode 100644 index 000000000..3aaa5a63e --- /dev/null +++ b/src/tests/parser/block/olIndicator/lookaheadOrderedListIndicator_0003.expected @@ -0,0 +1,4 @@ +Failure @0 (⟨1, 0⟩): unexpected end of input +Final stack: + +Remaining: "2." \ No newline at end of file diff --git a/src/tests/parser/block/olIndicator/lookaheadOrderedListIndicator_0003.input b/src/tests/parser/block/olIndicator/lookaheadOrderedListIndicator_0003.input new file mode 100644 index 000000000..c5aa09bb1 --- /dev/null +++ b/src/tests/parser/block/olIndicator/lookaheadOrderedListIndicator_0003.input @@ -0,0 +1 @@ +2. \ No newline at end of file diff --git a/src/tests/parser/block/olIndicator/lookaheadOrderedListIndicator_0004.expected b/src/tests/parser/block/olIndicator/lookaheadOrderedListIndicator_0004.expected new file mode 100644 index 000000000..e97212256 --- /dev/null +++ b/src/tests/parser/block/olIndicator/lookaheadOrderedListIndicator_0004.expected @@ -0,0 +1,6 @@ +Success! Final stack: + • (num "2") + • "Verso.Parser.OrderedListType.parenAfter 2" + +Remaining: +"2) " \ No newline at end of file diff --git a/src/tests/parser/block/olIndicator/lookaheadOrderedListIndicator_0004.input b/src/tests/parser/block/olIndicator/lookaheadOrderedListIndicator_0004.input new file mode 100644 index 000000000..75d671965 --- /dev/null +++ b/src/tests/parser/block/olIndicator/lookaheadOrderedListIndicator_0004.input @@ -0,0 +1 @@ +2) \ No newline at end of file diff --git a/src/tests/parser/block/olIndicator/lookaheadOrderedListIndicator_0005.expected b/src/tests/parser/block/olIndicator/lookaheadOrderedListIndicator_0005.expected new file mode 100644 index 000000000..4ea9f206e --- /dev/null +++ b/src/tests/parser/block/olIndicator/lookaheadOrderedListIndicator_0005.expected @@ -0,0 +1,4 @@ +Failure @0 (⟨1, 0⟩): digits +Final stack: + empty +Remaining: "-23) " \ No newline at end of file diff --git a/src/tests/parser/block/olIndicator/lookaheadOrderedListIndicator_0005.input b/src/tests/parser/block/olIndicator/lookaheadOrderedListIndicator_0005.input new file mode 100644 index 000000000..289c4b456 --- /dev/null +++ b/src/tests/parser/block/olIndicator/lookaheadOrderedListIndicator_0005.input @@ -0,0 +1 @@ +-23) \ No newline at end of file diff --git a/src/tests/parser/block/olIndicator/lookaheadOrderedListIndicator_0006.expected b/src/tests/parser/block/olIndicator/lookaheadOrderedListIndicator_0006.expected new file mode 100644 index 000000000..6e8b27cf5 --- /dev/null +++ b/src/tests/parser/block/olIndicator/lookaheadOrderedListIndicator_0006.expected @@ -0,0 +1,4 @@ +Failure @0 (⟨1, 0⟩): digits +Final stack: + empty +Remaining: "a-23) " \ No newline at end of file diff --git a/src/tests/parser/block/olIndicator/lookaheadOrderedListIndicator_0006.input b/src/tests/parser/block/olIndicator/lookaheadOrderedListIndicator_0006.input new file mode 100644 index 000000000..0e09270fe --- /dev/null +++ b/src/tests/parser/block/olIndicator/lookaheadOrderedListIndicator_0006.input @@ -0,0 +1 @@ +a-23) \ No newline at end of file diff --git a/src/tests/parser/block/olIndicator/lookaheadOrderedListIndicator_0007.expected b/src/tests/parser/block/olIndicator/lookaheadOrderedListIndicator_0007.expected new file mode 100644 index 000000000..9242c5806 --- /dev/null +++ b/src/tests/parser/block/olIndicator/lookaheadOrderedListIndicator_0007.expected @@ -0,0 +1,4 @@ +Failure @0 (⟨1, 0⟩): unexpected ' '; expected ')' or '.' +Final stack: + empty +Remaining: "23 ) " \ No newline at end of file diff --git a/src/tests/parser/block/olIndicator/lookaheadOrderedListIndicator_0007.input b/src/tests/parser/block/olIndicator/lookaheadOrderedListIndicator_0007.input new file mode 100644 index 000000000..120456cae --- /dev/null +++ b/src/tests/parser/block/olIndicator/lookaheadOrderedListIndicator_0007.input @@ -0,0 +1 @@ +23 ) \ No newline at end of file diff --git a/src/tests/parser/block/opener/blockOpener_0001.expected b/src/tests/parser/block/opener/blockOpener_0001.expected new file mode 100644 index 000000000..08f596a60 --- /dev/null +++ b/src/tests/parser/block/opener/blockOpener_0001.expected @@ -0,0 +1,4 @@ +Success! Final stack: + empty +Remaining: +"abc" \ No newline at end of file diff --git a/src/tests/parser/block/opener/blockOpener_0001.input b/src/tests/parser/block/opener/blockOpener_0001.input new file mode 100644 index 000000000..1198a6c90 --- /dev/null +++ b/src/tests/parser/block/opener/blockOpener_0001.input @@ -0,0 +1 @@ ++ abc \ No newline at end of file diff --git a/src/tests/parser/block/opener/blockOpener_0002.expected b/src/tests/parser/block/opener/blockOpener_0002.expected new file mode 100644 index 000000000..08f596a60 --- /dev/null +++ b/src/tests/parser/block/opener/blockOpener_0002.expected @@ -0,0 +1,4 @@ +Success! Final stack: + empty +Remaining: +"abc" \ No newline at end of file diff --git a/src/tests/parser/block/opener/blockOpener_0002.input b/src/tests/parser/block/opener/blockOpener_0002.input new file mode 100644 index 000000000..1c98dec5d --- /dev/null +++ b/src/tests/parser/block/opener/blockOpener_0002.input @@ -0,0 +1 @@ +* abc \ No newline at end of file diff --git a/src/tests/parser/block/opener/blockOpener_0003.expected b/src/tests/parser/block/opener/blockOpener_0003.expected new file mode 100644 index 000000000..08f596a60 --- /dev/null +++ b/src/tests/parser/block/opener/blockOpener_0003.expected @@ -0,0 +1,4 @@ +Success! Final stack: + empty +Remaining: +"abc" \ No newline at end of file diff --git a/src/tests/parser/block/opener/blockOpener_0003.input b/src/tests/parser/block/opener/blockOpener_0003.input new file mode 100644 index 000000000..1198a6c90 --- /dev/null +++ b/src/tests/parser/block/opener/blockOpener_0003.input @@ -0,0 +1 @@ ++ abc \ No newline at end of file diff --git a/src/tests/parser/block/recover/recoverBlock_0001.expected b/src/tests/parser/block/recover/recoverBlock_0001.expected new file mode 100644 index 000000000..c92769b4e --- /dev/null +++ b/src/tests/parser/block/recover/recoverBlock_0001.expected @@ -0,0 +1,46 @@ +Failure @55 (⟨3, 0⟩): '{'; expected '![', '$$', '$', '[' or '[^' +Final stack: + (Lean.Doc.Syntax.para + "para{" + [(Lean.Doc.Syntax.role + "{" + `tactic + [] + "}" + "[" + [(Lean.Doc.Syntax.code + "`" + (str "\"rw\"") + "`")] + "]") + (Lean.Doc.Syntax.role + "{" + `lit + [] + "}" + "[" + [(Lean.Doc.Syntax.code + "`" + (str "\" [t] \"") + "`")] + "]") + (Lean.Doc.Syntax.role + "{" + `kw + [] + "}" + "[" + [(Lean.Doc.Syntax.code + "`" + (str "\"at\"") + "`")] + "]") + (Lean.Doc.Syntax.role + "{" + `lit + [] + "}" + "[" + [(Lean.Doc.Syntax.footnote )] + "]")]) +Remaining: "test" \ No newline at end of file diff --git a/src/tests/parser/block/recover/recoverBlock_0001.input b/src/tests/parser/block/recover/recoverBlock_0001.input new file mode 100644 index 000000000..14718cb34 --- /dev/null +++ b/src/tests/parser/block/recover/recoverBlock_0001.input @@ -0,0 +1,3 @@ +{tactic}`rw`{lit}` [t] `{kw}`at`{lit} h` applies th + +test \ No newline at end of file diff --git a/src/tests/parser/block/ulIndicator/lookaheadUnorderedListIndicator_0001.expected b/src/tests/parser/block/ulIndicator/lookaheadUnorderedListIndicator_0001.expected new file mode 100644 index 000000000..9c3f712e4 --- /dev/null +++ b/src/tests/parser/block/ulIndicator/lookaheadUnorderedListIndicator_0001.expected @@ -0,0 +1,4 @@ +Success! Final stack: + "Verso.Parser.UnorderedListType.asterisk" +Remaining: +"* " \ No newline at end of file diff --git a/src/tests/parser/block/ulIndicator/lookaheadUnorderedListIndicator_0001.input b/src/tests/parser/block/ulIndicator/lookaheadUnorderedListIndicator_0001.input new file mode 100644 index 000000000..e48d96ff9 --- /dev/null +++ b/src/tests/parser/block/ulIndicator/lookaheadUnorderedListIndicator_0001.input @@ -0,0 +1 @@ +* \ No newline at end of file diff --git a/src/tests/parser/block/ulIndicator/lookaheadUnorderedListIndicator_0002.expected b/src/tests/parser/block/ulIndicator/lookaheadUnorderedListIndicator_0002.expected new file mode 100644 index 000000000..3b258a351 --- /dev/null +++ b/src/tests/parser/block/ulIndicator/lookaheadUnorderedListIndicator_0002.expected @@ -0,0 +1,4 @@ +Success! Final stack: + "Verso.Parser.UnorderedListType.dash" +Remaining: +"- " \ No newline at end of file diff --git a/src/tests/parser/block/ulIndicator/lookaheadUnorderedListIndicator_0002.input b/src/tests/parser/block/ulIndicator/lookaheadUnorderedListIndicator_0002.input new file mode 100644 index 000000000..0d439ac8b --- /dev/null +++ b/src/tests/parser/block/ulIndicator/lookaheadUnorderedListIndicator_0002.input @@ -0,0 +1 @@ +- \ No newline at end of file diff --git a/src/tests/parser/block/ulIndicator/lookaheadUnorderedListIndicator_0003.expected b/src/tests/parser/block/ulIndicator/lookaheadUnorderedListIndicator_0003.expected new file mode 100644 index 000000000..0ec34f7b7 --- /dev/null +++ b/src/tests/parser/block/ulIndicator/lookaheadUnorderedListIndicator_0003.expected @@ -0,0 +1,4 @@ +Success! Final stack: + "Verso.Parser.UnorderedListType.plus" +Remaining: +"+ " \ No newline at end of file diff --git a/src/tests/parser/block/ulIndicator/lookaheadUnorderedListIndicator_0003.input b/src/tests/parser/block/ulIndicator/lookaheadUnorderedListIndicator_0003.input new file mode 100644 index 000000000..2ca484d62 --- /dev/null +++ b/src/tests/parser/block/ulIndicator/lookaheadUnorderedListIndicator_0003.input @@ -0,0 +1 @@ ++ \ No newline at end of file diff --git a/src/tests/parser/block/ulIndicator/lookaheadUnorderedListIndicator_0004.expected b/src/tests/parser/block/ulIndicator/lookaheadUnorderedListIndicator_0004.expected new file mode 100644 index 000000000..9c3f712e4 --- /dev/null +++ b/src/tests/parser/block/ulIndicator/lookaheadUnorderedListIndicator_0004.expected @@ -0,0 +1,4 @@ +Success! Final stack: + "Verso.Parser.UnorderedListType.asterisk" +Remaining: +"* " \ No newline at end of file diff --git a/src/tests/parser/block/ulIndicator/lookaheadUnorderedListIndicator_0004.input b/src/tests/parser/block/ulIndicator/lookaheadUnorderedListIndicator_0004.input new file mode 100644 index 000000000..e48d96ff9 --- /dev/null +++ b/src/tests/parser/block/ulIndicator/lookaheadUnorderedListIndicator_0004.input @@ -0,0 +1 @@ +* \ No newline at end of file diff --git a/src/tests/parser/block/ulIndicator/lookaheadUnorderedListIndicator_0005.expected b/src/tests/parser/block/ulIndicator/lookaheadUnorderedListIndicator_0005.expected new file mode 100644 index 000000000..54ab873ab --- /dev/null +++ b/src/tests/parser/block/ulIndicator/lookaheadUnorderedListIndicator_0005.expected @@ -0,0 +1,4 @@ +Failure @0 (⟨1, 0⟩): unexpected end of input +Final stack: + +Remaining: " *" \ No newline at end of file diff --git a/src/tests/parser/block/ulIndicator/lookaheadUnorderedListIndicator_0005.input b/src/tests/parser/block/ulIndicator/lookaheadUnorderedListIndicator_0005.input new file mode 100644 index 000000000..42780ecb1 --- /dev/null +++ b/src/tests/parser/block/ulIndicator/lookaheadUnorderedListIndicator_0005.input @@ -0,0 +1 @@ + * \ No newline at end of file diff --git a/src/tests/parser/block/ulIndicator/lookaheadUnorderedListIndicator_0006.expected b/src/tests/parser/block/ulIndicator/lookaheadUnorderedListIndicator_0006.expected new file mode 100644 index 000000000..78f009875 --- /dev/null +++ b/src/tests/parser/block/ulIndicator/lookaheadUnorderedListIndicator_0006.expected @@ -0,0 +1,5 @@ +Failure @0 (⟨1, 0⟩): ' +' +Final stack: + +Remaining: "** " \ No newline at end of file diff --git a/src/tests/parser/block/ulIndicator/lookaheadUnorderedListIndicator_0006.input b/src/tests/parser/block/ulIndicator/lookaheadUnorderedListIndicator_0006.input new file mode 100644 index 000000000..0ca974ea5 --- /dev/null +++ b/src/tests/parser/block/ulIndicator/lookaheadUnorderedListIndicator_0006.input @@ -0,0 +1 @@ +** \ No newline at end of file diff --git a/src/tests/parser/blocks/recover/recoverBlocks_0001.expected b/src/tests/parser/blocks/recover/recoverBlocks_0001.expected new file mode 100644 index 000000000..e2c00cb0d --- /dev/null +++ b/src/tests/parser/blocks/recover/recoverBlocks_0001.expected @@ -0,0 +1,44 @@ +Failure @92 (⟨7, 0⟩): '{'; expected '![', '$$', '$', '[' or '[^' +Final stack: + [(Lean.Doc.Syntax.dl + "dl{" + [(Lean.Doc.Syntax.desc + ":" + [(Lean.Doc.Syntax.text (str "\" \"")) + (Lean.Doc.Syntax.role + "{" + `ref + [(Lean.Doc.Syntax.anon + (Lean.Doc.Syntax.arg_ident `defs))] + "}" + "[" + [(Lean.Doc.Syntax.text + (str "\"Basic definitions\""))] + "]")] + "=>" + [(Lean.Doc.Syntax.para + "para{" + [(Lean.Doc.Syntax.text + (str "\"The def is something\""))] + "}")]) + (Lean.Doc.Syntax.desc + ":" + [(Lean.Doc.Syntax.text (str "\" \"")) + (Lean.Doc.Syntax.role + "{" + `ref + [(Lean.Doc.Syntax.anon + (Lean.Doc.Syntax.arg_ident `large))] + "}" + "[" + [(Lean.Doc.Syntax.role + "{" + `Sufficiently + [(Lean.Doc.Syntax.anon + (Lean.Doc.Syntax.arg_ident `large))] + "}" + "[" + [(Lean.Doc.Syntax.footnote )] + "]")] + "]")])])] +Remaining: " More text\n\n: `foo`\n\n Thing\n" \ No newline at end of file diff --git a/src/tests/parser/blocks/recover/recoverBlocks_0001.input b/src/tests/parser/blocks/recover/recoverBlocks_0001.input new file mode 100644 index 000000000..96a14844c --- /dev/null +++ b/src/tests/parser/blocks/recover/recoverBlocks_0001.input @@ -0,0 +1,11 @@ +: {ref defs}[Basic definitions] + + The def is something + +: {ref large}{Sufficiently large} + + More text + +: `foo` + + Thing diff --git a/src/tests/parser/document/document_0001.expected b/src/tests/parser/document/document_0001.expected new file mode 100644 index 000000000..fb006f0ba --- /dev/null +++ b/src/tests/parser/document/document_0001.expected @@ -0,0 +1,19 @@ +Success! Final stack: + [(Lean.Doc.Syntax.para + "para{" + [(Lean.Doc.Syntax.image + "![" + (str "\"Lean logo\"") + "]" + (Lean.Doc.Syntax.url + "(" + (str "\"/static/lean_logo.svg\"") + ")"))] + "}") + (Lean.Doc.Syntax.para + "para{" + [(Lean.Doc.Syntax.text + (str + "\"This is an example website/blog, for testing purposes.\""))] + "}")] +All input consumed. \ No newline at end of file diff --git a/src/tests/parser/document/document_0001.input b/src/tests/parser/document/document_0001.input new file mode 100644 index 000000000..ceb60ff23 --- /dev/null +++ b/src/tests/parser/document/document_0001.input @@ -0,0 +1,3 @@ +![Lean logo](/static/lean_logo.svg) + +This is an example website/blog, for testing purposes. \ No newline at end of file diff --git a/src/tests/parser/inline/code/code_0001.expected b/src/tests/parser/inline/code/code_0001.expected new file mode 100644 index 000000000..6faadc05a --- /dev/null +++ b/src/tests/parser/inline/code/code_0001.expected @@ -0,0 +1,6 @@ +Success! Final stack: + (Lean.Doc.Syntax.code + "``" + (str "\"foo bar\"") + "``") +All input consumed. \ No newline at end of file diff --git a/src/tests/parser/inline/code/code_0001.input b/src/tests/parser/inline/code/code_0001.input new file mode 100644 index 000000000..26c2351ec --- /dev/null +++ b/src/tests/parser/inline/code/code_0001.input @@ -0,0 +1 @@ +``foo bar`` \ No newline at end of file diff --git a/src/tests/parser/inline/code/code_0002.expected b/src/tests/parser/inline/code/code_0002.expected new file mode 100644 index 000000000..cd7d7a06a --- /dev/null +++ b/src/tests/parser/inline/code/code_0002.expected @@ -0,0 +1,3 @@ +Success! Final stack: + (Lean.Doc.Syntax.code "`" (str "\" \"") "`") +All input consumed. \ No newline at end of file diff --git a/src/tests/parser/inline/code/code_0002.input b/src/tests/parser/inline/code/code_0002.input new file mode 100644 index 000000000..bac7389bb --- /dev/null +++ b/src/tests/parser/inline/code/code_0002.input @@ -0,0 +1 @@ +` ` \ No newline at end of file diff --git a/src/tests/parser/inline/code/code_0003.expected b/src/tests/parser/inline/code/code_0003.expected new file mode 100644 index 000000000..549b305de --- /dev/null +++ b/src/tests/parser/inline/code/code_0003.expected @@ -0,0 +1,3 @@ +Success! Final stack: + (Lean.Doc.Syntax.code "`" (str "\" \"") "`") +All input consumed. \ No newline at end of file diff --git a/src/tests/parser/inline/code/code_0003.input b/src/tests/parser/inline/code/code_0003.input new file mode 100644 index 000000000..e6ba24d95 --- /dev/null +++ b/src/tests/parser/inline/code/code_0003.input @@ -0,0 +1 @@ +` ` \ No newline at end of file diff --git a/src/tests/parser/inline/code/code_0004.expected b/src/tests/parser/inline/code/code_0004.expected new file mode 100644 index 000000000..b121bb503 --- /dev/null +++ b/src/tests/parser/inline/code/code_0004.expected @@ -0,0 +1,3 @@ +Success! Final stack: + (Lean.Doc.Syntax.code "`" (str "\" \"") "`") +All input consumed. \ No newline at end of file diff --git a/src/tests/parser/inline/code/code_0004.input b/src/tests/parser/inline/code/code_0004.input new file mode 100644 index 000000000..a3ece3ead --- /dev/null +++ b/src/tests/parser/inline/code/code_0004.input @@ -0,0 +1 @@ +` ` \ No newline at end of file diff --git a/src/tests/parser/inline/code/code_0005.expected b/src/tests/parser/inline/code/code_0005.expected new file mode 100644 index 000000000..1af0b73d3 --- /dev/null +++ b/src/tests/parser/inline/code/code_0005.expected @@ -0,0 +1,3 @@ +Success! Final stack: + (Lean.Doc.Syntax.code "`" (str "\"x\"") "`") +All input consumed. \ No newline at end of file diff --git a/src/tests/parser/inline/code/code_0005.input b/src/tests/parser/inline/code/code_0005.input new file mode 100644 index 000000000..8cc1e2f98 --- /dev/null +++ b/src/tests/parser/inline/code/code_0005.input @@ -0,0 +1 @@ +` x ` \ No newline at end of file diff --git a/src/tests/parser/inline/code/code_0006.expected b/src/tests/parser/inline/code/code_0006.expected new file mode 100644 index 000000000..32c839c11 --- /dev/null +++ b/src/tests/parser/inline/code/code_0006.expected @@ -0,0 +1,6 @@ +Success! Final stack: + (Lean.Doc.Syntax.code + "``" + (str "\"foo `stuff` bar\"") + "``") +All input consumed. \ No newline at end of file diff --git a/src/tests/parser/inline/code/code_0006.input b/src/tests/parser/inline/code/code_0006.input new file mode 100644 index 000000000..6f340fa8d --- /dev/null +++ b/src/tests/parser/inline/code/code_0006.input @@ -0,0 +1 @@ +``foo `stuff` bar`` \ No newline at end of file diff --git a/src/tests/parser/inline/code/code_0007.expected b/src/tests/parser/inline/code/code_0007.expected new file mode 100644 index 000000000..35297485f --- /dev/null +++ b/src/tests/parser/inline/code/code_0007.expected @@ -0,0 +1,7 @@ +Failure @4 (⟨1, 4⟩): expected '`' to close inline code +Final stack: + (Lean.Doc.Syntax.code + "`" + (str "\"foo\"") + ) +Remaining: "" \ No newline at end of file diff --git a/src/tests/parser/inline/code/code_0007.input b/src/tests/parser/inline/code/code_0007.input new file mode 100644 index 000000000..8814874d8 --- /dev/null +++ b/src/tests/parser/inline/code/code_0007.input @@ -0,0 +1 @@ +`foo \ No newline at end of file diff --git a/src/tests/parser/inline/code/code_0008.expected b/src/tests/parser/inline/code/code_0008.expected new file mode 100644 index 000000000..aff92ea2b --- /dev/null +++ b/src/tests/parser/inline/code/code_0008.expected @@ -0,0 +1,3 @@ +Success! Final stack: + (Lean.Doc.Syntax.code "`" (str "\" foo\"") "`") +All input consumed. \ No newline at end of file diff --git a/src/tests/parser/inline/code/code_0008.input b/src/tests/parser/inline/code/code_0008.input new file mode 100644 index 000000000..87e9555ea --- /dev/null +++ b/src/tests/parser/inline/code/code_0008.input @@ -0,0 +1 @@ +` foo` \ No newline at end of file diff --git a/src/tests/parser/inline/code/code_0009.expected b/src/tests/parser/inline/code/code_0009.expected new file mode 100644 index 000000000..2e0a05c54 --- /dev/null +++ b/src/tests/parser/inline/code/code_0009.expected @@ -0,0 +1,3 @@ +Success! Final stack: + (Lean.Doc.Syntax.code "`" (str "\"foo\"") "`") +All input consumed. \ No newline at end of file diff --git a/src/tests/parser/inline/code/code_0009.input b/src/tests/parser/inline/code/code_0009.input new file mode 100644 index 000000000..cfc7ed5fe --- /dev/null +++ b/src/tests/parser/inline/code/code_0009.input @@ -0,0 +1 @@ +` foo ` \ No newline at end of file diff --git a/src/tests/parser/inline/code/code_0010.expected b/src/tests/parser/inline/code/code_0010.expected new file mode 100644 index 000000000..cccc91e0a --- /dev/null +++ b/src/tests/parser/inline/code/code_0010.expected @@ -0,0 +1,6 @@ +Success! Final stack: + (Lean.Doc.Syntax.code + "`" + (str "\"fo\\no\"") + "`") +All input consumed. \ No newline at end of file diff --git a/src/tests/parser/inline/code/code_0010.input b/src/tests/parser/inline/code/code_0010.input new file mode 100644 index 000000000..018a5bfe1 --- /dev/null +++ b/src/tests/parser/inline/code/code_0010.input @@ -0,0 +1,2 @@ +` fo +o ` \ No newline at end of file diff --git a/src/tests/parser/inline/code/code_0011.expected b/src/tests/parser/inline/code/code_0011.expected new file mode 100644 index 000000000..f4be83ef0 --- /dev/null +++ b/src/tests/parser/inline/code/code_0011.expected @@ -0,0 +1,3 @@ +Success! Final stack: + (Lean.Doc.Syntax.code "``" (str "\"`x\"") "``") +All input consumed. \ No newline at end of file diff --git a/src/tests/parser/inline/code/code_0011.input b/src/tests/parser/inline/code/code_0011.input new file mode 100644 index 000000000..6b1d3de5b --- /dev/null +++ b/src/tests/parser/inline/code/code_0011.input @@ -0,0 +1 @@ +`` `x `` \ No newline at end of file diff --git a/src/tests/parser/inline/emph/emph_0001.expected b/src/tests/parser/inline/emph/emph_0001.expected new file mode 100644 index 000000000..13f6c44a3 --- /dev/null +++ b/src/tests/parser/inline/emph/emph_0001.expected @@ -0,0 +1,6 @@ +Success! Final stack: + (Lean.Doc.Syntax.emph + "_" + [(Lean.Doc.Syntax.text (str "\"aa\""))] + "_") +All input consumed. \ No newline at end of file diff --git a/src/tests/parser/inline/emph/emph_0001.input b/src/tests/parser/inline/emph/emph_0001.input new file mode 100644 index 000000000..e48a4bf50 --- /dev/null +++ b/src/tests/parser/inline/emph/emph_0001.input @@ -0,0 +1 @@ +_aa_ \ No newline at end of file diff --git a/src/tests/parser/inline/emph/emph_0002.expected b/src/tests/parser/inline/emph/emph_0002.expected new file mode 100644 index 000000000..c9eb95adb --- /dev/null +++ b/src/tests/parser/inline/emph/emph_0002.expected @@ -0,0 +1,7 @@ +Failure @4 (⟨1, 4⟩): expected '_' without preceding space +Final stack: + (Lean.Doc.Syntax.emph + "_" + [(Lean.Doc.Syntax.text (str "\"aa \""))] + ) +Remaining: "_" \ No newline at end of file diff --git a/src/tests/parser/inline/emph/emph_0002.input b/src/tests/parser/inline/emph/emph_0002.input new file mode 100644 index 000000000..07c26144b --- /dev/null +++ b/src/tests/parser/inline/emph/emph_0002.input @@ -0,0 +1 @@ +_aa _ \ No newline at end of file diff --git a/src/tests/parser/inline/emph/emph_0003.expected b/src/tests/parser/inline/emph/emph_0003.expected new file mode 100644 index 000000000..a86956ca6 --- /dev/null +++ b/src/tests/parser/inline/emph/emph_0003.expected @@ -0,0 +1,4 @@ +Failure @0 (⟨1, 0⟩): unexpected space or newline after opener +Final stack: + (Lean.Doc.Syntax.emph "_" ) +Remaining: "_ aa_" \ No newline at end of file diff --git a/src/tests/parser/inline/emph/emph_0003.input b/src/tests/parser/inline/emph/emph_0003.input new file mode 100644 index 000000000..c09ead4eb --- /dev/null +++ b/src/tests/parser/inline/emph/emph_0003.input @@ -0,0 +1 @@ +_ aa_ \ No newline at end of file diff --git a/src/tests/parser/inline/oneInline_0001.expected b/src/tests/parser/inline/oneInline_0001.expected new file mode 100644 index 000000000..6faadc05a --- /dev/null +++ b/src/tests/parser/inline/oneInline_0001.expected @@ -0,0 +1,6 @@ +Success! Final stack: + (Lean.Doc.Syntax.code + "``" + (str "\"foo bar\"") + "``") +All input consumed. \ No newline at end of file diff --git a/src/tests/parser/inline/oneInline_0001.input b/src/tests/parser/inline/oneInline_0001.input new file mode 100644 index 000000000..26c2351ec --- /dev/null +++ b/src/tests/parser/inline/oneInline_0001.input @@ -0,0 +1 @@ +``foo bar`` \ No newline at end of file diff --git a/src/tests/parser/inline/oneInline_0002.expected b/src/tests/parser/inline/oneInline_0002.expected new file mode 100644 index 000000000..32c839c11 --- /dev/null +++ b/src/tests/parser/inline/oneInline_0002.expected @@ -0,0 +1,6 @@ +Success! Final stack: + (Lean.Doc.Syntax.code + "``" + (str "\"foo `stuff` bar\"") + "``") +All input consumed. \ No newline at end of file diff --git a/src/tests/parser/inline/oneInline_0002.input b/src/tests/parser/inline/oneInline_0002.input new file mode 100644 index 000000000..6f340fa8d --- /dev/null +++ b/src/tests/parser/inline/oneInline_0002.input @@ -0,0 +1 @@ +``foo `stuff` bar`` \ No newline at end of file diff --git a/src/tests/parser/inline/oneInline_0003.expected b/src/tests/parser/inline/oneInline_0003.expected new file mode 100644 index 000000000..35297485f --- /dev/null +++ b/src/tests/parser/inline/oneInline_0003.expected @@ -0,0 +1,7 @@ +Failure @4 (⟨1, 4⟩): expected '`' to close inline code +Final stack: + (Lean.Doc.Syntax.code + "`" + (str "\"foo\"") + ) +Remaining: "" \ No newline at end of file diff --git a/src/tests/parser/inline/oneInline_0003.input b/src/tests/parser/inline/oneInline_0003.input new file mode 100644 index 000000000..8814874d8 --- /dev/null +++ b/src/tests/parser/inline/oneInline_0003.input @@ -0,0 +1 @@ +`foo \ No newline at end of file diff --git a/src/tests/parser/inline/oneInline_0004.expected b/src/tests/parser/inline/oneInline_0004.expected new file mode 100644 index 000000000..aff92ea2b --- /dev/null +++ b/src/tests/parser/inline/oneInline_0004.expected @@ -0,0 +1,3 @@ +Success! Final stack: + (Lean.Doc.Syntax.code "`" (str "\" foo\"") "`") +All input consumed. \ No newline at end of file diff --git a/src/tests/parser/inline/oneInline_0004.input b/src/tests/parser/inline/oneInline_0004.input new file mode 100644 index 000000000..87e9555ea --- /dev/null +++ b/src/tests/parser/inline/oneInline_0004.input @@ -0,0 +1 @@ +` foo` \ No newline at end of file diff --git a/src/tests/parser/inline/oneInline_0005.expected b/src/tests/parser/inline/oneInline_0005.expected new file mode 100644 index 000000000..2e0a05c54 --- /dev/null +++ b/src/tests/parser/inline/oneInline_0005.expected @@ -0,0 +1,3 @@ +Success! Final stack: + (Lean.Doc.Syntax.code "`" (str "\"foo\"") "`") +All input consumed. \ No newline at end of file diff --git a/src/tests/parser/inline/oneInline_0005.input b/src/tests/parser/inline/oneInline_0005.input new file mode 100644 index 000000000..cfc7ed5fe --- /dev/null +++ b/src/tests/parser/inline/oneInline_0005.input @@ -0,0 +1 @@ +` foo ` \ No newline at end of file diff --git a/src/tests/parser/inline/oneInline_0006.expected b/src/tests/parser/inline/oneInline_0006.expected new file mode 100644 index 000000000..cccc91e0a --- /dev/null +++ b/src/tests/parser/inline/oneInline_0006.expected @@ -0,0 +1,6 @@ +Success! Final stack: + (Lean.Doc.Syntax.code + "`" + (str "\"fo\\no\"") + "`") +All input consumed. \ No newline at end of file diff --git a/src/tests/parser/inline/oneInline_0006.input b/src/tests/parser/inline/oneInline_0006.input new file mode 100644 index 000000000..018a5bfe1 --- /dev/null +++ b/src/tests/parser/inline/oneInline_0006.input @@ -0,0 +1,2 @@ +` fo +o ` \ No newline at end of file diff --git a/src/tests/parser/inline/oneInline_0007.expected b/src/tests/parser/inline/oneInline_0007.expected new file mode 100644 index 000000000..e8271e541 --- /dev/null +++ b/src/tests/parser/inline/oneInline_0007.expected @@ -0,0 +1,7 @@ +Failure @6 (⟨2, 0⟩): expected '``' to close inline code +Final stack: + (Lean.Doc.Syntax.code + "``" + (str "\" fo\"") + ) +Remaining: "o `" \ No newline at end of file diff --git a/src/tests/parser/inline/oneInline_0007.input b/src/tests/parser/inline/oneInline_0007.input new file mode 100644 index 000000000..5a0c67cc4 --- /dev/null +++ b/src/tests/parser/inline/oneInline_0007.input @@ -0,0 +1,2 @@ +`` fo +o ` \ No newline at end of file diff --git a/src/tests/parser/inline/oneInline_0008.expected b/src/tests/parser/inline/oneInline_0008.expected new file mode 100644 index 000000000..3c2384895 --- /dev/null +++ b/src/tests/parser/inline/oneInline_0008.expected @@ -0,0 +1,10 @@ +Success! Final stack: + (Lean.Doc.Syntax.bold + "**" + [(Lean.Doc.Syntax.text (str "\"aa\"")) + (Lean.Doc.Syntax.linebreak + "line!" + (str "\"\\n\"")) + (Lean.Doc.Syntax.text (str "\"bb\""))] + "**") +All input consumed. \ No newline at end of file diff --git a/src/tests/parser/inline/oneInline_0008.input b/src/tests/parser/inline/oneInline_0008.input new file mode 100644 index 000000000..d52eda654 --- /dev/null +++ b/src/tests/parser/inline/oneInline_0008.input @@ -0,0 +1,2 @@ +**aa +bb** \ No newline at end of file diff --git a/src/tests/parser/inline/oneInline_0009.expected b/src/tests/parser/inline/oneInline_0009.expected new file mode 100644 index 000000000..ff7a12a23 --- /dev/null +++ b/src/tests/parser/inline/oneInline_0009.expected @@ -0,0 +1,4 @@ +Success! Final stack: + (Lean.Doc.Syntax.text (str "\"a \"")) +Remaining: +"* b" \ No newline at end of file diff --git a/src/tests/parser/inline/oneInline_0009.input b/src/tests/parser/inline/oneInline_0009.input new file mode 100644 index 000000000..8415737ae --- /dev/null +++ b/src/tests/parser/inline/oneInline_0009.input @@ -0,0 +1 @@ +a * b \ No newline at end of file diff --git a/src/tests/parser/inline/oneInline_0010.expected b/src/tests/parser/inline/oneInline_0010.expected new file mode 100644 index 000000000..6633c3fb0 --- /dev/null +++ b/src/tests/parser/inline/oneInline_0010.expected @@ -0,0 +1,10 @@ +Success! Final stack: + (Lean.Doc.Syntax.link + "[" + [(Lean.Doc.Syntax.text (str "\"Wikipedia\""))] + "]" + (Lean.Doc.Syntax.url + "(" + (str "\"https://en.wikipedia.org\"") + ")")) +All input consumed. \ No newline at end of file diff --git a/src/tests/parser/inline/oneInline_0010.input b/src/tests/parser/inline/oneInline_0010.input new file mode 100644 index 000000000..35ac92890 --- /dev/null +++ b/src/tests/parser/inline/oneInline_0010.input @@ -0,0 +1 @@ +[Wikipedia](https://en.wikipedia.org) \ No newline at end of file diff --git a/src/tests/parser/inline/oneInline_0011.expected b/src/tests/parser/inline/oneInline_0011.expected new file mode 100644 index 000000000..ee49cae64 --- /dev/null +++ b/src/tests/parser/inline/oneInline_0011.expected @@ -0,0 +1,10 @@ +Success! Final stack: + (Lean.Doc.Syntax.image + "![" + (str "\"\"") + "]" + (Lean.Doc.Syntax.url + "(" + (str "\"logo.png\"") + ")")) +All input consumed. \ No newline at end of file diff --git a/src/tests/parser/inline/oneInline_0011.input b/src/tests/parser/inline/oneInline_0011.input new file mode 100644 index 000000000..67f751262 --- /dev/null +++ b/src/tests/parser/inline/oneInline_0011.input @@ -0,0 +1 @@ +![](logo.png) \ No newline at end of file diff --git a/src/tests/parser/inline/oneInline_0012.expected b/src/tests/parser/inline/oneInline_0012.expected new file mode 100644 index 000000000..eb0441996 --- /dev/null +++ b/src/tests/parser/inline/oneInline_0012.expected @@ -0,0 +1,11 @@ +Failure @12 (⟨1, 12⟩): expected ')' +Final stack: + (Lean.Doc.Syntax.image + "![" + (str "\"\"") + "]" + (Lean.Doc.Syntax.url + "(" + (str "\"logo.png\"") + )) +Remaining: "\nabc" \ No newline at end of file diff --git a/src/tests/parser/inline/oneInline_0012.input b/src/tests/parser/inline/oneInline_0012.input new file mode 100644 index 000000000..5e8cc6b46 --- /dev/null +++ b/src/tests/parser/inline/oneInline_0012.input @@ -0,0 +1,2 @@ +![](logo.png +abc \ No newline at end of file diff --git a/src/tests/parser/inline/oneInline_0013.expected b/src/tests/parser/inline/oneInline_0013.expected new file mode 100644 index 000000000..419d9fa04 --- /dev/null +++ b/src/tests/parser/inline/oneInline_0013.expected @@ -0,0 +1,7 @@ +Failure @5 (⟨1, 5⟩): expected ']' +Final stack: + (Lean.Doc.Syntax.image + "![" + (str "\"abc\"") + ) +Remaining: "\n123" \ No newline at end of file diff --git a/src/tests/parser/inline/oneInline_0013.input b/src/tests/parser/inline/oneInline_0013.input new file mode 100644 index 000000000..018259b0f --- /dev/null +++ b/src/tests/parser/inline/oneInline_0013.input @@ -0,0 +1,2 @@ +![abc +123 \ No newline at end of file diff --git a/src/tests/parser/inline/oneInline_0014.expected b/src/tests/parser/inline/oneInline_0014.expected new file mode 100644 index 000000000..5e7d1406e --- /dev/null +++ b/src/tests/parser/inline/oneInline_0014.expected @@ -0,0 +1,10 @@ +Success! Final stack: + (Lean.Doc.Syntax.image + "![" + (str "\"alt text is good\"") + "]" + (Lean.Doc.Syntax.url + "(" + (str "\"logo.png\"") + ")")) +All input consumed. \ No newline at end of file diff --git a/src/tests/parser/inline/oneInline_0014.input b/src/tests/parser/inline/oneInline_0014.input new file mode 100644 index 000000000..9e92e39d8 --- /dev/null +++ b/src/tests/parser/inline/oneInline_0014.input @@ -0,0 +1 @@ +![alt text is good](logo.png) \ No newline at end of file diff --git a/src/tests/parser/inline/oneInline_0015.expected b/src/tests/parser/inline/oneInline_0015.expected new file mode 100644 index 000000000..f30b4eae1 --- /dev/null +++ b/src/tests/parser/inline/oneInline_0015.expected @@ -0,0 +1,8 @@ +Failure @19 (⟨1, 19⟩): expected '(' or '[' +Final stack: + (Lean.Doc.Syntax.image + "![" + (str "\"alt text is good\"") + "]" + (Lean.Doc.Syntax.url )) +Remaining: "](logo.png)" \ No newline at end of file diff --git a/src/tests/parser/inline/oneInline_0015.input b/src/tests/parser/inline/oneInline_0015.input new file mode 100644 index 000000000..e4b914937 --- /dev/null +++ b/src/tests/parser/inline/oneInline_0015.input @@ -0,0 +1 @@ +![alt text is good]](logo.png) \ No newline at end of file diff --git a/src/tests/parser/inline/oneInline_0016.expected b/src/tests/parser/inline/oneInline_0016.expected new file mode 100644 index 000000000..876a08e91 --- /dev/null +++ b/src/tests/parser/inline/oneInline_0016.expected @@ -0,0 +1,6 @@ +Success! Final stack: + (Lean.Doc.Syntax.footnote + "[^" + (str "\"1\"") + "]") +All input consumed. \ No newline at end of file diff --git a/src/tests/parser/inline/oneInline_0016.input b/src/tests/parser/inline/oneInline_0016.input new file mode 100644 index 000000000..bea07b734 --- /dev/null +++ b/src/tests/parser/inline/oneInline_0016.input @@ -0,0 +1 @@ +[^1] \ No newline at end of file diff --git a/src/tests/parser/inline/oneInline_0017.expected b/src/tests/parser/inline/oneInline_0017.expected new file mode 100644 index 000000000..5c46fd5dd --- /dev/null +++ b/src/tests/parser/inline/oneInline_0017.expected @@ -0,0 +1,8 @@ +Success! Final stack: + (Lean.Doc.Syntax.inline_math + "$" + (Lean.Doc.Syntax.code + "`" + (str "\"\\\\frac{x}{4}\"") + "`")) +All input consumed. \ No newline at end of file diff --git a/src/tests/parser/inline/oneInline_0017.input b/src/tests/parser/inline/oneInline_0017.input new file mode 100644 index 000000000..ce2f47e82 --- /dev/null +++ b/src/tests/parser/inline/oneInline_0017.input @@ -0,0 +1 @@ +$`\frac{x}{4}` \ No newline at end of file diff --git a/src/tests/parser/inline/oneInline_0018.expected b/src/tests/parser/inline/oneInline_0018.expected new file mode 100644 index 000000000..63cae14fc --- /dev/null +++ b/src/tests/parser/inline/oneInline_0018.expected @@ -0,0 +1,8 @@ +Success! Final stack: + (Lean.Doc.Syntax.inline_math + "$" + (Lean.Doc.Syntax.code + "`" + (str "\"\\\\frac{\\n x\\n}{\\n 4\\n}\\n\"") + "`")) +All input consumed. \ No newline at end of file diff --git a/src/tests/parser/inline/oneInline_0018.input b/src/tests/parser/inline/oneInline_0018.input new file mode 100644 index 000000000..564e267b2 --- /dev/null +++ b/src/tests/parser/inline/oneInline_0018.input @@ -0,0 +1,6 @@ +$`\frac{ + x +}{ + 4 +} +` \ No newline at end of file diff --git a/src/tests/parser/inline/oneInline_0019.expected b/src/tests/parser/inline/oneInline_0019.expected new file mode 100644 index 000000000..cc8fe55b0 --- /dev/null +++ b/src/tests/parser/inline/oneInline_0019.expected @@ -0,0 +1,8 @@ +Success! Final stack: + (Lean.Doc.Syntax.display_math + "$$" + (Lean.Doc.Syntax.code + "`" + (str "\"\\\\frac{x}{4}\"") + "`")) +All input consumed. \ No newline at end of file diff --git a/src/tests/parser/inline/oneInline_0019.input b/src/tests/parser/inline/oneInline_0019.input new file mode 100644 index 000000000..05ccf75c7 --- /dev/null +++ b/src/tests/parser/inline/oneInline_0019.input @@ -0,0 +1 @@ +$$`\frac{x}{4}` \ No newline at end of file diff --git a/src/tests/parser/inline/oneInline_0020.expected b/src/tests/parser/inline/oneInline_0020.expected new file mode 100644 index 000000000..83045d754 --- /dev/null +++ b/src/tests/parser/inline/oneInline_0020.expected @@ -0,0 +1,3 @@ +Success! Final stack: + (Lean.Doc.Syntax.text (str "\"$35.23\"")) +All input consumed. \ No newline at end of file diff --git a/src/tests/parser/inline/oneInline_0020.input b/src/tests/parser/inline/oneInline_0020.input new file mode 100644 index 000000000..ade1569bb --- /dev/null +++ b/src/tests/parser/inline/oneInline_0020.input @@ -0,0 +1 @@ +$35.23 \ No newline at end of file diff --git a/src/tests/parser/inline/oneInline_0021.expected b/src/tests/parser/inline/oneInline_0021.expected new file mode 100644 index 000000000..45d204a4a --- /dev/null +++ b/src/tests/parser/inline/oneInline_0021.expected @@ -0,0 +1,4 @@ +Success! Final stack: + (Lean.Doc.Syntax.text (str "\"$\"")) +Remaining: +"`code`" \ No newline at end of file diff --git a/src/tests/parser/inline/oneInline_0021.input b/src/tests/parser/inline/oneInline_0021.input new file mode 100644 index 000000000..a4ac79627 --- /dev/null +++ b/src/tests/parser/inline/oneInline_0021.input @@ -0,0 +1 @@ +\$`code` \ No newline at end of file diff --git a/src/tests/parser/inline/oneInline_0022.expected b/src/tests/parser/inline/oneInline_0022.expected new file mode 100644 index 000000000..f92e87787 --- /dev/null +++ b/src/tests/parser/inline/oneInline_0022.expected @@ -0,0 +1,3 @@ +Success! Final stack: + (Lean.Doc.Syntax.text (str "\"$$$\"")) +All input consumed. \ No newline at end of file diff --git a/src/tests/parser/inline/oneInline_0022.input b/src/tests/parser/inline/oneInline_0022.input new file mode 100644 index 000000000..7de3ef4a7 --- /dev/null +++ b/src/tests/parser/inline/oneInline_0022.input @@ -0,0 +1 @@ +$$$ \ No newline at end of file diff --git a/src/tests/parser/inline/role/role_0001.expected b/src/tests/parser/inline/role/role_0001.expected new file mode 100644 index 000000000..c1dba89e8 --- /dev/null +++ b/src/tests/parser/inline/role/role_0001.expected @@ -0,0 +1,13 @@ +Success! Final stack: + (Lean.Doc.Syntax.role + "{" + `hello + [] + "}" + "[" + [(Lean.Doc.Syntax.bold + "*" + [(Lean.Doc.Syntax.text (str "\"there\""))] + "*")] + "]") +All input consumed. \ No newline at end of file diff --git a/src/tests/parser/inline/role/role_0001.input b/src/tests/parser/inline/role/role_0001.input new file mode 100644 index 000000000..b5657de55 --- /dev/null +++ b/src/tests/parser/inline/role/role_0001.input @@ -0,0 +1 @@ +{hello}*there* \ No newline at end of file diff --git a/src/tests/parser/inline/role/role_0002.expected b/src/tests/parser/inline/role/role_0002.expected new file mode 100644 index 000000000..f6f692160 --- /dev/null +++ b/src/tests/parser/inline/role/role_0002.expected @@ -0,0 +1,10 @@ +Success! Final stack: + (Lean.Doc.Syntax.role + "{" + `hello + [] + "}" + "[" + [(Lean.Doc.Syntax.text (str "\"there\""))] + "]") +All input consumed. \ No newline at end of file diff --git a/src/tests/parser/inline/role/role_0002.input b/src/tests/parser/inline/role/role_0002.input new file mode 100644 index 000000000..82d9b0c5a --- /dev/null +++ b/src/tests/parser/inline/role/role_0002.input @@ -0,0 +1 @@ +{hello}[there] \ No newline at end of file diff --git a/src/tests/parser/inline/role/role_0003.expected b/src/tests/parser/inline/role/role_0003.expected new file mode 100644 index 000000000..83c54ca25 --- /dev/null +++ b/src/tests/parser/inline/role/role_0003.expected @@ -0,0 +1,22 @@ +Success! Final stack: + (Lean.Doc.Syntax.role + "{" + `ref + [(Lean.Doc.Syntax.anon + (Lean.Doc.Syntax.arg_ident `other))] + "}" + "[" + [(Lean.Doc.Syntax.role + "{" + `leanKw + [] + "}" + "[" + [(Lean.Doc.Syntax.code + "`" + (str "\"cmd\"") + "`")] + "]") + (Lean.Doc.Syntax.text (str "\" is great\""))] + "]") +All input consumed. \ No newline at end of file diff --git a/src/tests/parser/inline/role/role_0003.input b/src/tests/parser/inline/role/role_0003.input new file mode 100644 index 000000000..f9a43ff30 --- /dev/null +++ b/src/tests/parser/inline/role/role_0003.input @@ -0,0 +1 @@ +{ref other}[{leanKw}`cmd` is great] \ No newline at end of file diff --git a/src/tests/parser/inline/role/role_0004.expected b/src/tests/parser/inline/role/role_0004.expected new file mode 100644 index 000000000..759bf6389 --- /dev/null +++ b/src/tests/parser/inline/role/role_0004.expected @@ -0,0 +1,13 @@ +Success! Final stack: + (Lean.Doc.Syntax.role + "{" + `hello + [(Lean.Doc.Syntax.named_no_paren + `world + ":=" + (Lean.Doc.Syntax.arg_ident `gaia))] + "}" + "[" + [(Lean.Doc.Syntax.text (str "\"there\""))] + "]") +All input consumed. \ No newline at end of file diff --git a/src/tests/parser/inline/role/role_0004.input b/src/tests/parser/inline/role/role_0004.input new file mode 100644 index 000000000..f0aed6081 --- /dev/null +++ b/src/tests/parser/inline/role/role_0004.input @@ -0,0 +1 @@ +{hello world:=gaia}[there] \ No newline at end of file diff --git a/src/tests/parser/inline/role/role_0005.expected b/src/tests/parser/inline/role/role_0005.expected new file mode 100644 index 000000000..68f43c009 --- /dev/null +++ b/src/tests/parser/inline/role/role_0005.expected @@ -0,0 +1,24 @@ +Success! Final stack: + (Lean.Doc.Syntax.role + "{" + `hello + [(Lean.Doc.Syntax.named_no_paren + `world + ":=" + (Lean.Doc.Syntax.arg_ident `gaia))] + "}" + "[" + [(Lean.Doc.Syntax.text (str "\"there \"")) + (Lean.Doc.Syntax.bold + "*" + [(Lean.Doc.Syntax.text (str "\"is\""))] + "*") + (Lean.Doc.Syntax.text (str "\" \"")) + (Lean.Doc.Syntax.emph + "_" + [(Lean.Doc.Syntax.text + (str "\"a meaning!\""))] + "_") + (Lean.Doc.Syntax.text (str "\" \""))] + "]") +All input consumed. \ No newline at end of file diff --git a/src/tests/parser/inline/role/role_0005.input b/src/tests/parser/inline/role/role_0005.input new file mode 100644 index 000000000..f7a96975a --- /dev/null +++ b/src/tests/parser/inline/role/role_0005.input @@ -0,0 +1 @@ +{hello world:=gaia}[there *is* _a meaning!_ ] \ No newline at end of file diff --git a/src/tests/parser/inline/text/text_0001.expected b/src/tests/parser/inline/text/text_0001.expected new file mode 100644 index 000000000..d5fd8568d --- /dev/null +++ b/src/tests/parser/inline/text/text_0001.expected @@ -0,0 +1,4 @@ +Success! Final stack: + (Lean.Doc.Syntax.text (str "\" \"")) +Remaining: +"[\\[link\\]](https://link.com)" \ No newline at end of file diff --git a/src/tests/parser/inline/text/text_0001.input b/src/tests/parser/inline/text/text_0001.input new file mode 100644 index 000000000..214d3fb0c --- /dev/null +++ b/src/tests/parser/inline/text/text_0001.input @@ -0,0 +1 @@ + [\[link\]](https://link.com) \ No newline at end of file diff --git a/src/tests/parser/inlineTextChar/inlineTextChar_0001.expected b/src/tests/parser/inlineTextChar/inlineTextChar_0001.expected new file mode 100644 index 000000000..948a3a630 --- /dev/null +++ b/src/tests/parser/inlineTextChar/inlineTextChar_0001.expected @@ -0,0 +1,4 @@ +Failure @0 (⟨1, 0⟩): unexpected end of input +Final stack: + +Remaining: "" \ No newline at end of file diff --git a/src/tests/parser/inlineTextChar/inlineTextChar_0001.input b/src/tests/parser/inlineTextChar/inlineTextChar_0001.input new file mode 100644 index 000000000..e69de29bb diff --git a/src/tests/parser/inlineTextChar/inlineTextChar_0002.expected b/src/tests/parser/inlineTextChar/inlineTextChar_0002.expected new file mode 100644 index 000000000..58b7cea6a --- /dev/null +++ b/src/tests/parser/inlineTextChar/inlineTextChar_0002.expected @@ -0,0 +1,3 @@ +Success! Final stack: + empty +All input consumed. \ No newline at end of file diff --git a/src/tests/parser/inlineTextChar/inlineTextChar_0002.input b/src/tests/parser/inlineTextChar/inlineTextChar_0002.input new file mode 100644 index 000000000..2e65efe2a --- /dev/null +++ b/src/tests/parser/inlineTextChar/inlineTextChar_0002.input @@ -0,0 +1 @@ +a \ No newline at end of file diff --git a/src/tests/parser/inlineTextChar/inlineTextChar_0003.expected b/src/tests/parser/inlineTextChar/inlineTextChar_0003.expected new file mode 100644 index 000000000..c3fd7fc41 --- /dev/null +++ b/src/tests/parser/inlineTextChar/inlineTextChar_0003.expected @@ -0,0 +1,4 @@ +Success! Final stack: + empty +Remaining: +"bc" \ No newline at end of file diff --git a/src/tests/parser/inlineTextChar/inlineTextChar_0003.input b/src/tests/parser/inlineTextChar/inlineTextChar_0003.input new file mode 100644 index 000000000..f2ba8f84a --- /dev/null +++ b/src/tests/parser/inlineTextChar/inlineTextChar_0003.input @@ -0,0 +1 @@ +abc \ No newline at end of file diff --git a/src/tests/parser/inlineTextChar/inlineTextChar_0004.expected b/src/tests/parser/inlineTextChar/inlineTextChar_0004.expected new file mode 100644 index 000000000..52f3b75f4 --- /dev/null +++ b/src/tests/parser/inlineTextChar/inlineTextChar_0004.expected @@ -0,0 +1,4 @@ +Failure @0 (⟨1, 0⟩): '[' +Final stack: + +Remaining: "[abc" \ No newline at end of file diff --git a/src/tests/parser/inlineTextChar/inlineTextChar_0004.input b/src/tests/parser/inlineTextChar/inlineTextChar_0004.input new file mode 100644 index 000000000..b8d5035c1 --- /dev/null +++ b/src/tests/parser/inlineTextChar/inlineTextChar_0004.input @@ -0,0 +1 @@ +[abc \ No newline at end of file diff --git a/src/tests/parser/inlineTextChar/inlineTextChar_0005.expected b/src/tests/parser/inlineTextChar/inlineTextChar_0005.expected new file mode 100644 index 000000000..08f596a60 --- /dev/null +++ b/src/tests/parser/inlineTextChar/inlineTextChar_0005.expected @@ -0,0 +1,4 @@ +Success! Final stack: + empty +Remaining: +"abc" \ No newline at end of file diff --git a/src/tests/parser/inlineTextChar/inlineTextChar_0005.input b/src/tests/parser/inlineTextChar/inlineTextChar_0005.input new file mode 100644 index 000000000..78e3ae40b --- /dev/null +++ b/src/tests/parser/inlineTextChar/inlineTextChar_0005.input @@ -0,0 +1 @@ +!abc \ No newline at end of file diff --git a/src/tests/parser/manyInlineTextChar/manyInlineTextChar_0001.expected b/src/tests/parser/manyInlineTextChar/manyInlineTextChar_0001.expected new file mode 100644 index 000000000..141eb8787 --- /dev/null +++ b/src/tests/parser/manyInlineTextChar/manyInlineTextChar_0001.expected @@ -0,0 +1,4 @@ +Success! Final stack: + "!!" +Remaining: +"![abc" \ No newline at end of file diff --git a/src/tests/parser/manyInlineTextChar/manyInlineTextChar_0001.input b/src/tests/parser/manyInlineTextChar/manyInlineTextChar_0001.input new file mode 100644 index 000000000..baace3026 --- /dev/null +++ b/src/tests/parser/manyInlineTextChar/manyInlineTextChar_0001.input @@ -0,0 +1 @@ +!!![abc \ No newline at end of file diff --git a/src/tests/parser/manyInlineTextChar/manyInlineTextChar_0002.expected b/src/tests/parser/manyInlineTextChar/manyInlineTextChar_0002.expected new file mode 100644 index 000000000..86af371c4 --- /dev/null +++ b/src/tests/parser/manyInlineTextChar/manyInlineTextChar_0002.expected @@ -0,0 +1,4 @@ +Failure @0 (⟨1, 0⟩): '*' +Final stack: + [] +Remaining: "*" \ No newline at end of file diff --git a/src/tests/parser/manyInlineTextChar/manyInlineTextChar_0002.input b/src/tests/parser/manyInlineTextChar/manyInlineTextChar_0002.input new file mode 100644 index 000000000..f59ec20aa --- /dev/null +++ b/src/tests/parser/manyInlineTextChar/manyInlineTextChar_0002.input @@ -0,0 +1 @@ +* \ No newline at end of file diff --git a/src/tests/parser/manyInlineTextChar/manyInlineTextChar_0003.expected b/src/tests/parser/manyInlineTextChar/manyInlineTextChar_0003.expected new file mode 100644 index 000000000..69756435a --- /dev/null +++ b/src/tests/parser/manyInlineTextChar/manyInlineTextChar_0003.expected @@ -0,0 +1,4 @@ +Success! Final stack: + "!!!\\[abc" +Remaining: +"]" \ No newline at end of file diff --git a/src/tests/parser/manyInlineTextChar/manyInlineTextChar_0003.input b/src/tests/parser/manyInlineTextChar/manyInlineTextChar_0003.input new file mode 100644 index 000000000..133398899 --- /dev/null +++ b/src/tests/parser/manyInlineTextChar/manyInlineTextChar_0003.input @@ -0,0 +1 @@ +!!!\[abc] \ No newline at end of file diff --git a/src/tests/parser/metadataBlock/metadataBlock_0001.expected b/src/tests/parser/metadataBlock/metadataBlock_0001.expected new file mode 100644 index 000000000..606e773fc --- /dev/null +++ b/src/tests/parser/metadataBlock/metadataBlock_0001.expected @@ -0,0 +1,6 @@ +Success! Final stack: + (Lean.Doc.Syntax.metadata_block + "%%%" + (Term.structInstFields []) + "%%%") +All input consumed. \ No newline at end of file diff --git a/src/tests/parser/metadataBlock/metadataBlock_0001.input b/src/tests/parser/metadataBlock/metadataBlock_0001.input new file mode 100644 index 000000000..157458a32 --- /dev/null +++ b/src/tests/parser/metadataBlock/metadataBlock_0001.input @@ -0,0 +1,2 @@ +%%% +%%% \ No newline at end of file diff --git a/src/tests/parser/metadataBlock/metadataBlock_0002.expected b/src/tests/parser/metadataBlock/metadataBlock_0002.expected new file mode 100644 index 000000000..c09d89257 --- /dev/null +++ b/src/tests/parser/metadataBlock/metadataBlock_0002.expected @@ -0,0 +1,12 @@ +Success! Final stack: + (Lean.Doc.Syntax.metadata_block + "%%%" + (Term.structInstFields + [(Term.structInstField + (Term.structInstLVal `foo []) + [[] + [] + (Term.structInstFieldDef ":=" [] `bar)]) + []]) + "%%%") +All input consumed. \ No newline at end of file diff --git a/src/tests/parser/metadataBlock/metadataBlock_0002.input b/src/tests/parser/metadataBlock/metadataBlock_0002.input new file mode 100644 index 000000000..894b79e40 --- /dev/null +++ b/src/tests/parser/metadataBlock/metadataBlock_0002.input @@ -0,0 +1,4 @@ +%%% +foo := bar + +%%% \ No newline at end of file diff --git a/src/tests/parser/metadataBlock/metadataBlock_0003.expected b/src/tests/parser/metadataBlock/metadataBlock_0003.expected new file mode 100644 index 000000000..aa689840f --- /dev/null +++ b/src/tests/parser/metadataBlock/metadataBlock_0003.expected @@ -0,0 +1,16 @@ +Success! Final stack: + (Lean.Doc.Syntax.metadata_block + "%%%" + (Term.structInstFields + [(Term.structInstField + (Term.structInstLVal `foo []) + [[] + [] + (Term.structInstFieldDef ":=" [] `bar)]) + [] + (Term.structInstField + (Term.structInstLVal `x []) + []) + []]) + "%%%") +All input consumed. \ No newline at end of file diff --git a/src/tests/parser/metadataBlock/metadataBlock_0003.input b/src/tests/parser/metadataBlock/metadataBlock_0003.input new file mode 100644 index 000000000..05625731c --- /dev/null +++ b/src/tests/parser/metadataBlock/metadataBlock_0003.input @@ -0,0 +1,4 @@ +%%% +foo := bar +x +%%% \ No newline at end of file diff --git a/src/tests/parser/nameAndArgs/nameAndArgs_0001.expected b/src/tests/parser/nameAndArgs/nameAndArgs_0001.expected new file mode 100644 index 000000000..c9820cb0c --- /dev/null +++ b/src/tests/parser/nameAndArgs/nameAndArgs_0001.expected @@ -0,0 +1,8 @@ +Success! Final stack: + • `leanExample + • [(Lean.Doc.Syntax.named_no_paren + `context + ":=" + (Lean.Doc.Syntax.arg_num (num "2")))] + +All input consumed. \ No newline at end of file diff --git a/src/tests/parser/nameAndArgs/nameAndArgs_0001.input b/src/tests/parser/nameAndArgs/nameAndArgs_0001.input new file mode 100644 index 000000000..0ca118b32 --- /dev/null +++ b/src/tests/parser/nameAndArgs/nameAndArgs_0001.input @@ -0,0 +1 @@ +leanExample context := 2 \ No newline at end of file diff --git a/src/tests/parser/nameAndArgs/nameAndArgs_0002.expected b/src/tests/parser/nameAndArgs/nameAndArgs_0002.expected new file mode 100644 index 000000000..523e10673 --- /dev/null +++ b/src/tests/parser/nameAndArgs/nameAndArgs_0002.expected @@ -0,0 +1,11 @@ +Success! Final stack: + • `scheme + • [(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")))] + +All input consumed. \ No newline at end of file diff --git a/src/tests/parser/nameAndArgs/nameAndArgs_0002.input b/src/tests/parser/nameAndArgs/nameAndArgs_0002.input new file mode 100644 index 000000000..099760067 --- /dev/null +++ b/src/tests/parser/nameAndArgs/nameAndArgs_0002.input @@ -0,0 +1 @@ +scheme dialect:="chicken" 43 \ No newline at end of file diff --git a/src/tests/parser/nameAndArgs/nameAndArgs_0003.expected b/src/tests/parser/nameAndArgs/nameAndArgs_0003.expected new file mode 100644 index 000000000..bdc7273f5 --- /dev/null +++ b/src/tests/parser/nameAndArgs/nameAndArgs_0003.expected @@ -0,0 +1,12 @@ +Success! Final stack: + • `scheme + • [(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"))) + (Lean.Doc.Syntax.flag_on "+" `foo)] + +All input consumed. \ No newline at end of file diff --git a/src/tests/parser/nameAndArgs/nameAndArgs_0003.input b/src/tests/parser/nameAndArgs/nameAndArgs_0003.input new file mode 100644 index 000000000..4be9889fa --- /dev/null +++ b/src/tests/parser/nameAndArgs/nameAndArgs_0003.input @@ -0,0 +1 @@ +scheme dialect:="chicken" 43 +foo \ No newline at end of file diff --git a/src/tests/parser/nameAndArgs/nameAndArgs_0004.expected b/src/tests/parser/nameAndArgs/nameAndArgs_0004.expected new file mode 100644 index 000000000..7f6b81f2d --- /dev/null +++ b/src/tests/parser/nameAndArgs/nameAndArgs_0004.expected @@ -0,0 +1,13 @@ +Failure @29 (⟨1, 29⟩): expected flag name +Final stack: + • `scheme + • [(Lean.Doc.Syntax.named_no_paren + `dialect + ":=" + (Lean.Doc.Syntax.arg_str + (str "\"chicken\""))) + (Lean.Doc.Syntax.flag_on "+" ) + (Lean.Doc.Syntax.anon + (Lean.Doc.Syntax.arg_num (num "99")))] + +Remaining: " 99" \ No newline at end of file diff --git a/src/tests/parser/nameAndArgs/nameAndArgs_0004.input b/src/tests/parser/nameAndArgs/nameAndArgs_0004.input new file mode 100644 index 000000000..e14f14d53 --- /dev/null +++ b/src/tests/parser/nameAndArgs/nameAndArgs_0004.input @@ -0,0 +1 @@ +scheme dialect:="chicken" +43 99 \ No newline at end of file diff --git a/src/tests/parser/nameAndArgs/nameAndArgs_0005.expected b/src/tests/parser/nameAndArgs/nameAndArgs_0005.expected new file mode 100644 index 000000000..6ccf4f279 --- /dev/null +++ b/src/tests/parser/nameAndArgs/nameAndArgs_0005.expected @@ -0,0 +1,13 @@ +Failure @28 (⟨1, 28⟩): expected no space before +Final stack: + • `scheme + • [(Lean.Doc.Syntax.named_no_paren + `dialect + ":=" + (Lean.Doc.Syntax.arg_str + (str "\"chicken\""))) + (Lean.Doc.Syntax.flag_on "+" `x) + (Lean.Doc.Syntax.anon + (Lean.Doc.Syntax.arg_num (num "99")))] + +Remaining: "x 99" \ No newline at end of file diff --git a/src/tests/parser/nameAndArgs/nameAndArgs_0005.input b/src/tests/parser/nameAndArgs/nameAndArgs_0005.input new file mode 100644 index 000000000..f1f619282 --- /dev/null +++ b/src/tests/parser/nameAndArgs/nameAndArgs_0005.input @@ -0,0 +1 @@ +scheme dialect:="chicken" + x 99 \ No newline at end of file diff --git a/src/tests/parser/nameAndArgs/nameAndArgs_0006.expected b/src/tests/parser/nameAndArgs/nameAndArgs_0006.expected new file mode 100644 index 000000000..0fd9fbb32 --- /dev/null +++ b/src/tests/parser/nameAndArgs/nameAndArgs_0006.expected @@ -0,0 +1,12 @@ +Success! Final stack: + • `scheme + • [(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)" \ No newline at end of file diff --git a/src/tests/parser/nameAndArgs/nameAndArgs_0006.input b/src/tests/parser/nameAndArgs/nameAndArgs_0006.input new file mode 100644 index 000000000..47faa6abd --- /dev/null +++ b/src/tests/parser/nameAndArgs/nameAndArgs_0006.input @@ -0,0 +1,2 @@ +scheme dialect:="chicken" 43 +(foo) \ No newline at end of file diff --git a/src/tests/parser/nameAndArgs/nameAndArgs_0007.expected b/src/tests/parser/nameAndArgs/nameAndArgs_0007.expected new file mode 100644 index 000000000..5a0d8a8b3 --- /dev/null +++ b/src/tests/parser/nameAndArgs/nameAndArgs_0007.expected @@ -0,0 +1,6 @@ +Success! Final stack: + • `leanExample + • [(Lean.Doc.Syntax.anon + (Lean.Doc.Syntax.arg_ident `context))] + +All input consumed. \ No newline at end of file diff --git a/src/tests/parser/nameAndArgs/nameAndArgs_0007.input b/src/tests/parser/nameAndArgs/nameAndArgs_0007.input new file mode 100644 index 000000000..fb8c24572 --- /dev/null +++ b/src/tests/parser/nameAndArgs/nameAndArgs_0007.input @@ -0,0 +1 @@ +leanExample context \ No newline at end of file diff --git a/src/tests/parser/nameAndArgs/nameAndArgs_0008.expected b/src/tests/parser/nameAndArgs/nameAndArgs_0008.expected new file mode 100644 index 000000000..541147b6c --- /dev/null +++ b/src/tests/parser/nameAndArgs/nameAndArgs_0008.expected @@ -0,0 +1,8 @@ +Success! Final stack: + • `leanExample + • [(Lean.Doc.Syntax.anon + (Lean.Doc.Syntax.arg_ident `context)) + (Lean.Doc.Syntax.anon + (Lean.Doc.Syntax.arg_ident `more))] + +All input consumed. \ No newline at end of file diff --git a/src/tests/parser/nameAndArgs/nameAndArgs_0008.input b/src/tests/parser/nameAndArgs/nameAndArgs_0008.input new file mode 100644 index 000000000..dd713f29f --- /dev/null +++ b/src/tests/parser/nameAndArgs/nameAndArgs_0008.input @@ -0,0 +1 @@ +leanExample context more \ No newline at end of file diff --git a/src/tests/parser/nameAndArgs/nameAndArgs_0009.expected b/src/tests/parser/nameAndArgs/nameAndArgs_0009.expected new file mode 100644 index 000000000..9369dc2c4 --- /dev/null +++ b/src/tests/parser/nameAndArgs/nameAndArgs_0009.expected @@ -0,0 +1,11 @@ +Success! Final stack: + • `leanExample + • [(Lean.Doc.Syntax.anon + (Lean.Doc.Syntax.arg_ident `context)) + (Lean.Doc.Syntax.named_no_paren + `more + ":=" + (Lean.Doc.Syntax.arg_str + (str "\"stuff\"")))] + +All input consumed. \ No newline at end of file diff --git a/src/tests/parser/nameAndArgs/nameAndArgs_0009.input b/src/tests/parser/nameAndArgs/nameAndArgs_0009.input new file mode 100644 index 000000000..1ddaeb97b --- /dev/null +++ b/src/tests/parser/nameAndArgs/nameAndArgs_0009.input @@ -0,0 +1 @@ +leanExample context more:="stuff" \ No newline at end of file diff --git a/src/tests/parser/nameAndArgs/nameAndArgs_0010.expected b/src/tests/parser/nameAndArgs/nameAndArgs_0010.expected new file mode 100644 index 000000000..6b2cf8786 --- /dev/null +++ b/src/tests/parser/nameAndArgs/nameAndArgs_0010.expected @@ -0,0 +1,12 @@ +Success! Final stack: + • `leanExample + • [(Lean.Doc.Syntax.anon + (Lean.Doc.Syntax.arg_ident `context)) + (Lean.Doc.Syntax.named_no_paren + `more + ":=" + (Lean.Doc.Syntax.arg_str + (str "\"stuff\"")))] + +Remaining: +"\n\nabc" \ No newline at end of file diff --git a/src/tests/parser/nameAndArgs/nameAndArgs_0010.input b/src/tests/parser/nameAndArgs/nameAndArgs_0010.input new file mode 100644 index 000000000..b455b56ac --- /dev/null +++ b/src/tests/parser/nameAndArgs/nameAndArgs_0010.input @@ -0,0 +1,3 @@ +leanExample context more:="stuff" + +abc \ No newline at end of file diff --git a/src/tests/parser/val/arg_val_0001.expected b/src/tests/parser/val/arg_val_0001.expected new file mode 100644 index 000000000..a07cba777 --- /dev/null +++ b/src/tests/parser/val/arg_val_0001.expected @@ -0,0 +1,3 @@ +Success! Final stack: + (Lean.Doc.Syntax.arg_num (num "1")) +All input consumed. \ No newline at end of file diff --git a/src/tests/parser/val/arg_val_0001.input b/src/tests/parser/val/arg_val_0001.input new file mode 100644 index 000000000..56a6051ca --- /dev/null +++ b/src/tests/parser/val/arg_val_0001.input @@ -0,0 +1 @@ +1 \ No newline at end of file diff --git a/src/tests/parser/val/arg_val_0002.expected b/src/tests/parser/val/arg_val_0002.expected new file mode 100644 index 000000000..bb0af9adc --- /dev/null +++ b/src/tests/parser/val/arg_val_0002.expected @@ -0,0 +1,3 @@ +Success! Final stack: + (Lean.Doc.Syntax.arg_num (num "3")) +All input consumed. \ No newline at end of file diff --git a/src/tests/parser/val/arg_val_0002.input b/src/tests/parser/val/arg_val_0002.input new file mode 100644 index 000000000..e440e5c84 --- /dev/null +++ b/src/tests/parser/val/arg_val_0002.input @@ -0,0 +1 @@ +3 \ No newline at end of file diff --git a/src/tests/parser/val/arg_val_0003.expected b/src/tests/parser/val/arg_val_0003.expected new file mode 100644 index 000000000..b8a9299d1 --- /dev/null +++ b/src/tests/parser/val/arg_val_0003.expected @@ -0,0 +1,4 @@ +Failure @0 (⟨1, 0⟩): unexpected end of input; expected identifier, numeral or string literal +Final stack: + (Lean.Doc.Syntax.arg_str ) +Remaining: "" \ No newline at end of file diff --git a/src/tests/parser/val/arg_val_0003.input b/src/tests/parser/val/arg_val_0003.input new file mode 100644 index 000000000..e69de29bb diff --git a/src/tests/parser/val/arg_val_0004.expected b/src/tests/parser/val/arg_val_0004.expected new file mode 100644 index 000000000..3473ba6e3 --- /dev/null +++ b/src/tests/parser/val/arg_val_0004.expected @@ -0,0 +1,3 @@ +Success! Final stack: + (Lean.Doc.Syntax.arg_str (str "\"a b c\t d\"")) +All input consumed. \ No newline at end of file diff --git a/src/tests/parser/val/arg_val_0004.input b/src/tests/parser/val/arg_val_0004.input new file mode 100644 index 000000000..101b1a715 --- /dev/null +++ b/src/tests/parser/val/arg_val_0004.input @@ -0,0 +1 @@ +"a b c d" \ No newline at end of file diff --git a/src/tests/parser/val/arg_val_0005.expected b/src/tests/parser/val/arg_val_0005.expected new file mode 100644 index 000000000..05c15691c --- /dev/null +++ b/src/tests/parser/val/arg_val_0005.expected @@ -0,0 +1,4 @@ +Success! Final stack: + (Lean.Doc.Syntax.arg_str (str "\"a b c\t d\"")) +Remaining: +"\n" \ No newline at end of file diff --git a/src/tests/parser/val/arg_val_0005.input b/src/tests/parser/val/arg_val_0005.input new file mode 100644 index 000000000..54fb7822c --- /dev/null +++ b/src/tests/parser/val/arg_val_0005.input @@ -0,0 +1 @@ +"a b c d" diff --git a/src/tests/parser/val/arg_val_0006.expected b/src/tests/parser/val/arg_val_0006.expected new file mode 100644 index 000000000..37d5f420a --- /dev/null +++ b/src/tests/parser/val/arg_val_0006.expected @@ -0,0 +1,4 @@ +Success! Final stack: + (Lean.Doc.Syntax.arg_num (num "43")) +Remaining: +"\n\"foo\"" \ No newline at end of file diff --git a/src/tests/parser/val/arg_val_0006.input b/src/tests/parser/val/arg_val_0006.input new file mode 100644 index 000000000..4c37dc640 --- /dev/null +++ b/src/tests/parser/val/arg_val_0006.input @@ -0,0 +1,2 @@ +43 +"foo" \ No newline at end of file diff --git a/src/tests/parser/val/arg_val_0007.expected b/src/tests/parser/val/arg_val_0007.expected new file mode 100644 index 000000000..8377e2396 --- /dev/null +++ b/src/tests/parser/val/arg_val_0007.expected @@ -0,0 +1,4 @@ +Failure @0 (⟨1, 0⟩): unterminated string literal; expected identifier or numeral +Final stack: + (Lean.Doc.Syntax.arg_str ) +Remaining: "\"foo" \ No newline at end of file diff --git a/src/tests/parser/val/arg_val_0007.input b/src/tests/parser/val/arg_val_0007.input new file mode 100644 index 000000000..d45772e3c --- /dev/null +++ b/src/tests/parser/val/arg_val_0007.input @@ -0,0 +1 @@ +"foo \ No newline at end of file