Create a K source to AST to source tool

[Scott-Guest]

Related:

• 4222

We should consider creating a tool for round-tripping K source code to AST and back.

This serves two purposes:

• Enabling tooling for automatic migration. Breaking changes are currently feasible but tedious to implement, but automatic tooling will be needed as we develop more K semantics or introduce more involved breaking changes. For example,
  • Fixing the double escaping in regex terminals
  • The recent change replacing . with .K
    • @Baltoli reported that this was inordinately time consuming, but with the right infrastructure this could be a one-liner
  • Possibly removing unwrapped claim / implicit <k> cell insertion
• Auto-formatting K source code

[ehildenb]

pyk can definitely do this pretty easily. We can very much use kompile to read in and produce the AST, and then use pyk to read in the definition and then write it out again with a new pretty-printer. Pyk's pretty-printer would need some updating.

[ehildenb]

With some of @gtrepta work, we could probably also do it mostly in pyk, and just do inner parsing using kompile tooling.

[Scott-Guest]

@ehildenb Agreed, @Baltoli and I had similar thoughts.

There is a small gap between parsed outer syntax and the user source that we'll need to address (e.g. desugaring of inline priority declarations into a separate syntax priority statement), but it should be manageable.