{----------------------------------------------------------------------------

            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

-----------------------------------------------------------------------------