Conditional Rewrite - ku-fpg/haskino GitHub Wiki

#Conditionals Goal

Similar to the general rewrite rules described on the Rewrite steps page we would also like our compiler plug in to transform the following Haskino program which contains a Haskell conditional:

loop $ do 
    a <- digitalRead button1
    b <- digitalRead button2
    if a || b
    then do
        digitalWrite led1 a
        digitalWrite led2 b
    else do
        digitalWrite led1 (not a)
        digitalWrite led2 (not b)          
    delayMillis 1000

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

loopE $ do 
    a' <- digitalReadE (lit button1)
    b' <- digitalReadE (lit button2)
    ifThenElseE (a' ||* b')
        (do digitalWriteE (lit led1) a'
            digitalWriteE (lit led2) b')
        (do digitalWriteE (lit led1) (notB (lit a'))
            digitalWriteE (lit led2) (notB (lit b')))
    delayMillisE (lit 1000)

Conditional plugin pass

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 (b :: Bool) (m1 :: Arduino () ) (m2 :: Arduino ()).
if b then m1 else m2
  =
ifThenElseE (lit b) m1 m2

To simplify the plugin, we create a pass that actually applies the equivelent of the following rule which does a transformation to a shallow Haskino conditional.

forall (b :: Bool) (m1 :: Arduino () ) (m2 :: Arduino ()).
if b then m1 else m2
  =
ifThenElse b m1 m2

Additions to the First set of rules

Then we can apply all of the rules we used in the first set of the first example, along with one to convert the shallow conditional to a deep conditional:

forall (b :: Bool) (t :: Arduino ()) (e :: Arduino ()).
ifThenElse b t e
  =
ifThenElseE (rep b) t e

And one to push the abs from the outside of the not operation into the inside, while changing the or operation from the Bool to the Expr Bool operation.

forall (b :: Bool).
not b
  =
notB (rep b)