From 5991337279325925834ffa951d0c49e06610cf6f Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 24 Apr 2019 11:19:52 -0700 Subject: [PATCH] test(tests/playground/parser/test1): add test and `timeit` --- tests/playground/parser/test1.lean | 12 ++++++++++-- 1 file changed, 10 insertions(+), 2 deletions(-) diff --git a/tests/playground/parser/test1.lean b/tests/playground/parser/test1.lean index 0308b1e18b..e8448cdbb6 100644 --- a/tests/playground/parser/test1.lean +++ b/tests/playground/parser/test1.lean @@ -54,10 +54,13 @@ node setCompKind $ def testParser2 : TermParser := many (longestMatch [qualifiedP, parenIdentP, seqP, setCompP]) +def testParser3 : TermParser := +many (longestMatch [qualifiedP, seqP]) + @[noinline] def test (p : TermParser) (s : String) : IO Unit := match p.test s with | Except.error msg := IO.println msg -| Except.ok stx := IO.println stx -- IO.println "ok" +| Except.ok stx := IO.println "ok" -- IO.println stx -- IO.println "ok" def mkTestString1 : Nat → String → String | 0 s := s @@ -81,5 +84,10 @@ def test2 (n : Nat) : IO Unit := let s := mkTestString2 n "" in test testParser2 s +def test3 (n : Nat) : IO Unit := +let s := mkTestString2 n "" in +test testParser3 s + def main (xs : List String) : IO Unit := -test2 xs.head.toNat +timeit "test2" (test2 xs.head.toNat) *> +timeit "test3" (test3 xs.head.toNat)