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 s = (x,z):s 
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

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

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

cond :: (State -> Bool) 
           -> (State -> Maybe State) -> (State -> Maybe State)
             -> State -> Maybe State
cond p f0 f1 = \ s -> if p s then f0 s else f1 s

fix :: ((State -> Maybe State) -> State -> Maybe State) 
             -> State -> Maybe State
--fix f s = f (fix f) s

{-
fix f s = loop (\ _ ->  Nothing) 
         where loop g = case g s of 
                          Nothing -> loop (f g) 
                          Just s' -> Just s'
-}

approx f = iterate f (const Nothing) 

fix f s = let ss = map ($ s) (approx f)
          in head (dropWhile (== Nothing) ss)    

jd :: State -> Maybe State
jd s = Just s

(#) :: (State -> Maybe State) -> (State -> Maybe State)
         -> State -> Maybe State
(g # f) s = case f s of
               Nothing -> Nothing
               Just s' -> g s' 


stmt :: Stmt -> State -> Maybe State
stmt Skip = jd
stmt (stm0 :\ stm1) = stmt stm1 # stmt stm0
stmt (x := a) = \ s -> Just (upd x (aexp a s) s)
stmt (If b stm0 stm1) = cond (bexp b) (stmt stm0) (stmt stm1)
stmt (While b stm0) = fix f where
          f g = cond (bexp b) (g # stmt stm0) jd
xstmt (While b stm0) = \ s -> map ($ s) (approx f) where
          f g = cond (bexp b) (g # stmt stm0) jd


fac :: Stmt 
fac = --(Y := N 1) :\ 
      (While (N 1 :<= V X)
        ((Y := (V Y :* V X)) :\
         (X := (V X :- N 1))  
        )
      )