-- -------------------------------------------------------------------
--
-- appC.gs
-- 
-- An implementation of appendix C of
-- [Nielson and Nielson, semantics with applications]
--
-- -------------------------------------------------------------------
          
data  Config		=  Inter Stm State | Final State

-- -------------------------------------------------------------------
-- Secion C.1  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 not(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 not(b_val b s)


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

-- Example C.1
s_fac = s_ns factorial s_init
-- End Example C.1
                

-- -------------------------------------------------------------------
-- Secion C.2  Structural operatioal 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 not(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 not(b_val b s)

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


deriv_seq cf@(Inter ss s) = cf:(deriv_seq (sos_stm cf))
deriv_seq cf@(Final s)    = [cf]

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

-- Example C.6
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++")=" ++ (show (s x))
		        lay = layn

s_fac' = s_sos factorial s_init
-- End Example C.6