refactor: remove _aux_discr

src/Lean/Elab/AuxDiscr.lean

@@ -1,33 +0,0 @@
-/-
-Copyright (c) 2022 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Leonardo de Moura
--/
-
-namespace Lean
-
-/--
-  Create an auxiliary identifier for storing non-atomic discriminants.
-  This kind of free variable is cleared before elaborating a `match` alternative rhs.
--/
-def mkAuxDiscr [Monad m] [MonadQuotation m] : m Ident :=
-  `(_discr)
-
-/--
-  Create an auxiliary identifier for expanding notation such as `fun (a, b) => ...`.
-  This kind of free variable is cleared before elaborating a `match` alternative rhs.
--/
-def mkAuxFunDiscr [Monad m] [MonadQuotation m] : m Ident :=
-  `(_fun_discr)
-
-/-- Return true iff `n` is an auxiliary variable created by `expandNonAtomicDiscrs?` -/
-def isAuxDiscrName (n : Name) : Bool :=
-  n.hasMacroScopes && n.eraseMacroScopes == `_discr
-
-/--
-  Return true iff `n` is an auxiliary variable created by notation such as `fun (a, b) => ...`.
-  They are cleared before eliminating the `match` alternatives RHS -/
-def isAuxFunDiscrName (n : Name) : Bool :=
-  n.hasMacroScopes && n.eraseMacroScopes == `_fun_discr
-
-end Lean

src/Lean/Elab/Binders.lean

@@ -6,7 +6,6 @@ Authors: Leonardo de Moura
 import Lean.Elab.Quotation.Precheck
 import Lean.Elab.Term
 import Lean.Elab.BindersUtil
-import Lean.Elab.AuxDiscr
 
 namespace Lean.Elab.Term
 open Meta
@@ -459,16 +458,17 @@ def expandWhereDeclsOpt (whereDeclsOpt : Syntax) (body : Syntax) : MacroM Syntax
 /--
  Helper function for `expandMatchAltsIntoMatch`.
 -/
