Program transformation solution attempts

Example language

syntax Exp ::= "x" | "y" | "z" | Exp "*" Exp

rule [s] x => z

all

Applies s to all t's subterms, and succeeds if all subterms succeed.

s(x * x) => z * z
s(x * y) => x * y

It could be seen as a generalization of k's strict. It applies s to all children and succeeds if s succeeds for all of them. strict could be seen as doing the same thing, where "succeeds" means isResult.

This brings forward a more interesting discussion:

Could we make a parallel between "stuck" and "failed". Could we see a computation that is stuck with something atop the k cell as a computation that failed. Inversely, could we encode strategy failure as "stuck" with something atop the "monitor" (or different cell)?

##Deprecated discussion

Something along the lines of the following (partial) implementation for all:

rule <k> T(C1 R) => C1 ~> T(HOLE(C1) R) </k> <s> all(S) => S ~> all(S) ...</s>
rule STUCK <k> _ ~> T(HOLE(C1) R) => T(C1 R) </k> <s> S ~> all(S) => false ...</s>
rule <k> T(R) </k> <s> S ~> all(S) => true</s> if isResult(R)

Assuming T is AC.

A problem with this approach is that if S has side effects, they will not be rolled back on failure. Whether this is a good thing or not is an open discussion.

Solution attempt 1

Now, slowly through the operators:

Assuming that when no rule can be applied, the engine adds a cell <blocked/>. We also have the rule:

rule <blocked/> <s> X => false ...</s>

<*

rule <s> A <* B => A ~> HOLE <* B ...</s> <k> X => X ~> SNAPSHOT(X) ... </k>
rule <s> true <* B => B ...</s>
rule <s> false <* B => false ...</s>
rule <s> true ~> HOLE <* B => true <* B ...</s> <k> X ~> SNAPSHOT(_) => X ...</k>
rule <s> false ~> HOLE <* B => true <* B ...</s> <k> _ ~> SNAPSHOT(X) => X ...</k>

<+

rule <s> A <+ B => A ~> HOLE <+ B ...</s>
rule <s> false <+ B => B ...</s>
rule <s> true <+ B => true ...</s>
rule <s> true ~> HOLE <+ B => true <* B ...</s> <k> X ~> SNAPSHOT(_) => X ...</k>
rule <s> false ~> HOLE <+ B => true <* B ...</s> <k> _ ~> SNAPSHOT(X) => X ...</k>

child

rule <s> child(A) => A ~> child(HOLE) ...</s> <k> O(X) => X ~> O(HOLE(X)) ...</k>
rule <s> true ~> child(HOLE) => true ...</s> <k> X ~> O(HOLE(_)) => O(XRes) ...</k>
rule <s> false ~> child(HOLE) => false ...</s> <k> _ ~> O(HOLE(X)) => O(X) ...</k>

Solution attempt 2

The ideea is to have the strategy expression "evaluated" like any other expression in a language. The strategy expression to evaluate lives in the <s> cell, which is a k-like cell with some special heating/cooling rules.

<blocked/>

We get rid of the else on rules and replace it with a very simple <blocked/> marker which works as following:

When the computation cannot proceed anymore, a <blocked/> marker cell is added.

The following rules interprets the <blocked/> marker in the context of the strategy language:

rule <blocked/> <s> E => false ...</s>

I exemplify this for a strategy language where true means the strategy succeeded, and false means it failed. We could have other encoding if we wanted to.

Builtin cooling rules

rule <s> true ~> S => S[true/HOLE] ...</s> <k> X ~> E => E[X/HOLE(_)] </k>
rule <s> false ~> S => S[false/HOLE] ...</s> <k> _ ~> E => E[X/HOLE(X)] </k>

Notice that the HOLE now saves the current state of the expression.

Also, the heating cooling rules are generic and assume a E[X/HOLE(X)] replacement which I don't think k currently supports. We can overcome this by either implementing this feature, or generating cooling rules for each production.

if

List in a normal programming language, if is the essential building block in the strategy language.

 rule <s> if C then A else B => C ~> if HOLE then A else B ...</s> <k> X => X ~> HOLE(X) ...</k>
 rule <s> if true then A else B => A ...</s> <k> X => X ~> HOLE(X) ...</k>
 rule <s> if false then A else B => B ...</s> <k> X => X ~> HOLE(X) ...</k>

<+

"or" with a short circuit.

rule <s> A <+ B => if A then true else B ... </s>

<*

"and" with a short circuit.

rule <s> A <* B => if A then B else false ... </s>

+

"or" without the short circuit.

rule <s> A + B => if A then true else B ...</s> rule <s> A + B => if B then true else A ...</s>

strict

An attempt to express the strictness annotation in our strategy language.

Yhe rule which is a bit stranger, but should cover heating, with cooling solved by the strategy cooling (actually, we will need a special version of cooling strategies above cooling that check for isResult(E))

rule <s> A => HOLE(A) ...</s> <k> E(Y R) => Y ~> E(HOLE(Y) R) ... </k> if strict(1,E)

repeat

repeat until failure. On failure of A, return the result (i.e. the overall strategy succeeds).

rule <s> repeat(A) => if A then repeat(A) else true ...</s>

bottomup

This applies A to the entire tree, in a bottom-up postfix fashion.

This is a bit vague, but something along these lines should do it:

rule <s> bottomup(A) => bottomup(A) ~> HOLE + bottomup(A) ... </s> <k> E(S:KList A) => A ~> E(S:KList with a HOLE) ... </k>

rule <s> bottomup(A) => A ... </s> <k> E(no subterms) => E </k>

anywhere

one possible implementation is rule <s> anywhere(A) => repeat(bottomup(A)) </s>

Problems

• x[y+2] = z + 3 needs matching on two k elements

To figure out

• can I (currently) match on a variable which is a KLabel?
• can I iterate of the elements of a KList ?