refactor(kernel): move mk_tele_pi to expr.h, and rename it mk_pi

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-05-14 16:24:55 -07:00
parent 9c5dfc387b
commit 5d61d23bf6
3 changed files with 16 additions and 12 deletions

View file

@ -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; }

View file

@ -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;

View file

@ -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());