<br />
<b>Deprecated</b>:  The each() function is deprecated. This message will be suppressed on further calls in <b>/home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php</b> on line <b>456</b><br />
-- syntax of While

type Var = String

type Numl = Int

data Aexp = Var Var | Numl Numl 
          | Plus Aexp Aexp | Minus Aexp Aexp | Times Aexp Aexp

data Bexp = TrueBexp | FalseBexp | Eq Aexp Aexp | Leq Aexp Aexp 
          | Not Bexp | And Bexp Bexp | Or Bexp Bexp 

data Stm  = Ass Var Aexp | Skip | Seq Stm Stm
          | If Bexp Stm Stm | While Bexp Stm


-- semantic categories for direct style denotational semantics

type State = Var -> Int

bottom :: State
bottom x = bottom x

update :: State -> Var -> Int -> 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  :: ((State -> State) -> (State -> State)) -> (State -> State)
fix f = f (fix f)


-- direct style denotational semantics 

-- -- arithmetical expressions

semA :: Aexp -> State -> Int
semA (Var x) st       = st x
semA (Numl n) st      = n
semA (Plus a1 a2) st  = semA a1 st + semA a2 st 
semA (Minus a1 a2) st = semA a1 st - semA a2 st 
semA (Times a1 a2) st = semA a1 st * semA a2 st 


-- -- boolean expressions

semB :: Bexp -> State -> Bool
semB TrueBexp st    = True
semB FalseBexp st   = False
semB (Eq a1 a2) st  = semA a1 st == semA a2 st
semB (Leq a1 a2) st = semA a1 st <= semA a2 st
semB (Not b) st     = not (semB b st)
semB (And b1 b2) st = semB b1 st && semB b2 st
semB (Or b1 b2) st  = semB b1 st || semB b2 st


-- -- statements

dssemS :: Stm -> State -> State
dssemS (Ass x a) st    = update st x (semA a st)
dssemS Skip st         = st 
dssemS (Seq s1 s2) st  = (dssemS s2 . dssemS s1) st
dssemS (If b s1 s2) st = cond (semB b, dssemS s1, dssemS s2) st
dssemS (While b s) st  = fix f st where
                            f g = cond (semB b, g . dssemS s, id)


-- example

{-

   fact is abstract syntax for 

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

-}

fact :: Stm
fact = Seq (Ass "y" (Numl 1))
           (While (Not (Eq (Var "x") (Numl 1)))
                  (Seq (Ass "y" (Times (Var "y") (Var "x")))
                       (Ass "x" (Minus (Var "x") (Numl 1)))
                  )
           )

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