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

test(tests/playground/termparsertest1): new tests

Browse source
This commit is contained in:
Leonardo de Moura 2019-07-05 12:10:22 -07:00
parent 68d29fcdd4
commit f1fe5c8d8b
1 changed files with 37 additions and 25 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

62
tests/playground/termparsertest1.lean
View file

@ -9,30 +9,42 @@ termPTables ← builtinTermParsingTable.get;
stx ← IO.ofExcept $ runParser env termPTables input "<input>" "expr";
IO.println stx
def test (is : List String) : IO Unit :=
is.mfor $ fun input => do
IO.println input;
testParser input
def main (xs : List String) : IO Unit :=
do
testParser "Prod.mk";
testParser "x.{u, v+1}";
testParser "x.{u}";
testParser "x";
testParser "x.{max u v}";
testParser "x.{max u v, 0}";
testParser "f 0 1";
testParser "f.{u+1} \"foo\" x";
testParser "(f x, 0, 1)";
testParser "()";
testParser "(f x)";
testParser "(f x : Type)";
testParser "h (f x) (g y)";
testParser "if x then f x else g x";
testParser "if h : x then f x h else g x h";
testParser "have p x y from f x; g this";
testParser "suffices h : p x y from f x; g this";
testParser "show p x y from f x";
testParser "fun x y => f y x";
testParser "fun (x y : Nat) => f y x";
testParser "fun (x, y) => f y x";
testParser "fun z (x, y) => f y x";
testParser "fun ⟨x, y⟩ ⟨z, w⟩ => f y x w z";
testParser "fun (Prod.mk x y) => f y x";
pure ()
test [
"Prod.mk",
"x.{u, v+1}",
"x.{u}",
"x",
"x.{max u v}",
"x.{max u v, 0}",
"f 0 1",
"f.{u+1} \"foo\" x",
"(f x, 0, 1)",
"()",
"(f x)",
"(f x : Type)",
"h (f x) (g y)",
"if x then f x else g x",
"if h : x then f x h else g x h",
"have p x y from f x; g this",
"suffices h : p x y from f x; g this",
"show p x y from f x",
"fun x y => f y x",
"fun (x y : Nat) => f y x",
"fun (x, y) => f y x",
"fun z (x, y) => f y x",
"fun ⟨x, y⟩ ⟨z, w⟩ => f y x w z",
"fun (Prod.mk x y) => f y x",
"{ x := 10, y := 20 }",
"{ x := 10, y := 20, }",
"{ x // p x 10 }",
"{ x : Nat // p x 10 }",
"{ .. }",
"{ Prod . fst := 10, .. }"
]