Miscellaneous Scala clean up

flake.nix

@@ -61,13 +61,16 @@
 
             k-framework = { haskell-backend-bins, llvm-kompile-libs }:
               prev.callPackage ./nix/k.nix {
-                mvnHash = "sha256-AMxXqu1bbpnmsmLTizNw1n2llSdvx6AuNZRGUHqPn14=";
+                mvnHash = "sha256-blcFyUg6xzrYZZkoNpmDkD/NMjY+ILfF2h8zIA53G6U=";
                 manualMvnArtifacts = [
                   "org.scala-lang:scala-compiler:2.12.18"
                   "ant-contrib:ant-contrib:1.0b3"
                   "org.apache.ant:ant-nodeps:1.8.1"
                   "org.apache.maven.wagon:wagon-provider-api:1.0-alpha-6"
                 ];
+                manualMvnSourceArtifacts = [
+                  "org.scala-sbt:compiler-bridge_2.12"
+                ];
                 inherit (final) maven;
                 inherit (prev) llvm-backend;
                 clang = prev."clang_${toString final.llvm-version}";

kernel/src/main/java/org/kframework/backend/kore/ModuleToKORE.java

@@ -52,7 +52,6 @@
 import org.kframework.kore.KAs;
 import org.kframework.kore.KLabel;
 import org.kframework.kore.KList;
-import org.kframework.kore.KORE;
 import org.kframework.kore.KRewrite;
 import org.kframework.kore.KSequence;
 import org.kframework.kore.KToken;
@@ -386,7 +385,7 @@ private void collectTokenSortsAndAttributes(
       boolean heatCoolEq,
       String topCellSortStr) {
     for (SortHead sort : iterable(module.sortedDefinedSorts())) {
-      Att att = module.sortAttributesFor().get(sort).getOrElse(() -> KORE.Att());
+      Att att = module.sortAttributesFor().get(sort).getOrElse(() -> Att.empty());
       if (att.contains(Att.TOKEN())) {
         tokenSorts.add(sort);
       }
@@ -420,7 +419,7 @@ private void translateSorts(
         continue;
       }
       sb.append("  ");
-      Att att = module.sortAttributesFor().get(sort).getOrElse(() -> KORE.Att());
+      Att att = module.sortAttributesFor().get(sort).getOrElse(() -> Att.empty());
       if (att.contains(Att.HOOK())) {
         if (collectionSorts.contains(att.get(Att.HOOK()))) {
           Production concatProd =
@@ -871,7 +870,7 @@ private void genNoJunkAxiom(Sort sort, StringBuilder sb) {
         sbTemp.append(", ");
       }
     }
-    Att sortAtt = module.sortAttributesFor().get(sort.head()).getOrElse(() -> KORE.Att());
+    Att sortAtt = module.sortAttributesFor().get(sort.head()).getOrElse(() -> Att.empty());
     if (!hasToken && sortAtt.contains(Att.TOKEN())) {
       numTerms++;
       convertTokenProd(sort, sbTemp);
@@ -1870,7 +1869,7 @@ private void collectAttributes(Map<Att.Key, Boolean> attributes, Att att) {
           KLabel(KLabels.INJ, Sort("S1"), Sort("S2")),
           Sort("S2"),
           Seq(NonTerminal(Sort("S1"))),
-          Att());
+          Att.empty());
 
   private Production production(KApply term) {
     return production(term, false);

kernel/src/main/java/org/kframework/compile/AddSortInjections.java

@@ -141,7 +141,7 @@ private K internalAddSortInjections(K term, Sort expectedSort) {
       String hookAtt =
           mod.sortAttributesFor()
               .get(expectedSort.head())
-              .getOrElse(() -> Att())
+              .getOrElse(() -> Att.empty())
               .getOptional(Att.HOOK())
               .orElse("");
       if ((hookAtt.equals("MAP.Map") || hookAtt.equals("SET.Set") || hookAtt.equals("LIST.List"))

kernel/src/main/java/org/kframework/compile/CloseCells.java

@@ -83,11 +83,12 @@ KVariable newDotVariable(Sort s) {
     KVariable newLabel;
     do {
       if (s == null) {
-        newLabel = KVariable("_DotVar" + (counter++), Att().add(Att.ANONYMOUS()));
+        newLabel = KVariable("_DotVar" + (counter++), Att.empty().add(Att.ANONYMOUS()));
       } else {
         newLabel =
             KVariable(
-                "_DotVar" + (counter++), Att().add(Att.ANONYMOUS()).add(Att.SORT(), Sort.class, s));
+                "_DotVar" + (counter++),
+                Att.empty().add(Att.ANONYMOUS()).add(Att.SORT(), Sort.class, s));
       }
     } while (vars.contains(newLabel));
     vars.add(newLabel);

kernel/src/main/java/org/kframework/compile/ConstantFolding.java

@@ -56,7 +56,7 @@ public K apply(KApply k) {
         if (isLHS() || !isRHS()) {
           return super.apply(k);
         }
-        Att att = module.attributesFor().get(k.klabel()).getOrElse(() -> Att());
+        Att att = module.attributesFor().get(k.klabel()).getOrElse(() -> Att.empty());
         if (att.contains(Att.HOOK()) && !att.contains(Att.IMPURE())) {
           String hook = att.get(Att.HOOK());
           if (hookNamespaces.stream().anyMatch(ns -> hook.startsWith(ns + "."))) {

kernel/src/main/java/org/kframework/compile/GenerateSentencesFromConfigDecl.java

@@ -438,7 +438,7 @@ private static Tuple4<Set<Sentence>, Sort, K, Boolean> computeSentencesOfWellFor
               KLabel(initLabel),
               initSort,
               Seq(Terminal(initLabel), Terminal("("), NonTerminal(Sorts.Map()), Terminal(")")),
-              Att().add(Att.INITIALIZER()).add(Att.FUNCTION()));
+              Att.empty().add(Att.INITIALIZER()).add(Att.FUNCTION()));
       initializerRule =
           Rule(
               KRewrite(
@@ -447,14 +447,14 @@ private static Tuple4<Set<Sentence>, Sort, K, Boolean> computeSentencesOfWellFor
                       KLabel("<" + cellName + ">"), false, childInitializer, false)),
               BooleanUtils.TRUE,
               ensures == null ? BooleanUtils.TRUE : ensures,
-              Att().add(Att.INITIALIZER()));
+              Att.empty().add(Att.INITIALIZER()));
     } else {
       initializer =
           Production(
               KLabel(initLabel),
               initSort,
               Seq(Terminal(initLabel)),
-              Att().add(Att.INITIALIZER()).add(Att.FUNCTION()));
+              Att.empty().add(Att.INITIALIZER()).add(Att.FUNCTION()));
       initializerRule =
           Rule(
               KRewrite(
@@ -463,7 +463,7 @@ private static Tuple4<Set<Sentence>, Sort, K, Boolean> computeSentencesOfWellFor
                       KLabel("<" + cellName + ">"), false, childInitializer, false)),
               BooleanUtils.TRUE,
               ensures == null ? BooleanUtils.TRUE : ensures,
-              Att().add(Att.INITIALIZER()));
+              Att.empty().add(Att.INITIALIZER()));
     }
     if (!m.definedKLabels().contains(KLabel(initLabel))) {
       sentences.add(initializer);
@@ -505,7 +505,7 @@ private static Tuple4<Set<Sentence>, Sort, K, Boolean> computeSentencesOfWellFor
                     KLabel("no" + childSort),
                     childOptSort,
                     List(Terminal("no" + childSort)),
-                    Att().add(Att.CELL_OPT_ABSENT(), Sort.class, childSort)));
+                    Att.empty().add(Att.CELL_OPT_ABSENT(), Sort.class, childSort)));
           }
         }
       }