-private def expandMatchAltsIntoMatchAux (matchAlts : Syntax) (isTactic : Bool) (useExplicit : Bool) : Nat → Array Syntax → MacroM Syntax
-  | 0,   discrs => do
+private def expandMatchAltsIntoMatchAux (matchAlts : Syntax) (isTactic : Bool) (useExplicit : Bool) : Nat → Array Syntax → Array Ident → MacroM Syntax
+  | 0,   discrs, xs => do
     if isTactic then
       `(tactic|match $[$discrs:term],* with $matchAlts:matchAlts)
     else
-      `(match $[$discrs:term],* with $matchAlts:matchAlts)
-  | n+1, discrs => withFreshMacroScope do
-    let x ← mkAuxFunDiscr -- Recall that identifiers created with `mkAuxFunDiscr` are cleared by the `match` elaborator
-    let d ← `(@$x:ident) -- See comment below
-    let body ← expandMatchAltsIntoMatchAux matchAlts isTactic useExplicit n (discrs.push d)
+      let stx ← `(match $[$discrs:term],* with $matchAlts:matchAlts)
+      clearInMatch stx xs
+  | n+1, discrs, xs => withFreshMacroScope do
+    let x ← `(x) -- If this were implementation-detail, the `contradiction` tactic used by match would not find it.
+    let d ← `(@$x:ident)
+    let body ← expandMatchAltsIntoMatchAux matchAlts isTactic useExplicit n (discrs.push d) (xs.push x)
     if isTactic then
       `(tactic| intro $x:term; $body:tactic)
     else if useExplicit then
@@ -529,10 +529,10 @@ private def expandMatchAltsIntoMatchAux (matchAlts : Syntax) (isTactic : Bool) (
   The two definitions should be elaborated without errors and be equivalent.
  -/
 def expandMatchAltsIntoMatch (ref : Syntax) (matchAlts : Syntax) (useExplicit := true) : MacroM Syntax :=
-  withRef ref <| expandMatchAltsIntoMatchAux matchAlts (isTactic := false) (useExplicit := useExplicit) (getMatchAltsNumPatterns matchAlts) #[]
+  withRef ref <| expandMatchAltsIntoMatchAux matchAlts (isTactic := false) (useExplicit := useExplicit) (getMatchAltsNumPatterns matchAlts) #[] #[]
 
 def expandMatchAltsIntoMatchTactic (ref : Syntax) (matchAlts : Syntax) : MacroM Syntax :=
-  withRef ref <| expandMatchAltsIntoMatchAux matchAlts (isTactic := true) (useExplicit := false) (getMatchAltsNumPatterns matchAlts) #[]
+  withRef ref <| expandMatchAltsIntoMatchAux matchAlts (isTactic := true) (useExplicit := false) (getMatchAltsNumPatterns matchAlts) #[] #[]
 
 /--
   Similar to `expandMatchAltsIntoMatch`, but supports an optional `where` clause.
@@ -568,16 +568,15 @@ def expandMatchAltsWhereDecls (matchAltsWhereDecls : Syntax) : MacroM Syntax :=
   let rec loop (i : Nat) (discrs : Array Syntax) : MacroM Syntax :=
     match i with
     | 0   => do
-      let matchStx ← `(match $[$discrs:term],* with $matchAlts:matchAlts)
+      let matchStx ← `(match $[@$discrs:term],* with $matchAlts:matchAlts)
+      let matchStx ← clearInMatch matchStx discrs
       if whereDeclsOpt.isNone then
         return matchStx
       else
         expandWhereDeclsOpt whereDeclsOpt matchStx
     | n+1 => withFreshMacroScope do
-      -- See comment at `expandMatchAltsIntoMatch`,
-      let d ← mkAuxFunDiscr
-      let body ← loop n (discrs.push (← `(@$d:ident)))
-      `(@fun $d:ident => $body)
+      let body ← loop n (discrs.push (← `(x)))
+      `(@fun x => $body)
   loop (getMatchAltsNumPatterns matchAlts) #[]
 
 @[builtinMacro Parser.Term.fun] partial def expandFun : Macro

src/Lean/Elab/BindersUtil.lean

@@ -53,4 +53,21 @@ def expandMatchAlts? (stx : Syntax) : MacroM (Option Syntax) := do
       return none
   | _ => return none
 
+open TSyntax.Compat in
+def clearInMatchAlt (stx : TSyntax ``matchAlt) (vars : Array Ident) : TSyntax ``matchAlt :=
+  stx.1.modifyArg 3 fun rhs => Id.run do
+    let mut rhs := rhs
+    for v in vars do
+      -- rhs ← `(clear% $v; $rhs)
+      rhs := mkNode `Lean.Parser.Term.clear #[mkAtom "clear%", v, mkNullNode, rhs]
+    return rhs
+
+def clearInMatch (stx : Syntax) (vars : Array Ident) : MacroM Syntax := do
+  if vars.isEmpty then return stx
+  match stx with
+  | `(match $[$gen]? $[$motive]? $discrs,* with $alts:matchAlt*) =>
+    let alts := alts.map (clearInMatchAlt · vars)
+    `(match $[$gen]? $[$motive]? $discrs,* with $alts:matchAlt*)
+  | _ => return stx
+
 end Lean.Elab.Term

src/Lean/Elab/Match.lean

@@ -6,7 +6,6 @@ Authors: Leonardo de Moura
 import Lean.Meta.Match.Match
 import Lean.Meta.GeneralizeVars
 import Lean.Meta.ForEachExpr
-import Lean.Elab.AuxDiscr
 import Lean.Elab.BindersUtil
 import Lean.Elab.PatternVar
 import Lean.Elab.Quotation.Precheck
@@ -28,10 +27,6 @@ private def mkUserNameFor (e : Expr) : TermElabM Name := do
 
 
 /--
-   We treat `@x` as atomic to avoid unnecessary extra local declarations from being
-   inserted into the local context. Recall that `expandMatchAltsIntoMatch` uses `@` modifier.
-   Thus this is kind of discriminant is quite common.
-
    Remark: if the discriminat is `Systax.missing`, we abort the elaboration of the `match`-expression.
    This can happen due to error recovery. Example
    ```
