Remove Atts.KLABEL (#4506)

Related:
* #4045
* runtimeverification/kontrol#679

Changes:
* Remove `Atts.KLABEL`
* Make `Atts.SYMBOL` unary

pyk/src/pyk/kast/att.py

@@ -319,7 +319,6 @@ class Atts:
     INDEX: Final = AttKey('index', type=_INT)
     INITIALIZER: Final = AttKey('initializer', type=_NONE)
     INJECTIVE: Final = AttKey('injective', type=_NONE)
-    KLABEL: Final = AttKey('klabel', type=_ANY)
     LABEL: Final = AttKey('label', type=_ANY)
     LEFT: Final = AttKey('left', type=_ANY)  # LEFT and LEFT_INTERNAL on the Frontend
     LOCATION: Final = AttKey('org.kframework.attributes.Location', type=_LOCATION)
@@ -341,7 +340,7 @@ class Atts:
     SORT: Final = AttKey('org.kframework.kore.Sort', type=_ANY)
     SOURCE: Final = AttKey('org.kframework.attributes.Source', type=_PATH)
     STRICT: Final = AttKey('strict', type=_ANY)
-    SYMBOL: Final = AttKey('symbol', type=OptionalType(_STR))
+    SYMBOL: Final = AttKey('symbol', type=_STR)
     SYNTAX_MODULE: Final = AttKey('syntaxModule', type=_STR)
     TERMINALS: Final = AttKey('terminals', type=_STR)
     TOKEN: Final = AttKey('token', type=_NONE)

pyk/src/pyk/kast/pretty.py

@@ -217,8 +217,6 @@ def _print_knonterminal(self, knonterminal: KNonTerminal) -> str:
         return self.print(knonterminal.sort)
 
     def _print_kproduction(self, kproduction: KProduction) -> str:
-        if Atts.KLABEL not in kproduction.att and kproduction.klabel:
-            kproduction = kproduction.update_atts([Atts.KLABEL(kproduction.klabel.name)])
         syntax_str = 'syntax ' + self.print(kproduction.sort)
         if kproduction.items:
             syntax_str += ' ::= ' + ' '.join([self._print_kouter(pi) for pi in kproduction.items])
@@ -378,8 +376,8 @@ def build_symbol_table(
             unparser = unparser_for_production(prod)
 
             symbol_table[label] = unparser
-            if Atts.SYMBOL in prod.att and Atts.KLABEL in prod.att:
-                symbol_table[prod.att[Atts.KLABEL]] = unparser
+            if Atts.SYMBOL in prod.att:
+                symbol_table[prod.att[Atts.SYMBOL]] = unparser
 
     if opinionated:
         symbol_table['#And'] = lambda c1, c2: c1 + '\n#And ' + c2

pyk/src/pyk/kore_exec_covr/__main__.py

@@ -66,8 +66,8 @@ def do_analyze(definition_dir: Path, input_file: Path) -> None:
     print('=================================')
     for location_str, hits in applied_simplifications.items():
         rule_label_str = ''
-        if location_str in rule_dict and Atts.KLABEL in rule_dict[location_str].att:
-            rule_label_str = f'[{rule_dict[location_str].att[Atts.LABEL]}]'
+        if location_str in rule_dict and Atts.SYMBOL in rule_dict[location_str].att:
+            rule_label_str = f'[{rule_dict[location_str].att[Atts.SYMBOL]}]'
         if hits > 0:
             print(f'    {hits} applications of rule {rule_label_str} defined at {location_str}')
     total_simplifications = sum([v for v in applied_simplifications.values() if v > 0])

pyk/src/tests/unit/kast/test_att.py

@@ -17,9 +17,9 @@
     ('empty', (), ''),
     ('nullary', (Atts.FUNCTION(None),), '[function]'),
     ('two-nullaries', (Atts.FUNCTION(None), Atts.TOTAL(None)), '[function, total]'),
-    ('opt-none', (Atts.SYMBOL(None),), '[symbol]'),
-    ('opt-some-empty-str', (Atts.SYMBOL(''),), '[symbol("")]'),
-    ('opt-some-nonempty-str', (Atts.SYMBOL('foo'),), '[symbol("foo")]'),
+    ('opt-none', (Atts.CONCRETE(None),), '[concrete]'),
+    ('opt-some-empty-str', (Atts.CONCRETE(''),), '[concrete("")]'),
+    ('opt-some-nonempty-str', (Atts.CONCRETE('foo'),), '[concrete("foo")]'),
     ('multiple', (Atts.SYMBOL('foo'), Atts.FUNCTION(None), Atts.TOTAL(None)), '[symbol("foo"), function, total]'),
 )