Skip to content

Commit

Permalink
Revert "Miscellaneous Scala clean up" (#4078)
Browse files Browse the repository at this point in the history 
Reverts #4055

We will want to reinstate this PR once the required `scala-kore`
infrastructure is actually ready to use.
  • Loading branch information
@Baltoli
Baltoli authored Mar 5, 2024
1 parent 2070cac commit ec70555
Show file tree
Hide file tree
Showing 42 changed files with 190 additions and 243 deletions.
5 changes: 1 addition & 4 deletions flake.nix
View file
Original file line number Diff line number Diff line change
Expand Up @@ -61,16 +61,13 @@

k-framework = { haskell-backend-bins, llvm-kompile-libs }:
prev.callPackage ./nix/k.nix {
mvnHash = "sha256-e/W0s+3LaKkZSSOiDQdkbkFdAYF5ihaj47hlNce3+Hc=";
mvnHash = "sha256-AMxXqu1bbpnmsmLTizNw1n2llSdvx6AuNZRGUHqPn14=";
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}";
Expand Down
9 changes: 5 additions & 4 deletions kernel/src/main/java/org/kframework/backend/kore/ModuleToKORE.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -52,6 +52,7 @@
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;
Expand Down Expand Up @@ -385,7 +386,7 @@ private void collectTokenSortsAndAttributes(
boolean heatCoolEq,
String topCellSortStr) {
for (SortHead sort : iterable(module.sortedDefinedSorts())) {
Att att = module.sortAttributesFor().get(sort).getOrElse(() -> Att.empty());
Att att = module.sortAttributesFor().get(sort).getOrElse(() -> KORE.Att());
if (att.contains(Att.TOKEN())) {
tokenSorts.add(sort);
}
Expand Down Expand Up @@ -419,7 +420,7 @@ private void translateSorts(
continue;
}
sb.append(" ");
Att att = module.sortAttributesFor().get(sort).getOrElse(() -> Att.empty());
Att att = module.sortAttributesFor().get(sort).getOrElse(() -> KORE.Att());
if (att.contains(Att.HOOK())) {
if (collectionSorts.contains(att.get(Att.HOOK()))) {
Production concatProd =
Expand Down Expand Up @@ -870,7 +871,7 @@ private void genNoJunkAxiom(Sort sort, StringBuilder sb) {
sbTemp.append(", ");
}
}
Att sortAtt = module.sortAttributesFor().get(sort.head()).getOrElse(() -> Att.empty());
Att sortAtt = module.sortAttributesFor().get(sort.head()).getOrElse(() -> KORE.Att());
if (!hasToken && sortAtt.contains(Att.TOKEN())) {
numTerms++;
convertTokenProd(sort, sbTemp);
Expand Down Expand Up @@ -1869,7 +1870,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.empty());
Att());

private Production production(KApply term) {
return production(term, false);
Expand Down
2 changes: 1 addition & 1 deletion kernel/src/main/java/org/kframework/compile/AddSortInjections.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -141,7 +141,7 @@ private K internalAddSortInjections(K term, Sort expectedSort) {
String hookAtt =
mod.sortAttributesFor()
.get(expectedSort.head())
.getOrElse(() -> Att.empty())
.getOrElse(() -> Att())
.getOptional(Att.HOOK())
.orElse("");
if ((hookAtt.equals("MAP.Map") || hookAtt.equals("SET.Set") || hookAtt.equals("LIST.List"))
Expand Down
5 changes: 2 additions & 3 deletions kernel/src/main/java/org/kframework/compile/CloseCells.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -83,12 +83,11 @@ KVariable newDotVariable(Sort s) {
KVariable newLabel;
do {
if (s == null) {
newLabel = KVariable("_DotVar" + (counter++), Att.empty().add(Att.ANONYMOUS()));
newLabel = KVariable("_DotVar" + (counter++), Att().add(Att.ANONYMOUS()));
} else {
newLabel =
KVariable(
"_DotVar" + (counter++),
Att.empty().add(Att.ANONYMOUS()).add(Att.SORT(), Sort.class, s));
"_DotVar" + (counter++), Att().add(Att.ANONYMOUS()).add(Att.SORT(), Sort.class, s));
}
} while (vars.contains(newLabel));
vars.add(newLabel);
Expand Down
2 changes: 1 addition & 1 deletion kernel/src/main/java/org/kframework/compile/ConstantFolding.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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.empty());
Att att = module.attributesFor().get(k.klabel()).getOrElse(() -> Att());
if (att.contains(Att.HOOK()) && !att.contains(Att.IMPURE())) {
String hook = att.get(Att.HOOK());
if (hookNamespaces.stream().anyMatch(ns -> hook.startsWith(ns + "."))) {
Expand Down
40 changes: 16 additions & 24 deletions kernel/src/main/java/org/kframework/compile/GenerateSentencesFromConfigDecl.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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.empty().add(Att.INITIALIZER()).add(Att.FUNCTION()));
Att().add(Att.INITIALIZER()).add(Att.FUNCTION()));
initializerRule =
Rule(
KRewrite(
Expand All @@ -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.empty().add(Att.INITIALIZER()));
Att().add(Att.INITIALIZER()));
} else {
initializer =
Production(
KLabel(initLabel),
initSort,
Seq(Terminal(initLabel)),
Att.empty().add(Att.INITIALIZER()).add(Att.FUNCTION()));
Att().add(Att.INITIALIZER()).add(Att.FUNCTION()));
initializerRule =
Rule(
KRewrite(
Expand All @@ -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.empty().add(Att.INITIALIZER()));
Att().add(Att.INITIALIZER()));
}
if (!m.definedKLabels().contains(KLabel(initLabel))) {
sentences.add(initializer);
Expand Down Expand Up @@ -505,7 +505,7 @@ private static Tuple4<Set<Sentence>, Sort, K, Boolean> computeSentencesOfWellFor
KLabel("no" + childSort),
childOptSort,
List(Terminal("no" + childSort)),
Att.empty().add(Att.CELL_OPT_ABSENT(), Sort.class, childSort)));
Att().add(Att.CELL_OPT_ABSENT(), Sort.class, childSort)));
}
}
}
Expand All @@ -516,7 +516,7 @@ private static Tuple4<Set<Sentence>, Sort, K, Boolean> computeSentencesOfWellFor
KLabel("<" + cellName + ">-fragment"),
fragmentSort,
immutable(fragmentItems),
Att.empty().add(Att.CELL_FRAGMENT(), Sort.class, Sort(sortName))));
Att().add(Att.CELL_FRAGMENT(), Sort.class, Sort(sortName))));
}
}

