From 5b1b03bafd6040c0a8e58c443db72d0a46d80440 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 1 Oct 2013 08:41:50 -0700
Subject: [PATCH] refactor(is_convertible): move from normalizer to
 type_checker class

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/kernel/normalizer.cpp   | 66 ----------------------------------
 src/kernel/normalizer.h     |  4 ---
 src/kernel/type_checker.cpp | 71 +++++++++++++++++++++++++++++++++----
 src/kernel/type_checker.h   |  2 ++
 4 files changed, 66 insertions(+), 77 deletions(-)

diff --git a/src/kernel/normalizer.cpp b/src/kernel/normalizer.cpp
index ba986f531..d40ba76a4 100644
--- a/src/kernel/normalizer.cpp
+++ b/src/kernel/normalizer.cpp
@@ -290,31 +290,6 @@ class normalizer::imp {
         return r;
     }
 
-    bool is_convertible_core(expr const & given, expr const & expected) {
-        if (given == expected) {
-            return true;
-        } else {
-            expr const * g = &given;
-            expr const * e = &expected;
-            while (true) {
-                if (is_type(*e) && is_type(*g)) {
-                    if (m_env.is_ge(ty_level(*e), ty_level(*g)))
-                        return true;
-                }
-
-                if (is_type(*e) && *g == mk_bool_type())
-                    return true;
-
-                if (is_pi(*e) && is_pi(*g) && abst_domain(*e) == abst_domain(*g)) {
-                    g = &abst_body(*g);
-                    e = &abst_body(*e);
-                } else {
-                    return false;
-                }
-            }
-        }
-    }
-
     void set_ctx(context const & ctx) {
         if (!is_eqp(ctx, m_ctx)) {
             m_ctx = ctx;
@@ -353,39 +328,6 @@ public:
         return reify(normalize(e, value_stack(), k), k);
     }
 
-    bool is_convertible(expr const & given, expr const & expected, context const & ctx,
-                        substitution * subst, unification_constraints * uc) {
-        if (is_convertible_core(given, expected))
-            return true;
-        expr new_given    = given;
-        expr new_expected = expected;
-        if (has_metavar(new_given) || has_metavar(new_expected)) {
-            if (!subst)
-                return false;
-            new_given    = instantiate_metavars(new_given, *subst);
-            new_expected = instantiate_metavars(new_expected, *subst);
-            if (is_convertible_core(new_given, new_expected))
-                return true;
-            if (has_metavar(new_given) || has_metavar(new_expected)) {
-                // Very conservative approach, just postpone the problem.
-                // We may also try to normalize new_given and new_expected even if
-                // they contain metavariables.
-                if (uc) {
-                    uc->add(ctx, new_expected, new_given);
-                    return true;
-                } else {
-                    return false;
-                }
-            }
-        }
-        set_subst(subst);
-        set_ctx(ctx);
-        unsigned k   = m_ctx.size();
-        new_given    = reify(normalize(new_given, value_stack(), k), k);
-        new_expected = reify(normalize(new_expected, value_stack(), k), k);
-        return is_convertible_core(new_given, new_expected);
-    }
-
     void clear() { m_ctx = context(); m_cache.clear(); m_subst = nullptr; m_subst_timestamp = 0; }
     void set_interrupt(bool flag) { m_interrupted = flag; }
 };
@@ -395,20 +337,12 @@ normalizer::normalizer(environment const & env):normalizer(env, std::numeric_lim
 normalizer::normalizer(environment const & env, options const & opts):normalizer(env, get_normalizer_max_depth(opts)) {}
 normalizer::~normalizer() {}
 expr normalizer::operator()(expr const & e, context const & ctx, substitution const * subst) { return (*m_ptr)(e, ctx, subst); }
-bool normalizer::is_convertible(expr const & t1, expr const & t2, context const & ctx,
-                                substitution * subst, unification_constraints * uc) {
-    return m_ptr->is_convertible(t1, t2, ctx, subst, uc);
-}
 void normalizer::clear() { m_ptr->clear(); }
 void normalizer::set_interrupt(bool flag) { m_ptr->set_interrupt(flag); }
 
 expr normalize(expr const & e, environment const & env, context const & ctx, substitution const * subst) {
     return normalizer(env)(e, ctx, subst);
 }
-bool is_convertible(expr const & given, expr const & expected, environment const & env, context const & ctx,
-                    substitution * subst, unification_constraints * uc) {
-    return normalizer(env).is_convertible(given, expected, ctx, subst, uc);
-}
 }
 
 /*
diff --git a/src/kernel/normalizer.h b/src/kernel/normalizer.h
index f706487e0..da08e3438 100644
--- a/src/kernel/normalizer.h
+++ b/src/kernel/normalizer.h
@@ -26,8 +26,6 @@ public:
     ~normalizer();
 
     expr operator()(expr const & e, context const & ctx = context(), substitution const * subst = nullptr);
-    bool is_convertible(expr const & t1, expr const & t2, context const & ctx = context(),
-                        substitution * menv = nullptr, unification_constraints * uc = nullptr);
 
     void clear();
 
@@ -37,6 +35,4 @@ public:
 };
 /** \brief Normalize \c e using the environment \c env and context \c ctx */
 expr normalize(expr const & e, environment const & env, context const & ctx = context(), substitution const * subst = nullptr);
-bool is_convertible(expr const & t1, expr const & t2, environment const & env, context const & ctx = context(),
-                    substitution * subst = nullptr, unification_constraints * uc = nullptr);
 }
