Add an option to copy positions from old tree when doing substitutions

[jad-hamza]

[romac]

Reminder: Revert https://github.com/epfl-lara/stainless/pull/660/commits/a2f26006ca718c79381be179bfec461d986cfdae when this is released.

[samarion]

I'm not sure this really makes sense as you'll only copy the position over for the top-level substituted expression and not its children.

What is your use case? Maybe it would make more sense to use a custom transformer?

[romac]

I don’t know the specific use-/testcase Jad had in mind, but he indeed ended up using a custom transformer in https://github.com/epfl-lara/stainless/commit/a2f26006ca718c79381be179bfec461d986cfdae FYI

[jad-hamza]

Right, I needed it so that we don't lose the positions when substituting a variable with a new variable

you'll only copy the position over for the top-level substituted expression and not its children

Yes that's true, it's a bit weird having it in the general case. Should we move replaceKeepPositions from epfl-lara/stainless@a2f2600 (bad naming sorry) to Inox? (And change the signature to only replace variables with variables?)

[vkuncak]

@jad-hamza , is this still relevant? Is it for error reporting of positions?

[jad-hamza]

Yes it's useful when you're freshening variables to maintain positions. Normal substitution will substitute all variables (which are at different position) by just one instance of a variable (which has a single position).

Now that I look at my code again in Stainless, I wonder how it was supposed to work. The function is still replacing with one single instance, instead of cloning the variable.

Edit: we can close here and address this in Stainless if this function is not needed in Inox