From 745cc9902ba548cfaaacc95126f90618d563d2ec Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 3 Jul 2019 08:37:40 -0700 Subject: [PATCH] chore(tests/bench): fix tests --- tests/bench/binarytrees.lean | 8 ++++---- tests/bench/qsort.lean | 6 +++--- tests/bench/rbmap.lean | 4 ++-- tests/bench/rbmap_checkpoint.lean | 6 +++--- tests/bench/unionfind.lean | 20 ++++++++++---------- 5 files changed, 22 insertions(+), 22 deletions(-) diff --git a/tests/bench/binarytrees.lean b/tests/bench/binarytrees.lean index 54d31c8cb8..d4e07e1f5b 100644 --- a/tests/bench/binarytrees.lean +++ b/tests/bench/binarytrees.lean @@ -28,14 +28,14 @@ partial def sumT : UInt32 -> UInt32 -> UInt32 -> UInt32 | d i t := if i = 0 then t else - let a := check (make d) in + 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) in - (n, d, Task.mk (λ _, sumT (UInt32.ofNat d) (UInt32.ofNat n) 0)) :: depth (d+2) m + let n := 2 ^ (m - d + minN); + (n, d, Task.mk (fun _ => sumT (UInt32.ofNat d) (UInt32.ofNat n) 0)) :: depth (d+2) m else [] def main : List String → IO UInt32 @@ -53,7 +53,7 @@ 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 (toString m ++ "\t trees") d i.get); + vs.mmap (fun ⟨m,d,i⟩ => out (toString m ++ "\t trees") d i.get); -- confirm the the long-lived binary tree still exists out "long lived tree" maxN (check long); diff --git a/tests/bench/qsort.lean b/tests/bench/qsort.lean index c7fe68a698..69ab3ca9da 100644 --- a/tests/bench/qsort.lean +++ b/tests/bench/qsort.lean @@ -57,9 +57,9 @@ qsortAux lt as 0 (UInt32.ofNat (as.size - 1)) def main (xs : List String) : IO Unit := do let n := xs.head.toNat; -n.mfor $ λ _, -n.mfor $ λ i, do +n.mfor $ fun _ => +n.mfor $ fun i => do let xs := mkRandomArray i (UInt32.ofNat i) Array.empty; - let xs := qsort xs (λ a b, a < b); + let xs := qsort xs (fun a b => a < b); --IO.println xs; checkSortedAux xs 0 diff --git a/tests/bench/rbmap.lean b/tests/bench/rbmap.lean index 8d6e77e4ea..7e58649cf3 100644 --- a/tests/bench/rbmap.lean +++ b/tests/bench/rbmap.lean @@ -70,7 +70,7 @@ def mkMap (n : Nat) := mkMapAux n Leaf def main (xs : List String) : IO UInt32 := -let m := mkMap xs.head.toNat in -let v := fold (λ (k : Nat) (v : Bool) (r : Nat), if v then r + 1 else r) m 0 in +let m := mkMap xs.head.toNat; +let v := fold (fun (k : Nat) (v : Bool) (r : Nat) => if v then r + 1 else r) m 0; IO.println (toString v) *> pure 0 diff --git a/tests/bench/rbmap_checkpoint.lean b/tests/bench/rbmap_checkpoint.lean index c1e43050bf..be612f81ba 100644 --- a/tests/bench/rbmap_checkpoint.lean +++ b/tests/bench/rbmap_checkpoint.lean @@ -67,8 +67,8 @@ else ins t k v def mkMapAux (freq : Nat) : Nat → Tree → List Tree → List Tree | 0 m r := m::r | (n+1) m r := - let m := insert m n (n % 10 = 0) in - let r := if n % freq == 0 then m::r else r in + let m := insert m n (n % 10 = 0); + let r := if n % freq == 0 then m::r else r; mkMapAux n m r def mkMap (n : Nat) (freq : Nat) : List Tree := @@ -86,6 +86,6 @@ let n := n.toNat; let freq := freq.toNat; let freq := if freq == 0 then 1 else freq; let mList := mkMap n freq; -let v := fold (λ (k : Nat) (v : Bool) (r : Nat), if v then r + 1 else r) mList.head 0; +let v := fold (fun (k : Nat) (v : Bool) (r : Nat) => if v then r + 1 else r) mList.head 0; IO.println (toString (myLen mList 0) ++ " " ++ toString v) *> pure 0 diff --git a/tests/bench/unionfind.lean b/tests/bench/unionfind.lean index 98f3f4d846..4dfde10555 100644 --- a/tests/bench/unionfind.lean +++ b/tests/bench/unionfind.lean @@ -1,11 +1,11 @@ def StateT' (m : Type → Type) (σ : Type) (α : Type) := σ → m (α × σ) namespace StateT' variables {m : Type → Type} [Monad m] {σ : Type} {α β : Type} -@[inline] protected def pure (a : α) : StateT' m σ α := λ s, pure (a, s) -@[inline] protected def bind (x : StateT' m σ α) (f : α → StateT' m σ β) : StateT' m σ β := λ s, do (a, s') ← x s; f a s' -@[inline] def read : StateT' m σ σ := λ s, pure (s, s) -@[inline] def write (s' : σ) : StateT' m σ Unit := λ s, pure ((), s') -@[inline] def updt (f : σ → σ) : StateT' m σ Unit := λ s, pure ((), f s) +@[inline] protected def pure (a : α) : StateT' m σ α := fun s => pure (a, s) +@[inline] protected def bind (x : StateT' m σ α) (f : α → StateT' m σ β) : StateT' m σ β := fun s => do (a, s') ← x s; f a s' +@[inline] def read : StateT' m σ σ := fun s => pure (s, s) +@[inline] def write (s' : σ) : StateT' m σ Unit := fun s => pure ((), s') +@[inline] def updt (f : σ → σ) : StateT' m σ Unit := fun s => pure ((), f s) instance : Monad (StateT' m σ) := {pure := @StateT'.pure _ _ _, bind := @StateT'.bind _ _ _} end StateT' @@ -50,7 +50,7 @@ def findEntryAux : Nat → Node → M nodeData do { let e := s.fget ⟨n, h⟩; if e.find = n then pure e else do e₁ ← findEntryAux i e.find; - updt (λ s, s.set n e₁); + updt (fun s => s.set n e₁); pure e₁ } else error "invalid Node" @@ -63,17 +63,17 @@ do e ← findEntry n; pure e.find def mk : M Node := do n ← capacity; - updt $ λ s, s.push {find := n, rank := 1}; + updt $ fun s => s.push {find := n, rank := 1}; pure n def union (n₁ n₂ : Node) : M Unit := do r₁ ← findEntry n₁; r₂ ← findEntry n₂; if r₁.find = r₂.find then pure () - else updt $ λ s, + else updt $ fun s => if r₁.rank < r₂.rank then s.set r₁.find { find := r₂.find } else if r₁.rank = r₂.rank then - let s₁ := s.set r₁.find { find := r₂.find } in + let s₁ := s.set r₁.find { find := r₂.find }; s₁.set r₂.find { rank := r₂.rank + 1, .. r₂} else s.set r₂.find { find := r₁.find } @@ -120,7 +120,7 @@ else do numEqs def main (xs : List String) : IO UInt32 := -let n := xs.head.toNat in +let n := xs.head.toNat; match run (test n) with | (Except.ok v, s) := IO.println ("ok " ++ toString v) *> pure 0 | (Except.error e, s) := IO.println ("Error : " ++ e) *> pure 1