chore: update stage0

src/Lean/Elab/Do.lean

@@ -765,6 +765,19 @@ private def expandDoIf? (stx : Syntax) : MacroM (Option Syntax) := match stx wit
     return some e
   | _ => pure none
 
+/--
+  If the given syntax is a `doLetExpr` or `doLetMetaExpr`, return an equivalent `doIf` that has an `else` but no `else if`s or `if let`s.  -/
+private def expandDoLetExpr? (stx : Syntax) (doElems : List Syntax) : MacroM (Option Syntax) := match stx with
+  | `(doElem| let_expr $pat:matchExprPat := $discr:term | $elseBranch:doSeq) =>
+    return some (← `(doElem| match_expr (meta := false) $discr:term with
+                             | $pat:matchExprPat => $(mkDoSeq doElems.toArray)
+                             | _ => $elseBranch))
+  | `(doElem| let_expr $pat:matchExprPat ← $discr:term | $elseBranch:doSeq) =>
+    return some (← `(doElem| match_expr $discr:term with
+                             | $pat:matchExprPat => $(mkDoSeq doElems.toArray)
+                             | _ => $elseBranch))
+  | _ => return none
+
 structure DoIfView where
   ref        : Syntax
   optIdent   : Syntax
@@ -1146,7 +1159,8 @@ where
       for alt in alts do
         let rhs ← toTerm alt.rhs
         let optVar := if let some var := alt.var? then mkNullNode #[var, mkAtomFrom var "@"] else mkNullNode #[]
-        let termAlt := mkNode ``Parser.Term.matchExprAlt #[mkAtomFrom alt.ref "|", optVar, alt.funName, mkNullNode alt.pvars, mkAtomFrom alt.ref "=>", rhs]
+        let pat := mkNode ``Parser.Term.matchExprPat #[optVar, alt.funName, mkNullNode alt.pvars]
+        let termAlt := mkNode ``Parser.Term.matchExprAlt #[mkAtomFrom alt.ref "|", pat, mkAtomFrom alt.ref "=>", rhs]
         termAlts := termAlts.push termAlt
       let elseBranch := mkNode ``Parser.Term.matchExprElseAlt #[mkAtomFrom ref "|", mkHole ref, mkAtomFrom ref "=>", (← toTerm elseBranch)]
       let termMatchExprAlts := mkNode ``Parser.Term.matchExprAlts #[mkNullNode termAlts, elseBranch]
@@ -1614,10 +1628,11 @@ mutual
     let discr     := doMatchExpr[2]
     let alts      := doMatchExpr[4][0].getArgs -- Array of `doMatchExprAlt`
     let alts ← alts.mapM fun alt => do
-      let var? := if alt[1].isNone then none else some alt[1][0]
-      let funName  := alt[2]
-      let pvars    := alt[3].getArgs
-      let rhs      := alt[5]
+      let pat      := alt[1]
+      let var?     := if pat[0].isNone then none else some pat[0][0]
+      let funName  := pat[1]
+      let pvars    := pat[2].getArgs
+      let rhs      := alt[3]
       let rhs ← doSeqToCode (getDoSeqElems rhs)
       pure { ref, var?, funName, pvars, rhs }
     let elseBranch ← doSeqToCode (getDoSeqElems doMatchExpr[4][1][3])
@@ -1693,6 +1708,9 @@ mutual
       | none =>
       match (← liftMacroM <| expandDoIf? doElem) with
       | some doElem => doSeqToCode (doElem::doElems)
+      | none =>
+      match (← liftMacroM <| expandDoLetExpr? doElem doElems) with
+      | some doElem => doSeqToCode [doElem]
       | none =>
         let (liftedDoElems, doElem) ← expandLiftMethod doElem
         if !liftedDoElems.isEmpty then

src/Lean/Elab/MatchExpr.lean

