From 4568fe755ca011aeaee6e0770b8a4856a693e8de Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sat, 2 Jul 2022 15:25:06 -0700
Subject: [PATCH] chore: fix tests

---
 tests/bench/liasolver.lean               |  8 ++++----
 tests/lean/run/646.lean                  |  2 +-
 tests/lean/run/binrel.lean               |  2 +-
 tests/lean/run/depElim1.lean             |  2 +-
 tests/lean/run/matrix.lean               |  4 ++--
 tests/lean/run/maze.lean                 | 17 ++++++++---------
 tests/lean/run/meta2.lean                |  4 ++--
 tests/lean/run/sharecommon.lean          | 16 ++++++++--------
 tests/lean/run/structInst4.lean          |  2 +-
 tests/lean/run/whnfDelayedMVarIssue.lean |  2 +-
 10 files changed, 29 insertions(+), 30 deletions(-)

diff --git a/tests/bench/liasolver.lean b/tests/bench/liasolver.lean
index c3feee8216..1bce91cd56 100644
--- a/tests/bench/liasolver.lean
+++ b/tests/bench/liasolver.lean
@@ -108,7 +108,7 @@ def gcd (coeffs : HashMap Nat Int) : Nat :=
   | #[]           => panic! "Cannot calculate GCD of empty list of coefficients"
   | #[(i, x)]     => x
   | coeffsContent =>
-    coeffsContent[0].2.gcd coeffsContent[1].2
+    coeffsContent[0]!.2.gcd coeffsContent[1]!.2
       |> coeffs.fold fun acc k v => acc.gcd v
 
 namespace Equation
@@ -302,9 +302,9 @@ where
       let mut assignment := assignment
       let mut r := eq.const
       for (i, coeff) in eq.coeffs do
-        if assignment[i].isNone then
+        if assignment[i]!.isNone then
           assignment := readSolution i assignment
-        r := r + coeff*assignment[i].get!
+        r := r + coeff*assignment[i]!.get!
       return assignment.set! varIdx (some r)
 
 partial def solveProblem' (p : Problem) : Solution := Id.run <| do
@@ -322,7 +322,7 @@ def isSatAssignment (p : Problem) (assignment : Array Int) : Bool :=
   ¬ p.equations.any fun _ (eq : Equation) => Id.run <| do
     let mut r := 0
     for (i, coeff) in eq.coeffs do
-      r := r + coeff*assignment[i]
+      r := r + coeff*assignment[i]!
     return r ≠ eq.const
 
 def solveProblem (p : Problem) : Solution :=
diff --git a/tests/lean/run/646.lean b/tests/lean/run/646.lean
index 813392ea35..5438956705 100644
--- a/tests/lean/run/646.lean
+++ b/tests/lean/run/646.lean
@@ -11,6 +11,6 @@ def bench (f : ∀ {α : Type}, α → IO Unit := fun _ => pure ()) : IO Unit :=
   let arr := build n
   timeit "time" $
     for _ in [:1000] do
-      f $ #[1, 2, 3, 4].map fun ty => arr[ty]
+      f $ #[1, 2, 3, 4].map fun ty => arr[ty]!
 
 #eval bench
diff --git a/tests/lean/run/binrel.lean b/tests/lean/run/binrel.lean
index 78459c1354..e7616d2823 100644
--- a/tests/lean/run/binrel.lean
+++ b/tests/lean/run/binrel.lean
@@ -30,7 +30,7 @@ def ex10 (x : Lean.Syntax) : Bool :=
 
 def ex11 (xs : Array (Nat × Nat)) :=
   let f a b := binrel% LT.lt a.1 b.1
-  f xs[1] xs[2]
+  f xs[1]! xs[2]!
 
 def ex12 (i j : Int) :=
   binrel% Eq (i, j) (0, 0)
diff --git a/tests/lean/run/depElim1.lean b/tests/lean/run/depElim1.lean
index a01fc2f43b..0676706af4 100644
--- a/tests/lean/run/depElim1.lean
+++ b/tests/lean/run/depElim1.lean
@@ -56,7 +56,7 @@ partial def mkPattern : Expr → MetaM Pattern
           e.isAppOfArity `ArrayLit3 4 ||
           e.isAppOfArity `ArrayLit4 5 then
     let args := e.getAppArgs
