From bf8a7eb9b40effadbe823d5a2acafc5c29439fb8 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 21 Apr 2015 18:56:28 -0700
Subject: [PATCH] fix(library/scoped_ext): bug in local metadata in sections

The problem is described in issue #554
---
 hott/init/logic.hlean                         |  3 +
 hott/init/trunc.hlean                         |  1 +
 library/data/int/basic.lean                   |  1 +
 library/data/int/order.lean                   |  1 +
 library/data/nat/basic.lean                   |  1 +
 library/data/nat/order.lean                   |  1 +
 library/init/logic.lean                       |  1 +
 src/frontends/lean/builtin_cmds.cpp           |  4 +-
 src/frontends/lean/parser.cpp                 |  2 +-
 src/library/aliases.cpp                       |  4 +-
 src/library/scoped_ext.cpp                    | 14 ++--
 src/library/scoped_ext.h                      | 64 ++++++++++++-------
 tests/lean/local_notation_bug.lean            | 24 +++++++
 .../lean/local_notation_bug.lean.expected.out |  6 ++
 tests/lean/local_notation_bug2.lean           |  7 ++
 .../local_notation_bug2.lean.expected.out     |  1 +
 16 files changed, 99 insertions(+), 36 deletions(-)
 create mode 100644 tests/lean/local_notation_bug.lean
 create mode 100644 tests/lean/local_notation_bug.lean.expected.out
 create mode 100644 tests/lean/local_notation_bug2.lean
 create mode 100644 tests/lean/local_notation_bug2.lean.expected.out

diff --git a/hott/init/logic.hlean b/hott/init/logic.hlean
index fc3a7c5aa..348fdc4f5 100644
--- a/hott/init/logic.hlean
+++ b/hott/init/logic.hlean
@@ -316,6 +316,8 @@ if_pos unit.star
 definition if_empty {A : Type} (t e : A) : (if empty then t else e) = e :=
 if_neg not_empty
 
+section
+open eq.ops
 definition if_cond_congr {c₁ c₂ : Type} [H₁ : decidable c₁] [H₂ : decidable c₂] (Heq : c₁ ↔ c₂) {A : Type} (t e : A)
                       : (if c₁ then t else e) = (if c₂ then t else e) :=
 decidable.rec_on H₁
@@ -357,3 +359,4 @@ decidable.rec
 -- Remark: dite and ite are "definitionally equal" when we ignore the proofs.
 definition dite_ite_eq (c : Type) [H : decidable c] {A : Type} (t : A) (e : A) : dite c (λh, t) (λh, e) = ite c t e :=
 rfl
+end
diff --git a/hott/init/trunc.hlean b/hott/init/trunc.hlean
index 0cb548ae5..dfa20c697 100644
--- a/hott/init/trunc.hlean
+++ b/hott/init/trunc.hlean
@@ -249,6 +249,7 @@ namespace is_trunc
 
   /- interaction with the Unit type -/
 
+  open equiv
   -- A contractible type is equivalent to [Unit]. *)
   definition equiv_unit_of_is_contr [H : is_contr A] : A ≃ unit :=
     equiv.mk (λ (x : A), ⋆)
diff --git a/library/data/int/basic.lean b/library/data/int/basic.lean
index 250b3816d..703e53e8f 100644
--- a/library/data/int/basic.lean
+++ b/library/data/int/basic.lean
@@ -630,6 +630,7 @@ end
 /- instantiate ring theorems to int -/
 
 section port_algebra
+  open [classes] algebra
   theorem mul.left_comm : ∀a b c : ℤ, a * (b * c) = b * (a * c) := algebra.mul.left_comm
   theorem mul.right_comm : ∀a b c : ℤ, (a * b) * c = (a * c) * b := algebra.mul.right_comm
   theorem add.left_comm : ∀a b c : ℤ, a + (b + c) = b + (a + c) := algebra.add.left_comm
