diff --git a/.github/workflows/Dockerfile.maven-cache b/.github/workflows/Dockerfile.maven-cache
index 40fff36fc3a..968308a4fa5 100644
--- a/.github/workflows/Dockerfile.maven-cache
+++ b/.github/workflows/Dockerfile.maven-cache
@@ -23,7 +23,7 @@ ADD pom.xml /home/$USER/.tmp-
ADD llvm-backend/pom.xml /home/$USER/.tmp-maven/llvm-backend/
ADD llvm-backend/src/main/native/llvm-backend/matching/pom.xml /home/$USER/.tmp-maven/llvm-backend/src/main/native/llvm-backend/matching/
ADD haskell-backend/pom.xml /home/$USER/.tmp-maven/haskell-backend/
-ADD kernel/pom.xml /home/$USER/.tmp-maven/kernel/
+ADD k-frontend/pom.xml /home/$USER/.tmp-maven/k-frontend/
ADD k-distribution/pom.xml /home/$USER/.tmp-maven/k-distribution/
RUN cd /home/$USER/.tmp-maven && mvn --batch-mode dependency:go-offline
diff --git a/flake.nix b/flake.nix
index 715f993eff1..9efef9043ee 100644
--- a/flake.nix
+++ b/flake.nix
@@ -54,7 +54,7 @@
k-framework = { haskell-backend-bins, llvm-kompile-libs }:
prev.callPackage ./nix/k.nix {
- mvnHash = "sha256-R0lpOuz79szCLU+TaveYz5F7Lo7KtiYHJ9Nb7O2bczQ=";
+ mvnHash = "sha256-jJuIyObMoBWBLLU4hK9kt4q520D9MglyDk8Lbj+xYnE=";
manualMvnArtifacts = [
"org.scala-lang:scala-compiler:2.13.13"
"ant-contrib:ant-contrib:1.0b3"
diff --git a/haskell-backend/pom.xml b/haskell-backend/pom.xml
index b1263fc50d8..572daa1ab61 100644
--- a/haskell-backend/pom.xml
+++ b/haskell-backend/pom.xml
@@ -16,7 +16,7 @@
com.runtimeverification.k
- kernel
+ k-frontend
${project.version}
diff --git a/k-distribution/pom.xml b/k-distribution/pom.xml
index 84a422a69f7..36e64f398db 100644
--- a/k-distribution/pom.xml
+++ b/k-distribution/pom.xml
@@ -22,7 +22,7 @@
com.runtimeverification.k
- kernel
+ k-frontend
${project.version}
diff --git a/kernel/pom.xml b/k-frontend/pom.xml
similarity index 99%
rename from kernel/pom.xml
rename to k-frontend/pom.xml
index aba68ff6ed1..7d952fde02e 100644
--- a/kernel/pom.xml
+++ b/k-frontend/pom.xml
@@ -8,10 +8,10 @@
parent
1.0-SNAPSHOT
- kernel
+ k-frontend
jar
- K Framework Tool Kernel
+ K Framework Frontend
diff --git a/kernel/src/main/java/com/davekoelle/AlphanumComparator.java b/k-frontend/src/main/java/com/davekoelle/AlphanumComparator.java
similarity index 100%
rename from kernel/src/main/java/com/davekoelle/AlphanumComparator.java
rename to k-frontend/src/main/java/com/davekoelle/AlphanumComparator.java
diff --git a/kernel/src/main/java/org/kframework/List.java b/k-frontend/src/main/java/org/kframework/List.java
similarity index 100%
rename from kernel/src/main/java/org/kframework/List.java
rename to k-frontend/src/main/java/org/kframework/List.java
diff --git a/kernel/src/main/java/org/kframework/POSet.java b/k-frontend/src/main/java/org/kframework/POSet.java
similarity index 100%
rename from kernel/src/main/java/org/kframework/POSet.java
rename to k-frontend/src/main/java/org/kframework/POSet.java
diff --git a/kernel/src/main/java/org/kframework/SerializableSupplier.java b/k-frontend/src/main/java/org/kframework/SerializableSupplier.java
similarity index 100%
rename from kernel/src/main/java/org/kframework/SerializableSupplier.java
rename to k-frontend/src/main/java/org/kframework/SerializableSupplier.java
diff --git a/kernel/src/main/java/org/kframework/TopologicalSort.java b/k-frontend/src/main/java/org/kframework/TopologicalSort.java
similarity index 100%
rename from kernel/src/main/java/org/kframework/TopologicalSort.java
rename to k-frontend/src/main/java/org/kframework/TopologicalSort.java
diff --git a/kernel/src/main/java/org/kframework/attributes/HasLocation.java b/k-frontend/src/main/java/org/kframework/attributes/HasLocation.java
similarity index 100%
rename from kernel/src/main/java/org/kframework/attributes/HasLocation.java
rename to k-frontend/src/main/java/org/kframework/attributes/HasLocation.java
diff --git a/kernel/src/main/java/org/kframework/backend/Backends.java b/k-frontend/src/main/java/org/kframework/backend/Backends.java
similarity index 100%
rename from kernel/src/main/java/org/kframework/backend/Backends.java
rename to k-frontend/src/main/java/org/kframework/backend/Backends.java
diff --git a/kernel/src/main/java/org/kframework/backend/kore/ConstructorChecks.java b/k-frontend/src/main/java/org/kframework/backend/kore/ConstructorChecks.java
similarity index 100%
rename from kernel/src/main/java/org/kframework/backend/kore/ConstructorChecks.java
rename to k-frontend/src/main/java/org/kframework/backend/kore/ConstructorChecks.java
diff --git a/kernel/src/main/java/org/kframework/backend/kore/KoreBackend.java b/k-frontend/src/main/java/org/kframework/backend/kore/KoreBackend.java
similarity index 100%
rename from kernel/src/main/java/org/kframework/backend/kore/KoreBackend.java
rename to k-frontend/src/main/java/org/kframework/backend/kore/KoreBackend.java
diff --git a/kernel/src/main/java/org/kframework/backend/kore/ModuleToKORE.java b/k-frontend/src/main/java/org/kframework/backend/kore/ModuleToKORE.java
similarity index 100%
rename from kernel/src/main/java/org/kframework/backend/kore/ModuleToKORE.java
rename to k-frontend/src/main/java/org/kframework/backend/kore/ModuleToKORE.java
diff --git a/kernel/src/main/java/org/kframework/builtin/BooleanUtils.java b/k-frontend/src/main/java/org/kframework/builtin/BooleanUtils.java
similarity index 100%
rename from kernel/src/main/java/org/kframework/builtin/BooleanUtils.java
rename to k-frontend/src/main/java/org/kframework/builtin/BooleanUtils.java
diff --git a/kernel/src/main/java/org/kframework/builtin/Hooks.java b/k-frontend/src/main/java/org/kframework/builtin/Hooks.java
similarity index 100%
rename from kernel/src/main/java/org/kframework/builtin/Hooks.java
rename to k-frontend/src/main/java/org/kframework/builtin/Hooks.java
diff --git a/kernel/src/main/java/org/kframework/builtin/KLabels.java b/k-frontend/src/main/java/org/kframework/builtin/KLabels.java
similarity index 100%
rename from kernel/src/main/java/org/kframework/builtin/KLabels.java
rename to k-frontend/src/main/java/org/kframework/builtin/KLabels.java
diff --git a/kernel/src/main/java/org/kframework/compile/AddCoolLikeAtt.java b/k-frontend/src/main/java/org/kframework/compile/AddCoolLikeAtt.java
similarity index 100%
rename from kernel/src/main/java/org/kframework/compile/AddCoolLikeAtt.java
rename to k-frontend/src/main/java/org/kframework/compile/AddCoolLikeAtt.java
diff --git a/kernel/src/main/java/org/kframework/compile/AddImplicitComputationCell.java b/k-frontend/src/main/java/org/kframework/compile/AddImplicitComputationCell.java
similarity index 100%
rename from kernel/src/main/java/org/kframework/compile/AddImplicitComputationCell.java
rename to k-frontend/src/main/java/org/kframework/compile/AddImplicitComputationCell.java
diff --git a/kernel/src/main/java/org/kframework/compile/AddImplicitCounterCell.java b/k-frontend/src/main/java/org/kframework/compile/AddImplicitCounterCell.java
similarity index 100%
rename from kernel/src/main/java/org/kframework/compile/AddImplicitCounterCell.java
rename to k-frontend/src/main/java/org/kframework/compile/AddImplicitCounterCell.java
diff --git a/kernel/src/main/java/org/kframework/compile/AddParentCells.java b/k-frontend/src/main/java/org/kframework/compile/AddParentCells.java
similarity index 100%
rename from kernel/src/main/java/org/kframework/compile/AddParentCells.java
rename to k-frontend/src/main/java/org/kframework/compile/AddParentCells.java
diff --git a/kernel/src/main/java/org/kframework/compile/AddSortInjections.java b/k-frontend/src/main/java/org/kframework/compile/AddSortInjections.java
similarity index 100%
rename from kernel/src/main/java/org/kframework/compile/AddSortInjections.java
rename to k-frontend/src/main/java/org/kframework/compile/AddSortInjections.java
diff --git a/kernel/src/main/java/org/kframework/compile/AddTopCellToRules.java b/k-frontend/src/main/java/org/kframework/compile/AddTopCellToRules.java
similarity index 100%
rename from kernel/src/main/java/org/kframework/compile/AddTopCellToRules.java
rename to k-frontend/src/main/java/org/kframework/compile/AddTopCellToRules.java
diff --git a/kernel/src/main/java/org/kframework/compile/Backend.java b/k-frontend/src/main/java/org/kframework/compile/Backend.java
similarity index 100%
rename from kernel/src/main/java/org/kframework/compile/Backend.java
rename to k-frontend/src/main/java/org/kframework/compile/Backend.java
diff --git a/kernel/src/main/java/org/kframework/compile/CloseCells.java b/k-frontend/src/main/java/org/kframework/compile/CloseCells.java
similarity index 100%
rename from kernel/src/main/java/org/kframework/compile/CloseCells.java
rename to k-frontend/src/main/java/org/kframework/compile/CloseCells.java
diff --git a/kernel/src/main/java/org/kframework/compile/ComputeTransitiveFunctionDependencies.java b/k-frontend/src/main/java/org/kframework/compile/ComputeTransitiveFunctionDependencies.java
similarity index 100%
rename from kernel/src/main/java/org/kframework/compile/ComputeTransitiveFunctionDependencies.java
rename to k-frontend/src/main/java/org/kframework/compile/ComputeTransitiveFunctionDependencies.java
diff --git a/kernel/src/main/java/org/kframework/compile/ConcretizationInfo.java b/k-frontend/src/main/java/org/kframework/compile/ConcretizationInfo.java
similarity index 100%
rename from kernel/src/main/java/org/kframework/compile/ConcretizationInfo.java
rename to k-frontend/src/main/java/org/kframework/compile/ConcretizationInfo.java
diff --git a/kernel/src/main/java/org/kframework/compile/ConcretizeCells.java b/k-frontend/src/main/java/org/kframework/compile/ConcretizeCells.java
similarity index 100%
rename from kernel/src/main/java/org/kframework/compile/ConcretizeCells.java
rename to k-frontend/src/main/java/org/kframework/compile/ConcretizeCells.java
diff --git a/kernel/src/main/java/org/kframework/compile/ConfigurationInfo.java b/k-frontend/src/main/java/org/kframework/compile/ConfigurationInfo.java
similarity index 100%
rename from kernel/src/main/java/org/kframework/compile/ConfigurationInfo.java
rename to k-frontend/src/main/java/org/kframework/compile/ConfigurationInfo.java
diff --git a/kernel/src/main/java/org/kframework/compile/ConstantFolding.java b/k-frontend/src/main/java/org/kframework/compile/ConstantFolding.java
similarity index 100%
rename from kernel/src/main/java/org/kframework/compile/ConstantFolding.java
rename to k-frontend/src/main/java/org/kframework/compile/ConstantFolding.java
diff --git a/kernel/src/main/java/org/kframework/compile/ConvertDataStructureToLookup.java b/k-frontend/src/main/java/org/kframework/compile/ConvertDataStructureToLookup.java
similarity index 100%
rename from kernel/src/main/java/org/kframework/compile/ConvertDataStructureToLookup.java
rename to k-frontend/src/main/java/org/kframework/compile/ConvertDataStructureToLookup.java
diff --git a/kernel/src/main/java/org/kframework/compile/ExpandMacros.java b/k-frontend/src/main/java/org/kframework/compile/ExpandMacros.java
similarity index 100%
rename from kernel/src/main/java/org/kframework/compile/ExpandMacros.java
rename to k-frontend/src/main/java/org/kframework/compile/ExpandMacros.java
diff --git a/kernel/src/main/java/org/kframework/compile/FloatBuiltin.java b/k-frontend/src/main/java/org/kframework/compile/FloatBuiltin.java
similarity index 100%
rename from kernel/src/main/java/org/kframework/compile/FloatBuiltin.java
rename to k-frontend/src/main/java/org/kframework/compile/FloatBuiltin.java
diff --git a/kernel/src/main/java/org/kframework/compile/GatherVarsVisitor.java b/k-frontend/src/main/java/org/kframework/compile/GatherVarsVisitor.java
similarity index 100%
rename from kernel/src/main/java/org/kframework/compile/GatherVarsVisitor.java
rename to k-frontend/src/main/java/org/kframework/compile/GatherVarsVisitor.java
diff --git a/kernel/src/main/java/org/kframework/compile/GenerateCoverage.java b/k-frontend/src/main/java/org/kframework/compile/GenerateCoverage.java
similarity index 100%
rename from kernel/src/main/java/org/kframework/compile/GenerateCoverage.java
rename to k-frontend/src/main/java/org/kframework/compile/GenerateCoverage.java
diff --git a/kernel/src/main/java/org/kframework/compile/GenerateSentencesFromConfigDecl.java b/k-frontend/src/main/java/org/kframework/compile/GenerateSentencesFromConfigDecl.java
similarity index 100%
rename from kernel/src/main/java/org/kframework/compile/GenerateSentencesFromConfigDecl.java
rename to k-frontend/src/main/java/org/kframework/compile/GenerateSentencesFromConfigDecl.java
diff --git a/kernel/src/main/java/org/kframework/compile/GenerateSortPredicateRules.java b/k-frontend/src/main/java/org/kframework/compile/GenerateSortPredicateRules.java
similarity index 100%
rename from kernel/src/main/java/org/kframework/compile/GenerateSortPredicateRules.java
rename to k-frontend/src/main/java/org/kframework/compile/GenerateSortPredicateRules.java
diff --git a/kernel/src/main/java/org/kframework/compile/GenerateSortPredicateSyntax.java b/k-frontend/src/main/java/org/kframework/compile/GenerateSortPredicateSyntax.java
similarity index 100%
rename from kernel/src/main/java/org/kframework/compile/GenerateSortPredicateSyntax.java
rename to k-frontend/src/main/java/org/kframework/compile/GenerateSortPredicateSyntax.java
diff --git a/kernel/src/main/java/org/kframework/compile/GenerateSortProjections.java b/k-frontend/src/main/java/org/kframework/compile/GenerateSortProjections.java
similarity index 100%
rename from kernel/src/main/java/org/kframework/compile/GenerateSortProjections.java
rename to k-frontend/src/main/java/org/kframework/compile/GenerateSortProjections.java
diff --git a/kernel/src/main/java/org/kframework/compile/GuardOrPatterns.java b/k-frontend/src/main/java/org/kframework/compile/GuardOrPatterns.java
similarity index 100%
rename from kernel/src/main/java/org/kframework/compile/GuardOrPatterns.java
rename to k-frontend/src/main/java/org/kframework/compile/GuardOrPatterns.java
diff --git a/kernel/src/main/java/org/kframework/compile/IncompleteCellUtils.java b/k-frontend/src/main/java/org/kframework/compile/IncompleteCellUtils.java
similarity index 100%
rename from kernel/src/main/java/org/kframework/compile/IncompleteCellUtils.java
rename to k-frontend/src/main/java/org/kframework/compile/IncompleteCellUtils.java
diff --git a/kernel/src/main/java/org/kframework/compile/LabelInfo.java b/k-frontend/src/main/java/org/kframework/compile/LabelInfo.java
similarity index 100%
rename from kernel/src/main/java/org/kframework/compile/LabelInfo.java
rename to k-frontend/src/main/java/org/kframework/compile/LabelInfo.java
diff --git a/kernel/src/main/java/org/kframework/compile/MinimizeTermConstruction.java b/k-frontend/src/main/java/org/kframework/compile/MinimizeTermConstruction.java
similarity index 100%
rename from kernel/src/main/java/org/kframework/compile/MinimizeTermConstruction.java
rename to k-frontend/src/main/java/org/kframework/compile/MinimizeTermConstruction.java
diff --git a/kernel/src/main/java/org/kframework/compile/NormalizeVariables.java b/k-frontend/src/main/java/org/kframework/compile/NormalizeVariables.java
similarity index 100%
rename from kernel/src/main/java/org/kframework/compile/NormalizeVariables.java
rename to k-frontend/src/main/java/org/kframework/compile/NormalizeVariables.java
diff --git a/kernel/src/main/java/org/kframework/compile/NumberSentences.java b/k-frontend/src/main/java/org/kframework/compile/NumberSentences.java
similarity index 100%
rename from kernel/src/main/java/org/kframework/compile/NumberSentences.java
rename to k-frontend/src/main/java/org/kframework/compile/NumberSentences.java
diff --git a/kernel/src/main/java/org/kframework/compile/PatternValueAwareVisitor.java b/k-frontend/src/main/java/org/kframework/compile/PatternValueAwareVisitor.java
similarity index 100%
rename from kernel/src/main/java/org/kframework/compile/PatternValueAwareVisitor.java
rename to k-frontend/src/main/java/org/kframework/compile/PatternValueAwareVisitor.java
diff --git a/kernel/src/main/java/org/kframework/compile/PropagateMacro.java b/k-frontend/src/main/java/org/kframework/compile/PropagateMacro.java
similarity index 100%
rename from kernel/src/main/java/org/kframework/compile/PropagateMacro.java
rename to k-frontend/src/main/java/org/kframework/compile/PropagateMacro.java
diff --git a/kernel/src/main/java/org/kframework/compile/RefreshRules.java b/k-frontend/src/main/java/org/kframework/compile/RefreshRules.java
similarity index 100%
rename from kernel/src/main/java/org/kframework/compile/RefreshRules.java
rename to k-frontend/src/main/java/org/kframework/compile/RefreshRules.java
diff --git a/kernel/src/main/java/org/kframework/compile/RemoveUnit.java b/k-frontend/src/main/java/org/kframework/compile/RemoveUnit.java
similarity index 100%
rename from kernel/src/main/java/org/kframework/compile/RemoveUnit.java
rename to k-frontend/src/main/java/org/kframework/compile/RemoveUnit.java
diff --git a/kernel/src/main/java/org/kframework/compile/ResolveAnonVar.java b/k-frontend/src/main/java/org/kframework/compile/ResolveAnonVar.java
similarity index 100%
rename from kernel/src/main/java/org/kframework/compile/ResolveAnonVar.java
rename to k-frontend/src/main/java/org/kframework/compile/ResolveAnonVar.java
diff --git a/kernel/src/main/java/org/kframework/compile/ResolveComm.java b/k-frontend/src/main/java/org/kframework/compile/ResolveComm.java
similarity index 100%
rename from kernel/src/main/java/org/kframework/compile/ResolveComm.java
rename to k-frontend/src/main/java/org/kframework/compile/ResolveComm.java
diff --git a/kernel/src/main/java/org/kframework/compile/ResolveContexts.java b/k-frontend/src/main/java/org/kframework/compile/ResolveContexts.java
similarity index 100%
rename from kernel/src/main/java/org/kframework/compile/ResolveContexts.java
rename to k-frontend/src/main/java/org/kframework/compile/ResolveContexts.java
diff --git a/kernel/src/main/java/org/kframework/compile/ResolveFreshConfigConstants.java b/k-frontend/src/main/java/org/kframework/compile/ResolveFreshConfigConstants.java
similarity index 100%
rename from kernel/src/main/java/org/kframework/compile/ResolveFreshConfigConstants.java
rename to k-frontend/src/main/java/org/kframework/compile/ResolveFreshConfigConstants.java
diff --git a/kernel/src/main/java/org/kframework/compile/ResolveFreshConstants.java b/k-frontend/src/main/java/org/kframework/compile/ResolveFreshConstants.java
similarity index 100%
rename from kernel/src/main/java/org/kframework/compile/ResolveFreshConstants.java
rename to k-frontend/src/main/java/org/kframework/compile/ResolveFreshConstants.java
diff --git a/kernel/src/main/java/org/kframework/compile/ResolveFun.java b/k-frontend/src/main/java/org/kframework/compile/ResolveFun.java
similarity index 100%
rename from kernel/src/main/java/org/kframework/compile/ResolveFun.java
rename to k-frontend/src/main/java/org/kframework/compile/ResolveFun.java
diff --git a/kernel/src/main/java/org/kframework/compile/ResolveFunctionWithConfig.java b/k-frontend/src/main/java/org/kframework/compile/ResolveFunctionWithConfig.java
similarity index 100%
rename from kernel/src/main/java/org/kframework/compile/ResolveFunctionWithConfig.java
rename to k-frontend/src/main/java/org/kframework/compile/ResolveFunctionWithConfig.java
diff --git a/kernel/src/main/java/org/kframework/compile/ResolveHeatCoolAttribute.java b/k-frontend/src/main/java/org/kframework/compile/ResolveHeatCoolAttribute.java
similarity index 100%
rename from kernel/src/main/java/org/kframework/compile/ResolveHeatCoolAttribute.java
rename to k-frontend/src/main/java/org/kframework/compile/ResolveHeatCoolAttribute.java
diff --git a/kernel/src/main/java/org/kframework/compile/ResolveIOStreams.java b/k-frontend/src/main/java/org/kframework/compile/ResolveIOStreams.java
similarity index 100%
rename from kernel/src/main/java/org/kframework/compile/ResolveIOStreams.java
rename to k-frontend/src/main/java/org/kframework/compile/ResolveIOStreams.java
diff --git a/kernel/src/main/java/org/kframework/compile/ResolveSemanticCasts.java b/k-frontend/src/main/java/org/kframework/compile/ResolveSemanticCasts.java
similarity index 100%
rename from kernel/src/main/java/org/kframework/compile/ResolveSemanticCasts.java
rename to k-frontend/src/main/java/org/kframework/compile/ResolveSemanticCasts.java
diff --git a/kernel/src/main/java/org/kframework/compile/ResolveStrict.java b/k-frontend/src/main/java/org/kframework/compile/ResolveStrict.java
similarity index 100%
rename from kernel/src/main/java/org/kframework/compile/ResolveStrict.java
rename to k-frontend/src/main/java/org/kframework/compile/ResolveStrict.java
diff --git a/kernel/src/main/java/org/kframework/compile/RewriteAwareTransformer.java b/k-frontend/src/main/java/org/kframework/compile/RewriteAwareTransformer.java
similarity index 100%
rename from kernel/src/main/java/org/kframework/compile/RewriteAwareTransformer.java
rename to k-frontend/src/main/java/org/kframework/compile/RewriteAwareTransformer.java
diff --git a/kernel/src/main/java/org/kframework/compile/RewriteAwareVisitor.java b/k-frontend/src/main/java/org/kframework/compile/RewriteAwareVisitor.java
similarity index 100%
rename from kernel/src/main/java/org/kframework/compile/RewriteAwareVisitor.java
rename to k-frontend/src/main/java/org/kframework/compile/RewriteAwareVisitor.java
diff --git a/kernel/src/main/java/org/kframework/compile/SortCells.java b/k-frontend/src/main/java/org/kframework/compile/SortCells.java
similarity index 100%
rename from kernel/src/main/java/org/kframework/compile/SortCells.java
rename to k-frontend/src/main/java/org/kframework/compile/SortCells.java
diff --git a/kernel/src/main/java/org/kframework/compile/SortInfo.java b/k-frontend/src/main/java/org/kframework/compile/SortInfo.java
similarity index 100%
rename from kernel/src/main/java/org/kframework/compile/SortInfo.java
rename to k-frontend/src/main/java/org/kframework/compile/SortInfo.java
diff --git a/kernel/src/main/java/org/kframework/compile/checks/CheckAnonymous.java b/k-frontend/src/main/java/org/kframework/compile/checks/CheckAnonymous.java
similarity index 100%
rename from kernel/src/main/java/org/kframework/compile/checks/CheckAnonymous.java
rename to k-frontend/src/main/java/org/kframework/compile/checks/CheckAnonymous.java
diff --git a/kernel/src/main/java/org/kframework/compile/checks/CheckAssoc.java b/k-frontend/src/main/java/org/kframework/compile/checks/CheckAssoc.java
similarity index 100%
rename from kernel/src/main/java/org/kframework/compile/checks/CheckAssoc.java
rename to k-frontend/src/main/java/org/kframework/compile/checks/CheckAssoc.java
diff --git a/kernel/src/main/java/org/kframework/compile/checks/CheckAtt.java b/k-frontend/src/main/java/org/kframework/compile/checks/CheckAtt.java
similarity index 100%
rename from kernel/src/main/java/org/kframework/compile/checks/CheckAtt.java
rename to k-frontend/src/main/java/org/kframework/compile/checks/CheckAtt.java
diff --git a/kernel/src/main/java/org/kframework/compile/checks/CheckBracket.java b/k-frontend/src/main/java/org/kframework/compile/checks/CheckBracket.java
similarity index 100%
rename from kernel/src/main/java/org/kframework/compile/checks/CheckBracket.java
rename to k-frontend/src/main/java/org/kframework/compile/checks/CheckBracket.java
diff --git a/kernel/src/main/java/org/kframework/compile/checks/CheckConfigurationCells.java b/k-frontend/src/main/java/org/kframework/compile/checks/CheckConfigurationCells.java
similarity index 100%
rename from kernel/src/main/java/org/kframework/compile/checks/CheckConfigurationCells.java
rename to k-frontend/src/main/java/org/kframework/compile/checks/CheckConfigurationCells.java
diff --git a/kernel/src/main/java/org/kframework/compile/checks/CheckDeprecated.java b/k-frontend/src/main/java/org/kframework/compile/checks/CheckDeprecated.java
similarity index 100%
rename from kernel/src/main/java/org/kframework/compile/checks/CheckDeprecated.java
rename to k-frontend/src/main/java/org/kframework/compile/checks/CheckDeprecated.java
diff --git a/kernel/src/main/java/org/kframework/compile/checks/CheckFunctions.java b/k-frontend/src/main/java/org/kframework/compile/checks/CheckFunctions.java
similarity index 100%
rename from kernel/src/main/java/org/kframework/compile/checks/CheckFunctions.java
rename to k-frontend/src/main/java/org/kframework/compile/checks/CheckFunctions.java
diff --git a/kernel/src/main/java/org/kframework/compile/checks/CheckHOLE.java b/k-frontend/src/main/java/org/kframework/compile/checks/CheckHOLE.java
similarity index 100%
rename from kernel/src/main/java/org/kframework/compile/checks/CheckHOLE.java
rename to k-frontend/src/main/java/org/kframework/compile/checks/CheckHOLE.java
diff --git a/kernel/src/main/java/org/kframework/compile/checks/CheckK.java b/k-frontend/src/main/java/org/kframework/compile/checks/CheckK.java
similarity index 100%
rename from kernel/src/main/java/org/kframework/compile/checks/CheckK.java
rename to k-frontend/src/main/java/org/kframework/compile/checks/CheckK.java
diff --git a/kernel/src/main/java/org/kframework/compile/checks/CheckKLabels.java b/k-frontend/src/main/java/org/kframework/compile/checks/CheckKLabels.java
similarity index 100%
rename from kernel/src/main/java/org/kframework/compile/checks/CheckKLabels.java
rename to k-frontend/src/main/java/org/kframework/compile/checks/CheckKLabels.java
diff --git a/kernel/src/main/java/org/kframework/compile/checks/CheckLabels.java b/k-frontend/src/main/java/org/kframework/compile/checks/CheckLabels.java
similarity index 100%
rename from kernel/src/main/java/org/kframework/compile/checks/CheckLabels.java
rename to k-frontend/src/main/java/org/kframework/compile/checks/CheckLabels.java
diff --git a/kernel/src/main/java/org/kframework/compile/checks/CheckListDecl.java b/k-frontend/src/main/java/org/kframework/compile/checks/CheckListDecl.java
similarity index 100%
rename from kernel/src/main/java/org/kframework/compile/checks/CheckListDecl.java
rename to k-frontend/src/main/java/org/kframework/compile/checks/CheckListDecl.java
diff --git a/kernel/src/main/java/org/kframework/compile/checks/CheckRHSVariables.java b/k-frontend/src/main/java/org/kframework/compile/checks/CheckRHSVariables.java
similarity index 100%
rename from kernel/src/main/java/org/kframework/compile/checks/CheckRHSVariables.java
rename to k-frontend/src/main/java/org/kframework/compile/checks/CheckRHSVariables.java
diff --git a/kernel/src/main/java/org/kframework/compile/checks/CheckRewrite.java b/k-frontend/src/main/java/org/kframework/compile/checks/CheckRewrite.java
similarity index 100%
rename from kernel/src/main/java/org/kframework/compile/checks/CheckRewrite.java
rename to k-frontend/src/main/java/org/kframework/compile/checks/CheckRewrite.java
diff --git a/kernel/src/main/java/org/kframework/compile/checks/CheckSmtLemmas.java b/k-frontend/src/main/java/org/kframework/compile/checks/CheckSmtLemmas.java
similarity index 100%
rename from kernel/src/main/java/org/kframework/compile/checks/CheckSmtLemmas.java
rename to k-frontend/src/main/java/org/kframework/compile/checks/CheckSmtLemmas.java
diff --git a/kernel/src/main/java/org/kframework/compile/checks/CheckSortTopUniqueness.java b/k-frontend/src/main/java/org/kframework/compile/checks/CheckSortTopUniqueness.java
similarity index 100%
rename from kernel/src/main/java/org/kframework/compile/checks/CheckSortTopUniqueness.java
rename to k-frontend/src/main/java/org/kframework/compile/checks/CheckSortTopUniqueness.java
diff --git a/kernel/src/main/java/org/kframework/compile/checks/CheckStreams.java b/k-frontend/src/main/java/org/kframework/compile/checks/CheckStreams.java
similarity index 100%
rename from kernel/src/main/java/org/kframework/compile/checks/CheckStreams.java
rename to k-frontend/src/main/java/org/kframework/compile/checks/CheckStreams.java
diff --git a/kernel/src/main/java/org/kframework/compile/checks/CheckSyntaxGroups.java b/k-frontend/src/main/java/org/kframework/compile/checks/CheckSyntaxGroups.java
similarity index 100%
rename from kernel/src/main/java/org/kframework/compile/checks/CheckSyntaxGroups.java
rename to k-frontend/src/main/java/org/kframework/compile/checks/CheckSyntaxGroups.java
diff --git a/kernel/src/main/java/org/kframework/compile/checks/CheckTokens.java b/k-frontend/src/main/java/org/kframework/compile/checks/CheckTokens.java
similarity index 100%
rename from kernel/src/main/java/org/kframework/compile/checks/CheckTokens.java
rename to k-frontend/src/main/java/org/kframework/compile/checks/CheckTokens.java
diff --git a/kernel/src/main/java/org/kframework/compile/checks/ComputeUnboundVariables.java b/k-frontend/src/main/java/org/kframework/compile/checks/ComputeUnboundVariables.java
similarity index 100%
rename from kernel/src/main/java/org/kframework/compile/checks/ComputeUnboundVariables.java
rename to k-frontend/src/main/java/org/kframework/compile/checks/ComputeUnboundVariables.java
diff --git a/kernel/src/main/java/org/kframework/definition/Associativity.java b/k-frontend/src/main/java/org/kframework/definition/Associativity.java
similarity index 100%
rename from kernel/src/main/java/org/kframework/definition/Associativity.java
rename to k-frontend/src/main/java/org/kframework/definition/Associativity.java
diff --git a/kernel/src/main/java/org/kframework/definition/UserList.java b/k-frontend/src/main/java/org/kframework/definition/UserList.java
similarity index 100%
rename from kernel/src/main/java/org/kframework/definition/UserList.java
rename to k-frontend/src/main/java/org/kframework/definition/UserList.java
diff --git a/kernel/src/main/java/org/kframework/kast/KastFrontEnd.java b/k-frontend/src/main/java/org/kframework/kast/KastFrontEnd.java
similarity index 100%
rename from kernel/src/main/java/org/kframework/kast/KastFrontEnd.java
rename to k-frontend/src/main/java/org/kframework/kast/KastFrontEnd.java
diff --git a/kernel/src/main/java/org/kframework/kast/KastModule.java b/k-frontend/src/main/java/org/kframework/kast/KastModule.java
similarity index 100%
rename from kernel/src/main/java/org/kframework/kast/KastModule.java
rename to k-frontend/src/main/java/org/kframework/kast/KastModule.java
diff --git a/kernel/src/main/java/org/kframework/kast/KastOptions.java b/k-frontend/src/main/java/org/kframework/kast/KastOptions.java
similarity index 100%
rename from kernel/src/main/java/org/kframework/kast/KastOptions.java
rename to k-frontend/src/main/java/org/kframework/kast/KastOptions.java
diff --git a/kernel/src/main/java/org/kframework/kdep/KDepFrontEnd.java b/k-frontend/src/main/java/org/kframework/kdep/KDepFrontEnd.java
similarity index 100%
rename from kernel/src/main/java/org/kframework/kdep/KDepFrontEnd.java
rename to k-frontend/src/main/java/org/kframework/kdep/KDepFrontEnd.java
diff --git a/kernel/src/main/java/org/kframework/kdep/KDepModule.java b/k-frontend/src/main/java/org/kframework/kdep/KDepModule.java
similarity index 100%
rename from kernel/src/main/java/org/kframework/kdep/KDepModule.java
rename to k-frontend/src/main/java/org/kframework/kdep/KDepModule.java
diff --git a/kernel/src/main/java/org/kframework/kdep/KDepOptions.java b/k-frontend/src/main/java/org/kframework/kdep/KDepOptions.java
similarity index 100%
rename from kernel/src/main/java/org/kframework/kdep/KDepOptions.java
rename to k-frontend/src/main/java/org/kframework/kdep/KDepOptions.java
diff --git a/kernel/src/main/java/org/kframework/kil/ASTNode.java b/k-frontend/src/main/java/org/kframework/kil/ASTNode.java
similarity index 100%
rename from kernel/src/main/java/org/kframework/kil/ASTNode.java
rename to k-frontend/src/main/java/org/kframework/kil/ASTNode.java
diff --git a/kernel/src/main/java/org/kframework/kil/Definition.java b/k-frontend/src/main/java/org/kframework/kil/Definition.java
similarity index 100%
rename from kernel/src/main/java/org/kframework/kil/Definition.java
rename to k-frontend/src/main/java/org/kframework/kil/Definition.java
diff --git a/kernel/src/main/java/org/kframework/kil/DefinitionItem.java b/k-frontend/src/main/java/org/kframework/kil/DefinitionItem.java
similarity index 100%
rename from kernel/src/main/java/org/kframework/kil/DefinitionItem.java
rename to k-frontend/src/main/java/org/kframework/kil/DefinitionItem.java
diff --git a/kernel/src/main/java/org/kframework/kil/Import.java b/k-frontend/src/main/java/org/kframework/kil/Import.java
similarity index 100%
rename from kernel/src/main/java/org/kframework/kil/Import.java
rename to k-frontend/src/main/java/org/kframework/kil/Import.java
diff --git a/kernel/src/main/java/org/kframework/kil/Lexical.java b/k-frontend/src/main/java/org/kframework/kil/Lexical.java
similarity index 100%
rename from kernel/src/main/java/org/kframework/kil/Lexical.java
rename to k-frontend/src/main/java/org/kframework/kil/Lexical.java
diff --git a/kernel/src/main/java/org/kframework/kil/Module.java b/k-frontend/src/main/java/org/kframework/kil/Module.java
similarity index 100%
rename from kernel/src/main/java/org/kframework/kil/Module.java
rename to k-frontend/src/main/java/org/kframework/kil/Module.java
diff --git a/kernel/src/main/java/org/kframework/kil/ModuleItem.java b/k-frontend/src/main/java/org/kframework/kil/ModuleItem.java
similarity index 100%
rename from kernel/src/main/java/org/kframework/kil/ModuleItem.java
rename to k-frontend/src/main/java/org/kframework/kil/ModuleItem.java
diff --git a/kernel/src/main/java/org/kframework/kil/NonTerminal.java b/k-frontend/src/main/java/org/kframework/kil/NonTerminal.java
similarity index 100%
rename from kernel/src/main/java/org/kframework/kil/NonTerminal.java
rename to k-frontend/src/main/java/org/kframework/kil/NonTerminal.java
diff --git a/kernel/src/main/java/org/kframework/kil/PriorityBlock.java b/k-frontend/src/main/java/org/kframework/kil/PriorityBlock.java
similarity index 100%
rename from kernel/src/main/java/org/kframework/kil/PriorityBlock.java
rename to k-frontend/src/main/java/org/kframework/kil/PriorityBlock.java
diff --git a/kernel/src/main/java/org/kframework/kil/PriorityBlockExtended.java b/k-frontend/src/main/java/org/kframework/kil/PriorityBlockExtended.java
similarity index 100%
rename from kernel/src/main/java/org/kframework/kil/PriorityBlockExtended.java
rename to k-frontend/src/main/java/org/kframework/kil/PriorityBlockExtended.java
diff --git a/kernel/src/main/java/org/kframework/kil/PriorityExtended.java b/k-frontend/src/main/java/org/kframework/kil/PriorityExtended.java
similarity index 100%
rename from kernel/src/main/java/org/kframework/kil/PriorityExtended.java
rename to k-frontend/src/main/java/org/kframework/kil/PriorityExtended.java
diff --git a/kernel/src/main/java/org/kframework/kil/PriorityExtendedAssoc.java b/k-frontend/src/main/java/org/kframework/kil/PriorityExtendedAssoc.java
similarity index 100%
rename from kernel/src/main/java/org/kframework/kil/PriorityExtendedAssoc.java
rename to k-frontend/src/main/java/org/kframework/kil/PriorityExtendedAssoc.java
diff --git a/kernel/src/main/java/org/kframework/kil/Production.java b/k-frontend/src/main/java/org/kframework/kil/Production.java
similarity index 100%
rename from kernel/src/main/java/org/kframework/kil/Production.java
rename to k-frontend/src/main/java/org/kframework/kil/Production.java
diff --git a/kernel/src/main/java/org/kframework/kil/ProductionItem.java b/k-frontend/src/main/java/org/kframework/kil/ProductionItem.java
similarity index 100%
rename from kernel/src/main/java/org/kframework/kil/ProductionItem.java
rename to k-frontend/src/main/java/org/kframework/kil/ProductionItem.java
diff --git a/kernel/src/main/java/org/kframework/kil/Require.java b/k-frontend/src/main/java/org/kframework/kil/Require.java
similarity index 100%
rename from kernel/src/main/java/org/kframework/kil/Require.java
rename to k-frontend/src/main/java/org/kframework/kil/Require.java
diff --git a/kernel/src/main/java/org/kframework/kil/SortSynonym.java b/k-frontend/src/main/java/org/kframework/kil/SortSynonym.java
similarity index 100%
rename from kernel/src/main/java/org/kframework/kil/SortSynonym.java
rename to k-frontend/src/main/java/org/kframework/kil/SortSynonym.java
diff --git a/kernel/src/main/java/org/kframework/kil/StringSentence.java b/k-frontend/src/main/java/org/kframework/kil/StringSentence.java
similarity index 100%
rename from kernel/src/main/java/org/kframework/kil/StringSentence.java
rename to k-frontend/src/main/java/org/kframework/kil/StringSentence.java
diff --git a/kernel/src/main/java/org/kframework/kil/Syntax.java b/k-frontend/src/main/java/org/kframework/kil/Syntax.java
similarity index 100%
rename from kernel/src/main/java/org/kframework/kil/Syntax.java
rename to k-frontend/src/main/java/org/kframework/kil/Syntax.java
diff --git a/kernel/src/main/java/org/kframework/kil/SyntaxLexical.java b/k-frontend/src/main/java/org/kframework/kil/SyntaxLexical.java
similarity index 100%
rename from kernel/src/main/java/org/kframework/kil/SyntaxLexical.java
rename to k-frontend/src/main/java/org/kframework/kil/SyntaxLexical.java
diff --git a/kernel/src/main/java/org/kframework/kil/Terminal.java b/k-frontend/src/main/java/org/kframework/kil/Terminal.java
similarity index 100%
rename from kernel/src/main/java/org/kframework/kil/Terminal.java
rename to k-frontend/src/main/java/org/kframework/kil/Terminal.java
diff --git a/kernel/src/main/java/org/kframework/kil/UserList.java b/k-frontend/src/main/java/org/kframework/kil/UserList.java
similarity index 100%
rename from kernel/src/main/java/org/kframework/kil/UserList.java
rename to k-frontend/src/main/java/org/kframework/kil/UserList.java
diff --git a/kernel/src/main/java/org/kframework/kil/loader/Context.java b/k-frontend/src/main/java/org/kframework/kil/loader/Context.java
similarity index 100%
rename from kernel/src/main/java/org/kframework/kil/loader/Context.java
rename to k-frontend/src/main/java/org/kframework/kil/loader/Context.java
diff --git a/kernel/src/main/java/org/kframework/kompile/BackendModule.java b/k-frontend/src/main/java/org/kframework/kompile/BackendModule.java
similarity index 100%
rename from kernel/src/main/java/org/kframework/kompile/BackendModule.java
rename to k-frontend/src/main/java/org/kframework/kompile/BackendModule.java
diff --git a/kernel/src/main/java/org/kframework/kompile/CompiledDefinition.java b/k-frontend/src/main/java/org/kframework/kompile/CompiledDefinition.java
similarity index 100%
rename from kernel/src/main/java/org/kframework/kompile/CompiledDefinition.java
rename to k-frontend/src/main/java/org/kframework/kompile/CompiledDefinition.java
diff --git a/kernel/src/main/java/org/kframework/kompile/DefinitionParsing.java b/k-frontend/src/main/java/org/kframework/kompile/DefinitionParsing.java
similarity index 100%
rename from kernel/src/main/java/org/kframework/kompile/DefinitionParsing.java
rename to k-frontend/src/main/java/org/kframework/kompile/DefinitionParsing.java
diff --git a/kernel/src/main/java/org/kframework/kompile/Kompile.java b/k-frontend/src/main/java/org/kframework/kompile/Kompile.java
similarity index 100%
rename from kernel/src/main/java/org/kframework/kompile/Kompile.java
rename to k-frontend/src/main/java/org/kframework/kompile/Kompile.java
diff --git a/kernel/src/main/java/org/kframework/kompile/KompileFrontEnd.java b/k-frontend/src/main/java/org/kframework/kompile/KompileFrontEnd.java
similarity index 100%
rename from kernel/src/main/java/org/kframework/kompile/KompileFrontEnd.java
rename to k-frontend/src/main/java/org/kframework/kompile/KompileFrontEnd.java
diff --git a/kernel/src/main/java/org/kframework/kompile/KompileModule.java b/k-frontend/src/main/java/org/kframework/kompile/KompileModule.java
similarity index 100%
rename from kernel/src/main/java/org/kframework/kompile/KompileModule.java
rename to k-frontend/src/main/java/org/kframework/kompile/KompileModule.java
diff --git a/kernel/src/main/java/org/kframework/kompile/KompileOptions.java b/k-frontend/src/main/java/org/kframework/kompile/KompileOptions.java
similarity index 100%
rename from kernel/src/main/java/org/kframework/kompile/KompileOptions.java
rename to k-frontend/src/main/java/org/kframework/kompile/KompileOptions.java
diff --git a/kernel/src/main/java/org/kframework/kompile/KompileUsageFormatter.java b/k-frontend/src/main/java/org/kframework/kompile/KompileUsageFormatter.java
similarity index 100%
rename from kernel/src/main/java/org/kframework/kompile/KompileUsageFormatter.java
rename to k-frontend/src/main/java/org/kframework/kompile/KompileUsageFormatter.java
diff --git a/kernel/src/main/java/org/kframework/kore/AddAtt.java b/k-frontend/src/main/java/org/kframework/kore/AddAtt.java
similarity index 100%
rename from kernel/src/main/java/org/kframework/kore/AddAtt.java
rename to k-frontend/src/main/java/org/kframework/kore/AddAtt.java
diff --git a/kernel/src/main/java/org/kframework/kore/AddAttRec.java b/k-frontend/src/main/java/org/kframework/kore/AddAttRec.java
similarity index 100%
rename from kernel/src/main/java/org/kframework/kore/AddAttRec.java
rename to k-frontend/src/main/java/org/kframework/kore/AddAttRec.java
diff --git a/kernel/src/main/java/org/kframework/kore/AttCompare.java b/k-frontend/src/main/java/org/kframework/kore/AttCompare.java
similarity index 100%
rename from kernel/src/main/java/org/kframework/kore/AttCompare.java
rename to k-frontend/src/main/java/org/kframework/kore/AttCompare.java
diff --git a/kernel/src/main/java/org/kframework/kore/ExistsK.java b/k-frontend/src/main/java/org/kframework/kore/ExistsK.java
similarity index 100%
rename from kernel/src/main/java/org/kframework/kore/ExistsK.java
rename to k-frontend/src/main/java/org/kframework/kore/ExistsK.java
diff --git a/kernel/src/main/java/org/kframework/kore/FindK.java b/k-frontend/src/main/java/org/kframework/kore/FindK.java
similarity index 100%
rename from kernel/src/main/java/org/kframework/kore/FindK.java
rename to k-frontend/src/main/java/org/kframework/kore/FindK.java
diff --git a/kernel/src/main/java/org/kframework/kore/TransformK.java b/k-frontend/src/main/java/org/kframework/kore/TransformK.java
similarity index 100%
rename from kernel/src/main/java/org/kframework/kore/TransformK.java
rename to k-frontend/src/main/java/org/kframework/kore/TransformK.java
diff --git a/kernel/src/main/java/org/kframework/kore/VisitK.java b/k-frontend/src/main/java/org/kframework/kore/VisitK.java
similarity index 100%
rename from kernel/src/main/java/org/kframework/kore/VisitK.java
rename to k-frontend/src/main/java/org/kframework/kore/VisitK.java
diff --git a/kernel/src/main/java/org/kframework/kore/convertors/KILTransformation.java b/k-frontend/src/main/java/org/kframework/kore/convertors/KILTransformation.java
similarity index 100%
rename from kernel/src/main/java/org/kframework/kore/convertors/KILTransformation.java
rename to k-frontend/src/main/java/org/kframework/kore/convertors/KILTransformation.java
diff --git a/kernel/src/main/java/org/kframework/kore/convertors/KILtoKORE.java b/k-frontend/src/main/java/org/kframework/kore/convertors/KILtoKORE.java
similarity index 100%
rename from kernel/src/main/java/org/kframework/kore/convertors/KILtoKORE.java
rename to k-frontend/src/main/java/org/kframework/kore/convertors/KILtoKORE.java
diff --git a/kernel/src/main/java/org/kframework/kprove/KProve.java b/k-frontend/src/main/java/org/kframework/kprove/KProve.java
similarity index 100%
rename from kernel/src/main/java/org/kframework/kprove/KProve.java
rename to k-frontend/src/main/java/org/kframework/kprove/KProve.java
diff --git a/kernel/src/main/java/org/kframework/kprove/KProveFrontEnd.java b/k-frontend/src/main/java/org/kframework/kprove/KProveFrontEnd.java
similarity index 100%
rename from kernel/src/main/java/org/kframework/kprove/KProveFrontEnd.java
rename to k-frontend/src/main/java/org/kframework/kprove/KProveFrontEnd.java
diff --git a/kernel/src/main/java/org/kframework/kprove/KProveModule.java b/k-frontend/src/main/java/org/kframework/kprove/KProveModule.java
similarity index 100%
rename from kernel/src/main/java/org/kframework/kprove/KProveModule.java
rename to k-frontend/src/main/java/org/kframework/kprove/KProveModule.java
diff --git a/kernel/src/main/java/org/kframework/kprove/KProveOptions.java b/k-frontend/src/main/java/org/kframework/kprove/KProveOptions.java
similarity index 100%
rename from kernel/src/main/java/org/kframework/kprove/KProveOptions.java
rename to k-frontend/src/main/java/org/kframework/kprove/KProveOptions.java
diff --git a/kernel/src/main/java/org/kframework/kprove/ProofDefinitionBuilder.java b/k-frontend/src/main/java/org/kframework/kprove/ProofDefinitionBuilder.java
similarity index 100%
rename from kernel/src/main/java/org/kframework/kprove/ProofDefinitionBuilder.java
rename to k-frontend/src/main/java/org/kframework/kprove/ProofDefinitionBuilder.java
diff --git a/kernel/src/main/java/org/kframework/kprove/RewriterModule.java b/k-frontend/src/main/java/org/kframework/kprove/RewriterModule.java
similarity index 100%
rename from kernel/src/main/java/org/kframework/kprove/RewriterModule.java
rename to k-frontend/src/main/java/org/kframework/kprove/RewriterModule.java
diff --git a/kernel/src/main/java/org/kframework/ksearchpattern/KSearchPatternFrontEnd.java b/k-frontend/src/main/java/org/kframework/ksearchpattern/KSearchPatternFrontEnd.java
similarity index 100%
rename from kernel/src/main/java/org/kframework/ksearchpattern/KSearchPatternFrontEnd.java
rename to k-frontend/src/main/java/org/kframework/ksearchpattern/KSearchPatternFrontEnd.java
diff --git a/kernel/src/main/java/org/kframework/ksearchpattern/KSearchPatternModule.java b/k-frontend/src/main/java/org/kframework/ksearchpattern/KSearchPatternModule.java
similarity index 100%
rename from kernel/src/main/java/org/kframework/ksearchpattern/KSearchPatternModule.java
rename to k-frontend/src/main/java/org/kframework/ksearchpattern/KSearchPatternModule.java
diff --git a/kernel/src/main/java/org/kframework/ksearchpattern/KSearchPatternOptions.java b/k-frontend/src/main/java/org/kframework/ksearchpattern/KSearchPatternOptions.java
similarity index 100%
rename from kernel/src/main/java/org/kframework/ksearchpattern/KSearchPatternOptions.java
rename to k-frontend/src/main/java/org/kframework/ksearchpattern/KSearchPatternOptions.java
diff --git a/kernel/src/main/java/org/kframework/kserver/KServerFrontEnd.java b/k-frontend/src/main/java/org/kframework/kserver/KServerFrontEnd.java
similarity index 100%
rename from kernel/src/main/java/org/kframework/kserver/KServerFrontEnd.java
rename to k-frontend/src/main/java/org/kframework/kserver/KServerFrontEnd.java
diff --git a/kernel/src/main/java/org/kframework/kserver/KServerModule.java b/k-frontend/src/main/java/org/kframework/kserver/KServerModule.java
similarity index 100%
rename from kernel/src/main/java/org/kframework/kserver/KServerModule.java
rename to k-frontend/src/main/java/org/kframework/kserver/KServerModule.java
diff --git a/kernel/src/main/java/org/kframework/kserver/KServerOptions.java b/k-frontend/src/main/java/org/kframework/kserver/KServerOptions.java
similarity index 100%
rename from kernel/src/main/java/org/kframework/kserver/KServerOptions.java
rename to k-frontend/src/main/java/org/kframework/kserver/KServerOptions.java
diff --git a/kernel/src/main/java/org/kframework/lsp/CompletionHelper.java b/k-frontend/src/main/java/org/kframework/lsp/CompletionHelper.java
similarity index 100%
rename from kernel/src/main/java/org/kframework/lsp/CompletionHelper.java
rename to k-frontend/src/main/java/org/kframework/lsp/CompletionHelper.java
diff --git a/kernel/src/main/java/org/kframework/lsp/KLanguageServer.java b/k-frontend/src/main/java/org/kframework/lsp/KLanguageServer.java
similarity index 100%
rename from kernel/src/main/java/org/kframework/lsp/KLanguageServer.java
rename to k-frontend/src/main/java/org/kframework/lsp/KLanguageServer.java
diff --git a/kernel/src/main/java/org/kframework/lsp/KLanguageServerLauncher.java b/k-frontend/src/main/java/org/kframework/lsp/KLanguageServerLauncher.java
similarity index 100%
rename from kernel/src/main/java/org/kframework/lsp/KLanguageServerLauncher.java
rename to k-frontend/src/main/java/org/kframework/lsp/KLanguageServerLauncher.java
diff --git a/kernel/src/main/java/org/kframework/lsp/KPos.java b/k-frontend/src/main/java/org/kframework/lsp/KPos.java
similarity index 100%
rename from kernel/src/main/java/org/kframework/lsp/KPos.java
rename to k-frontend/src/main/java/org/kframework/lsp/KPos.java
diff --git a/kernel/src/main/java/org/kframework/lsp/KTextDocument.java b/k-frontend/src/main/java/org/kframework/lsp/KTextDocument.java
similarity index 100%
rename from kernel/src/main/java/org/kframework/lsp/KTextDocument.java
rename to k-frontend/src/main/java/org/kframework/lsp/KTextDocument.java
diff --git a/kernel/src/main/java/org/kframework/lsp/KTextDocumentService.java b/k-frontend/src/main/java/org/kframework/lsp/KTextDocumentService.java
similarity index 100%
rename from kernel/src/main/java/org/kframework/lsp/KTextDocumentService.java
rename to k-frontend/src/main/java/org/kframework/lsp/KTextDocumentService.java
diff --git a/kernel/src/main/java/org/kframework/lsp/KWorkspaceService.java b/k-frontend/src/main/java/org/kframework/lsp/KWorkspaceService.java
similarity index 100%
rename from kernel/src/main/java/org/kframework/lsp/KWorkspaceService.java
rename to k-frontend/src/main/java/org/kframework/lsp/KWorkspaceService.java
diff --git a/kernel/src/main/java/org/kframework/lsp/LSClientLogger.java b/k-frontend/src/main/java/org/kframework/lsp/LSClientLogger.java
similarity index 100%
rename from kernel/src/main/java/org/kframework/lsp/LSClientLogger.java
rename to k-frontend/src/main/java/org/kframework/lsp/LSClientLogger.java
diff --git a/kernel/src/main/java/org/kframework/lsp/TextDocumentSyncHandler.java b/k-frontend/src/main/java/org/kframework/lsp/TextDocumentSyncHandler.java
similarity index 100%
rename from kernel/src/main/java/org/kframework/lsp/TextDocumentSyncHandler.java
rename to k-frontend/src/main/java/org/kframework/lsp/TextDocumentSyncHandler.java
diff --git a/kernel/src/main/java/org/kframework/main/AbstractKModule.java b/k-frontend/src/main/java/org/kframework/main/AbstractKModule.java
similarity index 100%
rename from kernel/src/main/java/org/kframework/main/AbstractKModule.java
rename to k-frontend/src/main/java/org/kframework/main/AbstractKModule.java
diff --git a/kernel/src/main/java/org/kframework/main/FrontEnd.java b/k-frontend/src/main/java/org/kframework/main/FrontEnd.java
similarity index 100%
rename from kernel/src/main/java/org/kframework/main/FrontEnd.java
rename to k-frontend/src/main/java/org/kframework/main/FrontEnd.java
diff --git a/kernel/src/main/java/org/kframework/main/GlobalOptions.java b/k-frontend/src/main/java/org/kframework/main/GlobalOptions.java
similarity index 100%
rename from kernel/src/main/java/org/kframework/main/GlobalOptions.java
rename to k-frontend/src/main/java/org/kframework/main/GlobalOptions.java
diff --git a/kernel/src/main/java/org/kframework/main/JavaVersion.java b/k-frontend/src/main/java/org/kframework/main/JavaVersion.java
similarity index 100%
rename from kernel/src/main/java/org/kframework/main/JavaVersion.java
rename to k-frontend/src/main/java/org/kframework/main/JavaVersion.java
diff --git a/kernel/src/main/java/org/kframework/main/KModule.java b/k-frontend/src/main/java/org/kframework/main/KModule.java
similarity index 100%
rename from kernel/src/main/java/org/kframework/main/KModule.java
rename to k-frontend/src/main/java/org/kframework/main/KModule.java
diff --git a/kernel/src/main/java/org/kframework/main/Main.java b/k-frontend/src/main/java/org/kframework/main/Main.java
similarity index 100%
rename from kernel/src/main/java/org/kframework/main/Main.java
rename to k-frontend/src/main/java/org/kframework/main/Main.java
diff --git a/kernel/src/main/java/org/kframework/main/Tool.java b/k-frontend/src/main/java/org/kframework/main/Tool.java
similarity index 100%
rename from kernel/src/main/java/org/kframework/main/Tool.java
rename to k-frontend/src/main/java/org/kframework/main/Tool.java
diff --git a/kernel/src/main/java/org/kframework/parser/InputModes.java b/k-frontend/src/main/java/org/kframework/parser/InputModes.java
similarity index 100%
rename from kernel/src/main/java/org/kframework/parser/InputModes.java
rename to k-frontend/src/main/java/org/kframework/parser/InputModes.java
diff --git a/kernel/src/main/java/org/kframework/parser/KRead.java b/k-frontend/src/main/java/org/kframework/parser/KRead.java
similarity index 100%
rename from kernel/src/main/java/org/kframework/parser/KRead.java
rename to k-frontend/src/main/java/org/kframework/parser/KRead.java
diff --git a/kernel/src/main/java/org/kframework/parser/KoreParser.java b/k-frontend/src/main/java/org/kframework/parser/KoreParser.java
similarity index 100%
rename from kernel/src/main/java/org/kframework/parser/KoreParser.java
rename to k-frontend/src/main/java/org/kframework/parser/KoreParser.java
diff --git a/kernel/src/main/java/org/kframework/parser/ParserUtils.java b/k-frontend/src/main/java/org/kframework/parser/ParserUtils.java
similarity index 100%
rename from kernel/src/main/java/org/kframework/parser/ParserUtils.java
rename to k-frontend/src/main/java/org/kframework/parser/ParserUtils.java
diff --git a/kernel/src/main/java/org/kframework/parser/inner/ApplySynonyms.java b/k-frontend/src/main/java/org/kframework/parser/inner/ApplySynonyms.java
similarity index 100%
rename from kernel/src/main/java/org/kframework/parser/inner/ApplySynonyms.java
rename to k-frontend/src/main/java/org/kframework/parser/inner/ApplySynonyms.java
diff --git a/kernel/src/main/java/org/kframework/parser/inner/CollectProductionsVisitor.java b/k-frontend/src/main/java/org/kframework/parser/inner/CollectProductionsVisitor.java
similarity index 100%
rename from kernel/src/main/java/org/kframework/parser/inner/CollectProductionsVisitor.java
rename to k-frontend/src/main/java/org/kframework/parser/inner/CollectProductionsVisitor.java
diff --git a/kernel/src/main/java/org/kframework/parser/inner/ParseCache.java b/k-frontend/src/main/java/org/kframework/parser/inner/ParseCache.java
similarity index 100%
rename from kernel/src/main/java/org/kframework/parser/inner/ParseCache.java
rename to k-frontend/src/main/java/org/kframework/parser/inner/ParseCache.java
diff --git a/kernel/src/main/java/org/kframework/parser/inner/ParseInModule.java b/k-frontend/src/main/java/org/kframework/parser/inner/ParseInModule.java
similarity index 100%
rename from kernel/src/main/java/org/kframework/parser/inner/ParseInModule.java
rename to k-frontend/src/main/java/org/kframework/parser/inner/ParseInModule.java
diff --git a/kernel/src/main/java/org/kframework/parser/inner/RuleGrammarGenerator.java b/k-frontend/src/main/java/org/kframework/parser/inner/RuleGrammarGenerator.java
similarity index 100%
rename from kernel/src/main/java/org/kframework/parser/inner/RuleGrammarGenerator.java
rename to k-frontend/src/main/java/org/kframework/parser/inner/RuleGrammarGenerator.java
diff --git a/kernel/src/main/java/org/kframework/parser/inner/disambiguation/AddEmptyLists.java b/k-frontend/src/main/java/org/kframework/parser/inner/disambiguation/AddEmptyLists.java
similarity index 100%
rename from kernel/src/main/java/org/kframework/parser/inner/disambiguation/AddEmptyLists.java
rename to k-frontend/src/main/java/org/kframework/parser/inner/disambiguation/AddEmptyLists.java
diff --git a/kernel/src/main/java/org/kframework/parser/inner/disambiguation/AmbFilterError.java b/k-frontend/src/main/java/org/kframework/parser/inner/disambiguation/AmbFilterError.java
similarity index 100%
rename from kernel/src/main/java/org/kframework/parser/inner/disambiguation/AmbFilterError.java
rename to k-frontend/src/main/java/org/kframework/parser/inner/disambiguation/AmbFilterError.java
diff --git a/kernel/src/main/java/org/kframework/parser/inner/disambiguation/AmbiguityMergingTransformer.java b/k-frontend/src/main/java/org/kframework/parser/inner/disambiguation/AmbiguityMergingTransformer.java
similarity index 100%
rename from kernel/src/main/java/org/kframework/parser/inner/disambiguation/AmbiguityMergingTransformer.java
rename to k-frontend/src/main/java/org/kframework/parser/inner/disambiguation/AmbiguityMergingTransformer.java
diff --git a/kernel/src/main/java/org/kframework/parser/inner/disambiguation/CollapseRecordProdsVisitor.java b/k-frontend/src/main/java/org/kframework/parser/inner/disambiguation/CollapseRecordProdsVisitor.java
similarity index 100%
rename from kernel/src/main/java/org/kframework/parser/inner/disambiguation/CollapseRecordProdsVisitor.java
rename to k-frontend/src/main/java/org/kframework/parser/inner/disambiguation/CollapseRecordProdsVisitor.java
diff --git a/kernel/src/main/java/org/kframework/parser/inner/disambiguation/KAppToTermConsVisitor.java b/k-frontend/src/main/java/org/kframework/parser/inner/disambiguation/KAppToTermConsVisitor.java
similarity index 100%
rename from kernel/src/main/java/org/kframework/parser/inner/disambiguation/KAppToTermConsVisitor.java
rename to k-frontend/src/main/java/org/kframework/parser/inner/disambiguation/KAppToTermConsVisitor.java
diff --git a/kernel/src/main/java/org/kframework/parser/inner/disambiguation/PriorityVisitor.java b/k-frontend/src/main/java/org/kframework/parser/inner/disambiguation/PriorityVisitor.java
similarity index 100%
rename from kernel/src/main/java/org/kframework/parser/inner/disambiguation/PriorityVisitor.java
rename to k-frontend/src/main/java/org/kframework/parser/inner/disambiguation/PriorityVisitor.java
diff --git a/kernel/src/main/java/org/kframework/parser/inner/disambiguation/PushAmbiguitiesDownAndPreferAvoid.java b/k-frontend/src/main/java/org/kframework/parser/inner/disambiguation/PushAmbiguitiesDownAndPreferAvoid.java
similarity index 100%
rename from kernel/src/main/java/org/kframework/parser/inner/disambiguation/PushAmbiguitiesDownAndPreferAvoid.java
rename to k-frontend/src/main/java/org/kframework/parser/inner/disambiguation/PushAmbiguitiesDownAndPreferAvoid.java
diff --git a/kernel/src/main/java/org/kframework/parser/inner/disambiguation/PushTopLHSAmbiguityUp.java b/k-frontend/src/main/java/org/kframework/parser/inner/disambiguation/PushTopLHSAmbiguityUp.java
similarity index 100%
rename from kernel/src/main/java/org/kframework/parser/inner/disambiguation/PushTopLHSAmbiguityUp.java
rename to k-frontend/src/main/java/org/kframework/parser/inner/disambiguation/PushTopLHSAmbiguityUp.java
diff --git a/kernel/src/main/java/org/kframework/parser/inner/disambiguation/RemoveBracketVisitor.java b/k-frontend/src/main/java/org/kframework/parser/inner/disambiguation/RemoveBracketVisitor.java
similarity index 100%
rename from kernel/src/main/java/org/kframework/parser/inner/disambiguation/RemoveBracketVisitor.java
rename to k-frontend/src/main/java/org/kframework/parser/inner/disambiguation/RemoveBracketVisitor.java
diff --git a/kernel/src/main/java/org/kframework/parser/inner/disambiguation/RemoveOverloads.java b/k-frontend/src/main/java/org/kframework/parser/inner/disambiguation/RemoveOverloads.java
similarity index 100%
rename from kernel/src/main/java/org/kframework/parser/inner/disambiguation/RemoveOverloads.java
rename to k-frontend/src/main/java/org/kframework/parser/inner/disambiguation/RemoveOverloads.java
diff --git a/kernel/src/main/java/org/kframework/parser/inner/disambiguation/ResolveOverloadedTerminators.java b/k-frontend/src/main/java/org/kframework/parser/inner/disambiguation/ResolveOverloadedTerminators.java
similarity index 100%
rename from kernel/src/main/java/org/kframework/parser/inner/disambiguation/ResolveOverloadedTerminators.java
rename to k-frontend/src/main/java/org/kframework/parser/inner/disambiguation/ResolveOverloadedTerminators.java
diff --git a/kernel/src/main/java/org/kframework/parser/inner/disambiguation/TreeCleanerVisitor.java b/k-frontend/src/main/java/org/kframework/parser/inner/disambiguation/TreeCleanerVisitor.java
similarity index 100%
rename from kernel/src/main/java/org/kframework/parser/inner/disambiguation/TreeCleanerVisitor.java
rename to k-frontend/src/main/java/org/kframework/parser/inner/disambiguation/TreeCleanerVisitor.java
diff --git a/kernel/src/main/java/org/kframework/parser/inner/disambiguation/TypeInferenceVisitor.java b/k-frontend/src/main/java/org/kframework/parser/inner/disambiguation/TypeInferenceVisitor.java
similarity index 100%
rename from kernel/src/main/java/org/kframework/parser/inner/disambiguation/TypeInferenceVisitor.java
rename to k-frontend/src/main/java/org/kframework/parser/inner/disambiguation/TypeInferenceVisitor.java
diff --git a/kernel/src/main/java/org/kframework/parser/inner/disambiguation/TypeInferencer.java b/k-frontend/src/main/java/org/kframework/parser/inner/disambiguation/TypeInferencer.java
similarity index 100%
rename from kernel/src/main/java/org/kframework/parser/inner/disambiguation/TypeInferencer.java
rename to k-frontend/src/main/java/org/kframework/parser/inner/disambiguation/TypeInferencer.java
diff --git a/kernel/src/main/java/org/kframework/parser/inner/disambiguation/inference/BoundedSort.java b/k-frontend/src/main/java/org/kframework/parser/inner/disambiguation/inference/BoundedSort.java
similarity index 100%
rename from kernel/src/main/java/org/kframework/parser/inner/disambiguation/inference/BoundedSort.java
rename to k-frontend/src/main/java/org/kframework/parser/inner/disambiguation/inference/BoundedSort.java
diff --git a/kernel/src/main/java/org/kframework/parser/inner/disambiguation/inference/CompactSort.java b/k-frontend/src/main/java/org/kframework/parser/inner/disambiguation/inference/CompactSort.java
similarity index 100%
rename from kernel/src/main/java/org/kframework/parser/inner/disambiguation/inference/CompactSort.java
rename to k-frontend/src/main/java/org/kframework/parser/inner/disambiguation/inference/CompactSort.java
diff --git a/kernel/src/main/java/org/kframework/parser/inner/disambiguation/inference/InferenceDriver.java b/k-frontend/src/main/java/org/kframework/parser/inner/disambiguation/inference/InferenceDriver.java
similarity index 100%
rename from kernel/src/main/java/org/kframework/parser/inner/disambiguation/inference/InferenceDriver.java
rename to k-frontend/src/main/java/org/kframework/parser/inner/disambiguation/inference/InferenceDriver.java
diff --git a/kernel/src/main/java/org/kframework/parser/inner/disambiguation/inference/ParamId.java b/k-frontend/src/main/java/org/kframework/parser/inner/disambiguation/inference/ParamId.java
similarity index 100%
rename from kernel/src/main/java/org/kframework/parser/inner/disambiguation/inference/ParamId.java
rename to k-frontend/src/main/java/org/kframework/parser/inner/disambiguation/inference/ParamId.java
diff --git a/kernel/src/main/java/org/kframework/parser/inner/disambiguation/inference/SortInferenceError.java b/k-frontend/src/main/java/org/kframework/parser/inner/disambiguation/inference/SortInferenceError.java
similarity index 100%
rename from kernel/src/main/java/org/kframework/parser/inner/disambiguation/inference/SortInferenceError.java
rename to k-frontend/src/main/java/org/kframework/parser/inner/disambiguation/inference/SortInferenceError.java
diff --git a/kernel/src/main/java/org/kframework/parser/inner/disambiguation/inference/SortInferencer.java b/k-frontend/src/main/java/org/kframework/parser/inner/disambiguation/inference/SortInferencer.java
similarity index 100%
rename from kernel/src/main/java/org/kframework/parser/inner/disambiguation/inference/SortInferencer.java
rename to k-frontend/src/main/java/org/kframework/parser/inner/disambiguation/inference/SortInferencer.java
diff --git a/kernel/src/main/java/org/kframework/parser/inner/disambiguation/inference/SortVariable.java b/k-frontend/src/main/java/org/kframework/parser/inner/disambiguation/inference/SortVariable.java
similarity index 100%
rename from kernel/src/main/java/org/kframework/parser/inner/disambiguation/inference/SortVariable.java
rename to k-frontend/src/main/java/org/kframework/parser/inner/disambiguation/inference/SortVariable.java
diff --git a/kernel/src/main/java/org/kframework/parser/inner/disambiguation/inference/TermSort.java b/k-frontend/src/main/java/org/kframework/parser/inner/disambiguation/inference/TermSort.java
similarity index 100%
rename from kernel/src/main/java/org/kframework/parser/inner/disambiguation/inference/TermSort.java
rename to k-frontend/src/main/java/org/kframework/parser/inner/disambiguation/inference/TermSort.java
diff --git a/kernel/src/main/java/org/kframework/parser/inner/disambiguation/inference/VariableId.java b/k-frontend/src/main/java/org/kframework/parser/inner/disambiguation/inference/VariableId.java
similarity index 100%
rename from kernel/src/main/java/org/kframework/parser/inner/disambiguation/inference/VariableId.java
rename to k-frontend/src/main/java/org/kframework/parser/inner/disambiguation/inference/VariableId.java
diff --git a/kernel/src/main/java/org/kframework/parser/inner/kernel/EarleyParser.java b/k-frontend/src/main/java/org/kframework/parser/inner/kernel/EarleyParser.java
similarity index 100%
rename from kernel/src/main/java/org/kframework/parser/inner/kernel/EarleyParser.java
rename to k-frontend/src/main/java/org/kframework/parser/inner/kernel/EarleyParser.java
diff --git a/kernel/src/main/java/org/kframework/parser/inner/kernel/KSyntax2Bison.java b/k-frontend/src/main/java/org/kframework/parser/inner/kernel/KSyntax2Bison.java
similarity index 100%
rename from kernel/src/main/java/org/kframework/parser/inner/kernel/KSyntax2Bison.java
rename to k-frontend/src/main/java/org/kframework/parser/inner/kernel/KSyntax2Bison.java
diff --git a/kernel/src/main/java/org/kframework/parser/inner/kernel/Scanner.java b/k-frontend/src/main/java/org/kframework/parser/inner/kernel/Scanner.java
similarity index 100%
rename from kernel/src/main/java/org/kframework/parser/inner/kernel/Scanner.java
rename to k-frontend/src/main/java/org/kframework/parser/inner/kernel/Scanner.java
diff --git a/kernel/src/main/java/org/kframework/parser/json/JsonParser.java b/k-frontend/src/main/java/org/kframework/parser/json/JsonParser.java
similarity index 100%
rename from kernel/src/main/java/org/kframework/parser/json/JsonParser.java
rename to k-frontend/src/main/java/org/kframework/parser/json/JsonParser.java
diff --git a/kernel/src/main/java/org/kframework/parser/outer/ExtractFencedKCodeFromMarkdown.java b/k-frontend/src/main/java/org/kframework/parser/outer/ExtractFencedKCodeFromMarkdown.java
similarity index 100%
rename from kernel/src/main/java/org/kframework/parser/outer/ExtractFencedKCodeFromMarkdown.java
rename to k-frontend/src/main/java/org/kframework/parser/outer/ExtractFencedKCodeFromMarkdown.java
diff --git a/kernel/src/main/java/org/kframework/unparser/AddBrackets.java b/k-frontend/src/main/java/org/kframework/unparser/AddBrackets.java
similarity index 100%
rename from kernel/src/main/java/org/kframework/unparser/AddBrackets.java
rename to k-frontend/src/main/java/org/kframework/unparser/AddBrackets.java
diff --git a/kernel/src/main/java/org/kframework/unparser/ColorSetting.java b/k-frontend/src/main/java/org/kframework/unparser/ColorSetting.java
similarity index 100%
rename from kernel/src/main/java/org/kframework/unparser/ColorSetting.java
rename to k-frontend/src/main/java/org/kframework/unparser/ColorSetting.java
diff --git a/kernel/src/main/java/org/kframework/unparser/Formatter.java b/k-frontend/src/main/java/org/kframework/unparser/Formatter.java
similarity index 100%
rename from kernel/src/main/java/org/kframework/unparser/Formatter.java
rename to k-frontend/src/main/java/org/kframework/unparser/Formatter.java
diff --git a/kernel/src/main/java/org/kframework/unparser/Indenter.java b/k-frontend/src/main/java/org/kframework/unparser/Indenter.java
similarity index 100%
rename from kernel/src/main/java/org/kframework/unparser/Indenter.java
rename to k-frontend/src/main/java/org/kframework/unparser/Indenter.java
diff --git a/kernel/src/main/java/org/kframework/unparser/KPrint.java b/k-frontend/src/main/java/org/kframework/unparser/KPrint.java
similarity index 100%
rename from kernel/src/main/java/org/kframework/unparser/KPrint.java
rename to k-frontend/src/main/java/org/kframework/unparser/KPrint.java
diff --git a/kernel/src/main/java/org/kframework/unparser/OutputModes.java b/k-frontend/src/main/java/org/kframework/unparser/OutputModes.java
similarity index 100%
rename from kernel/src/main/java/org/kframework/unparser/OutputModes.java
rename to k-frontend/src/main/java/org/kframework/unparser/OutputModes.java
diff --git a/kernel/src/main/java/org/kframework/unparser/PrintOptions.java b/k-frontend/src/main/java/org/kframework/unparser/PrintOptions.java
similarity index 100%
rename from kernel/src/main/java/org/kframework/unparser/PrintOptions.java
rename to k-frontend/src/main/java/org/kframework/unparser/PrintOptions.java
diff --git a/kernel/src/main/java/org/kframework/unparser/ToJson.java b/k-frontend/src/main/java/org/kframework/unparser/ToJson.java
similarity index 100%
rename from kernel/src/main/java/org/kframework/unparser/ToJson.java
rename to k-frontend/src/main/java/org/kframework/unparser/ToJson.java
diff --git a/kernel/src/main/java/org/kframework/utils/BinaryLoader.java b/k-frontend/src/main/java/org/kframework/utils/BinaryLoader.java
similarity index 100%
rename from kernel/src/main/java/org/kframework/utils/BinaryLoader.java
rename to k-frontend/src/main/java/org/kframework/utils/BinaryLoader.java
diff --git a/kernel/src/main/java/org/kframework/utils/ColorUtil.java b/k-frontend/src/main/java/org/kframework/utils/ColorUtil.java
similarity index 100%
rename from kernel/src/main/java/org/kframework/utils/ColorUtil.java
rename to k-frontend/src/main/java/org/kframework/utils/ColorUtil.java
diff --git a/kernel/src/main/java/org/kframework/utils/ExitOnTimeoutThread.java b/k-frontend/src/main/java/org/kframework/utils/ExitOnTimeoutThread.java
similarity index 100%
rename from kernel/src/main/java/org/kframework/utils/ExitOnTimeoutThread.java
rename to k-frontend/src/main/java/org/kframework/utils/ExitOnTimeoutThread.java
diff --git a/kernel/src/main/java/org/kframework/utils/InterrupterRunnable.java b/k-frontend/src/main/java/org/kframework/utils/InterrupterRunnable.java
similarity index 100%
rename from kernel/src/main/java/org/kframework/utils/InterrupterRunnable.java
rename to k-frontend/src/main/java/org/kframework/utils/InterrupterRunnable.java
diff --git a/kernel/src/main/java/org/kframework/utils/Lazy.java b/k-frontend/src/main/java/org/kframework/utils/Lazy.java
similarity index 100%
rename from kernel/src/main/java/org/kframework/utils/Lazy.java
rename to k-frontend/src/main/java/org/kframework/utils/Lazy.java
diff --git a/kernel/src/main/java/org/kframework/utils/OS.java b/k-frontend/src/main/java/org/kframework/utils/OS.java
similarity index 100%
rename from kernel/src/main/java/org/kframework/utils/OS.java
rename to k-frontend/src/main/java/org/kframework/utils/OS.java
diff --git a/kernel/src/main/java/org/kframework/utils/RunProcess.java b/k-frontend/src/main/java/org/kframework/utils/RunProcess.java
similarity index 100%
rename from kernel/src/main/java/org/kframework/utils/RunProcess.java
rename to k-frontend/src/main/java/org/kframework/utils/RunProcess.java
diff --git a/kernel/src/main/java/org/kframework/utils/Stopwatch.java b/k-frontend/src/main/java/org/kframework/utils/Stopwatch.java
similarity index 100%
rename from kernel/src/main/java/org/kframework/utils/Stopwatch.java
rename to k-frontend/src/main/java/org/kframework/utils/Stopwatch.java
diff --git a/kernel/src/main/java/org/kframework/utils/StringUtil.java b/k-frontend/src/main/java/org/kframework/utils/StringUtil.java
similarity index 100%
rename from kernel/src/main/java/org/kframework/utils/StringUtil.java
rename to k-frontend/src/main/java/org/kframework/utils/StringUtil.java
diff --git a/kernel/src/main/java/org/kframework/utils/errorsystem/KEMException.java b/k-frontend/src/main/java/org/kframework/utils/errorsystem/KEMException.java
similarity index 100%
rename from kernel/src/main/java/org/kframework/utils/errorsystem/KEMException.java
rename to k-frontend/src/main/java/org/kframework/utils/errorsystem/KEMException.java
diff --git a/kernel/src/main/java/org/kframework/utils/errorsystem/KException.java b/k-frontend/src/main/java/org/kframework/utils/errorsystem/KException.java
similarity index 100%
rename from kernel/src/main/java/org/kframework/utils/errorsystem/KException.java
rename to k-frontend/src/main/java/org/kframework/utils/errorsystem/KException.java
diff --git a/kernel/src/main/java/org/kframework/utils/errorsystem/KExceptionManager.java b/k-frontend/src/main/java/org/kframework/utils/errorsystem/KExceptionManager.java
similarity index 100%
rename from kernel/src/main/java/org/kframework/utils/errorsystem/KExceptionManager.java
rename to k-frontend/src/main/java/org/kframework/utils/errorsystem/KExceptionManager.java
diff --git a/kernel/src/main/java/org/kframework/utils/file/DefinitionDir.java b/k-frontend/src/main/java/org/kframework/utils/file/DefinitionDir.java
similarity index 100%
rename from kernel/src/main/java/org/kframework/utils/file/DefinitionDir.java
rename to k-frontend/src/main/java/org/kframework/utils/file/DefinitionDir.java
diff --git a/kernel/src/main/java/org/kframework/utils/file/Environment.java b/k-frontend/src/main/java/org/kframework/utils/file/Environment.java
similarity index 100%
rename from kernel/src/main/java/org/kframework/utils/file/Environment.java
rename to k-frontend/src/main/java/org/kframework/utils/file/Environment.java
diff --git a/kernel/src/main/java/org/kframework/utils/file/FileUtil.java b/k-frontend/src/main/java/org/kframework/utils/file/FileUtil.java
similarity index 100%
rename from kernel/src/main/java/org/kframework/utils/file/FileUtil.java
rename to k-frontend/src/main/java/org/kframework/utils/file/FileUtil.java
diff --git a/kernel/src/main/java/org/kframework/utils/file/JarInfo.java b/k-frontend/src/main/java/org/kframework/utils/file/JarInfo.java
similarity index 97%
rename from kernel/src/main/java/org/kframework/utils/file/JarInfo.java
rename to k-frontend/src/main/java/org/kframework/utils/file/JarInfo.java
index c2b92f08d1e..a6b50252025 100644
--- a/kernel/src/main/java/org/kframework/utils/file/JarInfo.java
+++ b/k-frontend/src/main/java/org/kframework/utils/file/JarInfo.java
@@ -43,7 +43,7 @@ public static String getKBase() {
* Returns the absolute path of the includes directory. Paths are computed relative to the
* location this class is running from. When it is run from a jar file it assumes it is in a k
* installation at lib/java/*.jar. When it is run from a .class file it assumes it is running
- * within the K source project, from a class in kernel/target/classes/, and returns a path to
+ * within the K source project, from a class in k-frontend/target/classes/, and returns a path to
* k-distribution/include
*
* @return
diff --git a/kernel/src/main/java/org/kframework/utils/file/KompiledDir.java b/k-frontend/src/main/java/org/kframework/utils/file/KompiledDir.java
similarity index 100%
rename from kernel/src/main/java/org/kframework/utils/file/KompiledDir.java
rename to k-frontend/src/main/java/org/kframework/utils/file/KompiledDir.java
diff --git a/kernel/src/main/java/org/kframework/utils/file/TTYInfo.java b/k-frontend/src/main/java/org/kframework/utils/file/TTYInfo.java
similarity index 100%
rename from kernel/src/main/java/org/kframework/utils/file/TTYInfo.java
rename to k-frontend/src/main/java/org/kframework/utils/file/TTYInfo.java
diff --git a/kernel/src/main/java/org/kframework/utils/file/TempDir.java b/k-frontend/src/main/java/org/kframework/utils/file/TempDir.java
similarity index 100%
rename from kernel/src/main/java/org/kframework/utils/file/TempDir.java
rename to k-frontend/src/main/java/org/kframework/utils/file/TempDir.java
diff --git a/kernel/src/main/java/org/kframework/utils/file/WorkingDir.java b/k-frontend/src/main/java/org/kframework/utils/file/WorkingDir.java
similarity index 100%
rename from kernel/src/main/java/org/kframework/utils/file/WorkingDir.java
rename to k-frontend/src/main/java/org/kframework/utils/file/WorkingDir.java
diff --git a/kernel/src/main/java/org/kframework/utils/inject/Annotations.java b/k-frontend/src/main/java/org/kframework/utils/inject/Annotations.java
similarity index 100%
rename from kernel/src/main/java/org/kframework/utils/inject/Annotations.java
rename to k-frontend/src/main/java/org/kframework/utils/inject/Annotations.java
diff --git a/kernel/src/main/java/org/kframework/utils/inject/CommonModule.java b/k-frontend/src/main/java/org/kframework/utils/inject/CommonModule.java
similarity index 100%
rename from kernel/src/main/java/org/kframework/utils/inject/CommonModule.java
rename to k-frontend/src/main/java/org/kframework/utils/inject/CommonModule.java
diff --git a/kernel/src/main/java/org/kframework/utils/inject/Concrete.java b/k-frontend/src/main/java/org/kframework/utils/inject/Concrete.java
similarity index 100%
rename from kernel/src/main/java/org/kframework/utils/inject/Concrete.java
rename to k-frontend/src/main/java/org/kframework/utils/inject/Concrete.java
diff --git a/kernel/src/main/java/org/kframework/utils/inject/DefinitionLoadingModule.java b/k-frontend/src/main/java/org/kframework/utils/inject/DefinitionLoadingModule.java
similarity index 100%
rename from kernel/src/main/java/org/kframework/utils/inject/DefinitionLoadingModule.java
rename to k-frontend/src/main/java/org/kframework/utils/inject/DefinitionLoadingModule.java
diff --git a/kernel/src/main/java/org/kframework/utils/inject/DefinitionScope.java b/k-frontend/src/main/java/org/kframework/utils/inject/DefinitionScope.java
similarity index 100%
rename from kernel/src/main/java/org/kframework/utils/inject/DefinitionScope.java
rename to k-frontend/src/main/java/org/kframework/utils/inject/DefinitionScope.java
diff --git a/kernel/src/main/java/org/kframework/utils/inject/DefinitionScoped.java b/k-frontend/src/main/java/org/kframework/utils/inject/DefinitionScoped.java
similarity index 100%
rename from kernel/src/main/java/org/kframework/utils/inject/DefinitionScoped.java
rename to k-frontend/src/main/java/org/kframework/utils/inject/DefinitionScoped.java
diff --git a/kernel/src/main/java/org/kframework/utils/inject/JCommanderModule.java b/k-frontend/src/main/java/org/kframework/utils/inject/JCommanderModule.java
similarity index 100%
rename from kernel/src/main/java/org/kframework/utils/inject/JCommanderModule.java
rename to k-frontend/src/main/java/org/kframework/utils/inject/JCommanderModule.java
diff --git a/kernel/src/main/java/org/kframework/utils/inject/Main.java b/k-frontend/src/main/java/org/kframework/utils/inject/Main.java
similarity index 100%
rename from kernel/src/main/java/org/kframework/utils/inject/Main.java
rename to k-frontend/src/main/java/org/kframework/utils/inject/Main.java
diff --git a/kernel/src/main/java/org/kframework/utils/inject/Options.java b/k-frontend/src/main/java/org/kframework/utils/inject/Options.java
similarity index 100%
rename from kernel/src/main/java/org/kframework/utils/inject/Options.java
rename to k-frontend/src/main/java/org/kframework/utils/inject/Options.java
diff --git a/kernel/src/main/java/org/kframework/utils/inject/OuterParsingModule.java b/k-frontend/src/main/java/org/kframework/utils/inject/OuterParsingModule.java
similarity index 100%
rename from kernel/src/main/java/org/kframework/utils/inject/OuterParsingModule.java
rename to k-frontend/src/main/java/org/kframework/utils/inject/OuterParsingModule.java
diff --git a/kernel/src/main/java/org/kframework/utils/inject/RequestScoped.java b/k-frontend/src/main/java/org/kframework/utils/inject/RequestScoped.java
similarity index 100%
rename from kernel/src/main/java/org/kframework/utils/inject/RequestScoped.java
rename to k-frontend/src/main/java/org/kframework/utils/inject/RequestScoped.java
diff --git a/kernel/src/main/java/org/kframework/utils/inject/SimpleScope.java b/k-frontend/src/main/java/org/kframework/utils/inject/SimpleScope.java
similarity index 100%
rename from kernel/src/main/java/org/kframework/utils/inject/SimpleScope.java
rename to k-frontend/src/main/java/org/kframework/utils/inject/SimpleScope.java
diff --git a/kernel/src/main/java/org/kframework/utils/inject/Spec1.java b/k-frontend/src/main/java/org/kframework/utils/inject/Spec1.java
similarity index 100%
rename from kernel/src/main/java/org/kframework/utils/inject/Spec1.java
rename to k-frontend/src/main/java/org/kframework/utils/inject/Spec1.java
diff --git a/kernel/src/main/java/org/kframework/utils/inject/Spec2.java b/k-frontend/src/main/java/org/kframework/utils/inject/Spec2.java
similarity index 100%
rename from kernel/src/main/java/org/kframework/utils/inject/Spec2.java
rename to k-frontend/src/main/java/org/kframework/utils/inject/Spec2.java
diff --git a/kernel/src/main/java/org/kframework/utils/inject/StartTime.java b/k-frontend/src/main/java/org/kframework/utils/inject/StartTime.java
similarity index 100%
rename from kernel/src/main/java/org/kframework/utils/inject/StartTime.java
rename to k-frontend/src/main/java/org/kframework/utils/inject/StartTime.java
diff --git a/kernel/src/main/java/org/kframework/utils/options/BackendOptions.java b/k-frontend/src/main/java/org/kframework/utils/options/BackendOptions.java
similarity index 100%
rename from kernel/src/main/java/org/kframework/utils/options/BackendOptions.java
rename to k-frontend/src/main/java/org/kframework/utils/options/BackendOptions.java
diff --git a/kernel/src/main/java/org/kframework/utils/options/BaseEnumConverter.java b/k-frontend/src/main/java/org/kframework/utils/options/BaseEnumConverter.java
similarity index 100%
rename from kernel/src/main/java/org/kframework/utils/options/BaseEnumConverter.java
rename to k-frontend/src/main/java/org/kframework/utils/options/BaseEnumConverter.java
diff --git a/kernel/src/main/java/org/kframework/utils/options/DefinitionLoadingOptions.java b/k-frontend/src/main/java/org/kframework/utils/options/DefinitionLoadingOptions.java
similarity index 100%
rename from kernel/src/main/java/org/kframework/utils/options/DefinitionLoadingOptions.java
rename to k-frontend/src/main/java/org/kframework/utils/options/DefinitionLoadingOptions.java
diff --git a/kernel/src/main/java/org/kframework/utils/options/DurationConverter.java b/k-frontend/src/main/java/org/kframework/utils/options/DurationConverter.java
similarity index 100%
rename from kernel/src/main/java/org/kframework/utils/options/DurationConverter.java
rename to k-frontend/src/main/java/org/kframework/utils/options/DurationConverter.java
diff --git a/kernel/src/main/java/org/kframework/utils/options/InnerParsingOptions.java b/k-frontend/src/main/java/org/kframework/utils/options/InnerParsingOptions.java
similarity index 100%
rename from kernel/src/main/java/org/kframework/utils/options/InnerParsingOptions.java
rename to k-frontend/src/main/java/org/kframework/utils/options/InnerParsingOptions.java
diff --git a/kernel/src/main/java/org/kframework/utils/options/OuterParsingOptions.java b/k-frontend/src/main/java/org/kframework/utils/options/OuterParsingOptions.java
similarity index 100%
rename from kernel/src/main/java/org/kframework/utils/options/OuterParsingOptions.java
rename to k-frontend/src/main/java/org/kframework/utils/options/OuterParsingOptions.java
diff --git a/kernel/src/main/java/org/kframework/utils/options/OutputDirectoryOptions.java b/k-frontend/src/main/java/org/kframework/utils/options/OutputDirectoryOptions.java
similarity index 100%
rename from kernel/src/main/java/org/kframework/utils/options/OutputDirectoryOptions.java
rename to k-frontend/src/main/java/org/kframework/utils/options/OutputDirectoryOptions.java
diff --git a/kernel/src/main/java/org/kframework/utils/options/SMTOptions.java b/k-frontend/src/main/java/org/kframework/utils/options/SMTOptions.java
similarity index 100%
rename from kernel/src/main/java/org/kframework/utils/options/SMTOptions.java
rename to k-frontend/src/main/java/org/kframework/utils/options/SMTOptions.java
diff --git a/kernel/src/main/java/org/kframework/utils/options/SMTSolver.java b/k-frontend/src/main/java/org/kframework/utils/options/SMTSolver.java
similarity index 100%
rename from kernel/src/main/java/org/kframework/utils/options/SMTSolver.java
rename to k-frontend/src/main/java/org/kframework/utils/options/SMTSolver.java
diff --git a/kernel/src/main/java/org/kframework/utils/options/StringListConverter.java b/k-frontend/src/main/java/org/kframework/utils/options/StringListConverter.java
similarity index 100%
rename from kernel/src/main/java/org/kframework/utils/options/StringListConverter.java
rename to k-frontend/src/main/java/org/kframework/utils/options/StringListConverter.java
diff --git a/kernel/src/main/javacc/KastParser.jj b/k-frontend/src/main/javacc/KastParser.jj
similarity index 100%
rename from kernel/src/main/javacc/KastParser.jj
rename to k-frontend/src/main/javacc/KastParser.jj
diff --git a/kernel/src/main/javacc/Outer.jj b/k-frontend/src/main/javacc/Outer.jj
similarity index 100%
rename from kernel/src/main/javacc/Outer.jj
rename to k-frontend/src/main/javacc/Outer.jj
diff --git a/kernel/src/main/javacc/SmtSortParser.jj b/k-frontend/src/main/javacc/SmtSortParser.jj
similarity index 100%
rename from kernel/src/main/javacc/SmtSortParser.jj
rename to k-frontend/src/main/javacc/SmtSortParser.jj
diff --git a/kernel/src/main/jjtree/TagSelector.jjt b/k-frontend/src/main/jjtree/TagSelector.jjt
similarity index 100%
rename from kernel/src/main/jjtree/TagSelector.jjt
rename to k-frontend/src/main/jjtree/TagSelector.jjt
diff --git a/kernel/src/main/resources/org/kframework/utils/file/README.md b/k-frontend/src/main/resources/org/kframework/utils/file/README.md
similarity index 100%
rename from kernel/src/main/resources/org/kframework/utils/file/README.md
rename to k-frontend/src/main/resources/org/kframework/utils/file/README.md
diff --git a/kernel/src/main/resources/org/kframework/utils/file/versionMarker b/k-frontend/src/main/resources/org/kframework/utils/file/versionMarker
similarity index 100%
rename from kernel/src/main/resources/org/kframework/utils/file/versionMarker
rename to k-frontend/src/main/resources/org/kframework/utils/file/versionMarker
diff --git a/kernel/src/main/scala/org/kframework/RewriterResult.scala b/k-frontend/src/main/scala/org/kframework/RewriterResult.scala
similarity index 100%
rename from kernel/src/main/scala/org/kframework/RewriterResult.scala
rename to k-frontend/src/main/scala/org/kframework/RewriterResult.scala
diff --git a/kernel/src/main/scala/org/kframework/attributes/Att.scala b/k-frontend/src/main/scala/org/kframework/attributes/Att.scala
similarity index 100%
rename from kernel/src/main/scala/org/kframework/attributes/Att.scala
rename to k-frontend/src/main/scala/org/kframework/attributes/Att.scala
diff --git a/kernel/src/main/scala/org/kframework/attributes/Location.scala b/k-frontend/src/main/scala/org/kframework/attributes/Location.scala
similarity index 100%
rename from kernel/src/main/scala/org/kframework/attributes/Location.scala
rename to k-frontend/src/main/scala/org/kframework/attributes/Location.scala
diff --git a/kernel/src/main/scala/org/kframework/builtin/Sorts.scala b/k-frontend/src/main/scala/org/kframework/builtin/Sorts.scala
similarity index 100%
rename from kernel/src/main/scala/org/kframework/builtin/Sorts.scala
rename to k-frontend/src/main/scala/org/kframework/builtin/Sorts.scala
diff --git a/kernel/src/main/scala/org/kframework/collections.scala b/k-frontend/src/main/scala/org/kframework/collections.scala
similarity index 100%
rename from kernel/src/main/scala/org/kframework/collections.scala
rename to k-frontend/src/main/scala/org/kframework/collections.scala
diff --git a/kernel/src/main/scala/org/kframework/compile/ConfigurationInfoFromModule.scala b/k-frontend/src/main/scala/org/kframework/compile/ConfigurationInfoFromModule.scala
similarity index 100%
rename from kernel/src/main/scala/org/kframework/compile/ConfigurationInfoFromModule.scala
rename to k-frontend/src/main/scala/org/kframework/compile/ConfigurationInfoFromModule.scala
diff --git a/kernel/src/main/scala/org/kframework/compile/LabelInfoFromModule.scala b/k-frontend/src/main/scala/org/kframework/compile/LabelInfoFromModule.scala
similarity index 100%
rename from kernel/src/main/scala/org/kframework/compile/LabelInfoFromModule.scala
rename to k-frontend/src/main/scala/org/kframework/compile/LabelInfoFromModule.scala
diff --git a/kernel/src/main/scala/org/kframework/compile/RewriteToTop.scala b/k-frontend/src/main/scala/org/kframework/compile/RewriteToTop.scala
similarity index 100%
rename from kernel/src/main/scala/org/kframework/compile/RewriteToTop.scala
rename to k-frontend/src/main/scala/org/kframework/compile/RewriteToTop.scala
diff --git a/kernel/src/main/scala/org/kframework/definition/Constructors.scala b/k-frontend/src/main/scala/org/kframework/definition/Constructors.scala
similarity index 100%
rename from kernel/src/main/scala/org/kframework/definition/Constructors.scala
rename to k-frontend/src/main/scala/org/kframework/definition/Constructors.scala
diff --git a/kernel/src/main/scala/org/kframework/definition/outer-ext.scala b/k-frontend/src/main/scala/org/kframework/definition/outer-ext.scala
similarity index 100%
rename from kernel/src/main/scala/org/kframework/definition/outer-ext.scala
rename to k-frontend/src/main/scala/org/kframework/definition/outer-ext.scala
diff --git a/kernel/src/main/scala/org/kframework/definition/outer-to-string.scala b/k-frontend/src/main/scala/org/kframework/definition/outer-to-string.scala
similarity index 100%
rename from kernel/src/main/scala/org/kframework/definition/outer-to-string.scala
rename to k-frontend/src/main/scala/org/kframework/definition/outer-to-string.scala
diff --git a/kernel/src/main/scala/org/kframework/definition/outer.scala b/k-frontend/src/main/scala/org/kframework/definition/outer.scala
similarity index 100%
rename from kernel/src/main/scala/org/kframework/definition/outer.scala
rename to k-frontend/src/main/scala/org/kframework/definition/outer.scala
diff --git a/kernel/src/main/scala/org/kframework/definition/transformers.scala b/k-frontend/src/main/scala/org/kframework/definition/transformers.scala
similarity index 100%
rename from kernel/src/main/scala/org/kframework/definition/transformers.scala
rename to k-frontend/src/main/scala/org/kframework/definition/transformers.scala
diff --git a/kernel/src/main/scala/org/kframework/kore/ADT.scala b/k-frontend/src/main/scala/org/kframework/kore/ADT.scala
similarity index 100%
rename from kernel/src/main/scala/org/kframework/kore/ADT.scala
rename to k-frontend/src/main/scala/org/kframework/kore/ADT.scala
diff --git a/kernel/src/main/scala/org/kframework/kore/Assoc.scala b/k-frontend/src/main/scala/org/kframework/kore/Assoc.scala
similarity index 100%
rename from kernel/src/main/scala/org/kframework/kore/Assoc.scala
rename to k-frontend/src/main/scala/org/kframework/kore/Assoc.scala
diff --git a/kernel/src/main/scala/org/kframework/kore/Constructors.scala b/k-frontend/src/main/scala/org/kframework/kore/Constructors.scala
similarity index 100%
rename from kernel/src/main/scala/org/kframework/kore/Constructors.scala
rename to k-frontend/src/main/scala/org/kframework/kore/Constructors.scala
diff --git a/kernel/src/main/scala/org/kframework/kore/KORE.scala b/k-frontend/src/main/scala/org/kframework/kore/KORE.scala
similarity index 100%
rename from kernel/src/main/scala/org/kframework/kore/KORE.scala
rename to k-frontend/src/main/scala/org/kframework/kore/KORE.scala
diff --git a/kernel/src/main/scala/org/kframework/kore/Rich.scala b/k-frontend/src/main/scala/org/kframework/kore/Rich.scala
similarity index 100%
rename from kernel/src/main/scala/org/kframework/kore/Rich.scala
rename to k-frontend/src/main/scala/org/kframework/kore/Rich.scala
diff --git a/kernel/src/main/scala/org/kframework/kore/Unapply.scala b/k-frontend/src/main/scala/org/kframework/kore/Unapply.scala
similarity index 100%
rename from kernel/src/main/scala/org/kframework/kore/Unapply.scala
rename to k-frontend/src/main/scala/org/kframework/kore/Unapply.scala
diff --git a/kernel/src/main/scala/org/kframework/kore/interface.scala b/k-frontend/src/main/scala/org/kframework/kore/interface.scala
similarity index 100%
rename from kernel/src/main/scala/org/kframework/kore/interface.scala
rename to k-frontend/src/main/scala/org/kframework/kore/interface.scala
diff --git a/kernel/src/main/scala/org/kframework/kore/transformers.scala b/k-frontend/src/main/scala/org/kframework/kore/transformers.scala
similarity index 100%
rename from kernel/src/main/scala/org/kframework/kore/transformers.scala
rename to k-frontend/src/main/scala/org/kframework/kore/transformers.scala
diff --git a/kernel/src/main/scala/org/kframework/parser/Transformer.scala b/k-frontend/src/main/scala/org/kframework/parser/Transformer.scala
similarity index 100%
rename from kernel/src/main/scala/org/kframework/parser/Transformer.scala
rename to k-frontend/src/main/scala/org/kframework/parser/Transformer.scala
diff --git a/kernel/src/main/scala/org/kframework/parser/TreeNodesToKORE.scala b/k-frontend/src/main/scala/org/kframework/parser/TreeNodesToKORE.scala
similarity index 100%
rename from kernel/src/main/scala/org/kframework/parser/TreeNodesToKORE.scala
rename to k-frontend/src/main/scala/org/kframework/parser/TreeNodesToKORE.scala
diff --git a/kernel/src/main/scala/org/kframework/parser/kore/parser/KoreToK.scala b/k-frontend/src/main/scala/org/kframework/parser/kore/parser/KoreToK.scala
similarity index 100%
rename from kernel/src/main/scala/org/kframework/parser/kore/parser/KoreToK.scala
rename to k-frontend/src/main/scala/org/kframework/parser/kore/parser/KoreToK.scala
diff --git a/kernel/src/main/scala/org/kframework/parser/treeNodes.scala b/k-frontend/src/main/scala/org/kframework/parser/treeNodes.scala
similarity index 100%
rename from kernel/src/main/scala/org/kframework/parser/treeNodes.scala
rename to k-frontend/src/main/scala/org/kframework/parser/treeNodes.scala
diff --git a/kernel/src/main/scala/org/kframework/rewriter/Rewriter.scala b/k-frontend/src/main/scala/org/kframework/rewriter/Rewriter.scala
similarity index 100%
rename from kernel/src/main/scala/org/kframework/rewriter/Rewriter.scala
rename to k-frontend/src/main/scala/org/kframework/rewriter/Rewriter.scala
diff --git a/kernel/src/main/scala/org/kframework/unparser/KOREToTreeNodes.scala b/k-frontend/src/main/scala/org/kframework/unparser/KOREToTreeNodes.scala
similarity index 100%
rename from kernel/src/main/scala/org/kframework/unparser/KOREToTreeNodes.scala
rename to k-frontend/src/main/scala/org/kframework/unparser/KOREToTreeNodes.scala
diff --git a/kernel/src/main/scala/org/kframework/unparser/Unparse.scala b/k-frontend/src/main/scala/org/kframework/unparser/Unparse.scala
similarity index 100%
rename from kernel/src/main/scala/org/kframework/unparser/Unparse.scala
rename to k-frontend/src/main/scala/org/kframework/unparser/Unparse.scala
diff --git a/kernel/src/test/java/org/kframework/CollectionsTest.java b/k-frontend/src/test/java/org/kframework/CollectionsTest.java
similarity index 100%
rename from kernel/src/test/java/org/kframework/CollectionsTest.java
rename to k-frontend/src/test/java/org/kframework/CollectionsTest.java
diff --git a/kernel/src/test/java/org/kframework/POSetTest.java b/k-frontend/src/test/java/org/kframework/POSetTest.java
similarity index 100%
rename from kernel/src/test/java/org/kframework/POSetTest.java
rename to k-frontend/src/test/java/org/kframework/POSetTest.java
diff --git a/kernel/src/test/java/org/kframework/compile/AddParentsCellsTest.java b/k-frontend/src/test/java/org/kframework/compile/AddParentsCellsTest.java
similarity index 100%
rename from kernel/src/test/java/org/kframework/compile/AddParentsCellsTest.java
rename to k-frontend/src/test/java/org/kframework/compile/AddParentsCellsTest.java
diff --git a/kernel/src/test/java/org/kframework/compile/CloseCellsTest.java b/k-frontend/src/test/java/org/kframework/compile/CloseCellsTest.java
similarity index 100%
rename from kernel/src/test/java/org/kframework/compile/CloseCellsTest.java
rename to k-frontend/src/test/java/org/kframework/compile/CloseCellsTest.java
diff --git a/kernel/src/test/java/org/kframework/compile/ConstantFoldingTest.java b/k-frontend/src/test/java/org/kframework/compile/ConstantFoldingTest.java
similarity index 100%
rename from kernel/src/test/java/org/kframework/compile/ConstantFoldingTest.java
rename to k-frontend/src/test/java/org/kframework/compile/ConstantFoldingTest.java
diff --git a/kernel/src/test/java/org/kframework/compile/GenerateSentencesFromConfigDeclTest.java b/k-frontend/src/test/java/org/kframework/compile/GenerateSentencesFromConfigDeclTest.java
similarity index 100%
rename from kernel/src/test/java/org/kframework/compile/GenerateSentencesFromConfigDeclTest.java
rename to k-frontend/src/test/java/org/kframework/compile/GenerateSentencesFromConfigDeclTest.java
diff --git a/kernel/src/test/java/org/kframework/compile/NumberSentencesTest.java b/k-frontend/src/test/java/org/kframework/compile/NumberSentencesTest.java
similarity index 100%
rename from kernel/src/test/java/org/kframework/compile/NumberSentencesTest.java
rename to k-frontend/src/test/java/org/kframework/compile/NumberSentencesTest.java
diff --git a/kernel/src/test/java/org/kframework/compile/SortCellsTest.java b/k-frontend/src/test/java/org/kframework/compile/SortCellsTest.java
similarity index 100%
rename from kernel/src/test/java/org/kframework/compile/SortCellsTest.java
rename to k-frontend/src/test/java/org/kframework/compile/SortCellsTest.java
diff --git a/kernel/src/test/java/org/kframework/compile/TestConfiguration.java b/k-frontend/src/test/java/org/kframework/compile/TestConfiguration.java
similarity index 100%
rename from kernel/src/test/java/org/kframework/compile/TestConfiguration.java
rename to k-frontend/src/test/java/org/kframework/compile/TestConfiguration.java
diff --git a/kernel/src/test/java/org/kframework/kast/KastModuleTest.java b/k-frontend/src/test/java/org/kframework/kast/KastModuleTest.java
similarity index 100%
rename from kernel/src/test/java/org/kframework/kast/KastModuleTest.java
rename to k-frontend/src/test/java/org/kframework/kast/KastModuleTest.java
diff --git a/kernel/src/test/java/org/kframework/kompile/KompileFrontEndTest.java b/k-frontend/src/test/java/org/kframework/kompile/KompileFrontEndTest.java
similarity index 100%
rename from kernel/src/test/java/org/kframework/kompile/KompileFrontEndTest.java
rename to k-frontend/src/test/java/org/kframework/kompile/KompileFrontEndTest.java
diff --git a/kernel/src/test/java/org/kframework/kompile/KompileModuleTest.java b/k-frontend/src/test/java/org/kframework/kompile/KompileModuleTest.java
similarity index 100%
rename from kernel/src/test/java/org/kframework/kompile/KompileModuleTest.java
rename to k-frontend/src/test/java/org/kframework/kompile/KompileModuleTest.java
diff --git a/kernel/src/test/java/org/kframework/kompile/KompileOptionsTest.java b/k-frontend/src/test/java/org/kframework/kompile/KompileOptionsTest.java
similarity index 100%
rename from kernel/src/test/java/org/kframework/kompile/KompileOptionsTest.java
rename to k-frontend/src/test/java/org/kframework/kompile/KompileOptionsTest.java
diff --git a/kernel/src/test/java/org/kframework/kore/InterfaceTest.java b/k-frontend/src/test/java/org/kframework/kore/InterfaceTest.java
similarity index 100%
rename from kernel/src/test/java/org/kframework/kore/InterfaceTest.java
rename to k-frontend/src/test/java/org/kframework/kore/InterfaceTest.java
diff --git a/kernel/src/test/java/org/kframework/kore/VisitorTest.java b/k-frontend/src/test/java/org/kframework/kore/VisitorTest.java
similarity index 100%
rename from kernel/src/test/java/org/kframework/kore/VisitorTest.java
rename to k-frontend/src/test/java/org/kframework/kore/VisitorTest.java
diff --git a/kernel/src/test/java/org/kframework/lsp/LSPTests.java b/k-frontend/src/test/java/org/kframework/lsp/LSPTests.java
similarity index 100%
rename from kernel/src/test/java/org/kframework/lsp/LSPTests.java
rename to k-frontend/src/test/java/org/kframework/lsp/LSPTests.java
diff --git a/kernel/src/test/java/org/kframework/parser/inner/RuleGrammarTest.java b/k-frontend/src/test/java/org/kframework/parser/inner/RuleGrammarTest.java
similarity index 100%
rename from kernel/src/test/java/org/kframework/parser/inner/RuleGrammarTest.java
rename to k-frontend/src/test/java/org/kframework/parser/inner/RuleGrammarTest.java
diff --git a/kernel/src/test/java/org/kframework/parser/inner/disambiguation/AddEmptyListsTest.java b/k-frontend/src/test/java/org/kframework/parser/inner/disambiguation/AddEmptyListsTest.java
similarity index 100%
rename from kernel/src/test/java/org/kframework/parser/inner/disambiguation/AddEmptyListsTest.java
rename to k-frontend/src/test/java/org/kframework/parser/inner/disambiguation/AddEmptyListsTest.java
diff --git a/kernel/src/test/java/org/kframework/parser/json/JsonSerializationTests.java b/k-frontend/src/test/java/org/kframework/parser/json/JsonSerializationTests.java
similarity index 100%
rename from kernel/src/test/java/org/kframework/parser/json/JsonSerializationTests.java
rename to k-frontend/src/test/java/org/kframework/parser/json/JsonSerializationTests.java
diff --git a/kernel/src/test/java/org/kframework/parser/outer/MDsourceTest.java b/k-frontend/src/test/java/org/kframework/parser/outer/MDsourceTest.java
similarity index 100%
rename from kernel/src/test/java/org/kframework/parser/outer/MDsourceTest.java
rename to k-frontend/src/test/java/org/kframework/parser/outer/MDsourceTest.java
diff --git a/kernel/src/test/java/org/kframework/parser/outer/OuterParsingTests.java b/k-frontend/src/test/java/org/kframework/parser/outer/OuterParsingTests.java
similarity index 100%
rename from kernel/src/test/java/org/kframework/parser/outer/OuterParsingTests.java
rename to k-frontend/src/test/java/org/kframework/parser/outer/OuterParsingTests.java
diff --git a/kernel/src/test/java/org/kframework/unparser/AddBracketsTest.java b/k-frontend/src/test/java/org/kframework/unparser/AddBracketsTest.java
similarity index 100%
rename from kernel/src/test/java/org/kframework/unparser/AddBracketsTest.java
rename to k-frontend/src/test/java/org/kframework/unparser/AddBracketsTest.java
diff --git a/kernel/src/test/java/org/kframework/unparser/KPrintTest.java b/k-frontend/src/test/java/org/kframework/unparser/KPrintTest.java
similarity index 100%
rename from kernel/src/test/java/org/kframework/unparser/KPrintTest.java
rename to k-frontend/src/test/java/org/kframework/unparser/KPrintTest.java
diff --git a/kernel/src/test/java/org/kframework/utils/BaseTestCase.java b/k-frontend/src/test/java/org/kframework/utils/BaseTestCase.java
similarity index 100%
rename from kernel/src/test/java/org/kframework/utils/BaseTestCase.java
rename to k-frontend/src/test/java/org/kframework/utils/BaseTestCase.java
diff --git a/kernel/src/test/java/org/kframework/utils/ColorUtilTest.java b/k-frontend/src/test/java/org/kframework/utils/ColorUtilTest.java
similarity index 100%
rename from kernel/src/test/java/org/kframework/utils/ColorUtilTest.java
rename to k-frontend/src/test/java/org/kframework/utils/ColorUtilTest.java
diff --git a/kernel/src/test/java/org/kframework/utils/IOTestCase.java b/k-frontend/src/test/java/org/kframework/utils/IOTestCase.java
similarity index 100%
rename from kernel/src/test/java/org/kframework/utils/IOTestCase.java
rename to k-frontend/src/test/java/org/kframework/utils/IOTestCase.java
diff --git a/kernel/src/test/java/org/kframework/utils/StringUtilTest.java b/k-frontend/src/test/java/org/kframework/utils/StringUtilTest.java
similarity index 100%
rename from kernel/src/test/java/org/kframework/utils/StringUtilTest.java
rename to k-frontend/src/test/java/org/kframework/utils/StringUtilTest.java
diff --git a/kernel/src/test/java/org/kframework/utils/inject/DefinitionLoadingModuleTest.java b/k-frontend/src/test/java/org/kframework/utils/inject/DefinitionLoadingModuleTest.java
similarity index 100%
rename from kernel/src/test/java/org/kframework/utils/inject/DefinitionLoadingModuleTest.java
rename to k-frontend/src/test/java/org/kframework/utils/inject/DefinitionLoadingModuleTest.java
diff --git a/kernel/src/test/resources/.gitattributes b/k-frontend/src/test/resources/.gitattributes
similarity index 100%
rename from kernel/src/test/resources/.gitattributes
rename to k-frontend/src/test/resources/.gitattributes
diff --git a/kernel/src/test/resources/convertor-tests/kore.k b/k-frontend/src/test/resources/convertor-tests/kore.k
similarity index 100%
rename from kernel/src/test/resources/convertor-tests/kore.k
rename to k-frontend/src/test/resources/convertor-tests/kore.k
diff --git a/kernel/src/test/resources/fs-test.txt b/k-frontend/src/test/resources/fs-test.txt
similarity index 100%
rename from kernel/src/test/resources/fs-test.txt
rename to k-frontend/src/test/resources/fs-test.txt
diff --git a/kernel/src/test/resources/kast-data.kast b/k-frontend/src/test/resources/kast-data.kast
similarity index 100%
rename from kernel/src/test/resources/kast-data.kast
rename to k-frontend/src/test/resources/kast-data.kast
diff --git a/kernel/src/test/resources/kast/quote-unquote.kore b/k-frontend/src/test/resources/kast/quote-unquote.kore
similarity index 100%
rename from kernel/src/test/resources/kast/quote-unquote.kore
rename to k-frontend/src/test/resources/kast/quote-unquote.kore
diff --git a/kernel/src/test/resources/kmp/marker b/k-frontend/src/test/resources/kmp/marker
similarity index 100%
rename from kernel/src/test/resources/kmp/marker
rename to k-frontend/src/test/resources/kmp/marker
diff --git a/kernel/src/test/resources/test-kompiled/marker b/k-frontend/src/test/resources/test-kompiled/marker
similarity index 100%
rename from kernel/src/test/resources/test-kompiled/marker
rename to k-frontend/src/test/resources/test-kompiled/marker
diff --git a/kernel/src/test/scala/org/kframework/definition/OuterTest.scala b/k-frontend/src/test/scala/org/kframework/definition/OuterTest.scala
similarity index 100%
rename from kernel/src/test/scala/org/kframework/definition/OuterTest.scala
rename to k-frontend/src/test/scala/org/kframework/definition/OuterTest.scala
diff --git a/kernel/src/test/scala/org/kframework/definition/VisitorTest.scala b/k-frontend/src/test/scala/org/kframework/definition/VisitorTest.scala
similarity index 100%
rename from kernel/src/test/scala/org/kframework/definition/VisitorTest.scala
rename to k-frontend/src/test/scala/org/kframework/definition/VisitorTest.scala
diff --git a/kernel/src/test/scala/org/kframework/unparser/UnparseTest.scala b/k-frontend/src/test/scala/org/kframework/unparser/UnparseTest.scala
similarity index 100%
rename from kernel/src/test/scala/org/kframework/unparser/UnparseTest.scala
rename to k-frontend/src/test/scala/org/kframework/unparser/UnparseTest.scala
diff --git a/llvm-backend/pom.xml b/llvm-backend/pom.xml
index 3c73a895db1..08dc079f916 100644
--- a/llvm-backend/pom.xml
+++ b/llvm-backend/pom.xml
@@ -16,7 +16,7 @@
com.runtimeverification.k
- kernel
+ k-frontend
${project.version}
diff --git a/pom.xml b/pom.xml
index 104db1bab61..ceaebefaf51 100644
--- a/pom.xml
+++ b/pom.xml
@@ -9,7 +9,7 @@
K Framework Tool Parent
- kernel
+ k-frontend
k-distribution
haskell-backend
llvm-backend