michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

test(lean/scanner): add more tests for improving coverage

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-09-27 08:56:20 -07:00
parent 6fc177056e
commit 0ff69d28f3
1 changed files with 25 additions and 18 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

43
src/tests/frontends/lean/scanner.cpp
View file

@ -33,6 +33,15 @@ static void scan(char const * str, list<name> const & cmds = list<name>()) {
std::cout << "\n";
}
static void scan_error(char const * str) {
try {
scan(str);
lean_unreachable();
} catch (exception & ex) {
std::cout << "expected error: " << ex.what() << "\n";
}
}
static void check(char const * str, std::initializer_list<scanner::token> const & l, list<name> const & cmds = list<name>()) {
auto it = l.begin();
std::istringstream in(str);
@ -61,12 +70,7 @@ static void check_name(char const * str, name const & expected) {
static void tst1() {
scan("fun(x: Pi A : Type, A -> A), (* (* test *) *) x+1 = 2.0 λ");
try {
scan("(* (* foo *)");
lean_unreachable();
} catch (exception const & ex) {
std::cout << "expected error: " << ex.what() << "\n";
}
scan_error("(* (* foo *)");
}
static void tst2() {
@ -93,27 +97,30 @@ static void tst2() {
check_name("x::10::bla::0", name(name(name(name("x"), 10), "bla"), 0u));
check("0::1", {st::NatVal, st::Colon, st::Colon, st::NatVal});
check_name("\u2296\u2296", name("\u2296\u2296"));
try {
scan("x::1000000000000000000");
lean_unreachable();
} catch (exception const & ex) {
std::cout << "expected error: " << ex.what() << "\n";
}
scan_error("x::1000000000000000000");
scan("Theorem a : Bool Axiom b : Int", list<name>({"Theorem", "Axiom"}));
check("Theorem a : Bool Axiom b : Int", {st::CommandId, st::Id, st::Colon, st::Id, st::CommandId, st::Id, st::Colon, st::Id}, list<name>({"Theorem", "Axiom"}));
scan("foo \"tst\\\"\" : Int");
check("foo \"tst\\\"\" : Int", {st::Id, st::StringVal, st::Colon, st::Id});
try {
scan("\"foo");
lean_unreachable();
} catch (exception const & ex) {
std::cout << "expected error: " << ex.what() << "\n";
}
scan_error("\"foo");
scan("2.13 1.2 0.5");
}
static void tst3() {
scan_error("\"\\");
scan_error("\"\\a");
scan("\"\naaa\"");
scan_error("foo::0a::1");
scan("10.0.");
scan("{ } . forall exists let in \u2200 \u2203 := _");
std::ostringstream out;
out << scanner::token::Eof;
lean_assert_eq(out.str(), "EOF");
}
int main() {
tst1();
tst2();
tst3();
return has_violations() ? 1 : 0;
}