test(tests/playground): simple task benchmarks

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

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

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

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