1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
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 & license
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
|
