From fdb5ee9fc2a5cb0dc8d27d0d9c3a6603fc85aa27 Mon Sep 17 00:00:00 2001 From: Camil Staps Date: Tue, 29 Mar 2016 22:55:32 +0200 Subject: Readme: features, headings --- README.md | 31 ++++++++++++++++++++----------- 1 file changed, 20 insertions(+), 11 deletions(-) (limited to 'README.md') 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 & license Copyright © 2016 Camil Staps. Licensed under MIT, see LICENSE. @@ -140,4 +148,5 @@ Copyright © 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 -- cgit v1.2.3