From aff5f96a3dc31932f13bcec7dc962413259bf09b Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sun, 17 Feb 2019 11:47:02 -0800
Subject: [PATCH] test(tests/playground): simple task benchmarks

---
 tests/playground/task_test.lean  | 20 ++++++++++++++++++++
 tests/playground/task_test2.lean | 12 ++++++++++++
 tests/playground/task_test3.lean | 12 ++++++++++++
 tests/playground/task_test4.lean | 12 ++++++++++++
 4 files changed, 56 insertions(+)
 create mode 100644 tests/playground/task_test.lean
 create mode 100644 tests/playground/task_test2.lean
 create mode 100644 tests/playground/task_test3.lean
 create mode 100644 tests/playground/task_test4.lean

diff --git a/tests/playground/task_test.lean b/tests/playground/task_test.lean
new file mode 100644
index 0000000000..79155860b1
--- /dev/null
+++ b/tests/playground/task_test.lean
@@ -0,0 +1,20 @@
+def g (x : nat) : nat :=
+dbg_trace ("g: " ++ to_string x) $ λ _,
+  x + 1
+
+def f1 (x : nat) : nat :=
+dbg_sleep 1000 $ λ _,
+dbg_trace ("f1: " ++ to_string x) $ λ _,
+  g (x + 1)
+
+def f2 (x : nat) : nat :=
+dbg_sleep 100 $ λ _,
+dbg_trace ("f2: " ++ to_string x) $ λ _,
+  g x
+
+def main (xs : list string) : io uint32 :=
+let t1 := task.mk $ (λ _, f1 xs.head.to_nat) in
+let t2 := task.mk $ (λ _, f2 xs.head.to_nat) in
+dbg_sleep 1000 $ λ _,
+io.println' (to_string t1.get ++ " " ++ to_string t2.get) *>
+pure 0
diff --git a/tests/playground/task_test2.lean b/tests/playground/task_test2.lean
new file mode 100644
index 0000000000..392502ca1f
--- /dev/null
+++ b/tests/playground/task_test2.lean
@@ -0,0 +1,12 @@
+def run1 (i : nat) (n : nat) (xs : list nat) : nat :=
+n.repeat (λ _ r,
+  dbg_trace (">> [" ++ to_string i ++ "] " ++ to_string r) $ λ _,
+  xs.foldl (+) r)
+0
+
+def main (xs : list string) : io uint32 :=
+let ys := (list.repeat 1 xs.head.to_nat) in
+let ts : list (task nat) := (list.iota 10).map (λ i, task.mk $ λ _, run1 (i+1) xs.head.to_nat ys) in
+let ns : list nat := ts.map task.get in
+io.println' (">> " ++ to_string ns) *>
+pure 0
diff --git a/tests/playground/task_test3.lean b/tests/playground/task_test3.lean
new file mode 100644
index 0000000000..6ce856f06e
--- /dev/null
+++ b/tests/playground/task_test3.lean
@@ -0,0 +1,12 @@
+def run1 (i : nat) (n : nat) (xs : list nat) : nat :=
+n.repeat (λ _ r,
+  -- dbg_trace (">> [" ++ to_string i ++ "] " ++ to_string r) $ λ _,
+  xs.foldl (+) (r+i))
+0
+
+def main (xs : list string) : io uint32 :=
+let ys := (list.repeat 1 xs.head.to_nat) in
+let ts : list (task nat) := (list.iota 10).map (λ i, task.mk $ λ _, run1 (i+1) xs.head.to_nat ys) in
+let ns : list nat := ts.map task.get in
+io.println' (">> " ++ to_string ns) *>
+pure 0
diff --git a/tests/playground/task_test4.lean b/tests/playground/task_test4.lean
new file mode 100644
index 0000000000..753f6a76bc
--- /dev/null
+++ b/tests/playground/task_test4.lean
@@ -0,0 +1,12 @@
+def run1 (i : nat) (n : nat) (xs : list nat) : nat :=
+n.repeat (λ _ r,
+  let s := (">> [" ++ to_string i ++ "] " ++ to_string r) in
+  xs.foldl (+) (r + s.length))
+0
+
+def main (xs : list string) : io uint32 :=
+let ys := (list.repeat 1 xs.head.to_nat) in
+let ts : list (task nat) := (list.iota 10).map (λ i, task.mk $ λ _, run1 (i+1) xs.head.to_nat ys) in
+let ns : list nat := ts.map task.get in
+io.println' (">> " ++ to_string ns) *>
+pure 0