From 4fee7eaa70848758ddfb6c155413efe1b22efa1d Mon Sep 17 00:00:00 2001 From: Gabriel Ebner Date: Tue, 4 Jul 2017 15:04:50 +0200 Subject: [PATCH] feat(library/equations_compiler/elim_match): provide counter-examples for non-exhaustive matches --- src/library/equations_compiler/elim_match.cpp | 60 +++++++++- tests/lean/do_match_fail.lean.expected.out | 3 +- .../lean/eqn_compiler_loop.lean.expected.out | 3 +- tests/lean/eqn_hole.lean.expected.out | 3 +- tests/lean/non_exhaustive_error.lean | 4 + .../non_exhaustive_error.lean.expected.out | 106 +++++++++++++++++- 6 files changed, 172 insertions(+), 7 deletions(-) diff --git a/src/library/equations_compiler/elim_match.cpp b/src/library/equations_compiler/elim_match.cpp index 809b062d01..78fbdac19d 100644 --- a/src/library/equations_compiler/elim_match.cpp +++ b/src/library/equations_compiler/elim_match.cpp @@ -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 m_var_stack; list m_equations; + list m_example; }; + buffer m_unsolved; + struct lemma { local_context m_lctx; list 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 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 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 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 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 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 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 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 new_eqns; for (equation const & eqn : P.m_equations) { equation new_eqn = eqn; @@ -1148,8 +1182,9 @@ struct elim_match_fn { list 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(); } 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 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";); diff --git a/tests/lean/do_match_fail.lean.expected.out b/tests/lean/do_match_fail.lean.expected.out index 5f273e18d5..168d1190fa 100644 --- a/tests/lean/do_match_fail.lean.expected.out +++ b/tests/lean/do_match_fail.lean.expected.out @@ -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) diff --git a/tests/lean/eqn_compiler_loop.lean.expected.out b/tests/lean/eqn_compiler_loop.lean.expected.out index c40493c3c0..8aaa802cc5 100644 --- a/tests/lean/eqn_compiler_loop.lean.expected.out +++ b/tests/lean/eqn_compiler_loop.lean.expected.out @@ -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) diff --git a/tests/lean/eqn_hole.lean.expected.out b/tests/lean/eqn_hole.lean.expected.out index 6cb77da133..6fae7f8283 100644 --- a/tests/lean/eqn_hole.lean.expected.out +++ b/tests/lean/eqn_hole.lean.expected.out @@ -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 : ℕ → ℕ, diff --git a/tests/lean/non_exhaustive_error.lean b/tests/lean/non_exhaustive_error.lean index b95ed33a39..5c34a0bca2 100644 --- a/tests/lean/non_exhaustive_error.lean +++ b/tests/lean/non_exhaustive_error.lean @@ -1,4 +1,8 @@ +def g : ℕ × ℕ → ℕ +| (0, n) := n +| (m+2, 0) := m + definition f : string → nat → bool | "hello world" 1 := tt | "bye" _ := tt diff --git a/tests/lean/non_exhaustive_error.lean.expected.out b/tests/lean/non_exhaustive_error.lean.expected.out index 56703eab52..d5c8951fc5 100644 --- a/tests/lean/non_exhaustive_error.lean.expected.out +++ b/tests/lean/non_exhaustive_error.lean.expected.out @@ -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)