From 4564bfa1d358a881cb02e92e2270666ac92f4e0b Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sun, 27 Oct 2013 11:17:03 -0700
Subject: [PATCH] feat(library/elaborator): improve simple_ho_match

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/frontends/lean/frontend_elaborator.cpp |  5 ++++
 src/library/elaborator/elaborator.cpp      | 32 +++++++++++++++++++++-
 2 files changed, 36 insertions(+), 1 deletion(-)

diff --git a/src/frontends/lean/frontend_elaborator.cpp b/src/frontends/lean/frontend_elaborator.cpp
index 7a45d73cd..4be952dd9 100644
--- a/src/frontends/lean/frontend_elaborator.cpp
+++ b/src/frontends/lean/frontend_elaborator.cpp
@@ -6,6 +6,7 @@ Author: Leonardo de Moura
 */
 #include <vector>
 #include <utility>
+#include <algorithm>
 #include "util/interruptable_ptr.h"
 #include "kernel/type_checker.h"
 #include "kernel/type_checker_justification.h"
@@ -310,6 +311,10 @@ class frontend_elaborator::imp {
     };
 
     metavar_env elaborate_core() {
+        // std::stable_sort(m_ucs.begin(), m_ucs.end(),
+        //                 [](unification_constraint const & c1, unification_constraint const & c2) {
+        //                     return !is_choice(c1) && is_choice(c2);
+        //                 });
         elaborator elb(m_env, m_menv, m_ucs.size(), m_ucs.data());
         scoped_set_interruptable_ptr<elaborator> set(m_elaborator, &elb);
         return elb.next();
diff --git a/src/library/elaborator/elaborator.cpp b/src/library/elaborator/elaborator.cpp
index 321cffc95..d2be36ac8 100644
--- a/src/library/elaborator/elaborator.cpp
+++ b/src/library/elaborator/elaborator.cpp
@@ -651,6 +651,32 @@ class elaborator::imp {
         return true;
     }
 
+    /**
+       \brief Return true iff \c a may be an actual lower bound for a convertibility constraint.
+       That is, if the result is false, it means the convertability constraint is essentially
+       an equality constraint.
+    */
+    bool is_actual_lower(expr const & a) {
+        return is_type(a) || is_metavar(a) || a == Bool || (is_pi(a) && is_actual_lower(abst_body(a)));
+    }
+
+    /**
+       \brief Return true iff \c a may be an actual upper bound for a convertibility constraint.
+       That is, if the result is false, it means the convertability constraint is essentially
+       an equality constraint.
+    */
+    bool is_actual_upper(expr const & a) {
+        return is_type(a) || is_metavar(a) || (is_pi(a) && is_actual_upper(abst_body(a)));
+    }
+
+    /**
+       \brief See \c process_simple_ho_match
+    */
+    bool is_simple_ho_match(context const & ctx, expr const & a, expr const & b, bool is_lhs, unification_constraint const & c) {
+        return is_meta_app(a) && are_args_vars(ctx, a) && closed(b) &&
+            (is_eq(c) || (is_lhs && !is_actual_upper(b)) || (!is_lhs && !is_actual_lower(b)));
+    }
+
     /**
         \brief Return true iff ctx |- a == b is a "simple" higher-order matching constraint. By simple, we mean
         a constraint of the form
@@ -661,7 +687,7 @@ class elaborator::imp {
         // Solve constraint of the form
         //    ctx |- (?m x) == c
         // using imitation
-        if (is_eq(c) && is_meta_app(a) && are_args_vars(ctx, a) && closed(b)) {
+        if (is_simple_ho_match(ctx, a, b, is_lhs, c)) {
             expr m = arg(a, 0);
             buffer<expr> types;
             for (unsigned i = 1; i < num_args(a); i++)
@@ -1060,6 +1086,8 @@ class elaborator::imp {
         if (normalize_head(a, b, c)) { return true; }
 
         if (!eq) {
+            // TODO(Leo): use is_actual_lower and is_actual_upper
+
             // Try to assign convertability constraints.
             if (!is_type(b) && !is_meta(b) && is_metavar(a) && !is_assigned(a) && !has_local_context(a)) {
                 // We can assign a <- b at this point IF b is not (Type lvl) or Metavariable
@@ -1075,6 +1103,8 @@ class elaborator::imp {
             }
         }
 
+        // TODO(Leo): normalize pi domain... to make sure we are not missing solutions in process_simple_ho_match
+
         if (process_simple_ho_match(ctx, a, b, true, c) ||
             process_simple_ho_match(ctx, b, a, false, c))
             return true;