Rewrite Steps

#The Goal

We would like to create a compiler plug in to transform a Haskino program written with the shallow embedding into one written with a deep embedding. We will start with the following simple shallow example:

loop $ do  
    a <- digitalRead button1  
    b <- digitalRead button2  
    digitalWrite led (a || b)  

We would like to translate this into the following Deep code:

loopE $ do  
    a' <- digitalReadE (lit button1)  
    b' <- digitalReadE (lit button2)  
    digitalWriteE (lit led) (a' ||* b')  

Desugar

We start by de-sugaring the do notation:

loop $ digitalRead button1 >>= 
        \a -> digitalRead button2 >>=
            \b -> digitalWrite led (a || b)

First set of rules

The first set of transformations involves applying several GHC compiler rules. The first 3 rules transform the shallow Haskino commands and procedures into their deep versions.

Apply "loop" Rule

This is simple rule, which just changes the command:

forall (m :: Arduino ()). loop m = loopE m

After the rule application, our example is now:

loopE $ digitalRead button1 >>= 
        \a -> digitalRead button2 >>=
            \b -> digitalWrite led (a || b)

###Apply "digitalRead":

This rule also does a shallow to deep procdure substitution, but requires applying a rep to the procedure parameter to transform it into an expression, and a abs to the result of the procedure to transform it from an expression back to a literal.

forall (p :: Word8).
digitalRead p = abs <$> (digitalReadE $ rep p) 

The example then becomes:

loopE $ abs <$> digitalReadE(rep(button1)) >>=  
        (\a -> abs <$> digitalReadE(rep(button2)) >>=  
            (\b -> digitalWrite led (a || b)))  

###Apply "digitalWrite":

This rule also does a shallow to deep command substitution, but requires applying a rep to the command parameters as well, to transform them into expressions.

forall (p :: Word8) (b :: Bool).  
digitalWrite p b  
  =  
digitalWriteE (rep p) (rep b)  

The example then becomes:

loopE $ abs <$> digitalReadE(rep(button1)) >>= 
        (\a -> abs <$> digitalReadE(rep(button2)) >>=
            (\b -> digitalWriteE (rep(led)) (rep(a || b))))

###Apply "rep-push-or"

This rule pushes the rep from the outside of the or operation into the individual components, while changing the or operation from the Bool to the Expr Bool operation.

forall (b1 :: Bool) (b2 :: Bool).
rep (b1 || b2)
  =
(rep b1) ||* (rep b2)

The example then becomes:

loopE $ abs <$> digitalReadE(rep(button1)) >>= 
        (\a -> abs <$> digitalReadE(rep(button2)) >>=
            (\b -> digitalWriteE (rep(led)) ((rep(a) ||* rep(b)))))

###Apply "rep-3rd-monad":

This rule applies the 3rd monad rule to move the abs from outside to bind to being composed with the continuation.

forall (f :: Arduino (Expr Bool)) (k :: Bool -> Arduino b).
abs <$> f >>= k 
  =
f >>= k . abs

The example then becomes:

loopE $ digitalReadE(abs(button1)) >>= 
        (\a -> digitalReadE(abs(button2)) >>=
            (\b -> digitalWriteE (abs(led)) ((abs(a) ||* abs(b)))).rep).rep

Non Rule based transformations

###Apply "Parameter Change Transformation":

We would like to apply a rule like the following, but it is not possible with GHC's compiler rules. To do so, we will need to add a plugin pass to do the transformation.:

forall (f :: Arduino a).
(\x -> F[x]).abs
  =
(\x' -> let x=abs(x') in F[x])

After applying the parameter change/let transformation, the example becomes:

loopE $ digitalReadE(rep(button1)) >>= 
        (\a' -> let a=abs(a') in digitalReadE(rep(button2)) >>=
            (\b' -> let b=abs(b') in digitalWriteE (rep(led)) ((rep(a) ||* rep(b)))))

###Apply "Let Elimination":

A second transformation that cannot be done with GHC rules is to eliminate the abs, substituting abs(x') for x in the function body. This may be able to be done by the GHC simplifier pass, or it may need to be combined with the plugin pass for the transformation above.

After applying the let elimination, the example becomes:

loopE $ digitalReadE(rep(button1)) >>= 
        (\a' -> digitalReadE(rep(button2)) >>=
            (\b' -> digitalWriteE (rep(led)) ((rep(abs(a')) ||* rep(abs(b'))))))

Second set of rules

###Apply "rep-abs-fuse"

Finally, after applying the plugin based transformations, one other rule based transformation is required. It is an rep abs fuse rule which eliminates the rep abs combinations.

forall x.
rep(abs(x))
  =
x

The example then becomes the final desired deep form:

loopE $ digitalReadE(rep(button1)) >>= 
        \a' -> digitalReadE(rep(button2)) >>=
            \b' -> digitalWriteE rep(led) (a' ||* b')