From b2518f873d55b4f051a91da940e4f1940193bb6d Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 25 Apr 2014 18:17:32 -0700 Subject: [PATCH] feat(kernel/type_checker): handle ensure_pi when whnf is a meta application Signed-off-by: Leonardo de Moura --- src/kernel/expr.cpp | 16 +++++++ src/kernel/expr.h | 10 ++++- src/kernel/type_checker.cpp | 84 +++++++++++++++++++++++++++++++++++-- 3 files changed, 106 insertions(+), 4 deletions(-) diff --git a/src/kernel/expr.cpp b/src/kernel/expr.cpp index f77f9e859..8e17bad6b 100644 --- a/src/kernel/expr.cpp +++ b/src/kernel/expr.cpp @@ -313,6 +313,22 @@ expr mk_rev_app(unsigned num_args, expr const * args) { return mk_rev_app(mk_app(args[num_args-1], args[num_args-2]), num_args-2, args); } +expr mk_app_vars(expr const & f, unsigned n) { + expr r = f; + while (n > 0) { + --n; + r = mk_app(r, Var(n)); + } + return r; +} + +void get_app_args(expr const & e, buffer & args) { + if (is_app(e)) { + get_app_args(app_fn(e), args); + args.push_back(app_arg(e)); + } +} + 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); } diff --git a/src/kernel/expr.h b/src/kernel/expr.h index cdd314c1c..ee4cf686c 100644 --- a/src/kernel/expr.h +++ b/src/kernel/expr.h @@ -264,7 +264,7 @@ public: virtual expr get_type(unsigned num, expr const * args, expr const * arg_types, extension_context const & ctx) const = 0; virtual optional expand1(unsigned num, expr const * args, extension_context const & ctx) const = 0; virtual optional expand(unsigned num, expr const * args, extension_context const & ctx) const = 0; - virtual unsigned trust_level() const = 0; + virtual unsigned trust_level() const { return 0; } virtual int push_lua(lua_State * L) const; virtual bool operator==(macro_definition const & other) const; bool operator!=(macro_definition const & other) const { return !operator==(other); } @@ -396,6 +396,9 @@ inline expr expr::operator()(expr const & a1, expr const & a2, expr const & a3, expr const & a6, expr const & a7, expr const & a8) const { return mk_app({*this, a1, a2, a3, a4, a5, a6, a7, a8}); } + +/** \brief Return application (...((f x_{n-1}) x_{n-2}) ... x_0) */ +expr mk_app_vars(expr const & f, unsigned n); // ======================================= // ======================================= @@ -488,6 +491,11 @@ inline bool has_free_vars(expr const & e) { return get_free_var_range(e) > 0; } inline bool closed(expr const & e) { return !has_free_vars(e); } /** \brief Return true iff \c e contains a free variable >= low. */ inline bool has_free_var_ge(expr const & e, unsigned low) { return get_free_var_range(e) > low; } +/** + \brief Given \c e of the form (...(f a1) ... an), store a1 ... an in args. + If \c e is not an application, then nothing is stored in args. +*/ +void get_app_args(expr const & e, buffer & args); // ======================================= diff --git a/src/kernel/type_checker.cpp b/src/kernel/type_checker.cpp index 11014b790..fbe23f0a8 100644 --- a/src/kernel/type_checker.cpp +++ b/src/kernel/type_checker.cpp @@ -17,9 +17,10 @@ Author: Leonardo de Moura #include "kernel/error_msgs.h" #include "kernel/kernel_exception.h" #include "kernel/abstract.h" +#include "kernel/replace_fn.h" namespace lean { - +static name g_x_name("x"); /** \brief Auxiliary functional object used to implement type checker. */ struct type_checker::imp { environment m_env; @@ -56,7 +57,10 @@ struct type_checker::imp { expr max_sharing(expr const & e) { return m_memoize ? m_sharing(e) : e; } expr instantiate(expr const & e, unsigned n, expr const * s) { return max_sharing(lean::instantiate(e, n, s)); } expr instantiate(expr const & e, expr const & s) { return max_sharing(lean::instantiate(e, s)); } + expr mk_app(expr const & f, unsigned num, expr const * args) { return max_sharing(lean::mk_app(f, num, args)); } + expr mk_app(expr const & f, expr const & a) { return max_sharing(lean::mk_app(f, a)); } expr mk_rev_app(expr const & f, unsigned num, expr const * args) { return max_sharing(lean::mk_rev_app(f, num, args)); } + expr mk_app_vars(expr const & f, unsigned num) { return max_sharing(lean::mk_app_vars(f, num)); } optional expand_macro(expr const & m) { lean_assert(is_macro(m)); type_checker_context ctx(*this); @@ -521,6 +525,50 @@ struct type_checker::imp { return whnf(infer_type(e)) == Bool; } + /** + \brief Given a metavariable application ((?m t_1) ... t_k) + Create a telescope with the types of t_1 ... t_k. + If t_i is a local constant, then we abstract the occurrences of t_i in the types of t_{i+1} ... t_k. + Return false if the telescope still contains local constants after the abstraction step. + */ + bool meta_to_telescope(expr const & e, buffer & telescope) { + lean_assert(is_meta(e)); + lean_assert(closed(e)); + buffer> locals; + return meta_to_telescope_core(e, telescope, locals); + } + + /** + \brief Auxiliary method for meta_to_telescope + */ + bool meta_to_telescope_core(expr const & e, buffer & telescope, buffer> & locals) { + lean_assert(is_meta(e)); + if (is_app(e)) { + if (!meta_to_telescope_core(app_fn(e), telescope, locals)) + return false; + // infer type and abstract local constants + unsigned n = locals.size(); + expr t = replace(infer_type(app_arg(e)), + [&](expr const & e, unsigned offset) -> optional { + if (is_local(e)) { + for (unsigned i = 0; i < n; i++) { + if (locals[i] && is_eqp(*locals[i], e)) + return some_expr(mk_var(offset + n - i - 1)); + } + } + return none_expr(); + }); + if (has_local(t)) + return false; + telescope.push_back(t); + if (is_local(e)) + locals.push_back(some_expr(e)); + else + locals.push_back(none_expr()); + } + return true; + } + /** \brief Make sure \c e "is" a sort, and return the corresponding sort. If \c e is not a sort, then the whnf procedure is invoked. Then, there are @@ -550,6 +598,16 @@ struct type_checker::imp { } } + expr mk_tele_pi(buffer 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)) @@ -558,8 +616,28 @@ struct type_checker::imp { if (is_pi(e)) { return e; } else if (is_meta(e)) { - // TODO(Leo) - return e; + buffer telescope; + if (!meta_to_telescope(e, telescope)) + throw_kernel_exception(m_env, trace_back(s), + [=](formatter const & fmt, options const & o) { return pp_function_expected(fmt, 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_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)); + buffer args; + get_app_args(e, args); + expr A_args = mk_app(A, args.size(), args.data()); + args.push_back(Var(0)); + expr B_args = mk_app(B, args.size(), args.data()); + expr r = mk_pi(g_x_name, A, B); + justification j = mk_justification(trace_back(s), + [=](formatter const & fmt, options const & o, substitution const & subst) { + return pp_function_expected(fmt, o, subst.instantiate_metavars_wo_jst(s)); + }); + add_cnstr(mk_eq_cnstr(e, r, j)); + return r; } else { throw_kernel_exception(m_env, trace_back(s), [=](formatter const & fmt, options const & o) { return pp_function_expected(fmt, o, s); });