From f6f2c499ae8d86a4cef6e4cf71942eae3dc71013 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 13 Mar 2015 19:24:09 -0700
Subject: [PATCH] fix(library/tactic/rewrite_tactic): rewrite macros did not
 implement operator==

This problem was affecting the cache
---
 src/library/tactic/location.h         |  6 +++++
 src/library/tactic/rewrite_tactic.cpp | 37 +++++++++++++++++++++++++++
 2 files changed, 43 insertions(+)

diff --git a/src/library/tactic/location.h b/src/library/tactic/location.h
index b7f1fe3b3..44db1268e 100644
--- a/src/library/tactic/location.h
+++ b/src/library/tactic/location.h
@@ -47,6 +47,9 @@ public:
     unsigned contains(unsigned occ_idx) const;
     friend serializer & operator<<(serializer & s, occurrence const & o);
     friend deserializer & operator>>(deserializer & d, occurrence & o);
+
+    bool operator==(occurrence const & o) const { return m_kind == o.m_kind && m_occs == o.m_occs; }
+    bool operator!=(occurrence const & o) const { return !operator==(o); }
 };
 
 /** \brief Replace occurrences of \c t in \c e with the free variable #vidx.
@@ -83,6 +86,9 @@ public:
     optional<occurrence> includes_hypothesis(name const & h) const;
     void get_explicit_hypotheses_names(buffer<name> & r) const;
 
+    bool operator==(location const & l) const { return m_kind == l.m_kind && m_goal == l.m_goal && m_hyps == l.m_hyps; }
+    bool operator!=(location const & l) const { return !operator==(l); }
+
     friend serializer & operator<<(serializer & s, location const & loc);
     friend deserializer & operator>>(deserializer & d, location & loc);
 };
diff --git a/src/library/tactic/rewrite_tactic.cpp b/src/library/tactic/rewrite_tactic.cpp
index 4b333b750..9dca95843 100644
--- a/src/library/tactic/rewrite_tactic.cpp
+++ b/src/library/tactic/rewrite_tactic.cpp
@@ -81,6 +81,9 @@ public:
         d >> e.m_location;
         return d;
     }
+
+    bool operator==(unfold_info const & i) const { return m_names == i.m_names && m_location == i.m_location; }
+    bool operator!=(unfold_info const & i) const { return !operator==(i); }
 };
 
 class reduce_info {
@@ -97,6 +100,9 @@ public:
         d >> e.m_location;
         return d;
     }
+
+    bool operator==(reduce_info const & i) const { return m_location == i.m_location; }
+    bool operator!=(reduce_info const & i) const { return !operator==(i); }
 };
 
 class rewrite_info {
@@ -132,6 +138,13 @@ public:
         return rewrite_info(symm, OneOrMore, optional<unsigned>(), loc);
     }
 
+    bool operator==(rewrite_info const & i) const {
+        return
+            m_symm == i.m_symm && m_multiplicity == i.m_multiplicity &&
+            m_num  == i.m_num  && m_location == i.m_location;
+    }
+    bool operator!=(rewrite_info const & i) const { return !operator==(i); }
+
     bool symm() const {
         return m_symm;
     }
@@ -199,6 +212,12 @@ public:
         s << *g_rewrite_reduce_opcode << m_info;
     }
     reduce_info const & get_info() const { return m_info; }
+
+    virtual bool operator==(macro_definition_cell const & other) const {
+        if (auto o = dynamic_cast<rewrite_reduce_macro_cell const *>(&other))
+            return m_info == o->m_info;
+        return false;
+    }
 };
 
 expr mk_rewrite_reduce(location const & loc) {
@@ -231,6 +250,12 @@ public:
         s << *g_rewrite_fold_opcode << m_info;
     }
     fold_info const & get_info() const { return m_info; }
+
+    virtual bool operator==(macro_definition_cell const & other) const {
+        if (auto o = dynamic_cast<rewrite_fold_macro_cell const *>(&other))
+            return m_info == o->m_info;
+        return false;
+    }
 };
 
 expr mk_rewrite_fold(expr const & e, location const & loc) {
@@ -256,6 +281,12 @@ public:
         s << *g_rewrite_unfold_opcode << m_info;
     }
     unfold_info const & get_info() const { return m_info; }
+
+    virtual bool operator==(macro_definition_cell const & other) const {
+        if (auto o = dynamic_cast<rewrite_unfold_macro_cell const *>(&other))
+            return m_info == o->m_info;
+        return false;
+    }
 };
 
 expr mk_rewrite_unfold(list<name> const & ns, location const & loc) {
@@ -281,6 +312,12 @@ public:
         s << *g_rewrite_elem_opcode << m_info;
     }
     rewrite_info const & get_info() const { return m_info; }
+
+    virtual bool operator==(macro_definition_cell const & other) const {
+        if (auto o = dynamic_cast<rewrite_element_macro_cell const *>(&other))
+            return m_info == o->m_info;
+        return false;
+    }
 };
 
 expr mk_rw_macro(macro_definition const & def, optional<expr> const & pattern, expr const & H) {