From 75d5087d436a5a9caa8bc2b3ef1f5dfe5deefca0 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 17 Sep 2016 19:44:38 -0700 Subject: [PATCH] fix(library/type_context): using incorrect local_context at `revert` --- library/init/wf.lean | 6 +++-- src/library/type_context.cpp | 45 ++++++++++++++++++++++++++++-------- src/library/type_context.h | 10 ++++++-- 3 files changed, 47 insertions(+), 14 deletions(-) diff --git a/library/init/wf.lean b/library/init/wf.lean index 733cf4cb97..8eb04ffdda 100644 --- a/library/init/wf.lean +++ b/library/init/wf.lean @@ -58,8 +58,10 @@ namespace well_founded theorem fix_F_eq (x : A) (r : acc R x) : fix_F F x r = F x (λ (y : A) (p : y ≺ x), fix_F F y (acc.inv r p)) := - acc.drec (λ x acx ih, rfl) r - + @acc.drec A R + (λ x r, fix_F F x r = F x (λ (y : A) (p : y ≺ x), fix_F F y (acc.inv r p))) + (λ x r ih, rfl) + x r end variables {A : Type u} {C : A → Type v} {R : A → A → Prop} diff --git a/src/library/type_context.cpp b/src/library/type_context.cpp index f178c0ac57..45ee8248a9 100644 --- a/src/library/type_context.cpp +++ b/src/library/type_context.cpp @@ -359,7 +359,7 @@ pair type_context::revert_core(buffer & to_revert, lo } }); local_context new_ctx = ctx.remove(to_revert); - return mk_pair(new_ctx, mk_pi(to_revert, type)); + return mk_pair(new_ctx, mk_pi(ctx, to_revert, type)); } expr type_context::revert_core(buffer & to_revert, expr const & mvar) { @@ -373,10 +373,11 @@ expr type_context::revert(buffer & to_revert, expr const & mvar) { lean_assert(is_metavar_decl_ref(mvar)); lean_assert(std::all_of(to_revert.begin(), to_revert.end(), [&](expr const & l) { return static_cast(m_mctx.get_metavar_decl(mvar)->get_context().get_local_decl(l)); })); + local_context lctx = m_mctx.get_metavar_decl(mvar)->get_context(); expr new_mvar = revert_core(to_revert, mvar); expr r = new_mvar; for (expr const & a : to_revert) { - if (!m_lctx.get_local_decl(a)->get_value()) { + if (!lctx.get_local_decl(a)->get_value()) { // 'a' is not a let-decl r = mk_app(r, a); } @@ -400,12 +401,12 @@ expr type_context::abstract_locals(expr const & e, unsigned num_locals, expr con return delayed_abstract_locals(new_e, num_locals, locals); } -expr type_context::mk_binding(bool is_pi, unsigned num_locals, expr const * locals, expr const & e) { +expr type_context::mk_binding(bool is_pi, local_context const & lctx, unsigned num_locals, expr const * locals, expr const & e) { buffer decls; buffer types; buffer> values; for (unsigned i = 0; i < num_locals; i++) { - local_decl const & decl = *m_lctx.get_local_decl(locals[i]); + local_decl const & decl = *lctx.get_local_decl(locals[i]); decls.push_back(decl); types.push_back(abstract_locals(instantiate_mvars(decl.get_type()), i, locals)); if (auto v = decl.get_value()) @@ -429,28 +430,52 @@ expr type_context::mk_binding(bool is_pi, unsigned num_locals, expr const * loca return new_e; } +expr type_context::mk_lambda(local_context const & lctx, buffer const & locals, expr const & e) { + return mk_binding(false, lctx, locals.size(), locals.data(), e); +} + +expr type_context::mk_pi(local_context const & lctx, buffer const & locals, expr const & e) { + return mk_binding(true, lctx, locals.size(), locals.data(), e); +} + +expr type_context::mk_lambda(local_context const & lctx, expr const & local, expr const & e) { + return mk_binding(false, lctx, 1, &local, e); +} + +expr type_context::mk_pi(local_context const & lctx, expr const & local, expr const & e) { + return mk_binding(true, lctx, 1, &local, e); +} + +expr type_context::mk_lambda(local_context const & lctx, std::initializer_list const & locals, expr const & e) { + return mk_binding(false, lctx, locals.size(), locals.begin(), e); +} + +expr type_context::mk_pi(local_context const & lctx, std::initializer_list const & locals, expr const & e) { + return mk_binding(true, lctx, locals.size(), locals.begin(), e); +} + expr type_context::mk_lambda(buffer const & locals, expr const & e) { - return mk_binding(false, locals.size(), locals.data(), e); + return mk_lambda(m_lctx, locals, e); } expr type_context::mk_pi(buffer const & locals, expr const & e) { - return mk_binding(true, locals.size(), locals.data(), e); + return mk_pi(m_lctx, locals, e); } expr type_context::mk_lambda(expr const & local, expr const & e) { - return mk_binding(false, 1, &local, e); + return mk_lambda(m_lctx, local, e); } expr type_context::mk_pi(expr const & local, expr const & e) { - return mk_binding(true, 1, &local, e); + return mk_pi(m_lctx, local, e); } expr type_context::mk_lambda(std::initializer_list const & locals, expr const & e) { - return mk_binding(false, locals.size(), locals.begin(), e); + return mk_lambda(m_lctx, locals, e); } expr type_context::mk_pi(std::initializer_list const & locals, expr const & e) { - return mk_binding(true, locals.size(), locals.begin(), e); + return mk_pi(m_lctx, locals, e); } /* --------------------- diff --git a/src/library/type_context.h b/src/library/type_context.h index ae0ec63303..2fa51b1a9d 100644 --- a/src/library/type_context.h +++ b/src/library/type_context.h @@ -299,6 +299,13 @@ public: \remark locals is updated with dependencies. */ expr revert(buffer & locals, expr const & mvar); + expr mk_lambda(local_context const & lctx, buffer const & locals, expr const & e); + expr mk_pi(local_context const & lctx, buffer const & locals, expr const & e); + expr mk_lambda(local_context const & lctx, expr const & local, expr const & e); + expr mk_pi(local_context const & lctx, expr const & local, expr const & e); + expr mk_lambda(local_context const & lctx, std::initializer_list const & locals, expr const & e); + expr mk_pi(local_context const & lctx, std::initializer_list const & locals, expr const & e); + expr mk_lambda(buffer const & locals, expr const & e); expr mk_pi(buffer const & locals, expr const & e); expr mk_lambda(expr const & local, expr const & e); @@ -411,7 +418,7 @@ private: pair revert_core(buffer & to_revert, local_context const & ctx, expr const & type); expr revert_core(buffer & to_revert, expr const & mvar); - expr mk_binding(bool is_pi, unsigned num_locals, expr const * locals, expr const & e); + expr mk_binding(bool is_pi, local_context const & lctx, unsigned num_locals, expr const * locals, expr const & e); /* ------------ Temporary metavariable assignment. @@ -575,7 +582,6 @@ public: virtual expr whnf(expr const & e) override; virtual bool is_def_eq(expr const & e1, expr const & e2) override; - expr mk_lambda(buffer const & locals, expr const & e); expr mk_pi(buffer const & locals, expr const & e); expr mk_lambda(expr const & local, expr const & e);