-- syntax of While

type Var = String

type Exc = 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 Stm  = Var := Aexp | Skip | Stm :\ Stm
          | If Bexp Stm Stm | While Bexp Stm
          | Raise Exc
          | Handle Stm Exc Stm



-- semantic categories for direct style denotational semantics

type State = Var -> Integer

type Cont = State -> State

allzeros :: State
allzeros x = 0

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


type EnvE = Exc -> Cont

allids :: EnvE
allids e = id


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


-- -- statements

cssemS :: Stm -> EnvE -> Cont -> Cont
cssemS (x := a) envE c     = c'
                               where c' st = c (update st x (semA a st))
cssemS Skip envE c         = c
cssemS (s1 :\ s2) envE c   = (cssemS s1 envE . cssemS s2 envE) c
cssemS (If b s1 s2) envE c = cond (semB b, cssemS s1 envE c, cssemS s2 envE c)
cssemS (While b s) envE c  = fix f c where
                                f g c = cond (semB b, (cssemS s envE . g) c, c)
cssemS (Raise e) envE c    = envE e
cssemS (Handle s e s') envE c = cssemS s envE' c where
                                   envE' =  update envE e (cssemS s' envE c)

-- example

{-

   fact is abstract syntax for 

   y := 1 ; while not (x = 1) do (y := y * x ; x := x - 1) 

-}

--fact :: Stm


fact = 
  Handle
     ( ("y" := Num 1) :\
       (While (Not (Var "x" :== Num 1))
         (
           Handle
           (
             (If (Not (Var "x" :== Num 7))
                 (("y" := (Var "y" :* Var "x")) :\ ("x" := (Var "x" :- Num 1))
                 )
                 (Raise "seitse")
             )
           )
           "seitse"
           --("x" := Num 3)
           (Raise "seitse")
         ) 
       )
     )
     "seitse"
     ("x" := Num 1000)

 
              

testfact :: Integer -> (Integer, Integer)
testfact z = (st' "x", st' "y") where 
               st' = cssemS fact allids id st where
                 st  = update allzeros "x" z