test(tests/playground/parser): multiple targets
This commit is contained in:
Leonardo de Moura
parent
dd72df26bd
commit
f25554baa7
4 changed files with 110 additions and 105 deletions
|
|
@ -1,15 +1,16 @@
|
|||
LEANC=../../../bin/leanc
|
||||
LEAN=../../../bin/lean
|
||||
SRCS = $(shell ls *.lean)
|
||||
COMMON_SRCS = parser.lean
|
||||
SRCS = $(COMMON_SRCS) test1.lean test2.lean
|
||||
OLEANS = $(SRCS:.lean=.olean)
|
||||
CPPS = $(SRCS:.lean=.cpp)
|
||||
OBJS = $(SRCS:.lean=.o)
|
||||
COMMON_OBJS = $(COMMON_SRCS:.lean=.o)
|
||||
DEPS = $(SRCS:.lean=.depend)
|
||||
CPPFLAGS = -O3
|
||||
|
||||
.PHONY: all clean
|
||||
|
||||
all: parser $(OLEANS)
|
||||
all: test1 test2 $(OLEANS)
|
||||
|
||||
depends: $(DEPS)
|
||||
|
||||
|
|
@ -27,14 +28,17 @@ depends: $(DEPS)
|
|||
%.o: %.cpp
|
||||
$(LEANC) -c $(CPPFLAGS) -o $@ $<
|
||||
|
||||
parser: $(OBJS)
|
||||
$(LEANC) -o parser $(OBJS)
|
||||
test1: test1.o $(COMMON_OBJS)
|
||||
$(LEANC) -o $@ $?
|
||||
|
||||
test2: test2.o $(COMMON_OBJS)
|
||||
$(LEANC) -o $@ $?
|
||||
|
||||
clean:
|
||||
rm -f *.olean
|
||||
rm -f *.cpp
|
||||
rm -f *.o
|
||||
rm -f *.depend
|
||||
rm -f parser
|
||||
rm -f test1 test2
|
||||
|
||||
include $(DEPS)
|
||||
|
|
|
|||
|
|
@ -335,102 +335,3 @@ end
|
|||
|
||||
end Parser
|
||||
end Lean
|
||||
|
||||
abbrev Parser (α : Type) := ReaderT Nat (Lean.Parser.ParserM Unit Unit Unit) α
|
||||
|
||||
open Lean.Parser
|
||||
|
||||
-- setOption pp.implicit True
|
||||
-- setOption Trace.Compiler.boxed True
|
||||
|
||||
def testP : Parser Unit :=
|
||||
many1 (str "++" <|> str "**" <|> (str "--" *> takeUntil (= '\n') *> any *> pure ()))
|
||||
|
||||
def testP2 : Parser Unit :=
|
||||
many1 ((strLit *> whitespace *> pure ()) <|> (str "--" *> takeUntil (= '\n') *> any *> pure ()))
|
||||
|
||||
def testP3 : Parser Unit :=
|
||||
leanWhitespace
|
||||
|
||||
def testParser (x : Parser Unit) (input : String) : String :=
|
||||
match (x 0).run () () input with
|
||||
| Lean.Parser.Result.ok _ i _ _ := "Ok at " ++ toString i
|
||||
| Result.error msg i _ _ := "Error at " ++ toString i ++ ": " ++ msg
|
||||
|
||||
def IO.testParser {α : Type} [HasToString α] (x : Parser α) (input : String) : IO Unit :=
|
||||
match (x 0).run () () input with
|
||||
| Lean.Parser.Result.ok a _ _ _ := IO.println ("Ok " ++ toString a)
|
||||
| _ := throw "ERROR"
|
||||
|
||||
@[noinline] def test (p : Parser Unit) (s : String) : IO Unit :=
|
||||
IO.println (testParser p s)
|
||||
|
||||
def mkBigString : Nat → String → String
|
||||
| 0 s := s
|
||||
| (n+1) s := mkBigString n (s ++ "-- new comment\n")
|
||||
|
||||
def mkBigString2 : Nat → String → String
|
||||
| 0 s := s
|
||||
| (n+1) s := mkBigString2 n (s ++ "\"hello\\nworld\"\n-- comment\n")
|
||||
|
||||
def mkBigString3 : Nat → String → String
|
||||
| 0 s := s
|
||||
| (n+1) s := mkBigString3 n (s ++ "/- /- comment 1 -/ -/ \n -- comment 2 \n \t \n ")
|
||||
|
||||
def prof {α : Type} (msg : String) (p : IO α) : IO α :=
|
||||
let msg₁ := "Time for '" ++ msg ++ "':" in
|
||||
let msg₂ := "Memory usage for '" ++ msg ++ "':" in
|
||||
allocprof msg₂ (timeit msg₁ p)
|
||||
|
||||
def tst1 : IO Unit :=
|
||||
IO.testParser strLit "\"hello\n\""
|
||||
|
||||
def check {α} [HasBeq α] (p : Parser α) (s : String) (e : α) : IO Unit :=
|
||||
match (p 0).run () () s with
|
||||
| Lean.Parser.Result.ok v i _ _ := do
|
||||
IO.println ("Ok at " ++ toString i),
|
||||
unless (v == e) (throw "unexpected result")
|
||||
| Result.error msg _ _ _ := throw msg
|
||||
|
||||
def checkFailure {α} (p : Parser α) (s : String) : IO Unit :=
|
||||
match (p 0).run () () s with
|
||||
| Lean.Parser.Result.ok _ i _ _ := throw "Worked"
|
||||
| Result.error msg i _ _ := IO.println ("failed as expected at " ++ toString i ++ ", error: " ++ toString msg)
|
||||
|
||||
def str' (s : String) : Parser String :=
|
||||
str s *> pure s
|
||||
|
||||
def tst2 : IO Unit :=
|
||||
do check (ch 'a') "a" 'a',
|
||||
check any "a" 'a',
|
||||
check any "b" 'b',
|
||||
check (str' "foo" <|> str' "bla" <|> str' "boo") "bla" "bla",
|
||||
check (try (str' "foo" *> str' "foo") <|> str' "foo2" <|> str' "boo") "foo2" "foo2",
|
||||
checkFailure ((str' "foo" *> str' "abc") <|> str' "foo2" <|> str' "boo") "foo2",
|
||||
check (str' "foofoo" <|> str' "foo2" <|> str' "boo") "foo2" "foo2",
|
||||
check (leanWhitespace *> str' "hello") " \n-- comment\nhello" "hello",
|
||||
check (takeUntil (== '\n') *> ch '\n' *> str' "test") "\ntest" "test",
|
||||
check (takeUntil (== 't') *> str' "test") "test" "test",
|
||||
check (takeUntil (== '\n') *> ch '\n' *> str' "test") "abc\ntest" "test",
|
||||
check (try (ch 'a' *> ch 'b') <|> (ch 'a' *> ch 'c')) "ac" 'c',
|
||||
checkFailure ((ch 'a' *> ch 'b') <|> (ch 'a' *> ch 'c')) "ac",
|
||||
check (lookahead (ch 'a')) "abc" 'a',
|
||||
check (lookahead (ch 'a') *> str' "abc") "abc" "abc",
|
||||
check strLit "\"abc\\nd\"" "abc\nd",
|
||||
checkFailure strLit "abc\\nd\"",
|
||||
checkFailure strLit "\"abc",
|
||||
checkFailure strLit "\"abc\\ab̈\""
|
||||
|
||||
|
||||
def main (xs : List String) : IO Unit :=
|
||||
do
|
||||
tst1, tst2,
|
||||
let s₁ := mkBigString xs.head.toNat "",
|
||||
let s₂ := s₁ ++ "bad" ++ mkBigString 20 "",
|
||||
let s₃ := mkBigString2 xs.head.toNat "",
|
||||
let s₄ := mkBigString3 xs.head.toNat "",
|
||||
IO.println s₄.length,
|
||||
prof "Parser 1" (test testP s₁),
|
||||
prof "Parser 2" (test testP s₂),
|
||||
prof "Parser 3" (test testP2 s₃),
|
||||
prof "Parser 4" (test testP3 s₄)
|
||||
|
|
|
|||
59
tests/playground/parser/test1.lean
Normal file
59
tests/playground/parser/test1.lean
Normal file
|
|
@ -0,0 +1,59 @@
|
|||
import parser
|
||||
|
||||
abbrev Parser (α : Type) := ReaderT Nat (Lean.Parser.ParserM Unit Unit Unit) α
|
||||
|
||||
open Lean.Parser
|
||||
|
||||
-- setOption pp.implicit True
|
||||
-- setOption Trace.Compiler.boxed True
|
||||
|
||||
def testP : Parser Unit :=
|
||||
many1 (str "++" <|> str "**" <|> (str "--" *> takeUntil (= '\n') *> any *> pure ()))
|
||||
|
||||
def testP2 : Parser Unit :=
|
||||
many1 ((strLit *> whitespace *> pure ()) <|> (str "--" *> takeUntil (= '\n') *> any *> pure ()))
|
||||
|
||||
def testP3 : Parser Unit :=
|
||||
leanWhitespace
|
||||
|
||||
def testParser (x : Parser Unit) (input : String) : String :=
|
||||
match (x 0).run () () input with
|
||||
| Lean.Parser.Result.ok _ i _ _ := "Ok at " ++ toString i
|
||||
| Result.error msg i _ _ := "Error at " ++ toString i ++ ": " ++ msg
|
||||
|
||||
def IO.testParser {α : Type} [HasToString α] (x : Parser α) (input : String) : IO Unit :=
|
||||
match (x 0).run () () input with
|
||||
| Lean.Parser.Result.ok a _ _ _ := IO.println ("Ok " ++ toString a)
|
||||
| _ := throw "ERROR"
|
||||
|
||||
@[noinline] def test (p : Parser Unit) (s : String) : IO Unit :=
|
||||
IO.println (testParser p s)
|
||||
|
||||
def mkBigString : Nat → String → String
|
||||
| 0 s := s
|
||||
| (n+1) s := mkBigString n (s ++ "-- new comment\n")
|
||||
|
||||
def mkBigString2 : Nat → String → String
|
||||
| 0 s := s
|
||||
| (n+1) s := mkBigString2 n (s ++ "\"hello\\nworld\"\n-- comment\n")
|
||||
|
||||
def mkBigString3 : Nat → String → String
|
||||
| 0 s := s
|
||||
| (n+1) s := mkBigString3 n (s ++ "/- /- comment 1 -/ -/ \n -- comment 2 \n \t \n ")
|
||||
|
||||
def prof {α : Type} (msg : String) (p : IO α) : IO α :=
|
||||
let msg₁ := "Time for '" ++ msg ++ "':" in
|
||||
let msg₂ := "Memory usage for '" ++ msg ++ "':" in
|
||||
allocprof msg₂ (timeit msg₁ p)
|
||||
|
||||
def main (xs : List String) : IO Unit :=
|
||||
do
|
||||
let s₁ := mkBigString xs.head.toNat "",
|
||||
let s₂ := s₁ ++ "bad" ++ mkBigString 20 "",
|
||||
let s₃ := mkBigString2 xs.head.toNat "",
|
||||
let s₄ := mkBigString3 xs.head.toNat "",
|
||||
IO.println s₄.length,
|
||||
prof "Parser 1" (test testP s₁),
|
||||
prof "Parser 2" (test testP s₂),
|
||||
prof "Parser 3" (test testP2 s₃),
|
||||
prof "Parser 4" (test testP3 s₄)
|
||||
41
tests/playground/parser/test2.lean
Normal file
41
tests/playground/parser/test2.lean
Normal file
|
|
@ -0,0 +1,41 @@
|
|||
import parser
|
||||
|
||||
abbrev Parser (α : Type) := Lean.Parser.ParserM Unit Unit Unit α
|
||||
|
||||
open Lean.Parser
|
||||
|
||||
def check {α} [HasBeq α] (p : Parser α) (s : String) (e : α) : IO Unit :=
|
||||
match p.run () () s with
|
||||
| Lean.Parser.Result.ok v i _ _ := do
|
||||
IO.println ("Ok at " ++ toString i),
|
||||
unless (v == e) (throw "unexpected result")
|
||||
| Result.error msg _ _ _ := throw msg
|
||||
|
||||
def checkFailure {α} (p : Parser α) (s : String) : IO Unit :=
|
||||
match p.run () () s with
|
||||
| Lean.Parser.Result.ok _ i _ _ := throw "Worked"
|
||||
| Result.error msg i _ _ := IO.println ("failed as expected at " ++ toString i ++ ", error: " ++ toString msg)
|
||||
|
||||
def str' (s : String) : Parser String :=
|
||||
str s *> pure s
|
||||
|
||||
def main : IO Unit :=
|
||||
do check (ch 'a') "a" 'a',
|
||||
check any "a" 'a',
|
||||
check any "b" 'b',
|
||||
check (str' "foo" <|> str' "bla" <|> str' "boo") "bla" "bla",
|
||||
check (try (str' "foo" *> str' "foo") <|> str' "foo2" <|> str' "boo") "foo2" "foo2",
|
||||
checkFailure ((str' "foo" *> str' "abc") <|> str' "foo2" <|> str' "boo") "foo2",
|
||||
check (str' "foofoo" <|> str' "foo2" <|> str' "boo") "foo2" "foo2",
|
||||
check (leanWhitespace *> str' "hello") " \n-- comment\nhello" "hello",
|
||||
check (takeUntil (== '\n') *> ch '\n' *> str' "test") "\ntest" "test",
|
||||
check (takeUntil (== 't') *> str' "test") "test" "test",
|
||||
check (takeUntil (== '\n') *> ch '\n' *> str' "test") "abc\ntest" "test",
|
||||
check (try (ch 'a' *> ch 'b') <|> (ch 'a' *> ch 'c')) "ac" 'c',
|
||||
checkFailure ((ch 'a' *> ch 'b') <|> (ch 'a' *> ch 'c')) "ac",
|
||||
check (lookahead (ch 'a')) "abc" 'a',
|
||||
check (lookahead (ch 'a') *> str' "abc") "abc" "abc",
|
||||
check strLit "\"abc\\nd\"" "abc\nd",
|
||||
checkFailure strLit "abc\\nd\"",
|
||||
checkFailure strLit "\"abc",
|
||||
checkFailure strLit "\"abc\\ab̈\""
|
||||
Loading…
Add table
Reference in a new issue