-- syntax of Proc

type Var = String

type Pname = String

type Num = Integer

data Aexp = Var Var | Num Num 
          | Aexp :+ Aexp | Aexp :- Aexp | Aexp :* Aexp

data Bexp = T | F | Aexp :== Aexp | Aexp :<= Aexp 
          | Not Bexp | Bexp :&& Bexp | Bexp :|| Bexp 

data DecV = NilDecV | ConsDecV Var Aexp DecV

data DecP = NilDecP | ConsDecP Pname Stm DecP

data Stm  = Var := Aexp | Skip | Stm :\ Stm
          | If Bexp Stm Stm | While Bexp 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

allzeros :: Store
allzeros l = 0

update :: Eq a => (a -> b) -> a -> b -> (a -> b)
update 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

allunalloc :: EnvV
allunalloc x = -1

next :: Var
next = "next" 

type EnvP = Pname -> Store -> Store

allbottom :: EnvP
allbottom p sto = undefined



type State = Var -> Integer

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



-- direct style denotational semantics 

-- -- arithmetical expressions

semA :: Aexp -> State -> Integer
semA (Var x) st       = st x
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 :: Bexp -> 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

dssemDV :: DecV -> EnvV -> Store -> (EnvV, Store)
dssemDV NilDecV envV sto 
         = (envV, sto)
dssemDV (ConsDecV x a decV) envV sto 
         = dssemDV decV (update (update envV x l) next (new l)) 
                      (update sto l v) where
             l = envV 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 (update envP p g) where
             g = dssemS s envV envP


-- -- statements

dssemS :: Stm -> EnvV -> EnvP -> Store -> Store
dssemS (x := a) envV envP sto    
                   = update sto l (semA a (lkup envV sto)) where
                        l = envV x
dssemS Skip envV envP sto         
                   = sto
dssemS (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; x := x + 1) end
   end;
   next := 17

-}

useless :: Stm
useless = (Block (ConsDecV "x" (Num 7) NilDecV)
                (ConsDecP "p" ("x" := (Num 0)) NilDecP)
                (Block (ConsDecV "x" (Num 5) NilDecV)
                       (NilDecP)
                       ((Call "p") :\ ("x" := (Var "x" :+ Num 1))) 
                ))
          :\ (next := Num 17)



testuseless = (sto' 12, sto' 13, sto' 14) where 
               sto' = dssemS useless envV envP sto where
                 envV = update allunalloc next 12
                 envP = allbottom
                 sto  = allzeros