-    let type := args[0]
+    let type := args[0]!
     let ps   := args.extract 1 args.size
     let ps ← ps.toList.mapM mkPattern
     return Pattern.arrayLit type ps
diff --git a/tests/lean/run/matrix.lean b/tests/lean/run/matrix.lean
index 5ef07aca86..3d494c5fcc 100644
--- a/tests/lean/run/matrix.lean
+++ b/tests/lean/run/matrix.lean
@@ -57,10 +57,10 @@ instance [Mul α] : HMul α (Matrix m n α) (Matrix m n α) where
 end Matrix
 
 def m1 : Matrix 2 2 Int :=
-  fun i j => #[#[1, 2], #[3, 4]][i][j]
+  fun i j => #[#[1, 2], #[3, 4]][i]![j]!
 
 def m2 : Matrix 2 2 Int :=
-  fun i j => #[#[5, 6], #[7, 8]][i][j]
+  fun i j => #[#[5, 6], #[7, 8]][i]![j]!
 
 open Matrix -- activate .[.,.] notation
 
diff --git a/tests/lean/run/maze.lean b/tests/lean/run/maze.lean
index 5ef495d3bd..309aaca71a 100644
--- a/tests/lean/run/maze.lean
+++ b/tests/lean/run/maze.lean
@@ -98,9 +98,8 @@ def extractXY : Lean.Expr → Lean.MetaM Coords
 | e => do
   let e':Lean.Expr ← (Lean.Meta.whnf e)
   let sizeArgs := Lean.Expr.getAppArgs e'
-  let f := Lean.Expr.getAppFn e'
-  let x ← Lean.Meta.whnf sizeArgs[0]
-  let y ← Lean.Meta.whnf sizeArgs[1]
+  let x ← Lean.Meta.whnf sizeArgs[0]!
+  let y ← Lean.Meta.whnf sizeArgs[1]!
   let numCols := (Lean.Expr.natLit? x).get!
   let numRows := (Lean.Expr.natLit? y).get!
   return Coords.mk numCols numRows
@@ -111,8 +110,8 @@ partial def extractWallList : Lean.Expr → Lean.MetaM (List Coords)
   let f := Lean.Expr.getAppFn exp'
   if f.constName!.toString == "List.cons"
   then let consArgs := Lean.Expr.getAppArgs exp'
-       let rest ← extractWallList consArgs[2]
-       let ⟨wallCol, wallRow⟩ ← extractXY consArgs[1]
+       let rest ← extractWallList consArgs[2]!
+       let ⟨wallCol, wallRow⟩ ← extractXY consArgs[1]!
        return (Coords.mk wallCol wallRow) :: rest
   else return [] -- "List.nil"
 
@@ -120,9 +119,9 @@ partial def extractGameState : Lean.Expr → Lean.MetaM GameState
 | exp => do
     let exp': Lean.Expr ← (Lean.Meta.whnf exp)
     let gameStateArgs := Lean.Expr.getAppArgs exp'
-    let size ← extractXY gameStateArgs[0]
-    let playerCoords ← extractXY gameStateArgs[1]
-    let walls ← extractWallList gameStateArgs[2]
+    let size ← extractXY gameStateArgs[0]!
+    let playerCoords ← extractXY gameStateArgs[1]!
+    let walls ← extractWallList gameStateArgs[2]!
     pure ⟨size, playerCoords, walls⟩
 
 def update2dArray {α : Type} : Array (Array α) → Coords → α → Array (Array α)
@@ -130,7 +129,7 @@ def update2dArray {α : Type} : Array (Array α) → Coords → α → Array (Ar
    Array.set! a y $ Array.set! (Array.get! a y) x v
 
 def update2dArrayMulti {α : Type} : Array (Array α) → List Coords → α → Array (Array α)
-| a, [], v => a
+| a, [], _ => a
 | a, c::cs, v =>
      let a' := update2dArrayMulti a cs v
      update2dArray a' c v
diff --git a/tests/lean/run/meta2.lean b/tests/lean/run/meta2.lean
index 50dca8fb08..580c151431 100644
--- a/tests/lean/run/meta2.lean
+++ b/tests/lean/run/meta2.lean
@@ -52,7 +52,7 @@ do print "----- tst3 -----";
    let t   := mkLambda `x BinderInfo.default nat $ mkBVar 0;
    let mvar ← mkFreshExprMVar (mkForall `x BinderInfo.default nat nat);
    lambdaTelescope t fun xs _ => do
