From ed3c95f89255fcd8a98e088561ff4e91cf6b8652 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 27 Oct 2019 18:29:51 -0700 Subject: [PATCH] chore: fix tests --- tests/bench/binarytrees.lean | 2 +- tests/bench/qsort.lean | 4 ++-- tests/compiler/phashmap.lean | 4 ++-- tests/compiler/rbmap_library.lean | 2 +- tests/compiler/termparsertest1.lean | 4 ++-- tests/lean/binsearch.lean | 2 +- tests/lean/ctor_layout.lean | 6 +++--- tests/lean/ref1.lean | 6 +++--- 8 files changed, 15 insertions(+), 15 deletions(-) diff --git a/tests/bench/binarytrees.lean b/tests/bench/binarytrees.lean index 9d6a33852a..10349c67ed 100644 --- a/tests/bench/binarytrees.lean +++ b/tests/bench/binarytrees.lean @@ -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 (fun ⟨m,d,i⟩ => out (toString m ++ "\t trees") d i.get); + vs.mapM (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 57c88e3397..d5c85b119b 100644 --- a/tests/bench/qsort.lean +++ b/tests/bench/qsort.lean @@ -57,8 +57,8 @@ qsortAux lt as 0 (UInt32.ofNat (as.size - 1)) def main (xs : List String) : IO Unit := do let n := xs.head!.toNat; -n.mfor $ fun _ => -n.mfor $ fun i => do +n.forM $ fun _ => +n.forM $ fun i => do let xs := mkRandomArray i (UInt32.ofNat i) Array.empty; let xs := qsort xs (fun a b => a < b); --IO.println xs; diff --git a/tests/compiler/phashmap.lean b/tests/compiler/phashmap.lean index 4dc295605e..4815671f27 100644 --- a/tests/compiler/phashmap.lean +++ b/tests/compiler/phashmap.lean @@ -29,7 +29,7 @@ def mkMap (n : Nat) : Map := n.fold (fun i m => m.insert i (i*10)) PersistentHashMap.empty def check (n : Nat) (m : Map) : IO Unit := -n.mfor $ fun i => +n.forM $ fun i => match m.find i with | none => IO.println ("failed to find " ++ toString i) | some v => unless (v == i*10) (IO.println ("unexpected value " ++ toString i ++ " => " ++ toString v)) @@ -38,7 +38,7 @@ def delOdd (n : Nat) (m : Map) : Map := n.fold (fun i m => if i % 2 == 0 then m else m.erase i) m def check2 (n : Nat) (bot : Nat) (m : Map) : IO Unit := -n.mfor $ fun i => +n.forM $ fun i => if i % 2 == 0 && i >= bot then match m.find i with | none => IO.println ("failed to find " ++ toString i) diff --git a/tests/compiler/rbmap_library.lean b/tests/compiler/rbmap_library.lean index f8314d883f..7291f6890e 100644 --- a/tests/compiler/rbmap_library.lean +++ b/tests/compiler/rbmap_library.lean @@ -55,7 +55,7 @@ do IO.setRandSeed seed; IO.println ("tst3 size: " ++ toString a.size); let m := a.iterate m (fun i ⟨k, v⟩ m => if i.val % 2 == 0 then m.erase k else m); check (sz m == a.size / 2); - a.miterate () (fun i ⟨k, v⟩ _ => when (i.val % 2 == 1) (check (m.find k == some v))); + a.iterateM () (fun i ⟨k, v⟩ _ => when (i.val % 2 == 1) (check (m.find k == some v))); IO.println ("tst3 after, depth: " ++ toString (depth m) ++ ", size: " ++ toString (sz m)); pure () diff --git a/tests/compiler/termparsertest1.lean b/tests/compiler/termparsertest1.lean index 5815f6b02e..772e6efd52 100644 --- a/tests/compiler/termparsertest1.lean +++ b/tests/compiler/termparsertest1.lean @@ -10,7 +10,7 @@ stx ← IO.ofExcept $ runParser env termPTables input "" "expr"; IO.println stx def test (is : List String) : IO Unit := -is.mfor $ fun input => do +is.forM $ fun input => do IO.println input; testParser input @@ -23,7 +23,7 @@ match runParser env termPTables input "" "expr" with | Except.error msg => IO.println ("failed as expected, error: " ++ msg) def testFailures (is : List String) : IO Unit := -is.mfor $ fun input => do +is.forM $ fun input => do IO.println input; testParserFailure input diff --git a/tests/lean/binsearch.lean b/tests/lean/binsearch.lean index ccdc08ce5d..f15e091f3b 100644 --- a/tests/lean/binsearch.lean +++ b/tests/lean/binsearch.lean @@ -7,7 +7,7 @@ do let as := mkAssocArray n Array.empty; IO.println as; let as := as.qsort (fun a b => a.1 < b.1); -(2*n).mfor $ fun i => do +(2*n).forM $ fun i => do let entry := as.binSearch (i, false) (fun a b => a.1 < b.1); IO.println (">> " ++ toString i ++ " ==> " ++ toString entry) diff --git a/tests/lean/ctor_layout.lean b/tests/lean/ctor_layout.lean index 93c3659634..3de301dc9c 100644 --- a/tests/lean/ctor_layout.lean +++ b/tests/lean/ctor_layout.lean @@ -6,13 +6,13 @@ def tst : IO Unit := do initSearchPath "../../library:."; env ← importModules [`Init.Lean.Compiler.IR.Basic]; ctorLayout ← IO.ofExcept $ getCtorLayout env `Lean.IR.Expr.reuse; - ctorLayout.fieldInfo.mfor $ fun finfo => IO.println (format finfo); + ctorLayout.fieldInfo.forM $ fun finfo => IO.println (format finfo); IO.println "---"; ctorLayout ← IO.ofExcept $ getCtorLayout env `Lean.EnvironmentHeader.mk; - ctorLayout.fieldInfo.mfor $ fun finfo => IO.println (format finfo); + ctorLayout.fieldInfo.forM $ fun finfo => IO.println (format finfo); IO.println "---"; ctorLayout ← IO.ofExcept $ getCtorLayout env `Subtype.mk; - ctorLayout.fieldInfo.mfor $ fun finfo => IO.println (format finfo); + ctorLayout.fieldInfo.forM $ fun finfo => IO.println (format finfo); pure () #eval tst diff --git a/tests/lean/ref1.lean b/tests/lean/ref1.lean index 809b3333ae..4ea83e08b2 100644 --- a/tests/lean/ref1.lean +++ b/tests/lean/ref1.lean @@ -4,18 +4,18 @@ do v ← r.get; IO.println (">> " ++ toString v) def initArray (r : IO.Ref (Array Nat)) (n : Nat) : IO Unit := -n.mfor $ fun i => do +n.forM $ fun i => do r.modify $ fun a => a.push (2*i) def showArrayRef (r : IO.Ref (Array Nat)) : IO Unit := do a ← r.swap ∅; - a.size.mfor (fun i => IO.println ("[" ++ toString i ++ "]: " ++ toString (a.get! i))); + a.size.forM (fun i => IO.println ("[" ++ toString i ++ "]: " ++ toString (a.get! i))); r.swap a; pure () def tst (n : Nat) : IO Unit := do r₁ ← IO.mkRef 0; - n.mfor $ λ _ => inc r₁; + n.forM $ λ _ => inc r₁; r₂ ← IO.mkRef (∅ : Array Nat); initArray r₂ n; showArrayRef r₂