refactor(library/lazy_abstraction): lazy ==> delayed

src/frontends/lean/pp.cpp

@@ -32,7 +32,7 @@ Author: Leonardo de Moura
 #include "library/print.h"
 #include "library/abbreviation.h"
 #include "library/pp_options.h"
-#include "library/lazy_abstraction.h"
+#include "library/delayed_abstraction.h"
 #include "library/constants.h"
 #include "library/replace_visitor.h"
 #include "library/string.h"
@@ -873,14 +873,14 @@ auto pretty_fn::pp_explicit(expr const & e) -> result {
     return result(max_bp(), compose(*g_explicit_fmt, res_arg.fmt()));
 }
 
-auto pretty_fn::pp_lazy_abstraction(expr const & e) -> result {
+auto pretty_fn::pp_delayed_abstraction(expr const & e) -> result {
     if (m_lazy_abstraction) {
-        format r = pp(get_lazy_abstraction_expr(e)).fmt();
+        format r = pp(get_delayed_abstraction_expr(e)).fmt();
         r += format("{");
         format body;
         buffer<name> ns;
         buffer<expr> vs;
-        get_lazy_abstraction_info(e, ns, vs);
+        get_delayed_abstraction_info(e, ns, vs);
         for (unsigned i = 0; i < ns.size(); i++) {
             if (i > 0) body += comma() + line();
             body += format(ns[i]) + space() + format(":=") + space() + nest(m_indent, pp(vs[i]).fmt());
@@ -889,7 +889,7 @@ auto pretty_fn::pp_lazy_abstraction(expr const & e) -> result {
         r += format("}");
         return result(r);
     } else {
-        return pp(get_lazy_abstraction_expr(e));
+        return pp(get_delayed_abstraction_expr(e));
     }
 }
 
@@ -898,8 +898,8 @@ auto pretty_fn::pp_macro(expr const & e) -> result {
         return pp_explicit(e);
     } else if (is_quote(e)) {
         return result(format("`(") + nest(2, pp(get_quote_expr(e)).fmt()) + format(")"));
-    } else if (is_lazy_abstraction(e)) {
-        return pp_lazy_abstraction(e);
+    } else if (is_delayed_abstraction(e)) {
+        return pp_delayed_abstraction(e);
     } else if (is_inaccessible(e)) {
         format li = m_unicode ? format("⌞") : format("?(");
         format ri = m_unicode ? format("⌟") : format(")");

src/frontends/lean/pp.h

@@ -121,7 +121,7 @@ private:
     result pp_show(expr const & e);
     result pp_macro(expr const & e);
     result pp_explicit(expr const & e);
-    result pp_lazy_abstraction(expr const & e);
+    result pp_delayed_abstraction(expr const & e);
     result pp_let_macro(expr e);
     result pp_let(expr e);
     result pp_num(mpz const & n);

src/library/CMakeLists.txt

@@ -12,7 +12,7 @@ add_library(library OBJECT deep_copy.cpp expr_lt.cpp io_state.cpp
   composition_manager.cpp tc_multigraph.cpp noncomputable.cpp
   aux_recursors.cpp norm_num.cpp trace.cpp
   attribute_manager.cpp error_handling.cpp unification_hint.cpp
-  local_context.cpp metavar_context.cpp type_context.cpp export_decl.cpp lazy_abstraction.cpp
+  local_context.cpp metavar_context.cpp type_context.cpp export_decl.cpp delayed_abstraction.cpp
   fun_info.cpp congr_lemma.cpp defeq_canonizer.cpp scope_pos_info_provider.cpp
   # Legacy -- The following files will be eventually deleted
   normalize.cpp justification.cpp constraint.cpp metavar.cpp choice.cpp locals.cpp

src/library/delayed_abstraction.cpp

@@ -9,8 +9,8 @@ Author: Leonardo de Moura
 #include "library/replace_visitor.h"
 
 namespace lean {
-static name * g_lazy_abstraction_macro = nullptr;
-/** \brief Lazy abstraction macro. This is an auxiliary temporary macro used by the tactic framework.
+static name * g_delayed_abstraction_macro = nullptr;
+/** \brief Delayed abstraction macro. This is an auxiliary temporary macro used by the tactic framework.
     It is used in the following kind of situation.
     Suppose we have a goal ?M
 
@@ -22,20 +22,20 @@ static name * g_lazy_abstraction_macro = nullptr;
 
     The intro tactic adds the following assignment to the metavariable context
 
-           ?M := fun H : A, (lazy_abstraction[H] ?M' #0)
+           ?M := fun H : A, (delayed_abstraction[H] ?M' #0)
 
-     The lazy_abstraction macro indicates that when ?M' is instantiated, we need to replace
+     The delayed_abstraction macro indicates that when ?M' is instantiated, we need to replace
      the local constant H with the de-bruijn index 0 at this assignment.
 */
-class lazy_abstraction_macro : public macro_definition_cell {
+class delayed_abstraction_macro : public macro_definition_cell {
     list<name> m_value;
 public:
-    lazy_abstraction_macro(list<name> const & v):m_value(v) {}
+    delayed_abstraction_macro(list<name> const & v):m_value(v) {}
     virtual bool lt(macro_definition_cell const & d) const {
         /** TODO(Leo): improve if needed */
-        return length(m_value) < length(static_cast<lazy_abstraction_macro const &>(d).m_value);
+        return length(m_value) < length(static_cast<delayed_abstraction_macro const &>(d).m_value);
     }
-    virtual name get_name() const { return *g_lazy_abstraction_macro; }
+    virtual name get_name() const { return *g_delayed_abstraction_macro; }
     virtual expr check_type(expr const & e, abstract_type_context & ctx, bool) const {
         return ctx.infer(macro_arg(e, macro_num_args(e) - 1));
     }
@@ -44,7 +44,7 @@ public:
     }
     virtual unsigned trust_level() const { return 0; }
     virtual bool operator==(macro_definition_cell const & other) const {
-        lazy_abstraction_macro const * other_ptr = dynamic_cast<lazy_abstraction_macro const *>(&other);
+        delayed_abstraction_macro const * other_ptr = dynamic_cast<delayed_abstraction_macro const *>(&other);
         return other_ptr && m_value == other_ptr->m_value;
     }
     virtual unsigned hash() const {
@@ -56,7 +56,7 @@ public:
 };
 
 /** \brief Each name occurs only once. */
-bool validate_lazy_abstraction(buffer<name> const & b) {
+bool validate_delayed_abstraction(buffer<name> const & b) {
     for (unsigned i = 0; i < b.size(); i++) {
         for (unsigned j = i + 1; j < b.size(); j++) {
             if (b[i] == b[j])
@@ -66,37 +66,37 @@ bool validate_lazy_abstraction(buffer<name> const & b) {
     return true;
 }
 
-bool validate_lazy_abstraction(list<name> const & s) {
+bool validate_delayed_abstraction(list<name> const & s) {
     buffer<name> b;
     to_buffer(s, b);
-    return validate_lazy_abstraction(b);
+    return validate_delayed_abstraction(b);
 }
 
-expr mk_lazy_abstraction_core(expr const & e, buffer<name> const & ns, buffer<expr> const & vs) {
+expr mk_delayed_abstraction_core(expr const & e, buffer<name> const & ns, buffer<expr> const & vs) {
     lean_assert(is_metavar(e));
     lean_assert(ns.size() == vs.size());
     buffer<expr> args;
     args.append(vs);
     args.push_back(e);
-    return mk_macro(macro_definition(new lazy_abstraction_macro(to_list(ns))), args.size(), args.data());
+    return mk_macro(macro_definition(new delayed_abstraction_macro(to_list(ns))), args.size(), args.data());
 }
 
-bool is_lazy_abstraction(expr const & e) {
-    return is_macro(e) && dynamic_cast<lazy_abstraction_macro const *>(macro_def(e).raw()) != nullptr;
+bool is_delayed_abstraction(expr const & e) {
+    return is_macro(e) && dynamic_cast<delayed_abstraction_macro const *>(macro_def(e).raw()) != nullptr;
 }
 
-void get_lazy_abstraction_info(expr const & e, buffer<name> & ns, buffer<expr> & es) {
-    lean_assert(is_lazy_abstraction(e));
-    to_buffer(static_cast<lazy_abstraction_macro const *>(macro_def(e).raw())->get_names(), ns);
+void get_delayed_abstraction_info(expr const & e, buffer<name> & ns, buffer<expr> & es) {
+    lean_assert(is_delayed_abstraction(e));
+    to_buffer(static_cast<delayed_abstraction_macro const *>(macro_def(e).raw())->get_names(), ns);
     es.append(macro_num_args(e) - 1, macro_args(e));
 }
 
-expr const & get_lazy_abstraction_expr(expr const & e) {
-    lean_assert(is_lazy_abstraction(e));
+expr const & get_delayed_abstraction_expr(expr const & e) {
+    lean_assert(is_delayed_abstraction(e));
     return macro_arg(e, macro_num_args(e) - 1);
 }
 
-struct push_lazy_abstraction_fn : public replace_visitor {
+struct push_delayed_abstraction_fn : public replace_visitor {
     buffer<name>     m_ns;
     buffer<expr>     m_vs;
     buffer<unsigned> m_deltas;
@@ -146,17 +146,17 @@ struct push_lazy_abstraction_fn : public replace_visitor {
     }
 
     expr visit_macro(expr const & e) override {
-        if (is_lazy_abstraction(e)) {
+        if (is_delayed_abstraction(e)) {
             unsigned sz = m_vs.size();
             buffer<name> new_ns;
             buffer<expr> new_vs;
-            get_lazy_abstraction_info(e, new_ns, new_vs);
+            get_delayed_abstraction_info(e, new_ns, new_vs);
             lean_assert(new_ns.size() == new_vs.size());
             m_ns.append(new_ns);
             m_vs.append(new_vs);
             m_deltas.resize(m_vs.size(), 0);
             m_cache.clear();
-            expr r = visit(get_lazy_abstraction_expr(e));
+            expr r = visit(get_delayed_abstraction_expr(e));
             m_ns.shrink(sz);
             m_vs.shrink(sz);
             m_deltas.shrink(sz);
@@ -172,10 +172,10 @@ struct push_lazy_abstraction_fn : public replace_visitor {
         for (unsigned i = 0; i < m_vs.size(); i++) {
             new_vs.push_back(lift_free_vars(m_vs[i], m_deltas[i]));
         }
-        return mk_lazy_abstraction_core(e, m_ns, new_vs);
+        return mk_delayed_abstraction_core(e, m_ns, new_vs);
     }
 
-    push_lazy_abstraction_fn(buffer<name> const & ns, buffer<expr> const & vs) {
+    push_delayed_abstraction_fn(buffer<name> const & ns, buffer<expr> const & vs) {
         lean_assert(ns.size() == vs.size());
         m_ns.append(ns);
         m_vs.append(vs);
@@ -183,24 +183,24 @@ struct push_lazy_abstraction_fn : public replace_visitor {
     }
 };
 
-expr push_lazy_abstraction(expr const & e) {
-    lean_assert(is_lazy_abstraction(e));
-    expr const & a = get_lazy_abstraction_expr(e);
+expr push_delayed_abstraction(expr const & e) {
+    lean_assert(is_delayed_abstraction(e));
+    expr const & a = get_delayed_abstraction_expr(e);
     if (is_metavar(a)) {
         return e;
     } else {
         buffer<name> ns;
         buffer<expr> vs;
-        get_lazy_abstraction_info(e, ns, vs);
-        return push_lazy_abstraction_fn(ns, vs)(a);
+        get_delayed_abstraction_info(e, ns, vs);
+        return push_delayed_abstraction_fn(ns, vs)(a);
     }
 }
 
-expr push_lazy_abstraction(expr const & e, buffer<name> const & ns, buffer<expr> const & vs) {
-    return push_lazy_abstraction_fn(ns, vs)(e);
+expr push_delayed_abstraction(expr const & e, buffer<name> const & ns, buffer<expr> const & vs) {
+    return push_delayed_abstraction_fn(ns, vs)(e);
 }
 
-expr mk_lazy_abstraction(expr const & e, buffer<name> const & ns) {
+expr mk_delayed_abstraction(expr const & e, buffer<name> const & ns) {
     lean_assert(ns.size() > 0);
     buffer<expr> vs;
     unsigned sz = ns.size();
@@ -208,42 +208,42 @@ expr mk_lazy_abstraction(expr const & e, buffer<name> const & ns) {
         vs.push_back(mk_var(sz - i - 1));
     }
     if (is_metavar(e)) {
-        return mk_lazy_abstraction_core(e, ns, vs);
+        return mk_delayed_abstraction_core(e, ns, vs);
     } else {
-        return push_lazy_abstraction_fn(ns, vs)(e);
+        return push_delayed_abstraction_fn(ns, vs)(e);
     }
 }
 
-expr mk_lazy_abstraction(expr const & e, name const & n) {
+expr mk_delayed_abstraction(expr const & e, name const & n) {
     buffer<name> ns;
     ns.push_back(n);
-    return mk_lazy_abstraction(e, ns);
+    return mk_delayed_abstraction(e, ns);
 }
 
-expr mk_lazy_abstraction_with_locals(expr const & e, buffer<expr> const & ls) {
+expr mk_delayed_abstraction_with_locals(expr const & e, buffer<expr> const & ls) {
     lean_assert(is_metavar(e));
     lean_assert(std::all_of(ls.begin(), ls.end(), is_local));
     buffer<name> ns;
     for (expr const & l : ls)
         ns.push_back(mlocal_name(l));
-    return mk_lazy_abstraction_core(e, ns, ls);
+    return mk_delayed_abstraction_core(e, ns, ls);
 }
 
-expr mk_lazy_abstraction(expr const & e, buffer<name> const & ns, buffer<expr> const & vs) {
+expr mk_delayed_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);
+        return mk_delayed_abstraction_core(e, ns, vs);
     } else {
-        return push_lazy_abstraction_fn(ns, vs)(e);
+        return push_delayed_abstraction_fn(ns, vs)(e);
     }
 }
 
-void initialize_lazy_abstraction() {
-    g_lazy_abstraction_macro = new name("lazy_abstraction");
+void initialize_delayed_abstraction() {
+    g_delayed_abstraction_macro = new name("delayed_abstraction");
 }
 
-void finalize_lazy_abstraction() {
-    delete g_lazy_abstraction_macro;
+void finalize_delayed_abstraction() {
+    delete g_delayed_abstraction_macro;
 }
 }

src/library/delayed_abstraction.h

@@ -0,0 +1,32 @@
+/*
+Copyright (c) 2016 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#pragma once
+#include "kernel/environment.h"
+
+namespace lean {
+expr mk_delayed_abstraction(expr const & e, buffer<name> const & ns);
+expr mk_delayed_abstraction(expr const & e, name const & n);
+bool is_delayed_abstraction(expr const & e);
+expr const & get_delayed_abstraction_expr(expr const & e);
+void get_delayed_abstraction_info(expr const & e, buffer<name> & ns, buffer<expr> & es);
+expr push_delayed_abstraction(expr const & e);
+expr push_delayed_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_delayed_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_delayed_abstraction(expr const & e, buffer<name> const & ns, buffer<expr> const & vs);
+
+void initialize_delayed_abstraction();
+void finalize_delayed_abstraction();
+}

src/library/init_module.cpp

@@ -47,7 +47,7 @@ Author: Leonardo de Moura
 #include "library/metavar_context.h"
 #include "library/attribute_manager.h"
 #include "library/unification_hint.h"
-#include "library/lazy_abstraction.h"
+#include "library/delayed_abstraction.h"
 #include "library/app_builder.h"
 #include "library/fun_info.h"
 
@@ -127,11 +127,11 @@ void initialize_library_module() {
     initialize_fun_info();
     initialize_unification_hint();
     initialize_type_context();
-    initialize_lazy_abstraction();
+    initialize_delayed_abstraction();
 }
 
 void finalize_library_module() {
-    finalize_lazy_abstraction();
+    finalize_delayed_abstraction();
     finalize_type_context();
     finalize_unification_hint();
     finalize_fun_info();

src/library/lazy_abstraction.h

@@ -1,32 +0,0 @@
-/*
-Copyright (c) 2016 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-
-Author: Leonardo de Moura
-*/
-#pragma once
-#include "kernel/environment.h"
-
-namespace lean {
-expr mk_lazy_abstraction(expr const & e, buffer<name> const & ns);
-expr mk_lazy_abstraction(expr const & e, name const & n);
-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/metavar_util.h

@@ -6,7 +6,7 @@ Author: Leonardo de Moura
 */
 #include "kernel/instantiate.h"
 #include "library/replace_visitor.h"
-#include "library/lazy_abstraction.h"
+#include "library/delayed_abstraction.h"
 
 namespace lean {
 /*
@@ -174,8 +174,8 @@ class instantiate_mvars_fn : public replace_visitor {
         for (unsigned i = 0; i < macro_num_args(e); i++)
             new_args.push_back(visit(macro_arg(e, i)));
         expr r = update_macro(e, new_args.size(), new_args.data());
-        if (is_lazy_abstraction(r))
-            return push_lazy_abstraction(r);
+        if (is_delayed_abstraction(r))
+            return push_delayed_abstraction(r);
         else
             return r;
     }

src/library/tactic/assert_tactic.cpp

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 
 Author: Leonardo de Moura
 */
-#include "library/lazy_abstraction.h"
+#include "library/delayed_abstraction.h"
 #include "library/vm/vm_name.h"
 #include "library/vm/vm_expr.h"
 #include "library/tactic/tactic_state.h"
@@ -32,9 +32,9 @@ vm_obj assert_define(bool is_assert, name const & n, expr const & t, tactic_stat
     expr new_M_2         = mctx.mk_metavar_decl(lctx, g->get_type());
     expr new_val;
     if (is_assert)
-        new_val = mk_app(mk_lambda(n, t, mk_lazy_abstraction(new_M_2, mlocal_name(l))), new_M_1);
+        new_val = mk_app(mk_lambda(n, t, mk_delayed_abstraction(new_M_2, mlocal_name(l))), new_M_1);
     else
-        new_val = mk_let(n, t, new_M_1, mk_lazy_abstraction(new_M_2, mlocal_name(l)));
+        new_val = mk_let(n, t, new_M_1, mk_delayed_abstraction(new_M_2, mlocal_name(l)));
     mctx.assign(head(s.goals()), new_val);
     list<expr> new_gs    = cons(new_M_1, cons(new_M_2, tail(s.goals())));
     return mk_tactic_success(set_mctx_goals(s, mctx, new_gs));
@@ -72,9 +72,9 @@ vm_obj assertv_definev(bool is_assert, name const & n, expr const & t, expr cons
     expr new_M           = mctx.mk_metavar_decl(lctx, g->get_type());
     expr new_val;
     if (is_assert)
-        new_val = mk_app(mk_lambda(n, t, mk_lazy_abstraction(new_M, mlocal_name(l))), v);
+        new_val = mk_app(mk_lambda(n, t, mk_delayed_abstraction(new_M, mlocal_name(l))), v);
     else
-        new_val = mk_let(n, t, v, mk_lazy_abstraction(new_M, mlocal_name(l)));
+        new_val = mk_let(n, t, v, mk_delayed_abstraction(new_M, mlocal_name(l)));
     mctx.assign(head(s.goals()), new_val);
     list<expr> new_gs    = cons(new_M, tail(s.goals()));
     return mk_tactic_success(set_mctx_goals(s, mctx, new_gs));

src/library/tactic/intro_tactic.cpp

@@ -6,7 +6,7 @@ Author: Leonardo de Moura
 */
 #include "kernel/instantiate.h"
 #include "kernel/abstract.h"
-#include "library/lazy_abstraction.h"
+#include "library/delayed_abstraction.h"
 #include "library/vm/vm_name.h"
 #include "library/vm/vm_nat.h"
 #include "library/vm/vm_expr.h"
@@ -55,7 +55,7 @@ optional<expr> intron(environment const & env, options const & opts, metavar_con
         }
     }
     expr new_M   = ctx.mk_metavar_decl(ctx.lctx(), type);
-    expr new_val = abstract_locals(mk_lazy_abstraction_with_locals(new_M, new_Hs), new_Hs.size(), new_Hs.data());
+    expr new_val = abstract_locals(mk_delayed_abstraction_with_locals(new_M, new_Hs), new_Hs.size(), new_Hs.data());
     unsigned i   = new_Hs.size();
     while (i > 0) {
         --i;
@@ -139,7 +139,7 @@ vm_obj intro(name const & n, tactic_state const & s) {
         expr H               = lctx.mk_local_decl(n1, head_beta_reduce(binding_domain(type)), binding_info(type));
         expr new_type        = instantiate(binding_body(type), H);
         expr new_M           = mctx.mk_metavar_decl(lctx, new_type);
-        expr new_val         = mk_lambda(n1, binding_domain(type), mk_lazy_abstraction(new_M, mlocal_name(H)));
+        expr new_val         = mk_lambda(n1, binding_domain(type), mk_delayed_abstraction(new_M, mlocal_name(H)));
         mctx.assign(head(s.goals()), new_val);
         list<expr> new_gs(new_M, tail(s.goals()));
         return mk_tactic_success(to_obj(H), set_mctx_goals(s, mctx, new_gs));
@@ -149,7 +149,7 @@ vm_obj intro(name const & n, tactic_state const & s) {
         expr H               = lctx.mk_local_decl(n1, head_beta_reduce(let_type(type)), let_value(type));
         expr new_type        = instantiate(let_body(type), H);
         expr new_M           = mctx.mk_metavar_decl(lctx, new_type);
-        expr new_val         = mk_let(n1, let_type(type), let_value(type), mk_lazy_abstraction(new_M, mlocal_name(H)));
+        expr new_val         = mk_let(n1, let_type(type), let_value(type), mk_delayed_abstraction(new_M, mlocal_name(H)));
         mctx.assign(head(s.goals()), new_val);
         list<expr> new_gs(new_M, tail(s.goals()));
         return mk_tactic_success(to_obj(H), set_mctx_goals(s, mctx, new_gs));

src/library/type_context.cpp

@@ -23,7 +23,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"
+#include "library/delayed_abstraction.h"
 #include "library/fun_info.h"
 
 #ifndef LEAN_DEFAULT_CLASS_INSTANCE_MAX_DEPTH
@@ -730,17 +730,17 @@ 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_delayed_abstraction(e)) {
+        expr const & mvar = get_delayed_abstraction_expr(e);
         if (!is_metavar_decl_ref(mvar))
-            throw exception("unexpected occurrence of lazy abstraction macro");
+            throw exception("unexpected occurrence of delayed abstraction macro");
         buffer<name> ns;
         buffer<expr> es;
-        get_lazy_abstraction_info(e, ns, es);
+        get_delayed_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);
+        return push_delayed_abstraction(d->get_type(), ns, es);
     }
     auto def = macro_def(e);
     bool infer_only = true;

src/tests/library/CMakeLists.txt

@@ -11,6 +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")
+add_executable(delayed_abstraction delayed_abstraction.cpp ${library_tst_objs})
+target_link_libraries(delayed_abstraction ${EXTRA_LIBS})
+add_test(delayed_abstraction "${CMAKE_CURRENT_BINARY_DIR}/delayed_abstraction")

src/tests/library/delayed_abstraction.cpp

@@ -9,19 +9,19 @@ Author: Leonardo de Moura
 #include "util/sexpr/init_module.h"
 #include "kernel/init_module.h"
 #include "library/init_module.h"
-#include "library/lazy_abstraction.h"
+#include "library/delayed_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) {
+expr mk_delayed_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);
+    return mk_delayed_abstraction(e, ns, vs);
 }
 
 #define mkp mk_pair
@@ -39,14 +39,14 @@ void tst1() {
     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)});
+    expr e1 = mk_delayed_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)});
+    expr e2 = mk_delayed_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);