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 Exc 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 type Exception = String data Stm = Ass Var Aexp | Skip | Seq Stm Stm | If Bexp Stm Stm | While Bexp Stm | HandleIn Stm Exception Stm | Raise Exception -- semantic categories for continuation style denotational semantics type State = Var -> Int bottomState :: State bottomState x = bottomState x updateState :: State -> Var -> Int -> State updateState 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 :: ((Cont -> Cont) -> (Cont -> Cont)) -> (Cont -> Cont) fix f = f (fix f) type Cont = State -> State type EnvE = Exception -> Cont bottomEnvE :: EnvE bottomEnvE e = bottomEnvE e updateEnvE :: EnvE -> Exception -> Cont -> EnvE updateEnvE envE e' c e = if e == e' then c else envE e -- continuation 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 cssemS :: Stm -> EnvE -> Cont -> Cont cssemS (Ass x a) envE c st = c (updateState st x (semA a st)) cssemS Skip envE c st = c st cssemS (Seq s1 s2) envE c st = (cssemS s1 envE . cssemS s2 envE) c st cssemS (If b s1 s2) envE c st = cond (semB b, cssemS s1 envE c, cssemS s2 envE c) st cssemS (While b s) envE c st = fix f c st where f g c = cond (semB b, (cssemS s envE . g) c, c) cssemS (HandleIn s1 e s2) envE c st = cssemS s1 (updateEnvE envE e (cssemS s2 envE c)) c st cssemS (Raise e) envE c st = envE e st -- example {- loop is abstract syntax for begin while true do if x <= 0 then raise exit else x := x - 1 handle exit : y := 7 end -} loop :: Stm loop = HandleIn (While TrueBexp (If (Leq (Var "x") (Numl 0)) (Raise "exit") (Ass "x" (Minus (Var "x") (Numl 1))) ) ) "exit" (Ass "y" (Numl 7)) testloop :: Int -> (Int, Int) testloop z = (st' "x", st' "y") where st' = cssemS loop envE c st where envE = bottomEnvE c = id st = updateState bottomState "x" z