search

DistCompiler / pgo

PGo is a source to source compiler from Modular PlusCal specs into Go programs.
https://distcompiler.github.io/
Apache License 2.0
174 stars 14 forks source link

Macro Expansion Bug #161

Closed shayanh closed 3 years ago

shayanh commented 3 years ago

When I try to compile the PlusCal output of the attached spec to TLA+, I got the following error:

Screen Shot 2021-09-28 at 7 15 00 PM

attached spec: https://gist.github.com/shayanh/e15896c52216d67c3301ac88e8deffc0

fhackett commented 3 years ago

I see - thanks for the bug report.

The main underlying issue is that TLA+ does not support scope shadowing... at all. If you look at the generated code, it tries to define leader twice in the same scope, which is rejected by TLC. This isn't strictly the MPCal code's fault, because there is no way to work around this in MPCal-land: there is one mapping macro definition with one name, and it can result in the "same code" being nested inside itself.

So, I'll need to be even more conservative re: renamings. The fix is to ensure that expanded mapping macros use fresh names in with-bindings.