diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp index fe2934215..b122febca 100644 --- a/src/frontends/lean/elaborator.cpp +++ b/src/frontends/lean/elaborator.cpp @@ -337,7 +337,27 @@ expr elaborator::visit_choice(expr const & e, optional const & t, constrai name_generator const & /* ngen */) { return choose(std::make_shared(*this, ctx, full_ctx, meta, type, e)); }; - justification j = mk_justification("none of the overloads is applicable", some_expr(e)); + auto pp_fn = [=](formatter const & fmt, pos_info_provider const * pos_prov, substitution const &, bool is_main) { + format r = pp_previous_error_header(fmt, pos_prov, some_expr(e), is_main); + r += format("none of the overloads is applicable:"); + for (unsigned i = 0; i < get_num_choices(e); i++) { + expr const & c = get_choice(e, i); + expr const & f = get_app_fn(c); + optional fn; + if (is_constant(f)) + fn = const_name(f); + else if (is_local(f)) + fn = local_pp_name(f); + r += space(); + if (fn) { + r += format(*fn); + } else { + r += format("[nontrivial]"); + } + } + return r; + }; + justification j = mk_justification(some_expr(e), pp_fn); cs += mk_choice_cnstr(m, fn, to_delay_factor(cnstr_group::Basic), true, j); return m; } @@ -1158,7 +1178,9 @@ expr elaborator::visit_equations(expr const & eqns, constraint_seq & cs) { new_cs.linearize(tmp_cs); for (constraint const & c : tmp_cs) { justification j = c.get_justification(); - auto pp_fn = [=](formatter const & fmt, pos_info_provider const * pp, substitution const & s) { + auto pp_fn = [=](formatter const & fmt, pos_info_provider const * pp, substitution const & s, bool is_main) { + if (!is_main) + return format(); format r = j.pp(fmt, pp, s); r += compose(line(), format("The following identifier(s) are introduced as free variables by the " "left-hand-side of the equation:")); diff --git a/src/kernel/justification.cpp b/src/kernel/justification.cpp index f27c25f47..bd4bcaef3 100644 --- a/src/kernel/justification.cpp +++ b/src/kernel/justification.cpp @@ -6,6 +6,7 @@ Author: Leonardo de Moura */ #include #include +#include #include "util/buffer.h" #include "util/int64.h" #include "util/memory_pool.h" @@ -26,6 +27,18 @@ format to_pos(optional const & e, pos_info_provider const * p) { return f + space(); } +format pp_previous_error_header(formatter const &, pos_info_provider const * pos_prov, optional const & ref, bool is_main) { + if (!is_main) { + format r = line(); + r += to_pos(ref, pos_prov); + r += format("previous error additional information"); + r += line(); + return r; + } else { + return format(); + } +} + typedef uint64 approx_set; static approx_set mk_empty_set() { return 0; } static approx_set mk_union(approx_set s1, approx_set s2) { return s1 | s2; } @@ -263,25 +276,52 @@ optional justification::get_main_expr() const { } } } -format justification::pp(formatter const & fmt, pos_info_provider const * p, substitution const & s) const { + +struct jst_hash_fn { + unsigned operator()(justification const & j) const { return j.raw()->m_hash_alloc; } +}; + +struct jst_ptr_eq { + bool operator()(justification const & j1, justification const & j2) const { return j1.raw() == j2.raw(); } +}; + +class justification_set { + std::unordered_set m_set; +public: + bool contains(justification const & j) const { return m_set.find(j) != m_set.end(); } + void insert(justification const & j) { m_set.insert(j); } +}; + +format justification::pp_core(formatter const & fmt, pos_info_provider const * p, substitution const & s, + justification_set & set, bool is_main) const { + if (set.contains(*this)) + return format(); + set.insert(*this); justification_cell * it = m_ptr; - while (true) { - if (!it) - return format(); - switch (it->m_kind) { - case justification_kind::Asserted: - return to_asserted(it)->m_fn(fmt, p, s); - case justification_kind::Wrapper: - return to_wrapper(it)->m_fn(fmt, p, s); - case justification_kind::Assumption: + if (!it) + return format(); + switch (it->m_kind) { + case justification_kind::Asserted: + return to_asserted(it)->m_fn(fmt, p, s, is_main); + case justification_kind::Wrapper: + return to_wrapper(it)->m_fn(fmt, p, s, is_main); + case justification_kind::Assumption: + if (is_main) return format(format("Assumption "), format(to_assumption(it)->m_idx)); - case justification_kind::Composite: - it = to_composite(it)->m_child[0].raw(); - break; - } + else + return format(); + case justification_kind::Composite: + return + to_composite(it)->m_child[0].pp_core(fmt, p, s, set, is_main) + + to_composite(it)->m_child[1].pp_core(fmt, p, s, set, false); } } +format justification::pp(formatter const & fmt, pos_info_provider const * p, substitution const & s) const { + justification_set set; + return pp_core(fmt, p, s, set, true); +} + justification mk_wrapper(justification const & j, optional const & s, pp_jst_fn const & fn) { return justification(new (get_wrapper_allocator().allocate()) wrapper_cell(j, fn, s)); } @@ -305,16 +345,22 @@ justification mk_justification(optional const & s, pp_jst_fn const & fn) { return justification(new (get_asserted_allocator().allocate()) asserted_cell(fn, s)); } justification mk_justification(optional const & s, pp_jst_sfn const & fn) { - return mk_justification(s, [=](formatter const & fmt, pos_info_provider const *, substitution const & subst) { + return mk_justification(s, [=](formatter const & fmt, pos_info_provider const *, substitution const & subst, bool is_main) { // Remark: we are not using to_pos(s, p) anymore because we don't try to display complicated error messages anymore. // return compose(to_pos(s, p), fn(fmt, subst)); - return fn(fmt, subst); + if (is_main) + return fn(fmt, subst); + else + return format(); }); } justification mk_justification(char const * msg, optional const & s) { std::string _msg(msg); - return mk_justification(s, [=](formatter const &, pos_info_provider const *, substitution const &) { - return format(_msg); + return mk_justification(s, [=](formatter const &, pos_info_provider const *, substitution const &, bool is_main) { + if (is_main) + return format(_msg); + else + return format(); }); } std::ostream & operator<<(std::ostream & out, justification const & j) { diff --git a/src/kernel/justification.h b/src/kernel/justification.h index 97436670f..b8cccbb35 100644 --- a/src/kernel/justification.h +++ b/src/kernel/justification.h @@ -23,7 +23,9 @@ struct justification_cell; The pp_jst_fn is a generic funciton that produces these messages. We can associate these functions to justification objects. */ -typedef std::function pp_jst_fn; +typedef std::function pp_jst_fn; + +class justification_set; /** \brief Objects used to justify unification (and level) constraints and metavariable assignments. @@ -40,6 +42,8 @@ typedef std::function pp_jst_sf /** \brief Return a format object containing position information for the given expression (if available) */ format to_pos(optional const & e, pos_info_provider const * p); +format pp_previous_error_header(formatter const &, pos_info_provider const * pos_prov, optional const & ref, bool is_main); /** \brief Provide a custom pretty printer for \c j */ justification mk_wrapper(justification const & j, optional const & s, pp_jst_fn const & fn); diff --git a/tests/lean/subset_error.lean b/tests/lean/subset_error.lean new file mode 100644 index 000000000..5736e9c36 --- /dev/null +++ b/tests/lean/subset_error.lean @@ -0,0 +1,19 @@ +constant set : Type₁ → Type₁ +constant finset : Type₁ → Type₁ +constant set.mem : Π {A : Type₁}, A → set A → Prop +constant finset.mem : Π {A : Type₁}, A → finset A → Prop + +infix ∈ := set.mem +infix ∈ := finset.mem + +definition set.subset {A : Type₁} (s₁ s₂ : set A) : Prop := +∀ ⦃a : A⦄, a ∈ s₁ → a ∈ s₂ + +definition finset.subset {A : Type₁} (s₁ s₂ : finset A) : Prop := +∀ ⦃a : A⦄, a ∈ s₁ → a ∈ s₂ + +infix `⊆`:50 := set.subset +infix `⊆`:50 := finset.subset + +example (A : Type₁) (x : A) (S H : set A) (Pin : x ∈ S) (Psub : S ⊆ H) : x ∈ H := +Psub Pin -- Error, we cannot infer at preprocessing time the binder information for Psub diff --git a/tests/lean/subset_error.lean.expected.out b/tests/lean/subset_error.lean.expected.out new file mode 100644 index 000000000..e12f28c51 --- /dev/null +++ b/tests/lean/subset_error.lean.expected.out @@ -0,0 +1,12 @@ +subset_error.lean:18:51: error: type mismatch at application + x ∈ S +term + S +has type + set A +but is expected to have type + finset A +subset_error.lean:18:51: previous error additional information +none of the overloads is applicable: finset.mem set.mem +subset_error.lean:18:66: previous error additional information +none of the overloads is applicable: finset.subset set.subset