From 240ca3fc68d1cb3fa3e32923b94cd314306de2aa Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 26 Apr 2019 15:04:39 -0700
Subject: [PATCH] test(tests/playground/badupdate1): add test for exposing
 performance bug at `struct_cases_on_fn`

```
./run.sh badupdate1.lean 4000
8000
test1 2.12s
8000
test2 1.11ms
```
---
 tests/playground/badupdate1.lean | 23 +++++++++++++++++++++++
 1 file changed, 23 insertions(+)
 create mode 100644 tests/playground/badupdate1.lean

diff --git a/tests/playground/badupdate1.lean b/tests/playground/badupdate1.lean
new file mode 100644
index 0000000000..794a59363c
--- /dev/null
+++ b/tests/playground/badupdate1.lean
@@ -0,0 +1,23 @@
+structure S :=
+(vals : Array Nat) (sz : Nat)
+
+@[noinline] def inc0 (a : Array Nat) : Array Nat :=
+a.modify 0 (+1)
+
+set_option pp.implicit true
+-- set_option trace.compiler.boxed true
+
+def f1 (s : S) : S :=
+{ vals := inc0 s.vals, .. s}
+
+def f2 : S → S
+| ⟨vals, sz⟩ := ⟨inc0 vals, sz⟩
+
+def test (f : S → S) (n : Nat): IO Unit :=
+let s : S := { vals := mkArray (n*100) n, sz := n*100 } in
+let s     := n.repeat f s in
+IO.println (s.vals.get 0)
+
+def main (xs : List String) : IO Unit :=
+timeit "test1" (test f1 xs.head.toNat) *>
+timeit "test2" (test f2 xs.head.toNat)