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
-- use with Hugs -98 -- needed for Jyri's dirty output import IOExts -- syntax of While type Var = String type Msg = 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 data Stm = Var ::= AExpr | Skip | Stm :\ Stm | If BExpr Stm Stm | While BExpr Stm -- extensions | Print AExpr | Raise Exc | Handle Exc Stm Stm -- semantic categories for denotational semantics type State = Var -> Integer empty :: State empty x = error ("variable " ++ x ++ " has no value") -- empty x = undefined lkp :: Var -> State -> Integer lkp x st = st x upd :: Var -> Integer -> State -> State --upd x n st = \ x' -> if x' == x then n else st x' upd x n st = st' where st' x' | x' == x = n | otherwise = st x' -- denotational semantics -- -- arithmetical expressions semA :: AExpr -> State -> Integer semA (Var x) st = lkp 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 -- -- statements -- pure While semS :: Stm -> State -> State semS (x ::= a) st = upd x (semA a st) st semS Skip st = st semS (s1 :\ s2) st = semS s2 (semS s1 st) semS (If b s1 s2) st = if semB b st then semS s1 st else semS s2 st semS (While b s) st = if semB b st then semS (While b s) (semS s st) else st -- semS (While b s) st = semS (If b (s :\ While b s) Skip) st -- 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)) ) ) testfact :: Integer -> (Integer, Integer) testfact z = (lkp "x" st, lkp "y" st) where st = semS fact (upd "x" z empty) -- extension with output {- semSPrint :: Stm -> State -> ([Integer], State) semSPrint (x ::= a) st = ([], upd x (semA a st) st) semSPrint Skip st = ([], st) semSPrint (s1 :\ s2) st = (is ++ is', st'') where (is, st') = semSPrint s1 st (is', st'') = semSPrint s2 st' semSPrint (If b s1 s2) st = if semB b st then semSPrint s1 st else semSPrint s2 st semSPrint (While b s) st = semSPrint (If b (s :\ While b s) Skip) st semSPrint (Print a) st = ([semA a st], st) -} -- same but using the overt monad explicitly {- - defined in Prelude class Monad m where return :: a -> m a (>>=) :: m a -> (a -> m b) -> m b -} -- this instance declaration requires hugs -98 !! instance Monad ((,) [e]) where -- return :: a -> ([e], a) return a = ([], a) -- (>>=) :: ([e], a) -> (a -> ([e], b)) -> ([e], b) (es, a) >>= f = (es ++ es', b) where (es', b) = f a {- -- defined in Prelude primitive putChar :: Char -> IO () primitive putStr :: String -> IO () putStrLn :: String -> IO () putStrLn s = do putStr s putChar '\n' print :: Show a => a -> IO () print = putStrLn . show primitive primretIO :: a -> IO a primitive primbindIO :: IO a -> (a -> IO b) -> IO b instance Monad IO where return = primretIO (>>=) = primbindIO -} semSOutp :: Stm -> State -> ([Integer], State) -- alternatively, using the IO monad -- semSOutp :: Stm -> State -> IO State semSOutp (x ::= a) st = return (upd x (semA a st) st) semSOutp Skip st = return st semSOutp (s1 :\ s2) st = do st' <- semSOutp s1 st st'' <- semSOutp s2 st' return st'' {- -- syntactic sugar for : semSOutp (s1 :\ s2) st = semSOutp s1 st >>= \ st' -> semSOutp s2 st' >>= \ st'' -> return st'' = semSOutp s1 st >>= semSOutp s2 -} semSOutp (If b s1 s2) st = if semB b st then semSOutp s1 st else semSOutp s2 st semSOutp (While b s) st = semSOutp (If b (s :\ While b s) Skip) st semSOutp (Print a) st = ([semA a st], st) -- alternatively -- semSOutp (Print a) st = do { print (semA a st) ; return st } factOutp = ("y" ::= Num 1) :\ (While (Not (Var "x" :== Num 1)) (("y" ::= (Var "y" :* Var "x")) :\ (("x" ::= (Var "x" :- Num 1)) :\ (Print (Var "x") :\ Print (Var "y")) ) ) ) natsOutp = ("x" ::= Num 1) :\ (While T (Print (Var "x") :\ ("x" ::= (Var "x" :+ Num 1)))) testfactOutp :: Integer -> ([Integer], (Integer, Integer)) -- alternatively -- testfactOutp :: Integer -> IO (Integer, Integer) testfactOutp z = do st <- semSOutp factOutp (upd "x" z empty) return (lkp "x" st, lkp "y" st) testnatsOutp :: ([Integer], Integer) -- alternatively -- testnatsOutp :: IO Integer testnatsOutp = do st <- semSOutp natsOutp empty return (lkp "x" st) -- output real dirty as Jyri wants to have it, requires IOExts {- -- defined in IOExts unsafePerformIO :: IO a -> a -} {- unsafePrint :: Show a => a -> () unsafePrint a = unsafePerformIO (print a) semS :: Stm -> State -> State semS (x ::= a) st = upd x (semA a st) st semS Skip st = st semS (s1 :\ s2) st = semS s2 (semS s1 st) semS (If b s1 s2) st = if semB b st then semS s1 st else semS s2 st semS (While b s) st = semS (If b (s :\ While b s) Skip) st semS (Print a) st = case unsafePrint (semA a st) of () -> st testfactOutp :: Integer -> (Integer, Integer) testfactOutp z = (lkp "x" st, lkp "y" st) where st = semS factOutp (upd "x" z empty) testnatsOutp :: Integer -> Integer testnatsOutp = lkp "x" st where st = semS natsOutp empty -} -- exceptions (without handling) {- -- defined in Prelude Either a b = Left a | Right b -} instance Monad (Either e) where -- return :: e -> Either e a return = Right -- (>>=) :: Either e a -> (a -> Either e b) -> Either e b Left e >>= f = Left e Right a >>= f = f a -- note everything is as before, only the monad has changed -- and instead of Print we have supported Raise type Exc = String semSExc :: Stm -> State -> Either Exc State semSExc (x ::= a) st = return (upd x (semA a st) st) semSExc Skip st = return st semSExc (s1 :\ s2) st = do st' <- semSExc s1 st st'' <- semSExc s2 st' return st'' semSExc (If b s1 s2) st = if semB b st then semSExc s1 st else semSExc s2 st semSExc (While b s) st = semSExc (If b (s :\ While b s) Skip) st semSExc (Raise exc) st = Left exc factExc = If (Var "x" :<= Num 0) (Raise "input to fact must be pos") (("y" ::= Num 1) :\ (While (Not (Var "x" :== Num 1)) (("y" ::= (Var "y" :* Var "x")) :\ ("x" ::= (Var "x" :- Num 1)) ) ) ) testfactExc :: Integer -> Either Exc (Integer, Integer) testfactExc z = do st <- semSExc factExc (upd "x" z empty) return (lkp "x" st, lkp "y" st) -- exceptions with handling semSExcH :: Stm -> State -> Either (Exc, State) State semSExcH (x ::= a) st = return (upd x (semA a st) st) semSExcH Skip st = return st semSExcH (s1 :\ s2) st = do st' <- semSExcH s1 st st'' <- semSExcH s2 st' return st'' semSExcH (If b s1 s2) st = if semB b st then semSExcH s1 st else semSExcH s2 st semSExcH (While b s) st = semSExcH (If b (s :\ While b s) Skip) st semSExcH (Raise exc) st = Left (exc, st) semSExcH (Handle exc sE s) st = case semSExcH s st of Left (exc', st') | exc == exc' -> semSExcH sE st' | otherwise -> Left (exc', st') Right st' -> Right st'