chore: add temporary workaround to tests

We will remove it after we implement `doMatch`

src/Lean/Elab/Do.lean

@@ -127,10 +127,10 @@ private partial def expandDoElems : Bool → Array Syntax → Nat → MacroM Syn
         rest ← mkRest ();
         newBody ←
           if optElse.isNone then do
-            `(do let x ← $discr; match x with | $pat => $rest)
+            `(do let x ← $discr; (match x with | $pat => $rest))
           else
             let elseBody := optElse.getArg 1;
-            `(do let x ← $discr; match x with | $pat => $rest | _ => $elseBody);
+            `(do let x ← $discr; (match x with | $pat => $rest | _ => $elseBody));
         addPrefix newBody
       else if i < doElems.size - 1 && doElem.getKind == `Lean.Parser.Term.doExpr then do
         -- def doExpr := parser! termParser

tests/lean/PPRoundtrip.lean

@@ -17,12 +17,12 @@ let stx' ← liftCoreM $ PrettyPrinter.parenthesizeTerm stx';
 let f' ← liftCoreM $ PrettyPrinter.formatTerm stx';
 IO.println $ f'.pretty opts;
 let env ← getEnv;
-match Parser.runParserCategory env `term (toString f') "<input>" with
+(match Parser.runParserCategory env `term (toString f') "<input>" with
 | Except.error e => throwErrorAt stx e
 | Except.ok stx'' => do
   let e' ← elabTermAndSynthesize stx'' none <* throwErrorIfErrors;
   unlessM (isDefEq e e') $
-    throwErrorAt stx (fmt "failed to round-trip" ++ line ++ fmt e ++ line ++ fmt e')
+    throwErrorAt stx (fmt "failed to round-trip" ++ line ++ fmt e ++ line ++ fmt e'))
 
 -- set_option trace.PrettyPrinter.parenthesize true
 set_option format.width 20

tests/lean/run/28.lean

@@ -39,6 +39,6 @@ def evalInstr : instr → sim (Option val)
 | instr.store _ _ _ =>
    do let pv <- f;
       g;
-      match pv with
-      | val.bv 27 _ => throw (IO.userError "asdf")
-      | _ => throw (IO.userError "expected pointer value in store" )
+      (match pv with
+       | val.bv 27 _ => throw (IO.userError "asdf")
+       | _ => throw (IO.userError "expected pointer value in store" ))

tests/lean/run/catchThe.lean

@@ -9,9 +9,9 @@ abbrev M := ExceptT String $ MetaM
 
 def testM {α} [HasBeq α] [HasToString α] (x : M α) (expected : α)  : MetaM Unit := do
 let r ← x;
-match r with
+(match r with
 | Except.ok a    => unless (a == expected) $ throwError ("unexpected result " ++ toString a)
-| Except.error e => throwError ("FAILED: " ++ e)
+| Except.error e => throwError ("FAILED: " ++ e))
 
 @[noinline] def act1 : M Nat :=
 throwThe Exception $ Exception.error Syntax.missing "Error at act1"

tests/lean/run/depElim1.lean

@@ -26,20 +26,20 @@ inductive ArrayLit4 {α : Sort u} (a b c d : α) : Type u | mk : ArrayLit4 a b c
 
 private def getConstructorVal (ctorName : Name) (fn : Expr) (args : Array Expr) : MetaM (Option (ConstructorVal × Expr × Array Expr)) := do
 let env ← getEnv;
-match env.find? ctorName with
+(match env.find? ctorName with
 | some (ConstantInfo.ctorInfo v) => if args.size == v.nparams + v.nfields then pure $ some (v, fn, args) else pure none
-| _                              => pure none
+| _                              => pure none)
 
 private def constructorApp? (e : Expr) : MetaM (Option (ConstructorVal × Expr × Array Expr)) := do
 let env ← getEnv;
-match e with
+(match e with
 | Expr.lit (Literal.natVal n) _ =>
    if n == 0 then getConstructorVal `Nat.zero (mkConst `Nat.zero) #[] else getConstructorVal `Nat.succ (mkConst `Nat.succ) #[mkNatLit (n-1)]
 | _ =>
   let fn := e.getAppFn;
   match fn with
   | Expr.const n _ _ => getConstructorVal n fn e.getAppArgs
-  | _                => pure none
+  | _                => pure none)
 
 /- Convert expression using auxiliary hints `inaccessible` and `val` into a pattern -/
 partial def mkPattern : Expr → MetaM Pattern
@@ -75,13 +75,13 @@ partial def mkPattern : Expr → MetaM Pattern
     | none => do
       let e ← whnfD e;
       let r? ← constructorApp? e;
-      match r? with
+      (match r? with
       | none      => throwError "unexpected pattern"
       | some (cval, fn, args) => do
         let params := args.extract 0 cval.nparams;
         let fields := args.extract cval.nparams args.size;
         let pats ← fields.toList.mapM mkPattern;
-        pure $ Pattern.ctor cval.name fn.constLevels! params.toList pats
+        pure $ Pattern.ctor cval.name fn.constLevels! params.toList pats)
 
 partial def decodePats : Expr → MetaM (List Pattern)
 | e =>

tests/lean/run/elabCmd.lean

@@ -7,21 +7,21 @@ open Lean.Elab.Term
 
 def getCtors (c : Name) : TermElabM (List Name) := do
 let env ← getEnv;
-match env.find? c with
+(match env.find? c with
 | some (ConstantInfo.inductInfo val) =>
   pure val.ctors
-| _ => pure []
+| _ => pure [])
 
-def elabAnonCtor (args : Syntax) (τ : Expr) : TermElabM Expr := do
+def elabAnonCtor (args : Syntax) (τ : Expr) : TermElabM Expr :=
   match τ.getAppFn with
   | Expr.const C _ _ => do
     let ctors ← getCtors C;
-    match ctors with
+    (match ctors with
     | [c] => do
       let stx ← `($(Lean.mkIdent c) $(Array.getSepElems args.getArgs)*);
       elabTerm stx τ
 -- error handling
-    | _ => unreachable!
+    | _ => unreachable!)
   | _ => unreachable!
 
 elab "foo⟨" args:(sepBy term ", ") "⟩" : term <= τ => do

tests/lean/run/finally.lean

@@ -18,9 +18,9 @@ catch
 
 def checkE {α ε : Type} [HasBeq α] (x : IO (Except ε α)) (expected : α) : IO Unit := do
 let r ← x;
-match r with
+(match r with
 | Except.ok a    => unless (a == expected) $ throw $ IO.userError "unexpected result"
-| Except.error _ => throw $ IO.userError "unexpected error"
+| Except.error _ => throw $ IO.userError "unexpected error")
 
 #eval (tst1.run).run' 0
 

tests/lean/run/instuniv.lean

@@ -3,7 +3,7 @@ new_frontend
 open Lean
 
 unsafe def tst : IO Unit :=
-withImportModules [{module := `Init.Data.Array}] 0 fun env => do
+withImportModules [{module := `Init.Data.Array}] 0 fun env =>
    match env.find? `Array.foldl with
    | some info => do
      IO.println (info.instantiateTypeLevelParams [levelZero, levelZero]);

tests/lean/run/meta2.lean

@@ -16,9 +16,9 @@ unlessM x $ throwError "check failed"
 
 def getAssignment (m : Expr) : MetaM Expr :=
 do let v? ← getExprMVarAssignment? m.mvarId!;
-   match v? with
+   (match v? with
    | some v => pure v
-   | none   => throwError "metavariable is not assigned"
+   | none   => throwError "metavariable is not assigned")
 
 def nat   := mkConst `Nat
 def boolE := mkConst `Bool
@@ -734,12 +734,12 @@ check t;
 let t <- mkArrayLit nat [mkNatLit 1, mkNatLit 2];
 print t;
 check t;
-match t.arrayLit? with
+(match t.arrayLit? with
 | some (_, xs) => do
   check $ pure $ xs.length == 2;
-  match (xs.get! 0).natLit?, (xs.get! 1).natLit? with
+  (match (xs.get! 0).natLit?, (xs.get! 1).natLit? with
   | some 1, some 2 => pure ()
-  | _, _           => throwError "nat lits expected"
-| none => throwError "array lit expected"
+  | _, _           => throwError "nat lits expected")
+| none => throwError "array lit expected")
 
 #eval tst42

tests/lean/run/meta3.lean

@@ -17,9 +17,9 @@ unlessM x $ throwError "check failed"
 
 def getAssignment (m : Expr) : MetaM Expr :=
 do let v? ← getExprMVarAssignment? m.mvarId!;
-   match v? with
+   (match v? with
    | some v => pure v
-   | none   => throwError "metavariable is not assigned"
+   | none   => throwError "metavariable is not assigned")
 
 unsafe def run (mods : List Name) (x : MetaM Unit) (opts : Options := dbgOpt) : IO Unit :=
 withImportModules (mods.map $ fun m => {module := m}) 0 fun env => do

tests/lean/run/structInst2.lean

@@ -12,9 +12,9 @@ variables {m : Type u → Type v} [Monad m] {α β : Type u}
 @[inline] protected def bind (ma : OptionT2 m α) (f : α → OptionT2 m β) : OptionT2 m β :=
 (do {
     let a? ← ma;
-    match a? with
+    (match a? with
     | some a => f a
-    | none   => pure none
+    | none   => pure none)
 } : m (Option β))
 
 @[inline] protected def pure (a : α) : OptionT2 m α :=
@@ -22,9 +22,9 @@ variables {m : Type u → Type v} [Monad m] {α β : Type u}
 
 @[inline] protected def orelse (ma : OptionT2 m α) (mb : OptionT2 m α) : OptionT2 m α :=
 (do { let a? ← ma;
-        match a? with
+        (match a? with
         | some a => pure (some a)
-        | _      => mb } : m (Option α))
+        | _      => mb) } : m (Option α))
 
 @[inline] protected def fail : OptionT2 m α :=
 (pure none : m (Option α))

tests/lean/run/termparsertest1.lean

@@ -17,9 +17,9 @@ is.forM $ fun input => do
 def testParserFailure (input : String) : IO Unit :=
 do
 let env ← mkEmptyEnvironment;
-match runParserCategory env `term input "<input>" with
+(match runParserCategory env `term input "<input>" with
 | Except.ok stx    => throw (IO.userError ("unexpected success\n" ++ toString stx))
-| Except.error msg => IO.println ("failed as expected, error: " ++ msg)
+| Except.error msg => IO.println ("failed as expected, error: " ++ msg))
 
 def testFailures (is : List String) : IO Unit :=
 is.forM $ fun input => do

tests/lean/run/toExpr.lean

@@ -14,16 +14,16 @@ let decl := Declaration.defnDecl {
   isUnsafe := false
 };
 IO.println (toExpr a);
-match env.addAndCompile {} decl with
+(match env.addAndCompile {} decl with
 | Except.error _ => throwError "addDecl failed"
-| Except.ok env  => do
+| Except.ok env  =>
   match env.evalConst α auxName with
   | Except.error ex => throwError ex
   | Except.ok b => do
     IO.println b;
     unless (a == b) $
       throwError "toExpr failed";
-    pure ()
+    pure ())
 
 #eval test #[(1, 2), (3, 4)]
 #eval test ['a', 'b', 'c']