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

feat(library/equations_compiler): error recovery

Browse source
This commit is contained in:
Gabriel Ebner 2017-07-08 09:15:45 +02:00 • committed by Leonardo de Moura
parent bac64d49c9
commit 246d71f3ff
15 changed files with 161 additions and 131 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -245,18 +245,6 @@ expr elaborator::recoverable_error(optional<expr> const & expected_type, expr co
return mk_sorry(expected_type, ref);
}
template <class Fn>
expr elaborator::recover_expr_from_exception(optional<expr> const & expected_type, expr const & ref, Fn && fn) {
try {
return fn();
} catch (std::exception & ex) {
if (!try_report(ex, some_expr(ref))) {
throw;
} else {
return mk_sorry(expected_type, ref);
}
}
}
level elaborator::mk_univ_metavar() {
return m_ctx.mk_univ_metavar_decl();
@ -2372,7 +2360,7 @@ expr elaborator::visit_equations(expr const & e) {
new_e = instantiate_mvars(new_e);
ensure_no_unassigned_metavars(new_e);
metavar_context mctx = m_ctx.mctx();
expr r = compile_equations(m_env, m_opts, mctx, m_ctx.lctx(), new_e);
expr r = compile_equations(m_env, m_opts, mctx, m_ctx.lctx(), new_e, *this);
m_ctx.set_env(m_env);
m_ctx.set_mctx(mctx);
return r;

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

@ -157,6 +157,8 @@ private:
bool has_synth_sorry(expr const & e) { return has_synth_sorry({e}); }
bool has_synth_sorry(std::initializer_list<expr> && es);
public:
bool try_report(std::exception const & ex);
bool try_report(std::exception const & ex, optional<expr> const & ref);
void report_or_throw(elaborator_exception const & ex);
@ -165,6 +167,7 @@ private:
expr recoverable_error(optional<expr> const & expected_type, expr const & ref, elaborator_exception const & ex);
template <class Fn> expr recover_expr_from_exception(optional<expr> const & expected_type, expr const & ref, Fn &&);
private:
expr ensure_type(expr const & e, expr const & ref);
expr ensure_function(expr const & e, expr const & ref);
optional<expr> ensure_has_type(expr const & e, expr const & e_type, expr const & type, expr const & ref);
@ -343,6 +346,19 @@ public:
bool has_errors() const { return m_has_errors; }
};
template <class Fn>
expr elaborator::recover_expr_from_exception(optional<expr> const & expected_type, expr const & ref, Fn && fn) {
try {
return fn();
} catch (std::exception & ex) {
if (!try_report(ex, some_expr(ref))) {
throw;
} else {
return mk_sorry(expected_type, ref);
}
}
}
pair<expr, level_param_names> elaborate(environment & env, options const & opts, name const & decl_name,
metavar_context & mctx, local_context const & lctx,
expr const & e, bool check_unassigned, bool recover_from_errors);

25
src/library/equations_compiler/compiler.cpp
View file

@ -17,6 +17,7 @@ Author: Leonardo de Moura
#include "library/equations_compiler/unbounded_rec.h"
#include "library/equations_compiler/wf_rec.h"
#include "library/equations_compiler/elim_match.h"
#include "frontends/lean/elaborator.h"
namespace lean {
#define trace_compiler(Code) lean_trace("eqn_compiler", scope_trace_env _scope1(ctx.env(), ctx); Code)
@ -29,7 +30,7 @@ static bool has_nested_rec(expr const & eqns) {
static eqn_compiler_result compile_equations_core(environment & env, options const & opts,
metavar_context & mctx, local_context const & lctx,
expr const & eqns) {
expr const & eqns, elaborator & elab) {
type_context ctx(env, opts, mctx, lctx, transparency_mode::Semireducible);
trace_compiler(tout() << "compiling\n" << eqns << "\n";);
trace_compiler(tout() << "recursive: " << is_recursive_eqns(ctx, eqns) << "\n";);
@ -42,22 +43,22 @@ static eqn_compiler_result compile_equations_core(environment & env, options con
if (is_wf_equations(eqns)) {
throw exception("invalid use of 'using_well_founded', we do not need to use well founded recursion for meta definitions, since they can use unbounded recursion");
}
return unbounded_rec(env, opts, mctx, lctx, eqns);
return unbounded_rec(env, opts, mctx, lctx, eqns, elab);
}
if (is_wf_equations(eqns)) {
return wf_rec(env, opts, mctx, lctx, eqns);
return wf_rec(env, opts, mctx, lctx, eqns, elab);
}
if (header.m_num_fns == 1) {
if (!is_recursive_eqns(ctx, eqns)) {
return mk_nonrec(env, opts, mctx, lctx, eqns);
} else if (auto r = try_structural_rec(env, opts, mctx, lctx, eqns)) {
return mk_nonrec(env, opts, mctx, lctx, eqns, elab);
} else if (auto r = try_structural_rec(env, opts, mctx, lctx, eqns, elab)) {
return *r;
}
}
return wf_rec(env, opts, mctx, lctx, eqns);
return wf_rec(env, opts, mctx, lctx, eqns, elab);
}
/** Auxiliary class for pulling nested recursive calls.
@ -276,11 +277,11 @@ struct pull_nested_rec_fn : public replace_visitor {
}
}
eqn_compiler_result operator()(expr const & e) {
eqn_compiler_result operator()(expr const & e, elaborator & elab) {
expr new_e = visit(e);
lean_assert(m_lctx_stack.size() == 1);
local_context new_lctx = m_lctx_stack[0];
auto r = compile_equations_core(m_env, m_opts, m_mctx, new_lctx, new_e);
auto r = compile_equations_core(m_env, m_opts, m_mctx, new_lctx, new_e, elab);
type_context ctx = mk_type_context(new_lctx);
r.m_fns = map(r.m_fns, [&] (expr const & fn) { return replace_locals(fn, m_new_locals, m_new_values); });
m_mctx = ctx.mctx();
@ -302,14 +303,14 @@ static expr remove_aux_main_name(expr const & e) {
}
expr compile_equations(environment & env, options const & opts, metavar_context & mctx, local_context const & lctx,
expr const & _eqns) {
expr const & _eqns, elaborator & elab) {
expr eqns = _eqns;
equations_header const & header = get_equations_header(eqns);
eqn_compiler_result r;
if (!header.m_is_meta && has_nested_rec(eqns)) {
r = pull_nested_rec_fn(env, opts, mctx, lctx)(eqns);
r = pull_nested_rec_fn(env, opts, mctx, lctx)(eqns, elab);
} else {
r = compile_equations_core(env, opts, mctx, lctx, eqns);
r = compile_equations_core(env, opts, mctx, lctx, eqns, elab);
}
if (r.m_counter_examples) {
@ -318,7 +319,7 @@ expr compile_equations(environment & env, options const & opts, metavar_context
for (auto & ce : r.m_counter_examples) {
fmt += line() + pp(remove_aux_main_name(ce));
}
throw formatted_exception(_eqns, fmt);
elab.report_or_throw({_eqns, fmt});
}
buffer<expr> fns; to_buffer(r.m_fns, fns);

3
src/library/equations_compiler/compiler.h
View file

@ -8,8 +8,9 @@ Author: Leonardo de Moura
#include "library/metavar_context.h"
#include "library/equations_compiler/equations.h"
namespace lean {
class elaborator;
expr compile_equations(environment & env, options const & opts, metavar_context & mctx, local_context const & lctx,
expr const & eqns);
expr const & eqns, elaborator & elab);
void initialize_compiler();
void finalize_compiler();
}

97
src/library/equations_compiler/elim_match.cpp
View file

@ -38,6 +38,7 @@ Author: Leonardo de Moura
#include "library/equations_compiler/equations.h"
#include "library/equations_compiler/util.h"
#include "library/equations_compiler/elim_match.h"
#include "frontends/lean/elaborator.h"
#ifndef LEAN_DEFAULT_EQN_COMPILER_ITE
#define LEAN_DEFAULT_EQN_COMPILER_ITE true
@ -66,6 +67,7 @@ struct elim_match_fn {
environment m_env;
options m_opts;
metavar_context m_mctx;
elaborator & m_elab;
expr m_ref;
unsigned m_depth{0};
@ -73,6 +75,8 @@ struct elim_match_fn {
bool m_aux_lemmas;
unsigned m_num_steps{0};
bool m_error_during_process = false;
/* configuration options */
bool m_use_ite;
unsigned m_max_steps;
@ -82,8 +86,8 @@ struct elim_match_fn {
name_map<bool> m_enum;
elim_match_fn(environment const & env, options const & opts,
metavar_context const & mctx):
m_env(env), m_opts(opts), m_mctx(mctx) {
metavar_context const & mctx, elaborator & elab):
m_env(env), m_opts(opts), m_mctx(mctx), m_elab(elab) {
m_use_ite = get_eqn_compiler_ite(opts);
m_max_steps = get_eqn_compiler_max_steps(opts);
}
@ -1237,41 +1241,43 @@ struct elim_match_fn {
trace_match(tout() << "depth [" << m_depth << "]\n" << pp_problem(P) << "\n";);
lean_assert(check_problem(P));
m_num_steps++;
if (m_num_steps > m_max_steps) {
throw_error(sstream() << "equation compiler failed, maximum number of steps (" << m_max_steps << ") exceeded"
<< " (possible solution: use 'set_option eqn_compiler.max_steps <new-threshold>')"
<< " (use 'set_option trace.eqn_compiler.elim_match true' for additional details)");
}
if (P.m_var_stack) {
if (!P.m_equations) {
return process_no_equation(P);
} else if (!is_next_var(P)) {
return process_non_variable(P);
} else if (is_variable_transition(P)) {
return process_variable(P);
} else if (is_value_transition(P)) {
return process_value(P);
} else if (is_complete_transition(P)) {
return process_complete(P);
} else if (is_constructor_transition(P)) {
return process_constructor(P);
} else if (is_transport_transition(P)) {
return process_transport(P);
} else if (is_inaccessible_transition(P)) {
return process_inaccessible(P);
} else {
trace_match(tout() << "compilation failed at\n" << pp_problem(P) << "\n";);
if (!m_unsolved.empty()) {
// report non-exhaustive match
m_mctx.assign(P.m_goal, mk_sorry(m_mctx.get_metavar_decl(P.m_goal).get_type(), true));
return list<lemma>();
}
throw_error("equation compiler failed (use 'set_option trace.eqn_compiler.elim_match true' "
"for additional details)");
try {
if (m_num_steps > m_max_steps) {
throw_error(sstream() << "equation compiler failed, maximum number of steps (" << m_max_steps << ") exceeded"
<< " (possible solution: use 'set_option eqn_compiler.max_steps <new-threshold>')"
<< " (use 'set_option trace.eqn_compiler.elim_match true' for additional details)");
}
} else {
return process_leaf(P);
if (P.m_var_stack) {
if (!P.m_equations) {
return process_no_equation(P);
} else if (!is_next_var(P)) {
return process_non_variable(P);
} else if (is_variable_transition(P)) {
return process_variable(P);
} else if (is_value_transition(P)) {
return process_value(P);
} else if (is_complete_transition(P)) {
return process_complete(P);
} else if (is_constructor_transition(P)) {
return process_constructor(P);
} else if (is_transport_transition(P)) {
return process_transport(P);
} else if (is_inaccessible_transition(P)) {
return process_inaccessible(P);
} else {
trace_match(tout() << "compilation failed at\n" << pp_problem(P) << "\n";);
throw_error("equation compiler failed (use 'set_option trace.eqn_compiler.elim_match true' "
"for additional details)");
}
} else {
return process_leaf(P);
}
} catch (exception & ex) {
if (!m_elab.try_report(ex, some_expr(m_ref))) throw;
m_error_during_process = true;
m_mctx.assign(P.m_goal, mk_sorry(m_mctx.get_metavar_decl(P.m_goal).get_type(), true));
}
return list<lemma>();
}
expr finalize_lemma(expr const & fn, lemma const & L) {
@ -1313,12 +1319,14 @@ struct elim_match_fn {
expr ref = eqns_buffer[i];
while (is_lambda(ref)) ref = binding_body(ref);
if (j != i) {
throw generic_exception(ref, sstream() << "equation compiler error, equation #" << (i+1)
m_elab.report_or_throw(elaborator_exception(ref,
sstream() << "equation compiler error, equation #" << (i+1)
<< " has not been used in the compilation, note that the left-hand-side of equation #" << (j+1)
<< " is a variable");
<< " is a variable"));
} else {
throw generic_exception(ref, sstream() << "equation compiler error, equation #" << (i+1)
<< " has not been used in the compilation (possible solution: delete equation)");
m_elab.report_or_throw(elaborator_exception(ref,
sstream() << "equation compiler error, equation #" << (i+1)
<< " has not been used in the compilation (possible solution: delete equation)"));
}
}
}
@ -1354,7 +1362,8 @@ struct elim_match_fn {
lean_assert(check_problem(P));
list<lemma> pre_Ls = process(P);
auto counter_examples = get_counter_examples();
if (!counter_examples) check_no_unused_eqns(eqns);
if (!counter_examples && !m_error_during_process)
check_no_unused_eqns(eqns);
fn = m_mctx.instantiate_mvars(fn);
trace_match_debug(tout() << "code:\n" << fn << "\n";);
list<expr> Ls = finalize_lemmas(fn, pre_Ls);
@ -1363,8 +1372,8 @@ struct elim_match_fn {
};
elim_match_result elim_match(environment & env, options const & opts, metavar_context & mctx,
local_context const & lctx, expr const & eqns) {
elim_match_fn elim(env, opts, mctx);
local_context const & lctx, expr const & eqns, elaborator & elab) {
elim_match_fn elim(env, opts, mctx, elab);
auto r = elim(lctx, eqns);
env = elim.m_env;
return r;
@ -1378,9 +1387,9 @@ static expr get_fn_type_from_eqns(expr const & eqns) {
}
eqn_compiler_result mk_nonrec(environment & env, options const & opts, metavar_context & mctx,
local_context const & lctx, expr const & eqns) {
local_context const & lctx, expr const & eqns, elaborator & elab) {
equations_header header = get_equations_header(eqns);
auto R = elim_match(env, opts, mctx, lctx, eqns);
auto R = elim_match(env, opts, mctx, lctx, eqns, elab);
if (header.m_is_meta || header.m_is_lemma) {
/* Do not generate auxiliary equation or equational lemmas */
auto fn = mk_constant(head(header.m_fn_names));

7
src/library/equations_compiler/elim_match.h
View file

@ -8,14 +8,17 @@ Author: Leonardo de Moura
#include "library/type_context.h"
#include "library/equations_compiler/util.h"
namespace lean {
class elaborator;
struct elim_match_result {
expr m_fn;
list<expr> m_lemmas;
list<list<expr>> m_counter_examples;
};
elim_match_result elim_match(environment & env, options const & opts, metavar_context & mctx, local_context const & lctx, expr const & eqns);
elim_match_result elim_match(environment & env, options const & opts, metavar_context & mctx,
local_context const & lctx, expr const & eqns, elaborator & elab);
eqn_compiler_result mk_nonrec(environment & env, options const & opts, metavar_context & mctx,
local_context const & lctx, expr const & eqns);
local_context const & lctx, expr const & eqns,
elaborator & elab);
void initialize_elim_match();
void finalize_elim_match();
}

8
src/library/equations_compiler/structural_rec.cpp
View file

@ -957,12 +957,12 @@ struct structural_rec_fn {
}
}
optional<eqn_compiler_result> operator()(expr const & eqns) {
optional<eqn_compiler_result> operator()(expr const & eqns, elaborator & elab) {
m_ref = eqns;
m_header = get_equations_header(eqns);
auto new_eqns = elim_recursion(eqns);
if (!new_eqns) return {};
elim_match_result R = elim_match(m_env, m_opts, m_mctx, m_lctx, *new_eqns);
elim_match_result R = elim_match(m_env, m_opts, m_mctx, m_lctx, *new_eqns, elab);
expr fn = mk_function(R.m_fn);
if (m_header.m_aux_lemmas) {
lean_assert(!m_header.m_is_meta);
@ -977,9 +977,9 @@ struct structural_rec_fn {
};
optional<eqn_compiler_result> try_structural_rec(environment & env, options const & opts, metavar_context & mctx,
local_context const & lctx, expr const & eqns) {
local_context const & lctx, expr const & eqns, elaborator & elab) {
structural_rec_fn F(env, opts, mctx, lctx);
if (auto r = F(eqns)) {
if (auto r = F(eqns, elab)) {
env = F.env();
mctx = F.mctx();
return r;

3
src/library/equations_compiler/structural_rec.h
View file

@ -8,6 +8,7 @@ Author: Leonardo de Moura
#include "library/type_context.h"
#include "library/equations_compiler/util.h"
namespace lean {
class elaborator;
/** \brief Try to eliminate "recursive calls" in the equations \c eqns by using brec_on's below.
If successful, elim_match is used to compile pattern matching.
@ -17,7 +18,7 @@ namespace lean {
construction, where every recursive call is structurally smaller. */
optional<eqn_compiler_result> try_structural_rec(environment & env, options const & opts,
metavar_context & mctx, local_context const & lctx,
expr const & eqns);
expr const & eqns, elaborator & elab);
void initialize_structural_rec();
void finalize_structural_rec();

4
src/library/equations_compiler/unbounded_rec.cpp
View file

@ -36,10 +36,10 @@ static expr replace_rec_apps(type_context & ctx, expr const & e) {
eqn_compiler_result unbounded_rec(environment & env, options const & opts,
metavar_context & mctx, local_context const & lctx,
expr const & e) {
expr const & e, elaborator & elab) {
type_context ctx(env, opts, mctx, lctx, transparency_mode::Semireducible);
expr e1 = replace_rec_apps(ctx, e);
auto R = elim_match(env, opts, mctx, lctx, e1);
auto R = elim_match(env, opts, mctx, lctx, e1, elab);
list<expr> counter_examples;
if (R.m_counter_examples) {

3
src/library/equations_compiler/unbounded_rec.h
View file

@ -8,11 +8,12 @@ Author: Leonardo de Moura
#include "library/type_context.h"
#include "library/equations_compiler/util.h"
namespace lean {
class elaborator;
/** \brief Eliminate "recursive calls" using rec_fn_macro.
This compilation step can only be used to compile meta definitions.
If we use it on regular definitions, the kernel will reject it. */
eqn_compiler_result unbounded_rec(environment & env, options const & opts,
metavar_context & mctx, local_context const & lctx,
expr const & eqns);
expr const & eqns, elaborator & elab);
}

94
src/library/equations_compiler/wf_rec.cpp
View file

@ -12,6 +12,7 @@ Author: Leonardo de Moura
#include "library/pp_options.h"
#include "library/app_builder.h"
#include "library/aux_definition.h"
#include "frontends/lean/elaborator.h"
#include "library/replace_visitor_with_tc.h"
#include "library/vm/vm.h"
#include "library/vm/vm_list.h"
@ -33,6 +34,7 @@ struct wf_rec_fn {
options m_opts;
metavar_context m_mctx;
local_context m_lctx;
elaborator & m_elab;
expr m_ref;
equations_header m_header;
@ -43,8 +45,9 @@ struct wf_rec_fn {
expr m_dec_tac;
wf_rec_fn(environment const & env, options const & opts,
metavar_context const & mctx, local_context const & lctx):
m_env(env), m_opts(opts), m_mctx(mctx), m_lctx(lctx) {
metavar_context const & mctx, local_context const & lctx,
elaborator & elab):
m_env(env), m_opts(opts), m_mctx(mctx), m_lctx(lctx), m_elab(elab) {
}
type_context mk_type_context(local_context const & lctx) {
@ -154,18 +157,48 @@ struct wf_rec_fn {
metavar_context mctx = m_ctx.mctx();
tactic_state s = mk_tactic_state_for(m_parent.m_env, m_parent.m_opts,
name(m_fn_name, "_wf_rec_mk_dec_tactic"), mctx, m_ctx.lctx(), y_R_x);
vm_obj r = tactic_evaluator(m_ctx, m_parent.m_opts, ref)(m_parent.m_dec_tac, s);
if (auto new_s = tactic::is_success(r)) {
mctx = new_s->mctx();
bool postpone_push_delayed = true;
expr r = mctx.instantiate_mvars(new_s->main(), postpone_push_delayed);
m_parent.m_env = new_s->env();
m_ctx.set_env(new_s->env());
m_ctx.set_mctx(mctx);
return r;
try {
vm_obj r = tactic_evaluator(m_ctx, m_parent.m_opts, ref)(m_parent.m_dec_tac, s);
if (auto new_s = tactic::is_success(r)) {
mctx = new_s->mctx();
bool postpone_push_delayed = true;
expr r = mctx.instantiate_mvars(new_s->main(), postpone_push_delayed);
m_parent.m_env = new_s->env();
m_ctx.set_env(new_s->env());
m_ctx.set_mctx(mctx);
return r;
}
} catch (elaborator_exception & ex) {
bool using_well_founded = is_wf_equations(m_parent.m_ref);
auto R = m_parent.m_R;
nested_exception ex2(
ex.get_pos(),
[=](formatter const & fmt) {
format r;
formatter _fmt = fmt;
if (is_app_of(R, get_has_well_founded_r_name())) {
options o = fmt.get_options();
o = o.update_if_undef(get_pp_implicit_name(), true);
_fmt = fmt.update_options(o);
}
r += format("failed to prove recursive application is decreasing, well founded relation");
r += pp_indent_expr(_fmt, R);
if (!using_well_founded) {
r += line() + format("Possible solutions: ");
r += line() + format(" - Use 'using_well_founded' keyword in the end of your definition "
"to specify tactics for synthesizing well founded relations and "
"decreasing proofs.");
r += line() + format(" - The default decreasing tactic uses the 'assumption' tactic, "
"thus hints (aka local proofs) can be provided using 'have'-expressions.");
}
r += line() + format("The nested exception contains the failure state for the decreasing tactic.");
return r;
},
ex);
if (!m_parent.m_elab.try_report(ex2)) throw ex2;
}
throw generic_exception(ref, "failed to show recursive call is descreasing");
return m_parent.m_elab.mk_sorry(y_R_x);
}
virtual expr visit_app(expr const & e) {
@ -517,40 +550,11 @@ struct wf_rec_fn {
init(eqns, wf_tacs);
/* Eliminate recursion using functional. */
try {
eqns = elim_recursion(eqns);
} catch (exception_with_pos & ex) {
expr R = m_R;
bool using_well_founded = is_wf_equations(eqns);
throw nested_exception(
ex.get_pos(),
[=](formatter const & fmt) {
format r;
formatter _fmt = fmt;
if (is_app_of(R, get_has_well_founded_r_name())) {
options o = fmt.get_options();
o = o.update_if_undef(get_pp_implicit_name(), true);
_fmt = fmt.update_options(o);
}
r += format("failed to prove recursive application is decreasing, well founded relation");
r += pp_indent_expr(_fmt, R);
if (!using_well_founded) {
r += line() + format("Possible solutions: ");
r += line() + format(" - Use 'using_well_founded' keyword in the end of your definition "
"to specify tactics for synthesizing well founded relations and "
"decreasing proofs.");
r += line() + format(" - The default decreasing tactic uses the 'assumption' tactic, "
"thus hints (aka local proofs) can be provided using 'have'-expressions.");
}
r += line() + format("The nested exception contains the failure state for the decreasing tactic.");
return r;
},
ex);
}
eqns = elim_recursion(eqns);
trace_debug_wf(tout() << "after elim_recursion\n" << eqns << "\n";);
/* Eliminate pattern matching */
elim_match_result r = elim_match(m_env, m_opts, m_mctx, m_lctx, eqns);
elim_match_result r = elim_match(m_env, m_opts, m_mctx, m_lctx, eqns, m_elab);
expr fn = mk_fix_aux_function(get_equations_header(eqns), r.m_fn);
trace_debug_wf(tout() << "after mk_fix\n" << fn << " :\n " << mk_type_context().infer(fn) << "\n";);
@ -567,8 +571,8 @@ struct wf_rec_fn {
If successful, elim_match is used to compile pattern matching. */
eqn_compiler_result wf_rec(environment & env, options const & opts,
metavar_context & mctx, local_context const & lctx,
expr const & eqns) {
wf_rec_fn proc(env, opts, mctx, lctx);
expr const & eqns, elaborator & elab) {
wf_rec_fn proc(env, opts, mctx, lctx, elab);
auto r = proc(eqns);
env = proc.m_env;
mctx = proc.m_mctx;

3
src/library/equations_compiler/wf_rec.h
View file

@ -8,9 +8,10 @@ Author: Leonardo de Moura
#include "library/type_context.h"
#include "library/equations_compiler/util.h"
namespace lean {
class elaborator;
eqn_compiler_result wf_rec(environment & env, options const & opts,
metavar_context & mctx, local_context const & lctx,
expr const & eqns);
expr const & eqns, elaborator & elab);
void initialize_wf_rec();
void finalize_wf_rec();
}

2
tests/lean/1162.lean.expected.out
View file

@ -1 +1,3 @@
1162.lean:10:12: error: equation compiler error, equation #2 has not been used in the compilation, note that the left-hand-side of equation #1 is a variable
1162.lean:11:12: error: equation compiler error, equation #3 has not been used in the compilation, note that the left-hand-side of equation #1 is a variable
1162.lean:12:12: error: equation compiler error, equation #4 has not been used in the compilation, note that the left-hand-side of equation #1 is a variable

3
tests/lean/elab_error_recovery.lean
View file

@ -9,7 +9,8 @@ def half_baked : ℕ → ℕ
-- exceptions during tactic evaluation
| 7 := by do undefined
-- nested elaboration errors
| _ := begin exact [] end
| 10 := begin exact [] end
-- missing cases
#print half_baked._main

10
tests/lean/elab_error_recovery.lean.expected.out
View file

@ -19,8 +19,7 @@ elab_error_recovery.lean:12:20: error: invalid type ascription, expression has t
but is expected to have type
ℕ
state:
half_baked : ℕ → ℕ,
_x : ℕ
half_baked : ℕ → ℕ
⊢ ℕ
elab_error_recovery.lean:6:8: error: don't know how to synthesize placeholder
context:
@ -30,15 +29,18 @@ elab_error_recovery.lean:8:29: error: don't know how to synthesize placeholder
context:
half_baked : ℕ → ℕ
⊢ ℕ
elab_error_recovery.lean:1:4: error: non-exhaustive match, the following cases are missing:
half_baked _
def half_baked._main : ℕ → ℕ :=
λ (a : ℕ),
ite (a = 3) (id_rhs ℕ 2)
(ite (a = 0) (id_rhs ℕ (1 + ⁇))
(ite (a = 5) (id_rhs ℕ (⁇ + 4))
(ite (a = 42) (id_rhs ℕ (ite (2 ∈ 3) 3 ⁇)) (ite (a = 7) (id_rhs ℕ ⁇) (id_rhs ℕ ⁇)))))
(ite (a = 42) (id_rhs ℕ (ite (2 ∈ 3) 3 ⁇))
(ite (a = 7) (id_rhs ℕ ⁇) (ite (a = 10) (id_rhs ℕ ⁇) ⁇)))))
2
nat.succ (nat.succ (nat.succ (nat.succ ⁇)))
2
elab_error_recovery.lean:21:13: error: type expected at
elab_error_recovery.lean:22:13: error: type expected at
0
∀ (x : ⁇), x = x : Prop