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

feat(kernel/replace_fn): add template replace that captures commonly used pattern

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-12-17 18:31:59 -08:00
parent 23e518001a
commit 418623b874
7 changed files with 111 additions and 114 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

17
src/frontends/lean/pp.cpp
View file

@ -137,15 +137,14 @@ name get_unused_name(expr const & e) {
*/
expr replace_var_with_name(expr const & a, name const & n) {
expr c = mk_constant(n);
auto f = [=](expr const & m, unsigned offset) -> expr {
if (is_var(m)) {
unsigned vidx = var_idx(m);
if (vidx >= offset)
return vidx == offset ? c : mk_var(vidx - 1);
}
return m;
};
return replace_fn<decltype(f)>(f)(a);
return replace(a, [=](expr const & m, unsigned offset) -> expr {
if (is_var(m)) {
unsigned vidx = var_idx(m);
if (vidx >= offset)
return vidx == offset ? c : mk_var(vidx - 1);
}
return m;
});
}
/** \brief Functional object for pretty printing expressions */

42
src/kernel/abstract.cpp
View file

@ -13,33 +13,27 @@ Author: Leonardo de Moura
namespace lean {
expr abstract(expr const & e, unsigned n, expr const * s) {
lean_assert(std::all_of(s, s+n, closed));
auto f = [=](expr const & e, unsigned offset) -> expr {
unsigned i = n;
while (i > 0) {
--i;
if (s[i] == e)
return mk_var(offset + n - i - 1);
}
return e;
};
return replace_fn<decltype(f)>(f)(e);
return replace(e, [=](expr const & e, unsigned offset) -> expr {
unsigned i = n;
while (i > 0) {
--i;
if (s[i] == e)
return mk_var(offset + n - i - 1);
}
return e;
});
}
expr abstract_p(expr const & e, unsigned n, expr const * s) {
lean_assert(std::all_of(s, s+n, closed));
auto f = [=](expr const & e, unsigned offset) -> expr {
unsigned i = n;
while (i > 0) {
--i;
if (is_eqp(s[i], e))
return mk_var(offset + n - i - 1);
}
return e;
};
return replace_fn<decltype(f)>(f)(e);
return replace(e, [=](expr const & e, unsigned offset) -> expr {
unsigned i = n;
while (i > 0) {
--i;
if (is_eqp(s[i], e))
return mk_var(offset + n - i - 1);
}
return e;
});
}
#define MkBinder(FName) \
expr FName(std::initializer_list<std::pair<expr const &, expr const &>> const & l, expr const & b) { \

36
src/kernel/free_vars.cpp
View file

@ -336,15 +336,14 @@ bool has_free_var(expr const & e, unsigned i) { return has_free_var(e, i, i+1);
expr lower_free_vars(expr const & e, unsigned s, unsigned d, optional<metavar_env> const & DEBUG_CODE(menv)) {
lean_assert(s >= d);
lean_assert(!has_free_var(e, s-d, s, menv));
auto f = [=](expr const & e, unsigned offset) -> expr {
if (is_var(e) && var_idx(e) >= s + offset) {
lean_assert(var_idx(e) >= offset + d);
return mk_var(var_idx(e) - d);
} else {
return e;
}
};
return replace_fn<decltype(f)>(f)(e);
return replace(e, [=](expr const & e, unsigned offset) -> expr {
if (is_var(e) && var_idx(e) >= s + offset) {
lean_assert(var_idx(e) >= offset + d);
return mk_var(var_idx(e) - d);
} else {
return e;
}
});
}
expr lower_free_vars(expr const & e, unsigned s, unsigned d, metavar_env const & menv) { return lower_free_vars(e, s, d, some_menv(menv)); }
expr lower_free_vars(expr const & e, unsigned s, unsigned d) { return lower_free_vars(e, s, d, none_menv()); }
@ -355,16 +354,15 @@ expr lower_free_vars(expr const & e, unsigned d) { return lower_free_vars(e, d,
expr lift_free_vars(expr const & e, unsigned s, unsigned d, optional<metavar_env> const & menv) {
if (d == 0)
return e;
auto f = [=](expr const & e, unsigned offset) -> expr {
if (is_var(e) && var_idx(e) >= s + offset) {
return mk_var(var_idx(e) + d);
} else if (is_metavar(e)) {
return add_lift(e, s + offset, d, menv);
} else {
return e;
}
};
return replace_fn<decltype(f)>(f)(e);
return replace(e, [=](expr const & e, unsigned offset) -> expr {
if (is_var(e) && var_idx(e) >= s + offset) {
return mk_var(var_idx(e) + d);
} else if (is_metavar(e)) {
return add_lift(e, s + offset, d, menv);
} else {
return e;
}
});
}
expr lift_free_vars(expr const & e, unsigned s, unsigned d, metavar_env const & menv) { return lift_free_vars(e, s, d, some_menv(menv)); }
expr lift_free_vars(expr const & e, unsigned s, unsigned d) { return lift_free_vars(e, s, d, none_menv()); }

70
src/kernel/instantiate.cpp
View file

@ -13,27 +13,26 @@ Author: Leonardo de Moura
namespace lean {
expr instantiate_with_closed_relaxed(expr const & a, unsigned n, expr const * s, optional<metavar_env> const & menv) {
auto f = [=](expr const & m, unsigned offset) -> expr {
if (is_var(m)) {
unsigned vidx = var_idx(m);
if (vidx >= offset) {
if (vidx < offset + n)
return s[n - (vidx - offset) - 1];
else
return mk_var(vidx - n);
return replace(a, [=](expr const & m, unsigned offset) -> expr {
if (is_var(m)) {
unsigned vidx = var_idx(m);
if (vidx >= offset) {
if (vidx < offset + n)
return s[n - (vidx - offset) - 1];
else
return mk_var(vidx - n);
} else {
return m;
}
} else if (is_metavar(m)) {
expr r = m;
for (unsigned i = 0; i < n; i++)
r = add_inst(r, offset + n - i - 1, s[i], menv);
return r;
} else {
return m;
}
} else if (is_metavar(m)) {
expr r = m;
for (unsigned i = 0; i < n; i++)
r = add_inst(r, offset + n - i - 1, s[i], menv);
return r;
} else {
return m;
}
};
return replace_fn<decltype(f)>(f)(a);
});
}
expr instantiate_with_closed_relaxed(expr const & a, unsigned n, expr const * s, metavar_env const & menv) {
return instantiate_with_closed_relaxed(a, n, s, some_menv(menv));
@ -53,27 +52,26 @@ expr instantiate_with_closed(expr const & e, expr const & s) { return instantiat
expr instantiate_with_closed(expr const & e, expr const & s, metavar_env const & menv) { return instantiate_with_closed(e, s, some_menv(menv)); }
expr instantiate(expr const & a, unsigned s, unsigned n, expr const * subst, optional<metavar_env> const & menv) {
auto f = [=](expr const & m, unsigned offset) -> expr {
if (is_var(m)) {
unsigned vidx = var_idx(m);
if (vidx >= offset + s) {
if (vidx < offset + s + n)
return lift_free_vars(subst[n - (vidx - s - offset) - 1], offset, menv);
else
return mk_var(vidx - n);
return replace(a, [=](expr const & m, unsigned offset) -> expr {
if (is_var(m)) {
unsigned vidx = var_idx(m);
if (vidx >= offset + s) {
if (vidx < offset + s + n)
return lift_free_vars(subst[n - (vidx - s - offset) - 1], offset, menv);
else
return mk_var(vidx - n);
} else {
return m;
}
} else if (is_metavar(m)) {
expr r = m;
for (unsigned i = 0; i < n; i++)
r = add_inst(r, offset + s + n - i - 1, lift_free_vars(subst[i], offset + n - i - 1, menv), menv);
return r;
} else {
return m;
}
} else if (is_metavar(m)) {
expr r = m;
for (unsigned i = 0; i < n; i++)
r = add_inst(r, offset + s + n - i - 1, lift_free_vars(subst[i], offset + n - i - 1, menv), menv);
return r;
} else {
return m;
}
};
return replace_fn<decltype(f)>(f)(a);
});
}
expr instantiate(expr const & e, unsigned n, expr const * s, optional<metavar_env> const & menv) { return instantiate(e, 0, n, s, menv); }
expr instantiate(expr const & e, unsigned n, expr const * s, metavar_env const & menv) { return instantiate(e, n, s, some_menv(menv)); }

25
src/kernel/normalizer.cpp
View file

@ -117,19 +117,18 @@ class normalizer::imp {
/** \brief Convert the value \c v back into an expression in a context that contains \c k binders. */
expr reify(expr const & v, unsigned k) {
auto f = [&](expr const & e, unsigned DEBUG_CODE(offset)) {
lean_assert(offset == 0);
lean_assert(!is_lambda(e) && !is_pi(e) && !is_metavar(e) && !is_let(e));
if (is_var(e)) {
// de Bruijn level --> de Bruijn index
return mk_var(k - var_idx(e) - 1);
} else if (is_closure(e)) {
return reify_closure(to_closure(e), k);
} else {
return e;
}
};
return replace_fn<decltype(f)>(f)(v);
return replace(v, [&](expr const & e, unsigned DEBUG_CODE(offset)) {
lean_assert(offset == 0);
lean_assert(!is_lambda(e) && !is_pi(e) && !is_metavar(e) && !is_let(e));
if (is_var(e)) {
// de Bruijn level --> de Bruijn index
return mk_var(k - var_idx(e) - 1);
} else if (is_closure(e)) {
return reify_closure(to_closure(e), k);
} else {
return e;
}
});
}
/** \brief Return true iff the value_stack does affect the context of a metavariable */

10
src/kernel/replace_fn.h
View file

@ -210,4 +210,14 @@ public:
m_rs.clear();
}
};
template<typename F>
expr replace(expr const & e, F f) {
return replace_fn<F>(f)(e);
}
template<typename F, typename P>
expr replace(expr const & e, F f, P p) {
return replace_fn<F, P>(f, p)(e);
}
}

25
src/library/substitution.cpp
View file

@ -24,23 +24,22 @@ expr find(substitution & s, expr e) {
}
expr apply(substitution & s, expr const & e, optional<metavar_env> const & menv) {
auto f = [&](expr const & e, unsigned) -> expr {
if (is_metavar(e)) {
expr r = find(s, e);
if (r != e) {
if (has_metavar(r)) {
r = apply(s, r);
s.insert(metavar_name(e), r);
return replace(e, [&](expr const & e, unsigned) -> expr {
if (is_metavar(e)) {
expr r = find(s, e);
if (r != e) {
if (has_metavar(r)) {
r = apply(s, r);
s.insert(metavar_name(e), r);
}
return apply_local_context(r, metavar_lctx(e), menv);
} else {
return e;
}
return apply_local_context(r, metavar_lctx(e), menv);
} else {
return e;
}
} else {
return e;
}
};
return replace_fn<decltype(f)>(f)(e);
});
}
DECL_UDATA(substitution)