@@ -516,7 +516,7 @@ private static Tuple4<Set<Sentence>, Sort, K, Boolean> computeSentencesOfWellFor
                 KLabel("<" + cellName + ">-fragment"),
                 fragmentSort,
                 immutable(fragmentItems),
-                Att().add(Att.CELL_FRAGMENT(), Sort.class, Sort(sortName))));
+                Att.empty().add(Att.CELL_FRAGMENT(), Sort.class, Sort(sortName))));
       }
     }
 
@@ -553,7 +553,7 @@ private static Tuple4<Set<Sentence>, Sort, K, Boolean> computeSentencesOfWellFor
       String type = cellProperties.getOptional(Att.TYPE()).orElse("Bag");
       Sort bagSort = Sort(sortName + type);
       Att bagAtt =
-          Att()
+          Att.empty()
               .add(Att.ASSOC(), "")
               .add(Att.CELL_COLLECTION())
               .add(Att.ELEMENT(), bagSort.name() + "Item")
@@ -587,7 +587,9 @@ private static Tuple4<Set<Sentence>, Sort, K, Boolean> computeSentencesOfWellFor
           SyntaxSort(
               Seq(),
               bagSort,
-              Att().add(Att.HOOK(), type.toUpperCase() + '.' + type).add(Att.CELL_COLLECTION()));
+              Att.empty()
+                  .add(Att.HOOK(), type.toUpperCase() + '.' + type)
+                  .add(Att.CELL_COLLECTION()));
       Sentence bagSubsort = Production(Seq(), bagSort, Seq(NonTerminal(sort)));
       Sentence bagElement;
       if (type.equals("Map")) {
@@ -607,7 +609,10 @@ private static Tuple4<Set<Sentence>, Sort, K, Boolean> computeSentencesOfWellFor
                     Terminal(","),
                     NonTerminal(sort),
                     Terminal(")")),