@@ -52,23 +52,22 @@ Converts syntax representing a `match_expr` else-alternative into an `ElseAlt`.
 -/
 def toElseAlt? (stx : Syntax) : Option ElseAlt :=
   if !stx.isOfKind ``matchExprElseAlt then none else
-  some { rhs := stx.getArg 3 }
+  some { rhs := stx[3] }
 
 /--
 Converts syntax representing a `match_expr` alternative into an `Alt`.
 -/
 def toAlt? (stx : Syntax) : Option Alt :=
   if !stx.isOfKind ``matchExprAlt then none else
-  let var? : Option Ident :=
-    let optVar := stx.getArg 1
-    if optVar.isNone then none else some ⟨optVar.getArg 0⟩
-  let funName := ⟨stx.getArg 2⟩
-  let pvars := stx.getArg 3 |>.getArgs.toList.reverse.map fun arg =>
-    match arg with
-    | `(_) => none
-    | _ => some ⟨arg⟩
-  let rhs := stx.getArg 5
-  some { var?, funName, pvars, rhs }
+  match stx[1] with
+  | `(matchExprPat| $[$var? @]? $funName:ident $pvars*) =>
+    let pvars := pvars.toList.reverse.map fun arg =>
+      match arg.raw with
+      | `(_) => none
+      | _ => some ⟨arg⟩
+    let rhs := stx[3]
+    some { var?, funName, pvars, rhs }
+  | _ => none
 
 /--
 Returns the function names of alternatives that do not have any pattern variable left.
@@ -198,7 +197,15 @@ end MatchExpr
 @[builtin_macro Lean.Parser.Term.matchExpr] def expandMatchExpr : Macro := fun stx =>
   match stx with
   | `(match_expr $discr:term with $alts) =>
-    MatchExpr.main discr (alts.raw.getArg 0).getArgs (alts.raw.getArg 1)
+    MatchExpr.main discr alts.raw[0].getArgs alts.raw[1]
+  | _ => Macro.throwUnsupported
+
+@[builtin_macro Lean.Parser.Term.letExpr] def expandLetExpr : Macro := fun stx =>
+  match stx with
+  | `(let_expr $pat:matchExprPat := $discr:term | $elseBranch:term; $body:term) =>
+    `(match_expr $discr with
+      | $pat:matchExprPat => $body
+      | _ => $elseBranch)
   | _ => Macro.throwUnsupported
 
 end Lean.Elab.Term

src/Lean/Parser/Do.lean

@@ -60,6 +60,14 @@ def notFollowedByRedefinedTermToken :=
   "let " >> optional "mut " >> termParser >> " := " >> termParser >>
   checkColGt >> " | " >> doSeq
 
+@[builtin_doElem_parser] def doLetExpr  := leading_parser
+  "let_expr " >> matchExprPat >> " := " >> termParser >>
+  checkColGt >> " | " >> doSeq
+
+@[builtin_doElem_parser] def doLetMetaExpr  := leading_parser
+  "let_expr " >> matchExprPat >> " ← " >> termParser >>
+  checkColGt >> " | " >> doSeq
+
 @[builtin_doElem_parser] def doLetRec   := leading_parser
   group ("let " >> nonReservedSymbol "rec ") >> letRecDecls
 def doIdDecl   := leading_parser
@@ -151,8 +159,10 @@ def doMatchAlts := ppDedent <| matchAlts (rhsParser := doSeq)
   sepBy1 matchDiscr ", " >> " with" >> doMatchAlts
 
 def doMatchExprAlts := ppDedent <| matchExprAlts (rhsParser := doSeq)
+def optMetaFalse :=
+  optional ("(" >> nonReservedSymbol "meta" >>  " := " >> nonReservedSymbol "false" >> ") ")
 @[builtin_doElem_parser] def doMatchExpr := leading_parser:leadPrec
