Skip to content

Commit b5c5b7f

Browse files
BaltoliScott-Guestrv-jenkins
authored
Reapply "Miscellaneous Scala clean up" (#4078) (#4108)
This reverts commit ec70555, which was itself a revert of #4055 because of breakages in our Nix builds because of issues around the `scala-kore` dependency. This PR reinstates the original change now that `scala-kore` has been properly released and versioned, and also makes a fix (see comment below) for an issue with Nix / Maven integration that was producing spurious hash invalidations. --------- Co-authored-by: Scott Guest <[email protected]> Co-authored-by: rv-jenkins <[email protected]>
1 parent d144303 commit b5c5b7f

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

41 files changed

+238
-189
lines changed

‎flake.nix

Lines changed: 4 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -61,13 +61,16 @@
6161

6262
k-framework = { haskell-backend-bins, llvm-kompile-libs }:
6363
prev.callPackage ./nix/k.nix {
64-
mvnHash = "sha256-ZbASgB39pSRXxqMuUp9aRxkt0wKhgXV1e1YAQh+ZEIs=";
64+
mvnHash = "sha256-PT4IjnWxNRUeE9I1HHvwK9B3+7hM22kfPXgxOXxY9B4=";
6565
manualMvnArtifacts = [
6666
"org.scala-lang:scala-compiler:2.12.18"
6767
"ant-contrib:ant-contrib:1.0b3"
6868
"org.apache.ant:ant-nodeps:1.8.1"
6969
"org.apache.maven.wagon:wagon-provider-api:1.0-alpha-6"
7070
];
71+
manualMvnSourceArtifacts = [
72+
"org.scala-sbt:compiler-bridge_2.12:1.8.0"
73+
];
7174
inherit (final) maven;
7275
inherit (prev) llvm-backend;
7376
clang = prev."clang_${toString final.llvm-version}";

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

Lines changed: 4 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -52,7 +52,6 @@
5252
import org.kframework.kore.KAs;
5353
import org.kframework.kore.KLabel;
5454
import org.kframework.kore.KList;
55-
import org.kframework.kore.KORE;
5655
import org.kframework.kore.KRewrite;
5756
import org.kframework.kore.KSequence;
5857
import org.kframework.kore.KToken;
@@ -369,7 +368,7 @@ private void collectTokenSortsAndAttributes(
369368
boolean heatCoolEq,
370369
String topCellSortStr) {
371370
for (SortHead sort : iterable(module.sortedDefinedSorts())) {
372-
Att att = module.sortAttributesFor().get(sort).getOrElse(() -> KORE.Att());
371+
Att att = module.sortAttributesFor().get(sort).getOrElse(() -> Att.empty());
373372
if (att.contains(Att.TOKEN())) {
374373
tokenSorts.add(sort);
375374
}
@@ -403,7 +402,7 @@ private void translateSorts(
403402
continue;
404403
}
405404
sb.append(" ");
406-
Att att = module.sortAttributesFor().get(sort).getOrElse(() -> KORE.Att());
405+
Att att = module.sortAttributesFor().get(sort).getOrElse(() -> Att.empty());
407406
if (att.contains(Att.HOOK())) {
408407
if (collectionSorts.contains(att.get(Att.HOOK()))) {
409408
Production concatProd =
@@ -854,7 +853,7 @@ private void genNoJunkAxiom(Sort sort, StringBuilder sb) {
854853
sbTemp.append(", ");
855854
}
856855
}
857-
Att sortAtt = module.sortAttributesFor().get(sort.head()).getOrElse(() -> KORE.Att());
856+
Att sortAtt = module.sortAttributesFor().get(sort.head()).getOrElse(() -> Att.empty());
858857
if (!hasToken && sortAtt.contains(Att.TOKEN())) {
859858
numTerms++;
860859
convertTokenProd(sort, sbTemp);
@@ -1835,7 +1834,7 @@ private void collectAttributes(Map<Att.Key, Boolean> attributes, Att att) {
18351834
KLabel(KLabels.INJ, Sort("S1"), Sort("S2")),
18361835
Sort("S2"),
18371836
Seq(NonTerminal(Sort("S1"))),
1838-
Att());
1837+
Att.empty());
18391838

18401839
private Production production(KApply term) {
18411840
return production(term, false);

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -141,7 +141,7 @@ private K internalAddSortInjections(K term, Sort expectedSort) {
141141
String hookAtt =
142142
mod.sortAttributesFor()
143143
.get(expectedSort.head())
144-
.getOrElse(() -> Att())
144+
.getOrElse(() -> Att.empty())
145145
.getOptional(Att.HOOK())
146146
.orElse("");
147147
if ((hookAtt.equals("MAP.Map") || hookAtt.equals("SET.Set") || hookAtt.equals("LIST.List"))

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

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -83,11 +83,12 @@ KVariable newDotVariable(Sort s) {
8383
KVariable newLabel;
8484
do {
8585
if (s == null) {
86-
newLabel = KVariable("_DotVar" + (counter++), Att().add(Att.ANONYMOUS()));
86+
newLabel = KVariable("_DotVar" + (counter++), Att.empty().add(Att.ANONYMOUS()));
8787
} else {
8888
newLabel =
8989
KVariable(
90-
"_DotVar" + (counter++), Att().add(Att.ANONYMOUS()).add(Att.SORT(), Sort.class, s));
90+
"_DotVar" + (counter++),
91+
Att.empty().add(Att.ANONYMOUS()).add(Att.SORT(), Sort.class, s));
9192
}
9293
} while (vars.contains(newLabel));
9394
vars.add(newLabel);

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -56,7 +56,7 @@ public K apply(KApply k) {
5656
if (isLHS() || !isRHS()) {
5757
return super.apply(k);
5858
}
59-
Att att = module.attributesFor().get(k.klabel()).getOrElse(() -> Att());
59+
Att att = module.attributesFor().get(k.klabel()).getOrElse(() -> Att.empty());
6060
if (att.contains(Att.HOOK()) && !att.contains(Att.IMPURE())) {
6161
String hook = att.get(Att.HOOK());
6262
if (hookNamespaces.stream().anyMatch(ns -> hook.startsWith(ns + "."))) {

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

Lines changed: 24 additions & 16 deletions
Original file line numberDiff line numberDiff line change
@@ -442,7 +442,7 @@ private static Tuple4<Set<Sentence>, Sort, K, Boolean> computeSentencesOfWellFor
442442
KLabel(initLabel),
443443
initSort,
444444
Seq(Terminal(initLabel), Terminal("("), NonTerminal(Sorts.Map()), Terminal(")")),
445-
Att().add(Att.INITIALIZER()).add(Att.FUNCTION()));
445+
Att.empty().add(Att.INITIALIZER()).add(Att.FUNCTION()));
446446
initializerRule =
447447
Rule(
448448
KRewrite(
@@ -451,14 +451,14 @@ private static Tuple4<Set<Sentence>, Sort, K, Boolean> computeSentencesOfWellFor
451451
KLabel("<" + cellName + ">"), false, childInitializer, false)),
452452
BooleanUtils.TRUE,
453453
ensures == null ? BooleanUtils.TRUE : ensures,
454-
Att().add(Att.INITIALIZER()));
454+
Att.empty().add(Att.INITIALIZER()));
455455
} else {
456456
initializer =
457457
Production(
458458
KLabel(initLabel),
459459
initSort,
460460
Seq(Terminal(initLabel)),
461-
Att().add(Att.INITIALIZER()).add(Att.FUNCTION()));
461+
Att.empty().add(Att.INITIALIZER()).add(Att.FUNCTION()));
462462
initializerRule =
463463
Rule(
464464
KRewrite(
@@ -467,7 +467,7 @@ private static Tuple4<Set<Sentence>, Sort, K, Boolean> computeSentencesOfWellFor
467467
KLabel("<" + cellName + ">"), false, childInitializer, false)),
468468
BooleanUtils.TRUE,
469469
ensures == null ? BooleanUtils.TRUE : ensures,
470-
Att().add(Att.INITIALIZER()));
470+
Att.empty().add(Att.INITIALIZER()));
471471
}
472472
if (!m.definedKLabels().contains(KLabel(initLabel))) {
473473
sentences.add(initializer);
@@ -509,7 +509,7 @@ private static Tuple4<Set<Sentence>, Sort, K, Boolean> computeSentencesOfWellFor
509509
KLabel("no" + childSort),
510510
childOptSort,
511511
List(Terminal("no" + childSort)),
512-
Att().add(Att.CELL_OPT_ABSENT(), Sort.class, childSort)));
512+
Att.empty().add(Att.CELL_OPT_ABSENT(), Sort.class, childSort)));
513513
}
514514
}
515515
}
@@ -520,7 +520,7 @@ private static Tuple4<Set<Sentence>, Sort, K, Boolean> computeSentencesOfWellFor
520520
KLabel("<" + cellName + ">-fragment"),
521521
fragmentSort,
522522
immutable(fragmentItems),
523-
Att().add(Att.CELL_FRAGMENT(), Sort.class, Sort(sortName))));
523+
Att.empty().add(Att.CELL_FRAGMENT(), Sort.class, Sort(sortName))));
524524
}
525525
}
526526

