Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Fixes and improvements in module_to_kore #4704

Merged
merged 11 commits into from
Dec 10, 2024
Merged

Fixes and improvements in module_to_kore #4704

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
11 commits
Select commit Hold shift + click to select a range
a8f743c
Enable checking non-rule axioms in `test_module_to_kore`
tothtamas28 Dec 4, 2024
f248a18
Fix operand order in test assertions
tothtamas28 Dec 6, 2024
d8bd89b
Fix `assoc` axiom generation
tothtamas28 Dec 4, 2024
a691298
Fix no-confusion axiom generation
tothtamas28 Dec 5, 2024
71779fb
Add support for the `impure` attribute
tothtamas28 Dec 5, 2024
2e55d28
Fix bug in collection attribute generation
tothtamas28 Dec 6, 2024
1e38bf9
Fix sort declaration generation
tothtamas28 Dec 6, 2024
de26f38
Filter out some attributes
tothtamas28 Dec 6, 2024
6f31b2c
Add `TIMER` to hook namespaces
tothtamas28 Dec 9, 2024
1c0c276
Fix no-junk axiom generation
tothtamas28 Dec 9, 2024
cea2b66
Optimize
tothtamas28 Dec 9, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
7 changes: 7 additions & 0 deletions pyk/src/pyk/kast/att.py
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand All @@ -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)
Expand All @@ -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)
Expand All @@ -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)
Expand All @@ -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)
Expand Down
Loading
Loading