-
Notifications
You must be signed in to change notification settings - Fork 61
Program Transformation notes
Notes on what it takes to do program transformation using K. For now this is just a scratchpad. I (Cosmin) will bug you for feedback on various parts from time to time.
Refactoring a program means swapping the state exploration behavior between computational and structural rules. Computational rules should behave like equations, reducing the program whenever possible. Structural rules help us explore the space of equivalent programs, so they should be run in a model-checking mode, as rules.
Can K currently do rewriting modulo (any) equations?
Can K currently do matching modulo ACI? Can it do it on arbitrary operations?
When searching, we need the ability to generate multiple new states from applying rules on partially-heated terms. Furthermore, from each intermediate heating state, it should be possible to generate multiple new terms by applying different rules.
Issue #80 has a discussion related to this.
This is a tricky one. But essential.
Given an expression E I want to find any F and a G such that E = F \compose G.
Actually, not any, but a maximal one given a cost function c on F or G.
I approximate this now by finding the largest continuous subexpression of E that does not break name bindings, i.e. I don't select terms with variable which are bound within the outer expression.
It would be nice to have a more general solution.
Still, even the rough approximation above is not implementable in K now. It seems it would need the ability to match using a pattern defined as a recursive function.
Maybe it could be defined now by brute force enumeration of subexpressions, but it would be terribly inefficient considering that, for my case at least, the cost function c is monotonous with respect to the subexpression relation.
This is another discussion, which may also include nested rewrite rules.
This is nice-to-have optimization that is not present in the kiama-based system.
I don't know if "combinatorial" is the right word to describe it but here is what I'm thinking.
Consider the following expression: f + g, with a strict +.
Let's say that we have the rules:
f => f1, f => f2, g => g1, all transitions. We thus have 6 possible reachable states, excluding the initial one.
If the strict is implemented left to right, we need to apply g => g1 three times on the same g (for f + g, f1 + g, and f2 + g).
It may not seem like much on this small example, but it adds up.
Also, the six states are considered distinct and may (depending on how states are stored) require more memory.
It would be nice to be able to have distinct states for just part of the expression. This would save us from repeatedly applying the same rule on the same term. If somebody needs to enumerate the states, they can then be put together. Of course, there needs to be a mechanism that puts resulting expressions together when a rule may only match this way.
I would like the ability to piggyback information on a term.
E.g., when beta-reducing (/\ funkyName . bla(funkyName)) (x + y), it would be nice to attach to the x + y in bla(x + y) a bit of meta-information that says its original name was funkyName.
This is needed because many of the program transformation rules I have work best if they are applied to a beta-reduced term. On the other hand, when generating the final code, it is often necessary to reverse some of the beta-reduction (extract variable), both for performance and for readability.
In the current system, I didn't have time to implement this, and I simply give them ugly new names.
This cannot be implemented easing using a separate term -> name map because we also need context for those terms -- not every x + y in the program should be named funkyName. The meta-information needs to be somehow attached the the term.