@@ -557,7 +557,7 @@ private static Tuple4<Set<Sentence>, Sort, K, Boolean> computeSentencesOfWellFor
557557
String type = cellProperties.getOptional(Att.TYPE()).orElse("Bag");
558558
Sort bagSort = Sort(sortName + type);
559559
Att bagAtt =
560-
Att()
560+
Att.empty()
561561
.add(Att.ASSOC(), "")
562562
.add(Att.CELL_COLLECTION())
563563
.add(Att.ELEMENT(), bagSort.name() + "Item")
@@ -591,7 +591,9 @@ private static Tuple4<Set<Sentence>, Sort, K, Boolean> computeSentencesOfWellFor
591591
SyntaxSort(
592592
Seq(),
593593
bagSort,
594-
Att().add(Att.HOOK(), type.toUpperCase() + '.' + type).add(Att.CELL_COLLECTION()));
594+
Att.empty()
595+
.add(Att.HOOK(), type.toUpperCase() + '.' + type)
596+
.add(Att.CELL_COLLECTION()));
595597
Sentence bagSubsort = Production(Seq(), bagSort, Seq(NonTerminal(sort)));
596598
Sentence bagElement;
597599
if (type.equals("Map")) {
@@ -611,7 +613,10 @@ private static Tuple4<Set<Sentence>, Sort, K, Boolean> computeSentencesOfWellFor
611613
Terminal(","),
612614
NonTerminal(sort),
613615
Terminal(")")),
614-
Att().add(Att.HOOK(), elementHook).add(Att.FUNCTION()).add(Att.FORMAT(), "%5"));
616+
Att.empty()
617+
.add(Att.HOOK(), elementHook)
618+
.add(Att.FUNCTION())
619+
.add(Att.FORMAT(), "%5"));
615620
} else {
616621
bagElement =
617622
Production(
@@ -622,14 +627,17 @@ private static Tuple4<Set<Sentence>, Sort, K, Boolean> computeSentencesOfWellFor
622627
Terminal("("),
623628
NonTerminal(sort),
624629
Terminal(")")),
625-
Att().add(Att.HOOK(), elementHook).add(Att.FUNCTION()).add(Att.FORMAT(), "%3"));
630+
Att.empty()
631+
.add(Att.HOOK(), elementHook)
632+
.add(Att.FUNCTION())
633+
.add(Att.FORMAT(), "%3"));
626634
}
627635
Sentence bagUnit =
628636
Production(
629637
KLabel("." + bagSort.name()),
630638
bagSort,
631639
Seq(Terminal("." + bagSort.name())),
632-
Att().add(Att.HOOK(), unitHook).add(Att.FUNCTION()));
640+
Att.empty().add(Att.HOOK(), unitHook).add(Att.FUNCTION()));
633641
Sentence bag =
634642
Production(
635643
KLabel("_" + bagSort + "_"),
@@ -653,7 +661,7 @@ private static Tuple4<Set<Sentence>, Sort, K, Boolean> computeSentencesOfWellFor
653661
Terminal("("),
654662
NonTerminal(bagSort),
655663
Terminal(")")),
656-
Att().add(Att.HOOK(), "MAP.in_keys").add(Att.FUNCTION()).add(Att.TOTAL())));
664+
Att.empty().add(Att.HOOK(), "MAP.in_keys").add(Att.FUNCTION()).add(Att.TOTAL())));
657665

