Fixes and improvements in module_to_kore (#4704)

* Enable checking of non-rule axioms in the test
* Fix assoc, no-junk and no-confusion axiom generation
* Fix sort generation
* Fix a bug in collection attribute generation
* Add support for the `impure` attribute
* Filter out some internal attributes

Author: tothtamas28

pyk/src/pyk/kast/att.py

@@ -290,6 +290,7 @@ class Atts:
     ALIAS_REC: Final = AttKey('alias-rec', type=_NONE)
     ANYWHERE: Final = AttKey('anywhere', type=_NONE)
     ASSOC: Final = AttKey('assoc', type=_NONE)
+    AVOID: Final = AttKey('avoid', type=_NONE)
     BRACKET: Final = AttKey('bracket', type=_NONE)
     BRACKET_LABEL: Final = AttKey('bracketLabel', type=_ANY)
     CIRCULARITY: Final = AttKey('circularity', type=_NONE)
@@ -307,6 +308,7 @@ class Atts:
     DEPENDS: Final = AttKey('depends', type=_ANY)
     DIGEST: Final = AttKey('digest', type=_ANY)
     ELEMENT: Final = AttKey('element', type=_ANY)
+    EXIT: Final = AttKey('exit', type=_ANY)
     FORMAT: Final = AttKey('format', type=FormatType())
     FRESH_GENERATOR: Final = AttKey('freshGenerator', type=_NONE)
     FUNCTION: Final = AttKey('function', type=_NONE)
@@ -325,6 +327,8 @@ class Atts:
     MACRO: Final = AttKey('macro', type=_NONE)
     MACRO_REC: Final = AttKey('macro-rec', type=_NONE)
     MAINCELL: Final = AttKey('maincell', type=_NONE)
+    MULTIPLICITY: Final = AttKey('multiplicity', type=_ANY)
+    NO_EVALUATORS: Final = AttKey('no-evaluators', type=_NONE)
     OVERLOAD: Final = AttKey('overload', type=_STR)
     OWISE: Final = AttKey('owise', type=_NONE)
     PREDICATE: Final = AttKey('predicate', type=_ANY)
@@ -335,6 +339,7 @@ class Atts:
     PRODUCTION: Final = AttKey('org.kframework.definition.Production', type=_ANY)
     PROJECTION: Final = AttKey('projection', type=_NONE)
     RIGHT: Final = AttKey('right', type=_ANY)  # RIGHT and RIGHT_INTERNAL on the Frontend
+    RETURNS_UNIT: Final = AttKey('returnsUnit', type=_NONE)
     SIMPLIFICATION: Final = AttKey('simplification', type=_ANY)
     SEQSTRICT: Final = AttKey('seqstrict', type=_ANY)
     SORT: Final = AttKey('org.kframework.kore.Sort', type=_ANY)
@@ -345,9 +350,11 @@ class Atts:
     SYNTAX_MODULE: Final = AttKey('syntaxModule', type=_STR)
     SYMBOLIC: Final = AttKey('symbolic', type=OptionalType(_STR))
     TERMINALS: Final = AttKey('terminals', type=_STR)
+    TERMINATOR_SYMBOL: Final = AttKey('terminator-symbol', type=_ANY)
     TOKEN: Final = AttKey('token', type=_NONE)
     TOTAL: Final = AttKey('total', type=_NONE)
     TRUSTED: Final = AttKey('trusted', type=_NONE)
+    TYPE: Final = AttKey('type', type=_ANY)
     UNIT: Final = AttKey('unit', type=_STR)
     UNIQUE_ID: Final = AttKey('UNIQUE_ID', type=_ANY)
     UNPARSE_AVOID: Final = AttKey('unparseAvoid', type=_NONE)