Fixes and improvements in module_to_kore
#4704
Conversation
Oveloads that are otherwise constructors also require `constructor` axioms.
| res: list[Axiom] = [] | ||
| for sentence in module.sentences: | ||
| if not isinstance(sentence, KProduction): | ||
| for prod in module.productions: | ||
| if not prod.klabel: | ||
| continue | ||
| if not sentence.klabel: | ||
| if prod.klabel.name in BUILTIN_LABELS: | ||
| continue | ||
| if sentence.klabel.name in BUILTIN_LABELS: | ||
| if not Atts.FUNCTIONAL in prod.att: | ||
| continue | ||
| if not Atts.FUNCTIONAL in sentence.att: | ||
| continue | ||
| res.append(functional_axiom(sentence)) | ||
| res.append(functional_axiom(prod)) | ||
| return res |
There was a problem hiding this comment.
There is a clear pattern of repeated code here:
- for each production
prodin the module- if not
prod.klabel: skip - if
prod.klabel.name in BUILTIN_LABELS: skip - if
TARGET in prod.att: callTARGET_axiom(some instances have different criteria, sometimes several ones)
- if not
Since each productions should be part of exactly one group with a certain criterion, would it make sense to iterate over all productions just once, to classify them into TARGET groups and and dispatch to each TARGET_axiom in just one place?
(That place would be https://github.com/runtimeverification/k/pull/4704/files#diff-0e99d64ff2ae75d6aa4d5eb3c1822e330e1f2d1f8b69fb19bbb399e5780e2591R107-R119 )
| class AddImpureAtts(SingleModulePass): | ||
| """Add the `impure` attribute to all function symbol productions whose definition transitively contains `impure`.""" |
There was a problem hiding this comment.
While reading through this the question arose in my head whether this is really a "single-module" property.
Maybe it is only single-module because the compiler is smashing all user code into a single module? Because if imports are admitted one could easily import an impure "function" from a different module and call it on the RHS of a rule, or not?
There was a problem hiding this comment.
Yes, this is not single module in that sense. The name is probably misleading, but SingleModulePass means that it transforms a definition with a single module into another definition with a single module.
| @@ -1063,6 +1196,7 @@ class DiscardHookAtts(SingleModulePass): | |||
| 'SET', | |||
| 'STRING', | |||
| 'SUBSTITUTION', | |||
| 'TIMER', | |||
| 'UNIFICATION', | |||
| ) | |||
|
|
|||
There was a problem hiding this comment.
At ~1300 lines for this file, maybe worth refactoring into separate modules...
What comes to mind is a split into compiler passes and final axiom rendering.
tothtamas28
changed the title
module_to_koremodule_to_kore
|
I opened an issue for the refactorings: #4707 |
impureattribute