max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat(frontends/lean/elaborator): improve error messages for eliminators

Browse source
This commit is contained in:
Leonardo de Moura 2016-09-29 11:26:55 -07:00
parent c8a720212b
commit ceeebb7e40
11 changed files with 187 additions and 32 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/frontends/lean/CMakeLists.txt
View file

@ -5,6 +5,6 @@ notation_cmd.cpp calc.cpp decl_cmds.cpp util.cpp
inductive_cmds.cpp dependencies.cpp
pp.cpp structure_cmd.cpp structure_instance.cpp
init_module.cpp type_util.cpp local_ref_info.cpp decl_attributes.cpp nested_declaration.cpp
opt_cmd.cpp prenum.cpp print_cmd.cpp elaborator.cpp
opt_cmd.cpp prenum.cpp print_cmd.cpp elaborator.cpp elaborator_exception.cpp
match_expr.cpp local_context_adapter.cpp decl_util.cpp definition_cmds.cpp
brackets.cpp tactic_notation.cpp)

83
src/frontends/lean/elaborator.cpp
View file

@ -127,6 +127,11 @@ format elaborator::pp_indent(expr const & e) {
return pp_indent(mk_pp_ctx(), e);
}
format elaborator::pp(expr const & e) {
auto fn = mk_pp_ctx();
return fn(e);
}
format elaborator::pp_overloads(pp_fn const & pp_fn, buffer<expr> const & fns) {
format r("overloads:");
r += space();
@ -303,8 +308,9 @@ auto elaborator::use_elim_elab_core(name const & fn) -> optional<elim_info> {
buffer<expr> C_args;
expr const & C = get_app_args(type, C_args);
if (!is_local(C) || C_args.empty() || !std::all_of(C_args.begin(), C_args.end(), is_local)) {
trace_elab_detail(tout() << "'eliminator' elaboration is not used for '" << fn <<
"' because resulting type is not of the expected form\n";);
format msg = format("'eliminator' elaboration is not used for '") + format(fn) +
format("' because resulting type is not of the expected form\n");
m_elim_failure_info.insert(fn, msg);
return optional<elim_info>();
}
@ -359,9 +365,10 @@ auto elaborator::use_elim_elab_core(name const & fn) -> optional<elim_info> {
for (unsigned i = 0; i < found.size(); i++) {
if (!found[i]) {
trace_elab_detail(tout() << "'eliminator' elaboration is not used for '" << fn <<
"' because did not find a (reliable) way to synthesize '" << C_args[i] << "' " <<
"which occurs in the resulting type\n";);
format msg = format("'eliminator' elaboration is not used for '") + format(fn) +
format("' because a (reliable) way to synthesize '") + pp(C_args[i]) +
format("', which occurs in the resulting type, was not found\n");
m_elim_failure_info.insert(fn, msg);
return optional<elim_info>();
}
}
@ -828,29 +835,34 @@ expr elaborator::visit_elim_app(expr const & fn, elim_info const & info, buffer<
throw elaborator_exception(ref, "\"eliminator\" elaborator failed to compute the motive");
}
/* Elaborate postponed arguments */
for (unsigned i = 0; i < new_args.size(); i++) {
if (optional<expr> arg = postponed_args[i]) {
lean_assert(is_metavar(new_args[i]));
expr new_arg_type = instantiate_mvars(infer_type(new_args[i]));
expr new_arg = visit(*arg, some_expr(new_arg_type));
if (!is_def_eq(new_args[i], new_arg)) {
auto pp_fn = mk_pp_ctx();
throw elaborator_exception(ref, format("\"eliminator\" elaborator type mismatch, term") +
pp_indent(pp_fn, new_arg) +
line() + format("has type") +
pp_indent(pp_fn, infer_type(new_arg)) +
line() + format("but is expected to have type") +
pp_indent(pp_fn, new_arg_type));
} else {
new_args[i] = new_arg;
try {
/* Elaborate postponed arguments */
for (unsigned i = 0; i < new_args.size(); i++) {
if (optional<expr> arg = postponed_args[i]) {
lean_assert(is_metavar(new_args[i]));
expr new_arg_type = instantiate_mvars(infer_type(new_args[i]));
expr new_arg = visit(*arg, some_expr(new_arg_type));
if (!is_def_eq(new_args[i], new_arg)) {
auto pp_fn = mk_pp_ctx();
throw elaborator_exception(ref, format("\"eliminator\" elaborator type mismatch, term") +
pp_indent(pp_fn, new_arg) +
line() + format("has type") +
pp_indent(pp_fn, infer_type(new_arg)) +
line() + format("but is expected to have type") +
pp_indent(pp_fn, new_arg_type));
} else {
new_args[i] = new_arg;
}
}
}
}
expr r = instantiate_mvars(mk_app(mk_app(fn, new_args), extra_args));
trace_elab_debug(tout() << "elaborated recursor:\n " << r << "\n";);
return r;
expr r = instantiate_mvars(mk_app(mk_app(fn, new_args), extra_args));
trace_elab_debug(tout() << "elaborated recursor:\n " << r << "\n";);
return r;
} catch (elaborator_exception & ex) {
throw nested_elaborator_exception(ref, ex, format("the inferred motive for the eliminator-like application is") +
pp_indent(motive));
}
}
struct elaborator::first_pass_info {
@ -1320,12 +1332,27 @@ expr elaborator::visit_app_core(expr fn, buffer<expr> const & args, optional<exp
if (args.size() >= info->m_nexplicit) {
return visit_elim_app(new_fn, *info, args, expected_type, ref);
} else {
trace_elab(tout() << pos_string_for(ref) << " 'eliminator' elaboration is not used for '" << fn <<
"' because it is not fully applied, #" << info->m_nexplicit <<
" explicit arguments expected\n";);
try {
return visit_base_app(new_fn, amask, args, expected_type, ref);
} catch (elaborator_exception & ex) {
throw nested_elaborator_exception(ref, ex,
format("'eliminator' elaboration was not used for '") +
pp(fn) + format("' because it is not fully applied, #") +
format(info->m_nexplicit) + format(" explicit arguments expected"));
}
}
} else if (is_no_confusion(m_env, const_name(new_fn))) {
return visit_no_confusion_app(new_fn, args, expected_type, ref);
} else {
try {
return visit_base_app(new_fn, amask, args, expected_type, ref);
} catch (elaborator_exception & ex) {
if (auto error_msg = m_elim_failure_info.find(const_name(new_fn))) {
throw nested_elaborator_exception(ref, ex, *error_msg);
} else {
throw;
}
}
}
}
return visit_base_app(new_fn, amask, args, expected_type, ref);

3
src/frontends/lean/elaborator.h
View file

@ -68,7 +68,9 @@ private:
/** \brief Cache for constants that are handled using "eliminator" elaboration. */
typedef name_map<optional<elim_info>> elim_cache;
typedef name_map<format> elim_failure_info;
elim_cache m_elim_cache;
elim_failure_info m_elim_failure_info;
/* The following vector contains sorts that we should check
whether the computed universe is too specific or not. */
@ -89,6 +91,7 @@ private:
pp_fn mk_pp_ctx();
format pp_indent(pp_fn const & pp_fn, expr const & e);
format pp_indent(expr const & e);
format pp(expr const & e);
format pp_overloads(pp_fn const & pp_fn, buffer<expr> const & fns);
expr whnf(expr const & e) { return m_ctx.whnf(e); }

42
src/frontends/lean/elaborator_exception.cpp Normal file
View file

@ -0,0 +1,42 @@
/*
Copyright (c) 2016 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#include "library/scope_pos_info_provider.h"
#include "frontends/lean/elaborator_exception.h"
namespace lean {
throwable * elaborator_exception::clone() const {
return new elaborator_exception(m_expr, m_fmt);
}
throwable * nested_elaborator_exception::clone() const {
return new nested_elaborator_exception(m_expr, m_fmt, m_exception);
}
optional<expr> nested_elaborator_exception::get_main_expr() const {
if (auto r = m_exception->get_main_expr()) return r;
else return m_expr;
}
format nested_elaborator_exception::pp() const {
format r = m_exception->pp();
if (dynamic_cast<nested_elaborator_exception*>(m_exception.get()) == nullptr) {
r += line() + format("Additional information:");
}
pos_info_provider * pip = get_pos_info_provider();
if (pip && m_expr) {
if (auto p = pip->get_pos_info(*m_expr)) {
r += line() + format(pip->get_file_name()) +
colon() + format(p->first) + colon() + format(p->second) + colon() + space() + format("context: ") + m_fmt;
} else {
r += line() + format("context: ") + m_fmt;
}
} else {
r += line() + format("context: ") + m_fmt;
}
return r;
}
}

21
src/frontends/lean/elaborator_exception.h
View file

@ -5,16 +5,35 @@ Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#pragma once
#include "util/sstream.h"
#include "library/io_state.h"
namespace lean {
class elaborator_exception : public formatted_exception {
protected:
elaborator_exception(optional<expr> const & e, format const & fmt):formatted_exception(e, fmt) {}
public:
elaborator_exception(expr const & e, format const & fmt):formatted_exception(e, fmt) {}
elaborator_exception(expr const & e, sstream const & strm):formatted_exception(e, format(strm.str())) {}
elaborator_exception(expr const & e, char const * msg):formatted_exception(e, format(msg)) {}
virtual throwable * clone() const override { return new elaborator_exception(m_expr, m_fmt); }
virtual throwable * clone() const override;
virtual void rethrow() const override { throw *this; }
};
class nested_elaborator_exception : public elaborator_exception {
std::shared_ptr<elaborator_exception> m_exception;
nested_elaborator_exception(optional<expr> const & ref, format const & fmt,
std::shared_ptr<elaborator_exception> const & ex):
elaborator_exception(ref, fmt), m_exception(ex) {}
public:
nested_elaborator_exception(optional<expr> const & ref, elaborator_exception const & ex, format const & fmt):
elaborator_exception(ref, fmt),
m_exception(static_cast<elaborator_exception*>(ex.clone())) {}
nested_elaborator_exception(expr const & ref, elaborator_exception const & ex, format const & fmt):
nested_elaborator_exception(some_expr(ref), ex, fmt) {}
virtual void rethrow() const override { throw *this; }
virtual throwable * clone() const override;
virtual optional<expr> get_main_expr() const override;
virtual format pp() const override;
};
}

4
src/library/io_state.h
View file

@ -67,8 +67,8 @@ public:
virtual char const * what() const noexcept;
virtual throwable * clone() const { return new formatted_exception(m_expr, m_fmt); }
virtual void rethrow() const { throw *this; }
optional<expr> get_main_expr() const { return m_expr; }
format pp() const { return m_fmt; }
virtual optional<expr> get_main_expr() const { return m_expr; }
virtual format pp() const { return m_fmt; }
};
struct scope_global_ios {

5
tests/lean/def1.lean.expected.out
View file

@ -4,3 +4,8 @@ has type
?m_2 = ?m_2
but is expected to have type
f b = f c
Additional information:
def1.lean:5:16: context: the inferred motive for the eliminator-like application is
λ (_x : A), f _x = f c
def1.lean:5:3: context: the inferred motive for the eliminator-like application is
λ (_x : A), f a = f c

14
tests/lean/elab_error_msgs.lean Normal file
View file

@ -0,0 +1,14 @@
lemma ex1 (a b : Prop) : a ∧ b ∧ b → b ∧ a :=
and.rec (λ ha hb hb, ha)
@[elab_as_eliminator]
def bogus_elim {A : Type} {C : A → A → Prop} {a b : A} (h : C a a) : C a b :=
sorry
lemma ex2 (a b : Prop) : a ∧ b :=
bogus_elim trivial
lemma ex1 (a b : Prop) : a ∧ b ∧ b → b ∧ a :=
λ h, and.rec
(λ ha hb, ha + hb)
h

30
tests/lean/elab_error_msgs.lean.expected.out Normal file
View file

@ -0,0 +1,30 @@
elab_error_msgs.lean:2:0: error: type mismatch at application
and.rec (λ (ha : ?m_1) (hb : delayed[?m_2]) (hb : delayed[?m_4]), ha)
term
λ (ha : ?m_1) (hb : delayed[?m_2]) (hb : delayed[?m_4]), ha
has type
Π (ha : ?m_1) (hb : delayed[?m_2]) (hb_1 : delayed[?m_4]), delayed[?m_1]
but is expected to have type
?m_1 → ?m_2 → ?m_3
Additional information:
elab_error_msgs.lean:2:0: context: 'eliminator' elaboration was not used for 'and.rec' because it is not fully applied, #2 explicit arguments expected
elab_error_msgs.lean:9:0: error: type mismatch at application
bogus_elim trivial
term
trivial
has type
true
but is expected to have type
?m_2 ?m_3 ?m_3
Additional information:
elab_error_msgs.lean:9:0: context: 'eliminator' elaboration is not used for 'bogus_elim' because a (reliable) way to synthesize 'a', which occurs in the resulting type, was not found
elab_error_msgs.lean:13:20: error: failed to synthesize type class instance for
a b : Prop,
h : a ∧ b ∧ b,
ha : a,
hb : b ∧ b
⊢ has_add (b ∧ a)
Additional information:
elab_error_msgs.lean:12:5: context: the inferred motive for the eliminator-like application is
b ∧ a

9
tests/lean/hole_issue2.lean.expected.out
View file

@ -9,6 +9,9 @@ h : ⟦l₁⟧ ⊆ ⟦l₂⟧,
w : A,
hw : ¬list.count w l₁ ≤ list.count w l₂
⊢ false
Additional information:
hole_issue2.lean:19:0: context: the inferred motive for the eliminator-like application is
λ (_x _x_1 : bag A), decidable (_x ⊆ _x_1)
hole_issue2.lean:29:65: error: don't know how to synthesize placeholder
state:
A : Type,
@ -18,6 +21,9 @@ _match : Π (b : bool), subcount l₁ l₂ = b → decidable (⟦l₁⟧ ⊆ ⟦
H : subcount l₁ l₂ = ff,
h : ⟦l₁⟧ ⊆ ⟦l₂⟧
⊢ ∀ (a : A), ¬list.count a l₁ ≤ list.count a l₂ → false
Additional information:
hole_issue2.lean:26:0: context: the inferred motive for the eliminator-like application is
λ (_x _x_1 : bag A), decidable (_x ⊆ _x_1)
hole_issue2.lean:36:28: error: don't know how to synthesize placeholder
state:
A : Type,
@ -27,3 +33,6 @@ _match : Π (b : bool), subcount l₁ l₂ = b → decidable (⟦l₁⟧ ⊆ ⟦
H : subcount l₁ l₂ = ff,
h : ⟦l₁⟧ ⊆ ⟦l₂⟧
⊢ false
Additional information:
hole_issue2.lean:33:0: context: the inferred motive for the eliminator-like application is
λ (_x _x_1 : bag A), decidable (_x ⊆ _x_1)

6
tests/lean/red.lean.expected.out
View file

@ -10,9 +10,15 @@ has type
?m_2 = ?m_2
but is expected to have type
f a = a
Additional information:
red.lean:12:0: context: the inferred motive for the eliminator-like application is
λ (_x : ℕ), f a = a
red.lean:17:0: error: "eliminator" elaborator type mismatch, term
rfl
has type
?m_2 = ?m_2
but is expected to have type
f a = a
Additional information:
red.lean:17:0: context: the inferred motive for the eliminator-like application is
λ (_x : ℕ), f a = a