From cce6e4d58cbe1c296ccb727193ba804ceb74eebc Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 16 Jan 2017 20:01:25 -0800
Subject: [PATCH] fix(library/equations_compiler/compiler): fix #1315

---
 src/library/equations_compiler/compiler.cpp |  7 +++-
 tests/lean/run/1315a.lean                   | 35 ++++++++++++++++
 tests/lean/run/1315b.lean                   | 45 +++++++++++++++++++++
 3 files changed, 86 insertions(+), 1 deletion(-)
 create mode 100644 tests/lean/run/1315a.lean
 create mode 100644 tests/lean/run/1315b.lean

diff --git a/src/library/equations_compiler/compiler.cpp b/src/library/equations_compiler/compiler.cpp
index 201887314b..8e73cfaadf 100644
--- a/src/library/equations_compiler/compiler.cpp
+++ b/src/library/equations_compiler/compiler.cpp
@@ -210,7 +210,12 @@ struct pull_nested_rec_fn : public replace_visitor {
             expr g           = declare_new_local(uid, fn_aux, val_type);
             m_new_locals.push_back(g);
             m_new_values.push_back(val);
-            return mk_app(g, local_deps);
+            expr r           = g;
+            for (expr const & d : local_deps) {
+                if (!lctx().get_local_decl(d)->get_value())
+                    r = mk_app(r, d);
+            }
+            return r;
         } else {
             return default_visit_app(e, fn, args);
         }
diff --git a/tests/lean/run/1315a.lean b/tests/lean/run/1315a.lean
new file mode 100644
index 0000000000..2b691bf5ff
--- /dev/null
+++ b/tests/lean/run/1315a.lean
@@ -0,0 +1,35 @@
+def k : ℕ := 0
+
+def works : Π (n : ℕ) (m : ℕ), ℕ
+| 0 m := 0
+| (n+1) m :=
+  let val := m+1 in
+  match works n val with
+  | 0 := 0
+  | (l+1) := 0
+  end
+
+def works2 : Π (n : ℕ) (m : ℕ), ℕ
+| 0 m := 0
+| (n+1) m :=
+  match k with
+  | 0 := 0
+  | (i+1) :=
+  match works2 n (m+1) with
+  | 0 := 0
+  | (l+1) := 0
+  end
+ end
+
+def fails : Π (n : ℕ) (m : ℕ), ℕ
+| 0 m := 0
+| (n+1) m :=
+  match k with
+  | 0 := 0
+  | (i+1) :=
+  let val := m+1 in
+  match fails n val with
+  | 0 := 0
+  | (l+1) := 0
+  end
+ end
diff --git a/tests/lean/run/1315b.lean b/tests/lean/run/1315b.lean
new file mode 100644
index 0000000000..05fc1a7bfe
--- /dev/null
+++ b/tests/lean/run/1315b.lean
@@ -0,0 +1,45 @@
+open nat
+
+def k : ℕ := 0
+
+def fails : Π (n : ℕ) (m : ℕ), ℕ
+| 0 m := 0
+| (succ n) m :=
+  match k with
+  | 0 := 0
+  | (succ i) :=
+    let val := m+1 in
+    match fails n val with
+    | 0 := 0
+    | (succ l) := 0
+    end
+  end
+
+
+def test (k : ℕ) : Π (n : ℕ) (m : ℕ), ℕ
+| 0 m := 0
+| (succ n) m :=
+  match k with
+  | 0 := 1
+  | (succ i) :=
+    let val := m+1 in
+    match test n val with
+    | 0 := 2
+    | (succ l) := 3
+    end
+  end
+
+example (k m : ℕ) : test k 0 m = 0 :=
+rfl
+
+example (m n : ℕ) : test 0 (succ n) m = 1 :=
+rfl
+
+example (k m : ℕ) : test (succ k) 1 m = 2 :=
+rfl
+
+example (k m : ℕ) : test (succ k) 2 m = 3 :=
+rfl
+
+example (k m : ℕ) : test (succ k) 3 m = 3 :=
+rfl