||*************************************************************************||
|| Semantics with Applications: A formal introduction                      ||
|| --- Appendix D: Denotational Semantics in Miranda (appD.m)              ||
||     Hanne Riis Nielson & Flemming Nielson                               ||
||*************************************************************************||

%include "appB"

cond (p, g1, g2) s = g1 s, p s
                   = g2 s, ~ p s

fix ff = ff (fix ff)

s_ds:: stm -> state -> state

s_ds (Ass x a) s = update s (a_val a s) x
                   where
                   update s v x y = v, x = y
                                  = s y, otherwise

s_ds Skip = id

s_ds (Comp ss1 ss2) = (s_ds ss2) . (s_ds ss1)

s_ds (If b ss1 ss2) = cond (b_val b, s_ds ss1, s_ds ss2)

s_ds (While b ss) = fix ff
                    where
                    ff g = cond (b_val b, g . s_ds ss, id)

|| example

s_final = s_ds factorial s_init