diff options
| -rw-r--r-- | README.md | 71 | ||||
| -rw-r--r-- | While.icl | 4 | ||||
| -rw-r--r-- | test.icl | 3 |
3 files changed, 75 insertions, 3 deletions
@@ -51,6 +51,76 @@ 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`: + + (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 @@ -62,6 +132,7 @@ qualified imports where needed. - More boolean operators for testing integers besides `=` and `<=` - Prettyprint for `DerivTree` - Parser + - Add the state to the `toString` of `DerivTree` and `DerivSeq` ## Copyright & license Copyright © 2016 Camil Staps. Licensed under MIT, see LICENSE. @@ -53,8 +53,8 @@ dTree stm st ts r = {stm=stm, state=st, children=ts, result=r} // Structural Operational Semantics seq :: Stm State -> DerivSeq -seq stm st = case step stm st of (Done st) = [Done st] - (NDone stm st) = [NDone stm st : seq stm st] +seq stm st = case step stm st of (Done st`) = [NDone stm st, Done st`] + (NDone stm` st`) = [NDone stm st:seq stm` st`] where step :: Stm State -> DerivSeqNode step Skip st = Done st @@ -20,9 +20,10 @@ sqrt = 'z' := 0 :. 'o' := 'o' + 2 :. 's' := 's' + 'o' ) +//Start = toString (seq sqrt st) Start = toString (tree sqrt st) where st :: Var -> Int - st 'x' = 16 + st 'x' = 9 |