fix(kernel): bugs in justification module, add missing metavar methods, add basic metavar tests

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

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;

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<expr> 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;
+}
 }

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

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<void(name const & n, expr const & e, justification const & j)> const & fn) {
+void substitution::for_each(std::function<void(name const & n, expr const & e, justification const & j)> const & fn) const {
     m_subst.for_each([=](name const & n, std::pair<expr, justification> 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<expr, justification> instantiate_metavars(expr const & e, substitution const & s) {
+std::pair<expr, justification> substitution::instantiate_metavars(expr const & e) const {
-    instantiate_metavars_fn fn(const_cast<substitution&>(s), true, false);
+    instantiate_metavars_fn fn(const_cast<substitution&>(*this), 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) {
+std::pair<expr, justification> substitution::d_instantiate_metavars(expr const & e) {
-    instantiate_metavars_fn fn(s, true, true);
+    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) {
+expr substitution::instantiate_metavars_wo_jst(expr const & e) const {
-    return instantiate_metavars_fn(const_cast<substitution&>(s), false, false)(e);
+    return instantiate_metavars_fn(const_cast<substitution&>(*this), false, false)(e);
 }
 
-expr d_instantiate_metavars_wo_jst(expr const & e, substitution & s) {
+expr substitution::d_instantiate_metavars_wo_jst(expr const & e) {
-    return instantiate_metavars_fn(s, false, true)(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<bool>(it);
 }
 }

src/kernel/metavar.h

@@ -15,27 +15,42 @@ namespace lean {
 class substitution {
     rb_map<name, std::pair<expr, justification>, name_quick_cmp> m_subst;
 public:
+    typedef optional<std::pair<expr, justification>> opt_expr_jst;
     bool is_assigned(name const & m) const;
-    optional<std::pair<expr, justification>> get_assignment(name const & m) const;
+    opt_expr_jst get_assignment(name const & m) const;
     optional<expr> 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<void(name const & n, expr const & e, justification const & j)> const & fn);
+    void for_each(std::function<void(name const & n, expr const & e, justification const & j)> const & fn) const;
-};
+
-/**
+    bool is_assigned(expr const & m) const { lean_assert(is_metavar(m)); return is_assigned(mlocal_name(m)); }
-   \brief Instantiate metavariables in \c e assigned in the substitution \c s.
+    opt_expr_jst get_assignment(expr const & m) const { lean_assert(is_metavar(m)); return get_assignment(mlocal_name(m)); }
-*/
+    optional<expr> get_expr(expr const & m) const { lean_assert(is_metavar(m)); return get_expr(mlocal_name(m)); }
-std::pair<expr, justification> instantiate_metavars(expr const & e, substitution const & s);
+    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<expr, justification> 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<expr, justification> d_instantiate_metavars(expr const & e, substitution & s);
+    std::pair<expr, justification> 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, substitution const & s);
+    expr instantiate_metavars_wo_jst(expr const & e) const;
-expr d_instantiate_metavars_wo_jst(expr const & e, substitution & s);
+
+    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); }
+};
 }

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)
+add_executable(metavar metavar.cpp)
-# target_link_libraries(metavar ${EXTRA_LIBS})
+target_link_libraries(metavar ${EXTRA_LIBS})
-# add_test(metavar ${CMAKE_CURRENT_BINARY_DIR}/metavar)
+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})

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 <algorithm>
 #include <vector>
 #include <utility>
+#include <set>
 #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/free_vars.h"
-#include "kernel/normalizer.h"
+// #include "kernel/normalizer.h"
-#include "kernel/environment.h"
+// #include "kernel/environment.h"
-#include "kernel/type_checker.h"
+// #include "kernel/type_checker.h"
-#include "kernel/kernel_exception.h"
+// #include "kernel/kernel_exception.h"
-#include "kernel/kernel.h"
+// #include "kernel/kernel.h"
-#include "kernel/io_state.h"
+// #include "kernel/io_state.h"
-#include "library/printer.h"
+// #include "library/printer.h"
-#include "library/io_state_stream.h"
+// #include "library/io_state_stream.h"
-#include "library/placeholder.h"
+// #include "library/placeholder.h"
-#include "library/arith/arith.h"
+// #include "library/arith/arith.h"
-#include "frontends/lean/frontend.h"
+// #include "frontends/lean/frontend.h"
-#include "frontends/lua/register_modules.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<unsigned> & r) {
+    std::set<unsigned> already_found;
+    buffer<justification> 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<unsigned> 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<unification_constraint> const & uc) {
+static bool check_assumptions(justification const & j, std::initializer_list<unsigned> const & ls) {
-    formatter fmt = mk_simple_formatter();
+    buffer<unsigned> ids;
-    for (auto c : uc) {
+    collect_assumptions(j, ids);
-        out << c.pp(fmt, options(), nullptr, true) << "\n";
+    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;
+    substitution subst;
-    expr m1 = menv->mk_metavar();
+    expr m1 = mk_metavar("m1", Bool);
-    lean_assert(!menv->is_assigned(m1));
+    lean_assert(!subst.is_assigned(m1));
-    expr t1 = menv->get_type(m1);
+    expr m2 = mk_metavar("m2", Bool);
-    lean_assert(is_metavar(t1));
+    lean_assert(!is_eqp(m1, m2));
-    lean_assert(is_eqp(menv->get_type(m1), t1));
+    lean_assert(m1 != m2);
-    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);
     expr f = Const("f");
     expr a = Const("a");
-    menv->assign(m1, f(a));
+    subst.assign(m1, f(a));
-    lean_assert(menv->is_assigned(m1));
+    lean_assert(subst.is_assigned(m1));
-    lean_assert(!menv->is_assigned(m2));
+    lean_assert(!subst.is_assigned(m2));
-    lean_assert(*(menv->get_subst(m1)) == f(a));
+    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;
 }