Add timestamp to metavar_env

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

src/kernel/metavar.cpp

@@ -5,6 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 */
 #include <limits>
+#include "util/exception.h"
 #include "kernel/metavar.h"
 #include "kernel/replace.h"
 #include "kernel/free_vars.h"
@@ -12,7 +13,18 @@ Author: Leonardo de Moura
 #include "kernel/for_each.h"
 
 namespace lean {
+void metavar_env::inc_timestamp() {
+    if (m_timestamp == std::numeric_limits<unsigned>::max()) {
+        // This should not happen in real examples. We add it just to be safe.
+        throw exception("metavar_env timestamp overflow");
+    }
+    m_timestamp++;
+}
+
+metavar_env::metavar_env():m_timestamp(0) {}
+
 expr metavar_env::mk_metavar(context const & ctx) {
+    inc_timestamp();
     unsigned midx = m_env.size();
     m_env.push_back(data(ctx));
     return ::lean::mk_metavar(midx);
@@ -48,6 +60,7 @@ expr metavar_env::get_type(unsigned midx, unification_problems & up) {
 }
 
 void metavar_env::assign(unsigned midx, expr const & v) {
+    inc_timestamp();
     lean_assert(!is_assigned(midx));
     auto p = m_env[midx];
     m_env[midx] = data(v, p->m_type, p->m_ctx);

src/kernel/metavar.h

@@ -43,7 +43,17 @@ class metavar_env {
         data(expr const & s, expr const & t, context const & ctx):m_subst(s), m_type(t), m_ctx(ctx) {}
     };
     pvector<data> m_env;
+    unsigned      m_timestamp;
+    void inc_timestamp();
 public:
+    metavar_env();
+
+    /**
+       \brief The timestamp is increased whenever the environment is updated by
+       \c mk_metavar or \c assign.
+    */
+    unsigned get_timestamp() const { return m_timestamp; }
+
     /**
        \brief Create new metavariable in this environment.
     */

src/tests/kernel/metavar.cpp

@@ -234,6 +234,18 @@ static void tst10() {
     lean_assert(r == f(g(f(h(Var(2)))), Fun({x, N}, f(g(f(h(Var(3)))), h(Var(3)), x, Fun({y, N}, f(g(f(h(Var(4)))), x, y))))));
 }
 
+static void tst11() {
+    metavar_env menv;
+    unsigned t1 = menv.get_timestamp();
+    expr m = menv.mk_metavar();
+    unsigned t2 = menv.get_timestamp();
+    lean_assert(t2 > t1);
+    lean_assert(!menv.is_assigned(m));
+    lean_assert(menv.get_timestamp() == t2);
+    menv.assign(m, Const("a"));
+    lean_assert(menv.get_timestamp() > t2);
+}
+
 int main() {
     tst1();
     tst2();
@@ -245,5 +257,6 @@ int main() {
     tst8();
     tst9();
     tst10();
+    tst11();
     return has_violations() ? 1 : 0;
 }