feat: delaborate match h : d with ...

src/Lean/Meta/Match/Match.lean

@@ -17,11 +17,6 @@ import Lean.Meta.Match.CaseValues
 
 namespace Lean.Meta.Match
 
-structure DiscrInfo where
-  /-- `some h` if the discriminant is annotated with `h:` -/
-  hName? : Option Name := none
-  deriving Inhabited
-
 /-- The number of patterns in each AltLHS must be equal to the number of discriminants. -/
 private def checkNumPatterns (numDiscrs : Nat) (lhss : List AltLHS) : MetaM Unit := do
   if lhss.any fun lhs => lhs.patterns.length != numDiscrs then
@@ -784,6 +779,7 @@ where `v` is a universe parameter or 0 if `B[a_1, ..., a_n]` is a proposition. -
 def mkMatcher (input : MkMatcherInput) : MetaM MatcherResult := do
   let ⟨matcherName, matchType, discrInfos, lhss⟩ := input
   let numDiscrs := discrInfos.size
+  let numEqs := (discrInfos.filter fun info => info.hName?.isSome).size
   checkNumPatterns numDiscrs lhss
   forallBoundedTelescope matchType numDiscrs fun discrs matchTypeBody => do
   /- We generate an matcher that can eliminate using different motives with different universe levels.
@@ -794,6 +790,7 @@ def mkMatcher (input : MkMatcherInput) : MetaM MatcherResult := do
   let uElimGen ← if uElim == levelZero then pure levelZero else mkFreshLevelMVar
   let mkMatcher (type val : Expr) (minors : Array (Expr × Nat)) (s : State) : MetaM MatcherResult := do
     trace[Meta.Match.debug] "matcher value: {val}\ntype: {type}"
+    trace[Meta.Match.debug] "minors num params: {minors.map (·.2)}"
     /- The option `bootstrap.gen_matcher_code` is a helper hack. It is useful, for example,
        for compiling `src/Init/Data/Int`. It is needed because the compiler uses `Int.decLt`
        for generating code for `Int.casesOn` applications, but `Int.casesOn` is used to
@@ -812,12 +809,13 @@ def mkMatcher (input : MkMatcherInput) : MetaM MatcherResult := do
     discard <| isLevelDefEq uElimGen uElim
     let addMatcher :=
       match addMatcher with
-      | some addMatcher =>
+      | some addMatcher => addMatcher <|
         { numParams := matcher.getAppNumArgs
-          numDiscrs,
-          altNumParams := minors.map Prod.snd,
-          uElimPos? }
-        |> addMatcher
+          altNumParams := minors.map fun minor => minor.2 + numEqs
+          discrInfos
+          numDiscrs
+          uElimPos?
+          }
       | none => pure ()
 
     trace[Meta.Match.debug] "matcher: {matcher}"

src/Lean/Meta/Match/MatcherInfo.lean

@@ -8,6 +8,11 @@ import Lean.Meta.Basic
 namespace Lean.Meta
 namespace Match
 
+structure DiscrInfo where
+  /-- `some h` if the discriminant is annotated with `h:` -/
+  hName? : Option Name := none
+  deriving Inhabited
+
 /--
 A "matcher" auxiliary declaration has the following structure:
 - `numParams` parameters
@@ -18,10 +23,14 @@ A "matcher" auxiliary declaration has the following structure:
    `pos` is the position of the universe level parameter that specifies the elimination universe.
    It is `none` if the matcher only eliminates into `Prop`. -/
 structure MatcherInfo where
-  numParams : Nat
-  numDiscrs : Nat
+  numParams    : Nat
+  numDiscrs    : Nat
   altNumParams : Array Nat
-  uElimPos? : Option Nat
+  uElimPos?    : Option Nat
+  /--
+    `discrInfos[i] = { hName? := some h }` if the i-th discriminant was annotated with `h :`.
+  -/
+  discrInfos   : Array DiscrInfo
 
 def MatcherInfo.numAlts (info : MatcherInfo) : Nat :=
   info.altNumParams.size

src/Lean/Parser/Term.lean

@@ -144,7 +144,7 @@ def matchAltExpr := matchAlt
 def matchAlts (rhsParser : Parser := termParser) : Parser :=
   leading_parser withPosition $ many1Indent (ppLine >> matchAlt rhsParser)
 
