test(tests/playground/binarytrees.lean): more coarse parallelization

tests/playground/binarytrees.lean

@@ -21,17 +21,17 @@ def minN := 4
 def out (s) (n t : nat) := io.println' (s ++ " of depth " ++ to_string n ++ "\t check: " ++ to_string t)
 
 -- allocate and check lots of trees
-def sumT : nat -> nat -> list (task nat)
-| d 0 := []
-| d i :=
-  let a := task.mk $ λ _, check (make d) in
-  a :: sumT d (i-1)
+def sumT : nat -> nat -> nat -> nat
+| d 0 t := t
+| d i t :=
+  let a := check (make d) in
+  sumT d (i-1) (t + a)
 
 -- generate many trees
-meta def depth : nat -> nat -> list (nat × nat × nat)
+meta def depth : nat -> nat -> list (nat × nat × task nat)
 | d m := if d ≤ m then
     let n := 2 ^ (m - d + minN) in
-    (n, d, ((sumT d n).map task.get).foldl (+) 0) :: depth (d+2) m
+    (n, d, task.mk (λ _, sumT d n 0)) :: depth (d+2) m
   else []
 
 meta def main : list string → io uint32
@@ -49,7 +49,7 @@ meta def main : list string → io uint32
 
   -- allocate, walk, and deallocate many bottom-up binary trees
   let vs := (depth minN maxN), -- `using` (parList $ evalTuple3 r0 r0 rseq)
-  vs.mmap (λ ⟨m,d,i⟩, out (to_string m ++ "\t trees") d i),
+  vs.mmap (λ ⟨m,d,i⟩, out (to_string m ++ "\t trees") d i.get),
 
   -- confirm the the long-lived binary tree still exists
   out "long lived tree" maxN (check long),