@@ -46,23 +41,17 @@ private def mkUserNameFor (e : Expr) : TermElabM Name := do
    let d := <Syntax.missing>; match
    ```
    Recall that `Syntax.setArg stx i arg` is a no-op when `i` is out-of-bounds. -/
-def isAtomicDiscr? (discr : Syntax) : TermElabM (Option Expr) := do
+def isAtomicDiscr (discr : Syntax) : TermElabM Bool := do
   match discr with
-  | `($x:ident)  => isLocalIdent? x
-  | `(@$x:ident) => isLocalIdent? x
-  | _ => if discr.isMissing then throwAbortTerm else return none
+  | `($_:ident)  => pure true
+  | `(@$_:ident) => pure true
+  | `(?$_:ident) => pure true
+  | _ => if discr.isMissing then throwAbortTerm else pure false
 
 -- See expandNonAtomicDiscrs?
 private def elabAtomicDiscr (discr : Syntax) : TermElabM Expr := do
   let term := discr[1]
-  match (← isAtomicDiscr? term) with
-  | some e@(Expr.fvar fvarId) =>
-    let localDecl ← fvarId.getDecl
-    if !isAuxDiscrName localDecl.userName then
-      addTermInfo term e -- it is not an auxiliary local created by `expandNonAtomicDiscrs?`
-    else
-      instantiateMVars localDecl.value
-  | _ => throwErrorAt discr "unexpected discriminant"
+  elabTerm term none
 
 structure Discr where
   expr : Expr
