From 3c6002e96904e153c44f41fbb52f54bbb30ff113 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 22 Feb 2014 11:44:57 -0800 Subject: [PATCH] refactor(kernel): add mk_rev_app, update_rev_app, implement instantiate_metavars functions, modify instantiate (free vars) API Signed-off-by: Leonardo de Moura --- src/kernel/expr.cpp | 39 ++++++++++++++-- src/kernel/expr.h | 6 +++ src/kernel/instantiate.cpp | 22 +++------ src/kernel/instantiate.h | 4 +- src/kernel/metavar.cpp | 91 ++++++++++++++++++++++++++++++++++++++ src/kernel/metavar.h | 1 + 6 files changed, 140 insertions(+), 23 deletions(-) diff --git a/src/kernel/expr.cpp b/src/kernel/expr.cpp index e30f6f5505..1aec509baa 100644 --- a/src/kernel/expr.cpp +++ b/src/kernel/expr.cpp @@ -265,14 +265,33 @@ void expr_cell::dealloc() { } // Auxiliary constructors -expr mk_app(unsigned num_args, expr const * args) { - lean_assert(num_args >= 2); - expr r = mk_app(args[0], args[1]); - for (unsigned i = 2; i < num_args; i++) +expr mk_app(expr const & f, unsigned num_args, expr const * args) { + expr r = f; + for (unsigned i = 0; i < num_args; i++) r = mk_app(r, args[i]); return r; } +expr mk_app(unsigned num_args, expr const * args) { + lean_assert(num_args >= 2); + return mk_app(mk_app(args[0], args[1]), num_args - 2, args+2); +} + +expr mk_rev_app(expr const & f, unsigned num_args, expr const * args) { + expr r = f; + unsigned i = num_args; + while (i > 0) { + --i; + r = mk_app(r, args[i]); + } + return r; +} + +expr mk_rev_app(unsigned num_args, expr const * args) { + lean_assert(num_args >= 2); + return mk_rev_app(mk_app(args[num_args-1], args[num_args-2]), num_args-2, args); +} + 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); } @@ -305,6 +324,18 @@ expr update_app(expr const & e, expr const & new_fn, expr const & new_arg) { return e; } +expr update_rev_app(expr const & e, unsigned num, expr const * new_args) { + expr const * it = &e; + for (unsigned i = 0; i < num - 1; i++) { + if (!is_app(*it) || !is_eqp(app_arg(*it), new_args[i])) + return mk_rev_app(num, new_args); + it = &app_fn(*it); + } + if (!is_eqp(*it, new_args[num - 1])) + return mk_rev_app(num, new_args); + return e; +} + expr update_proj(expr const & e, expr const & new_arg) { if (!is_eqp(proj_arg(e), new_arg)) return mk_proj(is_fst(e), new_arg); diff --git a/src/kernel/expr.h b/src/kernel/expr.h index af87ddc4d2..6c5daf3b9c 100644 --- a/src/kernel/expr.h +++ b/src/kernel/expr.h @@ -384,9 +384,13 @@ inline expr mk_proj(bool first, expr const & a) { return expr(new expr_proj(firs inline expr mk_fst(expr const & a) { return mk_proj(true, a); } inline expr mk_snd(expr const & a) { return mk_proj(false, a); } inline expr mk_app(expr const & f, expr const & a) { return expr(new expr_app(f, a)); } + expr mk_app(expr const & f, unsigned num_args, expr const * args); expr mk_app(unsigned num_args, expr const * args); inline expr mk_app(std::initializer_list const & l) { return mk_app(l.size(), l.begin()); } template expr mk_app(T const & args) { return mk_app(args.size(), args.data()); } + expr mk_rev_app(expr const & f, unsigned num_args, expr const * args); + expr mk_rev_app(unsigned num_args, expr const * args); +template expr mk_rev_app(T const & args) { return mk_rev_app(args.size(), args.data()); } inline expr mk_binder(expr_kind k, name const & n, expr const & t, expr const & e) { return expr(new expr_binder(k, n, t, e)); } inline expr mk_lambda(name const & n, expr const & t, expr const & e) { return mk_binder(expr_kind::Lambda, n, t, e); } inline expr mk_pi(name const & n, expr const & t, expr const & e) { return mk_binder(expr_kind::Pi, n, t, e); } @@ -560,6 +564,8 @@ expr copy(expr const & e); // ======================================= // Update expr update_app(expr const & e, expr const & new_fn, expr const & new_arg); +expr update_rev_app(expr const & e, unsigned num, expr const * new_args); +template expr update_rev_app(expr const & e, C const & c) { return update_rev_app(e, c.size(), c.data()); } expr update_proj(expr const & e, expr const & new_arg); expr update_pair(expr const & e, expr const & new_first, expr const & new_second, expr const & new_type); expr update_binder(expr const & e, expr const & new_domain, expr const & new_body); diff --git a/src/kernel/instantiate.cpp b/src/kernel/instantiate.cpp index 6918e60bff..63b48dbd52 100644 --- a/src/kernel/instantiate.cpp +++ b/src/kernel/instantiate.cpp @@ -19,9 +19,9 @@ expr instantiate_core(expr const & a, unsigned s, unsigned n, expr const * subst if (vidx >= offset + s) { if (vidx < offset + s + n) { if (ClosedSubst) - return subst[n - (vidx - s - offset) - 1]; + return subst[vidx - s - offset]; else - return lift_free_vars(subst[n - (vidx - s - offset) - 1], offset); + return lift_free_vars(subst[vidx - s - offset], offset); } else { return mk_var(vidx - n); } @@ -60,11 +60,9 @@ bool is_head_beta(expr const & t) { } expr apply_beta(expr f, unsigned num_args, expr const * args) { + lean_assert(num_args > 0); if (!is_lambda(f)) { - buffer new_args; - new_args.push_back(f); - new_args.append(num_args, args); - return mk_app(new_args); + return mk_rev_app(f, num_args, args); } else { unsigned m = 1; while (is_lambda(binder_body(f)) && m < num_args) { @@ -72,16 +70,7 @@ expr apply_beta(expr f, unsigned num_args, expr const * args) { m++; } lean_assert(m <= num_args); - expr r = instantiate(binder_body(f), m, args); - if (m == num_args) { - return r; - } else { - buffer new_args; - new_args.push_back(r); - for (; m < num_args; m++) - new_args.push_back(args[m]); - return mk_app(new_args); - } + return mk_rev_app(instantiate(binder_body(f), m, args + (num_args - m)), num_args - m, args); } } @@ -96,7 +85,6 @@ expr head_beta_reduce(expr const & t) { expr const & f = app_fn(*it); args.push_back(app_arg(*it)); if (is_lambda(f)) { - std::reverse(args.begin(), args.end()); return apply_beta(f, args.size(), args.data()); } else { lean_assert(is_app(f)); diff --git a/src/kernel/instantiate.h b/src/kernel/instantiate.h index af5903f7fc..189eb0e4e2 100644 --- a/src/kernel/instantiate.h +++ b/src/kernel/instantiate.h @@ -10,7 +10,7 @@ Author: Leonardo de Moura namespace lean { class ro_metavar_env; /** - \brief Replace the free variables with indices 0, ..., n-1 with s[n-1], ..., s[0] in e. + \brief Replace the free variables with indices 0, ..., n-1 with s[0], ..., s[n-1] in e. \pre s[0], ..., s[n-1] must be closed expressions (i.e., no free variables). */ @@ -18,7 +18,7 @@ expr instantiate_with_closed(expr const & e, unsigned n, expr const * s); expr instantiate_with_closed(expr const & e, std::initializer_list const & l); expr instantiate_with_closed(expr const & e, expr const & s); -/** \brief Replace the free variables with indices 0, ..., n-1 with s[n-1], ..., s[0] in e. */ +/** \brief Replace the free variables with indices 0, ..., n-1 with s[0], ..., s[n-1] in e. */ expr instantiate(expr const & e, unsigned n, expr const * s); expr instantiate(expr const & e, std::initializer_list const & l); /** \brief Replace free variable \c i with \c s in \c e. */ diff --git a/src/kernel/metavar.cpp b/src/kernel/metavar.cpp index c675ea90f3..1c057d41d5 100644 --- a/src/kernel/metavar.cpp +++ b/src/kernel/metavar.cpp @@ -6,6 +6,10 @@ Author: Leonardo de Moura */ #include #include "kernel/metavar.h" +#include "kernel/free_vars.h" +#include "kernel/replace_visitor.h" +#include "kernel/justification.h" +#include "kernel/instantiate.h" namespace lean { bool substitution::is_assigned(name const & m) const { @@ -29,6 +33,7 @@ optional substitution::get_expr(name const & m) const { } void substitution::assign(name const & m, expr const & t, justification const & j) { + lean_assert(closed(t)); m_subst.insert(m, mk_pair(t, j)); } @@ -41,4 +46,90 @@ void substitution::for_each(std::functionfirst)) { + if (m_use_jst) + save_jst(p1->second); + return p1->first; + } else if (m_use_jst) { + if (m_update) { + auto p2 = d_instantiate_metavars(p1->first, m_subst); + justification new_jst = mk_composite1(p1->second, p2.second); + m_subst.assign(m_name, p2.first, new_jst); + save_jst(new_jst); + return p2.first; + } else { + auto p2 = instantiate_metavars(p1->first, m_subst); + save_jst(mk_composite1(p1->second, p2.second)); + return p2.first; + } + } else { + if (m_update) { + expr r = d_instantiate_metavars_wo_jst(p1->first, m_subst); + m_subst.assign(m_name, r); + return r; + } else { + return instantiate_metavars_wo_jst(p1->first, m_subst); + } + } + } else { + return m; + } + } + + virtual expr visit_app(expr const & e, context const & ctx) { + buffer args; + expr const * it = &e; + while (is_app(*it)) { + args.push_back(visit(app_arg(*it), ctx)); + it = &app_fn(*it); + } + expr const & f = *it; + if (is_metavar(f) && m_subst.is_assigned(mlocal_name(f))) { + expr new_f = visit_meta(f, ctx); + return apply_beta(new_f, args.size(), args.data()); + } else { + args.push_back(visit(f, ctx)); + return update_rev_app(e, args); + } + } + +public: + instantiate_metavars_fn(substitution & s, bool use_jst, bool updt): + m_subst(s), m_use_jst(use_jst), m_update(updt) {} + justification const & get_justification() const { return m_jst; } +}; + +std::pair instantiate_metavars(expr const & e, substitution const & s) { + instantiate_metavars_fn fn(const_cast(s), true, false); + expr r = fn(e); + return mk_pair(r, fn.get_justification()); +} + +std::pair d_instantiate_metavars(expr const & e, substitution & s) { + instantiate_metavars_fn fn(s, true, true); + expr r = fn(e); + return mk_pair(r, fn.get_justification()); +} + +expr instantiate_metavars_wo_jst(expr const & e, substitution const & s) { + return instantiate_metavars_fn(const_cast(s), false, false)(e); +} + +expr d_instantiate_metavars_wo_jst(expr const & e, substitution & s) { + return instantiate_metavars_fn(s, false, true)(e); +} } diff --git a/src/kernel/metavar.h b/src/kernel/metavar.h index 62cd551384..f75431a619 100644 --- a/src/kernel/metavar.h +++ b/src/kernel/metavar.h @@ -37,4 +37,5 @@ std::pair d_instantiate_metavars(expr const & e, substituti but does not return a justification object for the new expression. */ expr instantiate_metavars_wo_jst(expr const & e, substitution const & s); +expr d_instantiate_metavars_wo_jst(expr const & e, substitution & s); }