Readme: features, headings

1 files changed, 20 insertions, 11 deletions

diff --git a/README.md b/README.md
index c91aa82..0619e88 100644
--- a/README.md
+++ b/README.md
@@ -2,17 +2,20 @@
 Clean While tools
 
 This module provides types and tools to work with [While][while] in
-[Clean][clean].
+[Clean][clean]. Features include:
 
-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 `:.`.
+ - 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]
 
-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):
+## 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):
 
     sqrt :: Stm
     sqrt = 'z' := 0 :.
@@ -23,6 +26,7 @@ execution):
                'o' := 'o' + 2 :.
                's' := 's' + 'o' )
 
+### Evaluation
 We can now execute this code on a `State`, which maps `Var` (`Char`) to `Int`:
 
     Start :: Int
@@ -43,6 +47,7 @@ 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
@@ -51,7 +56,8 @@ 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`:
+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
@@ -129,10 +135,12 @@ qualified imports where needed.
 ## Todo
 
  - Gast testing
- - More boolean operators for testing integers besides `=` and `<=`
+ - More boolean operators for testing integers besides `==` and `<=`
+ - Can boolean operators be made functions rather than type constructors?
  - 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.
@@ -140,4 +148,5 @@ 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