From 6ceecf6a15ae5f862082762044d8955d5c1ec2e2 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 7 Jul 2014 12:59:57 -0700
Subject: [PATCH] feat(library/aliases): remove duplicates from aliasing tables

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/library/aliases.cpp            |  2 +-
 tests/lean/alias.lean              | 25 +++++++++++++++++++++++++
 tests/lean/alias.lean.expected.out |  5 +++++
 3 files changed, 31 insertions(+), 1 deletion(-)
 create mode 100644 tests/lean/alias.lean
 create mode 100644 tests/lean/alias.lean.expected.out

diff --git a/src/library/aliases.cpp b/src/library/aliases.cpp
index 390ac0759..0bfe9ab96 100644
--- a/src/library/aliases.cpp
+++ b/src/library/aliases.cpp
@@ -35,7 +35,7 @@ struct aliases_ext : public environment_extension {
     void add_alias(name const & a, expr const & e) {
         auto it = m_state.m_aliases.find(a);
         if (it)
-            m_state.m_aliases.insert(a, list<expr>(e, *it));
+            m_state.m_aliases.insert(a, list<expr>(e, filter(*it, [&](expr const & t) { return t != e; })));
         else
             m_state.m_aliases.insert(a, list<expr>(e));
         m_state.m_inv_aliases.insert(e, a);
diff --git a/tests/lean/alias.lean b/tests/lean/alias.lean
new file mode 100644
index 000000000..685ca9c6e
--- /dev/null
+++ b/tests/lean/alias.lean
@@ -0,0 +1,25 @@
+import logic
+
+namespace N1
+  variable num : Type.{1}
+  variable foo : num → num → num
+end
+
+namespace N2
+  variable val : Type.{1}
+  variable foo : val → val → val
+end
+
+using N2
+using N1
+variables a b : num
+print raw foo a b
+using N2
+print raw foo a b
+using N1
+print raw foo a b
+using N1
+print raw foo a b
+using N2
+print raw foo a b
+
diff --git a/tests/lean/alias.lean.expected.out b/tests/lean/alias.lean.expected.out
new file mode 100644
index 000000000..7a9e1b3aa
--- /dev/null
+++ b/tests/lean/alias.lean.expected.out
@@ -0,0 +1,5 @@
+(choice N1.foo N2.foo) a b
+(choice N2.foo N1.foo) a b
+(choice N1.foo N2.foo) a b
+(choice N1.foo N2.foo) a b
+(choice N2.foo N1.foo) a b