michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

refactor(kernel): add mk_rev_app, update_rev_app, implement instantiate_metavars functions, modify instantiate (free vars) API

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-02-22 11:44:57 -08:00
parent 42e253c962
commit 3c6002e969
6 changed files with 140 additions and 23 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

39
src/kernel/expr.cpp
View file

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

6
src/kernel/expr.h
View file

@ -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<expr> const & l) { return mk_app(l.size(), l.begin()); }
template<typename T> 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<typename T> 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<typename C> 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);

22
src/kernel/instantiate.cpp
View file

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

4
src/kernel/instantiate.h
View file

@ -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<expr> 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<expr> const & l);
/** \brief Replace free variable \c i with \c s in \c e. */

91
src/kernel/metavar.cpp
View file

@ -6,6 +6,10 @@ Author: Leonardo de Moura
*/
#include <utility>
#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<expr> 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::function<void(name const & n, expr const & e, j
fn(n, a.first, a.second);
});
}
class instantiate_metavars_fn : public replace_visitor {
protected:
substitution & m_subst;
justification m_jst;
bool m_use_jst;
bool m_update;
void save_jst(justification const & j) { m_jst = mk_composite1(m_jst, j); }
virtual expr visit_meta(expr const & m, context const &) {
name const & m_name = mlocal_name(m);
auto p1 = m_subst.get_assignment(m_name);
if (p1) {
if (!has_metavar(p1->first)) {
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<expr> 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<expr, justification> instantiate_metavars(expr const & e, substitution const & s) {
instantiate_metavars_fn fn(const_cast<substitution&>(s), true, false);
expr r = fn(e);
return mk_pair(r, fn.get_justification());
}
std::pair<expr, justification> 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<substitution&>(s), false, false)(e);
}
expr d_instantiate_metavars_wo_jst(expr const & e, substitution & s) {
return instantiate_metavars_fn(s, false, true)(e);
}
}

1
src/kernel/metavar.h
View file

@ -37,4 +37,5 @@ std::pair<expr, justification> 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);
}