diff --git a/library/data/int/order.lean b/library/data/int/order.lean
index d5e236835..498daab89 100644
--- a/library/data/int/order.lean
+++ b/library/data/int/order.lean
@@ -247,6 +247,7 @@ end
 /- instantiate ordered ring theorems to int -/
 
 section port_algebra
+  open [classes] algebra
   definition ge [reducible] (a b : ℤ) := algebra.has_le.ge a b
   definition gt [reducible] (a b : ℤ) := algebra.has_lt.gt a b
   infix >= := int.ge
diff --git a/library/data/nat/basic.lean b/library/data/nat/basic.lean
index fa4edafdc..604f3a30f 100644
--- a/library/data/nat/basic.lean
+++ b/library/data/nat/basic.lean
@@ -311,6 +311,7 @@ section
 end
 
 section port_algebra
+  open [classes] algebra
   theorem mul.left_comm : ∀a b c : ℕ, a * (b * c) = b * (a * c) := algebra.mul.left_comm
   theorem mul.right_comm : ∀a b c : ℕ, (a * b) * c = (a * c) * b := algebra.mul.right_comm
 
diff --git a/library/data/nat/order.lean b/library/data/nat/order.lean
index 598541cb9..72d7b84c5 100644
--- a/library/data/nat/order.lean
+++ b/library/data/nat/order.lean
@@ -173,6 +173,7 @@ section
 end
 
 section port_algebra
+  open [classes] algebra
   theorem add_pos_left : ∀{a : ℕ}, 0 < a → ∀b : ℕ, 0 < a + b :=
     take a H b, @algebra.add_pos_of_pos_of_nonneg _ _ a b H !zero_le
   theorem add_pos_right : ∀{a : ℕ}, 0 < a → ∀b : ℕ, 0 < b + a :=
diff --git a/library/init/logic.lean b/library/init/logic.lean
index 9945b03aa..95c28f0f4 100644
--- a/library/init/logic.lean
+++ b/library/init/logic.lean
@@ -384,6 +384,7 @@ match H a a with
 | inr n := absurd rfl n
 end
 
+open eq.ops
 theorem decidable_eq_inr_neg {A : Type} [H : decidable_eq A] {a b : A} : Π n : a ≠ b, H a b = inr n :=
 assume n,
 match H a b with
