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

refactor(kernel): cleanup instantiate and abstract procedures, implement update procedures

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-02-17 15:21:48 -08:00
parent db31cc37a1
commit 72e1678ad9
7 changed files with 109 additions and 158 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/kernel/CMakeLists.txt
View file

@ -1,6 +1,6 @@
add_library(kernel level.cpp diff_cnstrs.cpp expr.cpp expr_eq_fn.cpp
for_each_fn.cpp occurs.cpp replace_fn.cpp free_vars.cpp
# abstract.cpp instantiate.cpp
for_each_fn.cpp occurs.cpp replace_fn.cpp free_vars.cpp abstract.cpp
instantiate.cpp
# normalizer.cpp context.cpp level.cpp object.cpp environment.cpp
# type_checker.cpp kernel.cpp occurs.cpp metavar.cpp
# justification.cpp unification_constraint.cpp kernel_exception.cpp

44
src/kernel/expr.cpp
View file

@ -294,10 +294,50 @@ unsigned get_depth(expr const & e) {
bool operator==(expr const & a, expr const & b) { return expr_eq_fn()(a, b); }
expr update_app(expr const & e, expr const & new_fn, expr const & new_arg) {
if (!is_eqp(app_fn(e), new_fn) || !is_eqp(app_arg(e), new_arg))
return mk_app(new_fn, new_arg);
else
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);
else
return e;
}
expr update_pair(expr const & e, expr const & new_first, expr const & new_second, expr const & new_type) {
if (!is_eqp(pair_first(e), new_first) || !is_eqp(pair_second(e), new_second) || !is_eqp(pair_type(e), new_type))
return mk_pair(new_first, new_second, new_type);
else
return e;
}
expr update_binder(expr const & e, expr const & new_domain, expr const & new_body) {
if (!is_eqp(binder_domain(e), new_domain) || !is_eqp(binder_body(e), new_body))
return mk_binder(e.kind(), binder_name(e), new_domain, new_body);
else
return e;
}
expr update_let(expr const & e, optional<expr> const & new_type, expr const & new_val, expr const & new_body) {
if (!is_eqp(let_type(e), new_type) || !is_eqp(let_value(e), new_val) || !is_eqp(let_body(e), new_body))
return mk_let(let_name(e), new_type, new_val, new_body);
else
return e;
}
expr update_mlocal(expr const & e, expr const & new_type) {
if (!is_eqp(mlocal_type(e), new_type))
return mk_mlocal(is_metavar(e), mlocal_name(e), new_type);
else
return e;
}
#if 0
bool is_arrow(expr const & t) {
optional<bool> r = t.raw()->is_arrow();
if (r) {

28
src/kernel/expr.h
View file

@ -122,15 +122,11 @@ public:
friend expr mk_var(unsigned idx);
friend expr mk_sort(level const & l);
friend expr mk_constant(name const & n, levels const & ls);
friend expr mk_metavar(name const & n, expr const & t);
friend expr mk_local(name const & n, expr const & t);
friend expr mk_mlocal(bool is_meta, name const & n, expr const & t);
friend expr mk_app(expr const & f, expr const & a);
friend expr mk_pair(expr const & f, expr const & s, expr const & t);
friend expr mk_fst(expr const & p);
friend expr mk_snd(expr const & p);
friend expr mk_lambda(name const & n, expr const & t, expr const & e);
friend expr mk_pi(name const & n, expr const & t, expr const & e);
friend expr mk_sigma(name const & n, expr const & t, expr const & e);
friend expr mk_proj(bool fst, expr const & p);
friend expr mk_binder(expr_kind k, name const & n, expr const & t, expr const & e);
friend expr mk_let(name const & n, optional<expr> const & t, expr const & v, expr const & e);
friend expr mk_macro(macro * m);
@ -373,18 +369,21 @@ inline expr mk_constant(name const & n, levels const & ls) { return expr(new exp
inline expr mk_constant(name const & n) { return mk_constant(n, levels()); }
inline expr Const(name const & n) { return mk_constant(n); }
inline expr mk_macro(macro * m) { return expr(new expr_macro(m)); }
inline expr mk_metavar(name const & n, expr const & t) { return expr(new expr_mlocal(true, n, t)); }
inline expr mk_local(name const & n, expr const & t) { return expr(new expr_mlocal(false, n, t)); }
inline expr mk_mlocal(bool is_meta, name const & n, expr const & t) { return expr(new expr_mlocal(is_meta, n, t)); }
inline expr mk_metavar(name const & n, expr const & t) { return mk_mlocal(true, n, t); }
inline expr mk_local(name const & n, expr const & t) { return mk_mlocal(false, n, t); }
inline expr mk_pair(expr const & f, expr const & s, expr const & t) { return expr(new expr_dep_pair(f, s, t)); }
inline expr mk_fst(expr const & a) { return expr(new expr_proj(true, a)); }
inline expr mk_snd(expr const & a) { return expr(new expr_proj(false, a)); }
inline expr mk_proj(bool first, expr const & a) { return expr(new expr_proj(first, a)); }
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(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()); }
inline expr mk_lambda(name const & n, expr const & t, expr const & e) { return expr(new expr_binder(expr_kind::Lambda, n, t, e)); }
inline expr mk_pi(name const & n, expr const & t, expr const & e) { return expr(new expr_binder(expr_kind::Pi, n, t, e)); }
inline expr mk_sigma(name const & n, expr const & t, expr const & e) { return expr(new expr_binder(expr_kind::Sigma, n, t, e)); }
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); }
inline expr mk_sigma(name const & n, expr const & t, expr const & e) { return mk_binder(expr_kind::Sigma, n, t, e); }
inline expr mk_let(name const & n, optional<expr> const & t, expr const & v, expr const & e) {
return expr(new expr_let(n, t, v, e));
}
@ -556,7 +555,6 @@ struct expr_cell_offset_eqp { unsigned operator()(expr_cell_offset const & p1, e
*/
expr copy(expr const & e);
// =======================================
// Update
expr update_app(expr const & e, expr const & new_fn, expr const & new_arg);

88
src/kernel/instantiate.cpp
View file

@ -8,12 +8,11 @@ Author: Leonardo de Moura
#include <limits>
#include "kernel/free_vars.h"
#include "kernel/replace_fn.h"
#include "kernel/metavar.h"
#include "kernel/instantiate.h"
namespace lean {
template<bool ClosedSubst>
expr instantiate_core(expr const & a, unsigned s, unsigned n, expr const * subst, optional<ro_metavar_env> const & menv) {
expr instantiate_core(expr const & a, unsigned s, unsigned n, expr const * subst) {
return replace(a, [=](expr const & m, unsigned offset) -> expr {
if (is_var(m)) {
unsigned vidx = var_idx(m);
@ -22,56 +21,45 @@ expr instantiate_core(expr const & a, unsigned s, unsigned n, expr const * subst
if (ClosedSubst)
return subst[n - (vidx - s - offset) - 1];
else
return lift_free_vars(subst[n - (vidx - s - offset) - 1], offset, menv);
return lift_free_vars(subst[n - (vidx - s - offset) - 1], offset);
} else {
return mk_var(vidx - n);
}
} else {
return m;
}
} else if (is_metavar(m)) {
expr r = m;
for (unsigned i = 0; i < n; i++) {
expr v = ClosedSubst ? subst[i] : lift_free_vars(subst[i], offset + n - i - 1, menv);
r = add_inst(r, offset + s + n - i - 1, v, menv);
}
return r;
} else {
return m;
}
});
}
expr instantiate_with_closed(expr const & a, unsigned n, expr const * s, optional<ro_metavar_env> const & menv) {
lean_assert(std::all_of(s, s+n, [&](expr const & e) { return !has_free_var(e, 0, std::numeric_limits<unsigned>::max(), menv); }));
return instantiate_core<true>(a, 0, n, s, menv);
}
expr instantiate_with_closed(expr const & e, unsigned n, expr const * s, ro_metavar_env const & menv) { return instantiate_with_closed(e, n, s, some_ro_menv(menv)); }
expr instantiate_with_closed(expr const & e, unsigned n, expr const * s) { return instantiate_with_closed(e, n, s, none_ro_menv()); }
expr instantiate_with_closed(expr const & e, unsigned s, unsigned n, expr const * subst) { return instantiate_core<true>(e, s, n, subst); }
expr instantiate_with_closed(expr const & e, unsigned n, expr const * s) { return instantiate_with_closed(e, 0, n, s); }
expr instantiate_with_closed(expr const & e, std::initializer_list<expr> const & l) { return instantiate_with_closed(e, l.size(), l.begin()); }
expr instantiate_with_closed(expr const & e, expr const & s, optional<ro_metavar_env> const & menv) { return instantiate_with_closed(e, 1, &s, menv); }
expr instantiate_with_closed(expr const & e, expr const & s) { return instantiate_with_closed(e, 1, &s); }
expr instantiate_with_closed(expr const & e, expr const & s, ro_metavar_env const & menv) { return instantiate_with_closed(e, s, some_ro_menv(menv)); }
expr instantiate(expr const & a, unsigned s, unsigned n, expr const * subst, optional<ro_metavar_env> const & menv) {
return instantiate_core<false>(a, s, n, subst, menv);
}
expr instantiate(expr const & e, unsigned n, expr const * s, optional<ro_metavar_env> const & menv) { return instantiate(e, 0, n, s, menv); }
expr instantiate(expr const & e, unsigned n, expr const * s, ro_metavar_env const & menv) { return instantiate(e, n, s, some_ro_menv(menv)); }
expr instantiate(expr const & e, unsigned n, expr const * s) { return instantiate(e, n, s, none_ro_menv()); }
expr instantiate(expr const & e, unsigned s, unsigned n, expr const * subst) { return instantiate_core<false>(e, s, n, subst); }
expr instantiate(expr const & e, unsigned n, expr const * s) { return instantiate(e, 0, n, s); }
expr instantiate(expr const & e, std::initializer_list<expr> const & l) { return instantiate(e, l.size(), l.begin()); }
expr instantiate(expr const & e, unsigned i, expr const & s, optional<ro_metavar_env> const & menv) { return instantiate(e, i, 1, &s, menv); }
expr instantiate(expr const & e, unsigned i, expr const & s, ro_metavar_env const & menv) { return instantiate(e, i, 1, &s, some_ro_menv(menv)); }
expr instantiate(expr const & e, unsigned i, expr const & s) { return instantiate(e, i, 1, &s, none_ro_menv()); }
expr instantiate(expr const & e, expr const & s, optional<ro_metavar_env> const & menv) { return instantiate(e, 1, &s, menv); }
expr instantiate(expr const & e, expr const & s, ro_metavar_env const & menv) { return instantiate(e, s, some_ro_menv(menv)); }
expr instantiate(expr const & e, expr const & s) { return instantiate(e, s, none_ro_menv()); }
expr instantiate(expr const & e, unsigned i, expr const & s) { return instantiate(e, i, 1, &s); }
expr instantiate(expr const & e, expr const & s) { return instantiate(e, 0, s); }
bool is_head_beta(expr const & t) {
return is_app(t) && is_lambda(arg(t, 0));
expr const * it = &t;
while (is_app(*it)) {
expr const & f = app_fn(*it);
if (is_lambda(f)) {
return true;
} else if (is_app(f)) {
it = &f;
} else {
return false;
}
}
return false;
}
expr apply_beta(expr f, unsigned num_args, expr const * args, optional<ro_metavar_env> const & menv) {
expr apply_beta(expr f, unsigned num_args, expr const * args) {
if (!is_lambda(f)) {
buffer<expr> new_args;
new_args.push_back(f);
@ -79,12 +67,12 @@ expr apply_beta(expr f, unsigned num_args, expr const * args, optional<ro_metava
return mk_app(new_args);
} else {
unsigned m = 1;
while (is_lambda(abst_body(f)) && m < num_args) {
f = abst_body(f);
while (is_lambda(binder_body(f)) && m < num_args) {
f = binder_body(f);
m++;
}
lean_assert(m <= num_args);
expr r = instantiate(abst_body(f), m, args, menv);
expr r = instantiate(binder_body(f), m, args);
if (m == num_args) {
return r;
} else {
@ -96,34 +84,40 @@ expr apply_beta(expr f, unsigned num_args, expr const * args, optional<ro_metava
}
}
}
expr apply_beta(expr f, unsigned num_args, expr const * args, ro_metavar_env const & menv) { return apply_beta(f, num_args, args, some_ro_menv(menv)); }
expr apply_beta(expr f, unsigned num_args, expr const * args) { return apply_beta(f, num_args, args, none_ro_menv()); }
expr head_beta_reduce(expr const & t, optional<ro_metavar_env> const & menv) {
expr head_beta_reduce(expr const & t) {
if (!is_head_beta(t)) {
return t;
} else {
return apply_beta(arg(t, 0), num_args(t) - 1, &arg(t, 1), menv);
buffer<expr> args;
expr const * it = &t;
while (true) {
lean_assert(is_app(*it));
expr f = app_fn(*it);
args.push_back(app_arg(*it));
if (is_lambda(f)) {
return apply_beta(f, args.size(), args.data());
} else {
lean_assert(is_app(f));
it = &f;
}
}
}
}
expr head_beta_reduce(expr const & t) { return head_beta_reduce(t, none_ro_menv()); }
expr head_beta_reduce(expr const & t, ro_metavar_env const & menv) { return head_beta_reduce(t, some_ro_menv(menv)); }
expr beta_reduce(expr t, optional<ro_metavar_env> const & menv) {
expr beta_reduce(expr t) {
auto f = [=](expr const & m, unsigned) -> expr {
if (is_head_beta(m))
return head_beta_reduce(m, menv);
return head_beta_reduce(m);
else
return m;
};
while (true) {
expr new_t = replace_fn<decltype(f)>(f)(t);
expr new_t = replace_fn(f)(t);
if (new_t == t)
return new_t;
else
t = new_t;
}
}
expr beta_reduce(expr t, ro_metavar_env const & menv) { return beta_reduce(t, some_ro_menv(menv)); }
expr beta_reduce(expr t) { return beta_reduce(t, none_ro_menv()); }
}

37
src/kernel/instantiate.h
View file

@ -13,52 +13,21 @@ class ro_metavar_env;
\brief Replace the free variables with indices 0, ..., n-1 with s[n-1], ..., s[0] in e.
\pre s[0], ..., s[n-1] must be closed expressions (i.e., no free variables).
\remark When the parameter menv is not none, this function will minimize the use
of the local entry inst in metavariables occurring in \c e.
*/
expr instantiate_with_closed(expr const & e, unsigned n, expr const * s, optional<ro_metavar_env> const & menv);
expr instantiate_with_closed(expr const & e, unsigned n, expr const * s, ro_metavar_env const & menv);
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, optional<ro_metavar_env> const & menv);
expr instantiate_with_closed(expr const & e, expr const & s, ro_metavar_env const & menv);
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.
\remark When the parameter menv is not none, this function will minimize the use
of the local entry inst in metavariables occurring in \c e.
*/
expr instantiate(expr const & e, unsigned n, expr const * s, optional<ro_metavar_env> const & menv);
expr instantiate(expr const & e, unsigned n, expr const * s, ro_metavar_env const & menv);
/** \brief Replace the free variables with indices 0, ..., n-1 with s[n-1], ..., s[0] 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.
*/
expr instantiate(expr const & e, unsigned i, expr const & s, optional<ro_metavar_env> const & menv);
expr instantiate(expr const & e, unsigned i, expr const & s, ro_metavar_env const & menv);
/** \brief Replace free variable \c i with \c s in \c e. */
expr instantiate(expr const & e, unsigned i, expr const & s);
/**
\brief Replace free variable \c 0 with \c s in \c e.
*/
expr instantiate(expr const & e, expr const & s, optional<ro_metavar_env> const & menv);
expr instantiate(expr const & e, expr const & s, ro_metavar_env const & menv);
/** \brief Replace free variable \c 0 with \c s in \c e. */
expr instantiate(expr const & e, expr const & s);
expr apply_beta(expr f, unsigned num_args, expr const * args, optional<ro_metavar_env> const & menv);
expr apply_beta(expr f, unsigned num_args, expr const * args, ro_metavar_env const & menv);
expr apply_beta(expr f, unsigned num_args, expr const * args);
bool is_head_beta(expr const & t);
expr head_beta_reduce(expr const & t, optional<ro_metavar_env> const & menv);
expr head_beta_reduce(expr const & t, ro_metavar_env const & menv);
expr head_beta_reduce(expr const & t);
expr beta_reduce(expr t, optional<ro_metavar_env> const & menv);
expr beta_reduce(expr t, ro_metavar_env const & menv);
expr beta_reduce(expr t);
}

6
src/tests/kernel/CMakeLists.txt
View file

@ -36,9 +36,9 @@ add_test(diff_cnstrs ${CMAKE_CURRENT_BINARY_DIR}/diff_cnstrs)
# target_link_libraries(metavar ${EXTRA_LIBS})
# add_test(metavar ${CMAKE_CURRENT_BINARY_DIR}/metavar)
# set_tests_properties(metavar PROPERTIES ENVIRONMENT "LEAN_PATH=${LEAN_BINARY_DIR}/shell")
# add_executable(instantiate instantiate.cpp)
# target_link_libraries(instantiate ${EXTRA_LIBS})
# add_test(instantiate ${CMAKE_CURRENT_BINARY_DIR}/instantiate)
add_executable(instantiate instantiate.cpp)
target_link_libraries(instantiate ${EXTRA_LIBS})
add_test(instantiate ${CMAKE_CURRENT_BINARY_DIR}/instantiate)
# add_executable(universe_constraints universe_constraints.cpp)
# target_link_libraries(universe_constraints ${EXTRA_LIBS})
# add_test(universe_constraints ${CMAKE_CURRENT_BINARY_DIR}/universe_constraints)

60
src/tests/kernel/instantiate.cpp
View file

@ -7,7 +7,6 @@ Author: Leonardo de Moura
#include "util/test.h"
#include "kernel/abstract.h"
#include "kernel/instantiate.h"
#include "kernel/metavar.h"
using namespace lean;
static void tst1() {
@ -22,18 +21,14 @@ static void tst1() {
expr N = Const("N");
expr F1 = Fun({x, N}, x)(f, a);
lean_assert(is_head_beta(F1));
std::cout << F1 << " --> " << head_beta_reduce(F1) << "\n";
lean_assert_eq(head_beta_reduce(F1), f(a));
lean_assert(head_beta_reduce(F1) == f(a));
expr F2 = Fun({{h, N >> (N >> (N >> N))}, {y, N}}, h(y))(f, a, b, c);
lean_assert(is_head_beta(F2));
std::cout << F2 << " --> " << head_beta_reduce(F2) << "\n";
lean_assert_eq(head_beta_reduce(F2), f(a, b, c));
lean_assert(head_beta_reduce(F2) == f(a, b, c));
expr F3 = Fun({x, N}, f(Fun({y, N}, y)(x), x))(a);
lean_assert(is_head_beta(F3));
std::cout << F3 << " --> " << head_beta_reduce(F3) << "\n";
lean_assert_eq(head_beta_reduce(F3), f(Fun({y, N}, y)(a), a));
std::cout << F3 << " --> " << beta_reduce(F3) << "\n";
lean_assert_eq(beta_reduce(F3), f(a, a));
lean_assert(head_beta_reduce(F3) == f(Fun({y, N}, y)(a), a));
lean_assert(beta_reduce(F3) == f(a, a));
}
static void tst2() {
@ -42,57 +37,12 @@ static void tst2() {
expr f = Const("f");
expr N = Const("N");
expr F1 = Let({x, a}, f(x));
lean_assert_eq(head_beta_reduce(F1), F1);
}
static void tst3() {
metavar_env menv;
expr f = Const("f");
expr a = Const("a");
expr T = Const("T");
expr m1 = menv->mk_metavar();
expr m2 = menv->mk_metavar(context({{"x", T}, {"y", T}}));
lean_assert_eq(instantiate(f(m1, Var(0)), 0, a, menv), f(m1, a));
lean_assert_ne(instantiate(f(m1, Var(0)), 0, a, menv), instantiate(f(m1, Var(0)), 0, a));
lean_assert_ne(instantiate(f(m2, Var(0)), 0, a, menv), f(m2, a));
lean_assert_eq(instantiate(f(m2, Var(0)), 0, a, menv), f(add_inst(m2, 0, a), a));
expr x = Const("x");
lean_assert_eq(instantiate(Fun({x, T}, f(m1, Var(1), Var(0))), 0, f(Var(0)), menv),
Fun({x, T}, f(m1, f(Var(1)), Var(0))));
lean_assert_eq(instantiate(Fun({x, T}, f(m2, Var(1), Var(0))), 0, f(Var(0)), menv),
Fun({x, T}, f(add_inst(m2, 1, f(Var(1))), f(Var(1)), Var(0))));
lean_assert_eq(instantiate(Fun({x, T}, f(m2, Var(3), Var(0))), 2, f(Var(0)), menv),
Fun({x, T}, f(m2, f(Var(1)), Var(0))));
lean_assert_eq(instantiate(Fun({x, T}, f(m1, Var(3), Var(0))), 2, f(Var(0)), menv),
Fun({x, T}, f(m1, f(Var(1)), Var(0))));
lean_assert_eq(instantiate(Fun({x, T}, f(m2, Var(3), Var(0))), 1, f(Var(0)), menv),
Fun({x, T}, f(m2, Var(2), Var(0))));
expr m3 = menv->mk_metavar(context({{"x", T}, {"y", T}, {"z", T}}));
lean_assert_eq(instantiate(Fun({x, T}, f(m3, Var(3), Var(0))), 1, f(Var(0)), menv),
Fun({x, T}, f(add_inst(m3, 2, f(Var(1))), Var(2), Var(0))));
}
static void tst4() {
metavar_env menv;
expr T = Const("T");
expr m1 = menv->mk_metavar();
expr m2 = menv->mk_metavar(context({{"x", T}, {"y", T}}));
expr f = Const("f");
expr g = Const("f");
expr x = Const("x");
expr a = Const("a");
expr F1 = Fun({x, T}, g(x, m1))(a);
expr F2 = Fun({x, T}, g(x, m2))(a);
lean_assert_eq(head_beta_reduce(F1, menv), g(a, m1));
lean_assert_eq(head_beta_reduce(F1), g(a, add_inst(m1, 0, a)));
lean_assert_eq(head_beta_reduce(F2, menv), g(a, add_inst(m2, 0, a)));
lean_assert(head_beta_reduce(F1) == F1);
}
int main() {
save_stack_info();
tst1();
tst2();
tst3();
tst4();
return has_violations() ? 1 : 0;
}