tests

Author: kim-em

tests/bench/liasolver.lean

@@ -64,10 +64,10 @@ namespace Std.HashMap
     return false
 
   def mapValsM [Monad m] (f : β → m γ) (xs : HashMap α β) : m (HashMap α γ) :=
-    HashMap.empty (capacity := xs.size) |> xs.foldM fun acc k v => return acc.insert k (←f v)
+    HashMap.emptyWithCapacity (capacity := xs.size) |> xs.foldM fun acc k v => return acc.insert k (←f v)
 
   def mapVals (f : β → γ) (xs : HashMap α β) : HashMap α γ :=
-    HashMap.empty (capacity := xs.size) |> xs.fold fun acc k v => acc.insert k (f v)
+    HashMap.emptyWithCapacity (capacity := xs.size) |> xs.fold fun acc k v => acc.insert k (f v)
 
   def fastMapVals (f : α → β → β) (xs : HashMap α β) : HashMap α β :=
     xs.map f
@@ -275,7 +275,7 @@ partial def readSolution? (p : Problem) : Option Solution := Id.run <| do
     return none
   if p.equations.any (fun _ eq => eq.const ≠ 0) then
     return some Solution.unsat
-  let mut assignment : Array (Option Int) := mkArray p.nVars none
+  let mut assignment : Array (Option Int) := Array.replicate p.nVars none
   for i in *...p.nVars do
     assignment := readSolution i assignment
   return Solution.sat <| assignment.map (·.get!)

tests/lean/match4.lean

@@ -44,7 +44,7 @@ match x with
 def Vector' (α : Type) (n : Nat) := { a : Array α // a.size = n }
 
 def mkVec {α : Type} (n : Nat) (a : α) : Vector' α n :=
-⟨mkArray n a, Array.size_mkArray ..⟩
+⟨Array.replicate n a, Array.size_replicate ..⟩
 
 structure S :=
 (n : Nat)

tests/lean/repr_issue.lean

@@ -13,5 +13,5 @@ foo
 
 -- The following examples were producing an element of Type `id (Except String Nat)`.
 -- Type class resolution was failing to produce an instance for `Repr (id (Except String Nat))` because `id` is not transparent.
-#eval ex₁.run' (mkArray 10 1000) |>.run
-#eval ex₂.run' (mkArray 10 1000) |>.run
+#eval ex₁.run' (Array.replicate 10 1000) |>.run
+#eval ex₂.run' (Array.replicate 10 1000) |>.run

tests/lean/run/addDecorationsWithoutPartial.lean

