Merge branch 'develop' into java-records

runtimeverification · Oct 24, 2023 · 49d18e3 · 49d18e3
2 parents cac9021 + 0bbfe47
commit 49d18e3
Show file tree

Hide file tree

Showing 20 changed files with 317 additions and 444 deletions.
diff --git a/.github/workflows/release.yml b/.github/workflows/release.yml
@@ -424,8 +424,8 @@ jobs:
       - name: 'Install pandoc/texlive/calibre'
         run: |
           sudo apt update --yes
-          sudo apt install --yes wget texlive-xetex
-          sudo wget -nv -O- https://download.calibre-ebook.com/linux-installer.sh | sh /dev/stdin version=5.44.0
+          sudo apt install --yes wget texlive-xetex libegl1 libopengl0
+          sudo wget -nv -O- https://download.calibre-ebook.com/linux-installer.sh | sh /dev/stdin version=6.29.0
           sudo wget https://github.com/jgm/pandoc/releases/download/2.18/pandoc-2.18-1-amd64.deb -O /tmp/pandoc.deb
           sudo dpkg -i /tmp/pandoc.deb
       - name: 'Checkout code and set up web build'

diff --git a/k-distribution/src/main/scripts/lib/checkJava b/k-distribution/src/main/scripts/lib/checkJava
@@ -1,5 +1,5 @@
 #!/usr/bin/env bash
-MIN_VERSION="8"
+MIN_VERSION="17"
 echoerr() { echo "$@" 1>&2; }
 
 if type -p java >/dev/null; then

diff --git 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<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(")");
@@ -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
@@ -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
@@ -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()) {

diff --git 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
@@ -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) {

diff --git 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<org.kframework.definition.Sentence> 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
@@ -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());