From 70c0eda9fcce9a3854444d92f1f76a77c189f20a Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 7 Aug 2014 17:08:59 -0700
Subject: [PATCH] feat(frontends/lean): make sure all scopes are closed in the
 end of the module

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/frontends/lean/parser.cpp | 7 +++++++
 src/library/scoped_ext.cpp    | 5 +++++
 src/library/scoped_ext.h      | 1 +
 tests/lean/crash.lean         | 1 +
 tests/lean/run/cody1.lean     | 1 +
 tests/lean/run/cody2.lean     | 4 +++-
 tests/lean/run/elab_bug1.lean | 1 +
 tests/lean/run/univ_bug2.lean | 2 ++
 8 files changed, 21 insertions(+), 1 deletion(-)

diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp
index 45984bb6ba..01367857ac 100644
--- a/src/frontends/lean/parser.cpp
+++ b/src/frontends/lean/parser.cpp
@@ -1183,6 +1183,13 @@ bool parser::parse_commands() {
                 },
                 [&]() { sync_command(); });
         }
+        if (has_open_scopes(m_env)) {
+            m_found_errors = true;
+            if (!m_use_exceptions && m_show_errors)
+                display_error("invalid end of module, expecting 'end'", pos());
+            else if (m_use_exceptions)
+                throw_parser_exception("invalid end of module, expecting 'end'", pos());
+        }
     } catch (interrupt_parser) {}
     for (certified_declaration const & thm : m_theorem_queue.join()) {
         m_env.replace(thm);
diff --git a/src/library/scoped_ext.cpp b/src/library/scoped_ext.cpp
index c0f156b65d..19363dc0ba 100644
--- a/src/library/scoped_ext.cpp
+++ b/src/library/scoped_ext.cpp
@@ -136,6 +136,11 @@ environment pop_scope(environment const & env, name const & n) {
     return r;
 }
 
+bool has_open_scopes(environment const & env) {
+    scope_mng_ext ext = get_extension(env);
+    return !is_nil(ext.m_namespaces);
+}
+
 static int using_namespace_objects(lua_State * L) {
     int nargs = lua_gettop(L);
     environment const & env = to_environment(L, 1);
diff --git a/src/library/scoped_ext.h b/src/library/scoped_ext.h
index 9a8a0d1c36..0271ff32f3 100644
--- a/src/library/scoped_ext.h
+++ b/src/library/scoped_ext.h
@@ -26,6 +26,7 @@ environment using_namespace(environment const & env, io_state const & ios, name
 environment push_scope(environment const & env, io_state const & ios, bool section, name const & n = name());
 /** \brief Delete the most recent scope, all scoped extensions are notified. */
 environment pop_scope(environment const & env, name const & n = name());
+bool has_open_scopes(environment const & env);
 
 name const & get_namespace(environment const & env);
 list<name> const & get_namespaces(environment const & env);
diff --git a/tests/lean/crash.lean b/tests/lean/crash.lean
index 98bcd47c1a..b65542a4d5 100644
--- a/tests/lean/crash.lean
+++ b/tests/lean/crash.lean
@@ -9,3 +9,4 @@ theorem crash
             from H,
             _.
 
+end
\ No newline at end of file
diff --git a/tests/lean/run/cody1.lean b/tests/lean/run/cody1.lean
index 9db70c9f25..e72c41f58e 100644
--- a/tests/lean/run/cody1.lean
+++ b/tests/lean/run/cody1.lean
@@ -22,3 +22,4 @@ theorem false_aux : ¬ (δ (i delta))
             have H' : r (i delta) (i delta),
               from eq_rec H (symm retract),
             H H'.
+end
diff --git a/tests/lean/run/cody2.lean b/tests/lean/run/cody2.lean
index ac356b33d4..5b0ba77470 100644
--- a/tests/lean/run/cody2.lean
+++ b/tests/lean/run/cody2.lean
@@ -20,4 +20,6 @@ theorem delta_aux : ¬ (δ (i delta))
          := assume H : δ (i delta),
             H (subst (symm retract) H).
 
-check delta_aux.
\ No newline at end of file
+check delta_aux.
+
+end
\ No newline at end of file
diff --git a/tests/lean/run/elab_bug1.lean b/tests/lean/run/elab_bug1.lean
index cba7041597..686f26d3b7 100644
--- a/tests/lean/run/elab_bug1.lean
+++ b/tests/lean/run/elab_bug1.lean
@@ -65,3 +65,4 @@ iff_elim_left (@congr_app _ _ R iff P C a b H) H1
 theorem test2 (a b c d e : Prop) (H1 : a ↔ b) (H2 : a ∨ c → ¬(d → a)) : b ∨ c → ¬(d → b) :=
 subst_iff H1 H2
 
+end congruence
\ No newline at end of file
diff --git a/tests/lean/run/univ_bug2.lean b/tests/lean/run/univ_bug2.lean
index 845f60209f..a0b8f046ec 100644
--- a/tests/lean/run/univ_bug2.lean
+++ b/tests/lean/run/univ_bug2.lean
@@ -27,3 +27,5 @@ theorem test1 (S : Type) (T : Type) (f1 f2 : S → T) (s1 s2 : S) (Hf : f1 = f2)
 have Rs [fact] : simplifies_to f1 f2, from mk Hf,
 have Cs [fact] : simplifies_to s1 s2, from mk Hs,
 infer_eq _ _
+
+end simp
\ No newline at end of file