diff --git a/src/kernel/type_checker.cpp b/src/kernel/type_checker.cpp
index 3dc112a6b..e7f99a535 100644
--- a/src/kernel/type_checker.cpp
+++ b/src/kernel/type_checker.cpp
@@ -31,6 +31,9 @@ class type_checker::imp {
     unification_constraints * m_uc;
     volatile bool             m_interrupted;
 
+    expr normalize(expr const & e, context const & ctx) {
+        return m_normalizer(e, ctx, m_subst);
+    }
 
     expr lookup(context const & c, unsigned i) {
         auto p = lookup_ext(c, i);
@@ -43,7 +46,7 @@ class type_checker::imp {
     expr check_pi(expr const & e, expr const & s, context const & ctx) {
         if (is_pi(e))
             return e;
-        expr r = m_normalizer(e, ctx);
+        expr r = normalize(e, ctx);
         if (is_pi(r))
             return r;
         if (has_metavar(r) && m_subst && m_uc && m_mgen) {
@@ -64,7 +67,7 @@ class type_checker::imp {
     }
 
     level infer_universe_core(expr const & t, context const & ctx) {
-        expr u = m_normalizer(infer_type_core(t, ctx), ctx);
+        expr u = normalize(infer_type_core(t, ctx), ctx);
         if (is_type(u))
             return ty_level(u);
         if (u == Bool)
@@ -125,7 +128,7 @@ class type_checker::imp {
             while (true) {
                 expr const & c   = arg(e, i);
                 expr const & c_t = arg_types[i];
-                if (!is_convertible_core(c_t, abst_domain(f_t), ctx))
+                if (!is_convertible(c_t, abst_domain(f_t), ctx))
                     throw app_type_mismatch_exception(m_env, ctx, e, arg_types.size(), arg_types.data());
                 if (closed(abst_body(f_t)))
                     f_t = abst_body(f_t);
@@ -171,7 +174,7 @@ class type_checker::imp {
             expr lt = infer_type_core(let_value(e), ctx);
             if (let_type(e)) {
                 infer_universe_core(let_type(e), ctx); // check if it is really a type
-                if (!is_convertible_core(lt, let_type(e), ctx))
+                if (!is_convertible(lt, let_type(e), ctx))
                     throw def_type_mismatch_exception(m_env, ctx, let_name(e), let_type(e), let_value(e), lt);
             }
             {
@@ -200,8 +203,58 @@ class type_checker::imp {
         return r;
     }
 
-    bool is_convertible_core(expr const & t1, expr const & t2, context const & ctx) {
-        return m_normalizer.is_convertible(t1, t2, ctx, m_subst, m_uc);
+    bool is_convertible_core(expr const & given, expr const & expected) {
+        if (given == expected) {
+            return true;
+        } else {
+            expr const * g = &given;
+            expr const * e = &expected;
+            while (true) {
+                if (is_type(*e) && is_type(*g)) {
+                    if (m_env.is_ge(ty_level(*e), ty_level(*g)))
+                        return true;
+                }
+
+                if (is_type(*e) && *g == mk_bool_type())
+                    return true;
+
+                if (is_pi(*e) && is_pi(*g) && abst_domain(*e) == abst_domain(*g)) {
+                    g = &abst_body(*g);
+                    e = &abst_body(*e);
+                } else {
+                    return false;
+                }
+            }
+        }
+    }
+
+    bool is_convertible(expr const & given, expr const & expected, context const & ctx) {
+        if (is_convertible_core(given, expected))
+            return true;
+        expr new_given    = given;
+        expr new_expected = expected;
+        if (has_metavar(new_given) || has_metavar(new_expected)) {
+            if (!m_subst)
+                return false;
+            new_given    = instantiate_metavars(new_given, *m_subst);
+            new_expected = instantiate_metavars(new_expected, *m_subst);
+            if (is_convertible_core(new_given, new_expected))
+                return true;
+            if (has_metavar(new_given) || has_metavar(new_expected)) {
+                // Very conservative approach, just postpone the problem.
+                // We may also try to normalize new_given and new_expected even if
+                // they contain metavariables.
+                if (m_uc) {
+                    m_uc->add(ctx, new_expected, new_given);
+                    return true;
+                } else {
+                    return false;
+                }
+            }
+        }
+        new_given    = normalize(new_given, ctx);
+        new_expected = normalize(new_expected, ctx);
+        return is_convertible_core(new_given, new_expected);
     }
 
     void set_ctx(context const & ctx) {
@@ -256,7 +309,7 @@ public:
         set_ctx(ctx);
         set_subst(subst);
         flet<unification_constraints*> set_uc(m_uc, uc);
-        return is_convertible_core(t1, t2, ctx);
+        return is_convertible(t1, t2, ctx);
     }
 
     void set_interrupt(bool flag) {
@@ -295,4 +348,8 @@ normalizer & type_checker::get_normalizer() { return m_ptr->get_normalizer(); }
 expr  infer_type(expr const & e, environment const & env, context const & ctx) {
     return type_checker(env).infer_type(e, ctx);
 }
+bool is_convertible(expr const & given, expr const & expected, environment const & env, context const & ctx,
+                    substitution * subst, unification_constraints * uc) {
+    return type_checker(env).is_convertible(given, expected, ctx, subst, uc);
+}
 }
diff --git a/src/kernel/type_checker.h b/src/kernel/type_checker.h
index 7b0eeec96..9c08c8a1f 100644
--- a/src/kernel/type_checker.h
+++ b/src/kernel/type_checker.h
@@ -62,4 +62,6 @@ public:
 };
 
 expr infer_type(expr const & e, environment const & env, context const & ctx = context());
+bool is_convertible(expr const & t1, expr const & t2, environment const & env, context const & ctx = context(),
+                    substitution * subst = nullptr, unification_constraints * uc = nullptr);
 }