data Var = X | Y | Z deriving (Eq, Show)
type State = [(Var, Integer)]
lkp :: Var -> State -> Integer
lkp x [] = 0
lkp x ((y,z):s) = if x == y then z else lkp x s
upd :: Var -> Integer -> State -> State
upd x z [] = [(x,z)]
upd x z ((y,w):s) = if x == y then
(x,z):s
else (y,w):upd x z s
init :: State
init = []
data AExp = N Integer | V Var
| AExp :+ AExp | AExp :- AExp | AExp :* AExp deriving Show
aexp :: AExp -> State -> Integer
aexp (N z) _ = z
aexp (V x) s = lkp x s
aexp (a0 :+ a1) s = aexp a0 s + aexp a1 s
aexp (a0 :- a1) s = aexp a0 s - aexp a1 s
aexp (a0 :* a1) s = aexp a0 s * aexp a1 s
data BExp = TT | FF | AExp :== AExp | AExp :<= AExp
| Not BExp | BExp :&& BExp | BExp :|| BExp deriving Show
bexp :: BExp -> State -> Bool
bexp TT _ = True
bexp FF _ = False
bexp (a0 :== a1) s = aexp a0 s == aexp a1 s
bexp (a0 :<= a1) s = aexp a0 s <= aexp a1 s
bexp (Not b) s = not (bexp b s)
bexp (a0 :&& a1) s = bexp a0 s && bexp a1 s
bexp (a0 :|| a1) s = bexp a0 s || bexp a1 s
data Stmt = Skip | Stmt :\ Stmt
| Var := AExp
| If BExp Stmt Stmt
| While BExp Stmt deriving Show
stmt :: Stmt -> State -> State
stmt Skip s = s
stmt (stm0 :\ stm1) s = s' where
s'' = stmt stm0 s
s' = stmt stm1 s''
-- stmt (stm0 :\ stm1) s = stmt stm1 (stmt stm0 s)
stmt (x := a) s = upd x z s where
z = aexp a s
stmt (If b stm0 stm1) s =
if bexp b s then
stmt stm0 s
else stmt stm1 s
stmt (While b stm0) s =
if bexp b s then
stmt (While b stm0) (stmt stm0 s)
else s
step :: Stmt -> State -> Either State (Stmt, State)
step Skip s = Left s
step (x := a) s = Left (upd x (aexp a s) s)
step (stm0 :\ stm1) s = case step stm0 s of
Left s' -> Right (stm1, s')
Right (stm0', s') -> Right (stm0' :\ stm1, s')
step (If b stm0 stm1) s = if bexp b s then
Right (stm0, s)
else Right (stm1, s)
step (While b stm0) s = Right (If b (stm0 :\ (While b stm0)) Skip, s)
run :: Stmt -> State -> State
run stm s = case step stm s of
Left s' -> s'
Right (stm', s') -> run stm' s'
fac :: Stmt
fac = (Y := N 1) :\
(While (N 1 :<= V X)
((Y := (V Y :* V X)) :\
(X := (V X :- N 1))
)
)