-     let x := xs[0];
+     let x := xs[0]!
      checkM $ isExprDefEq (mkApp mvar x) (mkAppN add #[x, mkAppN add #[mkNatLit 10, x]]);
      pure ();
    let v ← getAssignment mvar;
@@ -65,7 +65,7 @@ def tst4 : MetaM Unit :=
 do print "----- tst4 -----";
    let t   := mkLambda `x BinderInfo.default nat $ mkBVar 0;
    lambdaTelescope t fun xs _ => do
-     let x := xs[0];
+     let x := xs[0]!
      let mvar ← mkFreshExprMVar (mkForall `x BinderInfo.default nat nat);
      -- the following `isExprDefEq` fails because `x` is also in the context of `mvar`
      checkM $ not <$> isExprDefEq (mkApp mvar x) (mkAppN add #[x, mkAppN add #[mkNatLit 10, x]]);
diff --git a/tests/lean/run/sharecommon.lean b/tests/lean/run/sharecommon.lean
index 3e8117d796..a093c59c30 100644
--- a/tests/lean/run/sharecommon.lean
+++ b/tests/lean/run/sharecommon.lean
@@ -100,20 +100,20 @@ IO.println c
 check $
   ptrAddrUnsafe a != ptrAddrUnsafe b &&
   ptrAddrUnsafe a != ptrAddrUnsafe c &&
-  ptrAddrUnsafe a[0] != ptrAddrUnsafe a[1] &&
-  ptrAddrUnsafe a[0] != ptrAddrUnsafe a[2] &&
-  ptrAddrUnsafe b[0] != ptrAddrUnsafe b[1] &&
-  ptrAddrUnsafe c[0] != ptrAddrUnsafe c[1]
+  ptrAddrUnsafe a[0]! != ptrAddrUnsafe a[1]! &&
+  ptrAddrUnsafe a[0]! != ptrAddrUnsafe a[2]! &&
+  ptrAddrUnsafe b[0]! != ptrAddrUnsafe b[1]! &&
+  ptrAddrUnsafe c[0]! != ptrAddrUnsafe c[1]!
 let a ← shareCommonM a
 let b ← shareCommonM b
 let c ← shareCommonM c
 check $
   ptrAddrUnsafe a == ptrAddrUnsafe b &&
   ptrAddrUnsafe a != ptrAddrUnsafe c &&
-  ptrAddrUnsafe a[0] == ptrAddrUnsafe a[1] &&
-  ptrAddrUnsafe a[0] != ptrAddrUnsafe a[2] &&
-  ptrAddrUnsafe b[0] == ptrAddrUnsafe b[1] &&
-  ptrAddrUnsafe c[0] == ptrAddrUnsafe c[1]
+  ptrAddrUnsafe a[0]! == ptrAddrUnsafe a[1]! &&
+  ptrAddrUnsafe a[0]! != ptrAddrUnsafe a[2]! &&
+  ptrAddrUnsafe b[0]! == ptrAddrUnsafe b[1]! &&
+  ptrAddrUnsafe c[0]! == ptrAddrUnsafe c[1]!
 pure ()
 
 #eval tst5.run
diff --git a/tests/lean/run/structInst4.lean b/tests/lean/run/structInst4.lean
index 99fc8cba77..cde1f3d5e3 100644
--- a/tests/lean/run/structInst4.lean
+++ b/tests/lean/run/structInst4.lean
@@ -15,7 +15,7 @@ structure Foo :=
 
 def foo : Foo := {}
 
-#check foo.x[1].1.2
+#check foo.x[1]!.1.2
 
 #check { foo with x[1].2 := true }
 #check { foo with x[1].fst.snd := 1 }
diff --git a/tests/lean/run/whnfDelayedMVarIssue.lean b/tests/lean/run/whnfDelayedMVarIssue.lean
index 76efdb0389..5c9e93f5cf 100644
--- a/tests/lean/run/whnfDelayedMVarIssue.lean
+++ b/tests/lean/run/whnfDelayedMVarIssue.lean
@@ -3,7 +3,7 @@ def Nat.isZero (n : Nat) :=
 
 def test (preDefs : Array (Array Nat)) : IO Unit := do
   for preDefs in preDefs do
-    let preDef := preDefs[0]
+    let preDef := preDefs[0]!
     if preDef.isZero then
       pure ()
     else