search

runtimeverification / k

K Framework Tools 7.0
BSD 3-Clause "New" or "Revised" License
442 stars 145 forks source link

pyk unparser should add paranthesis when needed #4253

Open ehildenb opened 4 months ago

ehildenb commented 4 months ago

Currently when unparsing terms that could be ambiguous parses, we don't emit any paranthesis. We should somehow detect that we need to emit paranthesis, and emit them if so. An example: https://github.com/runtimeverification/k/pull/4245/files#r1567534141

In particular, the unparser that is built should track of the lowest syntax priority of teh symbols underneath it that have non-terminals on either side, and if there is one lower than the current symbol being unparsed, emit paranthesis between them.

ehildenb commented 4 months ago

Barring that, the unparser should convert to kore and use kore-print, if it supports variables. This requires certain files to be present that kore-print needs to operate, which should be guaranteed by calling kompile, but the issue is that sometimes we generate modules. If we were to generate a module that contains new syntax, kore-print will have an out-dated unparser without us writing the definition to disk, and calling kompile on it. Of course, writing the new definition to disk requires having an unparser....