658666
// syntax KeyCell ::= CellMapKey(Cell) [function, total]
659667
// rule CellMapKey(<cell> K ...<\cell>) => K
@@ -667,7 +675,7 @@ private static Tuple4<Set<Sentence>, Sort, K, Boolean> computeSentencesOfWellFor
667675
Terminal("("),
668676
NonTerminal(sort),
669677
Terminal(")")),
670-
Att().add(Att.FUNCTION()).add(Att.TOTAL()));
678+
Att.empty().add(Att.FUNCTION()).add(Att.TOTAL()));
671679
KVariable key =
672680
KVariable("Key", Att.empty().add(Att.SORT(), Sort.class, childSorts.get(0)));
673681
Rule cellMapKeyRule =
@@ -785,7 +793,7 @@ private static KApply optionalCellInitializer(
785793
}
786794

787795
private static Att getCellPropertiesAsAtt(K k, String cellName) {
788-
Att att = Att();
796+
Att att = Att.empty();
789797
if (cellName.equals("k")) {
790798
att = att.add(Att.MAINCELL());
791799
}
@@ -796,11 +804,11 @@ private static Att getCellPropertiesAsAtt(K k, String cellName) {
796804
private static Att getCellPropertiesAsAtt(K k) {
797805
if (k instanceof KApply kapp) {
798806
if (kapp.klabel().name().equals("#cellPropertyListTerminator")) {
799-
return Att();
807+
return Att.empty();
800808
} else if (kapp.klabel().name().equals("#cellPropertyList")) {
801809
if (kapp.klist().size() == 2) {
802810
Tuple2<Att.Key, String> attribute = getCellProperty(kapp.klist().items().get(0));
803-
return Att()
811+
return Att.empty()
804812
.add(attribute._1(), attribute._2())
805813
.addAll(getCellPropertiesAsAtt(kapp.klist().items().get(1)));
806814
}

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

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -61,7 +61,7 @@ private Stream<? extends Sentence> gen(Sort sort) {
6161
KRewrite(
6262
KApply(
6363
KLabel("is" + sort),
64-
KVariable(sort.name(), Att().add(Att.SORT(), Sort.class, sort))),
64+
KVariable(sort.name(), Att.empty().add(Att.SORT(), Sort.class, sort))),
6565
BooleanUtils.TRUE),
6666
BooleanUtils.TRUE,
6767
BooleanUtils.TRUE));
@@ -70,7 +70,7 @@ private Stream<? extends Sentence> gen(Sort sort) {
7070
KRewrite(KApply(KLabel("is" + sort), KVariable("K")), BooleanUtils.FALSE),
7171
BooleanUtils.TRUE,
7272
BooleanUtils.TRUE,
73-
Att().add(Att.OWISE())));
73+
Att.empty().add(Att.OWISE())));
7474
return res.stream();
7575
}
7676
}

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

