Initial commit

1 files changed, 72 insertions, 0 deletions

diff --git a/README.md b/README.md
new file mode 100644
index 0000000..dc4c5e5
--- /dev/null
+++ b/README.md
@@ -0,0 +1,72 @@
+# 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
+
+## 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
+
+## 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
+