chore: update stage0

src/Lean/Elab.lean

@@ -49,3 +49,4 @@ import Lean.Elab.InheritDoc
 import Lean.Elab.ParseImportsFast
 import Lean.Elab.GuardMsgs
 import Lean.Elab.CheckTactic
+import Lean.Elab.MatchExpr

src/Lean/Elab/Do.lean

@@ -131,12 +131,31 @@ abbrev Var := Syntax  -- TODO: should be `Ident`
 
 /-- A `doMatch` alternative. `vars` is the array of variables declared by `patterns`. -/
 structure Alt (σ : Type) where
-  ref : Syntax
-  vars : Array Var
+  ref      : Syntax
+  vars     : Array Var
   patterns : Syntax
-  rhs : σ
+  rhs      : σ
   deriving Inhabited
 
+/-- A `doMatchExpr` alternative. -/
+structure AltExpr (σ : Type) where
+  ref     : Syntax
+  var?    : Option Var
+  funName : Syntax
+  pvars   : Array Syntax
+  rhs     : σ
+  deriving Inhabited
+
+def AltExpr.vars (alt : AltExpr σ) : Array Var := Id.run do
+  let mut vars := #[]
+  if let some var := alt.var? then
+    vars := vars.push var
+  for pvar in alt.pvars do
+    match pvar with
+    | `(_) => pure ()
+    | _ => vars := vars.push pvar
+  return vars
+
 /--
   Auxiliary datastructure for representing a `do` code block, and compiling "reassignments" (e.g., `x := x + 1`).
   We convert `Code` into a `Syntax` term representing the:
@@ -198,6 +217,7 @@ inductive Code where
   /-- Recall that an if-then-else may declare a variable using `optIdent` for the branches `thenBranch` and `elseBranch`. We store the variable name at `var?`. -/
   | ite          (ref : Syntax) (h? : Option Var) (optIdent : Syntax) (cond : Syntax) (thenBranch : Code) (elseBranch : Code)
   | match        (ref : Syntax) (gen : Syntax) (discrs : Syntax) (optMotive : Syntax) (alts : Array (Alt Code))
+  | matchExpr    (ref : Syntax) (meta : Bool) (discr : Syntax) (alts : Array (AltExpr Code)) (elseBranch : Code)
   | jmp          (ref : Syntax) (jpName : Name) (args : Array Syntax)
   deriving Inhabited
 
@@ -212,6 +232,7 @@ def Code.getRef? : Code → Option Syntax
   | .return ref _        => ref
   | .ite ref ..          => ref
   | .match ref ..        => ref
+  | .matchExpr ref ..    => ref
   | .jmp ref ..          => ref
 
 abbrev VarSet := RBMap Name Syntax Name.cmp
@@ -243,19 +264,28 @@ partial def CodeBlocl.toMessageData (codeBlock : CodeBlock) : MessageData :=
     | .match _ _ ds _ alts   =>
       m!"match {ds} with"
       ++ alts.foldl (init := m!"") fun acc alt => acc ++ m!"\n| {alt.patterns} => {loop alt.rhs}"
+    | .matchExpr _ meta d alts elseCode =>
+      let r := m!"match_expr {if meta then "" else "(meta := false)"} {d} with"
+      let r := r ++ alts.foldl (init := m!"") fun acc alt =>
+            let acc := acc ++ m!"\n| {if let some var := alt.var? then m!"{var}@" else ""}"
+            let acc := acc ++ m!"{alt.funName}"
+            let acc := acc ++ alt.pvars.foldl (init := m!"") fun acc pvar => acc ++ m!" {pvar}"
+            acc ++ m!" => {loop alt.rhs}"
+      r ++ m!"| _ => {loop elseCode}"
   loop codeBlock.code
 
 /-- Return true if the give code contains an exit point that satisfies `p` -/
 partial def hasExitPointPred (c : Code) (p : Code → Bool) : Bool :=
   let rec loop : Code → Bool
-    | .decl _ _ k         => loop k
-    | .reassign _ _ k     => loop k
-    | .joinpoint _ _ b k  => loop b || loop k
-    | .seq _ k            => loop k
-    | .ite _ _ _ _ t e    => loop t || loop e
-    | .match _ _ _ _ alts => alts.any (loop ·.rhs)
-    | .jmp ..             => false
-    | c                   => p c
+    | .decl _ _ k             => loop k
+    | .reassign _ _ k         => loop k
+    | .joinpoint _ _ b k      => loop b || loop k
+    | .seq _ k                => loop k
+    | .ite _ _ _ _ t e        => loop t || loop e
+    | .match _ _ _ _ alts     => alts.any (loop ·.rhs)
+    | .matchExpr _ _ _ alts e => alts.any (loop ·.rhs) || loop e
+    | .jmp ..                 => false
+    | c                       => p c
   loop c
 
 def hasExitPoint (c : Code) : Bool :=
@@ -300,13 +330,18 @@ partial def convertTerminalActionIntoJmp (code : Code) (jp : Name) (xs : Array V
     | .joinpoint n ps b k    => return .joinpoint n ps (← loop b) (← loop k)
     | .seq e k               => return .seq e (← loop k)
     | .ite ref x? h c t e    => return .ite ref x? h c (← loop t) (← loop e)
-    | .match ref g ds t alts => return .match ref g ds t (← alts.mapM fun alt => do pure { alt with rhs := (← loop alt.rhs) })
     | .action e              => mkAuxDeclFor e fun y =>
       let ref := e
       -- We jump to `jp` with xs **and** y
       let jmpArgs := xs.push y
       return Code.jmp ref jp jmpArgs
-    | c                            => return c
+    | .match ref g ds t alts =>
+      return .match ref g ds t (← alts.mapM fun alt => do pure { alt with rhs := (← loop alt.rhs) })
+    | .matchExpr ref meta d alts e => do
+      let alts ← alts.mapM fun alt => do pure { alt with rhs := (← loop alt.rhs) }
+      let e ← loop e
+      return .matchExpr ref meta d alts e
+    | c => return c
   loop code
 
 structure JPDecl where
@@ -372,14 +407,13 @@ def mkJmp (ref : Syntax) (rs : VarSet) (val : Syntax) (mkJPBody : Syntax → Mac
   return Code.jmp ref jp args
 
 /-- `pullExitPointsAux rs c` auxiliary method for `pullExitPoints`, `rs` is the set of update variable in the current path.  -/
-partial def pullExitPointsAux (rs : VarSet) (c : Code) : StateRefT (Array JPDecl) TermElabM Code :=
+partial def pullExitPointsAux (rs : VarSet) (c : Code) : StateRefT (Array JPDecl) TermElabM Code := do
   match c with
   | .decl xs stx k         => return .decl xs stx (← pullExitPointsAux (eraseVars rs xs) k)
   | .reassign xs stx k     => return .reassign xs stx (← pullExitPointsAux (insertVars rs xs) k)
   | .joinpoint j ps b k    => return .joinpoint j ps (← pullExitPointsAux rs b) (← pullExitPointsAux rs k)
   | .seq e k               => return .seq e (← pullExitPointsAux rs k)
   | .ite ref x? o c t e    => return .ite ref x? o c (← pullExitPointsAux (eraseOptVar rs x?) t) (← pullExitPointsAux (eraseOptVar rs x?) e)
-  | .match ref g ds t alts => return .match ref g ds t (← alts.mapM fun alt => do pure { alt with rhs := (← pullExitPointsAux (eraseVars rs alt.vars) alt.rhs) })
   | .jmp ..                => return  c
   | .break ref             => mkSimpleJmp ref rs (.break ref)
   | .continue ref          => mkSimpleJmp ref rs (.continue ref)
@@ -389,6 +423,13 @@ partial def pullExitPointsAux (rs : VarSet) (c : Code) : StateRefT (Array JPDecl
     mkAuxDeclFor e fun y =>
       let ref := e
       mkJmp ref rs y (fun yFresh => return .action (← ``(Pure.pure $yFresh)))
+  | .match ref g ds t alts =>
+    let alts ← alts.mapM fun alt => do pure { alt with rhs := (← pullExitPointsAux (eraseVars rs alt.vars) alt.rhs) }
+    return .match ref g ds t alts
+  | .matchExpr ref meta d alts e =>
+    let alts ← alts.mapM fun alt => do pure { alt with rhs := (← pullExitPointsAux (eraseVars rs alt.vars) alt.rhs) }
+    let e ← pullExitPointsAux rs e
+    return .matchExpr ref meta d alts e
 
 /--
 Auxiliary operation for adding new variables to the collection of updated variables in a CodeBlock.
@@ -457,6 +498,14 @@ partial def extendUpdatedVarsAux (c : Code) (ws : VarSet) : TermElabM Code :=
         pullExitPoints c
       else
         return .match ref g ds t (← alts.mapM fun alt => do pure { alt with rhs := (← update alt.rhs) })
+    | .matchExpr ref meta d alts e =>
+      if alts.any fun alt => alt.vars.any fun x => ws.contains x.getId then
+        -- If a pattern variable is shadowing a variable in ws, we `pullExitPoints`
+        pullExitPoints c
+      else
+        let alts ← alts.mapM fun alt => do pure { alt with rhs := (← update alt.rhs) }
+        let e ← update e
+        return .matchExpr ref meta d alts e
     | .ite ref none o c t e => return .ite ref none o c (← update t) (← update e)
     | .ite ref (some h) o cond t e =>
       if ws.contains h.getId then
@@ -570,6 +619,16 @@ def mkMatch (ref : Syntax) (genParam : Syntax) (discrs : Syntax) (optMotive : Sy
     return { ref := alt.ref, vars := alt.vars, patterns := alt.patterns, rhs := rhs.code : Alt Code }
   return { code := .match ref genParam discrs optMotive alts, uvars := ws }
 
+def mkMatchExpr (ref : Syntax) (meta : Bool) (discr : Syntax) (alts : Array (AltExpr CodeBlock)) (elseBranch : CodeBlock) : TermElabM CodeBlock := do
+  -- nary version of homogenize
+  let ws := alts.foldl (union · ·.rhs.uvars) {}
+  let ws := union ws elseBranch.uvars
+  let alts ← alts.mapM fun alt => do
+    let rhs ← extendUpdatedVars alt.rhs ws
+    return { alt with rhs := rhs.code : AltExpr Code }
+  let elseBranch ← extendUpdatedVars elseBranch ws
+  return { code := .matchExpr ref meta discr alts elseBranch.code, uvars := ws }
+
 /-- Return a code block that executes `terminal` and then `k` with the value produced by `terminal`.
    This method assumes `terminal` is a terminal -/
 def concat (terminal : CodeBlock) (kRef : Syntax) (y? : Option Var) (k : CodeBlock) : TermElabM CodeBlock := do
@@ -1077,10 +1136,25 @@ where
       let mut termAlts := #[]
       for alt in alts do
         let rhs ← toTerm alt.rhs
-        let termAlt := mkNode `Lean.Parser.Term.matchAlt #[mkAtomFrom alt.ref "|", mkNullNode #[alt.patterns], mkAtomFrom alt.ref "=>", rhs]
+        let termAlt := mkNode ``Parser.Term.matchAlt #[mkAtomFrom alt.ref "|", mkNullNode #[alt.patterns], mkAtomFrom alt.ref "=>", rhs]
         termAlts := termAlts.push termAlt
