git.iko.soy/Idris-dev
on 7afa310 help sign in
Idris-dev/libs/base/System/Concurrency/Process.idr
61 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.
14data Process : (msgType : Type) -> Type -> Type where
15 Lift : IO a -> Process msg a
17instance Functor (Process msg) where
18 map f (Lift a) = Lift (map f a)
20instance Applicative (Process msg) where
21 pure = Lift . return
22 (Lift f) <$> (Lift a) = Lift (f <$> a)
24instance Monad (Process msg) where
25 (Lift io) >>= k = Lift (do x <- io
26 case k x of
27 Lift v => v)
29run : Process msg x -> IO x
30run (Lift prog) = prog
32||| Get current process ID
33myID : Process msg (ProcID msg)
34myID = Lift (return (MkPID prim__vm))
36||| Send a message to another process
37send : ProcID msg -> msg -> Process msg ()
38send (MkPID p) m = Lift (sendToThread p (prim__vm, m))
40||| Return whether a message is waiting in the queue
41msgWaiting : Process msg Bool
42msgWaiting = Lift checkMsgs
44||| Receive a message - blocks if there is no message waiting
45recv : Process msg msg
46recv {msg} = do (senderid, m) <- Lift get
47 return m
48 where get : IO (Ptr, msg)
49 get = getMsg
51||| receive a message, and return with the sender's process ID.
52recvWithSender : Process msg (ProcID msg, msg)
53recvWithSender {msg}
54 = do (senderid, m) <- Lift get
55 return (MkPID senderid, m)
56 where get : IO (Ptr, msg)
57 get = getMsg
59create : Process msg () -> Process msg (ProcID msg)
60create (Lift p) = do ptr <- Lift (fork p)
61 return (MkPID ptr)