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

feat(library/equations_compiler/elim_match): provide counter-examples for non-exhaustive matches

Browse source
This commit is contained in:
Gabriel Ebner 2017-07-04 15:04:50 +02:00 • committed by Leonardo de Moura
parent 0cfb48c095
commit 4fee7eaa70
6 changed files with 172 additions and 7 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -10,6 +10,7 @@ Author: Leonardo de Moura
#include "kernel/instantiate.h"
#include "kernel/for_each_fn.h"
#include "kernel/replace_fn.h"
#include "kernel/abstract.h"
#include "kernel/inductive/inductive.h"
#include "library/trace.h"
#include "library/num.h"
@ -25,6 +26,7 @@ Author: Leonardo de Moura
#include "library/inverse.h"
#include "library/aux_definition.h"
#include "library/app_builder.h"
#include "library/sorry.h"
#include "library/delayed_abstraction.h"
#include "library/tactic/tactic_state.h"
#include "library/tactic/revert_tactic.h"
@ -104,8 +106,11 @@ struct elim_match_fn {
expr m_goal;
list<expr> m_var_stack;
list<equation> m_equations;
list<expr> m_example;
};
buffer<problem> m_unsolved;
struct lemma {
local_context m_lctx;
list<expr> m_vars;
@ -177,6 +182,7 @@ struct elim_match_fn {
lean_unreachable();
}
}
auto tc = mk_type_context(P);
return true;
}
@ -233,6 +239,13 @@ struct elim_match_fn {
for (equation const & eqn : P.m_equations) {
r += nest(line() + pp_equation(eqn));
}
auto example = format("example:");
for (auto & ex : P.m_example) {
example += space() + paren(pp(ex));
}
r += line() + nest(example);
return r;
}
@ -442,6 +455,7 @@ struct elim_match_fn {
for (name const & n : var_names)
vars.push_back(goal_lctx.get_local_decl(n).mk_ref());
P.m_var_stack = to_list(vars);
P.m_example = P.m_var_stack;
P.m_equations = mk_equations(lctx, eqns);
return mk_pair(P, mvar);
}
@ -626,6 +640,7 @@ struct elim_match_fn {
new_P.m_fn_name = P.m_fn_name;
new_P.m_goal = P.m_goal;
new_P.m_var_stack = tail(P.m_var_stack);
new_P.m_example = P.m_example;
buffer<equation> new_eqns;
for (equation const & eqn : P.m_equations) {
equation new_eqn = eqn;
@ -716,8 +731,11 @@ struct elim_match_fn {
expr x = head(P.m_var_stack);
expr x_type = ctx.relaxed_whnf(whnf_inductive(ctx, ctx.infer(x)));
lean_assert(is_inductive_app(x_type));
name I_name = const_name(get_app_fn(x_type));
buffer<expr> x_type_args;
auto x_type_const = get_app_args(x_type, x_type_args);
name I_name = const_name(x_type_const);
unsigned I_nparams = get_inductive_num_params(I_name);
lean_assert(x_type_args.size() >= I_nparams);
intros_list ilist;
hsubstitution_list slist;
list<expr> new_goals;
@ -750,6 +768,12 @@ struct elim_match_fn {
new_P.m_var_stack = update_var_stack(head(ilist), tail(P.m_var_stack), head(slist));
new_P.m_goal = new_goal;
name const & C = head(new_goal_cnames);
new_P.m_example = map(P.m_example, [&] (expr ex) {
ex = instantiate(abstract_local(ex, head(P.m_var_stack)),
mk_app(mk_app(mk_constant(C, const_levels(x_type_const)), I_nparams, x_type_args.begin()), head(ilist)));
ex = apply(ex, head(slist));
return ex;
});
new_P.m_equations = get_equations_for(C, I_nparams, head(slist), eqns);
to_buffer(process(new_P), new_Ls);
new_goals = tail(new_goals);
@ -804,6 +828,7 @@ struct elim_match_fn {
new_P.m_fn_name = name(P.m_fn_name, "_ite_val");
new_P.m_goal = value_goals[i];
new_P.m_var_stack = tail(P.m_var_stack);
new_P.m_example = cons(val, tail(P.m_example));
buffer<equation> new_eqns;
for (equation const & eqn : P.m_equations) {
expr const & p = head(eqn.m_patterns);
@ -856,6 +881,7 @@ struct elim_match_fn {
new_P.m_fn_name = name(P.m_fn_name, "_ite_else");
new_P.m_goal = else_goal;
new_P.m_var_stack = tail(P.m_var_stack);
new_P.m_example = P.m_example;
buffer<equation> new_eqns;
for (equation const & eqn : P.m_equations) {
expr const & p = head(eqn.m_patterns);
@ -966,6 +992,7 @@ struct elim_match_fn {
problem new_P;
new_P.m_fn_name = P.m_fn_name;
new_P.m_goal = P.m_goal;
new_P.m_example = P.m_example;
new_P.m_var_stack = tail(P.m_var_stack);
buffer<equation> new_eqns;
for (equation const & eqn : P.m_equations) {
@ -993,6 +1020,7 @@ struct elim_match_fn {
problem new_P;
new_P.m_fn_name = P.m_fn_name;
new_P.m_goal = P.m_goal;
new_P.m_example = P.m_example;
buffer<expr> new_var_stack;
for (unsigned i = I_nparams; i < C_args.size(); i++) {
new_var_stack.push_back(whnf_constructor(ctx, C_args[i]));
@ -1134,6 +1162,12 @@ struct elim_match_fn {
new_P.m_goal = *M_3;
new_P.m_var_stack = map(P.m_var_stack,
[&](expr const & x) { return replace_locals(x, to_revert, new_Hs); });
new_P.m_example = map(P.m_example, [&] (expr ex) {
auto f_x = instantiate(abstract_local(f_y1, y1), x);
ex = instantiate(abstract_local(ex, x), f_x);
ex = replace_locals(ex, to_revert, new_Hs);
return ex;
});
buffer<equation> new_eqns;
for (equation const & eqn : P.m_equations) {
equation new_eqn = eqn;
@ -1148,8 +1182,9 @@ struct elim_match_fn {
list<lemma> process_leaf(problem const & P) {
if (!P.m_equations) {
throw_error("invalid non-exhaustive set of equations (use 'set_option trace.eqn_compiler.elim_match true' "
"for additional details)");
m_unsolved.push_back(P);
m_mctx.assign(P.m_goal, mk_sorry(m_mctx.get_metavar_decl(P.m_goal).get_type(), true));
return list<lemma>();
}
equation const & eqn = head(P.m_equations);
m_used_eqns[eqn.m_eqn_idx] = true;
@ -1203,6 +1238,7 @@ struct elim_match_fn {
} else if (is_inaccessible_transition(P)) {
return process_inaccessible(P);
} else {
check_exhaustive(); // TODO(gabriel): not sure why we fail here in some non-exhaustive matches
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)");
@ -1262,6 +1298,23 @@ struct elim_match_fn {
}
}
void check_exhaustive() {
if (m_unsolved.empty()) return;
format msg;
msg += format("non-exhaustive set of equations, the following cases are missing:");
for (auto & P : m_unsolved) {
auto pp_fn = mk_pp_ctx(P);
msg += line();
for (auto & t : P.m_example) {
msg += space();
msg += paren(pp_fn(t));
}
}
throw formatted_exception(m_ref, msg);
}
elim_match_result operator()(local_context const & lctx, expr const & eqns) {
lean_assert(equations_num_fns(eqns) == 1);
DEBUG_CODE({
@ -1274,6 +1327,7 @@ struct elim_match_fn {
std::tie(P, fn) = mk_problem(lctx, eqns);
lean_assert(check_problem(P));
list<lemma> pre_Ls = process(P);
check_exhaustive();
check_no_unused_eqns(eqns);
fn = m_mctx.instantiate_mvars(fn);
trace_match_debug(tout() << "code:\n" << fn << "\n";);

3
tests/lean/do_match_fail.lean.expected.out
View file

@ -4,4 +4,5 @@ p q : Prop,
a : p,
a_1 : q
⊢ p
do_match_fail.lean:20:3: error: invalid non-exhaustive set of equations (use 'set_option trace.eqn_compiler.elim_match true' for additional details)
do_match_fail.lean:20:3: error: non-exhaustive set of equations, the following cases are missing:
(list.nil)

3
tests/lean/eqn_compiler_loop.lean.expected.out
View file

@ -1 +1,2 @@
eqn_compiler_loop.lean:3:8: error: invalid non-exhaustive set of equations (use 'set_option trace.eqn_compiler.elim_match true' for additional details)
eqn_compiler_loop.lean:3:8: error: non-exhaustive set of equations, the following cases are missing:
(succ a) (a_1)

3
tests/lean/eqn_hole.lean.expected.out
View file

@ -2,7 +2,8 @@ eqn_hole.lean:3:7: error: don't know how to synthesize placeholder
context:
f : ℕ → ℕ
⊢ ℕ
eqn_hole.lean:2:11: error: invalid non-exhaustive set of equations (use 'set_option trace.eqn_compiler.elim_match true' for additional details)
eqn_hole.lean:2:11: error: non-exhaustive set of equations, the following cases are missing:
(nat.succ a_1)
eqn_hole.lean:8:13: error: don't know how to synthesize placeholder
context:
g : ℕ → ℕ,

4
tests/lean/non_exhaustive_error.lean
View file

@ -1,4 +1,8 @@
def g : ℕ × ℕ → ℕ
| (0, n) := n
| (m+2, 0) := m
definition f : string → nat → bool
| "hello world" 1 := tt
| "bye" _ := tt

106
tests/lean/non_exhaustive_error.lean.expected.out
View file

@ -1 +1,105 @@
non_exhaustive_error.lean:2:11: error: invalid non-exhaustive set of equations (use 'set_option trace.eqn_compiler.elim_match true' for additional details)
non_exhaustive_error.lean:2:4: error: non-exhaustive set of equations, the following cases are missing:
((1, snd))
((nat.succ (nat.succ a_1), nat.succ a))
non_exhaustive_error.lean:6:11: error: non-exhaustive set of equations, the following cases are missing:
({data := list.nil char}) (a)
({data := ⟨0, is_lt⟩ :: a_2}) (a)
({data := ⟨1, is_lt⟩ :: a_2}) (a)
({data := ⟨2, is_lt⟩ :: a_2}) (a)
({data := ⟨3, is_lt⟩ :: a_2}) (a)
({data := ⟨4, is_lt⟩ :: a_2}) (a)
({data := ⟨5, is_lt⟩ :: a_2}) (a)
({data := ⟨6, is_lt⟩ :: a_2}) (a)
({data := ⟨7, is_lt⟩ :: a_2}) (a)
({data := ⟨8, is_lt⟩ :: a_2}) (a)
({data := ⟨9, is_lt⟩ :: a_2}) (a)
({data := ⟨10, is_lt⟩ :: a_2}) (a)
({data := ⟨11, is_lt⟩ :: a_2}) (a)
({data := ⟨12, is_lt⟩ :: a_2}) (a)
({data := ⟨13, is_lt⟩ :: a_2}) (a)
({data := ⟨14, is_lt⟩ :: a_2}) (a)
({data := ⟨15, is_lt⟩ :: a_2}) (a)
({data := ⟨16, is_lt⟩ :: a_2}) (a)
({data := ⟨17, is_lt⟩ :: a_2}) (a)
({data := ⟨18, is_lt⟩ :: a_2}) (a)
({data := ⟨19, is_lt⟩ :: a_2}) (a)
({data := ⟨20, is_lt⟩ :: a_2}) (a)
({data := ⟨21, is_lt⟩ :: a_2}) (a)
({data := ⟨22, is_lt⟩ :: a_2}) (a)
({data := ⟨23, is_lt⟩ :: a_2}) (a)
({data := ⟨24, is_lt⟩ :: a_2}) (a)
({data := ⟨25, is_lt⟩ :: a_2}) (a)
({data := ⟨26, is_lt⟩ :: a_2}) (a)
({data := ⟨27, is_lt⟩ :: a_2}) (a)
({data := ⟨28, is_lt⟩ :: a_2}) (a)
({data := ⟨29, is_lt⟩ :: a_2}) (a)
({data := ⟨30, is_lt⟩ :: a_2}) (a)
({data := ⟨31, is_lt⟩ :: a_2}) (a)
({data := ⟨32, is_lt⟩ :: a_2}) (a)
({data := ⟨33, is_lt⟩ :: a_2}) (a)
({data := ⟨34, is_lt⟩ :: a_2}) (a)
({data := ⟨35, is_lt⟩ :: a_2}) (a)
({data := ⟨36, is_lt⟩ :: a_2}) (a)
({data := ⟨37, is_lt⟩ :: a_2}) (a)
({data := ⟨38, is_lt⟩ :: a_2}) (a)
({data := ⟨39, is_lt⟩ :: a_2}) (a)
({data := ⟨40, is_lt⟩ :: a_2}) (a)
({data := ⟨41, is_lt⟩ :: a_2}) (a)
({data := ⟨42, is_lt⟩ :: a_2}) (a)
({data := ⟨43, is_lt⟩ :: a_2}) (a)
({data := ⟨44, is_lt⟩ :: a_2}) (a)
({data := ⟨45, is_lt⟩ :: a_2}) (a)
({data := ⟨46, is_lt⟩ :: a_2}) (a)
({data := ⟨47, is_lt⟩ :: a_2}) (a)
({data := ⟨48, is_lt⟩ :: a_2}) (a)
({data := ⟨49, is_lt⟩ :: a_2}) (a)
({data := ⟨50, is_lt⟩ :: a_2}) (a)
({data := ⟨51, is_lt⟩ :: a_2}) (a)
({data := ⟨52, is_lt⟩ :: a_2}) (a)
({data := ⟨53, is_lt⟩ :: a_2}) (a)
({data := ⟨54, is_lt⟩ :: a_2}) (a)
({data := ⟨55, is_lt⟩ :: a_2}) (a)
({data := ⟨56, is_lt⟩ :: a_2}) (a)
({data := ⟨57, is_lt⟩ :: a_2}) (a)
({data := ⟨58, is_lt⟩ :: a_2}) (a)
({data := ⟨59, is_lt⟩ :: a_2}) (a)
({data := ⟨60, is_lt⟩ :: a_2}) (a)
({data := ⟨61, is_lt⟩ :: a_2}) (a)
({data := ⟨62, is_lt⟩ :: a_2}) (a)
({data := ⟨63, is_lt⟩ :: a_2}) (a)
({data := ⟨64, is_lt⟩ :: a_2}) (a)
({data := ⟨65, is_lt⟩ :: a_2}) (a)
({data := ⟨66, is_lt⟩ :: a_2}) (a)
({data := ⟨67, is_lt⟩ :: a_2}) (a)
({data := ⟨68, is_lt⟩ :: a_2}) (a)
({data := ⟨69, is_lt⟩ :: a_2}) (a)
({data := ⟨70, is_lt⟩ :: a_2}) (a)
({data := ⟨71, is_lt⟩ :: a_2}) (a)
({data := ⟨72, is_lt⟩ :: a_2}) (a)
({data := ⟨73, is_lt⟩ :: a_2}) (a)
({data := ⟨74, is_lt⟩ :: a_2}) (a)
({data := ⟨75, is_lt⟩ :: a_2}) (a)
({data := ⟨76, is_lt⟩ :: a_2}) (a)
({data := ⟨77, is_lt⟩ :: a_2}) (a)
({data := ⟨78, is_lt⟩ :: a_2}) (a)
({data := ⟨79, is_lt⟩ :: a_2}) (a)
({data := ⟨80, is_lt⟩ :: a_2}) (a)
({data := ⟨81, is_lt⟩ :: a_2}) (a)
({data := ⟨82, is_lt⟩ :: a_2}) (a)
({data := ⟨83, is_lt⟩ :: a_2}) (a)
({data := ⟨84, is_lt⟩ :: a_2}) (a)
({data := ⟨85, is_lt⟩ :: a_2}) (a)
({data := ⟨86, is_lt⟩ :: a_2}) (a)
({data := ⟨87, is_lt⟩ :: a_2}) (a)
({data := ⟨88, is_lt⟩ :: a_2}) (a)
({data := ⟨89, is_lt⟩ :: a_2}) (a)
({data := ⟨90, is_lt⟩ :: a_2}) (a)
({data := ⟨91, is_lt⟩ :: a_2}) (a)
({data := ⟨92, is_lt⟩ :: a_2}) (a)
({data := ⟨93, is_lt⟩ :: a_2}) (a)
({data := ⟨94, is_lt⟩ :: a_2}) (a)
({data := ⟨95, is_lt⟩ :: a_2}) (a)
({data := ⟨96, is_lt⟩ :: a_2}) (a)
({data := ⟨97, is_lt⟩ :: a_2}) (a)
({data := ⟨98, is_lt⟩ :: a_2}) (a)
({data := ⟨99, is_lt⟩ :: a_2}) (a)