-- A simple programming language
-- Author: Martin Sulzmann

-- IMP-interpreter written in continuation-passing style
-- adding exceptions

-- data definitions

type Var = String

type Exception = String

data Value = N Int | BTrue | BFalse deriving Show

data Exp = Val Value | Id Var | Plus Exp Exp | Minus Exp Exp | Times Exp Exp
         | Div Exp Exp | Equal Exp Exp | Gt Exp Exp | And Exp Exp | Not Exp deriving Show

data Cmd = Skip | Assign Var Exp | Seq Cmd Cmd | ITE Exp Cmd Cmd 
         | While Exp Cmd | Newvar Var Exp Cmd 
         | Raise Exception | Handle Exception Cmd Cmd deriving Show

type State = Var -> Value

type EEnv = Var -> Cont

type Cont = State -> State


----------------------
-- state operations --
----------------------

lookupVar :: State -> Var -> Value
lookupVar s id = s id

updateState :: State -> Var -> Value -> State
updateState state id v = let state' id1 
 		              | id1 == id = v
		              | otherwise = state id1
 		         in state'


--------------------------
-- expression semantics --
--------------------------


evalExp :: State -> Exp -> Value
evalExp _ (Val v) = v
evalExp s (Id id) = lookupVar s id 
evalExp s (Plus e1 e2) = let (N i1) = evalExp s e1
                             (N i2) = evalExp s e2
                         in N (i1 + i2)
-- complete missing cases
evalExp s (Equal e1 e2) = let v1 = evalExp s e1
                              v2 = evalExp s e2
                              eqB BTrue BTrue = BTrue
                              eqB BFalse BFalse = BTrue
                              eqB _ _ = BFalse
                              eqInt i1 i2 
                                | i1 == i2  = BTrue
                                | otherwise = BFalse
                          in case v1 of
                              N i1   -> case v2 of
                                         N   i2 -> eqInt i1 i2
                                         _      -> error "Equal: Incompatible operands"
                              _      -> case v2 of
                                         N _   -> error "Equal: Incompatible operands"
                                         _     -> eqB v1 v2
evalExp s (Gt e1 e2) = let (N i1) = evalExp s e1
                           (N i2) = evalExp s e2
                           gtInt i1 i2
                            | i1 < i2   = BTrue
                            | otherwise = BFalse
                       in gtInt i1 i2
-- complete missing cases


-----------------------
-- command semantics --
-----------------------

evalCmd :: EEnv -> Cont -> Cmd -> Cont
evalCmd env ct Skip = ct
evalCmd env ct (Assign id e) = \ s -> updateState (ct s) id (evalExp (ct s) e)
evalCmd env ct (Seq c1 c2) = let ct' = evalCmd env ct c1
                             in evalCmd env ct' c2
evalCmd env ct (ITE e c1 c2) = \ s ->
                             let v = evalExp (ct s) e
                             in case v of
                                 BTrue  -> (evalCmd env ct c1) s
                                 BFalse -> (evalCmd env ct c2) s
                                 _      -> error "ITE: invalid condition"
evalCmd env ct (While e c) = \ s ->
                           let v= evalExp (ct s) e
                           in case v of
                              BFalse -> ct s
                              BTrue  -> ((evalCmd env ct (Seq c (While e c))) s)
                              _      -> error "While: invalid condition"
evalCmd env ct (Newvar id e c) = 
                             let ct' s = updateState (ct s) id (evalExp (ct s) e)
                                 ct'' = evalCmd env ct' c
                                 ct''' s = updateState (ct'' s) id (lookupVar (ct s) id)
                             in ct'''

-- Observe the difference between the two kinds of defining
-- the semantics of raising exceptions
evalCmd env ct (Raise e) = env e 
{-evalCmd env ct (Raise e) = let ct' = env e
 			       compose ct1 ct2 = \ s -> ct2 (ct1 s)
			   in compose ct ct'-}
evalCmd env ct (Handle e c1 c2) = let env' x = if x == e 
                                               then evalCmd env ct c1
                                               -- replace the above by
                                               -- then evalCmd env' ct c1
                                               -- and observe the effect
                                               -- evaluate prog6
				               else env x
                                  in evalCmd env' ct c2



-------------------------------
-- initial states, envs, ... --
-------------------------------



initstate :: State
initstate "x" = N 1
initstate "y" = BTrue
initstate "z" = N 0
initstate _   = error "Undefined"

initenv :: EEnv
initenv x = error ("Exception " ++ x ++ " undefined\n")

run p = (evalCmd initenv (\x->x) p) initstate


rundisplay p var = run p var


--------------
-- Examples --
--------------

--   x:= x + 3
--
prog1 :: Cmd
prog1 = Assign "x" (Plus (Id "x") (Val (N 3)))


-- handle "error" = x:=2
-- in x:=z; raise "error"
--
prog2 :: Cmd
prog2 = Handle "error" (Assign "x" (Val (N 2))) 
                       (Seq (Assign "x" (Val (N 3))) (Raise "error"))
-- (handle "error" = x:=2
--  in x:=3; raise "error")
--
prog3 :: Cmd
prog3 = Seq (Handle "error" (Assign "x" (Val (N 2))) 
                            (Seq (Assign "x" (Val (N 3))) (Raise "error")))
            (Assign "x" (Val (N 3)))

-- (handle "err1" = x:= 2
--  in (handle "err2: = (x:= 4; raise "err1")
--      in x:= 3; raise "err2"))
-- 
prog4 :: Cmd
prog4 = Handle "err1" (Assign "x" (Val (N 2)))
                      (Handle "err2" (Seq (Assign "x" (Val (N 4))) (Raise "err1"))
			             (Seq (Assign "x" (Val (N 3))) (Raise "err2")))


-- (handle "err1" = z:= 2
--  in (handle "err2: = (x:= 4; raise "err1")
--      in x:= 3; raise "err1"))
-- 
prog5 :: Cmd
prog5 = Handle "err1" (Assign "z" (Val (N 2)))
                      (Handle "err2" (Seq (Assign "x" (Val (N 4))) (Raise "err1"))
			             (Seq (Assign "x" (Val (N 3))) (Raise "err1")))



-- (handle "g1" = raise "g1") in raise "g1"

prog6 :: Cmd
prog6 = Handle "g1" (Raise "g1") (Raise "g1")

prog7 :: Cmd
prog7 = Handle "error" (Assign "x" (Val (N 2))) 
                       (Seq (Raise "error") (Assign "x" (Val (N 3))))
-- (handle "error" = x:=2
--  in raise "error"; x:=3)

prog8 :: Cmd
prog8 = Handle "error" Skip
                       (Seq prog1 (Raise "error"))