-- While extended with block structures and procedures

-- syntax

type Var = String

type Pname = String

data AExpr = Var Var | Num Integer
          | AExpr :+ AExpr | AExpr :- AExpr | AExpr :* AExpr

data BExpr = T | F | AExpr :== AExpr | AExpr :<= AExpr 
          | Not BExpr | BExpr :&& BExpr | BExpr :|| BExpr 

type DecV = [(Var, AExpr)]

type DecP = [(Pname, Stm)]

data Stm  = Var ::= AExpr | Skip | Stm :\ Stm
          | If BExpr Stm Stm | While BExpr Stm
          | Block DecV DecP Stm | Call Pname


-- semantic categories for direct style denotational semantics

type Loc = Integer

next :: Loc
next = -1

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


type Store = Loc -> Integer

emptyStore :: Store
emptyStore _ = undefined

updStore :: Loc -> Integer -> Store -> Store
updStore l n sto l' = if l' == l then n else sto l'

lkpStore :: Loc -> Store -> Integer
lkpStore l sto = sto l

type EnvV = Var -> Loc

emptyEnvV :: EnvV
emptyEnvV _ = undefined

updEnvV :: Var -> Loc -> EnvV -> EnvV
updEnvV x l envV x' = if x' == x then l else envV x'

lkpEnvV :: Var -> EnvV -> Loc
lkpEnvV x envV = envV x

type EnvP = Pname -> (Store -> Store)

emptyEnvP :: EnvP
emptyEnvP _ = undefined

updEnvP :: Pname -> (Store -> Store) -> EnvP -> EnvP
updEnvP p g envP p' = if p' == p then g else envP p'

lkpEnvP :: Pname -> EnvP -> (Store -> Store)
lkpEnvP p envP = envP p


type State = Var -> Integer

lkpState :: Var -> State -> Integer
lkpState x st = st x

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



-- denotational semantics 

-- -- arithmetical expressions

semA :: AExpr -> State -> Integer
semA (Var x) st    = lkpState x st
semA (Num n) st    = n
semA (a1 :+ a2) st = semA a1 st + semA a2 st 
semA (a1 :- a2) st = semA a1 st - semA a2 st 
semA (a1 :* a2) st = semA a1 st * semA a2 st 


-- -- boolean expressions

semB :: BExpr -> State -> Bool
semB T st           = True
semB F st           = False
semB (a1 :== a2) st = semA a1 st == semA a2 st
semB (a1 :<= a2) st = semA a1 st <= semA a2 st
semB (Not b) st     = not (semB b st)
semB (b1 :&& b2) st = semB b1 st && semB b2 st
semB (b1 :|| b2) st = semB b1 st || semB b2 st


-- -- variable declaration lists

semDV :: DecV -> EnvV -> Store -> (EnvV, Store)
semDV [] envV sto 
         = (envV, sto)
semDV ((x, a) : decV) envV sto 
         = semDV decV (updEnvV x l envV) 
                      (updStore next (new l) $ updStore l v sto) where
             l = lkpStore next sto
             v = semA a (mkState envV sto)


-- -- procedure declaration lists

semDP :: DecP -> EnvV -> EnvP -> EnvP
semDP [] envV envP 
         = envP
semDP ((p, s) : decP) envV envP
         = semDP decP envV (updEnvP p g envP) where
             g = semS s envV envP


-- -- statements

semS :: Stm -> EnvV -> EnvP -> (Store -> Store)
semS (x ::= a) envV envP sto    
                   = updStore l (semA a (mkState envV sto)) sto where
                        l = lkpEnvV x envV
semS Skip envV envP sto         
                   = sto
semS (s1 :\ s2) envV envP sto  
                   = semS s2 envV envP $ semS s1 envV envP sto
semS (If b s1 s2) envV envP sto 
                   = if semB b (mkState envV sto) 
                         then semS s1 envV envP sto else semS s2 envV envP sto
semS (While b s) envV envP sto  
                   = semS (If b (s :\ While b s) Skip) envV envP sto
semS (Block decV decP s) envV envP sto  
                   = semS s envV' envP' sto' where
                        (envV', sto') = semDV decV envV sto
                        envP' = semDP decP envV' envP
semS (Call p) envV envP sto
                   = lkpEnvP p envP 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 [("x", Num 7)]
                [("p", "x" ::= Num 0)]
                (Block [("x", Num 5)]
                       []
                       (Call "p")
                )


testuseless :: (Integer, Integer, Integer)
testuseless = (sto' 12, sto' 13, sto' next) where 
               sto' = semS useless envV envP sto where
                 envV = emptyEnvV
                 envP = emptyEnvP
                 sto  = updStore next 12 emptyStore