-- syntax of While

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



-- semantic categories for direct style denotational semantics

type State = Var -> Integer

allzeros :: State
allzeros x = 0

update :: State -> Var -> Integer -> State
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) outst@(_, st) = if pred st then g1 outst else g2 outst

fix :: (a -> a) -> a
--fix  :: ((State -> State) -> (State -> State)) -> (State -> State)
fix f = f (fix f)


-- 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
{-
dssemS :: Stm -> ([Integer], State) -> ([Integer], State)
dssemS (x := a) (out, st)  =  (out, update st x (semA a st))
dssemS Skip outst         = outst 
dssemS (s1 :\ s2) outst   = (dssemS s2 . dssemS s1) outst
dssemS (If b s1 s2) outst = cond (semB b, dssemS s1, dssemS s2) outst
dssemS (While b s) outst  = fix f outst where
                           f g = cond (semB b, g . dssemS s, id)
dssemS (Print a) (out, st) = (out ++ [semA a st], st)
-}

dssemS :: Stm -> State -> ([Integer], State)
dssemS (x := a) st        = ([], update st x (semA a st))
dssemS Skip st            = ([], st) 
dssemS (s1 :\ s2) st      = let (out', st') = dssemS s1 st
                                (out'', st'') = dssemS s2 st'
                            in (out' ++ out'', st'')
dssemS (If b s1 s2)    st = if semB b st then dssemS s1 st else dssemS s2 st
dssemS (While b s) st     = if semB b st then 
                                let (out', st') = dssemS s st
                                    (out'', st'') = dssemS (While b s) st'  
                                in (out' ++ out'', st'')
                            else ([], st)
dssemS (Print a) st       = ([semA a st], 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 T -- (Not (Var "x" :== Num 1))
                  ((("y" := (Var "y" :* Var "x")) :\
                       Print (Var "y"))    :\ ("x" := (Var "x" :- Num 1))
                  )
       )

               

--testfact :: Integer -> (Integer, Integer)
testfact z = (st' "y", outst') where 
               (outst', st') = dssemS fact st where
                 st  = update allzeros "x" z