From 70a5c6d5855e5c5fd47e2d0101abe7016b577698 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Tue, 26 Feb 2019 17:21:45 +0100 Subject: [PATCH] test(tests/playground/binarytrees.lean): more coarse parallelization --- tests/playground/binarytrees.lean | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) diff --git a/tests/playground/binarytrees.lean b/tests/playground/binarytrees.lean index 0c61f0a9da..2e825c2f91 100644 --- a/tests/playground/binarytrees.lean +++ b/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),