# CleanWhile
Clean While tools

This module provides types and tools to work with [While][while] in
[Clean][clean].

Typically you will need `:: Stm`, `:: State` and `eval`. A `Stm` is a statement
in the While language. Only `;` couldn't be implemented as-is, because it is
reserved in Clean. The statement composition operator is now `:.`.

For example, the 
[following program](http://www.cs.ru.nl/~hubbers/courses/sc/leertaak/04.html)
is a rounded down square root function (if `x=n` at the start and `n` is a
natural number, then `z` is the square root of `n`, rounded down, after
execution):

    sqrt :: Stm
    sqrt = 'z' := 0 :.
           'o' := 1 :.
           's' := 1 :.
           While ('s' <= 'x')
             ( 'z' := 'z' + 1 :.
               'o' := 'o' + 2 :.
               's' := 's' + 'o' )

We can now execute this code on a `State`, which maps `Var` (`Char`) to `Int`:

    Start :: Int
    Start = eval NS sqrt st 'z'
    where
        st :: Var -> Int
        st 'x' = 36

`eval NS sqrt st` is a `State` itself (the state that results from execution of
`sqrt` in `st`), so we apply that to `z` to get the result. Other than the
[documentation of While][while] suggests, a `State` can be a partial function
here. There is no efficient way of enforcing total functions in Clean.

The `NS` argument tells the module to use Natural Semantics (as opposed to
`SOS`, Structural Operational Semantics). The result should be the same (though
this has not been heavily tested, it has been proven for the derivation rules
that define NS and SOS, and the functions in this module are directly derived
from those rules). These two semantics are defined for While by Nielson and
Nielson in [Semantics with Applications: A Formal Introduction][wiley].

Besides evaluating statements, we can also construct derivation trees and
sequences. The following two Start rules generate a derivation tree for Natural
Semantics and a derivation sequence for Structural Operational Semantics. Both
types can be `toString`ed:

    Start = tree sqrt st
    Start = seq sqrt st

For example, the tree for `sqrt` in `st` with `st x = 9`:

    (z:=0; o:=1; s:=1; while s<=x do z:=z+1; o:=o+2; s:=s+o done
      z:=0
      (o:=1; s:=1; while s<=x do z:=z+1; o:=o+2; s:=s+o done
        o:=1
        (s:=1; while s<=x do z:=z+1; o:=o+2; s:=s+o done
          s:=1
          (while s<=x do z:=z+1; o:=o+2; s:=s+o done
            (z:=z+1; o:=o+2; s:=s+o
              z:=z+1
              (o:=o+2; s:=s+o
                o:=o+2
                s:=s+o
              )
            )
            (while s<=x do z:=z+1; o:=o+2; s:=s+o done
              (z:=z+1; o:=o+2; s:=s+o
                z:=z+1
                (o:=o+2; s:=s+o
                  o:=o+2
                  s:=s+o
                )
              )
              (while s<=x do z:=z+1; o:=o+2; s:=s+o done
                (z:=z+1; o:=o+2; s:=s+o
                  z:=z+1
                  (o:=o+2; s:=s+o
                    o:=o+2
                    s:=s+o
                  )
                )
                while s<=x do z:=z+1; o:=o+2; s:=s+o done
              )
            )
          )
        )
      )
    )

And the sequence:

    z:=0; o:=1; s:=1; while s<=x do z:=z+1; o:=o+2; s:=s+o done
    o:=1; s:=1; while s<=x do z:=z+1; o:=o+2; s:=s+o done
    s:=1; while s<=x do z:=z+1; o:=o+2; s:=s+o done
    while s<=x do z:=z+1; o:=o+2; s:=s+o done
    if s<=x then z:=z+1; o:=o+2; s:=s+o; while s<=x do z:=z+1; o:=o+2; s:=s+o done else skip
    z:=z+1; o:=o+2; s:=s+o; while s<=x do z:=z+1; o:=o+2; s:=s+o done
    o:=o+2; s:=s+o; while s<=x do z:=z+1; o:=o+2; s:=s+o done
    s:=s+o; while s<=x do z:=z+1; o:=o+2; s:=s+o done
    while s<=x do z:=z+1; o:=o+2; s:=s+o done
    if s<=x then z:=z+1; o:=o+2; s:=s+o; while s<=x do z:=z+1; o:=o+2; s:=s+o done else skip
    z:=z+1; o:=o+2; s:=s+o; while s<=x do z:=z+1; o:=o+2; s:=s+o done
    o:=o+2; s:=s+o; while s<=x do z:=z+1; o:=o+2; s:=s+o done
    s:=s+o; while s<=x do z:=z+1; o:=o+2; s:=s+o done
    while s<=x do z:=z+1; o:=o+2; s:=s+o done
    if s<=x then z:=z+1; o:=o+2; s:=s+o; while s<=x do z:=z+1; o:=o+2; s:=s+o done else skip
    z:=z+1; o:=o+2; s:=s+o; while s<=x do z:=z+1; o:=o+2; s:=s+o done
    o:=o+2; s:=s+o; while s<=x do z:=z+1; o:=o+2; s:=s+o done
    s:=s+o; while s<=x do z:=z+1; o:=o+2; s:=s+o done
    while s<=x do z:=z+1; o:=o+2; s:=s+o done
    if s<=x then z:=z+1; o:=o+2; s:=s+o; while s<=x do z:=z+1; o:=o+2; s:=s+o done else skip
    skip

As you can see, neither method outputs the states. Since a `State` is actually
a function (and not a `[(Var, Int)]`, for example), it is impossible to
`toString` a `State` *an sich*. It *may* be possible to `toString` states in
the context of a derivation tree or sequence, by looking for the variables
present or modified. This is something for a next version.

## Warning

This breaks `StdEnv` completely. Only import what you need, as always, and use
qualified imports where needed.

## Todo

 - Gast testing
 - More boolean operators for testing integers besides `=` and `<=`
 - Prettyprint for `DerivTree`
 - Parser
 - Add the state to the `toString` of `DerivTree` and `DerivSeq`

## Copyright &amp; license
Copyright &copy; 2016 Camil Staps. Licensed under MIT, see LICENSE.

[while]: http://profs.sci.univr.it/~merro/files/WhileExtra_l.pdf
[clean]: http://clean.cs.ru.nl/Clean
[wiley]: http://cs.ioc.ee/~tarmo/pls06/wiley.ps.gz