data Var = X | Y | Z | Next deriving (Eq, Show) 

data Pname = P | Q | R deriving (Eq, Show)


type Loc = Integer

type Store = [(Loc, Integer)]

type EnvV = [(Var, Loc)]

type EnvP = [(Pname, Store -> Store)]


type State = [(Var, Integer)]

lkp :: Eq a => a -> [(a,b)] -> b
lkp x [] = error "lookup failed"
lkp x ((y,z):s) = if x == y then z else lkp x s

upd :: Eq a => a -> b -> [(a,b)] -> [(a,b)]
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

initd :: [(a,b)]
initd = []

initEnvV :: EnvV
initEnvV = upd Next 0 initd


join :: (Eq a, Eq b) => [(a,b)] -> [(b,c)] -> [(a,c)]
join dict0 dict1= [ (a, lkp b dict1) | (a, b) <- dict0]



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
          | Block DecV DecP Stmt 
          | Call Pname   deriving Show

type DecV = [(Var, AExp)]

type DecP = [(Pname, Stmt)]


cond :: (Store -> Bool) 
          -> (Store -> Store) -> (Store -> Store) 
            -> Store -> Store
cond p f g = \ sto -> if p sto then f sto else g sto

fix :: ((Store -> Store) -> Store -> Store) -> Store -> Store
fix f = f (fix f)


decV :: DecV -> EnvV -> Store -> (EnvV, Store)

decV [] envV sto = (envV, sto)
decV ((x, a) : dvs) envV sto = decV dvs envV' sto'
          where ell   = lkp Next envV
                envV' = upd x ell (upd Next (ell+1) envV) 
                sto'  = upd ell (aexp a (join envV sto)) sto

decP :: DecP -> EnvV -> EnvP -> EnvP

decP [] envV envP = envP
decP ((p, stm) : dps) envV envP = decP dps envV envP'
          where g     = stmt stm envV envP 
                envP' = upd p g envP


stmt :: Stmt -> EnvV -> EnvP -> Store -> Store

stmt Skip envV envP = id
stmt (stm0 :\ stm1) envV envP 
       = stmt stm1 envV envP . stmt stm0 envV envP

stmt (x := a) envV envP 
       = \ sto -> upd (lkp x envV) (aexp a (join envV sto)) sto

stmt (If b stm0 stm1) envV envP 
       = cond (bexp b . join envV) 
               (stmt stm0 envV envP) (stmt stm1 envV envP)

stmt (While b stm0) envV envP = fix f 
     where f g = cond (bexp b . join envV) 
               (g . stmt stm0 envV envP) id

stmt (Block dvs dps stm) envV envP 
       = \ sto -> let (envV', sto') = decV dvs envV sto
                      envP'         = decP dps envV' envP
                  in stmt stm envV' envP' sto'

stmt (Call p) envV envP = lkp p envP



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

testfac = stmt fac envV envP sto 
              where envV = [(X, 0), (Y, 1), (Next, 2)]
                    envP = []
                    sto  = [(0, 6)]


bookExample = Block [(X, N 7)] [(P, X := N 0)]
                  ((Block [(X, N 5)] [] (Call P :\ (Z := V X)))
                   :\ (Y := V X))

testBookExample = stmt bookExample envV envP sto
              where envV = [(Y, 0), (Z, 1), (Next, 2)]
                    envP = []
                    sto  = []