fix: move auxDeclToFullName to LocalContext to fix name (un)resolution
#7075
Conversation
jrr6
force-pushed
the
unresolve-avoiding-local-metam
branch
from
2421ebe to
23829df
Compare
github-actions
bot
added
the
toolchain-available
leanprover-community-bot
added
the
breaks-mathlib
|
Mathlib CI status (docs):
|
| @@ -428,18 +432,8 @@ 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 | |||
There was a problem hiding this comment.
With resolveLocalName now living in MetaM, do you need the filter parameter and the separate avoidingLocals function? Why not simply always avoiding locals, for a simpler API?
There was a problem hiding this comment.
I did this to remain consistent with our current API, which has both functions (though unresolveNameGlobalAvoidingLocals isn't currently restricted to MetaM). According to #4593, this was done so that Lean.PrettyPrinter.Delaborator.delabConst can continue to use unresolveNameGlobal: in particular, there are certain circumstances in which that delaborator does not use the local-avoiding behavior (e.g., in match patterns or when pretty-printing universes). I'm not entirely certain of the rationale, but that behavior is only possible if we have a separate unresolveNameGlobal function.
There was a problem hiding this comment.
So much complexity :-)
Ok, convinced.
At this point we might auxDeclToFullName as well move into LocalContext so that unresolveNameGlobalAvoidingLocals can continue to use MonadLCtx, and resolveLocalName as well. Or an extra method to MonadLCtx. All a bit hard to decide when MetaM is the only instance of MonadLCtx :-D
There was a problem hiding this comment.
I opted for the first approach. This turned out to be a slightly more fiddly refactor than I anticipated, but now that it appears to be working, it happily resolves for free the issue I brought up in the other PR discussion: since local contexts are saved at the point of metavariable creation, the auxiliary-declaration mapping persists when we resume elaboration, so let recs and wheres resolve correctly. Also, since neither resolveLocalName nor unresolveNameGlobalAvoidingLocals depends on MetaM anymore, I've moved both of these functions to Lean.ResolveName.
One question: I noticed that the C++ code references the LocalContext type and some of its associated functions, but I'm not too familiar with that part of the code base. Is it necessary to make any changes to the kernel or runtime as a result of modifying the definition of LocalContext? (Everything seems to build and run fine as is.)
There was a problem hiding this comment.
If they reference just the functions, and not hard-coded offsets into it, it should be fine.
jrr6
changed the title
auxDeclToFullName to MetaM to fix name unresolutionauxDeclToFullName to LocalContext to fix name (un)resolution
This change fixes auxiliary-declaration name resolution in tactic blocks
jrr6
force-pushed
the
unresolve-avoiding-local-metam
branch
from
b10aa38 to
08d18d1
Compare
This PR ensures that names suggested by tactics like
simp?are not shadowed by auxiliary declarations in the local context and that names oflet recandwheredeclarations are correctly resolved in tactic blocks.This PR contains the following potentially breaking changes:
auxDeclToFullNamemap fromTermElab.ContexttoLocalContext.Lean.Elab.Term.resolveLocalName : Name → TermElabM …toLean.resolveLocalName [MonadResolveName m] [MonadEnv m] [MonadLCtx m] : Name → m ….TermElabMactionLean.Elab.Term.withAuxDeclto a monad-polymorphic actionLean.Meta.withAuxDecl.filterargument toLean.unresolveNameGlobal.Closes #6706, closes #7073.