From 75d06ebc347b12b71ea19a051b0117f729d314e8 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 27 Jul 2016 14:57:39 -0700 Subject: [PATCH] feat(library/type_context): use delayed abstraction at type_context (instead of restrict_metavars_context) --- src/library/delayed_abstraction.cpp | 14 ++++++++ src/library/delayed_abstraction.h | 5 +++ src/library/type_context.cpp | 54 +++++------------------------ src/library/type_context.h | 2 -- 4 files changed, 27 insertions(+), 48 deletions(-) diff --git a/src/library/delayed_abstraction.cpp b/src/library/delayed_abstraction.cpp index e458e4b681..950c310685 100644 --- a/src/library/delayed_abstraction.cpp +++ b/src/library/delayed_abstraction.cpp @@ -5,6 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ #include "kernel/free_vars.h" +#include "kernel/abstract.h" #include "kernel/abstract_type_context.h" #include "library/replace_visitor.h" @@ -239,6 +240,19 @@ expr mk_delayed_abstraction(expr const & e, buffer const & ns, buffer ns; + buffer vs; + for (unsigned i = 0; i < nlocals; i++) { + ns.push_back(mlocal_name(locals[i])); + vs.push_back(mk_var(nlocals - i - 1)); + } + return push_delayed_abstraction_fn(ns, vs)(e); +} + void initialize_delayed_abstraction() { g_delayed_abstraction_macro = new name("delayed_abstraction"); } diff --git a/src/library/delayed_abstraction.h b/src/library/delayed_abstraction.h index 3d07a7f530..4ded7b0448 100644 --- a/src/library/delayed_abstraction.h +++ b/src/library/delayed_abstraction.h @@ -27,6 +27,11 @@ expr mk_delayed_abstraction_with_locals(expr const & e, buffer const & ls) \pre !ns.empty() */ expr mk_delayed_abstraction(expr const & e, buffer const & ns, buffer const & vs); +/* Similar to abstract_locals, but create a delayed_abstraction macro around metavariables + occurring in \c e. */ +expr delayed_abstract_locals(expr const & e, unsigned nlocals, expr const * locals); +inline expr delayed_abstract_local(expr const & e, expr const & s) { return delayed_abstract_locals(e, 1, &s); } + void initialize_delayed_abstraction(); void finalize_delayed_abstraction(); } diff --git a/src/library/type_context.cpp b/src/library/type_context.cpp index 26c37fc23b..c00465697d 100644 --- a/src/library/type_context.cpp +++ b/src/library/type_context.cpp @@ -281,57 +281,19 @@ expr type_context::revert(buffer & to_revert, expr const & mvar) { 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 - ?M'@C' where C' is C without any locals (and its dependencies) */ -void type_context::restrict_metavars_context(expr const & e, unsigned num_locals, expr const * locals) { - if (!has_expr_metavar(e)) - return; - 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 { - local_context const & ctx = decl.get_context(); - buffer to_revert; - for (unsigned i = 0; i < num_locals; i++) { - if (ctx.get_local_decl(locals[i])) - to_revert.push_back(locals[i]); - } - if (!to_revert.empty()) { - revert(to_revert, e); - lean_assert(m_mctx.is_assigned(e)); - } - } - } - return true; - }); -} - -void type_context::restrict_metavars_context(local_decl const & d, unsigned num_locals, expr const * locals) { - restrict_metavars_context(d.get_type(), num_locals, locals); - if (auto v = d.get_value()) - restrict_metavars_context(*v, num_locals, locals); -} - +/* We use delayed_abstract_locals to make sure the variables being abstracted + will be abstracted correctly when any unassigned metavar ?M occurring in \c e gets instantiated. */ expr type_context::abstract_locals(expr const & e, unsigned num_locals, expr const * locals) { lean_assert(std::all_of(locals, locals+num_locals, is_local_decl_ref)); if (num_locals == 0) return e; - if (!in_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); + if (in_tmp_mode()) { + /* 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. */ + return ::lean::abstract_locals(e, num_locals, locals); } - return ::lean::abstract_locals(e, num_locals, locals); + expr new_e = instantiate_mvars(e); + return delayed_abstract_locals(new_e, num_locals, locals); } expr type_context::mk_binding(bool is_pi, unsigned num_locals, expr const * locals, expr const & e) { diff --git a/src/library/type_context.h b/src/library/type_context.h index 1de513fb64..564e9292ea 100644 --- a/src/library/type_context.h +++ b/src/library/type_context.h @@ -357,8 +357,6 @@ private: pair revert_core(buffer & to_revert, local_context const & ctx, expr const & type); expr revert_core(buffer & to_revert, expr const & mvar); - 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); /* ------------