-- -------------------------------------------------------------------
--
-- appB.gs
-- 
-- An implementation of appendix B of
-- [Nielson and Nielson, semantics with applications]
--
-- -------------------------------------------------------------------

-- -------------------------------------------------------------------
-- Secion B.1  Abstract syntax
-- -------------------------------------------------------------------

type  Var	=  [Char]

data  Aexp	=  N Int | V Var | Add Aexp Aexp |
		   Mult Aexp Aexp | Sub Aexp Aexp

data  Bexp	=  TRUE | FALSE | Eq Aexp Aexp | Le Aexp Aexp |
		   Neg Bexp | And Bexp Bexp

data  Stm	=  Ass Var Aexp | Skip | Comp Stm Stm |
		   If Bexp Stm Stm | While Bexp Stm 

-- Example B.1

factorial = Comp (Ass "y" (N 1))
                 (While (Neg (Eq (V "x") (N 1)))
                    (Comp (Ass "y" (Mult (V "y") (V "x")))
                          (Ass "x" (Sub (V "x") (N 1)))))
-- End Example B.1

---------------------------------------------------------------------
-- Secion B.2  Evaluation of expressions
---------------------------------------------------------------------

type  Z			=  Int
type  T			=  Bool

type  State		=  Var -> Z


-- Example B.3
s_init "x"		=  3
s_init y		=  0
-- End Example B.3

                
a_val			:: Aexp -> State -> Z
b_val			:: Bexp -> State -> T

a_val (N n) s		=  n
a_val (V x) s		=  s x
a_val (Add a1 a2) s	=  (a_val a1 s) + (a_val a2 s)
a_val (Mult a1 a2) s	=  (a_val a1 s) * (a_val a2 s)
a_val (Sub a1 a2) s	=  (a_val a1 s) - (a_val a2 s)
                                             
b_val TRUE s		=  True
b_val FALSE s		=  False
b_val (Eq a1 a2) s	=  a_val a1 s == a_val a2 s     -- equivalent but smaller
b_val (Le a1 a2) s	=  a_val a1 s <= a_val a2 s     -- equivalent but smaller
b_val (Neg b) s		=  not(b_val b s)               -- equivalent but smaller
b_val (And b1 b2) s	=  (b_val b1 s) && (b_val b2 s) -- equivalent but smaller