diff --git a/src/frontends/lean/builtin_cmds.cpp b/src/frontends/lean/builtin_cmds.cpp
index e36dbc170..908f88103 100644
--- a/src/frontends/lean/builtin_cmds.cpp
+++ b/src/frontends/lean/builtin_cmds.cpp
@@ -309,11 +309,11 @@ environment end_scoped_cmd(parser & p) {
     p.pop_local_scope();
     if (p.curr_is_identifier()) {
         name n = p.check_atomic_id_next("invalid end of scope, atomic identifier expected");
-        environment env = pop_scope(p.env(), n);
+        environment env = pop_scope(p.env(), p.ios(), n);
         redeclare_aliases(p, level_entries, entries);
         return env;
     } else {
-        environment env = pop_scope(p.env());
+        environment env = pop_scope(p.env(), p.ios());
         redeclare_aliases(p, level_entries, entries);
         return env;
     }
diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp
index d3ffa1527..07d4c7e9c 100644
--- a/src/frontends/lean/parser.cpp
+++ b/src/frontends/lean/parser.cpp
@@ -1634,7 +1634,7 @@ bool parser::parse_commands() {
     } catch (interrupt_parser) {
         commit_info();
         while (has_open_scopes(m_env))
-            m_env = pop_scope_core(m_env);
+            m_env = pop_scope_core(m_env, m_ios);
     }
     commit_info(m_scanner.get_line()+1, 0);
     for (certified_declaration const & thm : m_theorem_queue.join()) {
diff --git a/src/library/aliases.cpp b/src/library/aliases.cpp
index fa306a527..e22276413 100644
--- a/src/library/aliases.cpp
+++ b/src/library/aliases.cpp
@@ -102,7 +102,7 @@ struct aliases_ext : public environment_extension {
         return env;
     }
 
-    static environment push_scope(environment const & env, scope_kind k) {
+    static environment push_scope(environment const & env, io_state const &, scope_kind k) {
         aliases_ext ext = get_extension(env);
         ext.push(k != scope_kind::Namespace);
         environment new_env = update(env, ext);
@@ -111,7 +111,7 @@ struct aliases_ext : public environment_extension {
         return new_env;
     }
 
-    static environment pop_scope(environment const & env, scope_kind) {
+    static environment pop_scope(environment const & env, io_state const &, scope_kind) {
         aliases_ext ext = get_extension(env);
         ext.pop();
         return update(env, ext);
diff --git a/src/library/scoped_ext.cpp b/src/library/scoped_ext.cpp
index 9d23271dd..3fbb45bbc 100644
--- a/src/library/scoped_ext.cpp
+++ b/src/library/scoped_ext.cpp
@@ -161,7 +161,7 @@ environment push_scope(environment const & env, io_state const & ios, scope_kind
     ext.m_scope_kinds = cons(k, ext.m_scope_kinds);
     environment r = update(env, ext);
     for (auto const & t : get_exts()) {
-        r = std::get<3>(t)(r, k);
+        r = std::get<3>(t)(r, ios, k);
     }
     if (k == scope_kind::Namespace)
         r = using_namespace(r, ios, new_n);
@@ -182,7 +182,7 @@ static void namespace_reader(deserializer & d, module_idx, shared_environment &,
         });
 }
 
-environment pop_scope_core(environment const & env) {
+environment pop_scope_core(environment const & env, io_state const & ios) {
     scope_mng_ext ext = get_extension(env);
     if (is_nil(ext.m_namespaces))
         return env;
@@ -192,19 +192,19 @@ environment pop_scope_core(environment const & env) {
     ext.m_scope_kinds = tail(ext.m_scope_kinds);
     environment r = update(env, ext);
     for (auto const & t : get_exts()) {
-        r = std::get<4>(t)(r, k);
+        r = std::get<4>(t)(r, ios, k);
     }
     return r;
 }
 
-environment pop_scope(environment const & env, name const & n) {
+environment pop_scope(environment const & env, io_state const & ios, name const & n) {
     scope_mng_ext ext = get_extension(env);
     if (is_nil(ext.m_namespaces))
         throw exception("invalid end of scope, there are no open namespaces/sections/contexts");
     if (n != head(ext.m_headers))
         throw exception(sstream() << "invalid end of scope, begin/end mistmatch, scope starts with '"
                         << head(ext.m_headers) << "', and ends with '" << n << "'");
-    return pop_scope_core(env);
+    return pop_scope_core(env, ios);
 }
 
 bool has_open_scopes(environment const & env) {
@@ -240,9 +240,9 @@ static int push_scope(lua_State * L) {
 static int pop_scope(lua_State * L) {
     int nargs = lua_gettop(L);
     if (nargs == 1)
-        return push_environment(L, pop_scope(to_environment(L, 1)));
+        return push_environment(L, pop_scope(to_environment(L, 1), get_io_state(L)));
     else
-        return push_environment(L, pop_scope(to_environment(L, 1), to_name_ext(L, 2)));
+        return push_environment(L, pop_scope(to_environment(L, 1), get_io_state(L), to_name_ext(L, 2)));
 }
 
 void open_scoped_ext(lua_State * L) {
diff --git a/src/library/scoped_ext.h b/src/library/scoped_ext.h
index 7efa3f8f5..e8c9bd101 100644
--- a/src/library/scoped_ext.h
+++ b/src/library/scoped_ext.h
@@ -19,8 +19,8 @@ namespace lean {
 enum class scope_kind { Namespace, Section, Context };
 typedef environment (*using_namespace_fn)(environment const &, io_state const &, name const &);
 typedef environment (*export_namespace_fn)(environment const &, io_state const &, name const &);
-typedef environment (*push_scope_fn)(environment const &, scope_kind);
-typedef environment (*pop_scope_fn)(environment const &, scope_kind);
+typedef environment (*push_scope_fn)(environment const &, io_state const &, scope_kind);
+typedef environment (*pop_scope_fn)(environment const &, io_state const &, scope_kind);
 
 void register_scoped_ext(name const & n, using_namespace_fn use, export_namespace_fn ex, push_scope_fn push, pop_scope_fn pop);
 /** \brief Use objects defined in the namespace \c n.
@@ -37,11 +37,11 @@ environment push_scope(environment const & env, io_state const & ios, scope_kind
 /** \brief Delete the most recent scope, all scoped extensions are notified.
     \remark method throws an exception if there are no open scopes, or \c n does not match the name of the open scope
 */
-environment pop_scope(environment const & env, name const & n = name());
+environment pop_scope(environment const & env, io_state const & ios, name const & n = name());
 /** \brief Similar to \c pop_scope, but it always succeed.
     It always pops the current open scope, and does nothing if there are no open scope.
 */
-environment pop_scope_core(environment const & env);
+environment pop_scope_core(environment const & env, io_state const & ios);
 /** \brief Return true iff there are open scopes */
 bool has_open_scopes(environment const & env);
 
@@ -93,10 +93,11 @@ class scoped_ext : public environment_extension {
 
     state                 m_state;
     list<state>           m_scopes;
-    name_map<list<entry>> m_entries;
+    list<list<entry>>     m_nonlocal_entries; // nonlocal entries per scope (for sections)
+    name_map<list<entry>> m_entries_map;      // namespace -> entries
 
     void using_namespace_core(environment const & env, io_state const & ios, name const & n) {
-        if (auto it = m_entries.find(n)) {
+        if (auto it = m_entries_map.find(n)) {
             buffer<entry> entries;
             to_buffer(*it, entries);
             unsigned i = entries.size();
@@ -108,10 +109,10 @@ class scoped_ext : public environment_extension {
     }
 
     void register_entry_core(name n, entry const & e) {
-        if (auto it = m_entries.find(n))
-            m_entries.insert(n, cons(e, *it));
+        if (auto it = m_entries_map.find(n))
+            m_entries_map.insert(n, cons(e, *it));
         else
-            m_entries.insert(n, to_list(e));
+            m_entries_map.insert(n, to_list(e));
     }
 
     void add_entry_core(environment const & env, io_state const & ios, entry const & e) {
@@ -130,6 +131,8 @@ class scoped_ext : public environment_extension {
     scoped_ext _add_entry(environment const & env, io_state const & ios, entry const & e) const {
         scoped_ext r(*this);
         r.register_entry_core(get_namespace(env), e);
+        if (r.m_nonlocal_entries)
+            r.m_nonlocal_entries = cons(cons(e, head(r.m_nonlocal_entries)), tail(r.m_nonlocal_entries));
         add_entry(env, ios, r.m_state, e);
         return r;
     }
@@ -148,7 +151,7 @@ public:
     }
 
     environment export_namespace(environment env, io_state const & ios, name const & n) const {
-        if (auto it = m_entries.find(n)) {
+        if (auto it = m_entries_map.find(n)) {
             buffer<entry> entries;
             to_buffer(*it, entries);
             unsigned i = entries.size();
@@ -162,16 +165,26 @@ public:
 
     scoped_ext push() const {
         scoped_ext r(*this);
-        r.m_scopes     = cons(m_state, r.m_scopes);
+        r.m_scopes           = cons(m_state, r.m_scopes);
+        r.m_nonlocal_entries = cons(list<entry>(), r.m_nonlocal_entries);
         return r;
     }
 
-    scoped_ext pop() const {
+    pair<scoped_ext, list<entry>> pop(scope_kind k) const {
         lean_assert(!is_nil(m_scopes));
         scoped_ext r(*this);
         r.m_state  = head(m_scopes);
         r.m_scopes = tail(m_scopes);
-        return r;
+        if (k == scope_kind::Section) {
+            auto entries = head(r.m_nonlocal_entries);
+            r.m_nonlocal_entries = tail(r.m_nonlocal_entries);
+            if (r.m_nonlocal_entries)
+                r.m_nonlocal_entries = cons(append(entries, head(r.m_nonlocal_entries)), tail(r.m_nonlocal_entries));
+            return mk_pair(r, entries);
+        } else {
+            r.m_nonlocal_entries = tail(r.m_nonlocal_entries);
+            return mk_pair(r, list<entry>());
+        }
     }
 
     struct reg {
@@ -199,17 +212,20 @@ public:
     static environment export_namespace_fn(environment const & env, io_state const & ios, name const & n) {
         return get(env).export_namespace(env, ios, n);
     }
-    static environment push_fn(environment const & env, scope_kind k) {
-        if (k != scope_kind::Section)
-            return update(env, get(env).push());
-        else
-            return env;
+    static environment push_fn(environment const & env, io_state const &, scope_kind) {
+        return update(env, get(env).push());
     }
-    static environment pop_fn(environment const & env, scope_kind k) {
-        if (k != scope_kind::Section)
-            return update(env, get(env).pop());
-        else
-            return env;
+    static environment pop_fn(environment const & env, io_state const & ios, scope_kind k) {
+        auto p = get(env).pop(k);
+        environment new_env = update(env, p.first);
+        buffer<entry> entries;
+        to_buffer(p.second, entries);
+        unsigned i = entries.size();
+        while (i > 0) {
+            --i;
+            new_env = update(new_env, get(new_env)._add_tmp_entry(new_env, ios, entries[i]));
+        }
+        return new_env;
     }
     static environment register_entry(environment const & env, io_state const & ios, name const & n, entry const & e) {
         return update(env, get(env)._register_entry(env, ios, n, e));
@@ -243,7 +259,7 @@ public:
         return get(env).m_state;
     }
     static list<entry> const * get_entries(environment const & env, name const & n) {
-        return get(env).m_entries.find(n);
+        return get(env).m_entries_map.find(n);
     }
 };
 
diff --git a/tests/lean/local_notation_bug.lean b/tests/lean/local_notation_bug.lean
new file mode 100644
index 000000000..de812aee7
--- /dev/null
+++ b/tests/lean/local_notation_bug.lean
@@ -0,0 +1,24 @@
+import logic
+
+section
+  variables {A : Type}
+  variables f : A → A → A
+  local infixl `+++`:10 := f
+
+  variables a b c : A
+  check f a b
+  check a +++ b
+
+  definition foo : nat → bool :=
+  λn, bool.tt
+
+  notation `bla`:100 := 10
+  local attribute foo [coercion]
+  print coercions
+end
+
+print coercions -- should be empty
+check bla
+check 1 +++ 2   -- should say +++ is an invalid expression
+open nat
+print coercions
diff --git a/tests/lean/local_notation_bug.lean.expected.out b/tests/lean/local_notation_bug.lean.expected.out
new file mode 100644
index 000000000..93bf4ae95
--- /dev/null
+++ b/tests/lean/local_notation_bug.lean.expected.out
@@ -0,0 +1,6 @@
+f a b : A
+f a b : A
+nat ↣ bool : foo
+bla : num
+local_notation_bug.lean:22:8: error: invalid expression
+num ↣ nat : of_num
diff --git a/tests/lean/local_notation_bug2.lean b/tests/lean/local_notation_bug2.lean
new file mode 100644
index 000000000..7ce70798a
--- /dev/null
+++ b/tests/lean/local_notation_bug2.lean
@@ -0,0 +1,7 @@
+open nat
+section
+parameters (b : ℕ)
+definition add_b (n : ℕ) := n + b
+local postfix `%`:max := add_b
+end
+eval 5% -- Error, unexpected token
diff --git a/tests/lean/local_notation_bug2.lean.expected.out b/tests/lean/local_notation_bug2.lean.expected.out
new file mode 100644
index 000000000..e13686c29
--- /dev/null
+++ b/tests/lean/local_notation_bug2.lean.expected.out
@@ -0,0 +1 @@
+local_notation_bug2.lean:7:6: error: unexpected token