-                Att().add(Att.HOOK(), elementHook).add(Att.FUNCTION()).add(Att.FORMAT(), "%5"));
+                Att.empty()
+                    .add(Att.HOOK(), elementHook)
+                    .add(Att.FUNCTION())
+                    .add(Att.FORMAT(), "%5"));
       } else {
         bagElement =
             Production(
@@ -618,14 +623,17 @@ private static Tuple4<Set<Sentence>, Sort, K, Boolean> computeSentencesOfWellFor
                     Terminal("("),
                     NonTerminal(sort),
                     Terminal(")")),
-                Att().add(Att.HOOK(), elementHook).add(Att.FUNCTION()).add(Att.FORMAT(), "%3"));
+                Att.empty()
+                    .add(Att.HOOK(), elementHook)
+                    .add(Att.FUNCTION())
+                    .add(Att.FORMAT(), "%3"));
       }
       Sentence bagUnit =
           Production(
               KLabel("." + bagSort.name()),
               bagSort,
               Seq(Terminal("." + bagSort.name())),
-              Att().add(Att.HOOK(), unitHook).add(Att.FUNCTION()));
+              Att.empty().add(Att.HOOK(), unitHook).add(Att.FUNCTION()));
       Sentence bag =
           Production(
               KLabel("_" + bagSort + "_"),
@@ -649,7 +657,7 @@ private static Tuple4<Set<Sentence>, Sort, K, Boolean> computeSentencesOfWellFor
                     Terminal("("),
                     NonTerminal(bagSort),
                     Terminal(")")),
-                Att().add(Att.HOOK(), "MAP.in_keys").add(Att.FUNCTION()).add(Att.TOTAL())));
+                Att.empty().add(Att.HOOK(), "MAP.in_keys").add(Att.FUNCTION()).add(Att.TOTAL())));
 
         // syntax KeyCell ::= CellMapKey(Cell) [function, total]
         // rule CellMapKey(<cell> K ...<\cell>) => K
@@ -663,7 +671,7 @@ private static Tuple4<Set<Sentence>, Sort, K, Boolean> computeSentencesOfWellFor
                     Terminal("("),
                     NonTerminal(sort),
                     Terminal(")")),
-                Att().add(Att.FUNCTION()).add(Att.TOTAL()));
+                Att.empty().add(Att.FUNCTION()).add(Att.TOTAL()));
         KVariable key =
             KVariable("Key", Att.empty().add(Att.SORT(), Sort.class, childSorts.get(0)));
         Rule cellMapKeyRule =
@@ -764,7 +772,7 @@ private static KApply optionalCellInitializer(
   }
 
   private static Att getCellPropertiesAsAtt(K k, String cellName) {
-    Att att = Att();
+    Att att = Att.empty();
     if (cellName.equals("k")) {
       att = att.add(Att.MAINCELL());
     }
@@ -775,11 +783,11 @@ private static Att getCellPropertiesAsAtt(K k, String cellName) {
   private static Att getCellPropertiesAsAtt(K k) {
     if (k instanceof KApply kapp) {
       if (kapp.klabel().name().equals("#cellPropertyListTerminator")) {
-        return Att();
+        return Att.empty();
       } else if (kapp.klabel().name().equals("#cellPropertyList")) {
         if (kapp.klist().size() == 2) {
           Tuple2<Att.Key, String> attribute = getCellProperty(kapp.klist().items().get(0));
-          return Att()
+          return Att.empty()
               .add(attribute._1(), attribute._2())
               .addAll(getCellPropertiesAsAtt(kapp.klist().items().get(1)));
         }

kernel/src/main/java/org/kframework/compile/GenerateSortPredicateRules.java

@@ -61,7 +61,7 @@ private Stream<? extends Sentence> gen(Sort sort) {
               KRewrite(
                   KApply(
                       KLabel("is" + sort),
-                      KVariable(sort.name(), Att().add(Att.SORT(), Sort.class, sort))),
+                      KVariable(sort.name(), Att.empty().add(Att.SORT(), Sort.class, sort))),
                   BooleanUtils.TRUE),
               BooleanUtils.TRUE,
               BooleanUtils.TRUE));
@@ -70,7 +70,7 @@ private Stream<? extends Sentence> gen(Sort sort) {
               KRewrite(KApply(KLabel("is" + sort), KVariable("K")), BooleanUtils.FALSE),
               BooleanUtils.TRUE,
               BooleanUtils.TRUE,
-              Att().add(Att.OWISE())));
+              Att.empty().add(Att.OWISE())));
       return res.stream();
     }
   }

