From 5d61d23bf66fd5d7e89841833712a02722ab569c Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 14 May 2014 16:24:55 -0700
Subject: [PATCH] refactor(kernel): move mk_tele_pi to expr.h, and rename it
 mk_pi

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/kernel/expr.cpp         | 10 ++++++++++
 src/kernel/expr.h           |  4 ++++
 src/kernel/type_checker.cpp | 14 ++------------
 3 files changed, 16 insertions(+), 12 deletions(-)

diff --git a/src/kernel/expr.cpp b/src/kernel/expr.cpp
index 2ac8b2fef..0645516e5 100644
--- a/src/kernel/expr.cpp
+++ b/src/kernel/expr.cpp
@@ -346,6 +346,16 @@ static name g_default_var_name("a");
 bool is_default_var_name(name const & n) { return n == g_default_var_name; }
 expr mk_arrow(expr const & t, expr const & e) { return mk_pi(g_default_var_name, t, e); }
 
+expr mk_pi(unsigned sz, expr const * domain, expr const & range) {
+    expr r = range;
+    unsigned i = sz;
+    while (i > 0) {
+        --i;
+        r = mk_pi(name(g_default_var_name, i), domain[i], r);
+    }
+    return r;
+}
+
 expr Bool = mk_sort(mk_level_zero());
 expr Type = mk_sort(mk_level_one());
 expr mk_Bool() { return Bool; }
diff --git a/src/kernel/expr.h b/src/kernel/expr.h
index ce50fb7b6..7de639ee1 100644
--- a/src/kernel/expr.h
+++ b/src/kernel/expr.h
@@ -425,6 +425,10 @@ inline expr mk_pi(name const & n, expr const & t, expr const & e, expr_binder_in
 inline expr mk_let(name const & n, expr const & t, expr const & v, expr const & e) { return expr(new expr_let(n, t, v, e)); }
 inline expr mk_sort(level const & l) { return expr(new expr_sort(l)); }
 
+/** \brief Return <tt>Pi(x.{sz-1}, domain[sz-1], ..., Pi(x.{0}, domain[0], range)...)</tt> */
+expr mk_pi(unsigned sz, expr const * domain, expr const & range);
+inline expr mk_pi(buffer<expr> const & domain, expr const & range) { return mk_pi(domain.size(), domain.data(), range); }
+
 expr mk_Bool();
 expr mk_Type();
 extern expr Type;
diff --git a/src/kernel/type_checker.cpp b/src/kernel/type_checker.cpp
index b84b5142e..3c37faa07 100644
--- a/src/kernel/type_checker.cpp
+++ b/src/kernel/type_checker.cpp
@@ -176,16 +176,6 @@ struct type_checker::imp {
         }
     }
 
-    expr mk_tele_pi(buffer<expr> const & telescope, expr const & range) {
-        expr r = range;
-        unsigned i = telescope.size();
-        while (i > 0) {
-            --i;
-            r = mk_pi(name(g_x_name, i), telescope[i], r);
-        }
-        return r;
-    }
-
     /** \brief Similar to \c ensure_sort, but makes sure \c e "is" a Pi. */
     expr ensure_pi(expr e, expr const & s) {
         if (is_pi(e))
@@ -199,11 +189,11 @@ struct type_checker::imp {
                 throw_kernel_exception(m_env, s,
                                        [=](formatter const & fmt, options const & o) { return pp_function_expected(fmt, m_env, o, s); });
             expr ta    = mk_sort(mk_meta_univ(m_gen.next()));
-            expr A     = mk_metavar(m_gen.next(), mk_tele_pi(telescope, ta));
+            expr A     = mk_metavar(m_gen.next(), mk_pi(telescope, ta));
             expr A_xs  = mk_app_vars(A, telescope.size());
             telescope.push_back(A_xs);
             expr tb    = mk_sort(mk_meta_univ(m_gen.next()));
-            expr B     = mk_metavar(m_gen.next(), mk_tele_pi(telescope, tb));
+            expr B     = mk_metavar(m_gen.next(), mk_pi(telescope, tb));
             buffer<expr> args;
             get_app_args(e, args);
             expr A_args = mk_app(A, args.size(), args.data());