From cfab344bcc0858c43b341f62077765122ced66df Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 5 Jul 2017 16:57:18 -0700 Subject: [PATCH] fix(library/delayed_abstraction): fixes #1728 --- src/library/delayed_abstraction.cpp | 37 +++++++++++++++++--- src/library/delayed_abstraction.h | 5 +-- src/library/type_context.cpp | 2 +- tests/lean/elab_error_msgs.lean.expected.out | 6 ++-- tests/lean/run/1728.lean | 25 +++++++++++++ 5 files changed, 64 insertions(+), 11 deletions(-) create mode 100644 tests/lean/run/1728.lean diff --git a/src/library/delayed_abstraction.cpp b/src/library/delayed_abstraction.cpp index ad5438dbfb..307d09a480 100644 --- a/src/library/delayed_abstraction.cpp +++ b/src/library/delayed_abstraction.cpp @@ -9,6 +9,7 @@ Author: Leonardo de Moura #include "kernel/abstract.h" #include "kernel/abstract_type_context.h" #include "library/replace_visitor.h" +#include "library/metavar_context.h" namespace lean { static name * g_delayed_abstraction_macro = nullptr; @@ -99,9 +100,11 @@ expr const & get_delayed_abstraction_expr(expr const & e) { } struct push_delayed_abstraction_fn : public replace_visitor { - buffer m_ns; - buffer m_vs; - buffer m_deltas; + buffer m_ns; + buffer m_vs; + buffer m_deltas; + /* If m_mctx is not nullptr we use it to filter unnecessary delayed abstractions. */ + metavar_context const * m_mctx{nullptr}; void add_vidxs(int v) { for (unsigned & d : m_deltas) @@ -182,6 +185,25 @@ struct push_delayed_abstraction_fn : public replace_visitor { } expr visit_meta(expr const & e) override { + if (m_mctx && is_metavar_decl_ref(e)) { + if (optional decl = m_mctx->find_metavar_decl(e)) { + /* We only include delayed substitutions that are in the scope of `e` */ + local_context const & lctx = decl->get_context(); + buffer new_ns; + buffer new_vs; + for (unsigned i = 0; i < m_vs.size(); i++) { + if (lctx.find_local_decl(m_ns[i])) { + new_ns.push_back(m_ns[i]); + new_vs.push_back(lift_free_vars(m_vs[i], m_deltas[i])); + } + } + if (new_vs.empty()) + return e; + else + return mk_delayed_abstraction_core(e, new_ns, new_vs); + } + } + /* Otherwise include all delayed substitutions */ buffer new_vs; for (unsigned i = 0; i < m_vs.size(); i++) { new_vs.push_back(lift_free_vars(m_vs[i], m_deltas[i])); @@ -195,6 +217,11 @@ struct push_delayed_abstraction_fn : public replace_visitor { m_vs.append(vs); m_deltas.resize(vs.size(), 0); } + + push_delayed_abstraction_fn(buffer const & ns, buffer const & vs, metavar_context const & mctx): + push_delayed_abstraction_fn(ns, vs) { + m_mctx = &mctx; + } }; expr push_delayed_abstraction(expr const & e) { @@ -253,7 +280,7 @@ expr mk_delayed_abstraction(expr const & e, buffer const & ns, buffer const & ls) \pre !ns.empty() */ expr mk_delayed_abstraction(expr const & e, buffer const & ns, buffer const & vs); +class metavar_context; + /* Similar to abstract_locals, but create a delayed_abstraction macro around metavariables occurring in \c e. */ -expr delayed_abstract_locals(expr const & e, unsigned nlocals, expr const * locals); -inline expr delayed_abstract_local(expr const & e, expr const & s) { return delayed_abstract_locals(e, 1, &s); } +expr delayed_abstract_locals(metavar_context const & mctx, expr const & e, unsigned nlocals, expr const * locals); void initialize_delayed_abstraction(); void finalize_delayed_abstraction(); diff --git a/src/library/type_context.cpp b/src/library/type_context.cpp index 6d490c2eda..185bdda976 100644 --- a/src/library/type_context.cpp +++ b/src/library/type_context.cpp @@ -574,7 +574,7 @@ expr type_context::abstract_locals(expr const & e, unsigned num_locals, expr con return ::lean::abstract_locals(e, num_locals, locals); } expr new_e = instantiate_mvars(e); - return delayed_abstract_locals(new_e, num_locals, locals); + return delayed_abstract_locals(m_mctx, new_e, num_locals, locals); } expr type_context::mk_binding(bool is_pi, local_context const & lctx, unsigned num_locals, expr const * locals, expr const & e) { diff --git a/tests/lean/elab_error_msgs.lean.expected.out b/tests/lean/elab_error_msgs.lean.expected.out index 42b904d529..b273001a29 100644 --- a/tests/lean/elab_error_msgs.lean.expected.out +++ b/tests/lean/elab_error_msgs.lean.expected.out @@ -1,9 +1,9 @@ elab_error_msgs.lean:2:0: error: type mismatch at application - and.rec (λ (ha : ?m_1) (hb : delayed[?m_2]) (hb : delayed[?m_3]), ha) + and.rec (λ (ha : ?m_1) (hb : ?m_2) (hb : delayed[?m_3]), ha) term - λ (ha : ?m_1) (hb : delayed[?m_2]) (hb : delayed[?m_3]), ha + λ (ha : ?m_1) (hb : ?m_2) (hb : delayed[?m_3]), ha has type - Π (ha : ?m_1) (hb : delayed[?m_2]) (hb_1 : delayed[?m_3]), delayed[?m_1] + Π (ha : ?m_1) (hb : ?m_2), delayed[?m_3] → ?m_1 but is expected to have type ?m_1 → ?m_2 → ?m_4 Additional information: diff --git a/tests/lean/run/1728.lean b/tests/lean/run/1728.lean new file mode 100644 index 0000000000..c18e097288 --- /dev/null +++ b/tests/lean/run/1728.lean @@ -0,0 +1,25 @@ +structure Bijection ( U V : Type ) := + ( morphism : U → V ) + ( inverse : V → U ) + ( witness_1 : ∀ u : U, inverse (morphism u) = u ) + ( witness_2 : ∀ v : V, morphism (inverse v) = v ) + +class Finite ( α : Type ) := + ( cardinality : nat ) + ( bijection : Bijection α (fin cardinality) ) + +lemma empty_exfalso (x : false) : empty := begin exfalso, trivial end + +instance empty_is_Finite : Finite empty := { + cardinality := 0, + bijection := begin + split, + intros, + induction u, + intros, + induction v, + trace_state, + cases is_lt, + repeat {admit} + end +}