chore: cleanup src/Array/Basic.lean

src/Init/Data/Array.lean

@@ -7,5 +7,4 @@ prelude
 import Init.Data.Array.Basic
 import Init.Data.Array.QSort
 import Init.Data.Array.BinSearch
-import Init.Data.Array.ForIn
 import Init.Data.Array.Macros

src/Init/Data/Array/ForIn.lean

@@ -1,50 +0,0 @@
-/-
-Copyright (c) 2020 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Leonardo de Moura
--/
-prelude
-import Init.Data.Array.Basic
-
-namespace Array
-universes u v w
-
-/-
-  We claim this unsafe implementation is correct because an array cannot have more than `usizeSz` elements in our runtime.
-
-  This kind of low level trick can be removed with a little bit of compiler support. For example, if the compiler simplifies `as.size < usizeSz` to true. -/
-@[inline] unsafe def forInUnsafe {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (as : Array α) (b : β) (f : α → β → m (ForInStep β)) : m β :=
-  let sz := USize.ofNat as.size
-  let rec @[specialize] loop (i : USize) (b : β) : m β := do
-    if i < sz then
-      let a := as.uget i lcProof
-      match (← f a b) with
-      | ForInStep.done  b => pure b
-      | ForInStep.yield b => loop (i+1) b
-    else
-      pure b
-  loop 0 b
-
--- Move?
-private theorem zeroLtOfLt : {a b : Nat} → a < b → 0 < b
-  | 0,   _, h => h
-  | a+1, b, h =>
-    have a < b from Nat.ltTrans (Nat.ltSuccSelf _) h
-    zeroLtOfLt this
-
-/- Reference implementation for `Array.forIn` -/
-@[implementedBy Array.forInUnsafe]
-def forIn {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (as : Array α) (b : β) (f : α → β → m (ForInStep β)) : m β :=
-  let rec loop (i : Nat) (h : i ≤ as.size) (b : β) : m β := do
-    match i, h with
-    | 0,   _ => pure b
-    | i+1, h =>
-      have h' : i < as.size          from Nat.ltOfLtOfLe (Nat.ltSuccSelf i) h
-      have as.size - 1 < as.size     from Nat.subLt (zeroLtOfLt h') (decide! : 0 < 1)
-      have as.size - 1 - i < as.size from Nat.ltOfLeOfLt (Nat.subLe (as.size - 1) i) this
-      match (← f (as.get ⟨as.size - 1 - i, this⟩) b) with
-      | ForInStep.done b  => pure b
-      | ForInStep.yield b => loop i (Nat.leOfLt h') b
-  loop as.size (Nat.leRefl _) b
-
-end Array

src/Init/LeanInit.lean

@@ -7,7 +7,6 @@ prelude
 import Init.Data.Option.BasicAux
 import Init.Data.String.Basic
 import Init.Data.Array.Basic
-import Init.Data.Array.ForIn
 import Init.Data.UInt
 import Init.Data.Hashable
 import Init.Control.Reader

src/Lean/Meta/ExprDefEq.lean

@@ -717,7 +717,7 @@ private partial def processAssignment (mvarApp : Expr) (v : Expr) : MetaM Bool :
         let args := args.set ⟨i, h⟩ arg
         match arg with
         | Expr.fvar fvarId _ =>
-          if args.anyRange 0 i (fun prevArg => prevArg == arg) then
+          if args.any (start := 0) (stop := i) fun prevArg => prevArg == arg then
             useFOApprox args
           else if mvarDecl.lctx.contains fvarId && !cfg.quasiPatternApprox then
             useFOApprox args

src/Lean/Meta/Match/CaseArraySizes.lean

@@ -71,7 +71,7 @@ def caseArraySizes (mvarId : MVarId) (fvarId : FVarId) (sizes : Array Nat) (xNam
     let subst  := subgoal.subst
     let mvarId := subgoal.mvarId
     let hEqSz  := (subst.get hEq).fvarId!
-    if h : i < sizes.size then
+    if h : i.val < sizes.size then
        let n := sizes.get ⟨i, h⟩
        let mvarId ← clear mvarId subgoal.newHs[0]
        let mvarId ← clear mvarId (subst.get aSizeFVarId).fvarId!

src/Lean/Meta/Match/Match.lean

@@ -610,7 +610,7 @@ private def processValue (p : Problem) : MetaM (Array Problem) := do
     let values := collectValues p
     let subgoals ← caseValues p.mvarId x.fvarId! values
     subgoals.mapIdxM fun i subgoal => do
-      if h : i < values.size then
+      if h : i.val < values.size then
         let value := values.get ⟨i, h⟩
         -- (x = value) branch
         let subst := subgoal.subst
@@ -664,7 +664,7 @@ private def processArrayLit (p : Problem) : MetaM (Array Problem) := do
     let sizes := collectArraySizes p
     let subgoals ← caseArraySizes p.mvarId x.fvarId! sizes
     subgoals.mapIdxM fun i subgoal => do
-      if h : i < sizes.size then
+      if h : i.val < sizes.size then
         let size     := sizes.get! i
         let subst    := subgoal.subst
         let elems    := subgoal.elems.toList

src/Lean/Meta/WHNF.lean

@@ -72,7 +72,7 @@ private def toCtorWhenK (recVal : RecursorVal) (major : Expr) : MetaM (Option Ex
   let majorTypeI := majorType.getAppFn
   if !majorTypeI.isConstOf recVal.getInduct then
     pure none
-  else if majorType.hasExprMVar && majorType.getAppArgs.anyFrom recVal.nparams Expr.hasExprMVar then
+  else if majorType.hasExprMVar && majorType.getAppArgs.any (start := recVal.nparams) Expr.hasExprMVar then
     pure none
   else do
     let (some newCtorApp) ← mkNullaryCtor majorType recVal.nparams | pure none

src/Lean/PrettyPrinter/Formatter.lean

@@ -177,7 +177,7 @@ def categoryParser.formatter (cat : Name) : Formatter := group $ indent do
       let sp ← getStackSize
       stx.getArgs.forM fun stx => formatterForKind stx.getKind
       let stack ← getStack
-      if stack.size > sp && stack.anyRange sp stack.size fun f => f.pretty != (stack.get! sp).pretty then
+      if stack.size > sp && stack.any (start := sp) (stop := stack.size) fun f => f.pretty != (stack.get! sp).pretty then
         panic! "Formatter.visit: inequal choice children";
       -- discard all but one child format
       setStack $ stack.extract 0 (sp+1)

src/Lean/Syntax.lean

@@ -283,7 +283,10 @@ partial def reprint : Syntax → Option String
       if args.size == 0 then failure
       else do
         let s ← reprint args[0]
-        args.foldlFromM (fun s stx => do let s' ← reprint stx; guard (s == s'); pure s) s 1
+        args.foldlM (init := s) (start := 1) fun s stx => do
+          let s' ← reprint stx
+          guard (s == s')
+          pure s
     else args.foldlM (fun r stx => do let s ← reprint stx; pure $ r ++ s) ""
   | _ => ""
 

src/Std/Data/PersistentArray.lean

@@ -197,15 +197,15 @@ variable {β : Type v}
 | node cs, i, shift, b => do
   let j    := (div2Shift i shift).toNat
   let b ← foldlFromMAux f (cs.get! j) (mod2Shift i shift) (shift - initShift) b
-  cs.foldlFromM (fun b c => foldlMAux f c b) b (j+1)
-| leaf vs, i, _, b => vs.foldlFromM f b i.toNat
+  cs.foldlM (init := b) (start := j+1) fun b c => foldlMAux f c b
+| leaf vs, i, _, b => vs.foldlM (init := b) (start := i.toNat) f
 
 @[specialize] def foldlM (t : PersistentArray α) (f : β → α → m β) (init : β) (start : Nat := 0) : m β := do
 if start == 0 then
   let b ← foldlMAux f t.root init
   t.tail.foldlM f b
 else if start >= t.tailOff then
-  t.tail.foldlFromM f init (start - t.tailOff)
+  t.tail.foldlM (init := init) (start := start - t.tailOff) f
 else do
   let b ← foldlFromMAux f t.root (USize.ofNat start) t.shift init;
   t.tail.foldlM f b

tests/compiler/rbmap_library.lean

@@ -57,9 +57,17 @@ do IO.setRandSeed seed
    check (sz m == a.size)
    check (a.all (fun ⟨k, v⟩ => m.find? k == some v))
    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)
+   let i := 0
+   for (k, b) in a do
+     if i % 2 == 0 then
+       m := m.erase k
+     i := i + 1
    check (sz m == a.size / 2)
-   a.iterateM () (fun i ⟨k, v⟩ _ => when (i.val % 2 == 1) (check (m.find? k == some v)))
+   let i := 0
+   for (k, v) in a do
+     if i % 2 == 1 then
+       check (m.find? k == some v)
+     i := i + 1
    IO.println ("tst3 after, depth: " ++ toString (depth m) ++ ", size: " ++ toString (sz m))
    pure ()
 

tests/lean/lvl1.lean

@@ -4,7 +4,7 @@ namespace Lean
 namespace Level
 
 def mkMax (xs : Array Level) : Level :=
-xs.foldlFrom mkLevelMax (xs.get! 0) 1
+xs.foldl (start := 1) (init := xs[0]) mkLevelMax
 
 #eval toString $ normalize $ mkLevelSucc $ mkLevelSucc $ mkMax #[levelZero, mkLevelParam `w, mkLevelSucc (mkLevelSucc (mkLevelSucc (mkLevelParam `z))), levelOne, mkLevelSucc (mkLevelSucc (mkLevelParam `x)), levelZero, mkLevelParam `x, mkLevelParam `y, mkLevelParam `x, mkLevelParam `z, mkLevelSucc levelOne, mkLevelParam `w, mkLevelSucc (mkLevelParam `x)]
 #eval toString $ normalize $ mkLevelMax levelZero (mkLevelParam `x)