max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix: move auxDeclToFullName to LocalContext to fix name (un)resolution (#7075)

Browse source 
This PR ensures that names suggested by tactics like `simp?` are not
shadowed by auxiliary declarations in the local context and that names
of `let rec` and `where` declarations are correctly resolved in tactic
blocks.

This PR contains the following potentially breaking changes:
* Moves the `auxDeclToFullName` map from `TermElab.Context` to
`LocalContext`.
* Refactors `Lean.Elab.Term.resolveLocalName : Name → TermElabM …` to
`Lean.resolveLocalName [MonadResolveName m] [MonadEnv m] [MonadLCtx m] :
Name → m …`.
* Refactors the `TermElabM` action `Lean.Elab.Term.withAuxDecl` to a
monad-polymorphic action `Lean.Meta.withAuxDecl`.
* Adds an optional `filter` argument to `Lean.unresolveNameGlobal`.

Closes #6706, closes #7073.
This commit is contained in:
jrr6 2025-03-03 11:10:54 -05:00 • committed by GitHub
parent d3eb2fe13c
commit e337129108
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
10 changed files with 293 additions and 212 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/Lean/Elab/App.lean
View file

@ -1215,7 +1215,7 @@ private def resolveLValAux (e : Expr) (eType : Expr) (lval : LVal) : TermElabM L
let fullName := Name.mkStr structName fieldName
for localDecl in (← getLCtx) do
if localDecl.isAuxDecl then
if let some localDeclFullName := (← read).auxDeclToFullName.find? localDecl.fvarId then
if let some localDeclFullName := (← getLCtx).auxDeclToFullName.find? localDecl.fvarId then
if fullName == (privateToUserName? localDeclFullName).getD localDeclFullName then
/- LVal notation is being used to make a "local" recursive call. -/
return LValResolution.localRec structName fullName localDecl.toExpr

2
src/Lean/Elab/MutualInductive.lean
View file

@ -336,7 +336,7 @@ private def withInductiveLocalDecls (rs : Array PreElabHeaderResult) (x : Array
let rec loop (i : Nat) (indFVars : Array Expr) := do
if h : i < namesAndTypes.size then
let (declName, shortDeclName, type) := namesAndTypes[i]
Term.withAuxDecl shortDeclName type declName fun indFVar => loop (i+1) (indFVars.push indFVar)
withAuxDecl shortDeclName type declName fun indFVar => loop (i+1) (indFVars.push indFVar)
else
x params indFVars
loop 0 #[]

176
src/Lean/Elab/Term.lean
View file

@ -258,10 +258,6 @@ namespace Term
structure Context where
declName? : Option Name := none
/--
Map `.auxDecl` local declarations used to encode recursive declarations to their full-names.
-/
auxDeclToFullName : FVarIdMap Name := {}
macroStack : MacroStack := []
/--
When `mayPostpone == true`, an elaboration function may interrupt its execution by throwing `Exception.postpone`.
@ -627,15 +623,6 @@ def withLevelNames (levelNames : List Name) (x : TermElabM α) : TermElabM α :=
setLevelNames levelNames
try x finally setLevelNames levelNamesSaved
/--
Declare an auxiliary local declaration `shortDeclName : type` for elaborating recursive declaration `declName`,
update the mapping `auxDeclToFullName`, and then execute `k`.
-/
def withAuxDecl (shortDeclName : Name) (type : Expr) (declName : Name) (k : Expr → TermElabM α) : TermElabM α :=
withLocalDecl shortDeclName .default (kind := .auxDecl) type fun x =>
withReader (fun ctx => { ctx with auxDeclToFullName := ctx.auxDeclToFullName.insert x.fvarId! declName }) do
k x
def withoutErrToSorryImp (x : TermElabM α) : TermElabM α :=
withReader (fun ctx => { ctx with errToSorry := false }) x
@ -1522,169 +1509,6 @@ def blockImplicitLambda (stx : Syntax) : Bool :=
isExplicit stx || isExplicitApp stx || isLambdaWithImplicit stx || isHole stx || isTacticBlock stx ||
isNoImplicitLambda stx || isTypeAscription stx
def resolveLocalName (n : Name) : TermElabM (Option (Expr × List String)) := do
let lctx ← getLCtx
let auxDeclToFullName := (← read).auxDeclToFullName
let currNamespace ← getCurrNamespace
let view := extractMacroScopes n
/- Simple case. "Match" function for regular local declarations. -/
let matchLocalDecl? (localDecl : LocalDecl) (givenName : Name) : Option LocalDecl := do
guard (localDecl.userName == givenName)
return localDecl
/-
"Match" function for auxiliary declarations that correspond to recursive definitions being defined.
This function is used in the first-pass.
Note that we do not check for `localDecl.userName == givenName` in this pass as we do for regular local declarations.
Reason: consider the following example
```
mutual
inductive Foo
| somefoo : Foo | bar : Bar → Foo → Foo
inductive Bar
| somebar : Bar| foobar : Foo → Bar → Bar
end
mutual
private def Foo.toString : Foo → String
| Foo.somefoo => go 2 ++ toString.go 2 ++ Foo.toString.go 2
| Foo.bar b f => toString f ++ Bar.toString b
where
go (x : Nat) := s!"foo {x}"
private def _root_.Ex2.Bar.toString : Bar → String
| Bar.somebar => "bar"
| Bar.foobar f b => Foo.toString f ++ Bar.toString b
end
```
In the example above, we have two local declarations named `toString` in the local context, and
we want the `toString f` to be resolved to `Foo.toString f`.
-/
let matchAuxRecDecl? (localDecl : LocalDecl) (fullDeclName : Name) (givenNameView : MacroScopesView) : Option LocalDecl := do
let fullDeclView := extractMacroScopes fullDeclName
/- First cleanup private name annotations -/
let fullDeclView := { fullDeclView with name := (privateToUserName? fullDeclView.name).getD fullDeclView.name }
let fullDeclName := fullDeclView.review
let localDeclNameView := extractMacroScopes localDecl.userName
/- If the current namespace is a prefix of the full declaration name,
we use a relaxed matching test where we must satisfy the following conditions
- The local declaration is a suffix of the given name.
- The given name is a suffix of the full declaration.
Recall the `let rec`/`where` declaration naming convention. For example, suppose we have
```
def Foo.Bla.f ... :=
... go ...
where
go ... := ...
```
The current namespace is `Foo.Bla`, and the full name for `go` is `Foo.Bla.f.g`, but we want to
refer to it using just `go`. It is also accepted to refer to it using `f.go`, `Bla.f.go`, etc.
-/
if currNamespace.isPrefixOf fullDeclName then
/- Relaxed mode that allows us to access `let rec` declarations using shorter names -/
guard (localDeclNameView.isSuffixOf givenNameView)
guard (givenNameView.isSuffixOf fullDeclView)
return localDecl
else
/-
It is the standard algorithm we are using at `resolveGlobalName` for processing namespaces.
The current solution also has a limitation when using `def _root_` in a mutual block.
The non `def _root_` declarations may update the namespace. See the following example:
```
mutual
def Foo.f ... := ...
def _root_.g ... := ...
let rec h := ...
...
end
```
`def Foo.f` updates the namespace. Then, even when processing `def _root_.g ...`
the condition `currNamespace.isPrefixOf fullDeclName` does not hold.
This is not a big problem because we are planning to modify how we handle the mutual block in the future.
Note that we don't check for `localDecl.userName == givenName` here.
-/
let rec go (ns : Name) : Option LocalDecl := do
if { givenNameView with name := ns ++ givenNameView.name }.review == fullDeclName then
return localDecl
match ns with
| .str pre .. => go pre
| _ => failure
return (← go currNamespace)
/- Traverse the local context backwards looking for match `givenNameView`.
If `skipAuxDecl` we ignore `auxDecl` local declarations. -/
let findLocalDecl? (givenNameView : MacroScopesView) (skipAuxDecl : Bool) : Option LocalDecl :=
let givenName := givenNameView.review
let localDecl? := lctx.decls.findSomeRev? fun localDecl? => do
let localDecl ← localDecl?
if localDecl.isAuxDecl then
guard (!skipAuxDecl)
if let some fullDeclName := auxDeclToFullName.find? localDecl.fvarId then
matchAuxRecDecl? localDecl fullDeclName givenNameView
else
matchLocalDecl? localDecl givenName
else
matchLocalDecl? localDecl givenName
if localDecl?.isSome || skipAuxDecl then
localDecl?
else
-- Search auxDecls again trying an exact match of the given name
lctx.decls.findSomeRev? fun localDecl? => do
let localDecl ← localDecl?
guard localDecl.isAuxDecl
matchLocalDecl? localDecl givenName
/-
We use the parameter `globalDeclFound` to decide whether we should skip auxiliary declarations or not.
We set it to true if we found a global declaration `n` as we iterate over the `loop`.
Without this workaround, we would not be able to elaborate an example such as
```
def foo.aux := 1
def foo : Nat → Nat
| n => foo.aux -- should not be interpreted as `(foo).aux`
```
See test `aStructPerfIssue.lean` for another example.
We skip auxiliary declarations when `projs` is not empty and `globalDeclFound` is true.
Remark: we did not use to have the `globalDeclFound` parameter. Without this extra check we failed
to elaborate
```
example : Nat :=
let n := 0
n.succ + (m |>.succ) + m.succ
where
m := 1
```
See issue #1850.
-/
let rec loop (n : Name) (projs : List String) (globalDeclFound : Bool) := do
let givenNameView := { view with name := n }
let mut globalDeclFoundNext := globalDeclFound
unless globalDeclFound do
let r ← resolveGlobalName givenNameView.review
let r := r.filter fun (_, fieldList) => fieldList.isEmpty
unless r.isEmpty do
globalDeclFoundNext := true
/-
Note that we use `globalDeclFound` instead of `globalDeclFoundNext` in the following test.
Reason: a local should shadow a global with the same name.
Consider the following example. See issue #3079
```
def foo : Nat := 1
def bar : Nat :=
foo.add 1 -- should be 11
where
foo := 10
```
-/
match findLocalDecl? givenNameView (skipAuxDecl := globalDeclFound && !projs.isEmpty) with
| some decl => return some (decl.toExpr, projs)
| none => match n with
| .str pre s => loop pre (s::projs) globalDeclFoundNext
| _ => return none
loop view.name [] (globalDeclFound := false)
/-- Return true iff `stx` is a `Syntax.ident`, and it is a local variable. -/
def isLocalIdent? (stx : Syntax) : TermElabM (Option Expr) :=
match stx with

67
src/Lean/LocalContext.lean
View file

@ -159,14 +159,16 @@ end LocalDecl
/-- A LocalContext is an ordered set of local variable declarations.
It is used to store the free variables (also known as local constants) that
are in scope.
are in scope. It also maps free variables corresponding to auxiliary declarations
(recursive references and `where` and `let rec` bindings) to their fully-qualified global names.
When inspecting a goal or expected type in the infoview, the local
context is all of the variables above the `⊢` symbol.
-/
structure LocalContext where
fvarIdToDecl : PersistentHashMap FVarId LocalDecl := {}
decls : PersistentArray (Option LocalDecl) := {}
fvarIdToDecl : PersistentHashMap FVarId LocalDecl := {}
decls : PersistentArray (Option LocalDecl) := {}
auxDeclToFullName : FVarIdMap Name := {}
deriving Inhabited
namespace LocalContext
@ -186,10 +188,10 @@ It should not be used directly since the argument `(fvarId : FVarId)` is
assumed to be unique. You can create a unique fvarId with `mkFreshFVarId`. -/
def mkLocalDecl (lctx : LocalContext) (fvarId : FVarId) (userName : Name) (type : Expr) (bi : BinderInfo := BinderInfo.default) (kind : LocalDeclKind := .default) : LocalContext :=
match lctx with
| { fvarIdToDecl := map, decls := decls } =>
| { fvarIdToDecl := map, decls := decls, auxDeclToFullName } =>
let idx := decls.size
let decl := LocalDecl.cdecl idx fvarId userName type bi kind
{ fvarIdToDecl := map.insert fvarId decl, decls := decls.push decl }
{ fvarIdToDecl := map.insert fvarId decl, decls := decls.push decl, auxDeclToFullName }
-- `mkLocalDecl` without `kind`
@[export lean_local_ctx_mk_local_decl]
@ -199,23 +201,34 @@ private def mkLocalDeclExported (lctx : LocalContext) (fvarId : FVarId) (userNam
/-- Low level API for let declarations. Do not use directly.-/
def mkLetDecl (lctx : LocalContext) (fvarId : FVarId) (userName : Name) (type : Expr) (value : Expr) (nonDep := false) (kind : LocalDeclKind := default) : LocalContext :=
match lctx with
| { fvarIdToDecl := map, decls := decls } =>
| { fvarIdToDecl := map, decls := decls, auxDeclToFullName } =>
let idx := decls.size
let decl := LocalDecl.ldecl idx fvarId userName type value nonDep kind
{ fvarIdToDecl := map.insert fvarId decl, decls := decls.push decl }
{ fvarIdToDecl := map.insert fvarId decl, decls := decls.push decl, auxDeclToFullName }
@[export lean_local_ctx_mk_let_decl]
private def mkLetDeclExported (lctx : LocalContext) (fvarId : FVarId) (userName : Name) (type : Expr) (value : Expr) (nonDep : Bool) : LocalContext :=
mkLetDecl lctx fvarId userName type value nonDep
/-- Low level API for auxiliary declarations. Do not use directly. -/
def mkAuxDecl (lctx : LocalContext) (fvarId : FVarId) (userName : Name) (type : Expr) (fullName : Name) : LocalContext :=
match lctx with
| { fvarIdToDecl := map, decls := decls, auxDeclToFullName } =>
let idx := decls.size
let decl := LocalDecl.cdecl idx fvarId userName type .default .auxDecl
let auxDeclToFullName := auxDeclToFullName.insert fvarId fullName
{ fvarIdToDecl := map.insert fvarId decl, decls := decls.push decl, auxDeclToFullName }
/-- Low level API for adding a local declaration.
Do not use directly. -/
def addDecl (lctx : LocalContext) (newDecl : LocalDecl) : LocalContext :=
match lctx with
| { fvarIdToDecl := map, decls := decls } =>
| { fvarIdToDecl := map, decls := decls, auxDeclToFullName } =>
let idx := decls.size
let newDecl := newDecl.setIndex idx
{ fvarIdToDecl := map.insert newDecl.fvarId newDecl, decls := decls.push newDecl }
{ fvarIdToDecl := map.insert newDecl.fvarId newDecl
decls := decls.push newDecl
auxDeclToFullName }
@[export lean_local_ctx_find]
def find? (lctx : LocalContext) (fvarId : FVarId) : Option LocalDecl :=
@ -260,18 +273,26 @@ private partial def popTailNoneAux (a : PArray (Option LocalDecl)) : PArray (Opt
@[export lean_local_ctx_erase]
def erase (lctx : LocalContext) (fvarId : FVarId) : LocalContext :=
match lctx with
| { fvarIdToDecl := map, decls := decls } =>
| { fvarIdToDecl := map, decls := decls, auxDeclToFullName } =>
match map.find? fvarId with
| none => lctx
| some decl => { fvarIdToDecl := map.erase fvarId, decls := popTailNoneAux (decls.set decl.index none) }
| some decl =>
{ fvarIdToDecl := map.erase fvarId
decls := popTailNoneAux (decls.set decl.index none)
auxDeclToFullName :=
if decl.isAuxDecl then auxDeclToFullName.erase fvarId else auxDeclToFullName }
def pop (lctx : LocalContext): LocalContext :=
def pop (lctx : LocalContext) : LocalContext :=
match lctx with
| { fvarIdToDecl := map, decls := decls } =>
| { fvarIdToDecl := map, decls := decls, auxDeclToFullName } =>
if _ : decls.size = 0 then lctx
else match decls[decls.size - 1] with
| none => lctx -- unreachable
| some decl => { fvarIdToDecl := map.erase decl.fvarId, decls := popTailNoneAux decls.pop }
| some decl =>
{ fvarIdToDecl := map.erase decl.fvarId
decls := popTailNoneAux decls.pop
auxDeclToFullName :=
if decl.isAuxDecl then auxDeclToFullName.erase decl.fvarId else auxDeclToFullName }
def findFromUserName? (lctx : LocalContext) (userName : Name) : Option LocalDecl :=
lctx.decls.findSomeRev? fun decl =>
@ -298,18 +319,20 @@ def lastDecl (lctx : LocalContext) : Option LocalDecl :=
def setUserName (lctx : LocalContext) (fvarId : FVarId) (userName : Name) : LocalContext :=
let decl := lctx.get! fvarId
let decl := decl.setUserName userName
{ fvarIdToDecl := lctx.fvarIdToDecl.insert decl.fvarId decl,
decls := lctx.decls.set decl.index decl }
{ fvarIdToDecl := lctx.fvarIdToDecl.insert decl.fvarId decl,
decls := lctx.decls.set decl.index decl,
auxDeclToFullName := lctx.auxDeclToFullName }
def renameUserName (lctx : LocalContext) (fromName : Name) (toName : Name) : LocalContext :=
match lctx with
| { fvarIdToDecl := map, decls := decls } =>
| { fvarIdToDecl := map, decls := decls, auxDeclToFullName } =>
match lctx.findFromUserName? fromName with
| none => lctx
| some decl =>
let decl := decl.setUserName toName;
{ fvarIdToDecl := map.insert decl.fvarId decl,
decls := decls.set decl.index decl }
decls := decls.set decl.index decl,
auxDeclToFullName }
/--
Low-level function for updating the local context.
@ -317,13 +340,14 @@ def renameUserName (lctx : LocalContext) (fromName : Name) (toName : Name) : Loc
the `index` nor `fvarId` are modified. -/
@[inline] def modifyLocalDecl (lctx : LocalContext) (fvarId : FVarId) (f : LocalDecl → LocalDecl) : LocalContext :=
match lctx with
| { fvarIdToDecl := map, decls := decls } =>
| { fvarIdToDecl := map, decls := decls, auxDeclToFullName } =>
match lctx.find? fvarId with
| none => lctx
| some decl =>
let decl := f decl
{ fvarIdToDecl := map.insert decl.fvarId decl
decls := decls.set decl.index decl }
decls := decls.set decl.index decl
auxDeclToFullName }
/--
Set the kind of the given fvar.
@ -520,6 +544,7 @@ def LocalDecl.replaceFVarId (fvarId : FVarId) (e : Expr) (d : LocalDecl) : Local
def LocalContext.replaceFVarId (fvarId : FVarId) (e : Expr) (lctx : LocalContext) : LocalContext :=
let lctx := lctx.erase fvarId
{ fvarIdToDecl := lctx.fvarIdToDecl.map (·.replaceFVarId fvarId e)
decls := lctx.decls.map fun localDecl? => localDecl?.map (·.replaceFVarId fvarId e) }
decls := lctx.decls.map fun localDecl? => localDecl?.map (·.replaceFVarId fvarId e),
auxDeclToFullName := lctx.auxDeclToFullName }
end Lean

15
src/Lean/Meta/Basic.lean
View file

@ -1664,6 +1664,21 @@ def withLocalDeclsDND [Inhabited α] (declInfos : Array (Name × Expr)) (k : (xs
withLocalDeclsD
(declInfos.map (fun (name, typeCtor) => (name, fun _ => pure typeCtor))) k
private def withAuxDeclImp (shortDeclName : Name) (type : Expr) (declName : Name) (k : Expr → MetaM α) : MetaM α := do
let fvarId ← mkFreshFVarId
let ctx ← read
let lctx := ctx.lctx.mkAuxDecl fvarId shortDeclName type declName
let fvar := mkFVar fvarId
withReader (fun ctx => { ctx with lctx := lctx }) do
withNewFVar fvar type k
/--
Declare an auxiliary local declaration `shortDeclName : type` for elaborating recursive
declaration `declName`, update the mapping `auxDeclToFullName`, and then execute `k`.
-/
def withAuxDecl (shortDeclName : Name) (type : Expr) (declName : Name) (k : Expr → n α) : n α :=
map1MetaM (fun k => withAuxDeclImp shortDeclName type declName k) k
private def withNewBinderInfosImp (bs : Array (FVarId × BinderInfo)) (k : MetaM α) : MetaM α := do
let lctx := bs.foldl (init := (← getLCtx)) fun lctx (fvarId, bi) =>
lctx.setBinderInfo fvarId bi

7
src/Lean/MetavarContext.lean
View file

@ -588,8 +588,15 @@ def instantiateMVars [Monad m] [MonadMCtx m] (e : Expr) : m Expr := do
return r
def instantiateLCtxMVars [Monad m] [MonadMCtx m] (lctx : LocalContext) : m LocalContext :=
let auxDeclToFullName := lctx.auxDeclToFullName
lctx.foldlM (init := {}) fun lctx ldecl => do
match ldecl with
| .cdecl _ fvarId userName type _ .auxDecl =>
let type ← instantiateMVars type
let .some fullName := auxDeclToFullName.find? fvarId
| panic! s!"Invalid auxiliary declaration found in local context: \
{userName} does not have an associated full name."
return lctx.mkAuxDecl fvarId userName type fullName
| .cdecl _ fvarId userName type bi k =>
let type ← instantiateMVars type
return lctx.mkLocalDecl fvarId userName type bi k

187
src/Lean/ResolveName.lean
View file

@ -391,6 +391,170 @@ After `open Foo open Boo`, we have
def resolveGlobalConstNoOverload [Monad m] [MonadResolveName m] [MonadEnv m] [MonadError m] (id : Syntax) : m Name := do
ensureNonAmbiguous id (← resolveGlobalConst id)
/-- Resolves the name `n` in the local context. -/
def resolveLocalName [Monad m] [MonadResolveName m] [MonadEnv m] [MonadLCtx m] (n : Name) : m (Option (Expr × List String)) := do
let lctx ← getLCtx
let auxDeclToFullName := (← getLCtx).auxDeclToFullName
let currNamespace ← getCurrNamespace
let view := extractMacroScopes n
/- Simple case. "Match" function for regular local declarations. -/
let matchLocalDecl? (localDecl : LocalDecl) (givenName : Name) : Option LocalDecl := do
guard (localDecl.userName == givenName)
return localDecl
/-
"Match" function for auxiliary declarations that correspond to recursive definitions being defined.
This function is used in the first-pass.
Note that we do not check for `localDecl.userName == givenName` in this pass as we do for regular local declarations.
Reason: consider the following example
```
mutual
inductive Foo
| somefoo : Foo | bar : Bar → Foo → Foo
inductive Bar
| somebar : Bar| foobar : Foo → Bar → Bar
end
mutual
private def Foo.toString : Foo → String
| Foo.somefoo => go 2 ++ toString.go 2 ++ Foo.toString.go 2
| Foo.bar b f => toString f ++ Bar.toString b
where
go (x : Nat) := s!"foo {x}"
private def _root_.Ex2.Bar.toString : Bar → String
| Bar.somebar => "bar"
| Bar.foobar f b => Foo.toString f ++ Bar.toString b
end
```
In the example above, we have two local declarations named `toString` in the local context, and
we want the `toString f` to be resolved to `Foo.toString f`.
-/
let matchAuxRecDecl? (localDecl : LocalDecl) (fullDeclName : Name) (givenNameView : MacroScopesView) : Option LocalDecl := do
let fullDeclView := extractMacroScopes fullDeclName
/- First cleanup private name annotations -/
let fullDeclView := { fullDeclView with name := (privateToUserName? fullDeclView.name).getD fullDeclView.name }
let fullDeclName := fullDeclView.review
let localDeclNameView := extractMacroScopes localDecl.userName
/- If the current namespace is a prefix of the full declaration name,
we use a relaxed matching test where we must satisfy the following conditions
- The local declaration is a suffix of the given name.
- The given name is a suffix of the full declaration.
Recall the `let rec`/`where` declaration naming convention. For example, suppose we have
```
def Foo.Bla.f ... :=
... go ...
where
go ... := ...
```
The current namespace is `Foo.Bla`, and the full name for `go` is `Foo.Bla.f.g`, but we want to
refer to it using just `go`. It is also accepted to refer to it using `f.go`, `Bla.f.go`, etc.
-/
if currNamespace.isPrefixOf fullDeclName then
/- Relaxed mode that allows us to access `let rec` declarations using shorter names -/
guard (localDeclNameView.isSuffixOf givenNameView)
guard (givenNameView.isSuffixOf fullDeclView)
return localDecl
else
/-
It is the standard algorithm we are using at `resolveGlobalName` for processing namespaces.
The current solution also has a limitation when using `def _root_` in a mutual block.
The non `def _root_` declarations may update the namespace. See the following example:
```
mutual
def Foo.f ... := ...
def _root_.g ... := ...
let rec h := ...
...
end
```
`def Foo.f` updates the namespace. Then, even when processing `def _root_.g ...`
the condition `currNamespace.isPrefixOf fullDeclName` does not hold.
This is not a big problem because we are planning to modify how we handle the mutual block in the future.
Note that we don't check for `localDecl.userName == givenName` here.
-/
let rec go (ns : Name) : Option LocalDecl := do
if { givenNameView with name := ns ++ givenNameView.name }.review == fullDeclName then
return localDecl
match ns with
| .str pre .. => go pre
| _ => failure
return (← go currNamespace)
/- Traverse the local context backwards looking for match `givenNameView`.
If `skipAuxDecl` we ignore `auxDecl` local declarations. -/
let findLocalDecl? (givenNameView : MacroScopesView) (skipAuxDecl : Bool) : Option LocalDecl :=
let givenName := givenNameView.review
let localDecl? := lctx.decls.findSomeRev? fun localDecl? => do
let localDecl ← localDecl?
if localDecl.isAuxDecl then
guard (!skipAuxDecl)
if let some fullDeclName := auxDeclToFullName.find? localDecl.fvarId then
matchAuxRecDecl? localDecl fullDeclName givenNameView
else
matchLocalDecl? localDecl givenName
else
matchLocalDecl? localDecl givenName
if localDecl?.isSome || skipAuxDecl then
localDecl?
else
-- Search auxDecls again trying an exact match of the given name
lctx.decls.findSomeRev? fun localDecl? => do
let localDecl ← localDecl?
guard localDecl.isAuxDecl
matchLocalDecl? localDecl givenName
/-
We use the parameter `globalDeclFound` to decide whether we should skip auxiliary declarations or not.
We set it to true if we found a global declaration `n` as we iterate over the `loop`.
Without this workaround, we would not be able to elaborate an example such as
```
def foo.aux := 1
def foo : Nat → Nat
| n => foo.aux -- should not be interpreted as `(foo).aux`
```
See test `aStructPerfIssue.lean` for another example.
We skip auxiliary declarations when `projs` is not empty and `globalDeclFound` is true.
Remark: we did not use to have the `globalDeclFound` parameter. Without this extra check we failed
to elaborate
```
example : Nat :=
let n := 0
n.succ + (m |>.succ) + m.succ
where
m := 1
```
See issue #1850.
-/
let rec loop (n : Name) (projs : List String) (globalDeclFound : Bool) := do
let givenNameView := { view with name := n }
let mut globalDeclFoundNext := globalDeclFound
unless globalDeclFound do
let r ← resolveGlobalName givenNameView.review
let r := r.filter fun (_, fieldList) => fieldList.isEmpty
unless r.isEmpty do
globalDeclFoundNext := true
/-
Note that we use `globalDeclFound` instead of `globalDeclFoundNext` in the following test.
Reason: a local should shadow a global with the same name.
Consider the following example. See issue #3079
```
def foo : Nat := 1
def bar : Nat :=
foo.add 1 -- should be 11
where
foo := 10
```
-/
match findLocalDecl? givenNameView (skipAuxDecl := globalDeclFound && !projs.isEmpty) with
| some decl => return some (decl.toExpr, projs)
| none => match n with
| .str pre s => loop pre (s::projs) globalDeclFoundNext
| _ => return none
loop view.name [] (globalDeclFound := false)
/--
Finds a name that unambiguously resolves to the given name `n₀`.
Considers suffixes of `n₀` and suffixes of aliases of `n₀` when "unresolving".
@ -402,10 +566,14 @@ When `allowHorizAliases` is false, then "horizontal aliases" (ones that are not
The assumption is that non-horizontal aliases are "API exports" (i.e., intentional exports that should be considered to be the new canonical name).
"Non-API exports" arise from (1) using `export` to add names to a namespace for dot notation or (2) projects that want names to be conveniently and permanently accessible in their own namespaces.
`filter` specifies a predicate that the unresolved name must additionally satisfy.
This function is meant to be used for pretty printing.
If `n₀` is an accessible name, then the result will be an accessible name.
-/
def unresolveNameGlobal [Monad m] [MonadResolveName m] [MonadEnv m] (n₀ : Name) (fullNames := false) (allowHorizAliases := false) : m Name := do
def unresolveNameGlobal [Monad m] [MonadResolveName m] [MonadEnv m]
(n₀ : Name) (fullNames := false) (allowHorizAliases := false)
(filter : Name → m Bool := fun _ => pure true) : m Name := do
if n₀.hasMacroScopes then return n₀
if fullNames then
match (← resolveGlobalName n₀) with
@ -428,18 +596,13 @@ where
candidate := Name.appendCore cmpt candidate
if let [(potentialMatch, _)] ← resolveGlobalName candidate then
if potentialMatch == n₀ then
return some candidate
if (← filter candidate) then
return some candidate
return none
def unresolveNameGlobalAvoidingLocals [Monad m] [MonadResolveName m] [MonadEnv m] [MonadLCtx m]
(n₀ : Name) (fullNames := false) : m Name := do
let mut n ← unresolveNameGlobal n₀ fullNames
unless (← getLCtx).usesUserName n do return n
-- `n` is also a local declaration
if n == n₀ then
-- `n` is the fully qualified name. So, we append the `_root_` prefix
return `_root_ ++ n
else
return n₀
/-- Like `Lean.unresolveNameGlobal`, but also ensures that the unresolved name does not conflict
with the names of any local declarations. -/
def unresolveNameGlobalAvoidingLocals [Monad m] [MonadResolveName m] [MonadEnv m] [MonadLCtx m] (n₀ : Name) (fullNames := false) : m Name :=
unresolveNameGlobal n₀ (fullNames := fullNames) (filter := fun n => Option.isNone <$> resolveLocalName n)
end Lean

22
tests/lean/run/6706.lean Normal file
View file

@ -0,0 +1,22 @@
/-!
# `simp?`-suggested names conflicting with auxiliary declarations
https://github.com/leanprover/lean4/issues/6706
This test ensures that "unresolved" names provided by `simp?` do not conflict with local auxiliary
declarations.
-/
def P := True
theorem N.A.B : P := trivial
/-- info: Try this: simp only [N.A.B] -/
#guard_msgs in
theorem N.X.A.B : P := by
simp? [N.A.B]
/-- info: Try this: simp only [_root_.N.A.B] -/
#guard_msgs in
theorem A : P :=
let rec N.A.B := ()
by simp? [_root_.N.A.B]
where B := ()

25
tests/lean/run/7073.lean Normal file
View file

@ -0,0 +1,25 @@
/-!
# Auxiliary declaration name resolution in tactic blocks
https://github.com/leanprover/lean4/issues/7073
It should be possible to refer to auxiliary declarations by partially- or fully-qualified names
in tactic blocks.
-/
theorem A : True ∧ True := by
let rec B := trivial
exact And.intro A.B A.C
where C := trivial
namespace M
theorem N : True ∧ True ∧ True :=
let rec O := by exact M.N.P
by exact ⟨N.O, M.N.O, N.P⟩
where P := trivial
theorem Q.R : Nat → True
| 0 => trivial
| 1 => by exact Q.R 0
| n + 2 => by exact M.Q.R (n + 1)

2
tests/lean/run/998.lean
View file

@ -2,7 +2,7 @@ import Lean
set_option maxHeartbeats 100000
attribute [simp] Array.findIdx?.loop
attribute [simp] Lean.expandExplicitBindersAux.loop
attribute [simp] Lean.Elab.Term.resolveLocalName.loop
attribute [simp] Lean.resolveLocalName.loop
-- Mathlib