max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

test(tests/playground/parser/test1): add test and timeit

Browse source
This commit is contained in:
Leonardo de Moura 2019-04-24 11:19:52 -07:00
parent 5188adc685
commit 5991337279
1 changed files with 10 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

12
tests/playground/parser/test1.lean
View file

@ -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)