kernel/src/main/java/org/kframework/compile/GenerateSortPredicateSyntax.java

@@ -39,7 +39,10 @@ public Set<Sentence> gen(Module mod, Sort sort) {
             KLabel("is" + sort.toString()),
             Sorts.Bool(),
             Seq(Terminal("is" + sort), Terminal("("), NonTerminal(Sorts.K()), Terminal(")")),
-            Att().add(Att.FUNCTION()).add(Att.TOTAL()).add(Att.PREDICATE(), Sort.class, sort));
+            Att.empty()
+                .add(Att.FUNCTION())
+                .add(Att.TOTAL())
+                .add(Att.PREDICATE(), Sort.class, sort));
     if (!mod.productions().contains(prod)) return Collections.singleton(prod);
     return Collections.emptySet();
   }

kernel/src/main/java/org/kframework/compile/GenerateSortProjections.java

@@ -77,7 +77,7 @@ public Stream<? extends Sentence> gen(Sort sort) {
             KRewrite(KApply(lbl, var), var),
             BooleanUtils.TRUE,
             BooleanUtils.TRUE,
-            Att().add(Att.PROJECTION()));
+            Att.empty().add(Att.PROJECTION()));
     if (mod.definedKLabels().contains(lbl)) {
       return Stream.empty();
     }
@@ -86,7 +86,7 @@ public Stream<? extends Sentence> gen(Sort sort) {
             lbl,
             sort,
             Seq(Terminal(lbl.name()), Terminal("("), NonTerminal(Sorts.K()), Terminal(")")),
-            Att().add(Att.FUNCTION()).add(Att.PROJECTION()));
+            Att.empty().add(Att.FUNCTION()).add(Att.PROJECTION()));
     if (cover) {
       KLabel sideEffectLbl = KLabel("sideEffect:" + sort);
       Production sideEffect =
@@ -100,7 +100,7 @@ public Stream<? extends Sentence> gen(Sort sort) {
                   Terminal(","),
                   NonTerminal(sort),
                   Terminal(")")),
-              Att().add(Att.FUNCTION()));
+              Att.empty().add(Att.FUNCTION()));
       Rule sideEffectR =
           Rule(
               KRewrite(
@@ -149,7 +149,7 @@ public Stream<? extends Sentence> gen(Production prod) {
                     Terminal("("),
                     NonTerminal(prod.sort()),
                     Terminal(")")),
-                Att().add(Att.FUNCTION())));
+                Att.empty().add(Att.FUNCTION())));
         sentences.add(
             Rule(
                 KRewrite(KApply(lbl, KApply(prod.klabel().get(), KList(vars))), vars.get(i)),

kernel/src/main/java/org/kframework/compile/GuardOrPatterns.java

@@ -95,7 +95,8 @@ KVariable newDotVariable(Sort s) {
     do {
       newLabel =
           KVariable(
-              "_Gen" + (counter++), Att().add(Att.ANONYMOUS()).add(Att.SORT(), Sort.class, s));
+              "_Gen" + (counter++),
+              Att.empty().add(Att.ANONYMOUS()).add(Att.SORT(), Sort.class, s));
     } while (vars.contains(newLabel));
     vars.add(newLabel);
     return newLabel;

kernel/src/main/java/org/kframework/compile/MinimizeTermConstruction.java

@@ -219,7 +219,7 @@ public K apply(KApply k) {
   KVariable newDotVariable(Sort sort) {
     KVariable newLabel;
     do {
-      newLabel = KVariable("_Gen" + (counter++), Att().add(Att.SORT(), Sort.class, sort));
+      newLabel = KVariable("_Gen" + (counter++), Att.empty().add(Att.SORT(), Sort.class, sort));
     } while (vars.contains(newLabel));
     vars.add(newLabel);
     return newLabel;

kernel/src/main/java/org/kframework/compile/ResolveAnonVar.java

@@ -121,7 +121,7 @@ public K apply(KVariable k) {
   KVariable newDotVariable(String prefix, K k) {
     KVariable newLabel;
     Att locInfo =
-        Optional.of(Att())
+        Optional.of(Att.empty())
             .flatMap(
                 att ->
                     k.att()
@@ -132,8 +132,8 @@ KVariable newDotVariable(String prefix, K k) {
                     k.att()
                         .getOptional(Att.LOCATION(), Location.class)
                         .map(l -> att.add(Att.LOCATION(), Location.class, l)))
-            .orElse(Att());
-    Att att = Att().add(Att.ANONYMOUS()).addAll(locInfo);
+            .orElse(Att.empty());
+    Att att = Att.empty().add(Att.ANONYMOUS()).addAll(locInfo);
     if (prefix.equals("?")) {
       att = att.add(Att.FRESH());
     }