fix(library/type_context,library/lazy_abstraction): bug in lazy_abstraction, and handle lazy_abstraction in type inference

src/library/lazy_abstraction.cpp

@@ -140,7 +140,7 @@ struct push_lazy_abstraction_fn : public replace_visitor {
     expr visit_local(expr const & e) override {
         for (unsigned i = 0; i < m_ns.size(); i++) {
             if (m_ns[i] == mlocal_name(e))
-                return lift_free_vars(m_vs[i], m_deltas[i]);
+                return visit(lift_free_vars(m_vs[i], m_deltas[i]));
         }
         return e;
     }
@@ -196,6 +196,10 @@ expr push_lazy_abstraction(expr const & e) {
     }
 }
 
+expr push_lazy_abstraction(expr const & e, buffer<name> const & ns, buffer<expr> const & vs) {
+    return push_lazy_abstraction_fn(ns, vs)(e);
+}
+
 expr mk_lazy_abstraction(expr const & e, buffer<name> const & ns) {
     lean_assert(ns.size() > 0);
     buffer<expr> vs;
@@ -225,6 +229,16 @@ expr mk_lazy_abstraction_with_locals(expr const & e, buffer<expr> const & ls) {
     return mk_lazy_abstraction_core(e, ns, ls);
 }
 
+expr mk_lazy_abstraction(expr const & e, buffer<name> const & ns, buffer<expr> const & vs) {
+    lean_assert(ns.size() > 0);
+    lean_assert(ns.size() == vs.size());
+    if (is_metavar(e)) {
+        return mk_lazy_abstraction_core(e, ns, vs);
+    } else {
+        return push_lazy_abstraction_fn(ns, vs)(e);
+    }
+}
+
 void initialize_lazy_abstraction() {
     g_lazy_abstraction_macro = new name("lazy_abstraction");
 }

src/library/lazy_abstraction.h

@@ -14,12 +14,19 @@ bool is_lazy_abstraction(expr const & e);
 expr const & get_lazy_abstraction_expr(expr const & e);
 void get_lazy_abstraction_info(expr const & e, buffer<name> & ns, buffer<expr> & es);
 expr push_lazy_abstraction(expr const & e);
+expr push_lazy_abstraction(expr const & e, buffer<name> const & ns, buffer<expr> const & es);
 
 /* Create e{ls[0] := ls[0], ..., ls[n-1] := ls[n-1]}
    \pre is_metavar(e)
    \pre for all x in ls, is_local(x) */
 expr mk_lazy_abstraction_with_locals(expr const & e, buffer<expr> const & ls);
 
+/* Ceeate e{ns[0] := vs[0], ... ls[n-1] := vs[n-1]}
+   \pre is_metavar(e)
+   \pre ns.size() == es.size()
+   \pre !ns.empty() */
+expr mk_lazy_abstraction(expr const & e, buffer<name> const & ns, buffer<expr> const & vs);
+
 void initialize_lazy_abstraction();
 void finalize_lazy_abstraction();
 }

src/library/type_context.cpp

@@ -22,6 +22,7 @@ Author: Leonardo de Moura
 #include "library/type_context.h"
 #include "library/aux_recursors.h"
 #include "library/unification_hint.h"
+#include "library/lazy_abstraction.h"
 
 #ifndef LEAN_DEFAULT_CLASS_INSTANCE_MAX_DEPTH
 #define LEAN_DEFAULT_CLASS_INSTANCE_MAX_DEPTH 32
