From 363f7dc6f48a38df86aafc25c5c79412174dadb4 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 19 Apr 2019 14:47:07 -0700
Subject: [PATCH] test(tests/playground/mapVShmap): add example where `hmap` is
 almost 3x faster than `map`

---
 tests/playground/mapVShmap.lean | 34 +++++++++++++++++++++++++++++++++
 1 file changed, 34 insertions(+)
 create mode 100644 tests/playground/mapVShmap.lean

diff --git a/tests/playground/mapVShmap.lean b/tests/playground/mapVShmap.lean
new file mode 100644
index 0000000000..47d5df9e4c
--- /dev/null
+++ b/tests/playground/mapVShmap.lean
@@ -0,0 +1,34 @@
+def mkBigPairs : Nat → Array (Nat × Nat) → Array (Nat × Nat)
+| 0     ps := ps
+| (n+1) ps := mkBigPairs n (ps.push (n, n))
+
+set_option pp.implicit true
+set_option pp.binder_types false
+-- set_option trace.compiler.specialize true
+-- set_option trace.compiler.boxed true
+
+def f1 (ps : Array (Nat × Nat)) : Array (Nat × Nat) :=
+ps.hmap (λ p, match p with (n, m) := (n+1, m))
+
+def f2 (ps : Array (Nat × Nat)) : Array (Nat × Nat) :=
+ps.map (λ p, match p with (n, m) := (n+1, m))
+
+def prof {α : Type} (msg : String) (p : IO α) : IO α :=
+let msg₁ := "Time for '" ++ msg ++ "':" in
+timeit msg₁ p
+
+def test1 (n : Nat) (m : Array (Nat × Nat)) : IO Unit :=
+let m := n.repeat f1 m in
+let s := m.foldl (λ p n, n + p.1) 0 in
+IO.println s
+
+def test2 (n : Nat) (m : Array (Nat × Nat)) : IO Unit :=
+let m := n.repeat f2 m in
+let s := m.foldl (λ p n, n + p.1) 0 in
+IO.println s
+
+def main (xs : List String) : IO Unit :=
+let n := xs.head.toNat in
+let m := mkBigPairs n ∅ in
+prof "hmap" (test1 n m) *>
+prof "map"  (test2 n m)