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
{---------------------------------------------------------------------------- What is the Meaning of These Constant Interruptions? Graham Hutton and Joel Wright University of Nottingham March 2007 Instructions: 1) Download QuickCheck.hs from the web 2) Load the present file into Hugs 3) Enter "quickCheck correct" 4) See that 100 tests are passed! ----------------------------------------------------------------------------} import List import QuickCheck ----------------------------------------------------------------------------- -- Type declarations ----------------------------------------------------------------------------- data Expr = Val Int | Throw | Add Expr Expr | Seqn Expr Expr | Catch Expr Expr | Block Expr | Unblock Expr deriving (Show, Eq, Ord) data Status = B | U deriving (Show, Eq, Ord) type Stack = [Item] data Item = VAL Int | HAN Code | INT Status deriving (Show, Eq, Ord) type Code = [Op] data Op = PUSH Int | THROW | ADD | POP | MARK Code | UNMARK | SET Status | RESET deriving (Show, Eq, Ord) ----------------------------------------------------------------------------- -- Auxiliary functions on trees ----------------------------------------------------------------------------- data Tree a = Node a [Tree a] deriving (Show, Eq, Ord) leaves :: Tree a -> [a] leaves (Node x []) = [x] leaves (Node _ ts) = concat (map leaves ts) unfold :: (a -> [a]) -> a -> Tree a unfold f x = Node x [unfold f x' | x' <- f x] ----------------------------------------------------------------------------- -- Expression generator for quickcheck ----------------------------------------------------------------------------- instance Arbitrary Expr where arbitrary = sized arbExpr arbExpr :: Int -> Gen Expr arbExpr 0 = frequency [(6, do n <- arbitrary return (Val n)), (1, return Throw)] arbExpr n = frequency [(6, arbExpr 0), (3, do x <- arbExpr' y <- arbExpr' return (Add x y)), (3, do x <- arbExpr' y <- arbExpr' return (Seqn x y)), (3, do x <- arbExpr' y <- arbExpr' return (Catch x y)), (3, do x <- arbExpr (n-1) return (Block x)), (3, do x <- arbExpr (n-1) return (Unblock x))] where arbExpr' = arbExpr (n `div` 2) ----------------------------------------------------------------------------- -- Evaluation semantics ----------------------------------------------------------------------------- semantics :: Expr -> [Expr] semantics e = bigstep e U bigstep :: Expr -> Status -> [Expr] bigstep e B = eval e B bigstep e U = eval e U ++ [Throw] eval :: Expr -> Status -> [Expr] eval (Val n) i = [Val n] eval (Throw) i = [Throw] eval (Block x) i = bigstep x B eval (Unblock x) i = bigstep x U eval (Add x y) i = [Val (n+m) | Val n <- bigstep x i, Val m <- bigstep y i] ++ [Throw | Throw <- bigstep x i] ++ [Throw | Val n <- bigstep x i, Throw <- bigstep y i] eval (Seqn x y) i = [v | Val n <- bigstep x i, v <- bigstep y i] ++ [Throw | Throw <- bigstep x i] eval (Catch x y) i = [Val n | Val n <- bigstep x i] ++ [v | Throw <- bigstep x i, v <- bigstep y i] ----------------------------------------------------------------------------- -- Virtual machine ----------------------------------------------------------------------------- data State = TRIP Code Status Stack | PAIR Status Stack deriving (Show, Eq, Ord) machine :: State -> [State] machine s = leaves (unfold smallstep s) smallstep :: State -> [State] smallstep (TRIP ops i s) | null ops = [] | i == U = [trans (TRIP ops i s), PAIR U s] | otherwise = [trans (TRIP ops i s)] smallstep (PAIR i s) | null s = [] | otherwise = [trans (PAIR i s)] trans :: State -> State trans (TRIP (PUSH n : ops) i s) = TRIP ops i (VAL n : s) trans (TRIP (THROW : ops) i s) = PAIR i s trans (TRIP (ADD : ops) i (VAL m : VAL n : s)) = TRIP ops i (VAL (n+m) : s) trans (TRIP (POP : ops) i (VAL _ : s)) = TRIP ops i s trans (TRIP (MARK ops' : ops) i s) = TRIP ops i (HAN ops' : s) trans (TRIP (UNMARK : ops) i (x : HAN _ : s)) = TRIP ops i (x:s) trans (TRIP (SET i' : ops) i s) = TRIP ops i' (INT i : s) trans (TRIP (RESET : ops) _ (x : INT i' : s)) = TRIP ops i' (x : s) trans (PAIR i (VAL _ : s)) = PAIR i s trans (PAIR _ (INT i' : s)) = PAIR i' s trans (PAIR i (HAN ops : s)) = TRIP ops i s ----------------------------------------------------------------------------- -- Compiler ----------------------------------------------------------------------------- comp :: Expr -> Code -> Code comp (Val n) ops = PUSH n : ops comp (Throw) ops = THROW : ops comp (Add x y) ops = comp x (comp y (ADD : ops)) comp (Seqn x y) ops = comp x (POP : comp y ops) comp (Catch x y) ops = MARK (comp y ops) : comp x (UNMARK : ops) comp (Block x) ops = SET B : comp x (RESET : ops) comp (Unblock x) ops = SET U : comp x (RESET : ops) ----------------------------------------------------------------------------- -- Compiler correctness ----------------------------------------------------------------------------- correct :: Expr -> Bool correct e = equiv (semantics e) (machine s) where s = TRIP (comp e []) U [] equiv :: [Expr] -> [State] -> Bool equiv es sts = sort (nub es) == sort (nub (map unload sts)) unload :: State -> Expr unload (TRIP [] _ [VAL n]) = Val n unload (PAIR _ []) = Throw -----------------------------------------------------------------------------