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

fix(library/equations_compiler): do not unfold generalized inductives

Browse source
This commit is contained in:
Gabriel Ebner 2017-07-06 16:00:31 +02:00 • committed by Leonardo de Moura
parent 5e94ecc841
commit bcf44f7020
3 changed files with 12 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -682,8 +682,7 @@ struct elim_match_fn {
for (equation const & eqn : eqns) { for (equation const & eqn : eqns) {
lean_assert(eqn.m_patterns); lean_assert(eqn.m_patterns);
type_context ctx = mk_type_context(eqn.m_lctx); type_context ctx = mk_type_context(eqn.m_lctx);
/* We use ctx.relaxed_whnf to make sure we expose the kernel constructor */ expr pattern = whnf_constructor(ctx, head(eqn.m_patterns));
expr pattern = ctx.relaxed_whnf(head(eqn.m_patterns));
if (!is_constructor_app(ctx, pattern)) { if (!is_constructor_app(ctx, pattern)) {
throw_error("equation compiler failed, pattern is not a constructor " throw_error("equation compiler failed, pattern is not a constructor "
"(use 'set_option trace.eqn_compiler.elim_match true' for additional details)"); "(use 'set_option trace.eqn_compiler.elim_match true' for additional details)");
@ -741,7 +740,7 @@ struct elim_match_fn {
lean_assert(is_constructor_transition(P)); lean_assert(is_constructor_transition(P));
type_context ctx = mk_type_context(P); type_context ctx = mk_type_context(P);
expr x = head(P.m_var_stack); expr x = head(P.m_var_stack);
expr x_type = ctx.relaxed_whnf(whnf_inductive(ctx, ctx.infer(x))); expr x_type = whnf_inductive(ctx, ctx.infer(x));
lean_assert(is_inductive_app(x_type)); lean_assert(is_inductive_app(x_type));
buffer<expr> x_type_args; buffer<expr> x_type_args;
auto x_type_const = get_app_args(x_type, x_type_args); auto x_type_const = get_app_args(x_type, x_type_args);
@ -753,7 +752,7 @@ struct elim_match_fn {
list<expr> new_goals; list<expr> new_goals;
list<name> new_goal_cnames; list<name> new_goal_cnames;
try { try {
bool unfold_ginductive = true; bool unfold_ginductive = false;
list<name> ids; list<name> ids;
std::tie(new_goals, new_goal_cnames) = std::tie(new_goals, new_goal_cnames) =
cases(m_env, m_opts, transparency_mode::Semireducible, m_mctx, cases(m_env, m_opts, transparency_mode::Semireducible, m_mctx,

5
tests/lean/non_exhaustive_error.lean
View file

@ -21,3 +21,8 @@ with g : nat → nat → nat
| 0 0 := 1 | 0 0 := 1
end other end other
inductive term | mk : ℕ → list term → term
def const_name : term → ℕ
| (term.mk n []) := n

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

@ -16,3 +16,6 @@ f (nat.succ _) _
g 0 (nat.succ _) g 0 (nat.succ _)
g (nat.succ _) _ g (nat.succ _) _
non_exhaustive_error.lean:17:0: warning: declaration '_mutual.f.g' uses sorry non_exhaustive_error.lean:17:0: warning: declaration '_mutual.f.g' uses sorry
non_exhaustive_error.lean:27:4: error: non-exhaustive match, the following cases are missing:
const_name (term.mk _ (term.mk _ _ :: _))
non_exhaustive_error.lean:27:0: warning: declaration 'const_name' uses sorry