# CleanWhile
Clean While tools

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

 - Types for While statements, arithmetic and boolean expressions, states,
   derivation trees and derivation sequences
 - semi-prettyprint `toString` for those types
 - Evaluating statements in states
 - Constructing derivation trees and sequences according to the rules of
   Natural and Structural Operational Semantics as defined by [Nielson &
   Nielson][wiley]

## Example: square root
For example, the [following program][sqrt] 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):

    import While
    from WhileVars import o, s, x, z // o :== Var 'o'; etc.

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

### Evaluation
We can now execute this code on a `State`, which maps `Var` to `Int`:

    Start :: Int
    Start = eval NS sqrt st z
    where
        st :: Char -> Int  // Or: st :: Var -> Int  // st :: CharState
        st 'x' = 9         //     st (Var 'x') = 9  // st = \'x' -> 9

`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].

### Constructing derivation trees and sequences
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` (when passed to
`toString`):

    (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
 - Prettyprint for `DerivTree`
 - Parser
 - Add the state to the `toString` of `DerivTree` and `DerivSeq`
 - Easy interface for While language extensions

## 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
[sqrt]:  http://www.cs.ru.nl/~hubbers/courses/sc_1516/leertaak/04.html