-- syntax of Exc

type Var = 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 

type Exception = String

data Stm  = Ass Var Aexp | Skip | Seq Stm Stm
          | If Bexp Stm Stm | While Bexp Stm
          | HandleIn Stm Exception Stm | Raise Exception 


-- semantic categories for continuation style denotational semantics

type State = Var -> Int

bottomState :: State
bottomState x = bottomState x

updateState :: State -> Var -> Int -> State
updateState st y z x = if x == y then z else st x

cond :: (State -> Bool, State -> State, State -> State) -> (State -> State)
cond (pred, g1, g2) st = if pred st then g1 st else g2 st

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

type Cont = State -> State

type EnvE = Exception -> Cont

bottomEnvE :: EnvE
bottomEnvE e = bottomEnvE e

updateEnvE :: EnvE -> Exception -> Cont -> EnvE
updateEnvE envE e' c e = if e == e' then c else envE e


-- continuation 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


-- -- statements

cssemS :: Stm -> EnvE -> Cont -> Cont
cssemS (Ass x a) envE c st    
                    = c (updateState st x (semA a st))
cssemS Skip envE c st         
                    = c st 
cssemS (Seq s1 s2) envE c st  
                    = (cssemS s1 envE . cssemS s2 envE) c st
cssemS (If b s1 s2) envE c st 
                    = cond (semB b, cssemS s1 envE c, cssemS s2 envE c) st
cssemS (While b s) envE c st  
                    = fix f c st  where
                            f g c = cond (semB b, (cssemS s envE . g) c, c)
cssemS (HandleIn s1 e s2) envE c st 
                    = cssemS s1 (updateEnvE envE e (cssemS s2 envE c)) c st
cssemS (Raise e) envE c st 
                    = envE e st


-- example

{-
   loop is abstract syntax for
 
   begin while true do if x <= 0 then raise exit else x := x - 1 
         handle exit : y := 7 
   end
-}

loop :: Stm
loop = HandleIn (While TrueBexp
                       (If (Leq (Var "x") (Numl 0))
                           (Raise "exit")
                           (Ass "x" (Minus (Var "x") (Numl 1)))
                       )
                )
                "exit"
                (Ass "y" (Numl 7))

testloop :: Int -> (Int, Int)
testloop z = (st' "x", st' "y") where
                 st' = cssemS loop envE c st where
                     envE = bottomEnvE
                     c = id
                     st = updateState bottomState "x" z