@@ -39,8 +39,8 @@ unsafe def replaceUnsafeM (size : USize) (e : Expr) (f? : (e' : Expr) → sizeOf
 private def notAnExpr : Unit × Unit := ⟨⟨⟩, ⟨⟩⟩
 
 unsafe def initCache : State :=
-  { keys    := mkArray cacheSize.toNat (cast lcProof notAnExpr), -- `notAnExpr` is not a valid `Expr`
-    results := mkArray cacheSize.toNat default }
+  { keys    := Array.replicate cacheSize.toNat (cast lcProof notAnExpr), -- `notAnExpr` is not a valid `Expr`
+    results := Array.replicate cacheSize.toNat default }
 
 unsafe def replaceUnsafe (e : Expr) (f? : (e' : Expr) → sizeOf e' ≤ sizeOf e → Option Expr) : Expr :=
   (replaceUnsafeM cacheSize e f?).run' initCache

tests/lean/run/array1.lean

@@ -5,7 +5,7 @@ def v : Array Nat := Array.mk [1, 2, 3, 4]
 #guard v == #[1, 2, 3, 4, ]
 
 def w : Array Nat :=
-(mkArray 9 1).push 3
+(Array.replicate 9 1).push 3
 
 #check @Array.casesOn
 
@@ -15,17 +15,17 @@ def f : Fin w.size → Nat :=
 def arraySum (a : Array Nat) : Nat :=
 a.foldl Nat.add 0
 
-#guard mkArray 4 1 == #[1, 1, 1, 1]
+#guard Array.replicate 4 1 == #[1, 1, 1, 1]
 
 #guard Array.map (fun x => x+10) v == #[11, 12, 13, 14]
 
 #guard f ⟨1, sorry⟩ == 1
 
 #guard f ⟨9, sorry⟩ == 3
 
-#guard (((mkArray 1 1).push 2).push 3).foldl (fun x y => x + y) 0 == 6
+#guard (((Array.replicate 1 1).push 2).push 3).foldl (fun x y => x + y) 0 == 6
 
-#guard arraySum (mkArray 10 1) == 10
+#guard arraySum (Array.replicate 10 1) == 10
 
 axiom axLt {a b : Nat} : a < b
 

tests/lean/run/depElim1.lean

@@ -154,7 +154,7 @@ def mkTester (elimName : Name) (majors : List Expr) (lhss : List AltLHS) (inProp
 generalizeTelescope majors.toArray fun majors => do
   let resultType := if inProp then mkConst `True /- some proposition -/ else mkConst `Nat
   let matchType ← mkForallFVars majors resultType
-  Match.mkMatcher { matcherName := elimName, matchType, discrInfos := mkArray majors.size {}, lhss }
+  Match.mkMatcher { matcherName := elimName, matchType, discrInfos := Array.replicate majors.size {}, lhss }
 
 def test (ex : Name) (numPats : Nat) (elimName : Name) (inProp : Bool := false) : MetaM Unit :=
 withDepElimFrom ex numPats fun majors alts => do

tests/lean/run/maze.lean

@@ -144,13 +144,13 @@ def delabGameState : Lean.Expr → Lean.PrettyPrinter.Delaborator.Delab
        try extractGameState e
        catch err => failure -- can happen if game state has variables in it
 
-     let topBar := Array.mkArray numCols $ ← `(horizontal_border| ─)
+     let topBar := Array.replicate numCols $ ← `(horizontal_border| ─)
      let emptyCell ← `(game_cell| ░)
-     let emptyRow := Array.mkArray numCols emptyCell
+     let emptyRow := Array.replicate numCols emptyCell
      let emptyRowStx ← `(game_row| │$emptyRow:game_cell*│)
-     let allRows := Array.mkArray numRows emptyRowStx
+     let allRows := Array.replicate numRows emptyRowStx
 
-     let a0 := Array.mkArray numRows $ Array.mkArray numCols emptyCell
+     let a0 := Array.replicate numRows $ Array.replicate numCols emptyCell
      let a1 := update2dArray a0 playerCoords $ ← `(game_cell| @)
      let a2 := update2dArrayMulti a1 walls $ ← `(game_cell| ▓)
      let aa ← Array.mapM delabGameRow a2

tests/lean/run/unifhint2.lean

@@ -13,7 +13,7 @@ unif_hint natAddStep (x y z w : Nat) where
 def BV (n : Nat) := { a : Array Bool // a.size = n }
 
 def sext (x : BV s) (n : Nat) : BV (s+n) :=
-  ⟨mkArray (s+n) false, Array.size_mkArray ..⟩
+  ⟨Array.replicate (s+n) false, Array.size_replicate ..⟩
 
 def bvmul (x y : BV w) : BV w := x
 

tests/lean/run/unihint.lean

@@ -32,7 +32,7 @@ set_option pp.all true
 def BV (n : Nat) := { a : Array Bool // a.size = n }
 
 def sext (x : BV s) (n : Nat) : BV (s+n) :=
-  ⟨mkArray (s+n) false, Array.size_mkArray ..⟩
+  ⟨Array.replicate (s+n) false, Array.size_replicate ..⟩
 
 def bvmul (x y : BV w) : BV w :=
   x