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
-- While extended with block structures and procedures -- syntax type Var = String type Pname = String data AExpr = Var Var | Num Integer | AExpr :+ AExpr | AExpr :- AExpr | AExpr :* AExpr data BExpr = T | F | AExpr :== AExpr | AExpr :<= AExpr | Not BExpr | BExpr :&& BExpr | BExpr :|| BExpr type DecV = [(Var, AExpr)] type DecP = [(Pname, Stm)] data Stm = Var ::= AExpr | Skip | Stm :\ Stm | If BExpr Stm Stm | While BExpr Stm | Block DecV DecP Stm | Call Pname -- semantic categories for direct style denotational semantics type Loc = Integer next :: Loc next = -1 new :: Loc -> Loc new l = l + 1 type Store = Loc -> Integer emptyStore :: Store emptyStore _ = undefined updStore :: Loc -> Integer -> Store -> Store updStore l n sto l' = if l' == l then n else sto l' lkpStore :: Loc -> Store -> Integer lkpStore l sto = sto l type EnvV = Var -> Loc emptyEnvV :: EnvV emptyEnvV _ = undefined updEnvV :: Var -> Loc -> EnvV -> EnvV updEnvV x l envV x' = if x' == x then l else envV x' lkpEnvV :: Var -> EnvV -> Loc lkpEnvV x envV = envV x type EnvP = Pname -> (Store -> Store) emptyEnvP :: EnvP emptyEnvP _ = undefined updEnvP :: Pname -> (Store -> Store) -> EnvP -> EnvP updEnvP p g envP p' = if p' == p then g else envP p' lkpEnvP :: Pname -> EnvP -> (Store -> Store) lkpEnvP p envP = envP p type State = Var -> Integer lkpState :: Var -> State -> Integer lkpState x st = st x mkState :: EnvV -> Store -> State mkState envV sto = sto . envV -- denotational semantics -- -- arithmetical expressions semA :: AExpr -> State -> Integer semA (Var x) st = lkpState x st 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 :: BExpr -> 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 -- -- variable declaration lists semDV :: DecV -> EnvV -> Store -> (EnvV, Store) semDV [] envV sto = (envV, sto) semDV ((x, a) : decV) envV sto = semDV decV (updEnvV x l envV) (updStore next (new l) $ updStore l v sto) where l = lkpStore next sto v = semA a (mkState envV sto) -- -- procedure declaration lists semDP :: DecP -> EnvV -> EnvP -> EnvP semDP [] envV envP = envP semDP ((p, s) : decP) envV envP = semDP decP envV (updEnvP p g envP) where g = semS s envV envP -- -- statements semS :: Stm -> EnvV -> EnvP -> (Store -> Store) semS (x ::= a) envV envP sto = updStore l (semA a (mkState envV sto)) sto where l = lkpEnvV x envV semS Skip envV envP sto = sto semS (s1 :\ s2) envV envP sto = semS s2 envV envP $ semS s1 envV envP sto semS (If b s1 s2) envV envP sto = if semB b (mkState envV sto) then semS s1 envV envP sto else semS s2 envV envP sto semS (While b s) envV envP sto = semS (If b (s :\ While b s) Skip) envV envP sto semS (Block decV decP s) envV envP sto = semS s envV' envP' sto' where (envV', sto') = semDV decV envV sto envP' = semDP decP envV' envP semS (Call p) envV envP sto = lkpEnvP p envP sto -- example {- useless is abstract syntax for begin var x := 7 ; proc p is x := 0 ; begin var x := 5; call p end end -} useless :: Stm useless = Block [("x", Num 7)] [("p", "x" ::= Num 0)] (Block [("x", Num 5)] [] (Call "p") ) testuseless :: (Integer, Integer, Integer) testuseless = (sto' 12, sto' 13, sto' next) where sto' = semS useless envV envP sto where envV = emptyEnvV envP = emptyEnvP sto = updStore next 12 emptyStore