Merge remote-tracking branch 'origin/develop'

runtimeverification · Nov 6, 2023 · dcf8603 · dcf8603
2 parents c39415f + 8b6ccbc
commit dcf8603
Show file tree

Hide file tree

Showing 26 changed files with 78 additions and 111 deletions.
diff --git a/kernel/src/main/java/org/kframework/backend/kore/ModuleToKORE.java b/kernel/src/main/java/org/kframework/backend/kore/ModuleToKORE.java
@@ -2034,9 +2034,7 @@ private void convert(
 
     for (Tuple2<Tuple2<Att.Key, String>, ?> attribute :
         // Sort to stabilize error messages
-        stream(att.att())
-            .sorted(Comparator.comparing(Tuple2::toString))
-            .collect(Collectors.toList())) {
+        stream(att.att()).sorted(Comparator.comparing(Tuple2::toString)).toList()) {
       Att.Key key = attribute._1._1;
       String strKey = key.key();
       String clsName = attribute._1._2;
@@ -2095,7 +2093,7 @@ private void convertStringVarList(
                   else
                     throw KEMException.criticalError("No free variable found for " + s, location);
                 })
-            .collect(Collectors.toList());
+            .toList();
     String conn = "";
     for (KVariable var : variables) {
       sb.append(conn);

diff --git a/kernel/src/main/java/org/kframework/compile/AddParentCells.java b/kernel/src/main/java/org/kframework/compile/AddParentCells.java
@@ -60,10 +60,7 @@ protected List<KApply> makeParents(KLabel parent, boolean ellipses, List<K> allC
     List<K> children =
         allChildren.stream().filter(t -> !(t instanceof KRewrite)).collect(Collectors.toList());
     List<KRewrite> rewrites =
-        allChildren.stream()
-            .filter(t -> t instanceof KRewrite)
-            .map(t -> (KRewrite) t)
-            .collect(Collectors.toList());
+        allChildren.stream().filter(t -> t instanceof KRewrite).map(t -> (KRewrite) t).toList();
 
     // see if all children can fit together
     Set<Sort> usedCells = Sets.newHashSet();
@@ -200,10 +197,10 @@ Optional<Integer> getLevel(K k) {
       Optional<Integer> level = Optional.empty();
       for (K item : cells) {
         Optional<Integer> level2 = getLevel(item);
-        if (item instanceof KVariable && !level2.isPresent()) {
+        if (item instanceof KVariable && level2.isEmpty()) {
           continue;
         }
-        if (!level.isPresent()) {
+        if (level.isEmpty()) {
           level = level2;
         } else if (!level.equals(level2)) {
           throw KEMException.criticalError("Can't mix cells at different levels under a rewrite");
@@ -247,10 +244,10 @@ Optional<KLabel> getParent(K k) {
     } else {
       Optional<KLabel> leftParent = getParent(((KRewrite) k).left());
       Optional<KLabel> rightParent = getParent(((KRewrite) k).right());
-      if (!leftParent.isPresent()) {
+      if (leftParent.isEmpty()) {
         return rightParent;
       }
-      if (!rightParent.isPresent()) {
+      if (rightParent.isEmpty()) {
         return leftParent;
       }
       if (leftParent.equals(rightParent)) {

diff --git a/kernel/src/main/java/org/kframework/compile/AddSortInjections.java b/kernel/src/main/java/org/kframework/compile/AddSortInjections.java
@@ -503,9 +503,7 @@ private static Sort lub(
     assert !entries.isEmpty();
     entries = new HashSet<>(entries);
     Collection<Sort> filteredEntries =
-        entries.stream()
-            .filter(s -> s != null && !s.name().equals(SORTPARAM_NAME))
-            .collect(Collectors.toList());
+        entries.stream().filter(s -> s != null && !s.name().equals(SORTPARAM_NAME)).toList();
     if (filteredEntries.isEmpty()) { // if all sorts are parameters, take the first
       return entries.iterator().next();
     }

diff --git a/kernel/src/main/java/org/kframework/compile/ConvertDataStructureToLookup.java b/kernel/src/main/java/org/kframework/compile/ConvertDataStructureToLookup.java
@@ -121,7 +121,6 @@ public static Set<KLabel> filteredMapConstructors(Module m) {
     return stream(m.productions())
         .filter(p -> p.att().contains(Att.ASSOC()) && p.att().contains(Att.FILTER_ELEMENT()))
         .map(p -> p.klabel().get())
-        .distinct()
         .collect(Collectors.toSet());
   }
 
@@ -163,7 +162,7 @@ public void apply(KVariable v) {
    */
   K addSideCondition(K requires) {
     Optional<KApply> sideCondition = getSortedLookups().reduce(BooleanUtils::and);
-    if (!sideCondition.isPresent()) {
+    if (sideCondition.isEmpty()) {
       return requires;
     } else if (requires.equals(BooleanUtils.TRUE) && sideCondition.isPresent()) {
       return sideCondition.get();

diff --git a/kernel/src/main/java/org/kframework/compile/DeconstructIntegerAndFloatLiterals.java b/kernel/src/main/java/org/kframework/compile/DeconstructIntegerAndFloatLiterals.java
@@ -92,7 +92,7 @@ KVariable newDotVariable(Sort sort) {
 
   K addSideCondition(K requires) {
     Optional<KApply> sideCondition = state.stream().reduce(BooleanUtils::and);
-    if (!sideCondition.isPresent()) {
+    if (sideCondition.isEmpty()) {
       return requires;
     } else if (requires.equals(BooleanUtils.TRUE) && sideCondition.isPresent()) {
       return sideCondition.get();

diff --git a/kernel/src/main/java/org/kframework/compile/ExpandMacros.java b/kernel/src/main/java/org/kframework/compile/ExpandMacros.java
@@ -117,7 +117,7 @@ public ExpandMacros(
         stream(mod.rules())
             .filter(r -> isMacro(r.att(), reverse))
             .sorted(Comparator.comparingInt(r -> ModuleToKORE.getPriority(r.att())))
-            .collect(Collectors.toList());
+            .toList();
     macros =
         allMacros.stream()
             .filter(r -> getLeft(r, reverse) instanceof KApply)

diff --git a/kernel/src/main/java/org/kframework/compile/ResolveFreshConstants.java b/kernel/src/main/java/org/kframework/compile/ResolveFreshConstants.java
@@ -130,7 +130,7 @@ private K transform(K term) {
       public K apply(KVariable k) {
         if (freshVars.contains(k)) {
           Optional<Sort> s = k.att().getOptional(Sort.class);
-          if (!s.isPresent()) {
+          if (s.isEmpty()) {
             throw KEMException.compilerError("Fresh constant used without a declared sort.", k);
           }
           Option<KLabel> lbl = m.freshFunctionFor().get(s.get());

diff --git a/kernel/src/main/java/org/kframework/compile/ResolveSemanticCasts.java b/kernel/src/main/java/org/kframework/compile/ResolveSemanticCasts.java
@@ -72,20 +72,19 @@ K addSideCondition(K requires, boolean macro) {
       Optional<KApply> sideCondition =
           casts.stream()
               .map(
-                  k -> {
-                    return new TransformK() {
-                      @Override
-                      public K apply(KVariable k) {
-                        if (varToTypedVar.containsKey(k)) {
-                          return varToTypedVar.get(k);
+                  k ->
+                      new TransformK() {
+                        @Override
+                        public K apply(KVariable k) {
+                          if (varToTypedVar.containsKey(k)) {
+                            return varToTypedVar.get(k);
+                          }
+                          return k;
                         }
-                        return k;
-                      }
-                    }.apply(k);
-                  })
+                      }.apply(k))
               .map(k -> KApply(KLabel("is" + getSortNameOfCast((KApply) k)), transform(k)))
               .reduce(BooleanUtils::and);
-      if (!sideCondition.isPresent()) {
+      if (sideCondition.isEmpty()) {
         return requires;
       } else if (requires.equals(BooleanUtils.TRUE) && sideCondition.isPresent()) {
         return sideCondition.get();

diff --git a/kernel/src/main/java/org/kframework/compile/ResolveStrict.java b/kernel/src/main/java/org/kframework/compile/ResolveStrict.java
@@ -167,7 +167,7 @@ public K apply(KVariable var) {
                 .map(j -> KApply(KLabel("is" + result.toString()), KVariable("K" + (j - 1))))
                 .reduce(BooleanUtils::and);
         K requires;
-        if (!sideCondition.isPresent() || !sequential) {
+        if (sideCondition.isEmpty() || !sequential) {
           requires = BooleanUtils.TRUE;
         } else {
           requires = sideCondition.get();
@@ -261,7 +261,7 @@ public Set<Sentence> resolve(Production production, boolean sequential) {
                 .map(j -> KApply(result, KVariable("K" + (j - 1))))
                 .reduce(BooleanUtils::and);
         K requires;
-        if (!sideCondition.isPresent()) {
+        if (sideCondition.isEmpty()) {
           requires = BooleanUtils.TRUE;
         } else {
           requires = sideCondition.get();

diff --git a/kernel/src/main/java/org/kframework/compile/SortInfo.java b/kernel/src/main/java/org/kframework/compile/SortInfo.java
@@ -57,9 +57,8 @@ public static SortInfo fromModule(Module module) {
     joinOps
         .asMap()
         .forEach(
-            (sort, labels) -> {
-              info.closeOperators.put(sort, Iterators.getNext(labels.iterator(), null));
-            });
+            (sort, labels) ->
+                info.closeOperators.put(sort, Iterators.getNext(labels.iterator(), null)));
     return info;
   }
 }
diff --git a/kernel/src/main/java/org/kframework/compile/checks/CheckAtt.java b/kernel/src/main/java/org/kframework/compile/checks/CheckAtt.java
@@ -46,10 +46,7 @@ public void checkUnrecognizedModuleAtts() {
               "Unrecognized attributes on module "
                   + m.name()
                   + ": "
-                  + stream(m.att().unrecognizedKeys())
-                      .map(Key::toString)
-                      .sorted()
-                      .collect(Collectors.toList())
+                  + stream(m.att().unrecognizedKeys()).map(Key::toString).sorted().toList()
                   + "\nHint: User-defined groups can be added with the group(_) attribute."));
     }
   }
@@ -84,10 +81,7 @@ private void checkUnrecognizedAtts(Sentence sentence) {
       errors.add(
           KEMException.compilerError(
               "Unrecognized attributes: "
-                  + stream(sentence.att().unrecognizedKeys())
-                      .map(Key::toString)
-                      .sorted()
-                      .collect(Collectors.toList())
+                  + stream(sentence.att().unrecognizedKeys()).map(Key::toString).sorted().toList()
                   + "\nHint: User-defined groups can be added with the group(_) attribute.",
               sentence));
     }
@@ -99,8 +93,7 @@ private void checkRestrictedAtts(Sentence sentence) {
     Set<Key> keys = stream(att.att().keySet()).map(k -> k._1()).collect(Collectors.toSet());
     keys.removeIf(k -> k.allowedSentences().exists(c -> c.isAssignableFrom(cls)));
     if (!keys.isEmpty()) {
-      List<String> sortedKeys =
-          keys.stream().map(k -> k.toString()).sorted().collect(Collectors.toList());
+      List<String> sortedKeys = keys.stream().map(k -> k.toString()).sorted().toList();
       errors.add(
           KEMException.compilerError(
               cls.getSimpleName()

diff --git a/kernel/src/main/java/org/kframework/compile/checks/CheckBracket.java b/kernel/src/main/java/org/kframework/compile/checks/CheckBracket.java
@@ -2,7 +2,6 @@
 package org.kframework.compile.checks;
 
 import java.util.List;
-import java.util.stream.Collectors;
 import org.kframework.attributes.Att;
 import org.kframework.kil.Module;
 import org.kframework.kil.ModuleItem;
@@ -25,14 +24,12 @@ private static void check(ModuleItem i) {
         for (Production p : b.getProductions()) {
           if (p.containsAttribute(Att.BRACKET())) {
             List<ProductionItem> nts =
-                p.getItems().stream()
-                    .filter(x -> x instanceof NonTerminal)
-                    .collect(Collectors.toList());
+                p.getItems().stream().filter(x -> x instanceof NonTerminal).toList();
             if (nts.size() != 1
                 || !((NonTerminal) nts.get(0)).getSort().equals(s.getDeclaredSort().getSort()))
               throw KEMException.outerParserError(
-                  "bracket productions should have exactly one non-terminal of the same sort as the"
-                      + " production.",
+                  "bracket productions should have exactly one non-terminal "
+                      + "of the same sort as the production.",
                   p.getSource(),
                   p.getLocation());
           }

diff --git a/kernel/src/main/java/org/kframework/compile/checks/CheckKLabels.java b/kernel/src/main/java/org/kframework/compile/checks/CheckKLabels.java
@@ -164,19 +164,17 @@ public void check(Module mainMod) {
       if (prod.att().contains(Att.MAINCELL())
           || prod.att().contains(Att.UNUSED())
           || symbol.equals("<generatedTop>")
-          || !s.isPresent()
+          || s.isEmpty()
           || (prod.att().contains(Att.CELL())
               && stream(prod.nonterminals())
-                  .filter(
+                  .anyMatch(
                       nt ->
                           klabels
                               .get(symbol)
                               .sortAttributesFor()
                               .get(nt.sort().head())
                               .getOrElse(() -> Att.empty())
-                              .contains(Att.CELL_COLLECTION()))
-                  .findAny()
-                  .isPresent())) {
+                              .contains(Att.CELL_COLLECTION())))) {
         continue;
       }
       if (canonicalPath == null || !s.get().source().contains(canonicalPath)) {

diff --git a/kernel/src/main/java/org/kframework/compile/checks/CheckListDecl.java b/kernel/src/main/java/org/kframework/compile/checks/CheckListDecl.java
@@ -21,7 +21,7 @@
 public class CheckListDecl {
 
   public static void check(Module m) {
-    m.getItems().stream().forEach(CheckListDecl::check); // i -> check(i)
+    m.getItems().forEach(CheckListDecl::check); // i -> check(i)
   }
 
   private static final Set<Sort> BASE_SORTS =

diff --git a/kernel/src/main/java/org/kframework/kdep/KDepFrontEnd.java b/kernel/src/main/java/org/kframework/kdep/KDepFrontEnd.java
@@ -126,10 +126,7 @@ protected int run() {
 
     List<File> sortedFiles = new ArrayList<File>(allFiles);
     Collections.sort(
-        sortedFiles,
-        (File a, File b) -> {
-          return a.getAbsolutePath().compareTo(b.getAbsolutePath());
-        });
+        sortedFiles, (File a, File b) -> a.getAbsolutePath().compareTo(b.getAbsolutePath()));
 
     for (File file : sortedFiles) {
       System.out.println("    " + file.getAbsolutePath() + " \\");

diff --git a/kernel/src/main/java/org/kframework/kompile/CompiledDefinition.java b/kernel/src/main/java/org/kframework/kompile/CompiledDefinition.java
@@ -116,39 +116,38 @@ private void initializeConfigurationVariableDefaultSorts(FileUtil files) {
     // searching for #SemanticCastTo<Sort>(Map:lookup(_, #token(<VarName>, KConfigVar)))
     Collections.stream(kompiledDefinition.mainModule().rules())
         .forEach(
-            r -> {
-              new VisitK() {
-                @Override
-                public void apply(KApply k) {
-                  if (k.klabel().name().startsWith("project:")
-                      && k.items().size() == 1
-                      && k.items().get(0) instanceof KApply theMapLookup) {
-                    if (KLabels.MAP_LOOKUP.equals(theMapLookup.klabel())
-                        && theMapLookup.size() == 2
-                        && theMapLookup.items().get(1) instanceof KToken t) {
-                      if (t.sort().equals(Sorts.KConfigVar())) {
-                        Sort sort =
-                            Outer.parseSort(k.klabel().name().substring("project:".length()));
-                        configurationVariableDefaultSorts.put(t.s(), sort);
-                        if (sort.equals(Sorts.K())) {
-                          sort = Sorts.KItem();
+            r ->
+                new VisitK() {
+                  @Override
+                  public void apply(KApply k) {
+                    if (k.klabel().name().startsWith("project:")
+                        && k.items().size() == 1
+                        && k.items().get(0) instanceof KApply theMapLookup) {
+                      if (KLabels.MAP_LOOKUP.equals(theMapLookup.klabel())
+                          && theMapLookup.size() == 2
+                          && theMapLookup.items().get(1) instanceof KToken t) {
+                        if (t.sort().equals(Sorts.KConfigVar())) {
+                          Sort sort =
+                              Outer.parseSort(k.klabel().name().substring("project:".length()));
+                          configurationVariableDefaultSorts.put(t.s(), sort);
+                          if (sort.equals(Sorts.K())) {
+                            sort = Sorts.KItem();
+                          }
+                          String str =
+                              "declaredConfigVar_"
+                                  + t.s().substring(1)
+                                  + "='"
+                                  + sort.toString()
+                                  + "'\n";
+                          sb.append(str);
+                          String astr = "    '" + t.s().substring(1) + "'\n";
+                          arr.append(astr);
                         }
-                        String str =
-                            "declaredConfigVar_"
-                                + t.s().substring(1)
-                                + "='"
-                                + sort.toString()
-                                + "'\n";
-                        sb.append(str);
-                        String astr = "    '" + t.s().substring(1) + "'\n";
-                        arr.append(astr);
                       }
                     }
+                    super.apply(k);
                   }
-                  super.apply(k);
-                }
-              }.apply(r.body());
-            });
+                }.apply(r.body()));
     sb.append(arr);
     sb.append(")\n");
 

diff --git a/kernel/src/main/java/org/kframework/kompile/Kompile.java b/kernel/src/main/java/org/kframework/kompile/Kompile.java
@@ -736,7 +736,6 @@ private void checkIsSortPredicates(scala.collection.Set<Module> modules) {
                     m.productionsForSort()
                         .getOrElse(Sorts.Bool().head(), Set$.MODULE$::<Production>empty)))
         .collect(Collectors.toSet())
-        .stream()
         .forEach(
             prod -> {
               Seq<ProductionItem> items = prod.items();

diff --git a/kernel/src/main/java/org/kframework/lsp/TextDocumentSyncHandler.java b/kernel/src/main/java/org/kframework/lsp/TextDocumentSyncHandler.java
@@ -523,9 +523,7 @@ public CompletableFuture<List<? extends Location>> references(ReferenceParams pa
 
               if (isPositionOverLocation(pos, nameLoc)) {
                 List<DefinitionItem> allDi =
-                    files.values().stream()
-                        .flatMap(doc -> doc.dis.stream())
-                        .collect(Collectors.toList());
+                    files.values().stream().flatMap(doc -> doc.dis.stream()).toList();
                 allDi.stream()
                     .filter(ddi -> ddi instanceof Module)
                     .map(ddi -> ((Module) ddi))
@@ -787,9 +785,7 @@ public CompletableFuture<List<SelectionRange>> selectionRange(SelectionRangePara
                   + " #poss: "
                   + poss
                   + " rezDepth: "
-                  + lloc.stream()
-                      .map(TextDocumentSyncHandler::getSelectionRangeDepth)
-                      .collect(Collectors.toList()));
+                  + lloc.stream().map(TextDocumentSyncHandler::getSelectionRangeDepth).toList());
 
           return lloc;
         });

diff --git a/kernel/src/main/java/org/kframework/parser/KRead.java b/kernel/src/main/java/org/kframework/parser/KRead.java
@@ -66,7 +66,6 @@ public K prettyRead(
           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);
     };
   }