From fcd67649ed8e2d92846fd2be8f115e404c9f45fc Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sat, 7 Feb 2015 20:36:26 -0800
Subject: [PATCH] refactor(kernel): expose may_reduce_later method

---
 src/kernel/converter.cpp         | 1 +
 src/kernel/converter.h           | 7 +++++--
 src/kernel/default_converter.cpp | 4 ++++
 src/kernel/default_converter.h   | 1 +
 src/kernel/type_checker.h        | 2 ++
 src/library/unifier.cpp          | 4 +++-
 6 files changed, 16 insertions(+), 3 deletions(-)

diff --git a/src/kernel/converter.cpp b/src/kernel/converter.cpp
index 529bfa6db..3dadbb207 100644
--- a/src/kernel/converter.cpp
+++ b/src/kernel/converter.cpp
@@ -38,6 +38,7 @@ struct dummy_converter : public converter {
     virtual optional<module_idx> get_module_idx() const { return optional<module_idx>(); }
     virtual bool is_opaque(declaration const &) const { return false; }
     virtual optional<declaration> is_delta(expr const &) const { return optional<declaration>(); }
+    virtual bool may_reduce_later(expr const &, type_checker &) { return false; }
 };
 
 std::unique_ptr<converter> mk_dummy_converter() {
diff --git a/src/kernel/converter.h b/src/kernel/converter.h
index ea7c82207..dad641948 100644
--- a/src/kernel/converter.h
+++ b/src/kernel/converter.h
@@ -18,11 +18,14 @@ protected:
     extension_context & get_extension(type_checker & tc);
 public:
     virtual ~converter() {}
-    virtual pair<expr, constraint_seq> whnf(expr const & e, type_checker & c) = 0;
-    virtual pair<bool, constraint_seq> is_def_eq(expr const & t, expr const & s, type_checker & c, delayed_justification & j) = 0;
     virtual optional<module_idx> get_module_idx() const = 0;
     virtual bool is_opaque(declaration const & d) const = 0;
     virtual optional<declaration> is_delta(expr const & e) const = 0;
+
+    virtual bool may_reduce_later(expr const & e, type_checker & c) = 0;
+    virtual pair<expr, constraint_seq> whnf(expr const & e, type_checker & c) = 0;
+    virtual pair<bool, constraint_seq> is_def_eq(expr const & t, expr const & s, type_checker & c, delayed_justification & j) = 0;
+
     pair<bool, constraint_seq> is_def_eq(expr const & t, expr const & s, type_checker & c);
 };
 
diff --git a/src/kernel/default_converter.cpp b/src/kernel/default_converter.cpp
index d1594887a..5d1fbed46 100644
--- a/src/kernel/default_converter.cpp
+++ b/src/kernel/default_converter.cpp
@@ -51,6 +51,10 @@ bool default_converter::may_reduce_later(expr const & e) {
     return static_cast<bool>(m_env.norm_ext().may_reduce_later(e, get_extension(*m_tc)));
 }
 
+bool default_converter::may_reduce_later(expr const & e, type_checker & c) {
+    return static_cast<bool>(m_env.norm_ext().may_reduce_later(e, get_extension(c)));
+}
+
 /** \brief Weak head normal form core procedure. It does not perform delta reduction nor normalization extensions. */
 expr default_converter::whnf_core(expr const & e) {
     check_system("whnf");
diff --git a/src/kernel/default_converter.h b/src/kernel/default_converter.h
index 1dacd6ea0..a0f40ea96 100644
--- a/src/kernel/default_converter.h
+++ b/src/kernel/default_converter.h
@@ -77,6 +77,7 @@ public:
     virtual bool is_opaque(declaration const & d) const;
     virtual optional<module_idx> get_module_idx() const { return m_module_idx; }
 
+    virtual bool may_reduce_later(expr const & e, type_checker & c);
     virtual pair<expr, constraint_seq> whnf(expr const & e_prime, type_checker & c);
     virtual pair<bool, constraint_seq> is_def_eq(expr const & t, expr const & s, type_checker & c, delayed_justification & jst);
 };
diff --git a/src/kernel/type_checker.h b/src/kernel/type_checker.h
index f5c40d1a8..917914964 100644
--- a/src/kernel/type_checker.h
+++ b/src/kernel/type_checker.h
@@ -215,6 +215,8 @@ public:
 
     optional<declaration> is_delta(expr const & e) const { return m_conv->is_delta(e); }
 
+    bool may_reduce_later(expr const & e) { return m_conv->may_reduce_later(e, *this); }
+
     template<typename F>
     typename std::result_of<F()>::type with_params(level_param_names const & ps, F && f) {
         flet<level_param_names const *> updt(m_params, &ps);
diff --git a/src/library/unifier.cpp b/src/library/unifier.cpp
index 054ab2dd4..ecc66661c 100644
--- a/src/library/unifier.cpp
+++ b/src/library/unifier.cpp
@@ -940,7 +940,9 @@ struct unifier_fn {
             unsigned cidx = add_cnstr(c, cnstr_group::FlexFlex);
             add_meta_occ(lhs, cidx);
             add_meta_occ(rhs, cidx);
-        } else if (m_plugin->delay_constraint(*m_tc[relax], c)) {
+        } else if (m_tc[relax]->may_reduce_later(lhs) ||
+                   m_tc[relax]->may_reduce_later(rhs) ||
+                   m_plugin->delay_constraint(*m_tc[relax], c)) {
             unsigned cidx = add_cnstr(c, cnstr_group::PluginDelayed);
             add_meta_occs(lhs, cidx);
             add_meta_occs(rhs, cidx);