From 83450d4bd97e0d3099ec5fec9e349bcb559af5b0 Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Tue, 17 Jan 2023 16:53:33 +0100
Subject: [PATCH] test: clean up binarytrees.lean

---
 tests/bench/binarytrees.lean | 67 +++++++++++++++++-------------------
 1 file changed, 32 insertions(+), 35 deletions(-)

diff --git a/tests/bench/binarytrees.lean b/tests/bench/binarytrees.lean
index 8dde86c46f..91b1361f33 100755
--- a/tests/bench/binarytrees.lean
+++ b/tests/bench/binarytrees.lean
@@ -1,61 +1,58 @@
 inductive Tree
-| Nil
-| Node (l r : Tree) : Tree
-open Tree
-instance : Inhabited Tree := ⟨Nil⟩
+  | nil
+  | node (l r : Tree)
+instance : Inhabited Tree := ⟨.nil⟩
 
--- This Function has an extra argument to suppress the
+-- This function has an extra argument to suppress the
 -- common sub-expression elimination optimization
-partial def make' : UInt32 -> UInt32 -> Tree
-| n, d =>
-  if d = 0 then Node Nil Nil
-  else Node (make' n (d - 1)) (make' (n + 1) (d - 1))
+partial def make' (n d : UInt32) : Tree :=
+  if d = 0 then .node .nil .nil
+  else .node (make' n (d - 1)) (make' (n + 1) (d - 1))
 
 -- build a tree
 def make (d : UInt32) := make' d d
 
 def check : Tree → UInt32
-| Nil => 0
-| Node l r   => 1 + check l + check r
+  | .nil => 0
+  | .node l r => 1 + check l + check r
 
 def minN := 4
 
 def out (s : String) (n : Nat) (t : UInt32) : IO Unit :=
-IO.println (s ++ " of depth " ++ toString n ++ "\t check: " ++ toString t)
+  IO.println s!"{s} of depth {n}\t check: {t}"
 
 -- allocate and check lots of trees
-partial def sumT : UInt32 -> UInt32 -> UInt32 -> UInt32
-| d, i, t =>
+partial def sumT (d i t : UInt32) : UInt32 :=
   if i = 0 then t
   else
-    let a := check (make d);
+    let a := check (make d)
     sumT d (i-1) (t + a)
 
 -- generate many trees
-partial def depth : Nat -> Nat -> List (Nat × Nat × Task UInt32)
-| d, m => if d ≤ m then
-    let n := 2 ^ (m - d + minN);
-    (n, d, Task.spawn (fun _ => sumT (UInt32.ofNat d) (UInt32.ofNat n) 0)) :: depth (d+2) m
+partial def depth (d m : Nat) : List (Nat × Nat × Task UInt32) :=
+  if d ≤ m then
+    let n := 2 ^ (m - d + minN)
+    (n, d, Task.spawn (fun _ => sumT (.ofNat d) (.ofNat n) 0)) :: depth (d+2) m
   else []
 
 def main : List String → IO UInt32
-| [s] => do
-  let n := s.toNat!;
-  let maxN := Nat.max (minN + 2) n;
-  let stretchN := maxN + 1;
+  | [s] => do
+    let n := s.toNat!
+    let maxN := Nat.max (minN + 2) n
+    let stretchN := maxN + 1
 
-  -- stretch memory tree
-  let c := check (make $ UInt32.ofNat stretchN);
-  out "stretch tree" stretchN c;
+    -- stretch memory tree
+    let c := check (make $ UInt32.ofNat stretchN)
+    out "stretch tree" stretchN c
 
-  -- allocate a long lived tree
-  let long := make $ UInt32.ofNat maxN;
+    -- allocate a long lived tree
+    let long := make $ UInt32.ofNat maxN
 
-  -- allocate, walk, and deallocate many bottom-up binary trees
-  let vs := (depth minN maxN); -- `using` (parList $ evalTuple3 r0 r0 rseq)
-  vs.forM (fun (m, d, i) => out (toString m ++ "\t trees") d i.get);
+    -- allocate, walk, and deallocate many bottom-up binary trees
+    let vs := (depth minN maxN)  -- `using` (parList $ evalTuple3 r0 r0 rseq)
+    vs.forM (fun (m, d, i) => out s!"{m}\t trees" d i.get)
 
-  -- confirm the long-lived binary tree still exists
-  out "long lived tree" maxN (check long);
-  pure 0
-| _ => pure 1
+    -- confirm the long-lived binary tree still exists
+    out "long lived tree" maxN (check long)
+    return 0
+  | _ => return 1