-- use with Hugs -98

-- needed for Jyri's dirty output
import IOExts


-- syntax of While

type Var = String

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

data Stm  = Var ::= AExpr | Skip | Stm :\ Stm 
          | If BExpr Stm Stm | While BExpr Stm
	  -- extensions
          | Print AExpr | Raise Exc | Handle Exc Stm Stm


-- semantic categories for denotational semantics

type State = Var -> Integer

empty :: State
empty x = error ("variable " ++ x ++ " has no value")
-- empty x = undefined

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

upd :: Var -> Integer -> State -> State
--upd x n st = \ x' -> if x' == x then n else st x'
upd x n st = st' where
                 st' x' | x' == x   = n
                        | otherwise = st x'

-- denotational semantics 

-- -- arithmetical expressions

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


-- -- statements

-- pure While


semS :: Stm -> State -> State
semS (x ::= a) st    = upd x (semA a st) st
semS Skip st         = st 
semS (s1 :\ s2) st   = semS s2 (semS s1 st)
semS (If b s1 s2) st = if semB b st then semS s1 st else semS s2 st
semS (While b s) st  = if semB b st then semS (While b s) (semS s st)
                                        else st 
-- semS (While b s) st  = semS (If b (s :\ While b s) Skip) st


-- example

{-

   fact is abstract syntax for 

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

-}

fact :: Stm
fact =     ("y" ::= Num 1) :\
           (While (Not (Var "x" :== Num 1))
                  (("y" ::= (Var "y" :* Var "x")) :\
                   ("x" ::= (Var "x" :- Num 1))
                  )
           )

testfact :: Integer -> (Integer, Integer)
testfact z = (lkp "x" st, lkp "y" st) where 
               st = semS fact (upd "x" z empty)  



-- extension with output