@@ -703,6 +704,18 @@ expr type_context::infer_constant(expr const & e) {
 }
 
 expr type_context::infer_macro(expr const & e) {
+    if (is_lazy_abstraction(e)) {
+        expr const & mvar = get_lazy_abstraction_expr(e);
+        if (!is_metavar_decl_ref(mvar))
+            throw exception("unexpected occurrence of lazy abstraction macro");
+        buffer<name> ns;
+        buffer<expr> es;
+        get_lazy_abstraction_info(e, ns, es);
+        auto d = m_mctx.get_metavar_decl(mvar);
+        if (!d)
+            throw exception("infer type failed, unknown metavariable");
+        return push_lazy_abstraction(d->get_type(), ns, es);
+    }
     auto def = macro_def(e);
     bool infer_only = true;
     return def.check_type(e, *this, infer_only);

src/tests/library/CMakeLists.txt

@@ -11,3 +11,6 @@ add_test(occurs "${CMAKE_CURRENT_BINARY_DIR}/occurs")
 add_executable(head_map head_map.cpp ${library_tst_objs})
 target_link_libraries(head_map ${EXTRA_LIBS})
 add_test(head_map "${CMAKE_CURRENT_BINARY_DIR}/head_map")
+add_executable(lazy_abstraction lazy_abstraction.cpp ${library_tst_objs})
+target_link_libraries(lazy_abstraction ${EXTRA_LIBS})
+add_test(lazy_abstraction "${CMAKE_CURRENT_BINARY_DIR}/lazy_abstraction")

src/tests/library/lazy_abstraction.cpp

@@ -0,0 +1,70 @@
+/*
+Copyright (c) 2016 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#include "util/test.h"
+#include "util/init_module.h"
+#include "util/sexpr/init_module.h"
+#include "kernel/init_module.h"
+#include "library/init_module.h"
+#include "library/lazy_abstraction.h"
+#include "library/metavar_context.h"
+#include "library/type_context.h"
+using namespace lean;
+
+expr mk_lazy_abstraction(expr const & e, std::initializer_list<pair<expr, expr>> const & as) {
+    buffer<name> ns;
+    buffer<expr> vs;
+    for (auto p : as) {
+        ns.push_back(mlocal_name(p.first));
+        vs.push_back(p.second);
+    }
+    return mk_lazy_abstraction(e, ns, vs);
+}
+
+#define mkp mk_pair
+
+void tst1() {
+    environment env;
+    local_context lctx;
+    metavar_context mctx;
+    expr A  = lctx.mk_local_decl("A", mk_Prop());
+    expr a  = lctx.mk_local_decl("a", A);
+    expr b  = lctx.mk_local_decl("b", A);
+    expr m1 = mctx.mk_metavar_decl(lctx, A);
+    lean_assert(is_metavar_decl_ref(m1));
+    local_context lctx1;
+    expr A1 = lctx1.mk_local_decl("A1", mk_Prop());
+    expr a1 = lctx1.mk_local_decl("a1", A1);
+    expr b1 = lctx1.mk_local_decl("b1", A1);
+    expr e1 = mk_lazy_abstraction(m1, {mkp(A, A1), mkp(a, a1), mkp(b, b1)});
+    mctx.assign(m1, a);
+    lean_assert(mctx.instantiate_mvars(e1) == a1);
+    local_context lctx2;
+    expr A2 = lctx2.mk_local_decl("A2", mk_Prop());
+    expr a2 = lctx2.mk_local_decl("a2", A2);
+    expr b2 = lctx2.mk_local_decl("b2", A2);
+    expr e2 = mk_lazy_abstraction(e1, {mkp(A1, A2), mkp(a1, a2), mkp(b1, b2)});
+    lean_assert(mctx.instantiate_mvars(e1) == a1);
+    lean_assert(mctx.instantiate_mvars(e2) == a2);
+    aux_type_context ctx(env, options(), mctx, lctx2);
+    lean_assert(ctx->infer(e2) == A2);
+}
+
+int main() {
+    save_stack_info();
+    initialize_util_module();
+    initialize_sexpr_module();
+    initialize_kernel_module();
+    initialize_library_core_module();
+    initialize_library_module();
+    tst1();
+    finalize_library_module();
+    finalize_library_core_module();
+    finalize_kernel_module();
+    finalize_sexpr_module();
+    finalize_util_module();
+    return has_violations() ? 1 : 0;
+}