From 0ff69d28f32cd77b6582175a78e0704f1fd74fe7 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 27 Sep 2013 08:56:20 -0700
Subject: [PATCH] test(lean/scanner): add more tests for improving coverage

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/tests/frontends/lean/scanner.cpp | 43 ++++++++++++++++------------
 1 file changed, 25 insertions(+), 18 deletions(-)

diff --git a/src/tests/frontends/lean/scanner.cpp b/src/tests/frontends/lean/scanner.cpp
index 5f8b0adb2..d293f3259 100644
--- a/src/tests/frontends/lean/scanner.cpp
+++ b/src/tests/frontends/lean/scanner.cpp
@@ -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;
 }