From 45c4f2faa0a4e67ecdbe17ad8b29683de878e407 Mon Sep 17 00:00:00 2001 From: Gabriel Ebner Date: Mon, 10 Oct 2022 14:29:25 -0700 Subject: [PATCH] refactor: remove _aux_discr --- src/Lean/Elab/AuxDiscr.lean | 33 -------- src/Lean/Elab/Binders.lean | 29 ++++--- src/Lean/Elab/BindersUtil.lean | 17 ++++ src/Lean/Elab/Match.lean | 84 ++++++------------- src/Lean/Elab/MutualDef.lean | 13 --- src/Lean/Elab/Quotation.lean | 14 +++- src/Lean/PrettyPrinter/Delaborator/Basic.lean | 3 +- 7 files changed, 70 insertions(+), 123 deletions(-) delete mode 100644 src/Lean/Elab/AuxDiscr.lean diff --git a/src/Lean/Elab/AuxDiscr.lean b/src/Lean/Elab/AuxDiscr.lean deleted file mode 100644 index c07326fac3..0000000000 --- a/src/Lean/Elab/AuxDiscr.lean +++ /dev/null @@ -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 diff --git a/src/Lean/Elab/Binders.lean b/src/Lean/Elab/Binders.lean index d6546dc059..6923e52eac 100644 --- a/src/Lean/Elab/Binders.lean +++ b/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 diff --git a/src/Lean/Elab/BindersUtil.lean b/src/Lean/Elab/BindersUtil.lean index b6dc925fde..b5c7ede4f6 100644 --- a/src/Lean/Elab/BindersUtil.lean +++ b/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 diff --git a/src/Lean/Elab/Match.lean b/src/Lean/Elab/Match.lean index e0ed3d50d5..4d4d1ac749 100644 --- a/src/Lean/Elab/Match.lean +++ b/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 := ; 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 diff --git a/src/Lean/Elab/MutualDef.lean b/src/Lean/Elab/MutualDef.lean index fac8407b6c..b90a89c3d6 100644 --- a/src/Lean/Elab/MutualDef.lean +++ b/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 diff --git a/src/Lean/Elab/Quotation.lean b/src/Lean/Elab/Quotation.lean index 9cdf1a7512..d4f4eb28cf 100644 --- a/src/Lean/Elab/Quotation.lean +++ b/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) diff --git a/src/Lean/PrettyPrinter/Delaborator/Basic.lean b/src/Lean/PrettyPrinter/Delaborator/Basic.lean index 8330f6b471..f479917608 100644 --- a/src/Lean/PrettyPrinter/Delaborator/Basic.lean +++ b/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