Proposals for the K framework

1. Clean crip distinction between the meta levels

Disallow, at least at the KORE data structures level, KVariables which are KLabels. I.e., the following will not be KORE anymore:

X(1, 2, 3) => foo(X)

It would become something like:

#KApply(X, #KList(1, 2, 3))) => foo(X)

If we have the cycles, we may decide to still support the original syntax through implicit conversions.

Still under discussion.

2. Replace injections with simple direct dependencies

Instead of k-distribution hooking things through injections, it will simply depend on the projects directly. Along with this, we'll have a simple API module as the entry point to the entire tool.

Will need to have options be populated in a different way from command line.

OK from: all

3. Separate the parser from the kernel

This will allow the parser to be used independently from the rest of the tool. Other forks of K may decide to do the same. In that case, we could move the parser to its own repository.

4. Refactor ktest to make it simpler and make it easier to invoke from IntelliJ

If we have 4, this should be an easy change. We could have two test suites. A very quick one for continuous testing locally, and a larger one tested by the online integration testing tool.

If we have time, we could have the tests be configured by typesafe/config files, as a replacement for the custom junit solution.

We still need to discuss the exact solution.

OK from: Daejun, Cosmin

5. Replace Jenkins with cloud-hosted integration testing

This would free us from managing our own server. There are many options: Travis CI, Circle CI, etc.

OK from: all

6. Cut down on dependencies and publish the tool to Maven Central

OK from: all

7. Remove the current KSequence class and replace it with KApply(kSequenceLabel, ...)

The Java backend already does this. Propagate it throughout the compiler.

OK from: Andrei, Cosmin

8. Meta-level transitions for AST via explicit #up and #down

9. Meta-level definitions

10. Remove dead code from the Java backend

11. Finish the API access to the parser, compiler, and backend

12. Make quick test suite