From f25554baa7f4a78e98017a02ea0980559ea291fe Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 4 Apr 2019 10:50:34 -0700 Subject: [PATCH] test(tests/playground/parser): multiple targets --- tests/playground/parser/Makefile | 16 +++-- tests/playground/parser/parser.lean | 99 ----------------------------- tests/playground/parser/test1.lean | 59 +++++++++++++++++ tests/playground/parser/test2.lean | 41 ++++++++++++ 4 files changed, 110 insertions(+), 105 deletions(-) create mode 100644 tests/playground/parser/test1.lean create mode 100644 tests/playground/parser/test2.lean diff --git a/tests/playground/parser/Makefile b/tests/playground/parser/Makefile index 4f983861f7..fc9300683c 100644 --- a/tests/playground/parser/Makefile +++ b/tests/playground/parser/Makefile @@ -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) diff --git a/tests/playground/parser/parser.lean b/tests/playground/parser/parser.lean index 00542154a2..a459754b2b 100644 --- a/tests/playground/parser/parser.lean +++ b/tests/playground/parser/parser.lean @@ -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₄) diff --git a/tests/playground/parser/test1.lean b/tests/playground/parser/test1.lean new file mode 100644 index 0000000000..e2a866a44f --- /dev/null +++ b/tests/playground/parser/test1.lean @@ -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₄) diff --git a/tests/playground/parser/test2.lean b/tests/playground/parser/test2.lean new file mode 100644 index 0000000000..c9d2aacfc5 --- /dev/null +++ b/tests/playground/parser/test2.lean @@ -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̈\""