Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456
-- syntax of While type Var = String type Exc = 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 | Raise Exc | Handle Stm Exc Stm -- semantic categories for direct style denotational semantics type State = Var -> Integer type Cont = State -> State allzeros :: State allzeros x = 0 update :: Eq a => (a -> b) -> a -> b -> (a -> b) 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) type EnvE = Exc -> Cont allids :: EnvE allids e = id -- 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 cssemS :: Stm -> EnvE -> Cont -> Cont cssemS (x := a) envE c = c' where c' st = c (update st x (semA a st)) cssemS Skip envE c = c cssemS (s1 :\ s2) envE c = (cssemS s1 envE . cssemS s2 envE) c cssemS (If b s1 s2) envE c = cond (semB b, cssemS s1 envE c, cssemS s2 envE c) cssemS (While b s) envE c = fix f c where f g c = cond (semB b, (cssemS s envE . g) c, c) cssemS (Raise e) envE c = envE e cssemS (Handle s e s') envE c = cssemS s envE' c where envE' = update envE e (cssemS s' envE c) -- example {- fact is abstract syntax for y := 1 ; while not (x = 1) do (y := y * x ; x := x - 1) -} --fact :: Stm fact = Handle ( ("y" := Num 1) :\ (While (Not (Var "x" :== Num 1)) ( Handle ( (If (Not (Var "x" :== Num 7)) (("y" := (Var "y" :* Var "x")) :\ ("x" := (Var "x" :- Num 1)) ) (Raise "seitse") ) ) "seitse" --("x" := Num 3) (Raise "seitse") ) ) ) "seitse" ("x" := Num 1000) testfact :: Integer -> (Integer, Integer) testfact z = (st' "x", st' "y") where st' = cssemS fact allids id st where st = update allzeros "x" z