Expand Down Expand Up @@ -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.empty()
Att()
.add(Att.ASSOC(), "")
.add(Att.CELL_COLLECTION())
.add(Att.ELEMENT(), bagSort.name() + "Item")
Expand Down Expand Up @@ -587,9 +587,7 @@ private static Tuple4<Set<Sentence>, Sort, K, Boolean> computeSentencesOfWellFor
SyntaxSort(
Seq(),
bagSort,
Att.empty()
.add(Att.HOOK(), type.toUpperCase() + '.' + type)
.add(Att.CELL_COLLECTION()));
Att().add(Att.HOOK(), type.toUpperCase() + '.' + type).add(Att.CELL_COLLECTION()));
Sentence bagSubsort = Production(Seq(), bagSort, Seq(NonTerminal(sort)));
Sentence bagElement;
if (type.equals("Map")) {
Expand All @@ -609,10 +607,7 @@ private static Tuple4<Set<Sentence>, Sort, K, Boolean> computeSentencesOfWellFor
Terminal(","),
NonTerminal(sort),
Terminal(")")),
Att.empty()
.add(Att.HOOK(), elementHook)
.add(Att.FUNCTION())
.add(Att.FORMAT(), "%5"));
Att().add(Att.HOOK(), elementHook).add(Att.FUNCTION()).add(Att.FORMAT(), "%5"));
} else {
bagElement =
Production(
Expand All @@ -623,17 +618,14 @@ private static Tuple4<Set<Sentence>, Sort, K, Boolean> computeSentencesOfWellFor
Terminal("("),
NonTerminal(sort),
Terminal(")")),
Att.empty()
.add(Att.HOOK(), elementHook)
.add(Att.FUNCTION())
.add(Att.FORMAT(), "%3"));
Att().add(Att.HOOK(), elementHook).add(Att.FUNCTION()).add(Att.FORMAT(), "%3"));
}
Sentence bagUnit =
Production(
KLabel("." + bagSort.name()),
bagSort,
Seq(Terminal("." + bagSort.name())),
Att.empty().add(Att.HOOK(), unitHook).add(Att.FUNCTION()));
Att().add(Att.HOOK(), unitHook).add(Att.FUNCTION()));
Sentence bag =
Production(
KLabel("_" + bagSort + "_"),
Expand All @@ -657,7 +649,7 @@ private static Tuple4<Set<Sentence>, Sort, K, Boolean> computeSentencesOfWellFor
Terminal("("),
NonTerminal(bagSort),
Terminal(")")),
Att.empty().add(Att.HOOK(), "MAP.in_keys").add(Att.FUNCTION()).add(Att.TOTAL())));
Att().add(Att.HOOK(), "MAP.in_keys").add(Att.FUNCTION()).add(Att.TOTAL())));

