From 1cbf40a5d2e6ef8dafaec6be5309cadc4c734de0 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 6 Aug 2014 21:23:37 -0700
Subject: [PATCH] fix(frontends/lean): remove duplicate info entries, fix bug
 in save_overload

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/frontends/lean/elaborator.cpp | 25 ++++++++++++++++---------
 src/frontends/lean/info_manager.h |  4 ++++
 src/frontends/lean/parser.cpp     |  2 +-
 3 files changed, 21 insertions(+), 10 deletions(-)

diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp
index d42f6b1c1..4d323deb1 100644
--- a/src/frontends/lean/elaborator.cpp
+++ b/src/frontends/lean/elaborator.cpp
@@ -121,8 +121,6 @@ public:
     expr operator()(expr const & e) { return apply(e); }
 };
 
-typedef std::pair<pos_info, expr> pre_info_data;
-
 /** \brief Return a list of instances of the class \c cls_name that occur in \c ctx */
 list<expr> get_local_instances(list<expr> const & ctx, name const & cls_name) {
     buffer<expr> buffer;
@@ -310,7 +308,7 @@ class elaborator {
     bool                m_use_local_instances; // if true class-instance resolution will use the local context
     bool                m_relax_main_opaque; // if true, then treat opaque definitions from the main module as transparent
     info_manager *      m_info_manager;
-    std::vector<pre_info_data> m_info_data;
+    std::vector<type_info_data> m_pre_info_data;
 
     struct scope_ctx {
         context::scope m_scope1;
@@ -948,10 +946,10 @@ public:
                 type_checker::scope scope(*m_tc[m_relax_main_opaque]);
                 expr t = m_tc[m_relax_main_opaque]->infer(r);
                 if (replace) {
-                    while (!m_info_data.empty() && m_info_data.back().first == *p)
-                        m_info_data.pop_back();
+                    while (!m_pre_info_data.empty() && m_pre_info_data.back().eq_pos(p->first, p->second))
+                        m_pre_info_data.pop_back();
                 }
-                m_info_data.push_back(mk_pair(*p, t));
+                m_pre_info_data.push_back(type_info_data(p->first, p->second, t));
             }
         }
     }
@@ -1304,9 +1302,18 @@ public:
     void copy_info_to_manager(substitution s) {
         if (!m_info_manager)
             return;
-        for (auto & p : m_info_data) {
-            p.second = s.instantiate(p.second);
-            m_info_manager->add(std::unique_ptr<info_data>(new type_info_data(p.first.first, p.first.second, p.second)));
+        for (auto & p : m_pre_info_data) {
+            p = type_info_data(p.get_line(), p.get_column(), s.instantiate(p.get_type()));
+        }
+        std::stable_sort(m_pre_info_data.begin(), m_pre_info_data.end());
+        type_info_data prev;
+        bool first = true;
+        for (auto const & p : m_pre_info_data) {
+            if (first || !p.eq_pos(prev.get_line(), prev.get_column())) {
+                m_info_manager->add(std::unique_ptr<info_data>(new type_info_data(p)));
+                prev  = p;
+                first = false;
+            }
         }
     }
 
diff --git a/src/frontends/lean/info_manager.h b/src/frontends/lean/info_manager.h
index ac5c13694..2d17e426b 100644
--- a/src/frontends/lean/info_manager.h
+++ b/src/frontends/lean/info_manager.h
@@ -16,10 +16,12 @@ class info_data {
     unsigned m_line;
     unsigned m_column;
 public:
+    info_data():m_line(0), m_column(0) {}
     info_data(unsigned l, unsigned c):m_line(l), m_column(c) {}
     virtual ~info_data() {}
     unsigned get_line() const { return m_line; }
     unsigned get_column() const { return m_column; }
+    bool eq_pos(unsigned line, unsigned col) const { return m_line == line && m_column == col; }
     virtual void display(io_state_stream const & ios) const = 0;
 };
 bool operator<(info_data const & i1, info_data const & i2);
@@ -27,7 +29,9 @@ bool operator<(info_data const & i1, info_data const & i2);
 class type_info_data : public info_data {
     expr m_expr;
 public:
+    type_info_data() {}
     type_info_data(unsigned l, unsigned c, expr const & e):info_data(l, c), m_expr(e) {}
+    expr const & get_type() const { return m_expr; }
     virtual void display(io_state_stream const & ios) const;
 };
 
diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp
index 46d3bc0d4..ccc4694bd 100644
--- a/src/frontends/lean/parser.cpp
+++ b/src/frontends/lean/parser.cpp
@@ -1179,7 +1179,7 @@ void parser::save_snapshot() {
 }
 
 void parser::save_overload(expr const & e) {
-    if (!m_info_manager)
+    if (!m_info_manager || !is_choice(e))
         return;
     auto p = pos_of(e);
     m_info_manager->add(std::unique_ptr<info_data>(new overload_info_data(p.first, p.second, e)));