From bf13441bd705113d3dfb43e6c6a548cffbe80ff3 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 22 Feb 2014 16:12:06 -0800 Subject: [PATCH] fix(kernel): bugs in justification module, add missing metavar methods, add basic metavar tests Signed-off-by: Leonardo de Moura --- src/kernel/free_vars.cpp | 3 + src/kernel/justification.cpp | 17 +++- src/kernel/justification.h | 3 + src/kernel/metavar.cpp | 43 +++++++--- src/kernel/metavar.h | 51 ++++++++---- src/tests/kernel/CMakeLists.txt | 7 +- src/tests/kernel/metavar.cpp | 141 ++++++++++++++++++++++---------- 7 files changed, 188 insertions(+), 77 deletions(-) diff --git a/src/kernel/free_vars.cpp b/src/kernel/free_vars.cpp index 88a95c575..032e34fe5 100644 --- a/src/kernel/free_vars.cpp +++ b/src/kernel/free_vars.cpp @@ -65,6 +65,7 @@ protected: lean_unreachable(); // LCOV_EXCL_LINE case expr_kind::Meta: case expr_kind::Local: result = apply(mlocal_type(e), offset); + break; case expr_kind::App: result = apply(app_fn(e), offset) || apply(app_arg(e), offset); break; @@ -142,6 +143,7 @@ class free_var_range_fn { lean_unreachable(); // LCOV_EXCL_LINE case expr_kind::Meta: case expr_kind::Local: result = apply(mlocal_type(e)); + break; case expr_kind::App: result = std::max(apply(app_fn(e)), apply(app_arg(e))); break; @@ -237,6 +239,7 @@ protected: lean_unreachable(); // LCOV_EXCL_LINE case expr_kind::Meta: case expr_kind::Local: result = apply(mlocal_type(e), offset); + break; case expr_kind::App: result = apply(app_fn(e), offset) || apply(app_arg(e), offset); break; diff --git a/src/kernel/justification.cpp b/src/kernel/justification.cpp index e05d20a17..1ea3233df 100644 --- a/src/kernel/justification.cpp +++ b/src/kernel/justification.cpp @@ -154,7 +154,7 @@ justification const & composite_child1(justification const & j) { justification const & composite_child2(justification const & j) { lean_assert(j.is_composite()); - return to_composite(j.raw())->m_child[0]; + return to_composite(j.raw())->m_child[1]; } unsigned assumption_idx(justification const & j) { @@ -242,4 +242,19 @@ justification mk_justification(pp_jst_sfn const & fn, optional const & s) return compose(to_pos(s, p), fn(fmt, opts, subst)); }, s); } + +std::ostream & operator<<(std::ostream & out, justification const & j) { + if (j.is_none()) { + out << "none"; + } else if (j.is_asserted()) { + out << "asserted"; + } else if (j.is_assumption()) { + out << "(assumption " << assumption_idx(j) << ")"; + } else if (j.is_composite()) { + out << "(join " << composite_child1(j) << " " << composite_child2(j) << ")"; + } else { + out << "unexpected"; + } + return out; +} } diff --git a/src/kernel/justification.h b/src/kernel/justification.h index 77b914fef..8cfb8662a 100644 --- a/src/kernel/justification.h +++ b/src/kernel/justification.h @@ -132,4 +132,7 @@ unsigned assumption_idx(justification const & j); /** \brief Return true iff \c j depends on the assumption with index \c i. */ bool depends_on(justification const & j, unsigned i); + +/** \brief Printer for debugging purposes */ +std::ostream & operator<<(std::ostream & out, justification const & j); } diff --git a/src/kernel/metavar.cpp b/src/kernel/metavar.cpp index 1c057d41d..58fa720bc 100644 --- a/src/kernel/metavar.cpp +++ b/src/kernel/metavar.cpp @@ -10,6 +10,7 @@ Author: Leonardo de Moura #include "kernel/replace_visitor.h" #include "kernel/justification.h" #include "kernel/instantiate.h" +#include "kernel/find_fn.h" namespace lean { bool substitution::is_assigned(name const & m) const { @@ -41,7 +42,7 @@ void substitution::assign(name const & m, expr const & t) { assign(m, t, justification()); } -void substitution::for_each(std::function const & fn) { +void substitution::for_each(std::function const & fn) const { m_subst.for_each([=](name const & n, std::pair const & a) { fn(n, a.first, a.second); }); @@ -66,23 +67,23 @@ protected: return p1->first; } else if (m_use_jst) { if (m_update) { - auto p2 = d_instantiate_metavars(p1->first, m_subst); + auto p2 = m_subst.d_instantiate_metavars(p1->first); 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); + auto p2 = m_subst.instantiate_metavars(p1->first); 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); + expr r = m_subst.d_instantiate_metavars_wo_jst(p1->first); m_subst.assign(m_name, r); return r; } else { - return instantiate_metavars_wo_jst(p1->first, m_subst); + return m_subst.instantiate_metavars_wo_jst(p1->first); } } } else { @@ -113,23 +114,39 @@ public: 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); +std::pair substitution::instantiate_metavars(expr const & e) const { + instantiate_metavars_fn fn(const_cast(*this), 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); +std::pair substitution::d_instantiate_metavars(expr const & e) { + instantiate_metavars_fn fn(*this, 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 substitution::instantiate_metavars_wo_jst(expr const & e) const { + return instantiate_metavars_fn(const_cast(*this), false, false)(e); } -expr d_instantiate_metavars_wo_jst(expr const & e, substitution & s) { - return instantiate_metavars_fn(s, false, true)(e); +expr substitution::d_instantiate_metavars_wo_jst(expr const & e) { + return instantiate_metavars_fn(*this, false, true)(e); +} + +bool substitution::occurs(name const & m, expr const & e) const { + if (!has_metavar(e)) + return false; + auto it = find(e, [&](expr const & e, unsigned) { + if (is_metavar(e)) { + if (mlocal_name(e) == m) + return true; + auto s = get_expr(e); + return s && occurs(m, *s); + } else { + return false; + } + }); + return static_cast(it); } } diff --git a/src/kernel/metavar.h b/src/kernel/metavar.h index f75431a61..44eeaef5a 100644 --- a/src/kernel/metavar.h +++ b/src/kernel/metavar.h @@ -15,27 +15,42 @@ namespace lean { class substitution { rb_map, name_quick_cmp> m_subst; public: + typedef optional> opt_expr_jst; bool is_assigned(name const & m) const; - optional> get_assignment(name const & m) const; + opt_expr_jst get_assignment(name const & m) const; optional get_expr(name const & m) const; void assign(name const & m, expr const & t, justification const & j); void assign(name const & m, expr const & t); - void for_each(std::function const & fn); + void for_each(std::function const & fn) const; + + bool is_assigned(expr const & m) const { lean_assert(is_metavar(m)); return is_assigned(mlocal_name(m)); } + opt_expr_jst get_assignment(expr const & m) const { lean_assert(is_metavar(m)); return get_assignment(mlocal_name(m)); } + optional get_expr(expr const & m) const { lean_assert(is_metavar(m)); return get_expr(mlocal_name(m)); } + void assign(expr const & m, expr const & t, justification const & j) { lean_assert(is_metavar(m)); assign(mlocal_name(m), t, j); } + void assign(expr const & m, expr const & t) { lean_assert(is_metavar(m)); return assign(mlocal_name(m), t); } + + /** \brief Instantiate metavariables in \c e assigned in the substitution \c s. */ + std::pair instantiate_metavars(expr const & e) const; + + /** + \brief Similar to the previous function, but it compress the substitution. + By compress, we mean, for any metavariable \c m reachable from \c e, + if s[m] = t, and t has asssigned metavariables, then s[m] <- instantiate_metavars(t, s). + */ + std::pair d_instantiate_metavars(expr const & e); + + /** + \brief Instantiate metavariables in \c e assigned in the substitution \c s, + but does not return a justification object for the new expression. + */ + expr instantiate_metavars_wo_jst(expr const & e) const; + + expr d_instantiate_metavars_wo_jst(expr const & e); + + /** + \brief Return true iff \c m occurrs (directly or indirectly) in \c e. + */ + bool occurs(name const & m, expr const & e) const; + bool occurs(expr const & m, expr const & e) const { lean_assert(is_metavar(m)); return occurs(mlocal_name(m), e); } }; -/** - \brief Instantiate metavariables in \c e assigned in the substitution \c s. -*/ -std::pair instantiate_metavars(expr const & e, substitution const & s); -/** - \brief Similar to the previous function, but it compress the substitution. - By compress, we mean, for any metavariable \c m reachable from \c e, - if s[m] = t, and t has asssigned metavariables, then s[m] <- instantiate_metavars(t, s). -*/ -std::pair d_instantiate_metavars(expr const & e, substitution & s); -/** - \brief Instantiate metavariables in \c e assigned in the substitution \c s, - 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); } diff --git a/src/tests/kernel/CMakeLists.txt b/src/tests/kernel/CMakeLists.txt index 5e70f37d5..5f72b21d9 100644 --- a/src/tests/kernel/CMakeLists.txt +++ b/src/tests/kernel/CMakeLists.txt @@ -10,7 +10,6 @@ add_test(expr ${CMAKE_CURRENT_BINARY_DIR}/expr) add_executable(normalizer normalizer.cpp) target_link_libraries(normalizer ${EXTRA_LIBS}) add_test(normalizer ${CMAKE_CURRENT_BINARY_DIR}/normalizer) -# set_tests_properties(normalizer PROPERTIES ENVIRONMENT "LEAN_PATH=${LEAN_BINARY_DIR}/shell") # add_executable(threads threads.cpp) # target_link_libraries(threads ${EXTRA_LIBS}) # add_test(threads ${CMAKE_CURRENT_BINARY_DIR}/threads) @@ -32,9 +31,9 @@ add_test(replace ${CMAKE_CURRENT_BINARY_DIR}/replace) add_executable(occurs occurs.cpp) target_link_libraries(occurs ${EXTRA_LIBS}) add_test(occurs ${CMAKE_CURRENT_BINARY_DIR}/occurs) -# add_executable(metavar metavar.cpp) -# target_link_libraries(metavar ${EXTRA_LIBS}) -# add_test(metavar ${CMAKE_CURRENT_BINARY_DIR}/metavar) +add_executable(metavar metavar.cpp) +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}) diff --git a/src/tests/kernel/metavar.cpp b/src/tests/kernel/metavar.cpp index e7cbef4ab..d1934cd7e 100644 --- a/src/tests/kernel/metavar.cpp +++ b/src/tests/kernel/metavar.cpp @@ -1,5 +1,5 @@ /* -Copyright (c) 2013 Microsoft Corporation. All rights reserved. +Copyright (c) 2014 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura @@ -8,65 +8,122 @@ Author: Leonardo de Moura #include #include #include +#include #include "util/test.h" +#include "util/buffer.h" #include "kernel/metavar.h" #include "kernel/instantiate.h" #include "kernel/abstract.h" -#include "kernel/free_vars.h" -#include "kernel/normalizer.h" -#include "kernel/environment.h" -#include "kernel/type_checker.h" -#include "kernel/kernel_exception.h" -#include "kernel/kernel.h" -#include "kernel/io_state.h" -#include "library/printer.h" -#include "library/io_state_stream.h" -#include "library/placeholder.h" -#include "library/arith/arith.h" -#include "frontends/lean/frontend.h" -#include "frontends/lua/register_modules.h" +// #include "kernel/free_vars.h" +// #include "kernel/normalizer.h" +// #include "kernel/environment.h" +// #include "kernel/type_checker.h" +// #include "kernel/kernel_exception.h" +// #include "kernel/kernel.h" +// #include "kernel/io_state.h" +// #include "library/printer.h" +// #include "library/io_state_stream.h" +// #include "library/placeholder.h" +// #include "library/arith/arith.h" +// #include "frontends/lean/frontend.h" +// #include "frontends/lua/register_modules.h" using namespace lean; -static std::ostream & operator<<(std::ostream & out, metavar_env const & menv) { +void collect_assumptions(justification const & j, buffer & r) { + std::set already_found; + buffer todo; + todo.push_back(j); + while (!todo.empty()) { + justification j = todo.back(); + todo.pop_back(); + if (j.is_assumption()) { + unsigned idx = assumption_idx(j); + if (already_found.find(idx) == already_found.end()) { + already_found.insert(idx); + r.push_back(idx); + } + } else if (j.is_composite()) { + todo.push_back(composite_child1(j)); + todo.push_back(composite_child2(j)); + } + } +} + +void display_assumptions(std::ostream & out, justification const & j) { + buffer ids; + collect_assumptions(j, ids); + for (unsigned i = 0; i < ids.size(); i++) { + if (i > 0) out << " "; + out << ids[i]; + } +} + +static std::ostream & operator<<(std::ostream & out, substitution const & s) { bool first = true; - menv->for_each_subst([&](name const & n, expr const & v) { + s.for_each([&](name const & n, expr const & v, justification const & j) { if (first) first = false; else out << "\n"; - out << "?" << n << " <- " << v; + out << "?" << n << " <- " << v << " {"; + display_assumptions(out, j); + out << "}"; }); return out; } -static std::ostream & operator<<(std::ostream & out, buffer const & uc) { - formatter fmt = mk_simple_formatter(); - for (auto c : uc) { - out << c.pp(fmt, options(), nullptr, true) << "\n"; +static bool check_assumptions(justification const & j, std::initializer_list const & ls) { + buffer ids; + collect_assumptions(j, ids); + lean_assert(ids.size() == ls.size()); + for (unsigned id : ls) { + lean_assert(std::find(ids.begin(), ids.end(), id) != ids.end()); } - return out; + return true; } static void tst1() { - metavar_env menv; - expr m1 = menv->mk_metavar(); - lean_assert(!menv->is_assigned(m1)); - expr t1 = menv->get_type(m1); - lean_assert(is_metavar(t1)); - lean_assert(is_eqp(menv->get_type(m1), t1)); - lean_assert(is_eqp(menv->get_type(m1), t1)); - lean_assert(!menv->is_assigned(m1)); - expr m2 = menv->mk_metavar(); - lean_assert(!menv->is_assigned(m1)); - expr t2 = menv->get_type(m2); - lean_assert(is_metavar(m2)); - lean_assert(!is_eqp(t1, t2)); - lean_assert(t1 != t2); + substitution subst; + expr m1 = mk_metavar("m1", Bool); + lean_assert(!subst.is_assigned(m1)); + expr m2 = mk_metavar("m2", Bool); + lean_assert(!is_eqp(m1, m2)); + lean_assert(m1 != m2); expr f = Const("f"); expr a = Const("a"); - menv->assign(m1, f(a)); - lean_assert(menv->is_assigned(m1)); - lean_assert(!menv->is_assigned(m2)); - lean_assert(*(menv->get_subst(m1)) == f(a)); + subst.assign(m1, f(a)); + lean_assert(subst.is_assigned(m1)); + lean_assert(!subst.is_assigned(m2)); + lean_assert(*subst.get_expr(m1) == f(a)); + lean_assert(subst.instantiate_metavars(f(m1)).first == f(f(a))); + std::cout << subst << "\n"; } +static void tst2() { + substitution s; + expr m1 = mk_metavar("m1", Bool); + expr m2 = mk_metavar("m2", Bool); + expr m3 = mk_metavar("m3", Bool); + expr f = Const("f"); + expr g = Const("g"); + expr a = Const("a"); + s.assign(m1, f(m2), mk_assumption_justification(1)); + s.assign(m2, g(a), mk_assumption_justification(2)); + lean_assert(check_assumptions(s.get_assignment(m1)->second, {1})); + lean_assert(s.occurs(m1, f(m1))); + lean_assert(s.occurs(m2, f(m1))); + lean_assert(!s.occurs(m1, f(m2))); + lean_assert(!s.occurs(m1, f(a))); + lean_assert(!s.occurs(m3, f(m1))); + std::cout << s << "\n"; + auto p1 = s.instantiate_metavars(g(m1)); + check_assumptions(p1.second, {1, 2}); + lean_assert(check_assumptions(s.get_assignment(m1)->second, {1})); + lean_assert(p1.first == g(f(g(a)))); + auto p2 = s.d_instantiate_metavars(g(m1)); + check_assumptions(p2.second, {1, 2}); + std::cout << s << "\n"; + lean_assert(check_assumptions(s.get_assignment(m1)->second, {1, 2})); +} + +#if 0 static void tst2() { metavar_env menv; expr f = Const("f"); @@ -629,12 +686,13 @@ static void tst28() { lean_assert(add_lift(m2, 2, 2, menv) == m2); lean_assert(add_lift(m2, 2, 2, menv) != add_lift(m2, 2, 2)); } +#endif int main() { save_stack_info(); - register_modules(); tst1(); tst2(); +#if 0 tst3(); tst4(); tst5(); @@ -661,5 +719,6 @@ int main() { tst26(); tst27(); tst28(); +#endif return has_violations() ? 1 : 0; }