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

<blocked/>

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

To integrate this with rules, we have a rule that marks the blocked cell:

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

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>

if

 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> 
 rule <s> if false then A else B => B ...</s> <k> _ ~> HOLE(X) => X ~> HOLE(X) ...</k>

<+

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

<*

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

+

rule <s> A + B => A <+ B ...</s>

strict

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

repeat

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

bottomup

rule <s> bottomup(A) => A ~> bottomup(A) ... </s> <k> E(S:KList A) => A ~> E(S:KList) ... </k> to which we have to add a way of tracking that we've heated each subterm of E

To figure out

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