Extract inner parser as a more independent tool

[Baltoli]

We are in the process of moving a lot of the current frontend's functionality into Pyk, which is a better-understood codebase with a more modern understanding of K and its various intermediate representations. Because a lot of what the frontend does is just munging ASTs between different formats, we can reimplement this in Python without any significant performance loss. This migration process is trickier for the more algorithmic, performance-sensitive parts of the frontend.

The most significant such case is the inner parser, which is responsible for parsing anything in a K definition that isn't delimited by outer syntax[^1], according to the grammar induced by a module's syntax declarations.

Currently, the inner parser is pretty tightly coupled with the rest of the frontend's compilation processes, which makes it difficult to extract as a separable component callable from Pyk. We should think about what the actual interface of the inner parser is, and how we could start this extraction process.

Some starting points to think about:

• Documentation and precise specification of the parsing process; we construct a number of derived modules from the initial "seed" input, but it's not completely obvious from the top-level documentation how these are built and used.
• Caching and up-front work; we instantiate Earley parsers and scanners when each module is used for parsing.

[^1]: We already have an implementation of an outer parser for K in Pyk; doing so is relatively simple compared to the inner parser.

[ehildenb]

We do have kast --as-rule ..., which exposes basically the rule parser, but AFAICT it also runs the compilation pipeline. So if the goal is to only run parsing, then we can have kast --as-rule ... also have an option --output-parsed SOME_FILE.json, which tells it to output the parse tree as JSON kast. This would be similar to how we output parsed.json before running the compile pipeline, and compiled.json after running the compile pipeline (when invoking kompile).

[Baltoli]

@gtrepta I believe you're working on this (i.e. exposing a tool that lets you run the inner parsing + compilation pipeline on whatever Pyk generates from its outer parser / compiled.json, then can use Pyk again for ModuleToKore)?

[gtrepta]

@Baltoli Yes, it's fair to say that. When I finish my writeup in #4131 that should be a good place to start working on a CLI option for kompile to take an outer parsed definition from pyk.