-def matchDiscr := leading_parser optional (atomic (ident >> ":")) >> termParser
+def matchDiscr := leading_parser optional (atomic (ident >> " : ")) >> termParser
 
 def trueVal  := leading_parser nonReservedSymbol "true"
 def falseVal := leading_parser nonReservedSymbol "false"

src/Lean/PrettyPrinter/Delaborator/Builtins.lean

@@ -383,27 +383,34 @@ def delabAppMatch : Delab := whenPPOption getPPNotation <| whenPPOption getPPMat
       return { matcherTy := (← getConstInfo c).instantiateTypeLevelParams us, info := info : AppMatchState })
     (fun st => do
       if st.params.size < st.info.numParams then
-        pure { st with params := st.params.push (← getExpr) }
+        return { st with params := st.params.push (← getExpr) }
       else if st.motive.isNone then
-         -- store motive argument separately
-         let lamMotive ← getExpr
-         let piMotive ← lambdaTelescope lamMotive fun xs body => mkForallFVars xs body
-         -- TODO: pp.analyze has not analyzed `piMotive`, only `lamMotive`
-         -- Thus the binder types won't have any annotations
-         let piStx ← withTheReader SubExpr (fun cfg => { cfg with expr := piMotive }) delab
-         let named ← getPPOption getPPAnalysisNamedArg
-         pure { st with motive := (piStx, lamMotive), motiveNamed := named }
+        -- store motive argument separately
+        let lamMotive ← getExpr
+        let piMotive ← lambdaTelescope lamMotive fun xs body => mkForallFVars xs body
+        -- TODO: pp.analyze has not analyzed `piMotive`, only `lamMotive`
+        -- Thus the binder types won't have any annotations
+        let piStx ← withTheReader SubExpr (fun cfg => { cfg with expr := piMotive }) delab
+        let named ← getPPOption getPPAnalysisNamedArg
+        return { st with motive := (piStx, lamMotive), motiveNamed := named }
       else if st.discrs.size < st.info.numDiscrs then
-        pure { st with discrs := st.discrs.push (← delab) }
+        let idx := st.discrs.size
+        let discr ← delab
+        if let some hName := st.info.discrInfos[idx].hName? then
+          -- TODO: we should check whether the corresponding binder name, matches `hName`.
+          -- If it does not we should pretty print this `match` as a regular application.
+          return { st with discrs := st.discrs.push (← `(matchDiscr| $(mkIdent hName):ident : $discr:term)) }
+        else
+          return { st with discrs := st.discrs.push (← `(matchDiscr| $discr:term)) }
       else if st.rhss.size < st.info.altNumParams.size then
         /- We save the variables names here to be able to implement safe_shadowing.
            The pattern delaboration must use the names saved here. -/
         let (varNames, rhs) ← skippingBinders st.info.altNumParams[st.rhss.size] fun varNames => do
           let rhs ← delab
           return (varNames, rhs)
-        pure { st with rhss := st.rhss.push rhs, varNames := st.varNames.push varNames }
+        return { st with rhss := st.rhss.push rhs, varNames := st.varNames.push varNames }
       else
-        pure { st with moreArgs := st.moreArgs.push (← delab) })
+        return { st with moreArgs := st.moreArgs.push (← delab) })
 
   if st.discrs.size < st.info.numDiscrs || st.rhss.size < st.info.altNumParams.size then
     -- underapplied
@@ -421,9 +428,9 @@ def delabAppMatch : Delab := whenPPOption getPPNotation <| whenPPOption getPPMat
       let opts ← getOptions
       -- TODO: disable the match if other implicits are needed?
       if ← pure st.motiveNamed <||> shouldShowMotive lamMotive opts then
-        `(match (motive := $piStx) $[$st.discrs:term],* with $[| $pats,* => $st.rhss]*)
+        `(match (motive := $piStx) $[$st.discrs:matchDiscr],* with $[| $pats,* => $st.rhss]*)
       else
-        `(match $[$st.discrs:term],* with $[| $pats,* => $st.rhss]*)
+        `(match $[$st.discrs:matchDiscr],* with $[| $pats,* => $st.rhss]*)
     return Syntax.mkApp stx st.moreArgs
 
 /--