From f7c33c09c42b48dd2331a132dabdc10fc33ca7da Mon Sep 17 00:00:00 2001 From: Scott Guest Date: Tue, 13 Feb 2024 08:43:41 -0800 Subject: [PATCH] Remove special-casing for `group(_)` (#3981) When we originally added `group(_)` to replace unstructured attributes, we treated it as syntactic sugar where `[group(foo1,...,fooN)]` expands internally into `[foo1,...,fooN]`. However, on a second look, this expansion is unnecessary - `group(_)` is only relevant in the `Context` object used by `KILtoKORE` which maps tags in syntax blocks to sets of corresponding `Production`s. In this PR, we then - Remove all the `ProcessGroupAttributes` logic and instead just parse `group(_)` when we build the `Context`. - Remove the special-cased `KeyType.UserGroup` - (Opinionated) Remove the mention of `group(_)` from the "unrecognized attributes" error message. - The hint was useful when we first disallowed unstructured attributes. However, now that `group(_)` and the whitelist are more established, it feels a bit odd to assume any unrecognized attribute is an attempt to create a group. As a side effect of this change, - `syntax` declarations can now only refer to productions by their klabel or group. Previously, any attribute was permitted, and the priority or associativity would apply to everything with that attribute. - Cell properties will no longer expand ` ` - This should be disallowed entirely, but see #3982 - We no longer error if a group conflicts with a built-in attribute - Before, this error was required lest `[group(function)]` be treated the same as `[function]` --- .../include/kframework/builtin/kast.md | 24 +-- .../kframework/kore/convertors/BaseTest.java | 2 - .../tests/regression-new/checks/checkGroup.k | 4 +- .../regression-new/checks/checkGroup.k.out | 8 +- .../checks/checkModuleAtts.k.out | 10 +- .../pedanticAttributes/test.k.out | 2 - .../kframework/backend/kore/KoreBackend.java | 3 +- .../kframework/backend/kore/ModuleToKORE.java | 6 +- .../GenerateSentencesFromConfigDecl.java | 15 +- .../compile/ProcessGroupAttributes.java | 40 ---- .../compile/ResolveHeatCoolAttribute.java | 18 +- .../kframework/compile/checks/CheckAtt.java | 3 +- .../main/java/org/kframework/kil/Module.java | 6 +- .../java/org/kframework/kil/Production.java | 2 +- .../org/kframework/kil/loader/Context.java | 25 ++- .../kframework/kore/convertors/KILtoKORE.java | 5 +- .../org/kframework/parser/ParserUtils.java | 6 - .../kframework/parser/json/JsonParser.java | 15 +- .../java/org/kframework/unparser/ToJson.java | 3 - .../scala/org/kframework/attributes/Att.scala | 194 +++++++----------- 20 files changed, 128 insertions(+), 263 deletions(-) delete mode 100644 kernel/src/main/java/org/kframework/compile/ProcessGroupAttributes.java diff --git a/k-distribution/include/kframework/builtin/kast.md b/k-distribution/include/kframework/builtin/kast.md index 364e72249c4..2fe731742fd 100644 --- a/k-distribution/include/kframework/builtin/kast.md +++ b/k-distribution/include/kframework/builtin/kast.md @@ -142,26 +142,26 @@ module ML-SYNTAX [not-lr1] | "#Bottom" [klabel(#Bottom), symbol, group(mlUnary)] | "#True" [klabel(#Top), symbol, group(mlUnary), unparseAvoid] | "#False" [klabel(#Bottom), symbol, group(mlUnary), unparseAvoid] - | "#Not" "(" Sort ")" [klabel(#Not), symbol, mlOp, group(mlUnary)] + | "#Not" "(" Sort ")" [klabel(#Not), symbol, mlOp, group(mlUnary, mlOp)] - syntax {Sort1, Sort2} Sort2 ::= "#Ceil" "(" Sort1 ")" [klabel(#Ceil), symbol, mlOp, group(mlUnary)] - | "#Floor" "(" Sort1 ")" [klabel(#Floor), symbol, mlOp, group(mlUnary)] - | "{" Sort1 "#Equals" Sort1 "}" [klabel(#Equals), symbol, mlOp, group(mlEquals), comm, format(%1%i%n%2%d%n%3%i%n%4%d%n%5)] + syntax {Sort1, Sort2} Sort2 ::= "#Ceil" "(" Sort1 ")" [klabel(#Ceil), symbol, mlOp, group(mlUnary, mlOp)] + | "#Floor" "(" Sort1 ")" [klabel(#Floor), symbol, mlOp, group(mlUnary, mlOp)] + | "{" Sort1 "#Equals" Sort1 "}" [klabel(#Equals), symbol, mlOp, group(mlEquals, mlOp), comm, format(%1%i%n%2%d%n%3%i%n%4%d%n%5)] syntax priorities mlUnary > mlEquals > mlAnd - syntax {Sort} Sort ::= Sort "#And" Sort [klabel(#And), symbol, assoc, left, comm, unit(#Top), mlOp, group(mlAnd), format(%i%1%d%n%2%n%i%3%d)] - > Sort "#Or" Sort [klabel(#Or), symbol, assoc, left, comm, unit(#Bottom), mlOp, format(%i%1%d%n%2%n%i%3%d)] - > Sort "#Implies" Sort [klabel(#Implies), symbol, mlOp, group(mlImplies), format(%i%1%d%n%2%n%i%3%d)] + syntax {Sort} Sort ::= Sort "#And" Sort [klabel(#And), symbol, assoc, left, comm, unit(#Top), mlOp, group(mlAnd, mlOp), format(%i%1%d%n%2%n%i%3%d)] + > Sort "#Or" Sort [klabel(#Or), symbol, assoc, left, comm, unit(#Bottom), mlOp, group(mlOp), format(%i%1%d%n%2%n%i%3%d)] + > Sort "#Implies" Sort [klabel(#Implies), symbol, mlOp, group(mlImplies, mlOp), format(%i%1%d%n%2%n%i%3%d)] syntax priorities mlImplies > mlQuantifier - syntax {Sort1, Sort2} Sort2 ::= "#Exists" Sort1 "." Sort2 [klabel(#Exists), symbol, mlOp, mlBinder, group(mlQuantifier)] - | "#Forall" Sort1 "." Sort2 [klabel(#Forall), symbol, mlOp, mlBinder, group(mlQuantifier)] + syntax {Sort1, Sort2} Sort2 ::= "#Exists" Sort1 "." Sort2 [klabel(#Exists), symbol, mlOp, mlBinder, group(mlQuantifier, mlOp)] + | "#Forall" Sort1 "." Sort2 [klabel(#Forall), symbol, mlOp, mlBinder, group(mlQuantifier, mlOp)] - syntax {Sort} Sort ::= "#AG" "(" Sort ")" [klabel(#AG), symbol, mlOp] - | "#wEF" "(" Sort ")" [klabel(weakExistsFinally), symbol, mlOp] - | "#wAF" "(" Sort ")" [klabel(weakAlwaysFinally), symbol, mlOp] + syntax {Sort} Sort ::= "#AG" "(" Sort ")" [klabel(#AG), symbol, mlOp, group(mlOp)] + | "#wEF" "(" Sort ")" [klabel(weakExistsFinally), symbol, mlOp, group(mlOp)] + | "#wAF" "(" Sort ")" [klabel(weakAlwaysFinally), symbol, mlOp, group(mlOp)] endmodule ``` diff --git a/k-distribution/src/test/java/org/kframework/kore/convertors/BaseTest.java b/k-distribution/src/test/java/org/kframework/kore/convertors/BaseTest.java index 3f712149226..e948051c450 100644 --- a/k-distribution/src/test/java/org/kframework/kore/convertors/BaseTest.java +++ b/k-distribution/src/test/java/org/kframework/kore/convertors/BaseTest.java @@ -13,7 +13,6 @@ import org.junit.Rule; import org.junit.rules.TestName; import org.kframework.attributes.Source; -import org.kframework.compile.ProcessGroupAttributes; import org.kframework.kil.Definition; import org.kframework.kil.loader.Context; import org.kframework.parser.inner.CollectProductionsVisitor; @@ -100,7 +99,6 @@ protected DefinitionWithContext parseUsingOuter(File definitionFile) { def.setItems(Outer.parse(Source.apply(definitionFile.getPath()), definitionText, null)); def.setMainModule("TEST"); - ProcessGroupAttributes.apply(def); Context context = new Context(); return new DefinitionWithContext(def, context); } diff --git a/k-distribution/tests/regression-new/checks/checkGroup.k b/k-distribution/tests/regression-new/checks/checkGroup.k index 7738a18d8f3..82808630618 100644 --- a/k-distribution/tests/regression-new/checks/checkGroup.k +++ b/k-distribution/tests/regression-new/checks/checkGroup.k @@ -1,5 +1,5 @@ // Copyright (c) Runtime Verification, Inc. All Rights Reserved. -module TEST +module CHECKGROUP syntax Int ::= r"[\\+-]?[0-9]+" [prefer, token, prec(2)] - | Int "+" Int [group(function)] + | Int "+" Int [group(fun,)] endmodule diff --git a/k-distribution/tests/regression-new/checks/checkGroup.k.out b/k-distribution/tests/regression-new/checks/checkGroup.k.out index d23f3e64132..115acdee904 100644 --- a/k-distribution/tests/regression-new/checks/checkGroup.k.out +++ b/k-distribution/tests/regression-new/checks/checkGroup.k.out @@ -1,5 +1,5 @@ -[Error] Compiler: User-defined group 'function' conflicts with a built-in attribute. +[Error] Compiler: group(_) attribute expects a comma separated list of groups, each of which consists of a lower case letter followed by any number of alphanumeric or '-' characters. Source(checkGroup.k) - Location(4,18,4,47) - 4 | | Int "+" Int [group(function)] - . ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + Location(4,18,4,43) + 4 | | Int "+" Int [group(fun,)] + . ^~~~~~~~~~~~~~~~~~~~~~~~~ diff --git a/k-distribution/tests/regression-new/checks/checkModuleAtts.k.out b/k-distribution/tests/regression-new/checks/checkModuleAtts.k.out index 1463581f382..bd9b1eb32e1 100644 --- a/k-distribution/tests/regression-new/checks/checkModuleAtts.k.out +++ b/k-distribution/tests/regression-new/checks/checkModuleAtts.k.out @@ -1,9 +1,15 @@ +[Error] Compiler: Module cannot have the following attributes: [group] + Source(checkModuleAtts.k) + Location(2,1,3,10) + . v~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + 2 | module CHECKMODULEATTS [foo, group(bar), baz] + 3 | endmodule + . ~~~~~~~~^ [Error] Compiler: Unrecognized attributes: [baz, foo] -Hint: User-defined groups can be added with the group(_) attribute. Source(checkModuleAtts.k) Location(2,1,3,10) . v~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 2 | module CHECKMODULEATTS [foo, group(bar), baz] 3 | endmodule . ~~~~~~~~^ -[Error] Compiler: Had 1 structural errors. +[Error] Compiler: Had 2 structural errors. diff --git a/k-distribution/tests/regression-new/pedanticAttributes/test.k.out b/k-distribution/tests/regression-new/pedanticAttributes/test.k.out index 56725749b33..d9782745ca4 100644 --- a/k-distribution/tests/regression-new/pedanticAttributes/test.k.out +++ b/k-distribution/tests/regression-new/pedanticAttributes/test.k.out @@ -1,11 +1,9 @@ [Error] Compiler: Unrecognized attributes: [badAtt] -Hint: User-defined groups can be added with the group(_) attribute. Source(test.k) Location(3,18,3,71) 3 | syntax Int ::= r"[\\+-]?[0-9]+" [prefer, token, prec(2), badAtt(10)] . ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ [Error] Compiler: Unrecognized attributes: [badAtt] -Hint: User-defined groups can be added with the group(_) attribute. Source(test.k) Location(4,18,4,68) 4 | | Int "+" Int [group(badAttButOkay),badAtt,function] diff --git a/kernel/src/main/java/org/kframework/backend/kore/KoreBackend.java b/kernel/src/main/java/org/kframework/backend/kore/KoreBackend.java index 85c3bad93d9..7c613ff38c7 100644 --- a/kernel/src/main/java/org/kframework/backend/kore/KoreBackend.java +++ b/kernel/src/main/java/org/kframework/backend/kore/KoreBackend.java @@ -128,8 +128,7 @@ public Function steps() { .apply(d); DefinitionTransformer resolveHeatCoolAttribute = DefinitionTransformer.fromSentenceTransformer( - new ResolveHeatCoolAttribute(new HashSet<>())::resolve, - "resolving heat and cool attributes"); + ResolveHeatCoolAttribute::resolve, "resolving heat and cool attributes"); DefinitionTransformer resolveAnonVars = DefinitionTransformer.fromSentenceTransformer( new ResolveAnonVar()::resolve, "resolving \"_\" vars"); 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 dea3fe22171..42d182daaad 100644 --- a/kernel/src/main/java/org/kframework/backend/kore/ModuleToKORE.java +++ b/kernel/src/main/java/org/kframework/backend/kore/ModuleToKORE.java @@ -1863,8 +1863,7 @@ private KLabel computePolyKLabel(KApply k) { } private void collectAttributes(Map attributes, Att att) { - for (Tuple2, ?> attribute : - iterable(att.withUserGroupsAsGroupAtt().att())) { + for (Tuple2, ?> attribute : iterable(att.att())) { Att.Key name = attribute._1._1; Object val = attribute._2; String strVal = val.toString(); @@ -2024,9 +2023,6 @@ private void convert( sb.append("["); String conn = ""; - // Emit user groups as group(_) to prevent conflicts between user groups and internals - att = att.withUserGroupsAsGroupAtt(); - for (Tuple2, ?> attribute : // Sort to stabilize error messages stream(att.att()).sorted(Comparator.comparing(Tuple2::toString)).toList()) { diff --git a/kernel/src/main/java/org/kframework/compile/GenerateSentencesFromConfigDecl.java b/kernel/src/main/java/org/kframework/compile/GenerateSentencesFromConfigDecl.java index 6014fc5e07f..57ffe5b68fc 100644 --- a/kernel/src/main/java/org/kframework/compile/GenerateSentencesFromConfigDecl.java +++ b/kernel/src/main/java/org/kframework/compile/GenerateSentencesFromConfigDecl.java @@ -773,11 +773,9 @@ private static Att getCellPropertiesAsAtt(K k) { } else if (kapp.klabel().name().equals("#cellPropertyList")) { if (kapp.klist().size() == 2) { Tuple2 attribute = getCellProperty(kapp.klist().items().get(0)); - return ProcessGroupAttributes.getProcessedAtt( - Att() - .add(attribute._1(), attribute._2()) - .addAll(getCellPropertiesAsAtt(kapp.klist().items().get(1))), - k); + return Att() + .add(attribute._1(), attribute._2()) + .addAll(getCellPropertiesAsAtt(kapp.klist().items().get(1))); } } } @@ -795,12 +793,7 @@ private static Tuple2 getCellProperty(K k) { .orElseThrow( () -> KEMException.compilerError( - "Unrecognized attribute: " - + keyToken.s() - + "\n" - + "Hint: User-defined groups can be added with the" - + " group=\"...\" attribute.", - k)); + "Unrecognized property: " + keyToken.s(), k)); if (kapp.klist().items().get(0) instanceof KToken) { KToken valueToken = (KToken) kapp.klist().items().get(1); if (valueToken.sort().equals(Sorts.KString())) { diff --git a/kernel/src/main/java/org/kframework/compile/ProcessGroupAttributes.java b/kernel/src/main/java/org/kframework/compile/ProcessGroupAttributes.java deleted file mode 100644 index c5c6e45e4c4..00000000000 --- a/kernel/src/main/java/org/kframework/compile/ProcessGroupAttributes.java +++ /dev/null @@ -1,40 +0,0 @@ -// Copyright (c) Runtime Verification, Inc. All Rights Reserved. -package org.kframework.compile; - -import org.kframework.attributes.Att; -import org.kframework.attributes.HasLocation; -import org.kframework.kil.Definition; -import org.kframework.kil.Module; -import org.kframework.kil.Syntax; -import org.kframework.utils.errorsystem.KEMException; -import scala.util.Either; - -/** - * A pass which handles all "user group" attributes. Specifically, the attribute - * [group(att1,...,attN)] is replaced with the underlying attributes [att1,...,attN]. - */ -public class ProcessGroupAttributes { - public static Att getProcessedAtt(Att att, HasLocation node) { - Either newAttOrError = att.withGroupAttAsUserGroups(); - if (newAttOrError.isLeft()) { - throw KEMException.compilerError(newAttOrError.left().get(), node); - } - Att newAtt = newAttOrError.right().get(); - return newAtt; - } - - public static void apply(Module m) { - m.setAttributes(getProcessedAtt(m.getAttributes(), m)); - m.getItems().stream() - .filter((modItem) -> modItem instanceof Syntax) - .flatMap((s) -> ((Syntax) s).getPriorityBlocks().stream()) - .flatMap((pb) -> pb.getProductions().stream()) - .forEach((p) -> p.setAttributes(getProcessedAtt(p.getAttributes(), p))); - } - - public static void apply(Definition d) { - d.getItems().stream() - .filter((item) -> item instanceof Module) - .forEach((m) -> apply((Module) m)); - } -} diff --git a/kernel/src/main/java/org/kframework/compile/ResolveHeatCoolAttribute.java b/kernel/src/main/java/org/kframework/compile/ResolveHeatCoolAttribute.java index 8cde989b443..561caae4d4f 100644 --- a/kernel/src/main/java/org/kframework/compile/ResolveHeatCoolAttribute.java +++ b/kernel/src/main/java/org/kframework/compile/ResolveHeatCoolAttribute.java @@ -5,8 +5,6 @@ import static org.kframework.definition.Constructors.*; import static org.kframework.kore.KORE.*; -import java.util.Optional; -import java.util.Set; import org.kframework.attributes.Att; import org.kframework.builtin.BooleanUtils; import org.kframework.definition.Context; @@ -18,18 +16,18 @@ import org.kframework.kore.KLabel; import org.kframework.utils.errorsystem.KEMException; -public record ResolveHeatCoolAttribute(Set unrestrictedRules) { +public class ResolveHeatCoolAttribute { - private Rule resolve(Module m, Rule rule) { + private static Rule resolve(Module m, Rule rule) { return Rule(rule.body(), transform(m, rule.requires(), rule.att()), rule.ensures(), rule.att()); } - private Context resolve(Module m, Context context) { + private static Context resolve(Module m, Context context) { return new Context( context.body(), transform(m, context.requires(), context.att()), context.att()); } - private K transform(Module m, K requires, Att att) { + private static K transform(Module m, K requires, Att att) { String sort = att.getOptional(Att.RESULT()).orElse("KResult"); KLabel lbl = KLabel("is" + sort); if (!m.productionsFor().contains(lbl) @@ -49,19 +47,13 @@ && stream(m.allSorts()).noneMatch(s -> s.toString().equals(sort))) { return BooleanUtils.and(requires, BooleanUtils.not(predicate)); } if (att.contains(Att.COOL())) { - if (unrestrictedRules.stream() - .map(Att::getUserGroupOptional) - .flatMap(Optional::stream) - .anyMatch(att::contains)) { - return requires; - } return BooleanUtils.and(requires, predicate); } throw new AssertionError( "Called ResolveHeatCoolAttribute::transform on rule without " + "heat or cool attribute"); } - public Sentence resolve(Module m, Sentence s) { + public static Sentence resolve(Module m, Sentence s) { if (!s.att().contains(Att.HEAT()) && !s.att().contains(Att.COOL())) { return s; } diff --git a/kernel/src/main/java/org/kframework/compile/checks/CheckAtt.java b/kernel/src/main/java/org/kframework/compile/checks/CheckAtt.java index 075b1ea338d..f6e9e9b703a 100644 --- a/kernel/src/main/java/org/kframework/compile/checks/CheckAtt.java +++ b/kernel/src/main/java/org/kframework/compile/checks/CheckAtt.java @@ -78,8 +78,7 @@ private void checkUnrecognizedAtts(T term) { errors.add( KEMException.compilerError( "Unrecognized attributes: " - + stream(term.att().unrecognizedKeys()).map(Key::toString).sorted().toList() - + "\nHint: User-defined groups can be added with the group(_) attribute.", + + stream(term.att().unrecognizedKeys()).map(Key::toString).sorted().toList(), term)); } } diff --git a/kernel/src/main/java/org/kframework/kil/Module.java b/kernel/src/main/java/org/kframework/kil/Module.java index f12b3050931..3bb8efcc9b1 100644 --- a/kernel/src/main/java/org/kframework/kil/Module.java +++ b/kernel/src/main/java/org/kframework/kil/Module.java @@ -43,11 +43,7 @@ public List getItems() { @Override public void toString(StringBuilder sb) { - sb.append("module ") - .append(name) - .append(" ") - .append(getAttributes().withUserGroupsAsGroupAtt()) - .append("\n"); + sb.append("module ").append(name).append(" ").append(getAttributes()).append("\n"); for (ModuleItem i : items) { i.toString(sb); sb.append("\n"); diff --git a/kernel/src/main/java/org/kframework/kil/Production.java b/kernel/src/main/java/org/kframework/kil/Production.java index 6f90e86e0d9..199bd027a46 100644 --- a/kernel/src/main/java/org/kframework/kil/Production.java +++ b/kernel/src/main/java/org/kframework/kil/Production.java @@ -253,7 +253,7 @@ public void toString(StringBuilder sb) { i.toString(sb); sb.append(" "); } - sb.append(getAttributes().withUserGroupsAsGroupAtt()); + sb.append(getAttributes()); } public void setOwnerModuleName(String ownerModuleName) { diff --git a/kernel/src/main/java/org/kframework/kil/loader/Context.java b/kernel/src/main/java/org/kframework/kil/loader/Context.java index 9525ceb2935..da28ecabadb 100644 --- a/kernel/src/main/java/org/kframework/kil/loader/Context.java +++ b/kernel/src/main/java/org/kframework/kil/loader/Context.java @@ -1,8 +1,6 @@ // Copyright (c) Runtime Verification, Inc. All Rights Reserved. package org.kframework.kil.loader; -import static org.kframework.Collections.*; - import com.google.common.collect.HashMultimap; import com.google.common.collect.SetMultimap; import com.google.inject.Inject; @@ -11,8 +9,8 @@ import org.kframework.kil.Production; import org.kframework.kompile.KompileOptions; import org.kframework.main.GlobalOptions; +import org.kframework.utils.errorsystem.KEMException; import org.kframework.utils.inject.RequestScoped; -import scala.Tuple2; @RequestScoped public class Context implements Serializable { @@ -21,7 +19,7 @@ public class Context implements Serializable { public Context() {} /** - * Represents a map from all Klabels or attributes in string representation to sets of + * Represents a map from all Klabels and group(_) tags in string representation to sets of * corresponding productions. */ public SetMultimap tags = HashMultimap.create(); @@ -31,18 +29,23 @@ public Context() {} public KompileOptions kompileOptions; public void addProduction(Production p) { - if (p.containsAttribute(Att.GROUP())) { - throw new AssertionError( - "Must call ExpandGroupAttribute.apply(Definition) before creating a Context."); - } - if (p.getKLabel(false) != null) { tags.put(p.getKLabel(false), p); } else if (p.getAttributes().contains(Att.BRACKET())) { tags.put(p.getBracketLabel(false), p); } - for (Tuple2 a : iterable(p.getAttributes().att().keys())) { - tags.put(a._1.key(), p); + if (p.getAttributes().contains(Att.GROUP())) { + String groups = p.getAttributes().get(Att.GROUP()); + if (!groups.matches("\\s*[a-z][a-zA-Z0-9-]*\\s*(,\\s*[a-z][a-zA-Z0-9-]*\\s*)*")) { + throw KEMException.compilerError( + "group(_) attribute expects a comma separated list of " + + "groups, each of which consists of a lower case letter followed by any " + + "number of alphanumeric or '-' characters.", + p); + } + for (String group : groups.split("\\s*,\\s*")) { + tags.put(group, p); + } } } } 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 2ab89025ace..c7947c5db6a 100644 --- a/kernel/src/main/java/org/kframework/kore/convertors/KILtoKORE.java +++ b/kernel/src/main/java/org/kframework/kore/convertors/KILtoKORE.java @@ -14,7 +14,6 @@ import org.kframework.attributes.Att; import org.kframework.attributes.Location; import org.kframework.attributes.Source; -import org.kframework.compile.ProcessGroupAttributes; import org.kframework.compile.checks.CheckBracket; import org.kframework.compile.checks.CheckListDecl; import org.kframework.definition.Associativity; @@ -384,9 +383,7 @@ public void applyUserList( } public static org.kframework.attributes.Att convertAttributes(ASTNode t) { - Att attributes = ProcessGroupAttributes.getProcessedAtt(t.getAttributes(), t); - - return attributes + return t.getAttributes() .addAll(attributesFromLocation(t.getLocation())) .addAll(attributesFromSource(t.getSource())); } diff --git a/kernel/src/main/java/org/kframework/parser/ParserUtils.java b/kernel/src/main/java/org/kframework/parser/ParserUtils.java index 9b2e0a8dd5e..58c230c74de 100644 --- a/kernel/src/main/java/org/kframework/parser/ParserUtils.java +++ b/kernel/src/main/java/org/kframework/parser/ParserUtils.java @@ -22,7 +22,6 @@ import org.kframework.attributes.Att; import org.kframework.attributes.Location; import org.kframework.attributes.Source; -import org.kframework.compile.ProcessGroupAttributes; import org.kframework.definition.FlatModule; import org.kframework.definition.Module; import org.kframework.definition.ModuleTransformer; @@ -82,7 +81,6 @@ public static Module parseMainModuleOuterSyntax( def.setItems(Outer.parse(source, definitionText, null)); def.setMainModule(mainModule); - ProcessGroupAttributes.apply(def); Context context = new Context(); new CollectProductionsVisitor(context).visit(def); @@ -117,9 +115,6 @@ public List slurp( } } List items = Outer.parse(source, definitionText, null); - items.stream() - .filter((d) -> d instanceof org.kframework.kil.Module) - .forEach((m) -> ProcessGroupAttributes.apply((org.kframework.kil.Module) m)); if (options.verbose) { System.out.println("Importing: " + source); @@ -227,7 +222,6 @@ public Set loadModules( Definition def = new Definition(); def.setItems((List) (Object) kilModules); - ProcessGroupAttributes.apply(def); new CollectProductionsVisitor(context).visit(def); // Tuple4 of moduleName, Source, Location, digest diff --git a/kernel/src/main/java/org/kframework/parser/json/JsonParser.java b/kernel/src/main/java/org/kframework/parser/json/JsonParser.java index ede6d80c190..c507a3029ce 100644 --- a/kernel/src/main/java/org/kframework/parser/json/JsonParser.java +++ b/kernel/src/main/java/org/kframework/parser/json/JsonParser.java @@ -47,7 +47,6 @@ import org.kframework.utils.errorsystem.KEMException; import scala.Option; import scala.collection.JavaConverters; -import scala.util.Either; /** Parses a Json term into the KORE data structures. */ public class JsonParser { @@ -357,21 +356,11 @@ public static Att toAtt(JsonObject data) { "Unrecognized attribute " + key + " found in KAST Json term when unparsing KATT: " - + attMap - + "\n" - + "Hint: User-defined groups can be added with the group(_)" - + " attribute.")); + + attMap)); newAtt = newAtt.add(attKey, attMap.getString(key)); } } - Either newAttOrError = newAtt.withGroupAttAsUserGroups(); - if (newAttOrError.isLeft()) { - throw KEMException.criticalError( - newAttOrError.left().get() - + "\nOccurred in KAST Json term when unparsing KATT: " - + attMap); - } - return newAttOrError.right().get(); + return newAtt; } //////////////////// diff --git a/kernel/src/main/java/org/kframework/unparser/ToJson.java b/kernel/src/main/java/org/kframework/unparser/ToJson.java index 19f1ab5d9c2..b90d24a9c3b 100644 --- a/kernel/src/main/java/org/kframework/unparser/ToJson.java +++ b/kernel/src/main/java/org/kframework/unparser/ToJson.java @@ -128,9 +128,6 @@ public static JsonStructure toJson(Definition def) { } public static JsonStructure toJson(Att att) { - // Emit user groups as group(_) to prevent conflicts between user groups and internals - att = att.withUserGroupsAsGroupAtt(); - JsonObjectBuilder jatt = factory.createObjectBuilder(); jatt.add("node", JsonParser.KATT); diff --git a/kore/src/main/scala/org/kframework/attributes/Att.scala b/kore/src/main/scala/org/kframework/attributes/Att.scala index 4321e7ac2e6..68337b075b1 100644 --- a/kore/src/main/scala/org/kframework/attributes/Att.scala +++ b/kore/src/main/scala/org/kframework/attributes/Att.scala @@ -36,8 +36,6 @@ trait AttValue * - Att.getBuiltInKeyOptional(myAttStr), if checking a user-supplied attribute string. Be sure to * report an error if the lookup fails * - Att.getInternalKeyOptional(myAttStr), if expecting an internal key - * - Att.getUserGroupOptional(myAttStr), if expecting a user-group, enforcing that it is not a - * built-in * * During parsing, you may also use Att.unrecognizedKey(myAttStr) to delay error reporting on an * unrecognized attribute @@ -52,42 +50,6 @@ class Att private (val att: Map[(Att.Key, String), Any]) case _ => false } - // Remove all UserGroups and replace them with a group(_) attribute - def withUserGroupsAsGroupAtt: Att = { - val groups = att.keys.filter(_._1.keyType.equals(Att.KeyType.UserGroup)).toSet; - if (groups.isEmpty) - this - else - Att(att -- groups).add(Att.GROUP, groups.map(_._1.key).mkString(",")) - } - - // Remove the group(_) attribute and insert each of its arguments as a UserGroup - // Returns either Left of an error message or Right of the result - def withGroupAttAsUserGroups: Either[String, Att] = { - if (!contains(Att.GROUP, classOf[String])) - return Right(this) - val groups = get(Att.GROUP).trim - if (groups.isEmpty) - return Left("group(_) attribute expects a comma-separated list of arguments.") - val badComma = Left("Extraneous ',' in group(_) attribute.") - if (groups.startsWith(",") || groups.endsWith(",")) - return badComma - var att = this - for (group <- groups.split("\\s*,\\s*")) { - if (group.isEmpty) - return badComma - val groupKey = Att.getUserGroupOptional(group) - if (groupKey.isEmpty) - return Left("User-defined group '" + group + "' conflicts with a built-in attribute.") - if (!group.matches("[a-z][a-zA-Z0-9-]*")) - return Left( - "Invalid argument '" + group + "' in group(_) attribute. " + - "Expected a lower case letter followed by any number of alphanumeric or '-' characters." - ) - att = att.add(groupKey.get) - } - Right(att.remove(Att.GROUP)) - } val unrecognizedKeys: Set[Att.Key] = att.map(_._1._1).filter(_.keyType.equals(Att.KeyType.Unrecognized)).toSet @@ -168,30 +130,23 @@ object Att { sealed trait KeyType private object KeyType extends Serializable { // Attributes which are built-in and can appear in user source code - case object BuiltIn extends KeyType; + case object BuiltIn extends KeyType // Attributes which are compiler-internal and cannot appear in user source code - case object Internal extends KeyType; - // Attributes which represent user-defined groups via group(_). - // - // WARNING: Although we treat the arguments to group(_) as individual attributes internally, - // for any external interface (emitting KORE, JSON, etc.), we must re-emit them under the - // group(_) attribute, - // else there will be conflicts when a user group has the same name as an internal attribute. - case object UserGroup extends KeyType; + case object Internal extends KeyType // Attributes from user source code which are not recognized as built-ins // This is only used to delay error reporting until after parsing, allowing us to report // multiple errors - case object Unrecognized extends KeyType; + case object Unrecognized extends KeyType } sealed trait KeyParameter private object KeyParameter extends Serializable { // Attributes that must have parameters passed in (ie. [prec(25)] - case object Required extends KeyParameter; + case object Required extends KeyParameter // Attributes which may or may not have a parameter - case object Optional extends KeyParameter; + case object Optional extends KeyParameter // Attributes which may not have a parameter (ie. [function]) - case object Forbidden extends KeyParameter; + case object Forbidden extends KeyParameter } /* The Key class can only be constructed within Att. To enforce this, we must @@ -209,35 +164,34 @@ object Att { private[Key] def copy(): Unit = () } object Key { - private[Att] def apply(key: String, keyType: KeyType): Key = - Key(key, keyType, KeyParameter.Optional) - private[Att] def apply(key: String, keyType: KeyType, keyParam: KeyParameter): Key = - Key(key, keyType, keyParam, onlyon[AnyRef]) - private[Att] def apply( - key: String, - keyType: KeyType, - keyParam: KeyParameter, - allowedSentences: Set[Class[_]] - ): Key = new Key(key, keyType, keyParam, allowedSentences) private[Att] def builtin( key: String, keyParam: KeyParameter, allowedSentences: Set[Class[_]] ): Key = Key(key, KeyType.BuiltIn, keyParam, allowedSentences) + private[Att] def internal( + key: String + ): Key = + Key(key, KeyType.Internal, KeyParameter.Optional, onlyon[AnyRef]) } def unrecognizedKey(key: String): Att.Key = - Att.Key(key, KeyType.Unrecognized) + new Att.Key( + key, + KeyType.Unrecognized, + KeyParameter.Optional, + onlyon[AnyRef] + ) val empty: Att = Att(Map.empty) // Some helpers with scala reflection to make declaring class object sets more compact // If these break for some reason, replace their usage with Set(classOf[T1], classOf[T2], ...) - private def onlyon[T: ClassTag](): Set[Class[_]] = Set(classTag[T].runtimeClass) - private def onlyon2[T1: ClassTag, T2: ClassTag](): Set[Class[_]] = onlyon[T1] ++ onlyon[T2] - private def onlyon3[T1: ClassTag, T2: ClassTag, T3: ClassTag](): Set[Class[_]] = + private def onlyon[T: ClassTag]: Set[Class[_]] = Set(classTag[T].runtimeClass) + private def onlyon2[T1: ClassTag, T2: ClassTag]: Set[Class[_]] = onlyon[T1] ++ onlyon[T2] + private def onlyon3[T1: ClassTag, T2: ClassTag, T3: ClassTag]: Set[Class[_]] = onlyon2[T1, T2] ++ onlyon[T3] - private def onlyon4[T1: ClassTag, T2: ClassTag, T3: ClassTag, T4: ClassTag](): Set[Class[_]] = + private def onlyon4[T1: ClassTag, T2: ClassTag, T3: ClassTag, T4: ClassTag]: Set[Class[_]] = onlyon3[T1, T2, T3] ++ onlyon[T4] /* Built-in attribute keys which can appear in user source code */ @@ -344,54 +298,54 @@ object Att { final val WRAP_ELEMENT = Key.builtin("wrapElement", KeyParameter.Required, onlyon[Production]) /* Internal attribute keys which cannot appear in user source code */ - final val ANONYMOUS = Key("anonymous", KeyType.Internal) - final val BRACKET_LABEL = Key("bracketLabel", KeyType.Internal) - final val CELL_FRAGMENT = Key("cellFragment", KeyType.Internal) - final val CELL_OPT_ABSENT = Key("cellOptAbsent", KeyType.Internal) - final val CELL_SORT = Key("cellSort", KeyType.Internal) - final val CONCAT = Key("concat", KeyType.Internal) - final val CONTENT_START_COLUMN = Key("contentStartColumn", KeyType.Internal) - final val CONTENT_START_LINE = Key("contentStartLine", KeyType.Internal) - final val COOL_LIKE = Key("cool-like", KeyType.Internal) - final val DENORMAL = Key("denormal", KeyType.Internal) - final val DIGEST = Key("digest", KeyType.Internal) - final val DUMMY_CELL = Key("dummy_cell", KeyType.Internal) - final val FILTER_ELEMENT = Key("filterElement", KeyType.Internal) - final val FRESH = Key("fresh", KeyType.Internal) - final val HAS_DOMAIN_VALUES = Key("hasDomainValues", KeyType.Internal) - final val LEFT_INTERNAL = Key("left", KeyType.Internal) - final val LOCATION = Key(classOf[Location].getName, KeyType.Internal) - final val NAT = Key("nat", KeyType.Internal) - final val NOT_INJECTION = Key("notInjection", KeyType.Internal) - final val NOT_LR1_MODULES = Key("not-lr1-modules", KeyType.Internal) - final val ORIGINAL_PRD = Key("originalPrd", KeyType.Internal) - final val PREDICATE = Key("predicate", KeyType.Internal) + final val ANONYMOUS = Key.internal("anonymous") + final val BRACKET_LABEL = Key.internal("bracketLabel") + final val CELL_FRAGMENT = Key.internal("cellFragment") + final val CELL_OPT_ABSENT = Key.internal("cellOptAbsent") + final val CELL_SORT = Key.internal("cellSort") + final val CONCAT = Key.internal("concat") + final val CONTENT_START_COLUMN = Key.internal("contentStartColumn") + final val CONTENT_START_LINE = Key.internal("contentStartLine") + final val COOL_LIKE = Key.internal("cool-like") + final val DENORMAL = Key.internal("denormal") + final val DIGEST = Key.internal("digest") + final val DUMMY_CELL = Key.internal("dummy_cell") + final val FILTER_ELEMENT = Key.internal("filterElement") + final val FRESH = Key.internal("fresh") + final val HAS_DOMAIN_VALUES = Key.internal("hasDomainValues") + final val LEFT_INTERNAL = Key.internal("left") + final val LOCATION = Key.internal(classOf[Location].getName) + final val NAT = Key.internal("nat") + final val NOT_INJECTION = Key.internal("notInjection") + final val NOT_LR1_MODULES = Key.internal("not-lr1-modules") + final val ORIGINAL_PRD = Key.internal("originalPrd") + final val PREDICATE = Key.internal("predicate") final val PRETTY_PRINT_WITH_SORT_ANNOTATION = - Key("prettyPrintWithSortAnnotation", KeyType.Internal) - final val PRIORITIES = Key("priorities", KeyType.Internal) - final val PRODUCTION = Key(classOf[Production].getName, KeyType.Internal) - final val PROJECTION = Key("projection", KeyType.Internal) - final val RECORD_PRD = Key("recordPrd", KeyType.Internal) - final val RECORD_PRD_ZERO = Key("recordPrd-zero", KeyType.Internal) - final val RECORD_PRD_ONE = Key("recordPrd-one", KeyType.Internal) - final val RECORD_PRD_MAIN = Key("recordPrd-main", KeyType.Internal) - final val RECORD_PRD_EMPTY = Key("recordPrd-empty", KeyType.Internal) - final val RECORD_PRD_SUBSORT = Key("recordPrd-subsort", KeyType.Internal) - final val RECORD_PRD_REPEAT = Key("recordPrd-repeat", KeyType.Internal) - final val RECORD_PRD_ITEM = Key("recordPrd-item", KeyType.Internal) - final val REFRESHED = Key("refreshed", KeyType.Internal) - final val RIGHT_INTERNAL = Key("right", KeyType.Internal) - final val SMT_PRELUDE = Key("smt-prelude", KeyType.Internal) - final val SORT = Key(classOf[Sort].getName, KeyType.Internal) - final val SORT_PARAMS = Key("sortParams", KeyType.Internal) - final val SOURCE = Key(classOf[Source].getName, KeyType.Internal) - final val SYNTAX_MODULE = Key("syntaxModule", KeyType.Internal) - final val TEMPORARY_CELL_SORT_DECL = Key("temporary-cell-sort-decl", KeyType.Internal) - final val TERMINALS = Key("terminals", KeyType.Internal) - final val UNIQUE_ID = Key("UNIQUE_ID", KeyType.Internal) - final val USER_LIST = Key("userList", KeyType.Internal) - final val USER_LIST_TERMINATOR = Key("userListTerminator", KeyType.Internal) - final val WITH_CONFIG = Key("withConfig", KeyType.Internal) + Key.internal("prettyPrintWithSortAnnotation") + final val PRIORITIES = Key.internal("priorities") + final val PRODUCTION = Key.internal(classOf[Production].getName) + final val PROJECTION = Key.internal("projection") + final val RECORD_PRD = Key.internal("recordPrd") + final val RECORD_PRD_ZERO = Key.internal("recordPrd-zero") + final val RECORD_PRD_ONE = Key.internal("recordPrd-one") + final val RECORD_PRD_MAIN = Key.internal("recordPrd-main") + final val RECORD_PRD_EMPTY = Key.internal("recordPrd-empty") + final val RECORD_PRD_SUBSORT = Key.internal("recordPrd-subsort") + final val RECORD_PRD_REPEAT = Key.internal("recordPrd-repeat") + final val RECORD_PRD_ITEM = Key.internal("recordPrd-item") + final val REFRESHED = Key.internal("refreshed") + final val RIGHT_INTERNAL = Key.internal("right") + final val SMT_PRELUDE = Key.internal("smt-prelude") + final val SORT = Key.internal(classOf[Sort].getName) + final val SORT_PARAMS = Key.internal("sortParams") + final val SOURCE = Key.internal(classOf[Source].getName) + final val SYNTAX_MODULE = Key.internal("syntaxModule") + final val TEMPORARY_CELL_SORT_DECL = Key.internal("temporary-cell-sort-decl") + final val TERMINALS = Key.internal("terminals") + final val UNIQUE_ID = Key.internal("UNIQUE_ID") + final val USER_LIST = Key.internal("userList") + final val USER_LIST_TERMINATOR = Key.internal("userListTerminator") + final val WITH_CONFIG = Key.internal("withConfig") private val stringClassName = classOf[String].getName private val intClassName = classOf[java.lang.Integer].getName @@ -409,21 +363,14 @@ object Att { def getBuiltinKeyOptional(key: String): Optional[Key] = if (builtinKeys.contains(key)) { - Optional.of(builtinKeys.get(key).get) + Optional.of(builtinKeys(key)) } else { Optional.empty() } def getInternalKeyOptional(key: String): Optional[Key] = if (internalKeys.contains(key)) { - Optional.of(internalKeys.get(key).get) - } else { - Optional.empty() - } - - def getUserGroupOptional(group: String): Optional[Key] = - if (!builtinKeys.contains(group)) { - Optional.of(Key(group, KeyType.UserGroup, KeyParameter.Optional)) + Optional.of(internalKeys(key)) } else { Optional.empty() } @@ -432,7 +379,8 @@ object Att { getInternalKeyOptional(key).orElseThrow(() => new AssertionError( "Key '" + key + "' was not found among the internal attributes whitelist.\n" + - "To add a new internal attribute, create a field `final val MY_ATT = Key(\"my-att\", KeyType.Internal)` " + + "To add a new internal attribute, create a field `final val MY_ATT = Key.internal" + + "(\"my-att\")` " + "in the Att object." ) )