From e5a8c67d2253ec0e2c894cd98c1e235f6984bf07 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 13 Jan 2015 11:57:14 -0800
Subject: [PATCH] fix(library/definitional/equations): assertion violation

---
 src/library/definitional/equations.cpp | 18 +++++++++++++++---
 tests/lean/run/unzip_bug.lean          | 14 ++++++++++++++
 2 files changed, 29 insertions(+), 3 deletions(-)
 create mode 100644 tests/lean/run/unzip_bug.lean

diff --git a/src/library/definitional/equations.cpp b/src/library/definitional/equations.cpp
index 6af57000f..f741d8a99 100644
--- a/src/library/definitional/equations.cpp
+++ b/src/library/definitional/equations.cpp
@@ -1324,7 +1324,8 @@ class equation_compiler_fn {
         unsigned nparams    = *inductive::get_num_params(env(), const_name(I));
         buffer<expr> params;
         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);
         } else {
             list<expr>             new_context = prg.m_context;
@@ -1409,6 +1410,17 @@ class equation_compiler_fn {
         buffer<expr> params;
         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:
         //    indices, major premise (arg), and remaining arguments (rest)
         // 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);
             unsigned j = 0;
             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
-                } else if (contains_local(l, indices)) {
+                } else if (contains_local_at(l, indices)) {
                     indices_pos.push_back(j);
                 } else {
                     rest.push_back(l);
diff --git a/tests/lean/run/unzip_bug.lean b/tests/lean/run/unzip_bug.lean
new file mode 100644
index 000000000..281074b68
--- /dev/null
+++ b/tests/lean/run/unzip_bug.lean
@@ -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