||*************************************************************************||
|| Semantics with Applications: A formal introduction                      ||
|| --- Appendix C: Operational Semantics in Miranda (appC.m)               ||
||     Hanne Riis Nielson & Flemming Nielson                               ||
||*************************************************************************||

%include "appB"

config ::= Inter stm state | Final state

||-------------------------------------------------------------------------||
|| Natural semantics                                                       ||
||-------------------------------------------------------------------------||

ns_stm :: config -> config

ns_stm (Inter (Ass x a) s) = 
        Final (update s x (a_val a s))
        where 
        update s x v y = v, if x = y
                       = s y, otherwise

ns_stm (Inter (Skip) s) = Final s

ns_stm (Inter (Comp ss1 ss2) s) = Final s''
                                  where 
                                  Final s' = ns_stm (Inter ss1 s)
                                  Final s'' = ns_stm (Inter ss2 s')

ns_stm (Inter (If b ss1 ss2) s) = Final s', if b_val b s
                                  where 
                                  Final s' = ns_stm (Inter ss1 s)

ns_stm (Inter (If b ss1 ss2) s) = Final s', if ~(b_val b s)
                                  where 
                                  Final s' = ns_stm (Inter ss2 s)

ns_stm (Inter (While b ss) s) = Final s'', if b_val b s 
                                where 
                                Final s' = ns_stm (Inter ss s)
                                Final s'' = ns_stm (Inter (While b ss) s')

ns_stm (Inter (While b ss) s) = Final s, if ~(b_val b s)

s_ns ss s = s'
            where 
            Final s' = ns_stm (Inter ss s)

|| Example:

s_fac = s_ns factorial s_init

||-------------------------------------------------------------------------||
|| Structural operational semantics                                        ||
||-------------------------------------------------------------------------||

is_Final (Inter ss s) = False
is_Final (Final s) = True

sos_stm :: config -> config

sos_stm (Inter (Ass x a) s) = Final (update s x (a_val a s))
                              where 
                              update s x v y = v, if x = y
                                             = s y, otherwise

sos_stm (Inter Skip s) = Final s

sos_stm (Inter (Comp ss1 ss2) s) = Inter (Comp ss1' ss2) s', 
                                   if ~is_Final(sos_stm (Inter ss1 s))
                                   where 
                                   Inter ss1' s' = sos_stm (Inter ss1 s)

sos_stm (Inter (Comp ss1 ss2) s) = Inter ss2 s',
                                   if is_Final(sos_stm (Inter ss1 s))
                                   where 
                                   Final s' = sos_stm (Inter ss1 s)       

sos_stm (Inter (If b ss1 ss2) s) = Inter ss1 s, if b_val b s

sos_stm (Inter (If b ss1 ss2) s) = Inter ss2 s, if ~b_val b s

sos_stm (Inter (While b ss) s) =
         Inter (If b (Comp ss (While b ss)) Skip) s

deriv_seq (Inter ss s) = 
          (Inter ss s) : (deriv_seq (sos_stm (Inter ss s)))

deriv_seq (Final s) = [Final s]

s_sos ss s = s'
             where 
             Final s' = last (deriv_seq (Inter ss s))

|| Example:

fac_seq = deriv_seq (Inter factorial s_init)

show_seq fv l = lay (map show_config l)
                where
                show_config (Final s) = 
                  "final state:\n"++lay (map (show_val s) fv)
                show_config (Inter ss s) =
                  show ss++"\n"++lay (map (show_val s) fv)
                 show_val s x = " s("++x++")="++shownum (s x)

s_fac' = s_sos factorial s_init