{-
semSPrint :: Stm -> State -> ([Integer], State) 
semSPrint (x ::= a) st    = ([], upd x (semA a st) st)
semSPrint Skip st         = ([], st) 
semSPrint (s1 :\ s2) st   = (is ++ is', st'') 
                            where (is, st')   = semSPrint s1 st
                                  (is', st'') = semSPrint s2 st'
semSPrint (If b s1 s2) st = if semB b st then semSPrint s1 st else semSPrint s2 st
semSPrint (While b s) st  = semSPrint (If b (s :\ While b s) Skip) st
semSPrint (Print a) st    = ([semA a st], st) 
-}

-- same but using the overt monad explicitly

{- 
- defined in Prelude
class Monad m where
  return :: a -> m a
  (>>=) :: m a -> (a -> m b) -> m b
-}

-- this instance declaration requires hugs -98 !!

instance Monad ((,) [e]) where
  -- return :: a -> ([e], a)
  return a = ([], a)
  -- (>>=) :: ([e], a) -> (a -> ([e], b)) -> ([e], b)
  (es, a) >>= f = (es ++ es', b) 
                       where (es', b) = f a

{- 
-- defined in Prelude
primitive putChar :: Char   -> IO ()
primitive putStr  :: String -> IO ()

putStrLn :: String -> IO ()
putStrLn s = do putStr s
                putChar '\n'

print :: Show a => a -> IO ()
print = putStrLn . show

primitive primretIO  :: a -> IO a
primitive primbindIO :: IO a -> (a -> IO b) -> IO b

instance Monad IO where 
    return = primretIO
    (>>=)  = primbindIO
-}

semSOutp :: Stm -> State -> ([Integer], State)
-- alternatively, using the IO monad
-- semSOutp :: Stm -> State -> IO State
semSOutp (x ::= a) st    = return (upd x (semA a st) st)
semSOutp Skip st         = return st
semSOutp (s1 :\ s2) st   = do st'  <- semSOutp s1 st
                              st'' <- semSOutp s2 st'
                              return st''
{- 
-- syntactic sugar for :  
semSOutp (s1 :\ s2) st   = semSOutp s1 st  >>= \ st'  ->
                           semSOutp s2 st' >>= \ st'' ->
                           return st''
                         = semSOutp s1 st  >>= semSOutp s2
-}
semSOutp (If b s1 s2) st = if semB b st then semSOutp s1 st else semSOutp s2 st
semSOutp (While b s) st  = semSOutp (If b (s :\ While b s) Skip) st
semSOutp (Print a) st    = ([semA a st], st)
-- alternatively
-- semSOutp (Print a) st    = do { print (semA a st) ; return st }

factOutp = ("y" ::= Num 1) :\
            (While (Not (Var "x" :== Num 1))
                   (("y" ::= (Var "y" :* Var "x")) :\
                    (("x" ::= (Var "x" :- Num 1)) :\
                     (Print (Var "x") :\ Print (Var "y"))
                    ) 
                   )
            )

natsOutp = ("x" ::= Num 1) :\ (While T (Print (Var "x") :\ 
                                         ("x" ::= (Var "x" :+ Num 1))))

testfactOutp :: Integer -> ([Integer], (Integer, Integer))
-- alternatively
-- testfactOutp :: Integer -> IO (Integer, Integer)
testfactOutp z = do st <- semSOutp factOutp (upd "x" z empty)
                    return (lkp "x" st, lkp "y" st)


testnatsOutp :: ([Integer], Integer)
-- alternatively 
-- testnatsOutp :: IO Integer
testnatsOutp = do st <- semSOutp natsOutp empty
                  return (lkp "x" st)


-- output real dirty as Jyri wants to have it, requires IOExts

{-
-- defined in IOExts
unsafePerformIO :: IO a -> a
-}

{-
unsafePrint :: Show a => a -> ()
unsafePrint a = unsafePerformIO (print a)

semS :: Stm -> State -> State
semS (x ::= a) st    = upd x (semA a st) st
semS Skip st         = st 
semS (s1 :\ s2) st   = semS s2 (semS s1 st)
semS (If b s1 s2) st = if semB b st then semS s1 st else semS s2 st
semS (While b s) st  = semS (If b (s :\ While b s) Skip) st
semS (Print a) st    = case unsafePrint (semA a st) of
                              () -> st 

testfactOutp :: Integer -> (Integer, Integer)
testfactOutp z = (lkp "x" st, lkp "y" st) where 
                           st = semS factOutp (upd "x" z empty) 
testnatsOutp :: Integer -> Integer
testnatsOutp   = lkp "x" st where 
                           st = semS natsOutp empty   

-}

-- exceptions (without handling)

{-
-- defined in Prelude
Either a b = Left a | Right b 
-}


instance Monad (Either e) where
  -- return :: e -> Either e a
  return = Right 
  -- (>>=) :: Either e a -> (a -> Either e b) -> Either e b
  Left e  >>= f = Left e 
  Right a >>= f = f a

-- note everything is as before, only the monad has changed
-- and instead of Print we have supported Raise

type Exc = String

semSExc :: Stm -> State -> Either Exc State
semSExc (x ::= a) st    = return (upd x (semA a st) st)
semSExc Skip st         = return st
semSExc (s1 :\ s2) st   = do st'  <- semSExc s1 st
                             st'' <- semSExc s2 st'
                             return st''  
semSExc (If b s1 s2) st = if semB b st then semSExc s1 st else semSExc s2 st
semSExc (While b s) st  = semSExc (If b (s :\ While b s) Skip) st
semSExc (Raise exc) st  = Left exc

factExc = If (Var "x" :<= Num 0)
             (Raise "input to fact must be pos")
             (("y" ::= Num 1) :\
              (While (Not (Var "x" :== Num 1))
                     (("y" ::= (Var "y" :* Var "x")) :\
                      ("x" ::= (Var "x" :- Num 1))
                     )
              )
             )

testfactExc :: Integer -> Either Exc (Integer, Integer)
testfactExc z = do st <- semSExc factExc (upd "x" z empty)
                   return (lkp "x" st, lkp "y" st)


-- exceptions with handling


semSExcH :: Stm -> State -> Either (Exc, State) State
semSExcH (x ::= a) st    = return (upd x (semA a st) st)
semSExcH Skip st         = return st
semSExcH (s1 :\ s2) st   = do st'  <- semSExcH s1 st
                              st'' <- semSExcH s2 st'
                              return st''  
semSExcH (If b s1 s2) st = if semB b st then semSExcH s1 st else semSExcH s2 st
semSExcH (While b s) st  = semSExcH (If b (s :\ While b s) Skip) st
semSExcH (Raise exc) st  = Left (exc, st)
semSExcH (Handle exc sE s) st
                         = case semSExcH s st of
                             Left (exc', st') | exc == exc' -> semSExcH sE st'
                                              | otherwise   -> Left (exc', st')
                             Right st' -> Right st'