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 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 | Scan Var | Raise Exc | Handle Exc Stm Stm | Choose Stm Stm | Deadlock | ProbChoose Float 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' -- 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 -- nondeterminism {- -- defined in Prelude instance Monad [] where -- return :: a -> [a] return a = [a] -- (>>=) :: [a] -> (a -> [b]) -> [b] as >>= f = concat (map f as) -- as >>= f = [ b | a <- as, bs <- f a, b <- bs ] -} semSNDet :: Stm -> State -> [State] semSNDet (x ::= a) st = return (upd x (semA a st) st) semSNDet Skip st = return st semSNDet (s1 :\ s2) st = do st' <- semSNDet s1 st st'' <- semSNDet s2 st' return st'' semSNDet (If b s1 s2) st = if semB b st then semSNDet s1 st else semSNDet s2 st semSNDet (While b s) st = semSNDet (If b (s :\ While b s) Skip) st semSNDet (Choose s1 s2) st = semSNDet s1 st ++ semSNDet s2 st semSNDet Deadlock st = [] factNDet = ("y" ::= Num 1) :\ (While (Not (Var "x" :== Num 1)) ((Choose ("y" ::= (Var "y" :* Var "x")) Skip) :\ ("x" ::= (Var "x" :- Num 1)) ) ) testfactNDet :: Integer -> [(Integer, Integer)] testfactNDet z = do st <- semSNDet factNDet (upd "x" z empty) return (lkp "x" st, lkp "y" st) -- probabilistic choice data Dist a = Dist { undist :: [(Float, a)] } deriving Show instance Monad Dist where return a = Dist [(1.0, a)] Dist d >>= f = Dist [ (p * q, b) | (p, a) <- d, (q, b) <- undist (f a) ] semSPrC :: Stm -> State -> Dist State semSPrC (x ::= a) st = return (upd x (semA a st) st) semSPrC Skip st = return st semSPrC (s1 :\ s2) st = do st' <- semSPrC s1 st st'' <- semSPrC s2 st' return st'' semSPrC (If b s1 s2) st = if semB b st then semSPrC s1 st else semSPrC s2 st semSPrC (While b s) st = semSPrC (If b (s :\ While b s) Skip) st semSPrC (ProbChoose p s1 s2) st = Dist ([(p * q, st') | (q, st') <- undist (semSPrC s1 st) ] ++ [((1-p) * q, st') | (q, st') <- undist (semSPrC s2 st) ]) factPrC = ("y" ::= Num 1) :\ (While (Not (Var "x" :== Num 1)) ((ProbChoose (2/3) ("y" ::= (Var "y" :* Var "x")) Skip) :\ ("x" ::= (Var "x" :- Num 1)) ) ) testfactPrC :: Integer -> Dist (Integer, Integer) testfactPrC z = do st <- semSPrC factPrC (upd "x" z empty) return (lkp "x" st, lkp "y" st) -- a more complicated combined example: -- interactive input-output + nondeterminism data NDetIO a = Ret a | C (NDetIO a) (NDetIO a) | D | I (String -> NDetIO a) | O (String, NDetIO a) instance Monad NDetIO where return = Ret Ret a >>= f = f a C c1 c2 >>= f = C (c1 >>= f) (c2 >>= f) D >>= f = D I k >>= f = I (\ inp -> k inp >>= f) O (outp, c) >>= f = O (outp, c >>= f) semSNDetIO :: Stm -> State -> NDetIO State semSNDetIO (x ::= a) st = return (upd x (semA a st) st) semSNDetIO Skip st = return st semSNDetIO (s1 :\ s2) st = do st' <- semSNDetIO s1 st st'' <- semSNDetIO s2 st' return st'' semSNDetIO (If b s1 s2) st = if semB b st then semSNDetIO s1 st else semSNDetIO s2 st semSNDetIO (While b s) st = semSNDetIO (If b (s :\ While b s) Skip) st semSNDetIO (Print a) st = O (show (semA a st), return st) semSNDetIO (Scan x) st = I (\ str -> return (upd x (read str) st)) semSNDetIO (Choose s1 s2) st = C (semSNDetIO s1 st) (semSNDetIO s2 st) semSNDetIO Deadlock st = D factNDetIO = While T (Scan "x" :\ (("y" ::= Num 1) :\ ((While (Not (Var "x" :== Num 1)) ((Choose ("y" ::= (Var "y" :* Var "x")) Skip) :\ ("x" ::= (Var "x" :- Num 1)) ) ) :\ Print (Var "y") ) ) ) run :: NDetIO State -> IO State run (Ret st) = return st run (C c1 c2) = do putStr "Make a choice: " str <- getLine if read str then run c1 else run c2 run D = do putStr "Deadlock... " putChar '\n' run (I k) = do putStr "Give a number: " str <- getLine run (k str) run (O (str, c)) = do putStr str putChar '\n' run c testFactNDetIO :: IO (Integer, Integer) testFactNDetIO = do st <- run (semSNDetIO factNDetIO empty) return (lkp "x" st, lkp "y" st)