From 9bc2fe04d2543770ad13503cd16feccba6203aae Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 15 Mar 2016 13:31:08 -0700 Subject: [PATCH] dev(library/type_context): add mk_lambda and mk_pi for type_context --- src/library/type_context.cpp | 90 +++++++++++++++++++++++++++--------- src/library/type_context.h | 9 +++- 2 files changed, 77 insertions(+), 22 deletions(-) diff --git a/src/library/type_context.cpp b/src/library/type_context.cpp index 1d70936200..06fed1a4c2 100644 --- a/src/library/type_context.cpp +++ b/src/library/type_context.cpp @@ -7,6 +7,7 @@ Author: Leonardo de Moura #include "util/flet.h" #include "util/interrupt.h" #include "kernel/instantiate.h" +#include "kernel/abstract.h" #include "kernel/replace_fn.h" #include "kernel/for_each_fn.h" #include "library/idx_metavar.h" @@ -180,11 +181,22 @@ pair type_context::revert_core(unsigned num, expr const * l return mk_pair(new_ctx, mk_pi(reverted, type)); } -/* -expr type_context::revert(unsigned num, expr const * locals, metavar_decl const & mdecl, buffer & reverted) { - +expr type_context::revert_core(unsigned num, expr const * locals, expr const & mvar, buffer & reverted) { + lean_assert(is_metavar_decl_ref(mvar)); + metavar_decl const & d = *m_mctx.get_metavar_decl(mvar); + auto p = revert_core(num, locals, d.get_context(), d.get_type(), reverted); + return m_mctx.mk_metavar_decl(p.first, p.second); +} + +expr type_context::revert(unsigned num, expr const * locals, expr const & mvar) { + lean_assert(is_metavar_decl_ref(mvar)); + lean_assert(std::all_of(locals, locals+num, [&](expr const & l) { return mvar.get_context().contains(l); })); + buffer reverted; + expr new_mvar = revert_core(num, locals, mvar, reverted); + expr r = mk_app(new_mvar, reverted); + m_mctx.assign(mvar, r); + return r; } -*/ /* Make sure that for any (unassigned) metavariable ?M@C occurring in \c e, \c C does not contain any local in \c locals. This can be achieved by creating new metavariables @@ -195,10 +207,11 @@ void type_context::restrict_metavars_context(expr const & e, unsigned num_locals for_each(e, [&](expr const & e, unsigned) { if (!has_expr_metavar(e)) return false; if (is_metavar_decl_ref(e)) { + metavar_decl const & decl = *m_mctx.get_metavar_decl(e); + restrict_metavars_context(decl.get_type(), num_locals, locals); if (optional v = m_mctx.get_assignment(e)) { restrict_metavars_context(*v, num_locals, locals); } else { - metavar_decl const & decl = *m_mctx.get_metavar_decl(e); local_context const & ctx = decl.get_context(); buffer to_revert; for (unsigned i = 0; i < num_locals; i++) { @@ -206,7 +219,8 @@ void type_context::restrict_metavars_context(expr const & e, unsigned num_locals to_revert.push_back(locals[i]); } if (!to_revert.empty()) { - + revert(to_revert.size(), to_revert.data(), e); + lean_assert(m_mctx.is_assigned(e)); } } } @@ -221,25 +235,60 @@ void type_context::restrict_metavars_context(local_decl const & d, unsigned num_ } expr type_context::abstract_locals(expr const & e, unsigned num_locals, expr const * locals) { - for (unsigned i = 0; i < num_locals; i++) { - expr const & local = locals[i]; + lean_assert(std::all_of(locals, locals+num_locals, is_local_decl_ref)); + if (num_locals == 0) + return e; + if (!m_tmp_mode) { + /* In regular mode, we have to make sure the context of the metavariables occurring \c e + does not include the locals being abstracted. + Claim: this check is not necessary in tmp_mode because + 1- Regular metavariables should not depend on temporary local constants that have been created in tmp mode. + 2- The tmp metavariables all share the same fixed local context. + */ + restrict_metavars_context(e, num_locals, locals); } - - // TODO(Leo) - return e; + return ::lean::abstract_locals(e, num_locals, locals); } -expr type_context::mk_fun(buffer const & locals, expr const & e) { - // TODO(Leo) - lean_unreachable(); +expr type_context::mk_binding(bool is_pi, unsigned num_locals, expr const * locals, expr const & e) { + buffer decls; + buffer types; + buffer> values; + for (unsigned i = 0; i < num_locals; i++) { + local_decl const & decl = *m_lctx.get_local_decl(locals[i]); + decls.push_back(decl); + types.push_back(abstract_locals(decl.get_type(), i, locals)); + if (auto v = decl.get_value()) + values.push_back(some_expr(abstract_locals(*v, i, locals))); + else + values.push_back(none_expr()); + } + expr new_e = abstract_locals(e, num_locals, locals); + lean_assert(types.size() == values.size()); + unsigned i = types.size(); + while (i > 0) { + --i; + if (values[i]) { + new_e = mk_let(decls[i].get_pp_name(), types[i], *values[i], new_e); + } else if (is_pi) { + new_e = ::lean::mk_pi(decls[i].get_pp_name(), types[i], new_e, decls[i].get_info()); + } else { + new_e = ::lean::mk_lambda(decls[i].get_pp_name(), types[i], new_e, decls[i].get_info()); + } + } + return new_e; +} + +expr type_context::mk_lambda(buffer const & locals, expr const & e) { + return mk_binding(false, locals.size(), locals.data(), e); } expr type_context::mk_pi(buffer const & locals, expr const & e) { - // TODO(Leo) - lean_unreachable(); + return mk_binding(true, locals.size(), locals.data(), e); } + /* --------------------- Normalization -------------------- */ @@ -1101,7 +1150,7 @@ bool type_context::process_assignment(expr const & m, expr const & v) { if (args.empty()) { /* easy case */ } else if (args.size() == locals.size()) { - new_v = mk_fun(locals, new_v); + new_v = mk_lambda(locals, new_v); } else { /* This case is imprecise since it is not a higher order pattern. @@ -1123,7 +1172,7 @@ bool type_context::process_assignment(expr const & m, expr const & v) { mvar_type = ::lean::instantiate(binding_body(mvar_type), locals[i]); } lean_assert(locals.size() == args.size()); - new_v = mk_fun(locals, new_v); + new_v = mk_lambda(locals, new_v); } /* check types */ @@ -1195,8 +1244,8 @@ bool type_context::is_def_eq_eta(expr const & e1, expr const & e2) { if (is_pi(e2_type)) { // e2_type may not be a Pi because it is a stuck term. // We are ignoring this case and just failing. - expr new_e2 = mk_lambda(binding_name(e2_type), binding_domain(e2_type), - mk_app(e2, Var(0)), binding_info(e2_type)); + expr new_e2 = ::lean::mk_lambda(binding_name(e2_type), binding_domain(e2_type), + mk_app(e2, Var(0)), binding_info(e2_type)); scope s(*this); if (is_def_eq_core(e1, new_e2)) { s.commit(); @@ -1222,7 +1271,6 @@ bool type_context::is_def_eq_proof_irrel(expr const & e1, expr const & e2) { return false; } - /* struct unification_hint_fn { type_context & m_owner; diff --git a/src/library/type_context.h b/src/library/type_context.h index 62df840a77..05c4896ae3 100644 --- a/src/library/type_context.h +++ b/src/library/type_context.h @@ -164,7 +164,12 @@ public: virtual void pop_local() override; virtual expr abstract_locals(expr const & e, unsigned num_locals, expr const * locals) override; - expr mk_fun(buffer const & locals, expr const & e); + /** Given a metavariable \c mvar, and local constants in \c locals, return (mvar' C) where + C is a superset of \c locals and includes all local constants that depend on \c locals. + \pre all local constants in \c locals are in metavariable context. */ + expr revert(unsigned num, expr const * locals, expr const & mvar); + + expr mk_lambda(buffer const & locals, expr const & e); expr mk_pi(buffer const & locals, expr const & e); /* Add a let-decl (aka local definition) to the local context */ @@ -218,8 +223,10 @@ private: private: pair revert_core(unsigned num, expr const * locals, local_context const & ctx, expr const & type, buffer & reverted); + expr revert_core(unsigned num, expr const * locals, expr const & mvar, buffer & reverted); void restrict_metavars_context(expr const & e, unsigned num_locals, expr const * locals); void restrict_metavars_context(local_decl const & d, unsigned num_locals, expr const * locals); + expr mk_binding(bool is_pi, unsigned num_locals, expr const * locals, expr const & e); /* ------------ Temporary metavariable assignment.