search

IntersectMBO / plutus

The Plutus language implementation and tools
Apache License 2.0
1.57k stars 479 forks source link

Pretty-printing uniques explicitly #4808

Closed effectfully closed 3 months ago

effectfully commented 2 years ago

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: 1203fa3f63db6f949af4bba889a0d0691921d2af

michaelpj commented 2 years ago

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 commented 5 months ago

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.