-      let termMatchAlts := mkNode `Lean.Parser.Term.matchAlts #[mkNullNode termAlts]
-      return mkNode `Lean.Parser.Term.«match» #[mkAtomFrom ref "match", genParam, optMotive, discrs, mkAtomFrom ref "with", termMatchAlts]
+      let termMatchAlts := mkNode ``Parser.Term.matchAlts #[mkNullNode termAlts]
+      return mkNode ``Parser.Term.«match» #[mkAtomFrom ref "match", genParam, optMotive, discrs, mkAtomFrom ref "with", termMatchAlts]
+    | .matchExpr ref meta d alts elseBranch => withFreshMacroScope do
+      let d' ← `(discr)
+      let mut termAlts := #[]
+      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]
+        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]
+      let body := mkNode ``Parser.Term.matchExpr #[mkAtomFrom ref "match_expr", d', mkAtomFrom ref "with", termMatchExprAlts]
+      if meta then
+        `(Bind.bind (instantiateMVarsIfMVarApp $d) fun discr => $body)
+      else
+        `(let discr := $d; $body)
 
 def run (code : Code) (m : Syntax) (returnType : Syntax) (uvars : Array Var := #[]) (kind := Kind.regular) : MacroM Syntax :=
   toTerm code { m, returnType, kind, uvars }
@@ -1533,6 +1607,23 @@ mutual
     let matchCode ← mkMatch ref genParam discrs optMotive alts
     concatWith matchCode doElems
 
+  /-- Generate `CodeBlock` for `doMatchExpr; doElems` -/
+  partial def doMatchExprToCode (doMatchExpr : Syntax) (doElems: List Syntax) : M CodeBlock := do
+    let ref       := doMatchExpr
+    let meta      := doMatchExpr[1].isNone
+    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 rhs ← doSeqToCode (getDoSeqElems rhs)
+      pure { ref, var?, funName, pvars, rhs }
+    let elseBranch ← doSeqToCode (getDoSeqElems doMatchExpr[4][1][3])
+    let matchCode ← mkMatchExpr ref meta discr alts elseBranch
+    concatWith matchCode doElems
+
   /--
     Generate `CodeBlock` for `doTry; doElems`
     ```
@@ -1640,6 +1731,8 @@ mutual
             doForToCode doElem doElems
           else if k == ``Parser.Term.doMatch then
             doMatchToCode doElem doElems
+          else if k == ``Parser.Term.doMatchExpr then
+            doMatchExprToCode doElem doElems
           else if k == ``Parser.Term.doTry then
             doTryToCode doElem doElems
           else if k == ``Parser.Term.doBreak then

src/Lean/Elab/MatchExpr.lean

@@ -0,0 +1,204 @@
+/-
+Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+prelude
+import Lean.Elab.Term
+
+namespace Lean.Elab.Term
+namespace MatchExpr
+/--
+`match_expr` alternative. Recall that it has the following structure.
+```
+| (ident "@")? ident bindeIdent* => rhs
+```
+
+Example:
+```
+| c@Eq _ a b => f c a b
+```
+-/
+structure Alt where
+  /--
+  `some c` if there is a variable binding to the function symbol being matched.
+  `c` is the variable name.
+  -/
+  var?    : Option Ident
+  /-- Function being matched. -/
+  funName : Ident
+  /-- Pattern variables. The list uses `none` for representing `_`, and `some a` for pattern variable `a`. -/
+  pvars   : List (Option Ident)
+  /-- right-hand-side for the alternative. -/
+  rhs     : Syntax
+  /-- Store the auxliary continuation function for each right-hand-side. -/
+  k       : Ident := ⟨.missing⟩
+  /-- Actual value to be passed as an argument. -/
+  actuals : List Term := []
+
+/--
+`match_expr` else-alternative. Recall that it has the following structure.
+```
+| _ => rhs
+```
+-/
+structure ElseAlt where
+  rhs : Syntax
+
+open Parser Term
+
+/--
+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 }
+
+/--
+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 }
+
+/--
+Returns the function names of alternatives that do not have any pattern variable left.
+-/
+def getFunNamesToMatch (alts : List Alt) : List Ident := Id.run do
+  let mut funNames := #[]
+  for alt in alts do
+    if alt.pvars.isEmpty then
+      if Option.isNone <| funNames.find? fun funName => funName.getId == alt.funName.getId then
+        funNames := funNames.push alt.funName
+  return funNames.toList
+
+/--
+Returns `true` if there is at least one alternative whose next pattern variable is not a `_`.
+-/
+def shouldSaveActual (alts : List Alt) : Bool :=
+  alts.any fun alt => alt.pvars matches some _ :: _
+
+/--
+Returns the first alternative whose function name is `funName` **and**
+does not have pattern variables left to match.
+-/
+def getAltFor? (alts : List Alt) (funName : Ident) : Option Alt :=
+  alts.find? fun alt => alt.funName.getId == funName.getId && alt.pvars.isEmpty
+
+/--
+Removes alternatives that do not have any pattern variable left to be matched.
+For the ones that still have pattern variables, remove the first one, and
+save `actual` if the removed pattern variable is not a `_`.
+-/
+def next (alts : List Alt) (actual : Term) : List Alt :=
+  alts.filterMap fun alt =>
+    if let some _ :: pvars := alt.pvars then
+      some { alt with pvars, actuals := actual :: alt.actuals }
+    else if let none :: pvars := alt.pvars then
+      some { alt with pvars }
+    else
+      none
+
+/--
+Creates a fresh identifier for representing the continuation function used to
+execute the RHS of the given alternative, and stores it in the field `k`.
+-/
+def initK (alt : Alt) : MacroM Alt := withFreshMacroScope do
+  let k : Ident ← `(k)
+  return { alt with k }
+
+/--
+Generates parameters for the continuation function used to execute
+the RHS of the given alternative.
+-/
+def getParams (alt : Alt) : MacroM (Array Term) := do
+  let mut params := #[]
+  if let some var := alt.var? then
+    params := params.push (← `(($var : Expr)))
+  params := params ++ (← alt.pvars.toArray.reverse.filterMapM fun
+    | none => return none
+    | some arg => return some (← `(($arg : Expr))))
+  if params.isEmpty then
+    return #[(← `(_))]
+  return params
+
+/--
+Generates the actual arguments for invoking the auxiliary continuation function
+associated with the given alternative. The arguments are the actuals stored in `alt`.
+`discr` is also an argument if `alt.var?` is not none.
+-/
+def getActuals (discr : Term) (alt : Alt) : MacroM (Array Term) := do
+  let mut actuals := #[]
+  if alt.var?.isSome then
+    actuals := actuals.push discr
+  actuals := actuals ++ alt.actuals.toArray
+  if actuals.isEmpty then
+    return #[← `(())]
+  return actuals
+
+def toDoubleQuotedName (ident : Ident) : Term :=
+  ⟨mkNode ``Parser.Term.doubleQuotedName #[mkAtom "`", mkAtom "`", ident]⟩
+
+/--
+Generates an `if-then-else` tree for implementing a `match_expr` with discriminant `discr`,
+alternatives `alts`, and else-alternative `elseAlt`.
+-/
+partial def generate (discr : Term) (alts : List Alt) (elseAlt : ElseAlt) : MacroM Syntax := do
+  let alts ← alts.mapM initK
+  let discr' ← `(discr)
+  let kElse ← `(ke)
+  let rec loop (discr : Term) (alts : List Alt) : MacroM Term := withFreshMacroScope do
+    let funNamesToMatch := getFunNamesToMatch alts
+    let saveActual := shouldSaveActual alts
+    let actual ← if saveActual then `(a) else `(_)
+    let altsNext := next alts actual
+    let body ← if altsNext.isEmpty then
+      `($kElse ())
+    else
+      let discr' ← `(discr)
+      let body ← loop discr' altsNext
+      if saveActual then
+        `(if h : ($discr).isApp then let a := Expr.appArg $discr h; let discr := Expr.appFnCleanup $discr h; $body else $kElse ())
+      else
+        `(if h : ($discr).isApp then let discr := Expr.appFnCleanup $discr h; $body else $kElse ())
+    let mut result := body
+    for funName in funNamesToMatch do
+      if let some alt := getAltFor? alts funName then
+        let actuals ← getActuals discr alt
+        result ← `(if ($discr).isConstOf $(toDoubleQuotedName funName) then $alt.k $actuals* else $result)
+    return result
+  let body ← loop discr' alts
+  let mut result ← `(let_delayed ke := fun (_ : Unit) => $(⟨elseAlt.rhs⟩):term; let discr := Expr.cleanupAnnotations $discr:term; $body:term)
+  for alt in alts do
+    let params ← getParams alt
+    result ← `(let_delayed $alt.k:ident := fun $params:term* => $(⟨alt.rhs⟩):term; $result:term)
+  return result
+
+def main (discr : Term) (alts : Array Syntax) (elseAlt : Syntax) : MacroM Syntax := do
+  let alts ← alts.toList.mapM fun alt =>
+    if let some alt := toAlt? alt then
+      pure alt
+    else
+      Macro.throwErrorAt alt "unexpected `match_expr` alternative"
+  let some elseAlt := toElseAlt? elseAlt
+    | Macro.throwErrorAt elseAlt "unexpected `match_expr` else-alternative"
+  generate discr alts elseAlt
+
+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)
+  | _ => Macro.throwUnsupported
+
+end Lean.Elab.Term

src/Lean/Expr.lean

@@ -904,6 +904,14 @@ def appArg!' : Expr → Expr
   | app _ a   => a
   | _         => panic! "application expected"
 
+def appArg (e : Expr) (h : e.isApp) : Expr :=
+  match e, h with
+  | .app _ a, _ => a
+
+def appFn (e : Expr) (h : e.isApp) : Expr :=
+  match e, h with
+  | .app f _, _ => f
+
 def sortLevel! : Expr → Level
   | sort u => u
   | _      => panic! "sort expected"
@@ -1616,6 +1624,14 @@ partial def cleanupAnnotations (e : Expr) : Expr :=
   let e' := e.consumeMData.consumeTypeAnnotations
   if e' == e then e else cleanupAnnotations e'
 
+/--
+Similar to `appFn`, but also applies `cleanupAnnotations` to resulting function.
+This function is used compile the `match_expr` term.
+-/
+def appFnCleanup (e : Expr) (h : e.isApp) : Expr :=
+  match e, h with
+  | .app f _, _ => f.cleanupAnnotations
+
 def isFalse (e : Expr) : Bool :=
   e.cleanupAnnotations.isConstOf ``False
 

src/Lean/Meta/Basic.lean

@@ -1737,6 +1737,15 @@ def isDefEqNoConstantApprox (t s : Expr) : MetaM Bool :=
 def etaExpand (e : Expr) : MetaM Expr :=
   withDefault do forallTelescopeReducing (← inferType e) fun xs _ => mkLambdaFVars xs (mkAppN e xs)
 
+/--
+If `e` is of the form `?m ...` instantiate metavars
+-/
+def instantiateMVarsIfMVarApp (e : Expr) : MetaM Expr := do
+  if e.getAppFn.isMVar then
+    instantiateMVars e
+  else
+    return e
+
 end Meta
 
 builtin_initialize

src/Lean/Parser/Do.lean

@@ -50,7 +50,7 @@ def notFollowedByRedefinedTermToken :=
   -- but we include them in the following list to fix the ambiguity where
   -- an "open" command follows the `do`-block.
   -- If we don't add `do`, then users would have to indent `do` blocks or use `{ ... }`.
-  notFollowedBy ("set_option" <|> "open" <|> "if" <|> "match" <|> "let" <|> "have" <|>
+  notFollowedBy ("set_option" <|> "open" <|> "if" <|> "match" <|> "match_expr" <|> "let" <|> "let_expr" <|> "have" <|>
       "do" <|> "dbg_trace" <|> "assert!" <|> "for" <|> "unless" <|> "return" <|> symbol "try")
     "token at 'do' element"
 
@@ -150,6 +150,10 @@ def doMatchAlts := ppDedent <| matchAlts (rhsParser := doSeq)
   "match " >> optional Term.generalizingParam >> optional Term.motive >>
   sepBy1 matchDiscr ", " >> " with" >> doMatchAlts
 
+def doMatchExprAlts := ppDedent <| matchExprAlts (rhsParser := doSeq)
+@[builtin_doElem_parser] def doMatchExpr := leading_parser:leadPrec
+  "match_expr " >> optional ("(" >> nonReservedSymbol "meta" >>  " := " >> nonReservedSymbol "false" >> ") ") >> termParser >> " with" >> doMatchExprAlts
+
 def doCatch      := leading_parser
   ppDedent ppLine >> atomic ("catch " >> binderIdent) >> optional (" : " >> termParser) >> darrow >> doSeq
 def doCatchMatch := leading_parser

src/Lean/Parser/Term.lean

@@ -802,7 +802,6 @@ interpolated string literal) to stderr. It should only be used for debugging.
 @[builtin_term_parser] def assert := leading_parser:leadPrec
   withPosition ("assert! " >> termParser) >> optSemicolon termParser
 
-
 def macroArg       := termParser maxPrec
 def macroDollarArg := leading_parser "$" >> termParser 10
 def macroLastArg   := macroDollarArg <|> macroArg
@@ -823,6 +822,19 @@ Implementation of the `show_term` term elaborator.
 @[builtin_term_parser] def showTermElabImpl :=
   leading_parser:leadPrec "show_term_elab " >> termParser
 
+/-!
+`match_expr` support.
+-/
+
+def matchExprAlt (rhsParser : Parser) := leading_parser "| " >> ppIndent (optional (atomic (ident >> "@")) >> ident >> many binderIdent >> " => " >> rhsParser)
+def matchExprElseAlt (rhsParser : Parser) := leading_parser "| " >> ppIndent (hole >> " => " >> rhsParser)
+def matchExprAlts (rhsParser : Parser) :=
+  leading_parser withPosition $
+    many (ppLine >> checkColGe "irrelevant" >> notFollowedBy (symbol "| " >> " _ ") "irrelevant" >> matchExprAlt rhsParser)
+    >> (ppLine >> checkColGe "irrelevant" >> matchExprElseAlt rhsParser)
+@[builtin_term_parser] def matchExpr := leading_parser:leadPrec
+  "match_expr " >> termParser >> " with" >> ppDedent (matchExprAlts termParser)
+
 end Term
 
 @[builtin_term_parser default+1] def Tactic.quot : Parser := leading_parser
@@ -841,6 +853,7 @@ builtin_initialize
   register_parser_alias matchDiscr
   register_parser_alias bracketedBinder
   register_parser_alias attrKind
+  register_parser_alias optSemicolon
 
 end Parser
 end Lean

tests/lean/run/match_expr.lean

@@ -0,0 +1,56 @@
+import Lean
+open Lean Meta
+
+def test1 (e : Expr) : Option Expr :=
+  match_expr e with
+  | c@Eq α a b => some (mkApp3 c α b a)
+  | Eq.refl _ a => some a
+  | _ => none
+
+/--
+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 := test1 eq | throwError "unexpected"
+  logInfo eq
+  let rfl ← mkEqRefl (toExpr 3)
+  let some n := test1 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 := test1 eq | throwError "unexpected"
+  logInfo eq
+
+def test2 (e : Expr) : MetaM Expr := do
+  match_expr e with
+  | HAdd.hAdd _ _ _ _ a b => mkSub a b
+  | HMul.hMul _ _ _ _ a b => mkAdd b a
+  | _ => return e
+
+/--
+info: 2 - 5
+---
+info: 5 + 2
+---
+info: 5 - 2
+-/
+#guard_msgs in
+run_meta do
+  let e ← mkAdd (toExpr 2) (toExpr 5)
+  let e ← test2 e
+  logInfo e
+  let e ← mkMul (toExpr 2) (toExpr 5)
+  let e ← test2 e
+  logInfo e
+  let m ← mkFreshExprMVar none
+  let m ← test2 m
+  assert! m.isMVar
+  discard <| isDefEq m e
+  let m ← test2 m
+  logInfo m