Make KAST preprocessing pipeline explicit in `_module_to_kore`

runtimeverification / pyk

Python tools for the K Framework

BSD 3-Clause "New" or "Revised" License

13 stars 2 forks source link

Make KAST preprocessing pipeline explicit in `_module_to_kore` #1022

Closed tothtamas28 closed 5 months ago

tothtamas28 commented 5 months ago

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

ehildenb commented 5 months ago

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 commented 5 months ago

The anywhere attribute one could likely be solved

Opened an issue:

runtimeverification/k#4132