-- 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
          | Repeat Stm Bexp



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


-- 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 -> State -> State
dssemS (x := a) st     = update st x (semA a st)
dssemS Skip st         = st 
dssemS (s1 :\ s2) st   = (dssemS s2 . dssemS s1) st
                       -- dssemS s2  (dssemS s1 st)
dssemS (If b s1 s2) st = cond (semB b, dssemS s1, dssemS s2) st
                         --if semB b st then dssemS s1 st else dssemS s2 st
dssemS (While b s) st  = fix f st where
                           f g = cond (semB b, g . dssemS s, id)
                         --if (semB b st) then dssemS (While b s) (dssemS s st)
                         --               else st 
dssemS (Repeat s b) st = fix f st where
                           f g =  cond (semB b, id, g) . dssemS s  


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


repeatfact = (("x0" := Num 1) :\ ("y0" := Num 0)) :\
             Repeat 
               (((("x" := Var "x0") :\  fact) :\ ("y0" := (Var "y0" :+ Var "y"))) :\
                 ("x0" := (Var "x0" :+ Num 1)))
               (Var "x0" :== Num 5)

 
               

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