Make KAST preprocessing pipeline explicit in `_module_to_kore` #1022

tothtamas28 · 2024-03-25T14:53:25Z

Define class KompilerPass
Implement KAST preprocessing steps in terms of KompilerPass
Refactor simplified_module to use a Sequence[KompilerPass]

ehildenb · 2024-03-25T22:03:54Z

LGTM. I see that it seems the only non-SingleModulePass are AddAnywhereAtt and AddPrioritiesAtt? The anywhere attribute one could likely be solved by requiring the user to add it to the symbol that is an anywhere symbol, similar to how we do macro or alias, perhaps? But maybe that's not always possible with the uses of that attribute, which we'd have to audit.

tothtamas28 · 2024-03-26T08:58:13Z

The anywhere attribute one could likely be solved

Opened an issue:

Audit the anywhere attribute k#4132

Baltoli

Very nice, I like this design a lot. @gtrepta worth taking a look at this when we do the Scala -> Java port for the frontend's compiler pipeline.

…meverification/pyk#1022) * Define class `KompilerPass` * Implement KAST preprocessing steps in terms of `KompilerPass` * Refactor `simplified_module` to use a `Sequence[KompilerPass]` --------- Co-authored-by: devops <devops@runtimeverification.com>

tothtamas28 self-assigned this Mar 25, 2024

tothtamas28 marked this pull request as ready for review March 25, 2024 15:16

tothtamas28 requested review from Baltoli and ehildenb March 25, 2024 15:16

ehildenb approved these changes Mar 25, 2024

View reviewed changes

tothtamas28 mentioned this pull request Mar 26, 2024

Audit the anywhere attribute runtimeverification/k#4132

Open

tothtamas28 added 17 commits March 26, 2024 10:13

Replace _flatten_definition by FlattenDefinition

6f876a6

Replace _add_syntax_sorts to AddSyntaxSorts

40b42ba

Replace _add_collection_atts by AddCollectionAtts

5f230c0

Replace _add_domain_value_atts by AddDomainValueAtts

3738f80

Replace _pull_up_rewrites by PullUpRewrites

8a60c28

Replace _discard_symbol_atts by DiscardSymbolAtts

3f20781

Replace _discard_hook_atts by DiscardHookAtts

b2ab6ad

Replace _add_anywhere_atts by AddAnywhereAtts

0dd72ff

Replace _add_symbol_atts by AttSymbolAtts

c00e377

Replace _add_default_format_atts by AddDefaultFormatAtts

5251361

Replace _discard_format_atts by DiscardFormatAtts

128420c

Replace _inline_terminals_in_format_atts by InlineFormatTerminals

64876dd

Replace _add_color_atts by AddColorAtts

e093f10

Replace _add_terminal_atts by AddTerminalAtts

5e6bcfe

Replace _add_priorities_atts by AddPrioritiesAtts

3888ccc

Replace _add_assoc_atts by AddAssocAtts

29c9bc2

Extract pipeline

5554376

tothtamas28 force-pushed the refactor-module-to-kore branch from 510e455 to 5554376 Compare March 26, 2024 10:13

tothtamas28 and others added 2 commits March 26, 2024 10:13

Merge 5554376 into 7c4f531

994b3e7

Set Version: 0.1.739

278001d

tothtamas28 added the automerge label Mar 26, 2024

Baltoli approved these changes Mar 26, 2024

View reviewed changes

rv-jenkins merged commit d4c29fa into master Mar 26, 2024
12 checks passed

rv-jenkins deleted the refactor-module-to-kore branch March 26, 2024 10:43

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Make KAST preprocessing pipeline explicit in `_module_to_kore` #1022

Make KAST preprocessing pipeline explicit in `_module_to_kore` #1022

tothtamas28 commented Mar 25, 2024 •

edited

ehildenb commented Mar 25, 2024

tothtamas28 commented Mar 26, 2024

Baltoli left a comment

Make KAST preprocessing pipeline explicit in _module_to_kore #1022

Make KAST preprocessing pipeline explicit in _module_to_kore #1022

Conversation

tothtamas28 commented Mar 25, 2024 • edited

ehildenb commented Mar 25, 2024

tothtamas28 commented Mar 26, 2024

Baltoli left a comment

Choose a reason for hiding this comment

Make KAST preprocessing pipeline explicit in `_module_to_kore` #1022

Make KAST preprocessing pipeline explicit in `_module_to_kore` #1022

tothtamas28 commented Mar 25, 2024 •

edited