diff --git a/src/library/lazy_abstraction.cpp b/src/library/lazy_abstraction.cpp index e7fb4db878..75ca02b89e 100644 --- a/src/library/lazy_abstraction.cpp +++ b/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 const & ns, buffer const & vs) { + return push_lazy_abstraction_fn(ns, vs)(e); +} + expr mk_lazy_abstraction(expr const & e, buffer const & ns) { lean_assert(ns.size() > 0); buffer vs; @@ -225,6 +229,16 @@ expr mk_lazy_abstraction_with_locals(expr const & e, buffer const & ls) { return mk_lazy_abstraction_core(e, ns, ls); } +expr mk_lazy_abstraction(expr const & e, buffer const & ns, buffer 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"); } diff --git a/src/library/lazy_abstraction.h b/src/library/lazy_abstraction.h index 9ea009fa4a..a67d453d07 100644 --- a/src/library/lazy_abstraction.h +++ b/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 & ns, buffer & es); expr push_lazy_abstraction(expr const & e); +expr push_lazy_abstraction(expr const & e, buffer const & ns, buffer 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 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 const & ns, buffer const & vs); + void initialize_lazy_abstraction(); void finalize_lazy_abstraction(); } diff --git a/src/library/type_context.cpp b/src/library/type_context.cpp index f4ef3abaf2..1e107456b1 100644 --- a/src/library/type_context.cpp +++ b/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 ns; + buffer 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); diff --git a/src/tests/library/CMakeLists.txt b/src/tests/library/CMakeLists.txt index fdda3170ed..af14ea8893 100644 --- a/src/tests/library/CMakeLists.txt +++ b/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") diff --git a/src/tests/library/lazy_abstraction.cpp b/src/tests/library/lazy_abstraction.cpp new file mode 100644 index 0000000000..767c4b9b64 --- /dev/null +++ b/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> const & as) { + buffer ns; + buffer 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; +}