-  "match_expr " >> optional ("(" >> nonReservedSymbol "meta" >>  " := " >> nonReservedSymbol "false" >> ") ") >> termParser >> " with" >> doMatchExprAlts
+  "match_expr " >> optMetaFalse >> termParser >> " with" >> doMatchExprAlts
 
 def doCatch      := leading_parser
   ppDedent ppLine >> atomic ("catch " >> binderIdent) >> optional (" : " >> termParser) >> darrow >> doSeq

src/Lean/Parser/Term.lean

@@ -826,7 +826,8 @@ Implementation of the `show_term` term elaborator.
 `match_expr` support.
 -/
 
-def matchExprAlt (rhsParser : Parser) := leading_parser "| " >> ppIndent (optional (atomic (ident >> "@")) >> ident >> many binderIdent >> " => " >> rhsParser)
+def matchExprPat := leading_parser optional (atomic (ident >> "@")) >> ident >> many binderIdent
+def matchExprAlt (rhsParser : Parser) := leading_parser "| " >> ppIndent (matchExprPat >> " => " >> rhsParser)
 def matchExprElseAlt (rhsParser : Parser) := leading_parser "| " >> ppIndent (hole >> " => " >> rhsParser)
 def matchExprAlts (rhsParser : Parser) :=
   leading_parser withPosition $
@@ -835,6 +836,9 @@ def matchExprAlts (rhsParser : Parser) :=
 @[builtin_term_parser] def matchExpr := leading_parser:leadPrec
   "match_expr " >> termParser >> " with" >> ppDedent (matchExprAlts termParser)
 
+@[builtin_term_parser] def letExpr := leading_parser:leadPrec
+  withPosition ("let_expr " >> matchExprPat >> " := " >> termParser >> checkColGt >> " | " >> termParser) >> optSemicolon termParser
+
 end Term
 
 @[builtin_term_parser default+1] def Tactic.quot : Parser := leading_parser

tests/lean/run/match_expr.lean

@@ -54,3 +54,65 @@ run_meta do
   discard <| isDefEq m e
   let m ← test2 m
   logInfo m
+
+def test3 (e : Expr) : Option Expr :=
+  let_expr c@Eq α a b := e | none
+  some (mkApp3 c α b a)
+
+def test4 (e : Expr) : Option Expr :=
+  let_expr Eq.refl _ a := e | none
+  some a
+
+/--
+info: 3 = 1
+---
+info: 3
+---
+info: 4 = 2
+-/
+#guard_msgs in
+run_meta do
+  let eq ← mkEq (toExpr 1) (toExpr 3)
+  let eq := mkAnnotation `foo eq
+  let some eq := test3 eq | throwError "unexpected"
+  logInfo eq
+  let rfl ← mkEqRefl (toExpr 3)
+  let some n := test4 rfl | throwError "unexpected"
+  logInfo n
+  let eq := mkAnnotation `boo <| mkApp (mkAnnotation `bla (mkApp (mkAnnotation `foo eq.appFn!.appFn!) (toExpr 2))) (toExpr 4)
+  let some eq := test3 eq | throwError "unexpected"
+  logInfo eq
+
+def test5 (e : Expr) : MetaM Expr := do
+  let_expr HAdd.hAdd _ _ _ _ a b ← e
+    | return e
+  mkSub a b
+
+def test6 (e : Expr) : MetaM Expr := do
+  let_expr HAdd.hAdd _ _ _ _ a b := e
+    | return e
+  mkSub a b
+
+/--
+info: 2 - 5
+---
+info: 2 - 5
+---
+info: 2 - 5
+-/
+#guard_msgs in
+run_meta do
+  let e ← mkAdd (toExpr 2) (toExpr 5)
+  let e' ← test5 e
+  logInfo e'
+  let e' ← test6 e
+  logInfo e'
+  let m ← mkFreshExprMVar none
+  let m ← test5 m
+  assert! m.isMVar
+  discard <| isDefEq m e
+  let m' ← test5 m
+  logInfo m'
+  assert! m.isMVar
+  let m' ← test6 m -- does not instantiate mvars
+  assert! m'.isMVar