michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

fix(library/definitional/equations): assertion violation

Browse source
This commit is contained in:
Leonardo de Moura 2015-01-13 11:57:14 -08:00
parent 1fbfe59a9a
commit e5a8c67d22
2 changed files with 29 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

18
src/library/definitional/equations.cpp
View file

@ -1324,7 +1324,8 @@ class equation_compiler_fn {
unsigned nparams = *inductive::get_num_params(env(), const_name(I)); unsigned nparams = *inductive::get_num_params(env(), const_name(I));
buffer<expr> params; buffer<expr> params;
params.append(nparams, a_type_args.data()); params.append(nparams, a_type_args.data());
if (std::all_of(params.begin(), params.end(), [&](expr const & p) { return contains_local(p, m_global_context); })) { if (std::all_of(params.begin(), params.end(),
[&](expr const & p) { return !is_local(p) || contains_local(p, m_global_context); })) {
return mk_pair(prg, arg_pos); return mk_pair(prg, arg_pos);
} else { } else {
list<expr> new_context = prg.m_context; list<expr> new_context = prg.m_context;
@ -1409,6 +1410,17 @@ class equation_compiler_fn {
buffer<expr> params; buffer<expr> params;
params.append(nparams, a0_type_args.data()); params.append(nparams, a0_type_args.data());
// Return true if the local constant l is in the buffer b.
// This is similar to contains_local, but b may contain arbitrary terms
auto contains_local_at = [&](expr const & l, buffer<expr> const & b) {
lean_assert(is_mlocal(l));
for (expr const & e : b) {
if (is_local(e) && mlocal_name(l) == mlocal_name(e))
return true;
}
return false;
};
// Distribute parameters of the ith program intro three groups: // Distribute parameters of the ith program intro three groups:
// indices, major premise (arg), and remaining arguments (rest) // indices, major premise (arg), and remaining arguments (rest)
// We store the position of the rest arguments in the buffer rest_pos. // We store the position of the rest arguments in the buffer rest_pos.
@ -1424,9 +1436,9 @@ class equation_compiler_fn {
indices.append(arg_args.size() - nparams, arg_args.data() + nparams); indices.append(arg_args.size() - nparams, arg_args.data() + nparams);
unsigned j = 0; unsigned j = 0;
for (expr const & l : ctx) { for (expr const & l : ctx) {
if (mlocal_name(l) == mlocal_name(arg) || contains_local(l, params)) { if (mlocal_name(l) == mlocal_name(arg) || contains_local_at(l, params)) {
// do nothing // do nothing
} else if (contains_local(l, indices)) { } else if (contains_local_at(l, indices)) {
indices_pos.push_back(j); indices_pos.push_back(j);
} else { } else {
rest.push_back(l); rest.push_back(l);

14
tests/lean/run/unzip_bug.lean Normal file
View file

@ -0,0 +1,14 @@
import data.vector
open nat vector prod
variables {A B : Type}
definition unzip : Π {n : nat}, vector (A × B) n → vector A n × vector B n,
@unzip ⌞zero⌟ nil := (nil, nil),
@unzip ⌞succ n⌟ ((a, b) :: v) :=
match unzip v with
(va, vb) := (a :: va, b :: vb)
end
example : unzip ((1, 20) :: (2, 30) :: nil) = (1 :: 2 :: nil, 20 :: 30 :: nil) :=
rfl