From ec70555ac575bdba60ae59c389de3bebbdc47509 Mon Sep 17 00:00:00 2001 From: Bruce Collie Date: Tue, 5 Mar 2024 18:02:45 +0000 Subject: [PATCH] Revert "Miscellaneous Scala clean up" (#4078) Reverts runtimeverification/k#4055 We will want to reinstate this PR once the required `scala-kore` infrastructure is actually ready to use. --- flake.nix | 5 +-- .../kframework/backend/kore/ModuleToKORE.java | 9 ++-- .../kframework/compile/AddSortInjections.java | 2 +- .../org/kframework/compile/CloseCells.java | 5 +-- .../kframework/compile/ConstantFolding.java | 2 +- .../GenerateSentencesFromConfigDecl.java | 40 +++++++----------- .../compile/GenerateSortPredicateRules.java | 4 +- .../compile/GenerateSortPredicateSyntax.java | 5 +-- .../compile/GenerateSortProjections.java | 8 ++-- .../kframework/compile/GuardOrPatterns.java | 3 +- .../compile/MinimizeTermConstruction.java | 2 +- .../kframework/compile/ResolveAnonVar.java | 6 +-- .../kframework/compile/ResolveContexts.java | 26 +++--------- .../compile/ResolveFreshConstants.java | 5 +-- .../org/kframework/compile/ResolveFun.java | 4 +- .../compile/ResolveFunctionWithConfig.java | 5 +-- .../org/kframework/compile/SortCells.java | 3 +- .../kframework/kompile/DefinitionParsing.java | 2 +- .../java/org/kframework/kompile/Kompile.java | 4 +- .../kframework/kore/convertors/KILtoKORE.java | 10 ++--- .../org/kframework/parser/ParserUtils.java | 2 +- .../parser/inner/RuleGrammarGenerator.java | 12 +++--- .../compile/AddParentsCellsTest.java | 9 +--- .../kframework/compile/CloseCellsTest.java | 9 +--- .../GenerateSentencesFromConfigDeclTest.java | 34 +++++++-------- .../org/kframework/compile/SortCellsTest.java | 25 ++++++----- kore/pom.xml | 12 +++++- .../src/main/scala/org/kframework/POSet.scala | 2 +- .../scala/org/kframework/attributes/Att.scala | 2 +- .../compile/ConfigurationInfoFromModule.scala | 4 +- .../org/kframework/compile/MergeRules.scala | 2 +- .../org/kframework/compile/RewriteToTop.scala | 4 +- .../definition/outer-to-string.scala | 7 ++-- .../scala/org/kframework/kore/Assoc.scala | 2 +- .../main/scala/org/kframework/kore/KORE.scala | 42 +++++-------------- .../org/kframework/kore/ScalaSugar.scala | 38 +++++++++++++++++ .../kframework/parser/TreeNodesToKORE.scala | 4 +- .../kframework/unparser/KOREToTreeNodes.scala | 4 +- .../org/kframework/unparser/UnparseTest.scala | 40 ++++++------------ nix/build-maven-package.nix | 11 +---- nix/k.nix | 6 +-- pom.xml | 12 ++---- 42 files changed, 190 insertions(+), 243 deletions(-) create mode 100644 kore/src/main/scala/org/kframework/kore/ScalaSugar.scala diff --git a/flake.nix b/flake.nix index f6aaab5633d..9dcc385a76f 100644 --- a/flake.nix +++ b/flake.nix @@ -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}"; diff --git a/kernel/src/main/java/org/kframework/backend/kore/ModuleToKORE.java b/kernel/src/main/java/org/kframework/backend/kore/ModuleToKORE.java index 9833b5a0d45..2e52e5e7c73 100644 --- a/kernel/src/main/java/org/kframework/backend/kore/ModuleToKORE.java +++ b/kernel/src/main/java/org/kframework/backend/kore/ModuleToKORE.java @@ -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; @@ -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); } @@ -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 = @@ -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); @@ -1869,7 +1870,7 @@ private void collectAttributes(Map 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); diff --git a/kernel/src/main/java/org/kframework/compile/AddSortInjections.java b/kernel/src/main/java/org/kframework/compile/AddSortInjections.java index bccccbbefa1..f36e64ff014 100644 --- a/kernel/src/main/java/org/kframework/compile/AddSortInjections.java +++ b/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.empty()) + .getOrElse(() -> Att()) .getOptional(Att.HOOK()) .orElse(""); if ((hookAtt.equals("MAP.Map") || hookAtt.equals("SET.Set") || hookAtt.equals("LIST.List")) diff --git a/kernel/src/main/java/org/kframework/compile/CloseCells.java b/kernel/src/main/java/org/kframework/compile/CloseCells.java index cdb600d0d84..1d37ab99ac9 100644 --- a/kernel/src/main/java/org/kframework/compile/CloseCells.java +++ b/kernel/src/main/java/org/kframework/compile/CloseCells.java @@ -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); diff --git a/kernel/src/main/java/org/kframework/compile/ConstantFolding.java b/kernel/src/main/java/org/kframework/compile/ConstantFolding.java index fa4c03568ed..de4be22673c 100644 --- a/kernel/src/main/java/org/kframework/compile/ConstantFolding.java +++ b/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.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 + "."))) { diff --git a/kernel/src/main/java/org/kframework/compile/GenerateSentencesFromConfigDecl.java b/kernel/src/main/java/org/kframework/compile/GenerateSentencesFromConfigDecl.java index 9ddb87d3f76..cd1c837844f 100644 --- a/kernel/src/main/java/org/kframework/compile/GenerateSentencesFromConfigDecl.java +++ b/kernel/src/main/java/org/kframework/compile/GenerateSentencesFromConfigDecl.java @@ -438,7 +438,7 @@ private static Tuple4, 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( @@ -447,14 +447,14 @@ private static Tuple4, 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( @@ -463,7 +463,7 @@ private static Tuple4, 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); @@ -505,7 +505,7 @@ private static Tuple4, 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))); } } } @@ -516,7 +516,7 @@ private static Tuple4, 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)))); } } @@ -553,7 +553,7 @@ private static Tuple4, 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") @@ -587,9 +587,7 @@ private static Tuple4, 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")) { @@ -609,10 +607,7 @@ private static Tuple4, 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( @@ -623,17 +618,14 @@ private static Tuple4, 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 + "_"), @@ -657,7 +649,7 @@ private static Tuple4, 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( K ...<\cell>) => K @@ -671,7 +663,7 @@ private static Tuple4, 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 = @@ -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()); } @@ -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 attribute = getCellProperty(kapp.klist().items().get(0)); - return Att.empty() + return Att() .add(attribute._1(), attribute._2()) .addAll(getCellPropertiesAsAtt(kapp.klist().items().get(1))); } diff --git a/kernel/src/main/java/org/kframework/compile/GenerateSortPredicateRules.java b/kernel/src/main/java/org/kframework/compile/GenerateSortPredicateRules.java index ac17610ad2e..03a66176227 100644 --- a/kernel/src/main/java/org/kframework/compile/GenerateSortPredicateRules.java +++ b/kernel/src/main/java/org/kframework/compile/GenerateSortPredicateRules.java @@ -61,7 +61,7 @@ private Stream 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)); @@ -70,7 +70,7 @@ private Stream 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(); } } diff --git a/kernel/src/main/java/org/kframework/compile/GenerateSortPredicateSyntax.java b/kernel/src/main/java/org/kframework/compile/GenerateSortPredicateSyntax.java index 5148ffc0b9f..485a2c02528 100644 --- a/kernel/src/main/java/org/kframework/compile/GenerateSortPredicateSyntax.java +++ b/kernel/src/main/java/org/kframework/compile/GenerateSortPredicateSyntax.java @@ -39,10 +39,7 @@ public Set 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(); } diff --git a/kernel/src/main/java/org/kframework/compile/GenerateSortProjections.java b/kernel/src/main/java/org/kframework/compile/GenerateSortProjections.java index 5bc24ff704d..b51d2388104 100644 --- a/kernel/src/main/java/org/kframework/compile/GenerateSortProjections.java +++ b/kernel/src/main/java/org/kframework/compile/GenerateSortProjections.java @@ -77,7 +77,7 @@ public Stream 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(); } @@ -86,7 +86,7 @@ public Stream 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 = @@ -100,7 +100,7 @@ public Stream gen(Sort sort) { Terminal(","), NonTerminal(sort), Terminal(")")), - Att.empty().add(Att.FUNCTION())); + Att().add(Att.FUNCTION())); Rule sideEffectR = Rule( KRewrite( @@ -149,7 +149,7 @@ public Stream 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)), diff --git a/kernel/src/main/java/org/kframework/compile/GuardOrPatterns.java b/kernel/src/main/java/org/kframework/compile/GuardOrPatterns.java index e2d2223a8e7..6ee5564be82 100644 --- a/kernel/src/main/java/org/kframework/compile/GuardOrPatterns.java +++ b/kernel/src/main/java/org/kframework/compile/GuardOrPatterns.java @@ -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; diff --git a/kernel/src/main/java/org/kframework/compile/MinimizeTermConstruction.java b/kernel/src/main/java/org/kframework/compile/MinimizeTermConstruction.java index 8a94e94b415..4bbb7084728 100644 --- a/kernel/src/main/java/org/kframework/compile/MinimizeTermConstruction.java +++ b/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.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; diff --git a/kernel/src/main/java/org/kframework/compile/ResolveAnonVar.java b/kernel/src/main/java/org/kframework/compile/ResolveAnonVar.java index 5e58962e0dd..4a27b9b02ae 100644 --- a/kernel/src/main/java/org/kframework/compile/ResolveAnonVar.java +++ b/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.empty()) + Optional.of(Att()) .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.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()); } diff --git a/kernel/src/main/java/org/kframework/compile/ResolveContexts.java b/kernel/src/main/java/org/kframework/compile/ResolveContexts.java index 97ea822a0c3..e42e7f30ba1 100644 --- a/kernel/src/main/java/org/kframework/compile/ResolveContexts.java +++ b/kernel/src/main/java/org/kframework/compile/ResolveContexts.java @@ -105,10 +105,7 @@ private Stream resolve(Context context, Module input) { new FoldK() { @Override public Boolean apply(KApply k) { - if (input - .attributesFor() - .getOrElse(k.klabel(), () -> Att.empty()) - .contains(Att.MAINCELL())) { + if (input.attributesFor().getOrElse(k.klabel(), () -> Att()).contains(Att.MAINCELL())) { return true; } return super.apply(k); @@ -161,19 +158,13 @@ public void apply(KVariable k) { @Override public void apply(KApply k) { - if (input - .attributesFor() - .getOrElse(k.klabel(), () -> Att.empty()) - .contains(Att.MAINCELL())) { + if (input.attributesFor().getOrElse(k.klabel(), () -> Att()).contains(Att.MAINCELL())) { inMainCell = true; } if (k.klabel() instanceof KVariable && (inMainCell || !hasMainCell)) vars.put((KVariable) k.klabel(), InjectedKLabel(k.klabel())); super.apply(k); - if (input - .attributesFor() - .getOrElse(k.klabel(), () -> Att.empty()) - .contains(Att.MAINCELL())) { + if (input.attributesFor().getOrElse(k.klabel(), () -> Att()).contains(Att.MAINCELL())) { inMainCell = false; } } @@ -190,10 +181,7 @@ public K process(K k) { @Override public void apply(KApply k) { - if (input - .attributesFor() - .getOrElse(k.klabel(), () -> Att.empty()) - .contains(Att.MAINCELL())) { + if (input.attributesFor().getOrElse(k.klabel(), () -> Att()).contains(Att.MAINCELL())) { cooled = k.items().get(1); } super.apply(k); @@ -223,7 +211,7 @@ public void apply(KApply k) { items.remove(items.size() - 1); } items.add(Terminal(")")); - Production freezer = Production(freezerLabel, Sorts.KItem(), immutable(items), Att.empty()); + Production freezer = Production(freezerLabel, Sorts.KItem(), immutable(items), Att()); K frozen = KApply(freezerLabel, vars.values().stream().collect(Collections.toList())); Att heatAtt = addSuffixToLabel(context.att().add(Att.HEAT()), "-heat"); @@ -278,9 +266,7 @@ class Holder { new TransformK() { @Override public K apply(KApply k) { - if (mod.attributesFor() - .getOrElse(k.klabel(), () -> Att.empty()) - .contains(Att.MAINCELL())) { + if (mod.attributesFor().getOrElse(k.klabel(), () -> Att()).contains(Att.MAINCELL())) { h.found = true; return KApply(k.klabel(), k.items().get(0), rewrite, k.items().get(2)); } diff --git a/kernel/src/main/java/org/kframework/compile/ResolveFreshConstants.java b/kernel/src/main/java/org/kframework/compile/ResolveFreshConstants.java index 1bab71cc435..d9514effab3 100644 --- a/kernel/src/main/java/org/kframework/compile/ResolveFreshConstants.java +++ b/kernel/src/main/java/org/kframework/compile/ResolveFreshConstants.java @@ -94,10 +94,7 @@ private Rule resolve(Rule rule) { } if (left instanceof KApply) { kapp = (KApply) left; - if (m.attributesFor() - .get(kapp.klabel()) - .getOrElse(() -> Att.empty()) - .contains(Att.FUNCTION())) { + if (m.attributesFor().get(kapp.klabel()).getOrElse(() -> Att()).contains(Att.FUNCTION())) { return rule; } } diff --git a/kernel/src/main/java/org/kframework/compile/ResolveFun.java b/kernel/src/main/java/org/kframework/compile/ResolveFun.java index ed7fccdd4d3..14abd0f9147 100644 --- a/kernel/src/main/java/org/kframework/compile/ResolveFun.java +++ b/kernel/src/main/java/org/kframework/compile/ResolveFun.java @@ -218,7 +218,7 @@ private List closure(K k) { } private Production funProd(KLabel fun, K k, Sort arg, boolean total) { - Att att = total ? Att.empty().add(Att.TOTAL()) : Att.empty(); + Att att = total ? Att().add(Att.TOTAL()) : Att(); return lambdaProd(fun, k, arg, sort(RewriteToTop.toRight(k)), att); } @@ -227,7 +227,7 @@ private Production predProd(KLabel fun, K k, Sort arg) { } private Production lambdaProd(KLabel fun, K k, Sort arg, Sort rhs) { - return lambdaProd(fun, k, arg, rhs, Att.empty()); + return lambdaProd(fun, k, arg, rhs, Att()); } private Production lambdaProd(KLabel fun, K k, Sort arg, Sort rhs, Att att) { diff --git a/kernel/src/main/java/org/kframework/compile/ResolveFunctionWithConfig.java b/kernel/src/main/java/org/kframework/compile/ResolveFunctionWithConfig.java index d22bacb7f03..851b0c338bd 100644 --- a/kernel/src/main/java/org/kframework/compile/ResolveFunctionWithConfig.java +++ b/kernel/src/main/java/org/kframework/compile/ResolveFunctionWithConfig.java @@ -63,8 +63,7 @@ public ResolveFunctionWithConfig(Module mod) { topCellLabel = KLabels.GENERATED_TOP_CELL; CONFIG_VAR = KVariable( - "#Configuration", - Att.empty().add(Att.SORT(), Sort.class, topCell).add(Att.WITH_CONFIG())); + "#Configuration", Att().add(Att.SORT(), Sort.class, topCell).add(Att.WITH_CONFIG())); } private boolean ruleNeedsConfig(RuleOrClaim r) { @@ -166,7 +165,7 @@ private K resolve(K body, Module module) { List items = Stream.concat( funKApp.items().stream(), - Stream.of(KAs(secondChild, CONFIG_VAR, Att.empty().add(Att.WITH_CONFIG())))) + Stream.of(KAs(secondChild, CONFIG_VAR, Att().add(Att.WITH_CONFIG())))) .collect(Collections.toList()); K result = KApply(funKApp.klabel(), KList(items), funKApp.att()); if (rhs == null) { diff --git a/kernel/src/main/java/org/kframework/compile/SortCells.java b/kernel/src/main/java/org/kframework/compile/SortCells.java index 4967894bc66..bf499ac1291 100644 --- a/kernel/src/main/java/org/kframework/compile/SortCells.java +++ b/kernel/src/main/java/org/kframework/compile/SortCells.java @@ -890,8 +890,7 @@ public K apply(KApply k0) { .name() .substring(0, cellFragmentSort.name().indexOf("Fragment"))); KLabel cellLabel = cfg.cfg().getCellLabel(cellSort); - klist0.set( - idx, KApply(cellLabel, KList(item0), Att.empty().add(Att.DUMMY_CELL()))); + klist0.set(idx, KApply(cellLabel, KList(item0), Att().add(Att.DUMMY_CELL()))); } } } diff --git a/kernel/src/main/java/org/kframework/kompile/DefinitionParsing.java b/kernel/src/main/java/org/kframework/kompile/DefinitionParsing.java index 748a9ef03f2..3fa75aa1992 100644 --- a/kernel/src/main/java/org/kframework/kompile/DefinitionParsing.java +++ b/kernel/src/main/java/org/kframework/kompile/DefinitionParsing.java @@ -806,7 +806,7 @@ public Rule parseRule(CompiledDefinition compiledDef, String contents, Source so new Bubble( rule, contents, - Att.empty() + Att() .add(Att.CONTENT_START_LINE(), 1) .add(Att.CONTENT_START_COLUMN(), 1) .add(Att.SOURCE(), Source.class, source))) diff --git a/kernel/src/main/java/org/kframework/kompile/Kompile.java b/kernel/src/main/java/org/kframework/kompile/Kompile.java index d88b32367d8..91162d90937 100644 --- a/kernel/src/main/java/org/kframework/kompile/Kompile.java +++ b/kernel/src/main/java/org/kframework/kompile/Kompile.java @@ -457,7 +457,7 @@ public static Module subsortKItem(Module module) { for (Sort srt : iterable(module.allSorts())) { if (!RuleGrammarGenerator.isParserSort(srt)) { // KItem ::= Sort - Production prod = Production(Seq(), Sorts.KItem(), Seq(NonTerminal(srt)), Att.empty()); + Production prod = Production(Seq(), Sorts.KItem(), Seq(NonTerminal(srt)), Att()); if (!module.sentences().contains(prod)) { prods.add(prod); } @@ -726,7 +726,7 @@ public static Definition addSemanticsModule(Definition d) { Import(d.getModule("K-TERM").get(), true), Import(d.getModule(RuleGrammarGenerator.ID_PROGRAM_PARSING).get(), true)), Set(), - Att.empty()); + Att()); allModules.add(languageParsingModule); return Constructors.Definition(d.mainModule(), immutable(allModules), d.att()); } diff --git a/kernel/src/main/java/org/kframework/kore/convertors/KILtoKORE.java b/kernel/src/main/java/org/kframework/kore/convertors/KILtoKORE.java index d6434537639..66fc49f1886 100644 --- a/kernel/src/main/java/org/kframework/kore/convertors/KILtoKORE.java +++ b/kernel/src/main/java/org/kframework/kore/convertors/KILtoKORE.java @@ -121,7 +121,7 @@ public org.kframework.definition.Definition apply(Definition d) { + " when loading from front-end classes."); }), koreModules, - Att.empty()); + Att()); } @SuppressWarnings("unchecked") @@ -391,14 +391,14 @@ public static org.kframework.attributes.Att convertAttributes(ASTNode t) { private static Att attributesFromSource(Source source) { if (source != null) { - return Att.empty().add(Att.SOURCE(), Source.class, source); + return Att().add(Att.SOURCE(), Source.class, source); } - return Att.empty(); + return Att(); } private static org.kframework.attributes.Att attributesFromLocation(Location location) { if (location != null) { - return Att.empty().add(Att.LOCATION(), Location.class, location); - } else return Att.empty(); + return Att().add(Att.LOCATION(), Location.class, location); + } else return Att(); } } diff --git a/kernel/src/main/java/org/kframework/parser/ParserUtils.java b/kernel/src/main/java/org/kframework/parser/ParserUtils.java index 81372701eb1..58c230c74de 100644 --- a/kernel/src/main/java/org/kframework/parser/ParserUtils.java +++ b/kernel/src/main/java/org/kframework/parser/ParserUtils.java @@ -422,7 +422,7 @@ public org.kframework.definition.Definition loadDefinition( } return org.kframework.definition.Definition.apply( - mainModule, immutable(modules), Att.empty().add(Att.SYNTAX_MODULE(), syntaxModule.name())); + mainModule, immutable(modules), Att().add(Att.SYNTAX_MODULE(), syntaxModule.name())); } private Module getMainModule(String mainModuleName, Set modules) { diff --git a/kernel/src/main/java/org/kframework/parser/inner/RuleGrammarGenerator.java b/kernel/src/main/java/org/kframework/parser/inner/RuleGrammarGenerator.java index eee88c54516..56c73150d9a 100644 --- a/kernel/src/main/java/org/kframework/parser/inner/RuleGrammarGenerator.java +++ b/kernel/src/main/java/org/kframework/parser/inner/RuleGrammarGenerator.java @@ -418,7 +418,7 @@ public static Tuple3 getCombinedGrammarImpl( // syntax MInt{K} ::= MInt{6} Production p1 = Production( - Option.empty(), Seq(), Sort(s.name(), Sorts.K()), Seq(NonTerminal(s)), Att.empty()); + Option.empty(), Seq(), Sort(s.name(), Sorts.K()), Seq(NonTerminal(s)), Att()); prods.add(p1); } } @@ -627,7 +627,7 @@ public static Tuple3 getCombinedGrammarImpl( for (Sort srt : iterable(mod.allSorts())) { if (!isParserSort(srt) && !mod.listSorts().contains(srt)) { // KItem ::= Sort - prods3.add(Production(Seq(), Sorts.KItem(), Seq(NonTerminal(srt)), Att.empty())); + prods3.add(Production(Seq(), Sorts.KItem(), Seq(NonTerminal(srt)), Att())); } } // Add KItem subsorts to disambiguation for use by sort inference @@ -701,14 +701,14 @@ public static Tuple3 getCombinedGrammarImpl( Seq(), ul.sort, Seq(NonTerminal(Sort("Ne#" + ul.sort.name(), ul.sort.params()))), - Att.empty().add(Att.NOT_INJECTION())); + Att().add(Att.NOT_INJECTION())); // Es ::= Es#Terminator // if the list is * prod5 = Production( Seq(), ul.sort, Seq(NonTerminal(Sort(ul.sort.name() + "#Terminator", ul.sort.params()))), - Att.empty().add(Att.NOT_INJECTION())); + Att().add(Att.NOT_INJECTION())); } res.add(prod1); @@ -769,7 +769,7 @@ private static void addCellNameProd(Set prods, Sentence prod) { for (ProductionItem pi : iterable(((Production) prod).items())) { if (pi instanceof Terminal t) { if (alphaNum.matcher(t.value()).matches()) { - prods.add(Production(Seq(), Sorts.CellName(), Seq(t), Att.empty().add(Att.TOKEN()))); + prods.add(Production(Seq(), Sorts.CellName(), Seq(t), Att().add(Att.TOKEN()))); } } } @@ -778,7 +778,7 @@ private static void addCellNameProd(Set prods, Sentence prod) { private static Set makeCasts(Sort innerSort, Sort castSort, Sort labelSort) { Set prods = new HashSet<>(); - Att attrs1 = Att.empty().add(Att.SORT(), Sort.class, castSort); + Att attrs1 = Att().add(Att.SORT(), Sort.class, castSort); prods.add( Production( KLabel("#SyntacticCast"), diff --git a/kernel/src/test/java/org/kframework/compile/AddParentsCellsTest.java b/kernel/src/test/java/org/kframework/compile/AddParentsCellsTest.java index 6356daad2e4..01cb0fcc71f 100644 --- a/kernel/src/test/java/org/kframework/compile/AddParentsCellsTest.java +++ b/kernel/src/test/java/org/kframework/compile/AddParentsCellsTest.java @@ -13,7 +13,6 @@ import org.junit.rules.ExpectedException; import org.kframework.attributes.Att; import org.kframework.builtin.KLabels; -import org.kframework.builtin.Sorts; import org.kframework.kore.*; import org.kframework.utils.errorsystem.KEMException; @@ -50,10 +49,6 @@ public class AddParentsCellsTest { }; final AddParentCells pass = new AddParentCells(cfgInfo, labelInfo); - private static KToken intToToken(int n) { - return KToken(Integer.toString(n), Sorts.Int(), Att.empty()); - } - @Test public void testOneLeafCellNoCompletion() { K term = cell("", intToToken(2)); @@ -167,7 +162,7 @@ public void testRewriteWithCellVariable() { cell( "", KRewrite( - KVariable("KCell", Att.empty().add(Att.SORT(), Sort.class, Sort("KCell"))), + KVariable("KCell", Att().add(Att.SORT(), Sort.class, Sort("KCell"))), cell("", intToToken(1)))); K expected = cell( @@ -177,7 +172,7 @@ public void testRewriteWithCellVariable() { cell( "", KRewrite( - KVariable("KCell", Att.empty().add(Att.SORT(), Sort.class, Sort("KCell"))), + KVariable("KCell", Att().add(Att.SORT(), Sort.class, Sort("KCell"))), cell("", intToToken(1)))))); Assert.assertEquals(expected, pass.concretizeCell(term)); } diff --git a/kernel/src/test/java/org/kframework/compile/CloseCellsTest.java b/kernel/src/test/java/org/kframework/compile/CloseCellsTest.java index a3b5b8535a3..171d7ef496c 100644 --- a/kernel/src/test/java/org/kframework/compile/CloseCellsTest.java +++ b/kernel/src/test/java/org/kframework/compile/CloseCellsTest.java @@ -8,7 +8,6 @@ import org.junit.Rule; import org.junit.Test; import org.junit.rules.ExpectedException; -import org.kframework.attributes.Att; import org.kframework.builtin.KLabels; import org.kframework.builtin.Sorts; import org.kframework.kore.*; @@ -31,7 +30,7 @@ public class CloseCellsTest { addCell("ThreadCell", "EnvCell", "", Sort("Map")); addCell(null, "ListCell", "", Multiplicity.STAR, Sort("List")); addDefault("EnvCell", cell("", KApply(KLabel(".Map")))); - addDefault("KCell", cell("", KToken("defaultK", Sorts.String(), Att.empty()))); + addDefault("KCell", cell("", stringToToken("defaultK"))); } }; final LabelInfo labelInfo = @@ -46,10 +45,6 @@ public class CloseCellsTest { } }; - private static KToken intToToken(int n) { - return KToken(Integer.toString(n), Sorts.Int(), Att.empty()); - } - @Test public void testSimpleClosure() { K term = cell("", false, true, KApply(KLabel("_+_"), KVariable("I"), KVariable("J"))); @@ -147,7 +142,7 @@ public void testCloseCellTerm() { ccell( "", ccell("", intToToken(2)), - ccell("", KToken("defaultK", Sorts.String(), Att.empty()))))); + ccell("", stringToToken("defaultK"))))); Assert.assertEquals(expected, new CloseCells(cfgInfo, sortInfo, labelInfo).close(term)); } diff --git a/kernel/src/test/java/org/kframework/compile/GenerateSentencesFromConfigDeclTest.java b/kernel/src/test/java/org/kframework/compile/GenerateSentencesFromConfigDeclTest.java index 3d51e9ded09..3e851fb62a7 100644 --- a/kernel/src/test/java/org/kframework/compile/GenerateSentencesFromConfigDeclTest.java +++ b/kernel/src/test/java/org/kframework/compile/GenerateSentencesFromConfigDeclTest.java @@ -86,15 +86,14 @@ public void testSingleTop() { KLabel(".Opt"), KList(), Att.empty().add(Att.PRODUCTION(), Production.class, prod)))))); - Module m1 = - Module("CONFIG", Set(Import(def.getModule("KSEQ").get(), true)), Set(prod), Att.empty()); + Module m1 = Module("CONFIG", Set(Import(def.getModule("KSEQ").get(), true)), Set(prod), Att()); RuleGrammarGenerator parserGen = new RuleGrammarGenerator(def); Module m = RuleGrammarGenerator.getCombinedGrammar(parserGen.getConfigGrammar(m1), files) .getExtensionModule(); Set gen = - GenerateSentencesFromConfigDecl.gen(configuration, BooleanUtils.FALSE, Att.empty(), m); - Att initializerAtts = Att.empty().add(Att.INITIALIZER()); + GenerateSentencesFromConfigDecl.gen(configuration, BooleanUtils.FALSE, Att(), m); + Att initializerAtts = Att().add(Att.INITIALIZER()); Att productionAtts = initializerAtts.add(Att.FUNCTION()); Set reference = Set( @@ -105,19 +104,19 @@ public void testSingleTop() { Terminal(""), NonTerminal(Sort("ThreadCellBag")), Terminal("")), - Att.empty() + Att() .add(Att.CELL()) .add(Att.CELL_NAME(), "threads") .add(Att.FORMAT(), "%1%i%n%2%d%n%3")), SyntaxSort( Seq(), Sort("ThreadCellBag"), - Att.empty().add(Att.HOOK(), "BAG.Bag").add(Att.CELL_COLLECTION())), + Att().add(Att.HOOK(), "BAG.Bag").add(Att.CELL_COLLECTION())), Production( KLabel("_ThreadCellBag_"), Sort("ThreadCellBag"), Seq(NonTerminal(Sort("ThreadCellBag")), NonTerminal(Sort("ThreadCellBag"))), - Att.empty() + Att() .add(Att.ASSOC(), "") .add(Att.COMM(), "") .add(Att.UNIT(), ".ThreadCellBag") @@ -132,7 +131,7 @@ public void testSingleTop() { KLabel(".ThreadCellBag"), Sort("ThreadCellBag"), Seq(Terminal(".ThreadCellBag")), - Att.empty().add(Att.FUNCTION()).add(Att.HOOK(), "BAG.unit")), + Att().add(Att.FUNCTION()).add(Att.HOOK(), "BAG.unit")), Production(Seq(), Sort("ThreadCellBag"), Seq(NonTerminal(Sort("ThreadCell")))), Production( KLabel("ThreadCellBagItem"), @@ -142,10 +141,7 @@ public void testSingleTop() { Terminal("("), NonTerminal(Sort("ThreadCell")), Terminal(")")), - Att.empty() - .add(Att.FUNCTION()) - .add(Att.HOOK(), "BAG.element") - .add(Att.FORMAT(), "%3")), + Att().add(Att.FUNCTION()).add(Att.HOOK(), "BAG.element").add(Att.FORMAT(), "%3")), Production( KLabel(""), Sort("ThreadCell"), @@ -154,7 +150,7 @@ public void testSingleTop() { NonTerminal(Sort("KCell")), NonTerminal(Sort("OptCell")), Terminal("")), - Att.empty() + Att() .add(Att.CELL()) .add(Att.CELL_NAME(), "thread") .add(Att.MULTIPLICITY(), "*") @@ -163,7 +159,7 @@ public void testSingleTop() { KLabel(""), Sort("KCell"), Seq(Terminal(""), NonTerminal(Sort("K")), Terminal("")), - Att.empty() + Att() .add(Att.CELL()) .add(Att.CELL_NAME(), "k") .add(Att.MAINCELL()) @@ -172,7 +168,7 @@ public void testSingleTop() { KLabel(""), Sort("OptCell"), Seq(Terminal(""), NonTerminal(Sort("OptCellContent")), Terminal("")), - Att.empty() + Att() .add(Att.CELL()) .add(Att.CELL_NAME(), "opt") .add(Att.MULTIPLICITY(), "?") @@ -263,7 +259,7 @@ public void testSingleTop() { Terminal("-fragment"), NonTerminal(Sort("ThreadCellBag")), Terminal("-fragment")), - Att.empty().add(Att.CELL_FRAGMENT(), Sort.class, Sort("ThreadsCell"))), + Att().add(Att.CELL_FRAGMENT(), Sort.class, Sort("ThreadsCell"))), Production( KLabel("-fragment"), Sort("ThreadCellFragment"), @@ -272,19 +268,19 @@ public void testSingleTop() { NonTerminal(Sort("KCellOpt")), NonTerminal(Sort("OptCellOpt")), Terminal("-fragment")), - Att.empty().add(Att.CELL_FRAGMENT(), Sort.class, Sort("ThreadCell"))), + Att().add(Att.CELL_FRAGMENT(), Sort.class, Sort("ThreadCell"))), Production(Seq(), Sort("OptCellOpt"), Seq(NonTerminal(Sort("OptCell")))), Production( KLabel("noOptCell"), Sort("OptCellOpt"), Seq(Terminal("noOptCell")), - Att.empty().add(Att.CELL_OPT_ABSENT(), Sort.class, Sort("OptCell"))), + Att().add(Att.CELL_OPT_ABSENT(), Sort.class, Sort("OptCell"))), Production(Seq(), Sort("KCellOpt"), Seq(NonTerminal(Sort("KCell")))), Production( KLabel("noKCell"), Sort("KCellOpt"), Seq(Terminal("noKCell")), - Att.empty().add(Att.CELL_OPT_ABSENT(), Sort.class, Sort("KCell")))); + Att().add(Att.CELL_OPT_ABSENT(), Sort.class, Sort("KCell")))); assertEquals("Produced unexpected productions", Set(), gen.$amp$tilde(reference)); assertEquals("Missing expected productions", Set(), reference.$amp$tilde(gen)); diff --git a/kernel/src/test/java/org/kframework/compile/SortCellsTest.java b/kernel/src/test/java/org/kframework/compile/SortCellsTest.java index 9ca05af5b28..180d8992700 100644 --- a/kernel/src/test/java/org/kframework/compile/SortCellsTest.java +++ b/kernel/src/test/java/org/kframework/compile/SortCellsTest.java @@ -52,7 +52,7 @@ public class SortCellsTest { @Test public void testSimpleSplitting() { - KVariable Y = KVariable("Y", Att.empty().add(Att.SORT(), Sort.class, Sort("OptCell"))); + KVariable Y = KVariable("Y", Att().add(Att.SORT(), Sort.class, Sort("OptCell"))); K term = KRewrite(cell("", cell(""), KVariable("X"), Y), KVariable("X")); K expected = KRewrite( @@ -69,7 +69,7 @@ public void testSimpleSplitting() { */ @Test public void testSortedVar() { - KVariable Y = KVariable("Y", Att.empty().add(Att.SORT(), Sort.class, Sort("OptCell"))); + KVariable Y = KVariable("Y", Att().add(Att.SORT(), Sort.class, Sort("OptCell"))); K term = KRewrite(cell("", cell(""), KVariable("X"), Y), Y); K expected = KRewrite(cell("", KVariable("X"), cell(""), Y), Y); KExceptionManager kem = new KExceptionManager(new GlobalOptions()); @@ -433,25 +433,25 @@ public void testPredicateExpansion() { "", cell(""), KVariable("X"), - KVariable("Y", Att.empty().add(Att.SORT(), Sort.class, Sort("OptCell")))), + KVariable("Y", Att().add(Att.SORT(), Sort.class, Sort("OptCell")))), KVariable("X")), app("isThreadCellFragment", KVariable("X")), BooleanUtils.TRUE, - Att.empty()); + Att()); K expectedBody = KRewrite( cell( "", KVariable("X"), cell(""), - KVariable("Y", Att.empty().add(Att.SORT(), Sort.class, Sort("OptCell")))), + KVariable("Y", Att().add(Att.SORT(), Sort.class, Sort("OptCell")))), cell("-fragment", KVariable("X"), app("noEnvCell"), app(".OptCell"))); Rule expected = new Rule( expectedBody, BooleanUtils.and(BooleanUtils.TRUE, app("isKCell", KVariable("X"))), BooleanUtils.TRUE, - Att.empty()); + Att()); KExceptionManager kem = new KExceptionManager(new GlobalOptions()); Assert.assertEquals(expected, new SortCells(cfgInfo, labelInfo).sortCells(term)); Assert.assertEquals(0, kem.getExceptions().size()); @@ -471,11 +471,11 @@ public void testUnrelatedPredicate() { "", cell(""), KVariable("X"), - KVariable("Y", Att.empty().add(Att.SORT(), Sort.class, Sort("OptCell")))), + KVariable("Y", Att().add(Att.SORT(), Sort.class, Sort("OptCell")))), KVariable("X")), app("isTopCellFragment", KVariable("X")), BooleanUtils.TRUE, - Att.empty()); + Att()); K replacement = app("-fragment", KVariable("X"), app("noEnvCell"), app(".OptCell")); K expectedBody = KRewrite( @@ -483,11 +483,10 @@ public void testUnrelatedPredicate() { "", KVariable("X"), cell(""), - KVariable("Y", Att.empty().add(Att.SORT(), Sort.class, Sort("OptCell")))), + KVariable("Y", Att().add(Att.SORT(), Sort.class, Sort("OptCell")))), replacement); Rule expected = - new Rule( - expectedBody, app("isTopCellFragment", replacement), BooleanUtils.TRUE, Att.empty()); + new Rule(expectedBody, app("isTopCellFragment", replacement), BooleanUtils.TRUE, Att()); KExceptionManager kem = new KExceptionManager(new GlobalOptions()); Assert.assertEquals(expected, new SortCells(cfgInfo, labelInfo).sortCells(term)); Assert.assertEquals(0, kem.getExceptions().size()); @@ -499,8 +498,8 @@ public void testUnrelatedPredicate() { */ @Test public void testMultipleCells() { - KVariable T1 = KVariable("T1", Att.empty().add(Att.SORT(), Sort.class, Sort("ThreadCell"))); - KVariable T2 = KVariable("T2", Att.empty().add(Att.SORT(), Sort.class, Sort("ThreadCell"))); + KVariable T1 = KVariable("T1", Att().add(Att.SORT(), Sort.class, Sort("ThreadCell"))); + KVariable T2 = KVariable("T2", Att().add(Att.SORT(), Sort.class, Sort("ThreadCell"))); K term = cell("", KVariable("F"), cell("", KVariable("T")), app("_ThreadCellBag_", T1, T2)); K expected = diff --git a/kore/pom.xml b/kore/pom.xml index 81b049d1dfc..b98138dc0c3 100644 --- a/kore/pom.xml +++ b/kore/pom.xml @@ -53,7 +53,7 @@ net.alchim31.maven scala-maven-plugin - 4.8.1 + 3.3.1 scala-compile-first @@ -73,10 +73,18 @@ - -Werror + -Xexperimental -feature -deprecation + -language:implicitConversions + -language:postfixOps + + -source + ${java.version} + -target + ${java.version} + diff --git a/kore/src/main/scala/org/kframework/POSet.scala b/kore/src/main/scala/org/kframework/POSet.scala index baa8f85e760..d073f5a7c82 100644 --- a/kore/src/main/scala/org/kframework/POSet.scala +++ b/kore/src/main/scala/org/kframework/POSet.scala @@ -12,7 +12,7 @@ import scala.annotation.tailrec class POSet[T](val directRelations: Set[(T, T)]) extends Serializable { // convert the input set of relations to Map form for performance private val directRelationsMap: Map[T, Set[T]] = - directRelations.groupBy(_._1).mapValues(_.map(_._2).toSet).map(identity) + directRelations.groupBy(_._1).mapValues(_.map(_._2) toSet).map(identity) lazy val elements: Set[T] = directRelations.flatMap(a => Set(a._1, a._2)) diff --git a/kore/src/main/scala/org/kframework/attributes/Att.scala b/kore/src/main/scala/org/kframework/attributes/Att.scala index 7e37a646c5b..dd5419c39c6 100644 --- a/kore/src/main/scala/org/kframework/attributes/Att.scala +++ b/kore/src/main/scala/org/kframework/attributes/Att.scala @@ -571,6 +571,6 @@ trait AttributesToString { att.map { case ((attKey, `stringClassName`), "") => attKey.key case ((attKey, _), value) => attKey.key + "(" + value + ")" - }.toList + } toList } } diff --git a/kore/src/main/scala/org/kframework/compile/ConfigurationInfoFromModule.scala b/kore/src/main/scala/org/kframework/compile/ConfigurationInfoFromModule.scala index 48ee2e19aac..b7af001331c 100644 --- a/kore/src/main/scala/org/kframework/compile/ConfigurationInfoFromModule.scala +++ b/kore/src/main/scala/org/kframework/compile/ConfigurationInfoFromModule.scala @@ -124,7 +124,7 @@ class ConfigurationInfoFromModule(val m: Module) extends ConfigurationInfo { else Multiplicity.ONE - override def getParent(k: Sort): Sort = edges.collectFirst { case (p, `k`) => p }.get + override def getParent(k: Sort): Sort = edges.collectFirst { case (p, `k`) => p } get override def isCell(k: Sort): Boolean = cellSorts.contains(k) override def isCellLabel(kLabel: KLabel): Boolean = cellLabelsToSorts.contains(kLabel) override def isLeafCell(k: Sort): Boolean = !isParentCell(k) @@ -142,7 +142,7 @@ class ConfigurationInfoFromModule(val m: Module) extends ConfigurationInfo { override def leafCellType(k: Sort): Sort = cellProductions(k).items.collectFirst { case NonTerminal(n, _) => n - }.get + } get override def getDefaultCell(k: Sort): KApply = cellInitializer(k) diff --git a/kore/src/main/scala/org/kframework/compile/MergeRules.scala b/kore/src/main/scala/org/kframework/compile/MergeRules.scala index 19e38ba566b..ffdd5d7ca57 100644 --- a/kore/src/main/scala/org/kframework/compile/MergeRules.scala +++ b/kore/src/main/scala/org/kframework/compile/MergeRules.scala @@ -104,7 +104,7 @@ class MergeRules(val automatonAttribute: Att.Key, filterAttribute: Att.Key) setOfLists.head.indices .map(i => setOfLists.map(l => l(i))) .map(pushDisjunction) - val rulePs = ks.map(_._2).toSeq + val rulePs = ks.map(_._2) toSeq (KApply(klabel, childrenDisjunctionsOfklabel), KApply(or, rulePs)) } diff --git a/kore/src/main/scala/org/kframework/compile/RewriteToTop.scala b/kore/src/main/scala/org/kframework/compile/RewriteToTop.scala index d5025995ec8..751fd79e00c 100644 --- a/kore/src/main/scala/org/kframework/compile/RewriteToTop.scala +++ b/kore/src/main/scala/org/kframework/compile/RewriteToTop.scala @@ -15,7 +15,7 @@ object RewriteToTop { case t: KRewrite => t.left case t: KApply => compactInjections(KApply(t.klabel, immutable(t.klist.items).map(toLeft), t.att)) - case t: KSequence => KSequence(mutable(immutable(t.items).map(toLeft).toList), t.att) + case t: KSequence => KSequence(mutable(immutable(t.items).map(toLeft) toList), t.att) case t: KAs => KAs(toLeft(t.pattern), t.alias, t.att) case other => other } @@ -24,7 +24,7 @@ object RewriteToTop { case t: KRewrite => toRight(t.right) // recurse here because of KAs case t: KApply => compactInjections(KApply(t.klabel, immutable(t.klist.items).map(toRight), t.att)) - case t: KSequence => KSequence(mutable(immutable(t.items).map(toRight).toList), t.att) + case t: KSequence => KSequence(mutable(immutable(t.items).map(toRight) toList), t.att) case t: KAs => t.alias case other => other } diff --git a/kore/src/main/scala/org/kframework/definition/outer-to-string.scala b/kore/src/main/scala/org/kframework/definition/outer-to-string.scala index a2eb36f67ab..4bb6d6f95ab 100644 --- a/kore/src/main/scala/org/kframework/definition/outer-to-string.scala +++ b/kore/src/main/scala/org/kframework/definition/outer-to-string.scala @@ -86,10 +86,9 @@ trait SyntaxAssociativityToString { self: SyntaxAssociativity => override def toString = { val assocString = assoc match { - case Associativity.Left => "left" - case Associativity.Right => "right" - case Associativity.NonAssoc => "non-assoc" - case Associativity.Unspecified => "unspecified" + case Associativity.Left => "left" + case Associativity.Right => "right" + case Associativity.NonAssoc => "non-assoc" } "syntax associativity " + assocString + " " + tags.mkString(" ") + att.postfixString } diff --git a/kore/src/main/scala/org/kframework/kore/Assoc.scala b/kore/src/main/scala/org/kframework/kore/Assoc.scala index c0e56a03d25..4f8dd41c8be 100644 --- a/kore/src/main/scala/org/kframework/kore/Assoc.scala +++ b/kore/src/main/scala/org/kframework/kore/Assoc.scala @@ -26,7 +26,7 @@ object Assoc extends { else List(k) case other => List(other) - }.asJava + } asJava def flatten(label: KLabel, list: java.util.List[K], unit: KLabel): java.util.List[K] = flatten(label, list.asScala, unit).asJava diff --git a/kore/src/main/scala/org/kframework/kore/KORE.scala b/kore/src/main/scala/org/kframework/kore/KORE.scala index e78baddc4c2..06008125fcd 100644 --- a/kore/src/main/scala/org/kframework/kore/KORE.scala +++ b/kore/src/main/scala/org/kframework/kore/KORE.scala @@ -3,7 +3,6 @@ package org.kframework.kore import org.kframework.attributes import org.kframework.attributes.Att -import org.kframework.builtin.KLabels import scala.collection._ import scala.collection.JavaConverters._ @@ -14,26 +13,27 @@ import scala.collection.JavaConverters._ * See the wiki for more details: * https://github.com/runtimeverification/k/wiki/KORE-data-structures-guide */ -object KORE extends Constructors { +object KORE extends Constructors with ScalaSugared { + val c = KORE + val constructor = this + lazy val Att = attributes.Att.empty + def Location(startLine: Int, startColumn: Int, endLine: Int, endColumn: Int) = attributes.Location(startLine, startColumn, endLine, endColumn) - def KApply(klabel: KLabel, klist: KList): KApply = KApply(klabel, klist, Att.empty) + def KApply(klabel: KLabel, klist: KList): KApply = KApply(klabel, klist, Att) - def KApply(klabel: KLabel, ks: Seq[K], att: Att = Att.empty): KApply = - KApply(klabel, KList(ks.asJava), att) + def KToken(string: String, sort: Sort): KToken = KToken(string, sort, Att) - def KToken(string: String, sort: Sort): KToken = KToken(string, sort, Att.empty) + def KSequence(ks: java.util.List[K]): KSequence = KSequence(ks, Att) - def KSequence(ks: java.util.List[K]): KSequence = KSequence(ks, Att.empty) + def KRewrite(left: K, right: K): KRewrite = KRewrite(left, right, Att) - def KRewrite(left: K, right: K): KRewrite = KRewrite(left, right, Att.empty) + def KAs(pattern: K, alias: K): KAs = KAs(pattern, alias, Att) - def KAs(pattern: K, alias: K): KAs = KAs(pattern, alias, Att.empty) - - def InjectedKLabel(label: KLabel): InjectedKLabel = InjectedKLabel(label, Att.empty) + def InjectedKLabel(label: KLabel): InjectedKLabel = InjectedKLabel(label, Att) // def toKList: Collector[K, KList] = // Collector(() => new CombinerFromBuilder(KList.newBuilder())) @@ -76,24 +76,4 @@ object KORE extends Constructors { ADT.InjectedKLabel(klabel, att) def self = this - - object Sugar { - def ~>(l: K, r: K): KSequence = KSequence(Seq(l, r).asJava, Att.empty) - - def +(l: K, r: K): KApply = KApply(KLabel("+"), l, r) - - def -(l: K, r: K): KApply = KApply(KLabel("-"), l, r) - - def *(l: K, r: K): KApply = KApply(KLabel("*"), l, r) - - def /(l: K, r: K): KApply = KApply(KLabel("/"), l, r) - - def &(l: K, r: K): KApply = KApply(KLabel("&"), l, r) - - def ~(l: K, r: K): KApply = KApply(KLabel("~"), l, r) - - def &&(l: K, r: K): KApply = KApply(KLabels.AND, l, r) - - def ||(l: K, r: K): KApply = KApply(KLabels.OR, l, r) - } } diff --git a/kore/src/main/scala/org/kframework/kore/ScalaSugar.scala b/kore/src/main/scala/org/kframework/kore/ScalaSugar.scala new file mode 100644 index 00000000000..b3de1c421c7 --- /dev/null +++ b/kore/src/main/scala/org/kframework/kore/ScalaSugar.scala @@ -0,0 +1,38 @@ +// Copyright (c) Runtime Verification, Inc. All Rights Reserved. +package org.kframework.kore + +import org.kframework.attributes.Att +import org.kframework.builtin.KLabels +import org.kframework.builtin.Sorts +import scala.collection.JavaConverters._ + +trait ScalaSugared { + val c: Constructors + + import c._ + + implicit def stringToToken(s: String) = KToken(s, Sorts.String, Att.empty) + def stringToId(s: String): K = KToken(s, Sorts.Id, Att.empty) + implicit def symbolToLabel(l: Symbol) = KLabel(l.name) + implicit def intToToken(n: Int): K = KToken(n.toString, Sorts.Int, Att.empty) + + implicit class ApplicableKLabel(klabel: KLabel) { + def apply(l: K*): K = c.KApply(klabel, l) + } + + implicit class EnhancedK(k: K) { + def ~>(other: K) = KSequence(Seq(k, other).asJava, Att.empty) + def ==>(other: K) = KRewrite(k, other, Att.empty) + def +(other: K) = KLabel("+")(k, other) + def -(other: K) = KLabel("-")(k, other) + def *(other: K) = KLabel("*")(k, other) + def /(other: K) = KLabel("/")(k, other) + def &(other: K) = KLabel("&")(k, other) + def ~(other: K) = KLabel("~")(k, other) + def &&(other: K) = KLabels.AND.apply(k, other) + def ||(other: K) = KLabels.OR.apply(k, other) + } + + def KApply(klabel: KLabel, ks: Seq[K], att: Att = Att.empty): KApply = + c.KApply(klabel, c.KList(ks.asJava), att) +} diff --git a/kore/src/main/scala/org/kframework/parser/TreeNodesToKORE.scala b/kore/src/main/scala/org/kframework/parser/TreeNodesToKORE.scala index a41c5804bca..72ea930af95 100644 --- a/kore/src/main/scala/org/kframework/parser/TreeNodesToKORE.scala +++ b/kore/src/main/scala/org/kframework/parser/TreeNodesToKORE.scala @@ -42,7 +42,7 @@ class TreeNodesToKORE(parseSort: java.util.function.Function[String, Sort]) { ) case t @ TermCons(_, _) => termConsToKApply(t) case Ambiguity(items) => - KApply(KLabel("amb"), KList(items.asScala.toList.map(apply).asJava), Att.empty) + KApply(KLabel("amb"), KList(items.asScala.toList.map(apply) asJava), Att.empty) } def termConsToKApply(t: TermCons): K = { @@ -60,7 +60,7 @@ class TreeNodesToKORE(parseSort: java.util.function.Function[String, Sort]) { else t.production.klabel.get KApply( klabel.head, - KList(new util.ArrayList(t.items).asScala.reverse.map(apply).asJava), + KList(new util.ArrayList(t.items).asScala.reverse.map(apply) asJava), locationToAtt(t.location, t.source).add(Att.PRODUCTION, classOf[Production], realProd) ) } diff --git a/kore/src/main/scala/org/kframework/unparser/KOREToTreeNodes.scala b/kore/src/main/scala/org/kframework/unparser/KOREToTreeNodes.scala index 82dbc1ff1ce..c6e2a13a359 100644 --- a/kore/src/main/scala/org/kframework/unparser/KOREToTreeNodes.scala +++ b/kore/src/main/scala/org/kframework/unparser/KOREToTreeNodes.scala @@ -15,7 +15,7 @@ import scala.collection.JavaConverters._ object KOREToTreeNodes { - import org.kframework.kore.KORE._ + import org.kframework.kore.KORE.{ Att => _, _ } def wellTyped( args: Seq[Sort], @@ -45,7 +45,7 @@ object KOREToTreeNodes { ) case a: KApply => val scalaChildren = a.klist.items.asScala.map { i: K => apply(i, mod).asInstanceOf[Term] } - val children = ConsPStack.from(scalaChildren.reverse.asJava) + val children = ConsPStack.from(scalaChildren.reverse asJava) val loc = t.att.getOptional(Att.LOCATION, classOf[Location]) val source = t.att.getOptional(Att.SOURCE, classOf[Source]) val p = diff --git a/kore/src/test/scala/org/kframework/unparser/UnparseTest.scala b/kore/src/test/scala/org/kframework/unparser/UnparseTest.scala index 5685ea72989..70046d843be 100644 --- a/kore/src/test/scala/org/kframework/unparser/UnparseTest.scala +++ b/kore/src/test/scala/org/kframework/unparser/UnparseTest.scala @@ -4,7 +4,6 @@ package org.kframework.unparser import org.junit.Assert import org.junit.Test import org.kframework.attributes.Att -import org.kframework.builtin.Sorts import org.kframework.kore.ADT import org.kframework.kore.KORE._ @@ -18,18 +17,15 @@ class UnparseTest { } @Test def WrappedKLabel() { - Assert.assertEquals("#klabel(foo)", ToKast(InjectedKLabel(KLabel("foo"), Att.empty))) + Assert.assertEquals("#klabel(foo)", ToKast(InjectedKLabel('foo, Att.empty))) } @Test def EmptyApp() { - Assert.assertEquals("foo(.KList)", ToKast(KApply(KLabel("foo")))) + Assert.assertEquals("foo(.KList)", ToKast('foo())) } @Test def NestedApp() { - Assert.assertEquals( - "foo(a(.KList),b(.KList))", - ToKast(KApply(KLabel("foo"), KApply(KLabel("a")), KApply(KLabel("b")))) - ) + Assert.assertEquals("foo(a(.KList),b(.KList))", ToKast('foo('a(), 'b()))) } @Test def SequenceEmpty() { @@ -37,23 +33,17 @@ class UnparseTest { } @Test def Sequence() { - Assert.assertEquals( - "a(.KList)~>b(.KList)~>c(.KList)", - ToKast(Sugar.~>(KApply(KLabel("a")), Sugar.~>(KApply(KLabel("b")), KApply(KLabel("c"))))) - ) + Assert.assertEquals("a(.KList)~>b(.KList)~>c(.KList)", ToKast('a() ~> 'b() ~> 'c())) } @Test def Rewrite() { - Assert.assertEquals( - "a(.KList)=>b(.KList)", - ToKast(KRewrite(KApply(KLabel("a")), KApply(KLabel("b")))) - ) + Assert.assertEquals("a(.KList)=>b(.KList)", ToKast(KRewrite('a(), 'b()))) } @Test def Tokens() { Assert.assertEquals( """#token("9","Int")~>#token("Test","String")""", - ToKast(Sugar.~>(KToken("9", Sorts.Int, Att.empty), KToken("Test", Sorts.String, Att.empty))) + ToKast(intToToken(9) ~> "Test") ) } @@ -62,23 +52,17 @@ class UnparseTest { } @Test def Precedence1() { - Assert.assertEquals( - "``a(.KList)=>b(.KList)``~>c(.KList)", - ToKast(Sugar.~>(KRewrite(KApply(KLabel("a")), KApply(KLabel("b"))), KApply(KLabel("c")))) - ) + Assert.assertEquals("``a(.KList)=>b(.KList)``~>c(.KList)", ToKast(KRewrite('a(), 'b()) ~> 'c())) } @Test def Precedence2() { - Assert.assertEquals( - "a(.KList)=>b(.KList)~>c(.KList)", - ToKast(KRewrite(KApply(KLabel("a")), Sugar.~>(KApply(KLabel("b")), KApply(KLabel("c"))))) - ) + Assert.assertEquals("a(.KList)=>b(.KList)~>c(.KList)", ToKast(KRewrite('a(), 'b() ~> 'c()))) } @Test def TickSpace() { Assert.assertEquals( "`` `_+_`(.KList)=>b(.KList)``~>c(.KList)", - ToKast(Sugar.~>(KRewrite(KApply(KLabel("_+_")), KApply(KLabel("b"))), KApply(KLabel("c")))) + ToKast(KRewrite(KLabel("_+_")(), 'b()) ~> 'c()) ) } @@ -87,10 +71,10 @@ class UnparseTest { "#a(.KList)~>`#klabel`(.KList)~>#klabel(test)~>`#token`(.KList)~>#token(\"1\",\"Int\")", ToKast( KSequence( - KApply(KLabel("#a")), - KApply(KLabel("#klabel")), + KLabel("#a")(), + KLabel("#klabel")(), InjectedKLabel(KLabel("test"), Att.empty), - KApply(KLabel("#token")), + KLabel("#token")(), KToken("1", Sort("Int")) ) ) diff --git a/nix/build-maven-package.nix b/nix/build-maven-package.nix index 8ff94f03361..c0e9d4d4882 100644 --- a/nix/build-maven-package.nix +++ b/nix/build-maven-package.nix @@ -2,8 +2,7 @@ { src, sourceRoot ? null, buildOffline ? false, patches ? [ ], pname, version , mvnHash ? "", mvnFetchExtraArgs ? { }, mvnDepsParameters ? "" -, manualMvnArtifacts ? [ ], manualMvnSourceArtifacts ? [ ] -, mvnParameters ? "", ... }@args: +, manualMvnArtifacts ? [ ], mvnParameters ? "", ... }@args: # originally extracted from dbeaver # created to allow using maven packages in the same style as rust @@ -25,14 +24,6 @@ let echo "downloading manual $artifactId" mvn dependency:get -Dartifact="$artifactId" -Dmaven.repo.local=$out/.m2 done - - for artifactId in ${builtins.toString manualMvnSourceArtifacts} - do - group=$(echo $artifactId | cut -d':' -f1) - artifact=$(echo $artifactId | cut -d':' -f2) - echo "downloading manual sources $artifactId" - mvn dependency:sources -DincludeGroupIds=$group -DincludeArtifactIds=$artifact -Dmaven.repo.local=$out/.m2 - done '' + lib.optionalString (!buildOffline) '' mvn package -Dmaven.repo.local=$out/.m2 ${mvnParameters} '' + '' diff --git a/nix/k.nix b/nix/k.nix index 71df78ab634..c0e9401d9ea 100644 --- a/nix/k.nix +++ b/nix/k.nix @@ -1,4 +1,4 @@ -{ src, maven, mvnHash, manualMvnArtifacts, manualMvnSourceArtifacts, clang, stdenv, lib, runCommand +{ src, maven, mvnHash, manualMvnArtifacts, clang, stdenv, lib, runCommand , makeWrapper, bison, flex, gcc, git, gmp, jdk, jre, jre_minimal, mpfr, ncurses , pkg-config, python3, z3, haskell-backend, booster, rpc-client, prelude-kore, llvm-backend , debugger, version, llvm-kompile-libs, runtimeShell }: @@ -36,12 +36,12 @@ let k = current-llvm-kompile-libs: maven.buildMavenPackage rec { pname = "k"; - inherit version src mvnHash manualMvnArtifacts manualMvnSourceArtifacts; + inherit version src mvnHash manualMvnArtifacts; buildOffline = true; mvnParameters = - "-DskipTests -DskipKTest=true -Dllvm.backend.skip=true -Dhaskell.backend.skip=true -Dbooster.skip=true -DsecondaryCacheDir=secondary-cache"; + "-DskipTests -DskipKTest=true -Dllvm.backend.skip=true -Dhaskell.backend.skip=true -Dbooster.skip=true"; nativeBuildInputs = [ makeWrapper ]; diff --git a/pom.xml b/pom.xml index 1df0d141f00..305b92b4eb1 100644 --- a/pom.xml +++ b/pom.xml @@ -124,11 +124,6 @@ scalafmt-core_${scala.majorVersion} ${scalafmt.version} - - org.scala-sbt - compiler-bridge_2.12 - 1.8.0 - @@ -157,7 +152,7 @@ maven-dependency-plugin - 3.6.1 + 3.1.1 maven-surefire-plugin @@ -171,9 +166,10 @@ maven-compiler-plugin - 3.12.1 + 3.7.0 - ${java.version} + ${java.version} + ${java.version}