Remove back-edge dependency on the K frontend

[Baltoli]

Currently, the pattern-matching compiler depends on Scala code in the K frontend to parse KORE. This induces a backwards edge in the K ecosystem dependency graph that's previously been painful to deal with.¹ As part of our general work to simplify and reorganise the K ecosystem code, we want to remove this backwards edge in the graph: runtimeverification/k#4063 (comment)

Some thoughts on how we might achieve this:

• Pull the offending code out of the frontend and into the backend directly; the frontend will then need to depend on the backend to get the parser etc.
• Extract the KORE parser Scala code as a standalone library that lives in its own repository and can be consumed as a regular Maven dependency.
• much more work, longer term do a rewrite of the matching compiler to no longer use Scala.

Footnotes

1. It doesn't happen often because the KORE language is pretty stable, but when we last made changes (related to \left-assoc and \right-assoc) it was extremely painful for a number of reasons: getting PRs merged in lockstep with each other, people's maven caches getting stale and producing confusing errors, etc. ↩

[Baltoli]

The packages that are backwards dependencies from the LLVM backend into the frontend:

org.kframework.attributes.HasLocation
org.kframework.attributes.Location
org.kframework.attributes.Source
org.kframework.kore.K
org.kframework.kore.KORE.KApply
org.kframework.kore.KORE.KList
org.kframework.mpfr._
org.kframework.parser.kore
org.kframework.parser.kore.CompoundSort
org.kframework.parser.kore.Sort
org.kframework.parser.kore.SymbolOrAlias
org.kframework.parser.kore.Variable
org.kframework.parser.kore._
org.kframework.parser.kore.implementation.{
org.kframework.parser.kore.parser.KoreToK
org.kframework.parser.kore.parser.TextToKore
org.kframework.unparser.ToKast
org.kframework.utils.errorsystem.KEMException
org.kframework.utils.errorsystem.KException

My thoughts on the various components here and what we should do with them to resolve the back edge:

• Attribute usages: we should wean the library off these data structures and just define internal ones; they're only being used as PODs as far as I can tell.
  • Remove usages of K source and location classes #1002
• KORE data structures and parser: we should pull this whole subsystem out into a separate library except KoreToK which logically needs to remain a part of the frontend. As best I can tell, the features in that package are only being used to do pretty-printing for error-handling purposes; see below.
• MPFR: this is actually an external dependency; not relevant here
• Error handling subsystem: the matching compiler should define its own error types; the frontend can then be updated to translate between the kinds of exceptions the matching compiler throws, and to plug them into the KEM infrastructure.
  • Remove usages of K error handling infrastructure #1001
  • Add translation layer from pattern matching exceptions k#4069
  • Update dependency: llvm-backend/src/main/native/llvm-backend k#4071
• Unparser / KoreToK: for code that does pretty-printing of any kind (e.g. in the exhaustiveness checker), we will need to use the new KORE-only error handling mechanism to throw an exception upwards to K such that the frontend can then translate it to KEM, and do the appropriate pretty-printing.

This is all a pretty viable set of changes to make, I think - on a first look at the set of changes required I thought it might be a trickier job than anticipated, but on a bit more inspection we can pretty easily cut the backwards edge.

[Baltoli]

I think the first step to take here is to migrate the error-handling code out of the pattern matcher, and have the frontend do translation on the errors and warnings it sees.

• In places where we're passing KExceptions into handlers, we should instead define an analogous MatchingException and pass those instead.
• In places where we throw an unrecoverable exception, we should still throw, but have the frontend catch those exception types and translate them.