Skip to content

Commit

Permalink
Apply Java 17 automatic migration: enhanced switch (#3745)
Browse files Browse the repository at this point in the history 
This PR applies a **purely mechanical** upgrade of `switch` statements
in the K repository to use the new "enhanced" syntax from Java 17. I
have not altered any code here by hand; the results are obtained only
via IntelliJ's refactoring tools.
  • Loading branch information
@Baltoli
Baltoli authored Oct 24, 2023
1 parent b1fcdbc commit 0bbfe47
Show file tree
Hide file tree
Showing 18 changed files with 314 additions and 441 deletions.
78 changes: 28 additions & 50 deletions kernel/src/main/java/org/kframework/backend/kore/ModuleToKORE.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1696,38 +1696,23 @@ private Production production(KApply term, boolean instantiatePolySorts) {
}

private static String convertBuiltinLabel(String klabel) {
switch(klabel) {
case "#Bottom":
return "\\bottom";
case "#Top":
return "\\top";
case "#Or":
return "\\or";
case "#And":
return "\\and";
case "#Not":
return "\\not";
case "#Floor":
return "\\floor";
case "#Ceil":
return "\\ceil";
case "#Equals":
return "\\equals";
case "#Implies":
return "\\implies";
case "#Exists":
return "\\exists";
case "#Forall":
return "\\forall";
case "#AG":
return "allPathGlobally";
case "weakExistsFinally":
return ONE_PATH_OP;
case "weakAlwaysFinally":
return ALL_PATH_OP;
default:
throw KEMException.compilerError("Unsuppored kore connective in rule: " + klabel);
}
return switch (klabel) {
case "#Bottom" -> "\\bottom";
case "#Top" -> "\\top";
case "#Or" -> "\\or";
case "#And" -> "\\and";
case "#Not" -> "\\not";
case "#Floor" -> "\\floor";
case "#Ceil" -> "\\ceil";
case "#Equals" -> "\\equals";
case "#Implies" -> "\\implies";
case "#Exists" -> "\\exists";
case "#Forall" -> "\\forall";
case "#AG" -> "allPathGlobally";
case "weakExistsFinally" -> ONE_PATH_OP;
case "weakAlwaysFinally" -> ALL_PATH_OP;
default -> throw KEMException.compilerError("Unsuppored kore connective in rule: " + klabel);
};
}

public static void convert(KLabel klabel, StringBuilder sb) {
Expand Down Expand Up @@ -1858,14 +1843,12 @@ private void convert(Map<Att.Key, Boolean> attributes, Att att, StringBuilder sb
convertStringVarList(location, freeVarsMap, strVal, sb);
} else {
switch (strKey) {
case "unit":
case "element":
Production prod = production(KApply(KLabel(strVal)));
convert(prod.klabel().get(), prod.params(), sb);
sb.append("()");
break;
default:
sb.append(StringUtil.enquoteKString(strVal));
case "unit", "element" -> {
Production prod = production(KApply(KLabel(strVal)));
convert(prod.klabel().get(), prod.params(), sb);
sb.append("()");
}
default -> sb.append(StringUtil.enquoteKString(strVal));
}
}
sb.append(")");
Expand Down Expand Up @@ -1911,18 +1894,13 @@ private static String[] asciiReadableEncodingKoreCalc() {
public static String[] asciiReadableEncodingKore = asciiReadableEncodingKoreCalc();

private static void convert(String name, StringBuilder sb) {
switch(name) {
case "module":
case "endmodule":
case "sort":
case "hooked-sort":
case "symbol":
case "hooked-symbol":
case "alias":
case "axiom":
switch (name) {
case "module", "endmodule", "sort", "hooked-sort", "symbol", "hooked-symbol", "alias", "axiom" -> {
sb.append(name).append("'Kywd'");
return;
default: break;
}
default -> {
}
}
StringBuilder buffer = new StringBuilder();
StringUtil.encodeStringToAlphanumeric(buffer, name, asciiReadableEncodingKore, identChar, "'");
Expand Down
38 changes: 14 additions & 24 deletions kernel/src/main/java/org/kframework/compile/ConstantFolding.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -85,33 +85,23 @@ public K apply(KApply k) {
}

private Class<?> classOf(String hook) {
switch(hook) {
case "BOOL.Bool":
return boolean.class;
case "FLOAT.Float":
return FloatBuiltin.class;
case "INT.Int":
return BigInteger.class;
case "STRING.String":
return String.class;
default:
return String.class;
}
return switch (hook) {
case "BOOL.Bool" -> boolean.class;
case "FLOAT.Float" -> FloatBuiltin.class;
case "INT.Int" -> BigInteger.class;
case "STRING.String" -> String.class;
default -> String.class;
};
}

private Object unwrap(String token, String hook) {
switch(hook) {
case "BOOL.Bool":
return Boolean.valueOf(token);
case "FLOAT.Float":
return FloatBuiltin.of(token);
case "INT.Int":
return new BigInteger(token);
case "STRING.String":
return StringUtil.unquoteKString(token);
default:
return token;
}
return switch (hook) {
case "BOOL.Bool" -> Boolean.valueOf(token);
case "FLOAT.Float" -> FloatBuiltin.of(token);
case "INT.Int" -> new BigInteger(token);
case "STRING.String" -> StringUtil.unquoteKString(token);
default -> token;
};
}

private K wrap(Object result, Sort sort, Module module) {
Expand Down
11 changes: 4 additions & 7 deletions kernel/src/main/java/org/kframework/kast/KastFrontEnd.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -184,13 +184,10 @@ public int run() {

if (options.module == null) {
options.module = def.mainSyntaxModuleName();
switch (options.input) {
case KORE:
unparsingMod = def.languageParsingModule();
break;
default:
unparsingMod = def.kompiledDefinition.getModule(def.mainSyntaxModuleName()).get();
}
unparsingMod = switch (options.input) {
case KORE -> def.languageParsingModule();
default -> def.kompiledDefinition.getModule(def.mainSyntaxModuleName()).get();
};
} else {
Option<Module> maybeUnparsingMod = def.kompiledDefinition.getModule(options.module);
if (maybeUnparsingMod.isEmpty()) {
Expand Down
14 changes: 4 additions & 10 deletions kernel/src/main/java/org/kframework/kil/StringSentence.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -24,16 +24,10 @@ public StringSentence(String content, int contentStartLine, int contentStartColu

@Override
public void toString(StringBuilder sb) {
switch(type) {
case "config":
sb.append(" configuration ");
break;
case "alias":
sb.append(" context alias ");
break;
default:
sb.append(" ").append(type).append(" ");
break;
switch (type) {
case "config" -> sb.append(" configuration ");
case "alias" -> sb.append(" context alias ");
default -> sb.append(" ").append(type).append(" ");
}
if (!label.equals("")) {
sb.append("[").append(label).append("]: ");
Expand Down
77 changes: 29 additions & 48 deletions kernel/src/main/java/org/kframework/kompile/DefinitionParsing.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -576,74 +576,55 @@ private Sentence upSentence(K contents, String sentenceType) {
private Claim upClaim(K contents) {
KApply ruleContents = (KApply) contents;
List<org.kframework.kore.K> items = ruleContents.klist().items();
switch (ruleContents.klabel().name()) {
case "#ruleNoConditions":
return Claim(items.get(0), BooleanUtils.TRUE, BooleanUtils.TRUE, ruleContents.att());
case "#ruleRequires":
return Claim(items.get(0), items.get(1), BooleanUtils.TRUE, ruleContents.att());
case "#ruleEnsures":
return Claim(items.get(0), BooleanUtils.TRUE, items.get(1), ruleContents.att());
case "#ruleRequiresEnsures":
return Claim(items.get(0), items.get(1), items.get(2), ruleContents.att());
default:
throw new AssertionError("Wrong KLabel for claim content");
}
return switch (ruleContents.klabel().name()) {
case "#ruleNoConditions" -> Claim(items.get(0), BooleanUtils.TRUE, BooleanUtils.TRUE, ruleContents.att());
case "#ruleRequires" -> Claim(items.get(0), items.get(1), BooleanUtils.TRUE, ruleContents.att());
case "#ruleEnsures" -> Claim(items.get(0), BooleanUtils.TRUE, items.get(1), ruleContents.att());
case "#ruleRequiresEnsures" -> Claim(items.get(0), items.get(1), items.get(2), ruleContents.att());
default -> throw new AssertionError("Wrong KLabel for claim content");
};
}

private Rule upRule(K contents) {
KApply ruleContents = (KApply) contents;
List<org.kframework.kore.K> items = ruleContents.klist().items();
switch (ruleContents.klabel().name()) {
case "#ruleNoConditions":
return Rule(items.get(0), BooleanUtils.TRUE, BooleanUtils.TRUE, ruleContents.att());
case "#ruleRequires":
return Rule(items.get(0), items.get(1), BooleanUtils.TRUE, ruleContents.att());
case "#ruleEnsures":
return Rule(items.get(0), BooleanUtils.TRUE, items.get(1), ruleContents.att());
case "#ruleRequiresEnsures":
return Rule(items.get(0), items.get(1), items.get(2), ruleContents.att());
default:
throw new AssertionError("Wrong KLabel for rule content");
}
return switch (ruleContents.klabel().name()) {
case "#ruleNoConditions" -> Rule(items.get(0), BooleanUtils.TRUE, BooleanUtils.TRUE, ruleContents.att());
case "#ruleRequires" -> Rule(items.get(0), items.get(1), BooleanUtils.TRUE, ruleContents.att());
case "#ruleEnsures" -> Rule(items.get(0), BooleanUtils.TRUE, items.get(1), ruleContents.att());
case "#ruleRequiresEnsures" -> Rule(items.get(0), items.get(1), items.get(2), ruleContents.att());
default -> throw new AssertionError("Wrong KLabel for rule content");
};
}

private Context upContext(K contents) {
KApply ruleContents = (KApply) contents;
List<K> items = ruleContents.klist().items();
switch (ruleContents.klabel().name()) {
case "#ruleNoConditions":
return Context(items.get(0), BooleanUtils.TRUE, ruleContents.att());
case "#ruleRequires":
return Context(items.get(0), items.get(1), ruleContents.att());
default:
throw KEMException.criticalError("Illegal context with ensures clause detected.", contents);
}
return switch (ruleContents.klabel().name()) {
case "#ruleNoConditions" -> Context(items.get(0), BooleanUtils.TRUE, ruleContents.att());
case "#ruleRequires" -> Context(items.get(0), items.get(1), ruleContents.att());
default -> throw KEMException.criticalError("Illegal context with ensures clause detected.", contents);
};
}

private ContextAlias upAlias(K contents) {
KApply ruleContents = (KApply) contents;
List<K> items = ruleContents.klist().items();
switch (ruleContents.klabel().name()) {
case "#ruleNoConditions":
return ContextAlias(items.get(0), BooleanUtils.TRUE, ruleContents.att());
case "#ruleRequires":
return ContextAlias(items.get(0), items.get(1), ruleContents.att());
default:
throw KEMException.criticalError("Illegal context alias with ensures clause detected.", contents);
}
return switch (ruleContents.klabel().name()) {
case "#ruleNoConditions" -> ContextAlias(items.get(0), BooleanUtils.TRUE, ruleContents.att());
case "#ruleRequires" -> ContextAlias(items.get(0), items.get(1), ruleContents.att());
default -> throw KEMException.criticalError("Illegal context alias with ensures clause detected.", contents);
};
}

private Configuration upConfiguration(K contents) {
KApply configContents = (KApply) contents;
List<K> items = configContents.klist().items();
switch (configContents.klabel().name()) {
case "#ruleNoConditions":
return Configuration(items.get(0), BooleanUtils.TRUE, configContents.att());
case "#ruleEnsures":
return Configuration(items.get(0), items.get(1), configContents.att());
default:
throw KEMException.compilerError("Illegal configuration with requires clause detected.", configContents);
}
return switch (configContents.klabel().name()) {
case "#ruleNoConditions" -> Configuration(items.get(0), BooleanUtils.TRUE, configContents.att());
case "#ruleEnsures" -> Configuration(items.get(0), items.get(1), configContents.att());
default -> throw KEMException.compilerError("Illegal configuration with requires clause detected.", configContents);
};
}

private ParseCache loadCache(Module parser) {
Expand Down
16 changes: 6 additions & 10 deletions kernel/src/main/java/org/kframework/kore/convertors/KILtoKORE.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -136,16 +136,12 @@ public org.kframework.definition.SyntaxAssociativity apply(PriorityExtendedAssoc

public Associativity applyAssoc(String assocOrig) {
// "left", "right", "non-assoc"
switch (assocOrig) {
case "left":
return Associativity.Left;
case "right":
return Associativity.Right;
case "non-assoc":
return Associativity.NonAssoc;
default:
throw new AssertionError("Incorrect assoc string: " + assocOrig);
}
return switch (assocOrig) {
case "left" -> Associativity.Left;
case "right" -> Associativity.Right;
case "non-assoc" -> Associativity.NonAssoc;
default -> throw new AssertionError("Incorrect assoc string: " + assocOrig);
};
}

public Set<org.kframework.definition.Sentence> apply(PriorityExtended pe) {
Expand Down
44 changes: 22 additions & 22 deletions kernel/src/main/java/org/kframework/lsp/TextDocumentSyncHandler.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -175,28 +175,28 @@ public CompletableFuture<Either<List<CompletionItem>, CompletionList>> completio
String context = doc.getContextAt(pos);
List<DefinitionItem> allDi = slurp(position.getTextDocument().getUri());
switch (context) {
case "":
lci.add(getNewRequiresCompletion());
lci.add(getNewModuleCompletion()); break;
case "endmodule":
lci.add(getNewModuleCompletion()); break;
case "module":
lci.add(getNewImportCompletion());
lci.addAll(getNewSentenceCompletion()); break;
case "import":
case "imports":
lci.add(getNewImportCompletion());
lci.addAll(getNewSentenceCompletion());
lci.addAll(getImportCompletion(allDi)); break;
case "syntax":
lci.addAll(getNewSentenceCompletion());
lci.addAll(getSyntaxCompletion(allDi)); break;
case "context":
case "rule":
case "configuration":
case "claim":
lci.addAll(getNewSentenceCompletion());
lci.addAll(getRuleCompletion(allDi)); break;
case "" -> {
lci.add(getNewRequiresCompletion());
lci.add(getNewModuleCompletion());
}
case "endmodule" -> lci.add(getNewModuleCompletion());
case "module" -> {
lci.add(getNewImportCompletion());
lci.addAll(getNewSentenceCompletion());
}
case "import", "imports" -> {
lci.add(getNewImportCompletion());
lci.addAll(getNewSentenceCompletion());
lci.addAll(getImportCompletion(allDi));
}
case "syntax" -> {
lci.addAll(getNewSentenceCompletion());
lci.addAll(getSyntaxCompletion(allDi));
}
case "context", "rule", "configuration", "claim" -> {
lci.addAll(getNewSentenceCompletion());
lci.addAll(getRuleCompletion(allDi));
}
}
this.clientLogger.logMessage("Operation '" + "text/completion: " + position.getTextDocument().getUri() + " #pos: "
+ pos.getLine() + " " + pos.getCharacter() + " context: " + context + " #: " + lci.size());
Expand Down
Loading

0 comments on commit 0bbfe47

Please sign in to comment.