From c841763a05ce0424029909768fe3677e6b07fe02 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 6 Dec 2013 04:51:07 -0800
Subject: [PATCH] feat(library/elaborator): add special treatment for
 constraints of the form ?m[inst:i v] << t, where t is a proposition

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/kernel/context.cpp                      | 13 +++++++++++++
 src/kernel/context.h                        |  6 ++++++
 src/library/elaborator/elaborator.cpp       | 19 +++++++++++++++++--
 src/tests/library/elaborator/elaborator.cpp |  2 +-
 4 files changed, 37 insertions(+), 3 deletions(-)

diff --git a/src/kernel/context.cpp b/src/kernel/context.cpp
index 14da07abc..5504d1fca 100644
--- a/src/kernel/context.cpp
+++ b/src/kernel/context.cpp
@@ -46,4 +46,17 @@ static list<context_entry> remove_core(list<context_entry> const & l, unsigned s
 context context::remove(unsigned s, unsigned n) const {
     return context(remove_core(m_list, s, n));
 }
+
+static list<context_entry> insert_at_core(list<context_entry> const & l, unsigned i, name const & n, expr const & d) {
+    if (i == 0) {
+        return cons(context_entry(n, d), l);
+    } else {
+        lean_assert(l);
+        return cons(head(l), insert_at_core(tail(l), i - 1, n, d));
+    }
+}
+
+context context::insert_at(unsigned i, name const & n, expr const & d) const {
+    return context(insert_at_core(m_list, i, n, d));
+}
 }
diff --git a/src/kernel/context.h b/src/kernel/context.h
index f9436d926..a3e14b82a 100644
--- a/src/kernel/context.h
+++ b/src/kernel/context.h
@@ -51,6 +51,12 @@ public:
        \pre size() >= s + n
     */
     context remove(unsigned s, unsigned n) const;
+    /**
+       \brief Return a new context where then entry n : d is inserted at position i.
+
+       \pre size() >= i
+    */
+    context insert_at(unsigned i, name const & n, expr const & d) const;
 };
 
 /**
diff --git a/src/library/elaborator/elaborator.cpp b/src/library/elaborator/elaborator.cpp
index 11a98fd82..4d957ac6d 100644
--- a/src/library/elaborator/elaborator.cpp
+++ b/src/library/elaborator/elaborator.cpp
@@ -398,6 +398,7 @@ class elaborator::imp {
     */
     enum status { Processed, Failed, Continue };
     status process_metavar(unification_constraint const & c, expr const & a, expr const & b, bool is_lhs) {
+        context const & ctx = get_context(c);
         if (is_metavar(a)) {
             if (is_assigned(a)) {
                 // Case 1
@@ -410,7 +411,7 @@ class elaborator::imp {
                 if (has_metavar(b, a)) {
                     m_conflict = justification(new unification_failure_justification(c));
                     return Failed;
-                } else if (is_eq(c) || is_proposition(b, get_context(c))) {
+                } else if (is_eq(c) || is_proposition(b, ctx)) {
                     // At this point, we only assign metavariables if the constraint is an equational constraint,
                     // or b is a proposition.
                     // It is important to handle propositions since we don't want to normalize them.
@@ -426,7 +427,7 @@ class elaborator::imp {
                         justification new_jst(new normalize_justification(c));
                         expr new_a = pop_meta_context(a);
                         expr new_b = lower_free_vars(b, me.s() + me.n(), me.n());
-                        context new_ctx = get_context(c).remove(me.s(), me.n());
+                        context new_ctx = ctx.remove(me.s(), me.n());
                         if (!is_lhs)
                             swap(new_a, new_b);
                         push_new_constraint(is_eq(c), new_ctx, new_a, new_b, new_jst);
@@ -437,6 +438,20 @@ class elaborator::imp {
                         m_conflict = justification(new unification_failure_justification(c));
                         return Failed;
                     }
+                } else if (me.is_inst() && is_proposition(b, ctx) && !is_proposition(me.v(), ctx)) {
+                    // If b is a proposition, and the value in the local context is not,
+                    // we ignore it, and create new constraint without the head of the local context.
+                    // This is a little bit hackish. We do it because we want to preserve
+                    // the structure of the proposition. This is similar to the trick used
+                    // in the assign(a, b, c) branch above.
+                    justification new_jst(new normalize_justification(c));
+                    expr new_a = pop_meta_context(a);
+                    expr new_b = lift_free_vars(b, me.s(), 1);
+                    context new_ctx = ctx.insert_at(me.s(), g_x_name, Type()); // insert a dummy at position s
+                    if (!is_lhs)
+                        swap(new_a, new_b);
+                    push_new_constraint(is_eq(c), new_ctx, new_a, new_b, new_jst);
+                    return Processed;
                 }
             }
         }
diff --git a/src/tests/library/elaborator/elaborator.cpp b/src/tests/library/elaborator/elaborator.cpp
index b066c19e3..f1248629d 100644
--- a/src/tests/library/elaborator/elaborator.cpp
+++ b/src/tests/library/elaborator/elaborator.cpp
@@ -284,7 +284,7 @@ static void success(expr const & e, expr const & expected, environment const & e
     std::cout << "\n" << e << "\n\n";
     expr r = elaborate(e, env);
     std::cout << "\n" << e << "\n------>\n" << r << "\n";
-    lean_assert(r == expected);
+    lean_assert_eq(r, expected);
 }
 
 // Check elaborator failure