-- syntax of Proc

type Var = String

type Pname = String

type Numl = Int

data Aexp = Var Var | Numl Numl 
          | Plus Aexp Aexp | Minus Aexp Aexp | Times Aexp Aexp

data Bexp = TrueBexp | FalseBexp | Eq Aexp Aexp | Leq Aexp Aexp 
          | Not Bexp | And Bexp Bexp | Or Bexp Bexp 

data DecV = NilDecV | ConsDecV Var Aexp DecV

data DecP = NilDecP | ConsDecP Pname Stm DecP

data Stm  = Ass Var Aexp | Skip | Seq Stm Stm
          | If Bexp Stm Stm | While Bexp Stm
          | Block DecV DecP Stm | Call Pname


-- semantic categories for direct style denotational semantics

type Loc = Int

next :: Loc
next = -1

new :: Loc -> Loc
new l = l + 1


type Store = Loc -> Int

bottomStore :: Store
bottomStore l = bottomStore l

updateStore :: Store -> Loc -> Int -> Store
updateStore sto l' z l = if l == l' then z else sto l

cond :: (Store -> Bool, Store -> Store, Store -> Store) -> (Store -> Store)
cond (pred, g1, g2) sto = if pred sto then g1 sto else g2 sto

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


type EnvV = Var -> Loc

bottomEnvV :: EnvV
bottomEnvV x = bottomEnvV x

updateEnvV :: EnvV -> Var -> Loc -> EnvV
updateEnvV envV y l x = if x == y then l else envV x


type EnvP = Pname -> Store -> Store

bottomEnvP :: EnvP
bottomEnvP p = bottomEnvP p

updateEnvP :: EnvP -> Pname -> (Store -> Store) -> EnvP
updateEnvP envP q g p = if p == q then g else envP p


type State = Var -> Int

lkup :: EnvV -> Store -> State
lkup envV sto = sto . envV



-- direct style denotational semantics 

-- -- arithmetical expressions

semA :: Aexp -> State -> Int
semA (Var x) st       = st x
semA (Numl n) st      = n
semA (Plus a1 a2) st  = semA a1 st + semA a2 st 
semA (Minus a1 a2) st = semA a1 st - semA a2 st 
semA (Times a1 a2) st = semA a1 st * semA a2 st 


-- -- boolean expressions

semB :: Bexp -> State -> Bool
semB TrueBexp st    = True
semB FalseBexp st   = False
semB (Eq a1 a2) st  = semA a1 st == semA a2 st
semB (Leq a1 a2) st = semA a1 st <= semA a2 st
semB (Not b) st     = not (semB b st)
semB (And b1 b2) st = semB b1 st && semB b2 st
semB (Or b1 b2) st  = semB b1 st || semB b2 st


-- -- variable declaration lists

dssemDV :: DecV -> EnvV -> Store -> (EnvV, Store)
dssemDV NilDecV envV sto 
         = (envV, sto)
dssemDV (ConsDecV x a decV) envV sto 
         = dssemDV decV (updateEnvV envV x l) 
                      (updateStore (updateStore sto l v) next (new l)) where
             l = sto next
             v = semA a (lkup envV sto)


-- -- procedure declaration lists

dssemDP :: DecP -> EnvV -> EnvP -> EnvP
dssemDP NilDecP envV envP 
         = envP
dssemDP (ConsDecP p s decP) envV envP
         = dssemDP decP envV (updateEnvP envP p g) where
             g = dssemS s envV envP


-- -- statements

dssemS :: Stm -> EnvV -> EnvP -> Store -> Store
dssemS (Ass x a) envV envP sto    
                   = updateStore sto l (semA a (lkup envV sto)) where
                        l = envV x
dssemS Skip envV envP sto         
                   = sto
dssemS (Seq s1 s2) envV envP sto  
                   = (dssemS s2 envV envP . dssemS s1 envV envP) sto
dssemS (If b s1 s2) envV envP sto 
                   = cond (semB b . lkup envV, 
                         dssemS s1 envV envP, dssemS s2 envV envP) sto
dssemS (While b s) envV envP sto  
                   = fix f sto where
                        f g = cond (semB b. lkup envV, 
                                  g . dssemS s envV envP, id)
dssemS (Block decV decP s) envV envP sto  
                   = dssemS s envV' envP' sto' where
                        (envV', sto') = dssemDV decV envV sto
                        envP' = dssemDP decP envV' envP
dssemS (Call p) envV envP sto
                   = envP p sto



-- example

{-

   useless is abstract syntax for 

   begin var x := 7 ; proc p is x := 0 ; 
       begin var x := 5; call p end
   end

-}

useless :: Stm
useless = Block (ConsDecV "x" (Numl 7) NilDecV)
                (ConsDecP "p" (Ass "x" (Numl 0)) NilDecP)
                (Block (ConsDecV "x" (Numl 5) NilDecV)
                       (NilDecP)
                       (Call "p")
                )


testuseless :: (Int, Int, Int)
testuseless = (sto' 12, sto' 13, sto' next) where 
               sto' = dssemS useless envV envP sto where
                 envV = bottomEnvV
                 envP = bottomEnvP
                 sto  = updateStore bottomStore next 12