fix(library/equations_compiler/compiler): fix #1315

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);
         }

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

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