// syntax KeyCell ::= CellMapKey(Cell) [function, total]
// rule CellMapKey(<cell> K ...<\cell>) => K
Expand All @@ -671,7 +663,7 @@ private static Tuple4<Set<Sentence>, Sort, K, Boolean> computeSentencesOfWellFor
Terminal("("),
NonTerminal(sort),
Terminal(")")),
Att.empty().add(Att.FUNCTION()).add(Att.TOTAL()));
Att().add(Att.FUNCTION()).add(Att.TOTAL()));
KVariable key =
KVariable("Key", Att.empty().add(Att.SORT(), Sort.class, childSorts.get(0)));
Rule cellMapKeyRule =
Expand Down Expand Up @@ -772,7 +764,7 @@ private static KApply optionalCellInitializer(
}

private static Att getCellPropertiesAsAtt(K k, String cellName) {
Att att = Att.empty();
Att att = Att();
if (cellName.equals("k")) {
att = att.add(Att.MAINCELL());
}
Expand All @@ -783,11 +775,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.empty();
return Att();
} 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.empty()
return Att()
.add(attribute._1(), attribute._2())
.addAll(getCellPropertiesAsAtt(kapp.klist().items().get(1)));
}
Expand Down
4 changes: 2 additions & 2 deletions kernel/src/main/java/org/kframework/compile/GenerateSortPredicateRules.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -61,7 +61,7 @@ private Stream<? extends Sentence> gen(Sort sort) {
KRewrite(
KApply(
KLabel("is" + sort),
KVariable(sort.name(), Att.empty().add(Att.SORT(), Sort.class, sort))),
KVariable(sort.name(), Att().add(Att.SORT(), Sort.class, sort))),
BooleanUtils.TRUE),
BooleanUtils.TRUE,
BooleanUtils.TRUE));
Expand All @@ -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.empty().add(Att.OWISE())));
Att().add(Att.OWISE())));
return res.stream();
}
}
Expand Down
5 changes: 1 addition & 4 deletions kernel/src/main/java/org/kframework/compile/GenerateSortPredicateSyntax.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -39,10 +39,7 @@ public Set<Sentence> gen(Module mod, Sort sort) {
KLabel("is" + sort.toString()),
Sorts.Bool(),
Seq(Terminal("is" + sort), Terminal("("), NonTerminal(Sorts.K()), Terminal(")")),
Att.empty()
.add(Att.FUNCTION())
.add(Att.TOTAL())
.add(Att.PREDICATE(), Sort.class, sort));
Att().add(Att.FUNCTION()).add(Att.TOTAL()).add(Att.PREDICATE(), Sort.class, sort));
if (!mod.productions().contains(prod)) return Collections.singleton(prod);
return Collections.emptySet();
}
Expand Down
8 changes: 4 additions & 4 deletions kernel/src/main/java/org/kframework/compile/GenerateSortProjections.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -77,7 +77,7 @@ public Stream<? extends Sentence> gen(Sort sort) {
KRewrite(KApply(lbl, var), var),
BooleanUtils.TRUE,
BooleanUtils.TRUE,
Att.empty().add(Att.PROJECTION()));
Att().add(Att.PROJECTION()));
if (mod.definedKLabels().contains(lbl)) {
return Stream.empty();
}
Expand All @@ -86,7 +86,7 @@ public Stream<? extends Sentence> gen(Sort sort) {
lbl,
sort,
Seq(Terminal(lbl.name()), Terminal("("), NonTerminal(Sorts.K()), Terminal(")")),
Att.empty().add(Att.FUNCTION()).add(Att.PROJECTION()));
Att().add(Att.FUNCTION()).add(Att.PROJECTION()));
if (cover) {
KLabel sideEffectLbl = KLabel("sideEffect:" + sort);
Production sideEffect =
Expand All @@ -100,7 +100,7 @@ public Stream<? extends Sentence> gen(Sort sort) {
Terminal(","),
NonTerminal(sort),
Terminal(")")),
Att.empty().add(Att.FUNCTION()));
Att().add(Att.FUNCTION()));
Rule sideEffectR =
Rule(
KRewrite(
Expand Down Expand Up @@ -149,7 +149,7 @@ public Stream<? extends Sentence> gen(Production prod) {
Terminal("("),
NonTerminal(prod.sort()),
Terminal(")")),
Att.empty().add(Att.FUNCTION())));
Att().add(Att.FUNCTION())));
sentences.add(
Rule(
KRewrite(KApply(lbl, KApply(prod.klabel().get(), KList(vars))), vars.get(i)),
Expand Down
3 changes: 1 addition & 2 deletions kernel/src/main/java/org/kframework/compile/GuardOrPatterns.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -95,8 +95,7 @@ KVariable newDotVariable(Sort s) {
do {
newLabel =
KVariable(
"_Gen" + (counter++),
Att.empty().add(Att.ANONYMOUS()).add(Att.SORT(), Sort.class, s));
"_Gen" + (counter++), Att().add(Att.ANONYMOUS()).add(Att.SORT(), Sort.class, s));
} while (vars.contains(newLabel));
vars.add(newLabel);
return newLabel;
Expand Down
2 changes: 1 addition & 1 deletion kernel/src/main/java/org/kframework/compile/MinimizeTermConstruction.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -219,7 +219,7 @@ public K apply(KApply k) {
KVariable newDotVariable(Sort sort) {
KVariable newLabel;
do {
newLabel = KVariable("_Gen" + (counter++), Att.empty().add(Att.SORT(), Sort.class, sort));
newLabel = KVariable("_Gen" + (counter++), Att().add(Att.SORT(), Sort.class, sort));
} while (vars.contains(newLabel));
vars.add(newLabel);
return newLabel;
Expand Down
6 changes: 3 additions & 3 deletions kernel/src/main/java/org/kframework/compile/ResolveAnonVar.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -121,7 +121,7 @@ public K apply(KVariable k) {
KVariable newDotVariable(String prefix, K k) {
KVariable newLabel;
Att locInfo =
Optional.of(Att.empty())
Optional.of(Att())
.flatMap(
att ->
k.att()
Expand All @@ -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.empty());
Att att = Att.empty().add(Att.ANONYMOUS()).addAll(locInfo);
.orElse(Att());
Att att = Att().add(Att.ANONYMOUS()).addAll(locInfo);
if (prefix.equals("?")) {
att = att.add(Att.FRESH());
}
Expand Down
Loading

0 comments on commit ec70555

Please sign in to comment.