@@ -758,14 +747,6 @@ private def withToClear (toClear : Array FVarId) (type : Expr) (k : TermElabM α
           localInsts := localInsts.filter fun localInst => localInst.fvar.fvarId! != fvarId
     withLCtx lctx localInsts k
 
-
-private def withoutAuxDiscrs (matchType : Expr) (k : TermElabM α) : TermElabM α := do
-  let mut toClear := #[]
-  for localDecl in (← getLCtx) do
-    if isAuxDiscrName localDecl.userName || isAuxFunDiscrName localDecl.userName then
-      toClear := toClear.push localDecl.fvarId
-  withToClear toClear matchType k
-
 /--
   Generate equalities `h : discr = pattern` for discriminants annotated with `h :`.
   We use these equalities to elaborate the right-hand-side of a `match` alternative.
@@ -794,7 +775,6 @@ where
   they have been generalized/refined.
 -/
 private def elabMatchAltView (discrs : Array Discr) (alt : MatchAltView) (matchType : Expr) (toClear : Array FVarId) : ExceptT PatternElabException TermElabM (AltLHS × Expr) := withRef alt.ref do
-  withoutAuxDiscrs matchType do
     let (patternVars, alt) ← collectPatternVars alt
     trace[Elab.match] "patternVars: {patternVars}"
     withPatternVars patternVars fun patternVarDecls => do
@@ -1128,13 +1108,11 @@ private def expandNonAtomicDiscrs? (matchStx : Syntax) : TermElabM (Option Synta
   let matchOptMotive := getMatchOptMotive matchStx
   if matchOptMotive.isNone then do
     let discrs := getDiscrs matchStx
-    let allLocal ← discrs.allM fun discr => Option.isSome <$> isAtomicDiscr? discr[1]
+    let allLocal ← discrs.allM fun discr => isAtomicDiscr discr[1]
     if allLocal then
       return none
     else
-      -- We use `foundFVars` to make sure the discriminants are distinct variables.
-      -- See: code for computing "matchType" at `elabMatchTypeAndDiscrs`
-      let rec loop (discrs : List Syntax) (discrsNew : Array Syntax) (foundFVars : FVarIdSet) := do
+      let rec loop (discrs : List Syntax) (discrsNew : Array Syntax)  := do
         match discrs with
         | [] =>
           let discrs := Syntax.mkSep discrsNew (mkAtomFrom matchStx ", ")
@@ -1143,17 +1121,14 @@ private def expandNonAtomicDiscrs? (matchStx : Syntax) : TermElabM (Option Synta
           -- Recall that
           -- matchDiscr := leading_parser optional (ident >> ":") >> termParser
           let term := discr[1]
-          let addAux : TermElabM Syntax := withFreshMacroScope do
-            let d ← mkAuxDiscr
-            unless isAuxDiscrName d.getId do -- Use assertion?
-              throwError "unexpected internal auxiliary discriminant name"
-            let discrNew := discr.setArg 1 d
-            let r ← loop discrs (discrsNew.push discrNew) foundFVars
-            `(let $d := $term; $r)
-          match (← isAtomicDiscr? term) with
-          | some x  => if x.isFVar then loop discrs (discrsNew.push discr) (foundFVars.insert x.fvarId!) else addAux
-          | none    => addAux
-      return some (← loop discrs.toList #[] {})
+          if (← isAtomicDiscr term) then
+            loop discrs (discrsNew.push discr)
+          else
+            withFreshMacroScope do
+              let discrNew := discr.setArg 1 (← `(?x))
+              let r ← loop discrs (discrsNew.push discrNew)
+              `(let_mvar% ?x := $term; $r)
+      return some (← loop discrs.toList #[])
   else
     -- We do not pull non atomic discriminants when match type is provided explicitly by the user
     return none
@@ -1170,18 +1145,17 @@ private def tryPostponeIfDiscrTypeIsMVar (matchStx : Syntax) : TermElabM Unit :=
     let discrs := getDiscrs matchStx
     for discr in discrs do
       let term := discr[1]
-      match (← isAtomicDiscr? term) with
-      | none   => throwErrorAt discr "unexpected discriminant" -- see `expandNonAtomicDiscrs?
-      | some d =>
-        let dType ← inferType d
-        trace[Elab.match] "discr {d} : {dType}"
-        tryPostponeIfMVar dType
+      let d ← elabTerm term none
+      let dType ← inferType d
+      trace[Elab.match] "discr {d} : {← instantiateMVars dType}"
+      tryPostponeIfMVar dType
 
 /--
 We (try to) elaborate a `match` only when the expected type is available.
 If the `matchType` has not been provided by the user, we also try to postpone elaboration if the type
 of a discriminant is not available. That is, it is of the form `(?m ...)`.
-We use `expandNonAtomicDiscrs?` to make sure all discriminants are local variables.
+We use `expandNonAtomicDiscrs?` to make sure all discriminants are metavariables,
+so that they are not elaborated twice.
 This is a standard trick we use in the elaborator, and it is also used to elaborate structure instances.
 Suppose, we are trying to elaborate
 ```
@@ -1190,12 +1164,10 @@ match g x with
 ```
 `expandNonAtomicDiscrs?` converts it intro
 ```
-let _discr := g x
-match _discr with
+let_mvar% ?discr := g x
+match ?discr with
   | ... => ...
 ```
-Thus, at `tryPostponeIfDiscrTypeIsMVar` we only need to check whether the type of `_discr` is not of the form `(?m ...)`.
-Note that, the auxiliary variable `_discr` is expanded at `elabAtomicDiscr`.
 
 This elaboration technique is needed to elaborate terms such as:
 ```lean
@@ -1268,14 +1240,12 @@ builtin_initialize
 @[builtinTermElab «nomatch»] def elabNoMatch : TermElab := fun stx expectedType? => do
   match stx with
   | `(nomatch $discrExpr) =>
-    match (← isLocalIdent? discrExpr) with
-    | some _ =>
+    if (← isAtomicDiscr discrExpr) then
       let expectedType ← waitExpectedType expectedType?
       let discr := mkNode ``Lean.Parser.Term.matchDiscr #[mkNullNode, discrExpr]
       elabMatchAux none #[discr] #[] mkNullNode expectedType
-    | _ =>
-      let d ← mkAuxDiscr
-      let stxNew ← `(let $d := $discrExpr; nomatch $d)
+    else
+      let stxNew ← `(let_mvar% ?x := $discrExpr; nomatch ?x)
       withMacroExpansion stx stxNew <| elabTerm stxNew expectedType?
   | _ => throwUnsupportedSyntax
 

src/Lean/Elab/MutualDef.lean

@@ -720,14 +720,6 @@ private def levelMVarToParamHeaders (views : Array DefView) (headers : Array Def
   let newHeaders ← (process).run' 1
   newHeaders.mapM fun header => return { header with type := (← instantiateMVars header.type) }
 
-/-- Remove auxiliary match discriminant let-declarations. -/
-def eraseAuxDiscr (e : Expr) : CoreM Expr := do
-  Core.transform e fun e => do
-    if let .letE n _ v b .. := e then
-      if isAuxDiscrName n then
-        return .visit (b.instantiate1 v)
-    return .continue
-
 partial def checkForHiddenUnivLevels (allUserLevelNames : List Name) (preDefs : Array PreDefinition) : TermElabM Unit :=
   unless (← MonadLog.hasErrors) do
     -- We do not report this kind of error if the declaration already contains errors
@@ -800,11 +792,6 @@ where
         let preDefs ← withLevelNames allUserLevelNames <| levelMVarToParamPreDecls preDefs
         let preDefs ← instantiateMVarsAtPreDecls preDefs
         let preDefs ← fixLevelParams preDefs scopeLevelNames allUserLevelNames
-        let preDefs ← preDefs.mapM fun preDef =>
-          if preDef.kind.isTheorem || preDef.kind.isExample then
-            return preDef
-          else
-            return { preDef with value := (← eraseAuxDiscr preDef.value) }
         for preDef in preDefs do
           trace[Elab.definition] "after eraseAuxDiscr, {preDef.declName} : {preDef.type} :=\n{preDef.value}"
         checkForHiddenUnivLevels allUserLevelNames preDefs

src/Lean/Elab/Quotation.lean

@@ -581,6 +581,15 @@ private partial def compileStxMatch (discrs : List Term) (alts : List Alt) : Ter
 
 abbrev IdxSet := HashSet Nat
 
+private partial def hasNoErrorIfUnused : Syntax → Bool
+  | `(no_error_if_unused% $_) => true
+  -- | `(clear% $_; $body) => hasNoErrorIfUnused body
+  | stx =>
+    if stx.getKind == `Lean.Parser.Term.clear then
+      hasNoErrorIfUnused stx[3]
+    else
+      false
+
 /--
 Given `rhss` the right-hand-sides of a `match`-syntax notation,
 We tag them with with fresh identifiers `alt_idx`. We use them to detect whether an alternative
@@ -596,9 +605,8 @@ private def markRhss (rhss : Array Term) : TermElabM (NameMap Nat × IdxSet × A
   let mut ignoreIfUnused : IdxSet := {}
   let mut rhssNew := #[]
   for rhs in rhss do
-    match rhs with
-    | `(no_error_if_unused% $_ ) => ignoreIfUnused := ignoreIfUnused.insert rhssNew.size
-    | _ => pure ()
+    if hasNoErrorIfUnused rhs then
+      ignoreIfUnused := ignoreIfUnused.insert rhssNew.size
     let (idx, rhs) ← withFreshMacroScope do
       let idx ← `(alt_idx)
       let rhs ← `(alt_idx $rhs)

src/Lean/PrettyPrinter/Delaborator/Basic.lean

@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Sebastian Ullrich
 -/
 import Lean.Elab.Term
-import Lean.Elab.AuxDiscr
 import Lean.PrettyPrinter.Delaborator.Options
 import Lean.PrettyPrinter.Delaborator.SubExpr
 import Lean.PrettyPrinter.Delaborator.TopDownAnalyze
@@ -171,7 +170,7 @@ def getUnusedName (suggestion : Name) (body : Expr) : DelabM Name := do
   -- Use a nicer binder name than `[anonymous]`. We probably shouldn't do this in all LocalContext use cases, so do it here.
   let suggestion := if suggestion.isAnonymous then `a else suggestion
   -- We use this small hack to convert identifiers created using `mkAuxFunDiscr` to simple names
-  let suggestion := if isAuxFunDiscrName suggestion then `x else suggestion.eraseMacroScopes
+  let suggestion := suggestion.eraseMacroScopes
   let lctx ← getLCtx
   if !lctx.usesUserName suggestion then
     return suggestion