From 1bfaf19277cdf6ee8fd165bbf888f452a0f78b48 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 5 Jul 2017 16:40:45 -0700 Subject: [PATCH] chore(library/delayed_abstraction): clarify delayed_abstraction API --- src/frontends/lean/elaborator.cpp | 2 +- src/library/delayed_abstraction.cpp | 2 +- src/library/delayed_abstraction.h | 9 ++++++++- src/library/metavar_util.h | 4 +++- src/library/type_context.cpp | 2 +- 5 files changed, 14 insertions(+), 5 deletions(-) diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp index 660eefa8bc..a0554a2546 100644 --- a/src/frontends/lean/elaborator.cpp +++ b/src/frontends/lean/elaborator.cpp @@ -3619,7 +3619,7 @@ static expr replace_with_simple_metavars(metavar_context mctx, name_map & buffer ns; buffer es; get_delayed_abstraction_info(e, ns, es); expr mvar_type = mctx.instantiate_mvars(decl->get_type()); - mvar_type = push_delayed_abstraction(mvar_type, ns, es); + mvar_type = append_delayed_abstraction(mvar_type, ns, es); expr new_type = replace_with_simple_metavars(mctx, cache, mvar_type); expr new_mvar = mk_metavar(mlocal_name(mvar), new_type); return some_expr(new_mvar); diff --git a/src/library/delayed_abstraction.cpp b/src/library/delayed_abstraction.cpp index 902e88a44c..ad5438dbfb 100644 --- a/src/library/delayed_abstraction.cpp +++ b/src/library/delayed_abstraction.cpp @@ -210,7 +210,7 @@ expr push_delayed_abstraction(expr const & e) { } } -expr push_delayed_abstraction(expr const & e, buffer const & ns, buffer const & vs) { +expr append_delayed_abstraction(expr const & e, buffer const & ns, buffer const & vs) { return push_delayed_abstraction_fn(ns, vs)(e); } diff --git a/src/library/delayed_abstraction.h b/src/library/delayed_abstraction.h index 4ded7b0448..c87af08903 100644 --- a/src/library/delayed_abstraction.h +++ b/src/library/delayed_abstraction.h @@ -13,8 +13,15 @@ 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 & ns, buffer & es); +/* Given a delayed abstraction `[delayed t, h_1 := e_1, ..., h_n := e_n]`, push + the delayed substitutions `h_i := e_i` to the metavariables occurring in `t`. + + Remark: if `t` is a metavariable, then we just return `e`. */ expr push_delayed_abstraction(expr const & e); -expr push_delayed_abstraction(expr const & e, buffer const & ns, buffer const & es); +/* Append the new delayed substitutions `ns[i] := es[i]` to the metavariables occurring in `e`. + + \pre ns.size() == es.size() */ +expr append_delayed_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) diff --git a/src/library/metavar_util.h b/src/library/metavar_util.h index a8de0f84e7..29fc77889e 100644 --- a/src/library/metavar_util.h +++ b/src/library/metavar_util.h @@ -24,6 +24,8 @@ bool is_assigned(expr const & e) const; optional get_assignment(expr const & e) const; void assign(expr const & m, expr const & v); +push_delayed_abstraction + bool in_tmp_mode() const; */ @@ -205,7 +207,7 @@ public: expr r = visit(e); if (m_found_delayed_abstraction) { buffer ns; buffer es; - r = push_delayed_abstraction(r, ns, es); + r = append_delayed_abstraction(r, ns, es); } return r; } diff --git a/src/library/type_context.cpp b/src/library/type_context.cpp index fb4b32d8a8..6d490c2eda 100644 --- a/src/library/type_context.cpp +++ b/src/library/type_context.cpp @@ -1139,7 +1139,7 @@ expr type_context::infer_macro(expr const & e) { get_delayed_abstraction_info(e, ns, es); auto d = m_mctx.find_metavar_decl(mvar); if (!d) throw_unknown_metavar(mvar); - return push_delayed_abstraction(d->get_type(), ns, es); + return append_delayed_abstraction(d->get_type(), ns, es); } auto def = macro_def(e); bool infer_only = true;