From 22c814a902493eabb850b1a0c4c2c8332c9a5960 Mon Sep 17 00:00:00 2001 From: Scott Guest Date: Mon, 12 Feb 2024 20:20:17 -0500 Subject: [PATCH 1/5] Update whitelist to track which attributes are emitted to the backend --- .../kframework/backend/kore/ModuleToKORE.java | 5 +- .../scala/org/kframework/attributes/Att.scala | 443 ++++++++++++------ 2 files changed, 303 insertions(+), 145 deletions(-) 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 2c60639d3b7..2e52e5e7c73 100644 --- a/kernel/src/main/java/org/kframework/backend/kore/ModuleToKORE.java +++ b/kernel/src/main/java/org/kframework/backend/kore/ModuleToKORE.java @@ -2013,7 +2013,10 @@ private void convert( for (Tuple2, ?> attribute : // Sort to stabilize error messages - stream(att.att()).sorted(Comparator.comparing(Tuple2::toString)).toList()) { + stream(att.att()) + .filter(e -> e._1._1.shouldEmit()) + .sorted(Comparator.comparing(Tuple2::toString)) + .toList()) { Att.Key key = attribute._1._1; String strKey = key.key(); String clsName = attribute._1._2; diff --git a/kore/src/main/scala/org/kframework/attributes/Att.scala b/kore/src/main/scala/org/kframework/attributes/Att.scala index 7c2f6f00a5f..101f798eb32 100644 --- a/kore/src/main/scala/org/kframework/attributes/Att.scala +++ b/kore/src/main/scala/org/kframework/attributes/Att.scala @@ -140,6 +140,14 @@ object Att { case object Forbidden extends KeyParameter } + sealed trait KeyRange + private object KeyRange extends Serializable { + // Attributes that are only used by the frontend, and will not be emitted to the backends + case object FrontendOnly extends KeyRange + // Attributes used by both the frontend and at least one backend + case object WholePipeline extends KeyRange + } + /* The Key class can only be constructed within Att. To enforce this, we must * - Make the constructor private * - Manually declare apply() and make it private, lest a public one is generated @@ -149,8 +157,10 @@ object Att { key: String, keyType: KeyType, keyParam: KeyParameter, - allowedSentences: Set[Class[_]] + allowedSentences: Set[Class[_]], + keyRange: KeyRange ) extends Serializable { + val shouldEmit: Boolean = keyRange.equals(KeyRange.WholePipeline) override def toString: String = key private[Key] def copy(): Unit = () } @@ -158,12 +168,14 @@ object Att { private[Att] def builtin( key: String, keyParam: KeyParameter, - allowedSentences: Set[Class[_]] - ): Key = Key(key, KeyType.BuiltIn, keyParam, allowedSentences) + allowedSentences: Set[Class[_]], + KeyRange: KeyRange + ): Key = Key(key, KeyType.BuiltIn, keyParam, allowedSentences, KeyRange) private[Att] def internal( - key: String + key: String, + KeyRange: KeyRange ): Key = - Key(key, KeyType.Internal, KeyParameter.Optional, onlyon[AnyRef]) + Key(key, KeyType.Internal, KeyParameter.Optional, onlyon[AnyRef], KeyRange) } def unrecognizedKey(key: String): Att.Key = @@ -171,7 +183,8 @@ object Att { key, KeyType.Unrecognized, KeyParameter.Optional, - onlyon[AnyRef] + onlyon[AnyRef], + KeyRange.FrontendOnly ) val empty: Att = Att(Map.empty) @@ -186,160 +199,302 @@ object Att { onlyon3[T1, T2, T3] ++ onlyon[T4] /* Built-in attribute keys which can appear in user source code */ - final val ALIAS = Key.builtin("alias", KeyParameter.Forbidden, onlyon[Production]) - final val ALIAS_REC = Key.builtin("alias-rec", KeyParameter.Forbidden, onlyon[Production]) - final val ALL_PATH = Key.builtin("all-path", KeyParameter.Forbidden, onlyon2[Claim, Module]) - final val ANYWHERE = Key.builtin("anywhere", KeyParameter.Forbidden, onlyon[Rule]) - final val APPLY_PRIORITY = Key.builtin("applyPriority", KeyParameter.Required, onlyon[Production]) - final val ASSOC = Key.builtin("assoc", KeyParameter.Forbidden, onlyon[Production]) - final val AVOID = Key.builtin("avoid", KeyParameter.Forbidden, onlyon[Production]) - final val BAG = Key.builtin("bag", KeyParameter.Forbidden, onlyon[Production]) - final val BINDER = Key.builtin("binder", KeyParameter.Forbidden, onlyon[Production]) - final val BRACKET = Key.builtin("bracket", KeyParameter.Forbidden, onlyon[Production]) - final val CELL = Key.builtin("cell", KeyParameter.Forbidden, onlyon[Production]) + final val ALIAS = + Key.builtin("alias", KeyParameter.Forbidden, onlyon[Production], KeyRange.WholePipeline) + final val ALIAS_REC = + Key.builtin("alias-rec", KeyParameter.Forbidden, onlyon[Production], KeyRange.WholePipeline) + final val ALL_PATH = + Key.builtin("all-path", KeyParameter.Forbidden, onlyon2[Claim, Module], KeyRange.FrontendOnly) + final val ANYWHERE = + Key.builtin("anywhere", KeyParameter.Forbidden, onlyon[Rule], KeyRange.WholePipeline) + final val APPLY_PRIORITY = + Key.builtin("applyPriority", KeyParameter.Required, onlyon[Production], KeyRange.FrontendOnly) + final val ASSOC = + Key.builtin("assoc", KeyParameter.Forbidden, onlyon[Production], KeyRange.WholePipeline) + final val AVOID = + Key.builtin("avoid", KeyParameter.Forbidden, onlyon[Production], KeyRange.FrontendOnly) + final val BAG = + Key.builtin("bag", KeyParameter.Forbidden, onlyon[Production], KeyRange.FrontendOnly) + final val BINDER = + Key.builtin("binder", KeyParameter.Forbidden, onlyon[Production], KeyRange.WholePipeline) + final val BRACKET = + Key.builtin("bracket", KeyParameter.Forbidden, onlyon[Production], KeyRange.WholePipeline) + final val CELL = + Key.builtin("cell", KeyParameter.Forbidden, onlyon[Production], KeyRange.FrontendOnly) final val CELL_COLLECTION = - Key.builtin("cellCollection", KeyParameter.Forbidden, onlyon2[Production, SyntaxSort]) - final val CELL_NAME = Key.builtin("cellName", KeyParameter.Required, onlyon[Production]) - final val CIRCULARITY = Key.builtin("circularity", KeyParameter.Forbidden, onlyon[Claim]) - final val COLOR = Key.builtin("color", KeyParameter.Required, onlyon[Production]) - final val COLORS = Key.builtin("colors", KeyParameter.Required, onlyon[Production]) - final val COMM = Key.builtin("comm", KeyParameter.Forbidden, onlyon2[Production, Rule]) + Key.builtin( + "cellCollection", + KeyParameter.Forbidden, + onlyon2[Production, SyntaxSort], + KeyRange.FrontendOnly + ) + final val CELL_NAME = + Key.builtin("cellName", KeyParameter.Required, onlyon[Production], KeyRange.FrontendOnly) + final val CIRCULARITY = + Key.builtin("circularity", KeyParameter.Forbidden, onlyon[Claim], KeyRange.WholePipeline) + final val COLOR = + Key.builtin("color", KeyParameter.Required, onlyon[Production], KeyRange.FrontendOnly) + final val COLORS = + Key.builtin("colors", KeyParameter.Required, onlyon[Production], KeyRange.WholePipeline) + final val COMM = + Key.builtin("comm", KeyParameter.Forbidden, onlyon2[Production, Rule], KeyRange.WholePipeline) final val CONCRETE = - Key.builtin("concrete", KeyParameter.Optional, onlyon3[Module, Production, Rule]) - final val CONSTRUCTOR = Key.builtin("constructor", KeyParameter.Forbidden, onlyon[Production]) - final val CONTEXT = Key.builtin("context", KeyParameter.Required, onlyon[ContextAlias]) - final val COOL = Key.builtin("cool", KeyParameter.Forbidden, onlyon[Rule]) - final val DEPENDS = Key.builtin("depends", KeyParameter.Required, onlyon[Claim]) - final val DEPRECATED = Key.builtin("deprecated", KeyParameter.Forbidden, onlyon[Production]) - final val ELEMENT = Key.builtin("element", KeyParameter.Required, onlyon[Production]) - final val EXIT = Key.builtin("exit", KeyParameter.Forbidden, onlyon[Production]) - final val FORMAT = Key.builtin("format", KeyParameter.Required, onlyon[Production]) + Key.builtin( + "concrete", + KeyParameter.Optional, + onlyon3[Module, Production, Rule], + KeyRange.WholePipeline + ) + final val CONSTRUCTOR = + Key.builtin("constructor", KeyParameter.Forbidden, onlyon[Production], KeyRange.WholePipeline) + final val CONTEXT = + Key.builtin("context", KeyParameter.Required, onlyon[ContextAlias], KeyRange.FrontendOnly) + final val COOL = Key.builtin("cool", KeyParameter.Forbidden, onlyon[Rule], KeyRange.WholePipeline) + final val DEPENDS = + Key.builtin("depends", KeyParameter.Required, onlyon[Claim], KeyRange.WholePipeline) + final val DEPRECATED = + Key.builtin("deprecated", KeyParameter.Forbidden, onlyon[Production], KeyRange.WholePipeline) + final val ELEMENT = + Key.builtin("element", KeyParameter.Required, onlyon[Production], KeyRange.WholePipeline) + final val EXIT = + Key.builtin("exit", KeyParameter.Forbidden, onlyon[Production], KeyRange.FrontendOnly) + final val FORMAT = + Key.builtin("format", KeyParameter.Required, onlyon[Production], KeyRange.WholePipeline) final val FRESH_GENERATOR = - Key.builtin("freshGenerator", KeyParameter.Forbidden, onlyon[Production]) - final val FUNCTION = Key.builtin("function", KeyParameter.Forbidden, onlyon[Production]) - final val FUNCTIONAL = Key.builtin("functional", KeyParameter.Forbidden, onlyon[Production]) - final val GROUP = Key.builtin("group", KeyParameter.Required, onlyon[Sentence]) - final val HASKELL = Key.builtin("haskell", KeyParameter.Forbidden, onlyon[Module]) - final val HEAT = Key.builtin("heat", KeyParameter.Forbidden, onlyon[Rule]) - final val HOOK = Key.builtin("hook", KeyParameter.Required, onlyon2[Production, SyntaxSort]) - final val HYBRID = Key.builtin("hybrid", KeyParameter.Optional, onlyon[Production]) - final val IDEM = Key.builtin("idem", KeyParameter.Forbidden, onlyon[Production]) - final val IMPURE = Key.builtin("impure", KeyParameter.Forbidden, onlyon[Production]) - final val INDEX = Key.builtin("index", KeyParameter.Required, onlyon[Production]) - final val INITIAL = Key.builtin("initial", KeyParameter.Forbidden, onlyon[Production]) + Key.builtin( + "freshGenerator", + KeyParameter.Forbidden, + onlyon[Production], + KeyRange.WholePipeline + ) + final val FUNCTION = + Key.builtin("function", KeyParameter.Forbidden, onlyon[Production], KeyRange.WholePipeline) + final val FUNCTIONAL = + Key.builtin("functional", KeyParameter.Forbidden, onlyon[Production], KeyRange.WholePipeline) + final val GROUP = + Key.builtin("group", KeyParameter.Required, onlyon[Sentence], KeyRange.FrontendOnly) + final val HASKELL = + Key.builtin("haskell", KeyParameter.Forbidden, onlyon[Module], KeyRange.FrontendOnly) + final val HEAT = Key.builtin("heat", KeyParameter.Forbidden, onlyon[Rule], KeyRange.FrontendOnly) + final val HOOK = + Key.builtin( + "hook", + KeyParameter.Required, + onlyon2[Production, SyntaxSort], + KeyRange.WholePipeline + ) + final val HYBRID = + Key.builtin("hybrid", KeyParameter.Optional, onlyon[Production], KeyRange.FrontendOnly) + final val IDEM = + Key.builtin("idem", KeyParameter.Forbidden, onlyon[Production], KeyRange.WholePipeline) + final val IMPURE = + Key.builtin("impure", KeyParameter.Forbidden, onlyon[Production], KeyRange.FrontendOnly) + final val INDEX = + Key.builtin("index", KeyParameter.Required, onlyon[Production], KeyRange.FrontendOnly) + final val INITIAL = + Key.builtin("initial", KeyParameter.Forbidden, onlyon[Production], KeyRange.FrontendOnly) final val INITIALIZER = - Key.builtin("initializer", KeyParameter.Forbidden, onlyon2[Production, Rule]) - final val INJECTIVE = Key.builtin("injective", KeyParameter.Forbidden, onlyon[Production]) - final val INTERNAL = Key.builtin("internal", KeyParameter.Forbidden, onlyon[Production]) - final val KLABEL = Key.builtin("klabel", KeyParameter.Required, onlyon[Production]) + Key.builtin( + "initializer", + KeyParameter.Forbidden, + onlyon2[Production, Rule], + KeyRange.FrontendOnly + ) + final val INJECTIVE = + Key.builtin("injective", KeyParameter.Forbidden, onlyon[Production], KeyRange.WholePipeline) + final val INTERNAL = + Key.builtin("internal", KeyParameter.Forbidden, onlyon[Production], KeyRange.FrontendOnly) + final val KLABEL = + Key.builtin("klabel", KeyParameter.Required, onlyon[Production], KeyRange.WholePipeline) final val TERMINATOR_KLABEL = - Key.builtin("terminator-klabel", KeyParameter.Required, onlyon[Production]) - final val LABEL = Key.builtin("label", KeyParameter.Required, onlyon[Sentence]) - final val LATEX = Key.builtin("latex", KeyParameter.Required, onlyon[Production]) - final val LEFT = Key.builtin("left", KeyParameter.Forbidden, onlyon[Production]) - final val LOCATIONS = Key.builtin("locations", KeyParameter.Forbidden, onlyon[SyntaxSort]) - final val MACRO = Key.builtin("macro", KeyParameter.Forbidden, onlyon[Production]) - final val MACRO_REC = Key.builtin("macro-rec", KeyParameter.Forbidden, onlyon[Production]) - final val MAINCELL = Key.builtin("maincell", KeyParameter.Forbidden, onlyon[Production]) - final val MEMO = Key.builtin("memo", KeyParameter.Forbidden, onlyon[Production]) - final val ML_BINDER = Key.builtin("mlBinder", KeyParameter.Forbidden, onlyon[Production]) - final val ML_OP = Key.builtin("mlOp", KeyParameter.Forbidden, onlyon[Production]) - final val MULTIPLICITY = Key.builtin("multiplicity", KeyParameter.Required, onlyon[Production]) - final val NON_ASSOC = Key.builtin("non-assoc", KeyParameter.Forbidden, onlyon[Production]) - final val NON_EXECUTABLE = Key.builtin("non-executable", KeyParameter.Forbidden, onlyon[Rule]) - final val NOT_LR1 = Key.builtin("not-lr1", KeyParameter.Forbidden, onlyon[Module]) - final val NO_EVALUATORS = Key.builtin("no-evaluators", KeyParameter.Forbidden, onlyon[Production]) - final val ONE_PATH = Key.builtin("one-path", KeyParameter.Forbidden, onlyon2[Claim, Module]) - final val OWISE = Key.builtin("owise", KeyParameter.Forbidden, onlyon[Rule]) - final val OVERLOAD = Key.builtin("overload", KeyParameter.Required, onlyon[Production]) - final val PARSER = Key.builtin("parser", KeyParameter.Required, onlyon[Production]) - final val PREC = Key.builtin("prec", KeyParameter.Required, onlyon[Production]) - final val PREFER = Key.builtin("prefer", KeyParameter.Forbidden, onlyon[Production]) + + Key.builtin( + "terminator-klabel", + KeyParameter.Required, + onlyon[Production], + KeyRange.WholePipeline + ) + final val LABEL = + Key.builtin("label", KeyParameter.Required, onlyon[Sentence], KeyRange.WholePipeline) + final val LATEX = + Key.builtin("latex", KeyParameter.Required, onlyon[Production], KeyRange.FrontendOnly) + final val LEFT = + Key.builtin("left", KeyParameter.Forbidden, onlyon[Production], KeyRange.FrontendOnly) + final val LOCATIONS = + Key.builtin("locations", KeyParameter.Forbidden, onlyon[SyntaxSort], KeyRange.FrontendOnly) + final val MACRO = + Key.builtin("macro", KeyParameter.Forbidden, onlyon[Production], KeyRange.WholePipeline) + final val MACRO_REC = + Key.builtin("macro-rec", KeyParameter.Forbidden, onlyon[Production], KeyRange.WholePipeline) + final val MAINCELL = + Key.builtin("maincell", KeyParameter.Forbidden, onlyon[Production], KeyRange.FrontendOnly) + final val MEMO = + Key.builtin("memo", KeyParameter.Forbidden, onlyon[Production], KeyRange.WholePipeline) + final val ML_BINDER = + Key.builtin("mlBinder", KeyParameter.Forbidden, onlyon[Production], KeyRange.FrontendOnly) + final val ML_OP = + Key.builtin("mlOp", KeyParameter.Forbidden, onlyon[Production], KeyRange.FrontendOnly) + final val MULTIPLICITY = + Key.builtin("multiplicity", KeyParameter.Required, onlyon[Production], KeyRange.FrontendOnly) + final val NON_ASSOC = + Key.builtin("non-assoc", KeyParameter.Forbidden, onlyon[Production], KeyRange.FrontendOnly) + final val NON_EXECUTABLE = + Key.builtin("non-executable", KeyParameter.Forbidden, onlyon[Rule], KeyRange.WholePipeline) + final val NOT_LR1 = + Key.builtin("not-lr1", KeyParameter.Forbidden, onlyon[Module], KeyRange.FrontendOnly) + final val NO_EVALUATORS = + Key.builtin("no-evaluators", KeyParameter.Forbidden, onlyon[Production], KeyRange.WholePipeline) + final val ONE_PATH = + Key.builtin("one-path", KeyParameter.Forbidden, onlyon2[Claim, Module], KeyRange.FrontendOnly) + final val OVERLOAD = + Key.builtin("overload", KeyParameter.Required, onlyon[Production], KeyRange.FrontendOnly) + final val OWISE = + Key.builtin("owise", KeyParameter.Forbidden, onlyon[Rule], KeyRange.WholePipeline) + final val PARSER = + Key.builtin("parser", KeyParameter.Required, onlyon[Production], KeyRange.FrontendOnly) + final val PREC = + Key.builtin("prec", KeyParameter.Required, onlyon[Production], KeyRange.FrontendOnly) + final val PREFER = + Key.builtin("prefer", KeyParameter.Forbidden, onlyon[Production], KeyRange.FrontendOnly) final val PRESERVES_DEFINEDNESS = - Key.builtin("preserves-definedness", KeyParameter.Forbidden, onlyon[Rule]) + Key.builtin( + "preserves-definedness", + KeyParameter.Forbidden, + onlyon[Rule], + KeyRange.WholePipeline + ) final val PRIORITY = - Key.builtin("priority", KeyParameter.Required, onlyon4[Context, ContextAlias, Production, Rule]) - final val PRIVATE = Key.builtin("private", KeyParameter.Forbidden, onlyon2[Module, Production]) - final val PUBLIC = Key.builtin("public", KeyParameter.Forbidden, onlyon2[Module, Production]) + Key.builtin( + "priority", + KeyParameter.Required, + onlyon4[Context, ContextAlias, Production, Rule], + KeyRange.WholePipeline + ) + final val PRIVATE = Key.builtin( + "private", + KeyParameter.Forbidden, + onlyon2[Module, Production], + KeyRange.FrontendOnly + ) + final val PUBLIC = Key.builtin( + "public", + KeyParameter.Forbidden, + onlyon2[Module, Production], + KeyRange.FrontendOnly + ) final val RESULT = - Key.builtin("result", KeyParameter.Required, onlyon4[Context, ContextAlias, Production, Rule]) - final val RETURNS_UNIT = Key.builtin("returnsUnit", KeyParameter.Forbidden, onlyon[Production]) - final val RIGHT = Key.builtin("right", KeyParameter.Forbidden, onlyon[Production]) - final val SEQSTRICT = Key.builtin("seqstrict", KeyParameter.Optional, onlyon[Production]) - final val SIMPLIFICATION = Key.builtin("simplification", KeyParameter.Optional, onlyon[Rule]) - final val SMTLIB = Key.builtin("smtlib", KeyParameter.Required, onlyon[Production]) - final val SMT_HOOK = Key.builtin("smt-hook", KeyParameter.Required, onlyon[Production]) - final val SMT_LEMMA = Key.builtin("smt-lemma", KeyParameter.Forbidden, onlyon[Rule]) - final val STREAM = Key.builtin("stream", KeyParameter.Optional, onlyon2[Production, Rule]) - final val STRICT = Key.builtin("strict", KeyParameter.Optional, onlyon[Production]) - final val SYMBOL = Key.builtin("symbol", KeyParameter.Optional, onlyon[Production]) + Key.builtin( + "result", + KeyParameter.Required, + onlyon4[Context, ContextAlias, Production, Rule], + KeyRange.FrontendOnly + ) + final val RETURNS_UNIT = + Key.builtin("returnsUnit", KeyParameter.Forbidden, onlyon[Production], KeyRange.FrontendOnly) + final val RIGHT = + Key.builtin("right", KeyParameter.Forbidden, onlyon[Production], KeyRange.FrontendOnly) + final val SEQSTRICT = + Key.builtin("seqstrict", KeyParameter.Optional, onlyon[Production], KeyRange.FrontendOnly) + final val SIMPLIFICATION = + Key.builtin("simplification", KeyParameter.Optional, onlyon[Rule], KeyRange.WholePipeline) + final val SMTLIB = + Key.builtin("smtlib", KeyParameter.Required, onlyon[Production], KeyRange.WholePipeline) + final val SMT_HOOK = + Key.builtin("smt-hook", KeyParameter.Required, onlyon[Production], KeyRange.WholePipeline) + final val SMT_LEMMA = + Key.builtin("smt-lemma", KeyParameter.Forbidden, onlyon[Rule], KeyRange.WholePipeline) + final val STREAM = + Key.builtin("stream", KeyParameter.Optional, onlyon2[Production, Rule], KeyRange.FrontendOnly) + final val STRICT = + Key.builtin("strict", KeyParameter.Optional, onlyon[Production], KeyRange.FrontendOnly) + final val SYMBOL = + Key.builtin("symbol", KeyParameter.Optional, onlyon[Production], KeyRange.WholePipeline) final val SYMBOLIC = - Key.builtin("symbolic", KeyParameter.Optional, onlyon3[Module, Production, Rule]) - final val TAG = Key.builtin("tag", KeyParameter.Required, onlyon[Rule]) - final val TOKEN = Key.builtin("token", KeyParameter.Forbidden, onlyon2[SyntaxSort, Production]) - final val TOTAL = Key.builtin("total", KeyParameter.Forbidden, onlyon[Production]) - final val TRUSTED = Key.builtin("trusted", KeyParameter.Forbidden, onlyon[Claim]) - final val TYPE = Key.builtin("type", KeyParameter.Required, onlyon[Production]) + Key.builtin( + "symbolic", + KeyParameter.Optional, + onlyon3[Module, Production, Rule], + KeyRange.WholePipeline + ) + final val TAG = Key.builtin("tag", KeyParameter.Required, onlyon[Rule], KeyRange.FrontendOnly) + final val TOKEN = Key.builtin( + "token", + KeyParameter.Forbidden, + onlyon2[SyntaxSort, Production], + KeyRange.WholePipeline + ) + final val TOTAL = + Key.builtin("total", KeyParameter.Forbidden, onlyon[Production], KeyRange.WholePipeline) + final val TRUSTED = + Key.builtin("trusted", KeyParameter.Forbidden, onlyon[Claim], KeyRange.WholePipeline) + final val TYPE = + Key.builtin("type", KeyParameter.Required, onlyon[Production], KeyRange.FrontendOnly) final val UNBOUND_VARIABLES = Key.builtin( "unboundVariables", KeyParameter.Required, - onlyon4[Context, ContextAlias, Production, RuleOrClaim] + onlyon4[Context, ContextAlias, Production, RuleOrClaim], + KeyRange.FrontendOnly ) - final val UNIT = Key.builtin("unit", KeyParameter.Required, onlyon[Production]) - final val UNPARSE_AVOID = Key.builtin("unparseAvoid", KeyParameter.Forbidden, onlyon[Production]) - final val UNUSED = Key.builtin("unused", KeyParameter.Forbidden, onlyon[Production]) - final val WRAP_ELEMENT = Key.builtin("wrapElement", KeyParameter.Required, onlyon[Production]) + final val UNIT = + Key.builtin("unit", KeyParameter.Required, onlyon[Production], KeyRange.WholePipeline) + final val UNPARSE_AVOID = + Key.builtin("unparseAvoid", KeyParameter.Forbidden, onlyon[Production], KeyRange.FrontendOnly) + final val UNUSED = + Key.builtin("unused", KeyParameter.Forbidden, onlyon[Production], KeyRange.FrontendOnly) + final val WRAP_ELEMENT = + Key.builtin("wrapElement", KeyParameter.Required, onlyon[Production], KeyRange.FrontendOnly) /* Internal attribute keys which cannot appear in user source code */ - 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 ANONYMOUS = Key.internal("anonymous", KeyRange.FrontendOnly) + final val BRACKET_LABEL = Key.internal("bracketLabel", KeyRange.FrontendOnly) + final val CELL_FRAGMENT = Key.internal("cellFragment", KeyRange.FrontendOnly) + final val CELL_OPT_ABSENT = Key.internal("cellOptAbsent", KeyRange.FrontendOnly) + final val CELL_SORT = Key.internal("cellSort", KeyRange.FrontendOnly) + final val CONCAT = Key.internal("concat", KeyRange.WholePipeline) + final val CONTENT_START_COLUMN = Key.internal("contentStartColumn", KeyRange.FrontendOnly) + final val CONTENT_START_LINE = Key.internal("contentStartLine", KeyRange.FrontendOnly) + final val COOL_LIKE = Key.internal("cool-like", KeyRange.WholePipeline) + final val DENORMAL = Key.internal("denormal", KeyRange.FrontendOnly) + final val DIGEST = Key.internal("digest", KeyRange.FrontendOnly) + final val DUMMY_CELL = Key.internal("dummy_cell", KeyRange.FrontendOnly) + final val FILTER_ELEMENT = Key.internal("filterElement", KeyRange.FrontendOnly) + final val FRESH = Key.internal("fresh", KeyRange.FrontendOnly) + final val HAS_DOMAIN_VALUES = Key.internal("hasDomainValues", KeyRange.WholePipeline) + final val LEFT_INTERNAL = Key.internal("left", KeyRange.FrontendOnly) + final val LOCATION = Key.internal(classOf[Location].getName, KeyRange.WholePipeline) + final val NAT = Key.internal("nat", KeyRange.WholePipeline) + final val NOT_INJECTION = Key.internal("notInjection", KeyRange.FrontendOnly) + final val NOT_LR1_MODULES = Key.internal("not-lr1-modules", KeyRange.FrontendOnly) + final val ORIGINAL_PRD = Key.internal("originalPrd", KeyRange.FrontendOnly) + final val PREDICATE = Key.internal("predicate", KeyRange.FrontendOnly) final val PRETTY_PRINT_WITH_SORT_ANNOTATION = - 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 SYMBOL_OVERLOAD = Key.internal("symbol-overload") - 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") + Key.internal("prettyPrintWithSortAnnotation", KeyRange.FrontendOnly) + final val PRIORITIES = Key.internal("priorities", KeyRange.FrontendOnly) + final val PRODUCTION = Key.internal(classOf[Production].getName, KeyRange.FrontendOnly) + final val PROJECTION = Key.internal("projection", KeyRange.FrontendOnly) + final val RECORD_PRD = Key.internal("recordPrd", KeyRange.FrontendOnly) + final val RECORD_PRD_ZERO = Key.internal("recordPrd-zero", KeyRange.FrontendOnly) + final val RECORD_PRD_ONE = Key.internal("recordPrd-one", KeyRange.FrontendOnly) + final val RECORD_PRD_MAIN = Key.internal("recordPrd-main", KeyRange.FrontendOnly) + final val RECORD_PRD_EMPTY = Key.internal("recordPrd-empty", KeyRange.FrontendOnly) + final val RECORD_PRD_SUBSORT = Key.internal("recordPrd-subsort", KeyRange.FrontendOnly) + final val RECORD_PRD_REPEAT = Key.internal("recordPrd-repeat", KeyRange.FrontendOnly) + final val RECORD_PRD_ITEM = Key.internal("recordPrd-item", KeyRange.FrontendOnly) + final val REFRESHED = Key.internal("refreshed", KeyRange.FrontendOnly) + final val RIGHT_INTERNAL = Key.internal("right", KeyRange.FrontendOnly) + final val SMT_PRELUDE = Key.internal("smt-prelude", KeyRange.FrontendOnly) + final val SORT = Key.internal(classOf[Sort].getName, KeyRange.FrontendOnly) + final val SORT_PARAMS = Key.internal("sortParams", KeyRange.FrontendOnly) + final val SOURCE = Key.internal(classOf[Source].getName, KeyRange.WholePipeline) + final val SYMBOL_OVERLOAD = Key.internal("symbol-overload", KeyRange.WholePipeline) + final val SYNTAX_MODULE = Key.internal("syntaxModule", KeyRange.FrontendOnly) + final val TEMPORARY_CELL_SORT_DECL = + Key.internal("temporary-cell-sort-decl", KeyRange.FrontendOnly) + final val TERMINALS = Key.internal("terminals", KeyRange.FrontendOnly) + final val UNIQUE_ID = Key.internal("UNIQUE_ID", KeyRange.WholePipeline) + final val USER_LIST = Key.internal("userList", KeyRange.FrontendOnly) + final val USER_LIST_TERMINATOR = Key.internal("userListTerminator", KeyRange.FrontendOnly) + final val WITH_CONFIG = Key.internal("withConfig", KeyRange.FrontendOnly) private val stringClassName = classOf[String].getName private val intClassName = classOf[java.lang.Integer].getName From cd6e744dcbae734b98bf062d00b04ca6eec05dfc Mon Sep 17 00:00:00 2001 From: Scott Guest Date: Thu, 15 Feb 2024 15:35:41 -0500 Subject: [PATCH 2/5] Emit left and right (internal), priorities, terminals --- kore/src/main/scala/org/kframework/attributes/Att.scala | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/kore/src/main/scala/org/kframework/attributes/Att.scala b/kore/src/main/scala/org/kframework/attributes/Att.scala index 101f798eb32..6238f3d4b15 100644 --- a/kore/src/main/scala/org/kframework/attributes/Att.scala +++ b/kore/src/main/scala/org/kframework/attributes/Att.scala @@ -460,7 +460,7 @@ object Att { final val FILTER_ELEMENT = Key.internal("filterElement", KeyRange.FrontendOnly) final val FRESH = Key.internal("fresh", KeyRange.FrontendOnly) final val HAS_DOMAIN_VALUES = Key.internal("hasDomainValues", KeyRange.WholePipeline) - final val LEFT_INTERNAL = Key.internal("left", KeyRange.FrontendOnly) + final val LEFT_INTERNAL = Key.internal("left", KeyRange.WholePipeline) final val LOCATION = Key.internal(classOf[Location].getName, KeyRange.WholePipeline) final val NAT = Key.internal("nat", KeyRange.WholePipeline) final val NOT_INJECTION = Key.internal("notInjection", KeyRange.FrontendOnly) @@ -469,7 +469,7 @@ object Att { final val PREDICATE = Key.internal("predicate", KeyRange.FrontendOnly) final val PRETTY_PRINT_WITH_SORT_ANNOTATION = Key.internal("prettyPrintWithSortAnnotation", KeyRange.FrontendOnly) - final val PRIORITIES = Key.internal("priorities", KeyRange.FrontendOnly) + final val PRIORITIES = Key.internal("priorities", KeyRange.WholePipeline) final val PRODUCTION = Key.internal(classOf[Production].getName, KeyRange.FrontendOnly) final val PROJECTION = Key.internal("projection", KeyRange.FrontendOnly) final val RECORD_PRD = Key.internal("recordPrd", KeyRange.FrontendOnly) @@ -481,7 +481,7 @@ object Att { final val RECORD_PRD_REPEAT = Key.internal("recordPrd-repeat", KeyRange.FrontendOnly) final val RECORD_PRD_ITEM = Key.internal("recordPrd-item", KeyRange.FrontendOnly) final val REFRESHED = Key.internal("refreshed", KeyRange.FrontendOnly) - final val RIGHT_INTERNAL = Key.internal("right", KeyRange.FrontendOnly) + final val RIGHT_INTERNAL = Key.internal("right", KeyRange.WholePipeline) final val SMT_PRELUDE = Key.internal("smt-prelude", KeyRange.FrontendOnly) final val SORT = Key.internal(classOf[Sort].getName, KeyRange.FrontendOnly) final val SORT_PARAMS = Key.internal("sortParams", KeyRange.FrontendOnly) @@ -490,7 +490,7 @@ object Att { final val SYNTAX_MODULE = Key.internal("syntaxModule", KeyRange.FrontendOnly) final val TEMPORARY_CELL_SORT_DECL = Key.internal("temporary-cell-sort-decl", KeyRange.FrontendOnly) - final val TERMINALS = Key.internal("terminals", KeyRange.FrontendOnly) + final val TERMINALS = Key.internal("terminals", KeyRange.WholePipeline) final val UNIQUE_ID = Key.internal("UNIQUE_ID", KeyRange.WholePipeline) final val USER_LIST = Key.internal("userList", KeyRange.FrontendOnly) final val USER_LIST_TERMINATOR = Key.internal("userListTerminator", KeyRange.FrontendOnly) From 5af0a8263475604249c9e2125ce02f537c35cc38 Mon Sep 17 00:00:00 2001 From: Scott Guest Date: Mon, 19 Feb 2024 19:36:47 -0500 Subject: [PATCH 3/5] Update flaky inset-11-spec.k test output From 2b7591397e391f108426e1ed1292e68385e6d1d0 Mon Sep 17 00:00:00 2001 From: Scott Guest Date: Fri, 23 Feb 2024 15:32:51 -0500 Subject: [PATCH 4/5] WIP --- .../org/kframework/attributes/Attribute.java | 45 + .../org/kframework/attributes/ClassSet.java | 34 + .../org/kframework/attributes/JavaAtt.java | 834 ++++++++++++++++++ 3 files changed, 913 insertions(+) create mode 100644 kore/src/main/java/org/kframework/attributes/Attribute.java create mode 100644 kore/src/main/java/org/kframework/attributes/ClassSet.java create mode 100644 kore/src/main/java/org/kframework/attributes/JavaAtt.java diff --git a/kore/src/main/java/org/kframework/attributes/Attribute.java b/kore/src/main/java/org/kframework/attributes/Attribute.java new file mode 100644 index 00000000000..7bc222fbe1d --- /dev/null +++ b/kore/src/main/java/org/kframework/attributes/Attribute.java @@ -0,0 +1,45 @@ +// Copyright (c) Runtime Verification, Inc. All Rights Reserved. +package org.kframework.attributes; + +import com.google.common.collect.Sets; +import java.util.Arrays; +import java.util.EnumSet; + +public abstract class Attribute { + + public enum Syntax { + CELL, + CLAIM, + CONTEXT, + CONTEXT_ALIAS, + MODULE, + PRODUCTION, + RULE, + SENTENCE, + SYNTAX_SORT, + UNCHECKED + } + + public sealed interface Visibility { + record User(EnumSet allowedSyntax) implements Visibility { + User(Syntax... allowed) { + this(Sets.newEnumSet(Arrays.asList(allowed), Syntax.class)); + } + } + + record Internal() implements Visibility {} + } + + public enum EmitToKORE { + YES, + NO + } + + public final Visibility visibility; + public final EmitToKORE emit; + + protected Attribute(Visibility visibility, EmitToKORE emit) { + this.visibility = visibility; + this.emit = emit; + } +} diff --git a/kore/src/main/java/org/kframework/attributes/ClassSet.java b/kore/src/main/java/org/kframework/attributes/ClassSet.java new file mode 100644 index 00000000000..4b9454d4854 --- /dev/null +++ b/kore/src/main/java/org/kframework/attributes/ClassSet.java @@ -0,0 +1,34 @@ +// Copyright (c) Runtime Verification, Inc. All Rights Reserved. +package org.kframework.attributes; + +import java.util.Objects; +import java.util.Optional; +import org.pcollections.HashPMap; + +public class ClassSet { + + public final HashPMap, Object> data; + + private ClassSet(HashPMap, Object> data) { + this.data = data; + } + + public ClassSet add(Class elemClass, T elem) { + return new ClassSet<>(data.plus(elemClass, elem)); + } + + public Optional get(Class elemClass) { + if (!data.containsKey(elemClass)) { + return Optional.empty(); + } + return Optional.of(Objects.requireNonNull(elemClass.cast(data.get(elemClass)))); + } + + public boolean contains(Class elemClass) { + return data.containsKey(elemClass); + } + + public ClassSet remove(Class elemClass) { + return new ClassSet<>(data.minus(elemClass)); + } +} diff --git a/kore/src/main/java/org/kframework/attributes/JavaAtt.java b/kore/src/main/java/org/kframework/attributes/JavaAtt.java new file mode 100644 index 00000000000..b6d8027be11 --- /dev/null +++ b/kore/src/main/java/org/kframework/attributes/JavaAtt.java @@ -0,0 +1,834 @@ +// Copyright (c) Runtime Verification, Inc. All Rights Reserved. +package org.kframework.attributes; + +import com.google.common.collect.ImmutableSet; +import java.util.Arrays; +import java.util.Optional; +import java.util.Set; +import java.util.function.Function; +import java.util.stream.Collectors; +import org.kframework.utils.errorsystem.KEMException; +import scala.util.Either; +import scala.util.Left; + +public class JavaAtt { + public record Key( + Class type, + String key, + Function, Either> parser) {} + + public class MyAtt {} + ; + + public static class Whitelist { + public static final Key FOO_1 = new Key<>(MyAtt.class, "foo", s -> null); + public static final Key FOO_2 = new Key<>(MyAtt.class, "foo", s -> null); + } + + public static final ImmutableSet> whitelist = + Arrays.stream(JavaAtt.Whitelist.class.getDeclaredFields()) + .map( + f -> { + try { + return (Key) f.get(null); + } catch (IllegalAccessException e) { + throw KEMException.internalError( + "Malformed Att.Whitelist field: " + + f.getName() + + "\nExpected `public static final Key MY_ATT = new Key<>(...)`"); + } + }) + .collect(ImmutableSet.toImmutableSet()); + + static { + String dupKeysErr = + whitelist.stream().collect(Collectors.groupingBy(Key::key)).entrySet().stream() + .filter(e -> e.getValue().size() > 1) + .map( + e -> + "\"" + + e.getKey() + + "\": " + + e.getValue().stream().map(k -> k.type.getSimpleName()).toList()) + .collect(Collectors.joining("\n")); + if (!dupKeysErr.isEmpty()) { + throw KEMException.internalError("Found duplicate keys in Att.Whitelist!\n" + dupKeysErr); + } + } + + public sealed interface ParseError { + record UnrecognizedKey(String key) implements ParseError {} + + record BadValue(KEMException e) implements ParseError {} + } + + public static Either parse(String key, Optional value) { + Set> keys = + whitelist.stream().filter(k -> k.key.equals(key)).collect(Collectors.toSet()); + if (keys.size() > 1) { + throw new AssertionError( + "Attribute " + + key + + value.map(v -> "(" + v + ")").orElse("") + + " parsed by multiple Att.Whitelist keys: " + + keys.stream().map(p -> p.type.getSimpleName()).toList()); + } + if (keys.isEmpty()) { + return Left.apply(new ParseError.UnrecognizedKey(key)); + } + return null; + } + + // public static Either> parse(String key, String value) { + // Attribute foo = + // switch (key) { + // case "alias" -> TaggedData.ALIAS; + // case "alias-rec" -> TaggedData.ALIAS_REC; + // case "all-path" -> TaggedData.ALL_PATH; + // case "anywhere" -> TaggedData.ANYWHERE; + // case "applyPriority" -> new ApplyPriority(); + // case "assoc" -> TaggedData.ASSOC; + // case "avoid" -> TaggedData.AVOID; + // case "bag" -> TaggedData.BAG; + // case "binder" -> TaggedData.BINDER; + // case "bracket" -> TaggedData.BRACKET; + // case "cell" -> TaggedData.CELL; + // case "cellCollection" -> TaggedData.CELL_COLLECTION; + // case "cellName" -> new CellName(); + // case "circularity" -> TaggedData.CIRCULARITY; + // case "color" -> new Color(); + // case "colors" -> new Colors(); + // case "comm" -> TaggedData.COMM; + // case "concrete" -> new Concrete(); + // case "constructor" -> TaggedData.CONSTRUCTOR; + // case "context" -> new Context(); + // case "cool" -> TaggedData.COOL; + // case "depends" -> new Depends(); + // case "deprecated" -> TaggedData.DEPRECATED; + // case "element" -> new Element(); + // case "exit" -> TaggedData.EXIT; + // case "format" -> new Format(); + // case "freshGenerator" -> TaggedData.FRESH_GENERATOR; + // case "function" -> TaggedData.FUNCTION; + // case "functional" -> TaggedData.FUNCTIONAL; + // case "group" -> new Group(); + // case "haskell" -> TaggedData.HASKELL; + // case "heat" -> TaggedData.HEAT; + // case "hook" -> new Hook(); + // case "hybrid" -> new Hybrid(); + // case "idem" -> TaggedData.IDEM; + // case "impure" -> TaggedData.IMPURE; + // case "index" -> new Index(); + // case "initial" -> TaggedData.INITIAL; + // case "initializer" -> TaggedData.INITIALIZER; + // case "injective" -> TaggedData.INJECTIVE; + // case "internal" -> TaggedData.INTERNAL; + // case "klabel" -> new Klabel(); + // case "terminator-klabel" -> new TerminatorKlabel(); + // case "label" -> new Label(); + // case "latex" -> new Latex(); + // case "left" -> TaggedData.LEFT; + // case "locations" -> TaggedData.LOCATIONS; + // case "macro" -> TaggedData.MACRO; + // case "macro-rec" -> TaggedData.MACRO_REC; + // case "maincell" -> TaggedData.MAINCELL; + // case "memo" -> TaggedData.MEMO; + // case "mlBinder" -> TaggedData.ML_BINDER; + // case "mlOp" -> TaggedData.ML_OP; + // case "multiplicity" -> new Multiplicity(); + // case "non-assoc" -> TaggedData.NON_ASSOC; + // case "non-executable" -> TaggedData.NON_EXECUTABLE; + // case "not-lr1" -> TaggedData.NOT_LR1; + // case "no-evaluators" -> TaggedData.NO_EVALUATORS; + // case "one-path" -> TaggedData.ONE_PATH; + // case "owise" -> TaggedData.OWISE; + // case "parser" -> new Parser(); + // case "prec" -> new Prec(); + // case "prefer" -> TaggedData.PREFER; + // case "preserves-definedness" -> TaggedData.PRESERVES_DEFINEDNESS; + // case "priority" -> new Priority(); + // case "private" -> TaggedData.PRIVATE; + // case "public" -> TaggedData.PUBLIC; + // case "result" -> new Result(); + // case "returnsUnit" -> TaggedData.RETURNS_UNIT; + // case "right" -> TaggedData.RIGHT; + // case "seqstrict" -> new Seqstrict(); + // case "simplification" -> new Simplification(); + // case "smtlib" -> new SMTlib(); + // case "smt-hook" -> new SMTHook(); + // case "smt-lemma" -> TaggedData.SMT_LEMMA; + // case "stream" -> new Stream(); + // case "strict" -> new Strict(); + // case "symbol" -> new Symbol(); + // case "symbolic" -> new Symbolic(); + // case "tag" -> new Tag(); + // case "token" -> TaggedData.TOKEN; + // case "total" -> TaggedData.TOTAL; + // case "trusted" -> TaggedData.TRUSTED; + // case "type" -> new Type(); + // case "unboundVariables" -> new UnboundVariables(); + // case "unit" -> new Unit(); + // case "unparseAvoid" -> TaggedData.UNPARSE_AVOID; + // case "unused" -> TaggedData.UNUSED; + // case "wrapElement" -> new WrapElement(); + // case "anonymous" -> new Anonymous(); + // case "bracketLabel" -> new BracketLabel(); + // case "cellFragment" -> new CellFragment(); + // case "cellOptAbsent" -> new CellOptAbsent(); + // case "cellSort" -> new CellSort(); + // case "concat" -> new Concat(); + // case "contentStartColumn" -> new ContentStartColumn(); + // case "contentStartLine" -> new ContentStartLine(); + // case "cool-like" -> new CoolLike(); + // case "denormal" -> new Denormal(); + // case "digest" -> new Digest(); + // case "dummy_cell" -> new DummyCell(); + // case "filterElement" -> new FilterElement(); + // case "fresh" -> new Fresh(); + // case "hasDomainValues" -> new HasDomainValues(); + // case "left" -> new LeftInternal(); + // case "nat" -> new Nat(); + // case "notInjection" -> new NotInjection(); + // case "not-lr1-modules" -> new NotLr1Modules(); + // case "originalPrd" -> new OriginalPrd(); + // case "overload" -> new Overload(); + // case "predicate" -> new Predicate(); + // case "prettyPrintWithSortAnnotation" -> new PrettyPrintWithSortAnnotation(); + // case "priorities" -> new Priorities(); + // case "projection" -> new Projection(); + // case "recordPrd" -> new RecordPrd(); + // case "recordPrd-zero" -> new RecordPrdZero(); + // case "recordPrd-one" -> new RecordPrdOne(); + // case "recordPrd-main" -> new RecordPrdMain(); + // case "recordPrd-empty" -> new RecordPrdEmpty(); + // case "recordPrd-subsort" -> new RecordPrdSubsort(); + // case "recordPrd-repeat" -> new RecordPrdRepeat(); + // case "recordPrd-item" -> new RecordPrdItem(); + // case "refreshed" -> new Refreshed(); + // case "right" -> new RightInternal(); + // case "smt-prelude" -> new SMTPrelude(); + // case "sortParams" -> new SortParams(); + // case "symbol-overload" -> new SymbolOverload(); + // case "syntaxModule" -> new SyntaxModule(); + // case "temporary-cell-sort-decl" -> new TemporaryCellSortDecl(); + // case "terminals" -> new Terminals(); + // case "UNIQUE_ID" -> new UniqueId(); + // case "userList" -> new UserList(); + // case "userListTerminator" -> new UserListTerminator(); + // case "withConfig" -> new WithConfig(); + // default -> null; + // }; + // } + + // public static final class Alias extends MarkerAttribute { + // private Alias() { + // super(new Key<>(Alias.class), "alias", new Visibility.User(Syntax.PRODUCTION)); + // } + // } + // + // public static final class AliasRec extends MarkerAttribute { + // private AliasRec() { + // super(new Key<>(AliasRec.class), "alias-rec", new Visibility.User(Syntax.PRODUCTION)); + // } + // } + // + // public static final class AllPath extends MarkerAttribute { + // private AllPath() { + // super(new Key<>(AllPath.class), "all-path", new Visibility.User(Syntax.CLAIM, + // Syntax.MODULE)); + // } + // } + // + // public static final class Anywhere extends MarkerAttribute { + // private Anywhere() { + // super(new Key<>(Anywhere.class), "anywhere", new Visibility.User(Syntax.RULE)); + // } + // } + // + // public static final class Assoc extends MarkerAttribute { + // private Assoc() { + // super(new Key<>(Assoc.class), "assoc", new Visibility.User(Syntax.PRODUCTION)); + // } + // } + // + // public static final class Avoid extends MarkerAttribute { + // private Avoid() { + // super(new Key<>(Avoid.class), "avoid", new Visibility.User(Syntax.PRODUCTION)); + // } + // } + // + // public static final class Bag extends MarkerAttribute { + // private Bag() { + // super(new Key<>(Bag.class), "bag", new Visibility.User(Syntax.PRODUCTION)); + // } + // } + // + // public static final class Binder extends MarkerAttribute { + // private Binder() { + // super(new Key<>(Binder.class), "binder", new Visibility.User(Syntax.PRODUCTION)); + // } + // } + // + // public static final class Bracket extends MarkerAttribute { + // private Bracket() { + // super(new Key<>(Bracket.class), "bracket", new Visibility.User(Syntax.PRODUCTION)); + // } + // } + // + // public static final class Cell extends MarkerAttribute { + // private Cell() { + // super(new Key<>(Cell.class), "cell", new Visibility.User(Syntax.PRODUCTION)); + // } + // } + // + // public static final class CellCollection extends MarkerAttribute { + // private CellCollection() { + // super( + // new Key<>(CellCollection.class), + // "cellCollection", + // new Visibility.User(Syntax.PRODUCTION, Syntax.SYNTAX_SORT)); + // } + // } + // + // public static final class Circularity extends MarkerAttribute { + // private Circularity() { + // super(new Key<>(Circularity.class), "circularity", new Visibility.User(Syntax.CLAIM)); + // } + // } + // + // public static final class Comm extends MarkerAttribute { + // private Comm() { + // super(new Key<>(Comm.class), "comm", new Visibility.User(Syntax.PRODUCTION, Syntax.RULE)); + // } + // } + // + // public static final class Constructor extends MarkerAttribute { + // private Constructor() { + // super(new Key<>(Constructor.class), "constructor", new + // Visibility.User(Syntax.PRODUCTION)); + // } + // } + // + // public static final class Cool extends MarkerAttribute { + // private Cool() { + // super(new Key<>(Cool.class), "cool", new Visibility.User(Syntax.RULE)); + // } + // } + // + // public static final class Deprecated extends MarkerAttribute { + // private Deprecated() { + // super(new Key<>(Deprecated.class), "deprecated", new Visibility.User(Syntax.PRODUCTION)); + // } + // } + // + // public static final class Exit extends MarkerAttribute { + // private Exit() { + // super(new Key<>(Exit.class), "exit", new Visibility.User(Syntax.PRODUCTION)); + // } + // } + // + // public static final class FreshGenerator extends MarkerAttribute { + // private FreshGenerator() { + // super( + // new Key<>(FreshGenerator.class), + // "freshGenerator", + // new Visibility.User(Syntax.PRODUCTION)); + // } + // } + // + // public static final class Function extends MarkerAttribute { + // private Function() { + // super(new Key<>(Function.class), "function", new Visibility.User(Syntax.PRODUCTION)); + // } + // } + // + // public static final class Functional extends MarkerAttribute { + // private Functional() { + // super(new Key<>(Functional.class), "functional", new Visibility.User(Syntax.PRODUCTION)); + // } + // } + // + // public static final class Haskell extends MarkerAttribute { + // private Haskell() { + // super(new Key<>(Haskell.class), "haskell", new Visibility.User(Syntax.MODULE)); + // } + // } + // + // public static final class Heat extends MarkerAttribute { + // private Heat() { + // super(new Key<>(Heat.class), "heat", new Visibility.User(Syntax.RULE)); + // } + // } + // + // public static final class Idem extends MarkerAttribute { + // private Idem() { + // super(new Key<>(Idem.class), "idem", new Visibility.User(Syntax.PRODUCTION)); + // } + // } + // + // public static final class Impure extends MarkerAttribute { + // private Impure() { + // super(new Key<>(Impure.class), "impure", new Visibility.User(Syntax.PRODUCTION)); + // } + // } + // + // public static final class Initial extends MarkerAttribute { + // private Initial() { + // super(new Key<>(Initial.class), "initial", new Visibility.User(Syntax.PRODUCTION)); + // } + // } + // + // public static final class Initializer extends MarkerAttribute { + // private Initializer() { + // super( + // new Key<>(Initializer.class), + // "initializer", + // new Visibility.User(Syntax.PRODUCTION, Syntax.RULE)); + // } + // } + // + // public static final class Injective extends MarkerAttribute { + // private Injective() { + // super(new Key<>(Injective.class), "injective", new Visibility.User(Syntax.PRODUCTION)); + // } + // } + // + // public static final class Internal extends MarkerAttribute { + // private Internal() { + // super(new Key<>(Internal.class), "internal", new Visibility.User(Syntax.PRODUCTION)); + // } + // } + // + // public static final class Left extends MarkerAttribute { + // private Left() { + // super(new Key<>(Left.class), "left", new Visibility.User(Syntax.PRODUCTION)); + // } + // } + // + // public static final class Locations extends MarkerAttribute { + // private Locations() { + // super(new Key<>(Locations.class), "locations", new Visibility.User(Syntax.SYNTAX_SORT)); + // } + // } + // + // public static final class Macro extends MarkerAttribute { + // private Macro() { + // super(new Key<>(Macro.class), "macro", new Visibility.User(Syntax.PRODUCTION)); + // } + // } + // + // public static final class MacroRec extends MarkerAttribute { + // private MacroRec() { + // super(new Key<>(MacroRec.class), "macro-rec", new Visibility.User(Syntax.PRODUCTION)); + // } + // } + // + // public static final class Maincell extends MarkerAttribute { + // private Maincell() { + // super(new Key<>(Maincell.class), "maincell", new Visibility.User(Syntax.PRODUCTION)); + // } + // } + // + // public static final class Memo extends MarkerAttribute { + // private Memo() { + // super(new Key<>(Memo.class), "memo", new Visibility.User(Syntax.PRODUCTION)); + // } + // } + // + // public static final class MLBinder extends MarkerAttribute { + // private MLBinder() { + // super(new Key<>(MLBinder.class), "mlBinder", new Visibility.User(Syntax.PRODUCTION)); + // } + // } + // + // public static final class MLOp extends MarkerAttribute { + // private MLOp() { + // super(new Key<>(MLOp.class), "mlOp", new Visibility.User(Syntax.PRODUCTION)); + // } + // } + // + // public static final class NonAssoc extends MarkerAttribute { + // private NonAssoc() { + // super(new Key<>(NonAssoc.class), "non-assoc", new Visibility.User(Syntax.PRODUCTION)); + // } + // } + // + // public static final class NonExecutable extends MarkerAttribute { + // private NonExecutable() { + // super(new Key<>(NonExecutable.class), "non-executable", new Visibility.User(Syntax.RULE)); + // } + // } + // + // public static final class NotLR1 extends MarkerAttribute { + // private NotLR1() { + // super(new Key<>(NotLR1.class), "not-lr1", new Visibility.User(Syntax.MODULE)); + // } + // } + // + // public static final class NoEvaluators extends MarkerAttribute { + // private NoEvaluators() { + // super(new Key<>(NoEvaluators.class), "no-evaluators", new + // Visibility.User(Syntax.PRODUCTION)); + // } + // } + // + // public static final class OnePath extends MarkerAttribute { + // private OnePath() { + // super(new Key<>(OnePath.class), "one-path", new Visibility.User(Syntax.CLAIM, + // Syntax.MODULE)); + // } + // } + // + // public static final class Owise extends MarkerAttribute { + // private Owise() { + // super(new Key<>(Owise.class), "owise", new Visibility.User(Syntax.RULE)); + // } + // } + // + // public static final class Prefer extends MarkerAttribute { + // private Prefer() { + // super(new Key<>(Prefer.class), "prefer", new Visibility.User(Syntax.PRODUCTION)); + // } + // } + // + // public static final class PreservesDefinedness extends MarkerAttribute { + // private PreservesDefinedness() { + // super( + // new Key<>(PreservesDefinedness.class), + // "preserves-definedness", + // new Visibility.User(Syntax.RULE)); + // } + // } + // + // public static final class Private extends MarkerAttribute { + // private Private() { + // super( + // new Key<>(Private.class), + // "private", + // new Visibility.User(Syntax.MODULE, Syntax.PRODUCTION)); + // } + // } + // + // public static final class Public extends MarkerAttribute { + // private Public() { + // super( + // new Key<>(Public.class), "public", new Visibility.User(Syntax.MODULE, + // Syntax.PRODUCTION)); + // } + // } + // + // public static final class ReturnsUnit extends MarkerAttribute { + // private ReturnsUnit() { + // super(new Key<>(ReturnsUnit.class), "returnsUnit", new + // Visibility.User(Syntax.PRODUCTION)); + // } + // } + // + // public static final class Right extends MarkerAttribute { + // private Right() { + // super(new Key<>(Right.class), "right", new Visibility.User(Syntax.PRODUCTION)); + // } + // } + // + // public static final class SMTLemma extends MarkerAttribute { + // private SMTLemma() { + // super(new Key<>(SMTLemma.class), "smt-lemma", new Visibility.User(Syntax.RULE)); + // } + // } + // + // public static final class Token extends MarkerAttribute { + // private Token() { + // super( + // new Key<>(Token.class), + // "token", + // new Visibility.User(Syntax.SYNTAX_SORT, Syntax.PRODUCTION)); + // } + // } + // + // public static final class Total extends MarkerAttribute { + // private Total() { + // super(new Key<>(Total.class), "total", new Visibility.User(Syntax.PRODUCTION)); + // } + // } + // + // public static final class Trusted extends MarkerAttribute { + // private Trusted() { + // super(new Key<>(Trusted.class), "trusted", new Visibility.User(Syntax.CLAIM)); + // } + // } + // + // public static final class UnparseAvoid extends MarkerAttribute { + // private UnparseAvoid() { + // super(new Key<>(UnparseAvoid.class), "unparseAvoid", new + // Visibility.User(Syntax.PRODUCTION)); + // } + // } + // + // public static final class Unused extends MarkerAttribute { + // private Unused() { + // super(new Key<>(Unused.class), "unused", new Visibility.User(Syntax.PRODUCTION)); + // } + // } + // + // public static final class Anonymous extends MarkerAttribute { + // private Anonymous() { + // super(new Key<>(Anonymous.class), "anonymous", new Visibility.Internal()); + // } + // } + // + // public static final class BracketLabel extends MarkerAttribute { + // private BracketLabel() { + // super(new Key<>(BracketLabel.class), "bracketLabel", new Visibility.Internal()); + // } + // } + // + // public static final class CellFragment extends MarkerAttribute { + // private CellFragment() { + // super(new Key<>(CellFragment.class), "cellFragment", new Visibility.Internal()); + // } + // } + // + // public static final class CellOptAbsent extends MarkerAttribute { + // private CellOptAbsent() { + // super(new Key<>(CellOptAbsent.class), "cellOptAbsent", new Visibility.Internal()); + // } + // } + // + // public static final class CellSort extends MarkerAttribute { + // private CellSort() { + // super(new Key<>(CellSort.class), "cellSort", new Visibility.Internal()); + // } + // } + // + // public static final class Concat extends MarkerAttribute { + // private Concat() { + // super(new Key<>(Concat.class), "concat", new Visibility.Internal()); + // } + // } + // + // public static final class ContentStartColumn extends MarkerAttribute { + // private ContentStartColumn() { + // super(new Key<>(ContentStartColumn.class), "contentStartColumn", new + // Visibility.Internal()); + // } + // } + // + // public static final class ContentStartLine extends MarkerAttribute { + // private ContentStartLine() { + // super(new Key<>(ContentStartLine.class), "contentStartLine", new Visibility.Internal()); + // } + // } + // + // public static final class CoolLike extends MarkerAttribute { + // private CoolLike() { + // super(new Key<>(CoolLike.class), "cool-like", new Visibility.Internal()); + // } + // } + // + // public static final class Denormal extends MarkerAttribute { + // private Denormal() { + // super(new Key<>(Denormal.class), "denormal", new Visibility.Internal()); + // } + // } + // + // public static final class Digest extends MarkerAttribute { + // private Digest() { + // super(new Key<>(Digest.class), "digest", new Visibility.Internal()); + // } + // } + // + // public static final class DummyCell extends MarkerAttribute { + // private DummyCell() { + // super(new Key<>(DummyCell.class), "dummy_cell", new Visibility.Internal()); + // } + // } + // + // public static final class FilterElement extends MarkerAttribute { + // private FilterElement() { + // super(new Key<>(FilterElement.class), "filterElement", new Visibility.Internal()); + // } + // } + // + // public static final class Fresh extends MarkerAttribute { + // private Fresh() { + // super(new Key<>(Fresh.class), "fresh", new Visibility.Internal()); + // } + // } + // + // public static final class HasDomainValues extends MarkerAttribute { + // private HasDomainValues() { + // super(new Key<>(HasDomainValues.class), "hasDomainValues", new Visibility.Internal()); + // } + // } + // + // public static final class LeftInternal extends MarkerAttribute { + // private LeftInternal() { + // super(new Key<>(LeftInternal.class), "left", new Visibility.Internal()); + // } + // } + // + // public static final class Nat extends MarkerAttribute { + // private Nat() { + // super(new Key<>(Nat.class), "nat", new Visibility.Internal()); + // } + // } + // + // public static final class NotInjection extends MarkerAttribute { + // private NotInjection() { + // super(new Key<>(NotInjection.class), "notInjection", new Visibility.Internal()); + // } + // } + // + // public static final class NotLR1Modules extends MarkerAttribute { + // private NotLR1Modules() { + // super(new Key<>(NotLR1Modules.class), "not-lr1-modules", new Visibility.Internal()); + // } + // } + // + // public static final class OriginalPrd extends MarkerAttribute { + // private OriginalPrd() { + // super(new Key<>(OriginalPrd.class), "originalPrd", new Visibility.Internal()); + // } + // } + // + // public static final class Overload extends MarkerAttribute { + // private Overload() { + // super(new Key<>(Overload.class), "overload", new Visibility.Internal()); + // } + // } + // + // public static final class Predicate extends MarkerAttribute { + // private Predicate() { + // super(new Key<>(Predicate.class), "predicate", new Visibility.Internal()); + // } + // } + // + // public static final class PrettyPrintWithSortAnnotation + // extends MarkerAttribute { + // private PrettyPrintWithSortAnnotation() { + // super( + // new Key<>(PrettyPrintWithSortAnnotation.class), + // "prettyPrintWithSortAnnotation", + // new Visibility.Internal()); + // } + // } + // + // public static final class Priorities extends MarkerAttribute { + // private Priorities() { + // super(new Key<>(Priorities.class), "priorities", new Visibility.Internal()); + // } + // } + // + // public static final class Projection extends MarkerAttribute { + // private Projection() { + // super(new Key<>(Projection.class), "projection", new Visibility.Internal()); + // } + // } + // + // public static final class RecordPrd extends MarkerAttribute { + // private RecordPrd() { + // super(new Key<>(RecordPrd.class), "recordPrd", new Visibility.Internal()); + // } + // } + // + // public static final class RecordPrdZero extends MarkerAttribute { + // private RecordPrdZero() { + // super(new Key<>(RecordPrdZero.class), "recordPrd-zero", new Visibility.Internal()); + // } + // } + // + // public static final class RecordPrdOne extends MarkerAttribute { + // private RecordPrdOne() { + // super(new Key<>(RecordPrdOne.class), "recordPrd-one", new Visibility.Internal()); + // } + // } + // + // public static final class RecordPrdMain extends MarkerAttribute { + // private RecordPrdMain() { + // super(new Key<>(RecordPrdMain.class), "recordPrd-main", new Visibility.Internal()); + // } + // } + // + // public static final class RecordPrdEmpty extends MarkerAttribute { + // private RecordPrdEmpty() { + // super(new Key<>(RecordPrdEmpty.class), "recordPrd-empty", new Visibility.Internal()); + // } + // } + // + // public static final class RecordPrdSubsort extends MarkerAttribute { + // private RecordPrdSubsort() { + // super(new Key<>(RecordPrdSubsort.class), "recordPrd-subsort", new Visibility.Internal()); + // } + // } + // + // public static final class RecordPrdRepeat extends MarkerAttribute { + // private RecordPrdRepeat() { + // super(new Key<>(RecordPrdRepeat.class), "recordPrd-repeat", new Visibility.Internal()); + // } + // } + // + // public static final class RecordPrdItem extends MarkerAttribute { + // private RecordPrdItem() { + // super(new Key<>(RecordPrdItem.class), "recordPrd-item", new Visibility.Internal()); + // } + // } + // + // public static final class Refreshed extends MarkerAttribute { + // private Refreshed() { + // super(new Key<>(Refreshed.class), "refreshed", new Visibility.Internal()); + // } + // } + // + // public static final class RightInternal extends MarkerAttribute { + // private RightInternal() { + // super(new Key<>(RightInternal.class), "right", new Visibility.Internal()); + // } + // } + // + // public static final class SMTPrelude extends MarkerAttribute { + // private SMTPrelude() { + // super(new Key<>(SMTPrelude.class), "smt-prelude", new Visibility.Internal()); + // } + // } + // + // public static final class SortParams extends MarkerAttribute { + // private SortParams() { + // super(new Key<>(SortParams.class), "sortParams", new Visibility.Internal()); + // } + // } + // + // public static final class SyntaxModule extends MarkerAttribute { + // private SyntaxModule() { + // super(new Key<>(SyntaxModule.class), "syntaxModule", new Visibility.Internal()); + // } + // } + // + // public static final class TemporaryCellSortDecl extends MarkerAttribute + // { + // private TemporaryCellSortDecl() { + // super( + // new Key<>(TemporaryCellSortDecl.class), + // "temporary-cell-sort-decl", + // new Visibility.Internal()); + // } + // } + // + // public static final class UserList extends MarkerAttribute { + // private UserList() { + // super(new Key<>(UserList.class), "userList", new Visibility.Internal()); + // } + // } + // + // public static final class UserListTerminator extends MarkerAttribute { + // private UserListTerminator() { + // super(new Key<>(UserListTerminator.class), "userListTerminator", new + // Visibility.Internal()); + // } + // } + // + // public static final class WithConfig extends MarkerAttribute { + // private WithConfig() { + // super(new Key<>(WithConfig.class), "withConfig", new Visibility.Internal()); + // } + // } +} From 20549491e9cb17a0cec2d25049f669cb514d8ca6 Mon Sep 17 00:00:00 2001 From: Scott Guest Date: Fri, 23 Feb 2024 15:35:44 -0500 Subject: [PATCH 5/5] Formatting --- kore/src/main/scala/org/kframework/attributes/Att.scala | 1 - 1 file changed, 1 deletion(-) diff --git a/kore/src/main/scala/org/kframework/attributes/Att.scala b/kore/src/main/scala/org/kframework/attributes/Att.scala index 6238f3d4b15..c5b7e940b2c 100644 --- a/kore/src/main/scala/org/kframework/attributes/Att.scala +++ b/kore/src/main/scala/org/kframework/attributes/Att.scala @@ -307,7 +307,6 @@ object Att { final val KLABEL = Key.builtin("klabel", KeyParameter.Required, onlyon[Production], KeyRange.WholePipeline) final val TERMINATOR_KLABEL = - Key.builtin( "terminator-klabel", KeyParameter.Required,