40 lines
1 KiB
Text
40 lines
1 KiB
Text
import init.lean.parser.parser
|
|
open Lean
|
|
open Lean.Parser
|
|
|
|
namespace Foo
|
|
|
|
@[builtinTestParser] def pairParser :=
|
|
parser! "(" >> numLit >> "," >> ident >> ")"
|
|
|
|
@[builtinTestParser] def pairsParser :=
|
|
parser! "{" >> sepBy1 testParser "," >> "}"
|
|
|
|
@[builtinTestParser] def functionParser :=
|
|
parser! "fun" >> ident >> "," >> testParser
|
|
|
|
@[builtinTestParser] def identParser : Parser :=
|
|
ident
|
|
|
|
@[builtinTestParser] def numParser : Parser :=
|
|
numLit
|
|
|
|
@[builtinTestParser] def strParser : Parser :=
|
|
strLit
|
|
|
|
end Foo
|
|
|
|
def testParser (input : String) : IO Unit :=
|
|
do
|
|
env ← mkEmptyEnvironment;
|
|
testPTables ← builtinTestParsingTable.get;
|
|
stx ← IO.ofExcept $ runParser env testPTables input;
|
|
IO.println stx
|
|
|
|
def main (xs : List String) : IO Unit :=
|
|
do
|
|
testParser "(10, hello)";
|
|
testParser "{ hello, 400, \"hello\", (10, hello), /- comment -/ (20, world), { fun x, (10, hello) }, { (30, foo) } }";
|
|
-- Following example has syntax error
|
|
testParser
|
|
"{ hello, 400, \"hello\", (10, hello), /- comment -/ (20, world), { fun x, [ (10, hello) }, { (30, foo) } }"
|