Best Practices for Renaming Variables in Exprs

Stream: metaprogramming / tactics

[Ernest Ng]

Hi! I was wondering what is the best way to rename variables in an Expr? Suppose I am trying to create the following pattern-match programmatically:

match n with
| Nat.succ n => do
  let x ← f n
...

In the pattern match above, the n in the pattern Nat.succ n shadows the scrutinee n, so I'd like to replace all occurrences of n in the LHSes & RHSes of the pattern match with some fresh variable n', with this being the resultant pattern-match:

match n with
| Nat.succ n' => do
  let x ← f n'
...

I am working in a codebase in which the following structure (simplified) is used to create these pattern-matches programmatically:

structure PatternMatch where
  /-- Cases (LHSes) of the pattern match -/
  matchLHSes : Array Expr

  /--  RHSes of the pattern match (Invariant: `matchLHSes.length == matchRHSes.length`) -/
  matchRHSes : Array Expr

I was wondering how to rename the variable n in the Exprs in both matchLHSes and matchRHSes in a principled way? I plan on using LocalContext.getUnusedName to produce a fresh user-accessible name, so I'm wondering whether I should just use LocalContext.renameUserName to rename n to n', or if I ought to use Expr.replaceFVar to perform the replacement directly on Exprs (the latter requires manipulating FVarIds, which I am worried about)? Thanks!

[Kyle Miller]

Just to be clear, variables themselves don't have names, due to the locally nameless encoding. Names in closed expressions are encoded in the forallE, lam, and letE expressions themselves, and for open expressions they are encoded in the LocalContext.

If you have the variables as fvars, then to make a name change all you need to do is take the current local context, create a new one from it with changed names, then use withLCtx' to enter this new context, where you build the expression.

If you are manipulating Exprs directly after the fact, you only need to modify the corresponding forallE/lam/letE to do the alpha rename.

You're right to hesitate with manipulating FVarIds. That's likely too low level, and also I'm not sure how this would rename the variables (unless you somehow have a local context with two copies of variables, one with the new name?)

[Ernest Ng]

Great, thank you so much! It looks like creating a new LocalContext and using withLCtx' to enter the new context did the trick for my example above!

[Kyle Miller]

It's possible to change types of local variables too this way too — but if you ever do this, take care! There are caches in MetaM that likely need to be cleared (withFreshCache), for example the inferType cache. Also, there is the LocalInstances cache that could need refreshing.

It's fine changing names of variables though without worrying what this will do to the caches, since the names don't affect anything in MetaM.

[Ernest Ng]

Ah good to know, thanks! I only plan on using LocalContext.renameUserName to update the LocalContext, so hopefully all the changes I'm making (i.e. renaming) are type-preserving.