Proposals for the K framework

A dump of things I've been thinking for a long time.

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.

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.

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. Have options be populated from both the command line and configuration files (along with removing their injection)

typesafe/config can a good options.

5. Replace ktest with a junit-based solution

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.

6. 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.

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

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

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

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

10. Meta-level definitions