git.iko.soy/Idris-dev
on b36dfcd help sign in
Idris-dev/lib/System/Concurrency/Process.idr
68 lines 1.7 kB history raw
1-- WARNING: No guarantees that this works properly yet!
3module System.Concurrency.Process
5import System.Concurrency.Raw
7%access public
9abstract
10data ProcID msg = MkPID Ptr
12-- Type safe message passing programs. Parameterised over the type of
13-- message which can be send, and the return type.
15data Process : (msgType : Type) -> Type -> Type where
16 lift : IO a -> Process msg a
18instance Functor (Process msg) where
19 map f (lift a) = lift (map f a)
21instance Applicative (Process msg) where
22 pure = lift . return
23 (lift f) <$> (lift a) = lift (f <$> a)
25instance Monad (Process msg) where
26 (lift io) >>= k = lift (do x <- io
27 case k x of
28 lift v => v)
30run : Process msg x -> IO x
31run (lift prog) = prog
33-- Get current process ID
35myID : Process msg (ProcID msg)
36myID = lift (return (MkPID prim__vm))
38-- Send a message to another process
40send : ProcID msg -> msg -> Process msg ()
41send (MkPID p) m = lift (sendToThread p (prim__vm, m))
43-- Return whether a message is waiting in the queue
45msgWaiting : Process msg Bool
46msgWaiting = lift checkMsgs
48-- Receive a message - blocks if there is no message waiting
50recv : Process msg msg
51recv {msg} = do (senderid, m) <- lift get
52 return m
53 where get : IO (Ptr, msg)
54 get = getMsg
56-- receive a message, and return with the sender's process ID.
58recvWithSender : Process msg (ProcID msg, msg)
59recvWithSender {msg}
60 = do (senderid, m) <- lift get
61 return (MkPID senderid, m)
62 where get : IO (Ptr, msg)
63 get = getMsg
65create : |(thread : Process msg ()) -> Process msg (ProcID msg)
66create (lift p) = do ptr <- lift (fork p)
67 return (MkPID ptr)