From a26c7d47f2a6e8e8b1e3b6529c139a3b48cc2acb Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 17 Sep 2013 03:14:02 -0700
Subject: [PATCH] Add simplification to add_lift

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/kernel/metavar.cpp       | 13 ++++++++++---
 src/tests/kernel/metavar.cpp | 12 ++++++++++++
 2 files changed, 22 insertions(+), 3 deletions(-)

diff --git a/src/kernel/metavar.cpp b/src/kernel/metavar.cpp
index 79b1d01d2..b0c88131e 100644
--- a/src/kernel/metavar.cpp
+++ b/src/kernel/metavar.cpp
@@ -119,10 +119,17 @@ expr instantiate_metavars(expr const & e, metavar_env const & env) {
 }
 
 meta_ctx add_lift(meta_ctx const & ctx, unsigned s, unsigned n) {
-    if (n == 0)
+    if (n == 0) {
         return ctx;
-    else
-        return cons(mk_lift(s, n), ctx);
+    } else if (ctx) {
+        meta_entry e = head(ctx);
+        // Simplification rule
+        //    lift:(s1+n1):n2 lift:s1:n1 --->  lift:s1:n1+n2
+        if (e.is_lift() && s == e.s() + e.n()) {
+            return add_lift(tail(ctx), e.s(), e.n() + n);
+        }
+    }
+    return cons(mk_lift(s, n), ctx);
 }
 
 expr add_lift(expr const & m, unsigned s, unsigned n) {
diff --git a/src/tests/kernel/metavar.cpp b/src/tests/kernel/metavar.cpp
index 2c4d92036..bbf49a92d 100644
--- a/src/tests/kernel/metavar.cpp
+++ b/src/tests/kernel/metavar.cpp
@@ -432,6 +432,17 @@ static void tst20() {
     std::cout << norm(F, ctx) << "\n";
 }
 
+static void tst21() {
+    metavar_env menv;
+    expr m1 = menv.mk_metavar();
+    lean_assert(add_lift(add_lift(m1, 0, 1), 1, 1) ==
+                add_lift(m1, 0, 2));
+    lean_assert(add_lift(add_lift(m1, 1, 2), 3, 4) ==
+                add_lift(m1, 1, 6));
+    lean_assert(add_lift(add_lift(m1, 1, 3), 3, 4) !=
+                add_lift(m1, 1, 7));
+}
+
 int main() {
     tst1();
     tst2();
@@ -453,5 +464,6 @@ int main() {
     tst18();
     tst19();
     tst20();
+    tst21();
     return has_violations() ? 1 : 0;
 }