From d75a9c840ca521f4f25f1ba25d42057148f8e240 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 13 Oct 2014 21:08:36 -0700
Subject: [PATCH] fix(frontends/lean/parser): segfault when ending scope
 without opening, fixes #244

---
 src/frontends/lean/local_decls.h     | 1 +
 src/frontends/lean/parser.cpp        | 3 +++
 tests/lean/bad_end.lean              | 1 +
 tests/lean/bad_end.lean.expected.out | 1 +
 4 files changed, 6 insertions(+)
 create mode 100644 tests/lean/bad_end.lean
 create mode 100644 tests/lean/bad_end.lean.expected.out

diff --git a/src/frontends/lean/local_decls.h b/src/frontends/lean/local_decls.h
index a996469b4..336d62abb 100644
--- a/src/frontends/lean/local_decls.h
+++ b/src/frontends/lean/local_decls.h
@@ -46,6 +46,7 @@ public:
         std::tie(m_map, m_counter, m_entries) = head(m_scopes);
         m_scopes  = tail(m_scopes);
     }
+    bool has_scopes() const { return !is_nil(m_scopes); }
     bool empty() const { return m_map.empty(); }
     struct mk_scope {
         local_decls & m_d;
diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp
index eb90b9a77..9716531a0 100644
--- a/src/frontends/lean/parser.cpp
+++ b/src/frontends/lean/parser.cpp
@@ -417,6 +417,9 @@ void parser::push_local_scope(bool save_options) {
 }
 
 void parser::pop_local_scope() {
+    if (!m_local_level_decls.has_scopes()) {
+        throw parser_error("invalid 'end', there is no open namespace/section/context", pos());
+    }
     m_local_level_decls.pop();
     m_local_decls.pop();
     lean_assert(!is_nil(m_parser_scope_stack));
diff --git a/tests/lean/bad_end.lean b/tests/lean/bad_end.lean
new file mode 100644
index 000000000..afdac78d1
--- /dev/null
+++ b/tests/lean/bad_end.lean
@@ -0,0 +1 @@
+end foo
diff --git a/tests/lean/bad_end.lean.expected.out b/tests/lean/bad_end.lean.expected.out
new file mode 100644
index 000000000..66ed1a0d4
--- /dev/null
+++ b/tests/lean/bad_end.lean.expected.out
@@ -0,0 +1 @@
+bad_end.lean:1:4: error: invalid 'end', there is no open namespace/section/context