Foo.hs

module Foo() where

{-@
data Message = Ping { pingPid :: Pid }
             | Pong { pongPid :: Pid } 
@-}

data Message = Ping Pid
             | Pong Pid

data Process a = P a
data Pid = Pid Int
         deriving Eq

instance Functor Process where
instance Applicative Process where
instance Monad Process where  

{-@ send :: Pid -> m:m -> Process () @-}
send :: Pid -> m -> Process ()
send p m = undefined

{-@ recv :: Process m @-}
recv :: Process m
recv = undefined

{-@ measure msgPid @-}               
{-@ msgPid :: x:Message -> {v:Pid | v = msgPid x} @-}
msgPid :: Message -> Pid               
msgPid (Ping p) = p
msgPid (Pong p) = p

{-@ foo :: Process () @-}
foo :: Process ()
foo = do x <- recv
         let p = case x of
                   Ping p -> p
                   Pong p -> p
         send p x