Investigate KIL representation

[gtrepta]

Right now we parse definitions into KIL and then transform them into the kore structures. Is KIL still necessary?

[Baltoli]

@dwightguth: this is ancient code, and the compiler used to operate over this. The plan previously was to migrate the outer parser to generating this directly, rather than doing what we do currently. Ought to be possible to remove the KIL, but would need to match up the KIL structures with the "KORE" ones

[Baltoli]

There may be tweaks needed here and there to get things working properly.

[Baltoli]

kompile -E relies on the KIL structures to do pretty-printing; will need to change the "KORE" data structures to make sure that this behaviour is maintained.

[gtrepta]

One path to eliminating KIL could possibly be to allow pyk to do the outer parsing, after more integrations are done with #4066 and some functionality is added for the pipeline experiments

[Baltoli]

That seems like a reasonable approach to take; removing KIL from the existing frontend doesn't quite entail a full rewrite of the outer parser, but it's getting in that direction. Given that we want to be doing this with Pyk anyway, we may as well wait and just eliminate the frontend outer parser entirely in time.