diff --git a/kernel/src/main/java/org/kframework/backend/kore/ModuleToKORE.java b/kernel/src/main/java/org/kframework/backend/kore/ModuleToKORE.java index a00ac5b32a8..ac85673bfba 100644 --- a/kernel/src/main/java/org/kframework/backend/kore/ModuleToKORE.java +++ b/kernel/src/main/java/org/kframework/backend/kore/ModuleToKORE.java @@ -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) { @@ -1858,14 +1843,12 @@ private void convert(Map 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(")"); @@ -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, "'"); diff --git a/kernel/src/main/java/org/kframework/compile/ConstantFolding.java b/kernel/src/main/java/org/kframework/compile/ConstantFolding.java index da6bef9dd05..1fb51489e3b 100644 --- a/kernel/src/main/java/org/kframework/compile/ConstantFolding.java +++ b/kernel/src/main/java/org/kframework/compile/ConstantFolding.java @@ -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) { diff --git a/kernel/src/main/java/org/kframework/kast/KastFrontEnd.java b/kernel/src/main/java/org/kframework/kast/KastFrontEnd.java index 0f539ee397a..0b8ed8c45fe 100644 --- a/kernel/src/main/java/org/kframework/kast/KastFrontEnd.java +++ b/kernel/src/main/java/org/kframework/kast/KastFrontEnd.java @@ -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 maybeUnparsingMod = def.kompiledDefinition.getModule(options.module); if (maybeUnparsingMod.isEmpty()) { diff --git a/kernel/src/main/java/org/kframework/kil/StringSentence.java b/kernel/src/main/java/org/kframework/kil/StringSentence.java index 87e1d1a2fd7..beb00217d24 100644 --- a/kernel/src/main/java/org/kframework/kil/StringSentence.java +++ b/kernel/src/main/java/org/kframework/kil/StringSentence.java @@ -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("]: "); diff --git a/kernel/src/main/java/org/kframework/kompile/DefinitionParsing.java b/kernel/src/main/java/org/kframework/kompile/DefinitionParsing.java index 6eabf9d788f..bfa4dab18b3 100644 --- a/kernel/src/main/java/org/kframework/kompile/DefinitionParsing.java +++ b/kernel/src/main/java/org/kframework/kompile/DefinitionParsing.java @@ -576,74 +576,55 @@ private Sentence upSentence(K contents, String sentenceType) { private Claim upClaim(K contents) { KApply ruleContents = (KApply) contents; List 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 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 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 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 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) { diff --git a/kernel/src/main/java/org/kframework/kore/convertors/KILtoKORE.java b/kernel/src/main/java/org/kframework/kore/convertors/KILtoKORE.java index c595e194d48..af7e7bbaa2c 100644 --- a/kernel/src/main/java/org/kframework/kore/convertors/KILtoKORE.java +++ b/kernel/src/main/java/org/kframework/kore/convertors/KILtoKORE.java @@ -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 apply(PriorityExtended pe) { diff --git a/kernel/src/main/java/org/kframework/lsp/TextDocumentSyncHandler.java b/kernel/src/main/java/org/kframework/lsp/TextDocumentSyncHandler.java index e4cd1d88c23..f79b7318780 100644 --- a/kernel/src/main/java/org/kframework/lsp/TextDocumentSyncHandler.java +++ b/kernel/src/main/java/org/kframework/lsp/TextDocumentSyncHandler.java @@ -175,28 +175,28 @@ public CompletableFuture, CompletionList>> completio String context = doc.getContextAt(pos); List 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()); diff --git a/kernel/src/main/java/org/kframework/parser/KRead.java b/kernel/src/main/java/org/kframework/parser/KRead.java index 867851c956c..58642dd00fb 100644 --- a/kernel/src/main/java/org/kframework/parser/KRead.java +++ b/kernel/src/main/java/org/kframework/parser/KRead.java @@ -60,20 +60,13 @@ public K prettyRead(Module mod, Sort sort, String startSymbolLocation, CompiledD } public K prettyRead(Module mod, Sort sort, String startSymbolLocation, CompiledDefinition def, Source source, String stringToParse, InputModes inputMode, boolean partialParseDebug) { - switch (inputMode) { - case BINARY: - case JSON: - case KAST: - return deserialize(stringToParse, inputMode, source); - case KORE: - return new KoreParser(mod.sortAttributesFor()).parseString(stringToParse); - case PROGRAM: - return def.parseSingleTerm(mod, sort, startSymbolLocation, kem, files, stringToParse, source, partialParseDebug); - case RULE: - throw KEMException.internalError("Should have been handled directly by the kast front end: " + inputMode); - default: - throw KEMException.criticalError("Unsupported input mode: " + inputMode); - } + return switch (inputMode) { + case BINARY, JSON, KAST -> deserialize(stringToParse, inputMode, source); + case KORE -> new KoreParser(mod.sortAttributesFor()).parseString(stringToParse); + case PROGRAM -> def.parseSingleTerm(mod, sort, startSymbolLocation, kem, files, stringToParse, source, partialParseDebug); + case RULE -> throw KEMException.internalError("Should have been handled directly by the kast front end: " + inputMode); + default -> throw KEMException.criticalError("Unsupported input mode: " + inputMode); + }; } public void createBisonParser(Module mod, Sort sort, File outputFile, boolean glr, String bisonFile, long stackDepth, boolean library) { @@ -143,16 +136,12 @@ public K deserialize(String stringToParse, Source source) { } public static K deserialize(String stringToParse, InputModes inputMode, Source source) { - switch (inputMode) { - case BINARY: - return BinaryParser.parse(stringToParse.getBytes()); - case JSON: - return JsonParser.parse(stringToParse); - case KAST: - return KastParser.parse(stringToParse, source); - default: - throw KEMException.criticalError("Unsupported input mode for deserialization: " + inputMode); - } + return switch (inputMode) { + case BINARY -> BinaryParser.parse(stringToParse.getBytes()); + case JSON -> JsonParser.parse(stringToParse); + case KAST -> KastParser.parse(stringToParse, source); + default -> throw KEMException.criticalError("Unsupported input mode for deserialization: " + inputMode); + }; } public static K autoDeserialize(byte[] kast, Source source) { diff --git a/kernel/src/main/java/org/kframework/parser/inner/disambiguation/TypeInferenceVisitor.java b/kernel/src/main/java/org/kframework/parser/inner/disambiguation/TypeInferenceVisitor.java index 1fe2654aee4..bb8dc27508d 100644 --- a/kernel/src/main/java/org/kframework/parser/inner/disambiguation/TypeInferenceVisitor.java +++ b/kernel/src/main/java/org/kframework/parser/inner/disambiguation/TypeInferenceVisitor.java @@ -94,22 +94,24 @@ public Either, Term> apply(Term t) { // skip the rest as there is nothing to infer return Right.apply(t); } - switch(inferencer.status()) { - case SATISFIABLE: + switch (inferencer.status()) { + case SATISFIABLE -> { // there is at least one solution, so compute it and pop the soft constraints inferencer.computeModel(); inferencer.pop(); - break; - case UNKNOWN: + } + case UNKNOWN -> { // constraints could not be solved, so error inferencer.pop(); throw KEMException.internalError("Could not solve sort constraints.", t); - case UNSATISFIABLE: + } + case UNSATISFIABLE -> { // no solutions exist. This is a type error, so ask the inferencer for an error message and return inferencer.pop(); Set kex = inferencer.error(); return Left.apply(kex); } + } boolean hasAnotherSolution = true; Set> models = new HashSet<>(); boolean once = true; @@ -122,38 +124,36 @@ public Either, Term> apply(Term t) { boolean isMaximal = false; do { inferencer.pushGreater(); - switch(inferencer.status()) { - case SATISFIABLE: - // is not maximal, keep going - isMaximal = false; - inferencer.computeModel(); - inferencer.pop(); - break; - case UNKNOWN: - // constraints coiuld not be solved, so error - throw KEMException.internalError("Could not solve sortconstraints.", t); - case UNSATISFIABLE: - isMaximal = true; - inferencer.pop(); - break; + switch (inferencer.status()) { + case SATISFIABLE -> { + // is not maximal, keep going + isMaximal = false; + inferencer.computeModel(); + inferencer.pop(); + } + case UNKNOWN -> + // constraints coiuld not be solved, so error + throw KEMException.internalError("Could not solve sortconstraints.", t); + case UNSATISFIABLE -> { + isMaximal = true; + inferencer.pop(); + } } } while (!isMaximal); models.add(inferencer.getModel()); // assert that we don't want any solutions less than this one inferencer.pushNotModel(); - switch(inferencer.status()) { - case SATISFIABLE: - // found another solution, keep going - hasAnotherSolution = true; - break; - case UNKNOWN: - // constraints could not be solved, so error - throw KEMException.internalError("Could not solve sort constraints.", t); - case UNSATISFIABLE: - // no more solutions, terminate loop - hasAnotherSolution = false; - break; - } + hasAnotherSolution = switch (inferencer.status()) { + case SATISFIABLE -> + // found another solution, keep going + true; + case UNKNOWN -> + // constraints could not be solved, so error + throw KEMException.internalError("Could not solve sort constraints.", t); + case UNSATISFIABLE -> + // no more solutions, terminate loop + false; + }; } while (hasAnotherSolution); // remove all models that are not maximal Set candidates = new HashSet<>(); diff --git a/kernel/src/main/java/org/kframework/parser/inner/disambiguation/TypeInferencer.java b/kernel/src/main/java/org/kframework/parser/inner/disambiguation/TypeInferencer.java index 215d7176d67..362fc8429ee 100644 --- a/kernel/src/main/java/org/kframework/parser/inner/disambiguation/TypeInferencer.java +++ b/kernel/src/main/java/org/kframework/parser/inner/disambiguation/TypeInferencer.java @@ -238,16 +238,15 @@ private void replayConstraints(List constraints) { println("))"); status = null; Status status = status(); - switch(status) { - case SATISFIABLE: + switch (status) { + case SATISFIABLE -> { println("(pop)"); print("(assert (and "); print(constraint.smt); println("))"); - break; - case UNKNOWN: - throw KEMException.internalError("Could not solve sort constraints.", currentTerm); - case UNSATISFIABLE: + } + case UNKNOWN -> throw KEMException.internalError("Could not solve sort constraints.", currentTerm); + case UNSATISFIABLE -> { println("(pop)"); computeStatus(); if (constraint.name != null) { @@ -260,6 +259,7 @@ private void replayConstraints(List constraints) { throw new LocalizedError("Unexpected sort " + actualSort + " for term parsed as production " + constraint.actualParams.get().production() + ". Expected: " + expectedSort, constraint.actualParams.get()); } } + } } } @@ -797,17 +797,12 @@ private Status computeStatus() { throw KEMException.internalError("Unexpected EOF reached while waiting for response from z3.", currentTerm); } } while (!result.equals("sat") && !result.equals("unsat") && !result.equals("unknown") && !result.equals("timeout") && !result.startsWith("(error")); - switch (result) { - case "sat": - return Status.SATISFIABLE; - case "unsat": - return Status.UNSATISFIABLE; - case "unknown": - case "timeout": - return Status.UNKNOWN; - default: - throw KEMException.internalError("Unexpected result from z3: " + result, currentTerm); - } + return switch (result) { + case "sat" -> Status.SATISFIABLE; + case "unsat" -> Status.UNSATISFIABLE; + case "unknown", "timeout" -> Status.UNKNOWN; + default -> throw KEMException.internalError("Unexpected result from z3: " + result, currentTerm); + }; } catch (IOException e) { throw KEMException.internalError("Could not read from z3 process", e, currentTerm); } diff --git a/kernel/src/main/java/org/kframework/parser/json/JsonParser.java b/kernel/src/main/java/org/kframework/parser/json/JsonParser.java index 35f1373d000..54cf32d61b4 100644 --- a/kernel/src/main/java/org/kframework/parser/json/JsonParser.java +++ b/kernel/src/main/java/org/kframework/parser/json/JsonParser.java @@ -168,94 +168,93 @@ public static FlatModule toFlatModule(JsonObject data) throws IOException { /////////////////////////// public static Sentence toSentence(JsonObject data) { - switch(data.getString("node")) { - case KCONTEXT: { - K body = toK(data.getJsonObject("body")); - K requires = toK(data.getJsonObject("requires")); - Att att = toAtt(data.getJsonObject("att")); - return new Context(body, requires, att); - } - case KRULE: { - K body = toK(data.getJsonObject("body")); - K requires = toK(data.getJsonObject("requires")); - K ensures = toK(data.getJsonObject("ensures")); - Att att = toAtt(data.getJsonObject("att")); - return new Rule(body, requires, ensures, att); - } - case KCLAIM: { - K body = toK(data.getJsonObject("body")); - K requires = toK(data.getJsonObject("requires")); - K ensures = toK(data.getJsonObject("ensures")); - Att att = toAtt(data.getJsonObject("att")); - return new Claim(body, requires, ensures, att); - } - case KSYNTAXPRIORITY: { - JsonArray priorities = data.getJsonArray("priorities"); - Att att = toAtt(data.getJsonObject("att")); - List> syntaxPriorities = new ArrayList<>(); - priorities.getValuesAs(JsonArray.class).forEach(tags -> syntaxPriorities.add(toTags(tags))); - return new SyntaxPriority(immutable(syntaxPriorities), att); - } - case KSYNTAXASSOCIATIVITY: { - String assocString = data.getString("assoc"); - Associativity assoc = "Left".equals(assocString) ? Associativity.Left - : "Right".equals(assocString) ? Associativity.Right - : "NonAssoc".equals(assocString) ? Associativity.NonAssoc - : Associativity.Unspecified; - scala.collection.Set tags = toTags(data.getJsonArray("tags")); - Att att = toAtt(data.getJsonObject("att")); - return new SyntaxAssociativity(assoc, tags, att); - } - case KCONFIGURATION: { - K body = toK(data.getJsonObject("body")); - K ensures = toK(data.getJsonObject("ensures")); - Att att = toAtt(data.getJsonObject("att")); - return new Configuration(body, ensures, att); - } - case KSYNTAXSORT: { - Sort sort = toSort(data.getJsonObject("sort")); - Att att = toAtt(data.getJsonObject("att")); - List params = new ArrayList<>(); - for (JsonObject s : data.getJsonArray("params").getValuesAs(JsonObject.class)) { - params.add(toSort(s)); - } - return new SyntaxSort(immutable(params), sort, att); - } - case KSORTSYNONYM: { - Sort newSort = toSort(data.getJsonObject("newSort")); - Sort oldSort = toSort(data.getJsonObject("oldSort")); - Att att = toAtt(data.getJsonObject("att")); - return new SortSynonym(newSort, oldSort, att); - } - case KSYNTAXLEXICAL: { - String name = data.getString("name"); - String regex = data.getString("regex"); - Att att = toAtt(data.getJsonObject("att")); - return new SyntaxLexical(name, regex, att); + switch (data.getString("node")) { + case KCONTEXT -> { + K body = toK(data.getJsonObject("body")); + K requires = toK(data.getJsonObject("requires")); + Att att = toAtt(data.getJsonObject("att")); + return new Context(body, requires, att); + } + case KRULE -> { + K body = toK(data.getJsonObject("body")); + K requires = toK(data.getJsonObject("requires")); + K ensures = toK(data.getJsonObject("ensures")); + Att att = toAtt(data.getJsonObject("att")); + return new Rule(body, requires, ensures, att); + } + case KCLAIM -> { + K body = toK(data.getJsonObject("body")); + K requires = toK(data.getJsonObject("requires")); + K ensures = toK(data.getJsonObject("ensures")); + Att att = toAtt(data.getJsonObject("att")); + return new Claim(body, requires, ensures, att); + } + case KSYNTAXPRIORITY -> { + JsonArray priorities = data.getJsonArray("priorities"); + Att att = toAtt(data.getJsonObject("att")); + List> syntaxPriorities = new ArrayList<>(); + priorities.getValuesAs(JsonArray.class).forEach(tags -> syntaxPriorities.add(toTags(tags))); + return new SyntaxPriority(immutable(syntaxPriorities), att); + } + case KSYNTAXASSOCIATIVITY -> { + String assocString = data.getString("assoc"); + Associativity assoc = "Left".equals(assocString) ? Associativity.Left + : "Right".equals(assocString) ? Associativity.Right + : "NonAssoc".equals(assocString) ? Associativity.NonAssoc + : Associativity.Unspecified; + scala.collection.Set tags = toTags(data.getJsonArray("tags")); + Att att = toAtt(data.getJsonObject("att")); + return new SyntaxAssociativity(assoc, tags, att); + } + case KCONFIGURATION -> { + K body = toK(data.getJsonObject("body")); + K ensures = toK(data.getJsonObject("ensures")); + Att att = toAtt(data.getJsonObject("att")); + return new Configuration(body, ensures, att); + } + case KSYNTAXSORT -> { + Sort sort = toSort(data.getJsonObject("sort")); + Att att = toAtt(data.getJsonObject("att")); + List params = new ArrayList<>(); + for (JsonObject s : data.getJsonArray("params").getValuesAs(JsonObject.class)) { + params.add(toSort(s)); } - case KBUBBLE: { - String sentenceType = data.getString("sentenceType"); - String contents = data.getString("contents"); - Att att = toAtt(data.getJsonObject("att")); - return new Bubble(sentenceType, contents, att); + return new SyntaxSort(immutable(params), sort, att); + } + case KSORTSYNONYM -> { + Sort newSort = toSort(data.getJsonObject("newSort")); + Sort oldSort = toSort(data.getJsonObject("oldSort")); + Att att = toAtt(data.getJsonObject("att")); + return new SortSynonym(newSort, oldSort, att); + } + case KSYNTAXLEXICAL -> { + String name = data.getString("name"); + String regex = data.getString("regex"); + Att att = toAtt(data.getJsonObject("att")); + return new SyntaxLexical(name, regex, att); + } + case KBUBBLE -> { + String sentenceType = data.getString("sentenceType"); + String contents = data.getString("contents"); + Att att = toAtt(data.getJsonObject("att")); + return new Bubble(sentenceType, contents, att); + } + case KPRODUCTION -> { + Option klabel = Option.apply(data.containsKey("klabel") ? toKLabel(data.getJsonObject("klabel")) : null); + Sort sort = toSort(data.getJsonObject("sort")); + Att att = toAtt(data.getJsonObject("att")); + + List pItems = new ArrayList<>(); + for (JsonObject pi : data.getJsonArray("productionItems").getValuesAs(JsonObject.class)) { + pItems.add(toProductionItem(pi)); } - case KPRODUCTION: { - Option klabel = Option.apply(data.containsKey("klabel") ? toKLabel(data.getJsonObject("klabel")) : null); - Sort sort = toSort(data.getJsonObject("sort")); - Att att = toAtt(data.getJsonObject("att")); - - List pItems = new ArrayList<>(); - for (JsonObject pi: data.getJsonArray("productionItems").getValuesAs(JsonObject.class)) { - pItems.add(toProductionItem(pi)); - } - List params = new ArrayList<>(); - for (JsonObject s : data.getJsonArray("params").getValuesAs(JsonObject.class)) { - params.add(toSort(s)); - } - return new Production(klabel, immutable(params), sort, immutable(pItems), att); + List params = new ArrayList<>(); + for (JsonObject s : data.getJsonArray("params").getValuesAs(JsonObject.class)) { + params.add(toSort(s)); } - default: - throw KEMException.criticalError("Unexpected node found in KAST Json term: " + data.getString("node")); + return new Production(klabel, immutable(params), sort, immutable(pItems), att); + } + default -> throw KEMException.criticalError("Unexpected node found in KAST Json term: " + data.getString("node")); } } @@ -272,24 +271,23 @@ private static Sort toSort(JsonObject data) { } private static ProductionItem toProductionItem(JsonObject data) { - switch(data.getString("node")) { - case KNONTERMINAL: { - Sort sort = toSort(data.getJsonObject("sort")); - Option name = Option.apply(data.containsKey("name") ? data.getString("name") : null); - return new NonTerminal(sort, name); - } - case KREGEXTERMINAL: { - String precedeRegex = data.getString("precedeRegex"); - String regex = data.getString("regex"); - String followRegex = data.getString("followRegex"); - return new RegexTerminal(precedeRegex, regex, followRegex); - } - case KTERMINAL: { - String value = data.getString("value"); - return new Terminal(value); - } - default: - throw KEMException.criticalError("Unexpected node found in ProductionItem Json term: " + data.getString("node")); + switch (data.getString("node")) { + case KNONTERMINAL -> { + Sort sort = toSort(data.getJsonObject("sort")); + Option name = Option.apply(data.containsKey("name") ? data.getString("name") : null); + return new NonTerminal(sort, name); + } + case KREGEXTERMINAL -> { + String precedeRegex = data.getString("precedeRegex"); + String regex = data.getString("regex"); + String followRegex = data.getString("followRegex"); + return new RegexTerminal(precedeRegex, regex, followRegex); + } + case KTERMINAL -> { + String value = data.getString("value"); + return new Terminal(value); + } + default -> throw KEMException.criticalError("Unexpected node found in ProductionItem Json term: " + data.getString("node")); } } diff --git a/kernel/src/main/java/org/kframework/unparser/Formatter.java b/kernel/src/main/java/org/kframework/unparser/Formatter.java index e575c7e0054..38a497d2b50 100644 --- a/kernel/src/main/java/org/kframework/unparser/Formatter.java +++ b/kernel/src/main/java/org/kframework/unparser/Formatter.java @@ -46,30 +46,19 @@ public static void format(Term term, Indenter indenter, ColorSetting colorize) { if (c == '%') { char c2 = format.charAt(i + 1); i++; - switch(c2) { - case 'n': - indenter.newline(); - break; - case 'i': + switch (c2) { + case 'n' -> indenter.newline(); + case 'i' -> { indenter.indent(); indent++; - break; - case 'd': + } + case 'd' -> { indenter.dedent(); indent--; - break; - case '0': - case '1': - case '2': - case '3': - case '4': - case '5': - case '6': - case '7': - case '8': - case '9': + } + case '0', '1', '2', '3', '4', '5', '6', '7', '8', '9' -> { StringBuilder sb = new StringBuilder(); - for(; i < format.length() && format.charAt(i) >= '0' && format.charAt(i) <= '9';i++) { + for (; i < format.length() && format.charAt(i) >= '0' && format.charAt(i) <= '9'; i++) { sb.append(format.charAt(i)); } i--; @@ -96,7 +85,7 @@ public static void format(Term term, Indenter indenter, ColorSetting colorize) { Term inner = tc.get(nt); boolean assoc = false; if (inner instanceof TermCons) { - TermCons innerTc = (TermCons)inner; + TermCons innerTc = (TermCons) inner; Production origProd = tc.production().att().getOptional(Att.ORIGINAL_PRD(), Production.class).orElse(tc.production()); Production innerOrigProd = innerTc.production().att().getOptional(Att.ORIGINAL_PRD(), Production.class).orElse(innerTc.production()); if (innerOrigProd.equals(origProd) && origProd.att().contains(Att.ASSOC())) { @@ -117,9 +106,8 @@ public static void format(Term term, Indenter indenter, ColorSetting colorize) { } else { throw KEMException.internalError("Cannot currently format productions with regex terminals which are not tokens.", tc.production()); } - break; - default: - indenter.append(c2); + } + default -> indenter.append(c2); } } else { indenter.append(c); diff --git a/kernel/src/main/java/org/kframework/unparser/KPrint.java b/kernel/src/main/java/org/kframework/unparser/KPrint.java index ee9882e9f76..62303a0daa1 100644 --- a/kernel/src/main/java/org/kframework/unparser/KPrint.java +++ b/kernel/src/main/java/org/kframework/unparser/KPrint.java @@ -165,20 +165,14 @@ public byte[] serialize(K term) { } public static byte[] serialize(K term, OutputModes outputMode) { - switch (outputMode) { - case KAST: - return (ToKast.apply(term) + "\n").getBytes(); - case NONE: - return "".getBytes(); - case BINARY: - return ToBinary.apply(term); - case JSON: - return ToJson.apply(term); - case LATEX: - return ToLatex.apply(term); - default: - throw KEMException.criticalError("Unsupported serialization mode: " + outputMode); - } + return switch (outputMode) { + case KAST -> (ToKast.apply(term) + "\n").getBytes(); + case NONE -> "".getBytes(); + case BINARY -> ToBinary.apply(term); + case JSON -> ToJson.apply(term); + case LATEX -> ToLatex.apply(term); + default -> throw KEMException.criticalError("Unsupported serialization mode: " + outputMode); + }; } public String unparseTerm(K input, Module test) { diff --git a/kernel/src/main/java/org/kframework/utils/ColorUtil.java b/kernel/src/main/java/org/kframework/utils/ColorUtil.java index 1537503cb9a..9aaf2d06123 100644 --- a/kernel/src/main/java/org/kframework/utils/ColorUtil.java +++ b/kernel/src/main/java/org/kframework/utils/ColorUtil.java @@ -370,16 +370,12 @@ private static String getEightBitTerminalCode(int code) { } public synchronized static String RgbToAnsi(String rgb, ColorSetting colorSetting) { - switch(colorSetting) { - case OFF: - return ""; - case ON: - return getClosestTerminalCode(colors.get(rgb), ansiColorsToTerminalCodes); - case EXTENDED: - return getClosestTerminalCode(colors.get(rgb), eightBitColorsToTerminalCodes); - default: - throw new UnsupportedOperationException("colorSettung: " + colorSetting); - } + return switch (colorSetting) { + case OFF -> ""; + case ON -> getClosestTerminalCode(colors.get(rgb), ansiColorsToTerminalCodes); + case EXTENDED -> getClosestTerminalCode(colors.get(rgb), eightBitColorsToTerminalCodes); + default -> throw new UnsupportedOperationException("colorSettung: " + colorSetting); + }; } public static void main(String[] args) { diff --git a/kernel/src/main/java/org/kframework/utils/options/DurationConverter.java b/kernel/src/main/java/org/kframework/utils/options/DurationConverter.java index 353086ed54d..343a224ec16 100644 --- a/kernel/src/main/java/org/kframework/utils/options/DurationConverter.java +++ b/kernel/src/main/java/org/kframework/utils/options/DurationConverter.java @@ -25,20 +25,14 @@ public Duration convert(String value) { } catch (ArrayIndexOutOfBoundsException | NumberFormatException e) { throw durationException(value); } - switch (unit) { - case "ms": - return Duration.ofMillis(num); - case "s": - return Duration.ofSeconds(num); - case "m": - return Duration.ofMinutes(num); - case "h": - return Duration.ofHours(num); - case "d": - return Duration.ofDays(num); - default: - throw durationException(value); - } + return switch (unit) { + case "ms" -> Duration.ofMillis(num); + case "s" -> Duration.ofSeconds(num); + case "m" -> Duration.ofMinutes(num); + case "h" -> Duration.ofHours(num); + case "d" -> Duration.ofDays(num); + default -> throw durationException(value); + }; } private ParameterException durationException(String value) { diff --git a/kernel/src/test/java/org/kframework/unparser/KPrintTest.java b/kernel/src/test/java/org/kframework/unparser/KPrintTest.java index 48f3dc7f012..68111ca261c 100644 --- a/kernel/src/test/java/org/kframework/unparser/KPrintTest.java +++ b/kernel/src/test/java/org/kframework/unparser/KPrintTest.java @@ -40,16 +40,12 @@ private String asKast(K term) { private K unparseThenParse(K origTerm, OutputModes outputMode) { byte[] unparsed = KPrint.serialize(origTerm, outputMode); - switch (outputMode) { - case JSON: - return JsonParser.parse(unparsed); - case BINARY: - return BinaryParser.parse(unparsed); - case KAST: - return KastParser.parse(bytes2String(unparsed), new Source("KPrintTest")); - default: - return KToken("###", Sort("UnsupportedOutputMode")); - } + return switch (outputMode) { + case JSON -> JsonParser.parse(unparsed); + case BINARY -> BinaryParser.parse(unparsed); + case KAST -> KastParser.parse(bytes2String(unparsed), new Source("KPrintTest")); + default -> KToken("###", Sort("UnsupportedOutputMode")); + }; } @Test diff --git a/kore/src/main/java/org/kframework/compile/ConfigurationInfo.java b/kore/src/main/java/org/kframework/compile/ConfigurationInfo.java index 4274f502ddf..f0d7e16df0c 100644 --- a/kore/src/main/java/org/kframework/compile/ConfigurationInfo.java +++ b/kore/src/main/java/org/kframework/compile/ConfigurationInfo.java @@ -105,16 +105,12 @@ enum Multiplicity { STAR; public static Multiplicity of(String multiplicity) { - switch(multiplicity) { - case "1": - return ConfigurationInfo.Multiplicity.ONE; - case "*": - return ConfigurationInfo.Multiplicity.STAR; - case "?": - return ConfigurationInfo.Multiplicity.OPTIONAL; - default: - throw new IllegalArgumentException(multiplicity); - } + return switch (multiplicity) { + case "1" -> Multiplicity.ONE; + case "*" -> Multiplicity.STAR; + case "?" -> Multiplicity.OPTIONAL; + default -> throw new IllegalArgumentException(multiplicity); + }; } } } diff --git a/llvm-backend/src/main/java/org/kframework/backend/llvm/LLVMBackend.java b/llvm-backend/src/main/java/org/kframework/backend/llvm/LLVMBackend.java index 56b22571b40..2e0e4b1c692 100644 --- a/llvm-backend/src/main/java/org/kframework/backend/llvm/LLVMBackend.java +++ b/llvm-backend/src/main/java/org/kframework/backend/llvm/LLVMBackend.java @@ -90,19 +90,10 @@ public void accept(Backend.Holder h) { if (options.llvmKompileType.equals("python") && options.llvmKompileOutput != null) { throw KEMException.criticalError("Can't use --llvm-kompile-output with --llvm-kompile-type python"); } - String llvmType; - switch (options.llvmKompileType) { - case "main": - case "search": - case "static": - case "library": - case "python": - case "c": - llvmType = options.llvmKompileType; - break; - default: - throw KEMException.criticalError("Non-valid argument for --llvm-kompile-type: " + options.llvmKompileType + ". Expected [main|search|library|static|python|c]"); - } + String llvmType = switch (options.llvmKompileType) { + case "main", "search", "static", "library", "python", "c" -> options.llvmKompileType; + default -> throw KEMException.criticalError("Non-valid argument for --llvm-kompile-type: " + options.llvmKompileType + ". Expected [main|search|library|static|python|c]"); + }; String llvmOutput = "interpreter"; if (options.llvmKompileOutput != null) {