Lines changed: 4 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -39,7 +39,10 @@ public Set<Sentence> gen(Module mod, Sort sort) {
3939
KLabel("is" + sort.toString()),
4040
Sorts.Bool(),
4141
Seq(Terminal("is" + sort), Terminal("("), NonTerminal(Sorts.K()), Terminal(")")),
42-
Att().add(Att.FUNCTION()).add(Att.TOTAL()).add(Att.PREDICATE(), Sort.class, sort));
42+
Att.empty()
43+
.add(Att.FUNCTION())
44+
.add(Att.TOTAL())
45+
.add(Att.PREDICATE(), Sort.class, sort));
4346
if (!mod.productions().contains(prod)) return Collections.singleton(prod);
4447
return Collections.emptySet();
4548
}

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

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -77,7 +77,7 @@ public Stream<? extends Sentence> gen(Sort sort) {
7777
KRewrite(KApply(lbl, var), var),
7878
BooleanUtils.TRUE,
7979
BooleanUtils.TRUE,
80-
Att().add(Att.PROJECTION()));
80+
Att.empty().add(Att.PROJECTION()));
8181
if (mod.definedKLabels().contains(lbl)) {
8282
return Stream.empty();
8383
}
@@ -86,7 +86,7 @@ public Stream<? extends Sentence> gen(Sort sort) {
8686
lbl,
8787
sort,
8888
Seq(Terminal(lbl.name()), Terminal("("), NonTerminal(Sorts.K()), Terminal(")")),
89-
Att().add(Att.FUNCTION()).add(Att.PROJECTION()));
89+
Att.empty().add(Att.FUNCTION()).add(Att.PROJECTION()));
9090
if (cover) {
9191
KLabel sideEffectLbl = KLabel("sideEffect:" + sort);
9292
Production sideEffect =
@@ -100,7 +100,7 @@ public Stream<? extends Sentence> gen(Sort sort) {
100100
Terminal(","),
101101
NonTerminal(sort),
102102
Terminal(")")),
103-
Att().add(Att.FUNCTION()));
103+
Att.empty().add(Att.FUNCTION()));
104104
Rule sideEffectR =
105105
Rule(
106106
KRewrite(
@@ -149,7 +149,7 @@ public Stream<? extends Sentence> gen(Production prod) {
149149
Terminal("("),
150150
NonTerminal(prod.sort()),
151151
Terminal(")")),
152-
Att().add(Att.FUNCTION())));
152+
Att.empty().add(Att.FUNCTION())));
153153
sentences.add(
154154
Rule(
155155
KRewrite(KApply(lbl, KApply(prod.klabel().get(), KList(vars))), vars.get(i)),

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

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -95,7 +95,8 @@ KVariable newDotVariable(Sort s) {
9595
do {
9696
newLabel =
9797
KVariable(
98-
"_Gen" + (counter++), Att().add(Att.ANONYMOUS()).add(Att.SORT(), Sort.class, s));
98+
"_Gen" + (counter++),
99+
Att.empty().add(Att.ANONYMOUS()).add(Att.SORT(), Sort.class, s));
99100
} while (vars.contains(newLabel));
100101
vars.add(newLabel);
101102
return newLabel;

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -219,7 +219,7 @@ public K apply(KApply k) {
219219
KVariable newDotVariable(Sort sort) {
220220
KVariable newLabel;
221221
do {
222-
newLabel = KVariable("_Gen" + (counter++), Att().add(Att.SORT(), Sort.class, sort));
222+
newLabel = KVariable("_Gen" + (counter++), Att.empty().add(Att.SORT(), Sort.class, sort));
223223
} while (vars.contains(newLabel));
224224
vars.add(newLabel);
225225
return newLabel;

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

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -121,7 +121,7 @@ public K apply(KVariable k) {
121121
KVariable newDotVariable(String prefix, K k) {
122122
KVariable newLabel;
123123
Att locInfo =
124-
Optional.of(Att())
124+
Optional.of(Att.empty())
125125
.flatMap(
126126
att ->
127127
k.att()
@@ -132,8 +132,8 @@ KVariable newDotVariable(String prefix, K k) {
132132
k.att()
133133
.getOptional(Att.LOCATION(), Location.class)
134134
.map(l -> att.add(Att.LOCATION(), Location.class, l)))
135-
.orElse(Att());
136-
Att att = Att().add(Att.ANONYMOUS()).addAll(locInfo);
135+
.orElse(Att.empty());
136+
Att att = Att.empty().add(Att.ANONYMOUS()).addAll(locInfo);
137137
if (prefix.equals("?")) {
138138
att = att.add(Att.FRESH());
139139
}

0 commit comments

Comments
 (0)