Pretty-printing uniques explicitly

[effectfully]

Summary

Currently the unique of a variable is not pretty-printed with the default strategy, which I believe is in fact a bug, because parsing a pretty-printed program may get you back a different program. Not up to alpha, an actually different program. A program with a free variable is almost guaranteed to trigger this, however it doesn't need to be free for that, consider pretty-printing and parsing back \x_0 x_1 -> x_0 -- you'll get \x_0 x_1 -> x_1 back.

Now we could just pretty-print the uniques by default, but this has its own problems: it practically changes the names, because syntactically a pretty-printed unique is indistinguishable from a normal part of a name (i.e. x_0 was either the x name with the pretty-printed 0 unique or the x_0 name without a pretty-printed unique). Randomly changing names confuse people, invalidate in-memory environments and cause other kinds of disruption.

Thanks to Runtime Verification Inc. for reaching out to us regarding these issues.

Steps to reproduce the behavior

1. pretty-print the AST of \x_0 x_1 -> x_0 using the default strategy
2. parse it back

Actual Result

got a different term back

Expected Result

the resulting term is alpha-equal to the original one

Describe the approach you would take to fix this

We can solve all these problems by always pretty-printing the uniques and not making them a syntactically legal part of the textual name of the variable. For example by pretty-printing the x variable having the 0 unique as x!0 or x#0 or whatever (suggestions are welcome).

System info

Plutus: 1203fa3

[michaelpj]

We can solve all these problems by always pretty-printing the uniques and not making them a syntactically legal part of the textual name of the variable.

And by parsing this format as well, obviously.

[bezirg]

mpj wrote on SCP-817:

At the moment it doesn't, so we can't necessarily tell in our tests that we don't mix up same-named arguments.

But in order to not make the tests awful we'd want to do what we do for PLC and de-Bruijnify the terms, which would require writing a similar pass for PIR. So it's a bit of work.